Theorem osumlem3 5532

Description: Lemma for osum 5538.

Hypotheses

Ref	Expression
osumlem1.1	|- A e. CH
osumlem1.2	|- B e. CH
osumlem1.3	|- B (_ (_|_` A)
osumlem1.4	|- (ph <-> (((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))))

Assertion

Ref	Expression
osumlem3	|- (ph -> (norm` (D -v y)) <_ (norm` (R -v z)))

Proof of Theorem osumlem3

Step	Hyp	Ref	Expression
1		osumlem1.4	. 2 |- (ph <-> (((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))))
2		osumlem1.1	. . . . . . 7 |- A e. CH
3		osumlem1.2	. . . . . . 7 |- B e. CH
4		osumlem1.3	. . . . . . 7 |- B (_ (_|_` A)
5		pm4.2 148	. . . . . . 7 |- ((((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) <-> (((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))))
6	2, 3, 4, 5	osumlem1 5530	. . . . . 6 |- ((((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> (((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)))
7		hvsubclt 4998	. . . . . . . . . . 11 |- ((C e. H~ /\ x e. H~) -> (C -v x) e. H~)
8	7	adantrr 312	. . . . . . . . . 10 |- ((C e. H~ /\ (x e. H~ /\ y e. H~)) -> (C -v x) e. H~)
9	8	adantlr 310	. . . . . . . . 9 |- (((C e. H~ /\ D e. H~) /\ (x e. H~ /\ y e. H~)) -> (C -v x) e. H~)
10	9	adantrr 312	. . . . . . . 8 |- (((C e. H~ /\ D e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> (C -v x) e. H~)
11	10	adantlr 310	. . . . . . 7 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> (C -v x) e. H~)
12		normclt 5076	. . . . . . 7 |- ((C -v x) e. H~ -> (norm` (C -v x)) e. RR)
13	11, 12	syl 12	. . . . . 6 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> (norm` (C -v x)) e. RR)
14		sqege0t 4708	. . . . . 6 |- ((norm` (C -v x)) e. RR -> 0 <_ ((norm` (C -v x))^2))
15	6, 13, 14	3syl 21	. . . . 5 |- ((((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> 0 <_ ((norm` (C -v x))^2))
16		ax0re 4063	. . . . . . . 8 |- 0 e. RR
17	16	a1i 7	. . . . . . 7 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> 0 e. RR)
18		sqreclt 4697	. . . . . . . 8 |- ((norm` (C -v x)) e. RR -> ((norm` (C -v x))^2) e. RR)
19	11, 12, 18	3syl 21	. . . . . . 7 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> ((norm` (C -v x))^2) e. RR)
20		hvsubclt 4998	. . . . . . . . . . . 12 |- ((D e. H~ /\ y e. H~) -> (D -v y) e. H~)
21	20	adantrl 311	. . . . . . . . . . 11 |- ((D e. H~ /\ (x e. H~ /\ y e. H~)) -> (D -v y) e. H~)
22	21	adantll 309	. . . . . . . . . 10 |- (((C e. H~ /\ D e. H~) /\ (x e. H~ /\ y e. H~)) -> (D -v y) e. H~)
23	22	adantrr 312	. . . . . . . . 9 |- (((C e. H~ /\ D e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> (D -v y) e. H~)
24	23	adantlr 310	. . . . . . . 8 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> (D -v y) e. H~)
25		normclt 5076	. . . . . . . 8 |- ((D -v y) e. H~ -> (norm` (D -v y)) e. RR)
26		sqreclt 4697	. . . . . . . 8 |- ((norm` (D -v y)) e. RR -> ((norm` (D -v y))^2) e. RR)
27	24, 25, 26	3syl 21	. . . . . . 7 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> ((norm` (D -v y))^2) e. RR)
28	17, 19, 27	3jca 604	. . . . . 6 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> (0 e. RR /\ ((norm` (C -v x))^2) e. RR /\ ((norm` (D -v y))^2) e. RR))
29		leadd1t 4350	. . . . . 6 |- ((0 e. RR /\ ((norm` (C -v x))^2) e. RR /\ ((norm` (D -v y))^2) e. RR) -> (0 <_ ((norm` (C -v x))^2) <-> (0 + ((norm` (D -v y))^2)) <_ (((norm` (C -v x))^2) + ((norm` (D -v y))^2))))
30	6, 28, 29	3syl 21	. . . . 5 |- ((((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> (0 <_ ((norm` (C -v x))^2) <-> (0 + ((norm` (D -v y))^2)) <_ (((norm` (C -v x))^2) + ((norm` (D -v y))^2))))
31	15, 30	mpbid 170	. . . 4 |- ((((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> (0 + ((norm` (D -v y))^2)) <_ (((norm` (C -v x))^2) + ((norm` (D -v y))^2)))
32	27	recnd 4099	. . . . 5 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> ((norm` (D -v y))^2) e. CC)
33		addid2t 4132	. . . . 5 |- (((norm` (D -v y))^2) e. CC -> (0 + ((norm` (D -v y))^2)) = ((norm` (D -v y))^2))
34	6, 32, 33	3syl 21	. . . 4 |- ((((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> (0 + ((norm` (D -v y))^2)) = ((norm` (D -v y))^2))
35	2, 3, 4, 5	osumlem2 5531	. . . 4 |- ((((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> (((norm` (C -v x))^2) + ((norm` (D -v y))^2)) = ((norm` (R -v z))^2))
36	31, 34, 35	3brtr3d 2086	. . 3 |- ((((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> ((norm` (D -v y))^2) <_ ((norm` (R -v z))^2))
37		hvsubclt 4998	. . . . . . 7 |- ((R e. H~ /\ z e. H~) -> (R -v z) e. H~)
38	37	adantrl 311	. . . . . 6 |- ((R e. H~ /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> (R -v z) e. H~)
39	38	adantll 309	. . . . 5 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> (R -v z) e. H~)
40	24, 39	jca 236	. . . 4 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> ((D -v y) e. H~ /\ (R -v z) e. H~))
41		le2sqet 4707	. . . . 5 |- (((norm` (D -v y)) e. RR /\ (norm` (R -v z)) e. RR) -> ((0 <_ (norm` (D -v y)) /\ 0 <_ (norm` (R -v z))) -> ((norm` (D -v y)) <_ (norm` (R -v z)) <-> ((norm` (D -v y))^2) <_ ((norm` (R -v z))^2))))
42		normclt 5076	. . . . . 6 |- ((R -v z) e. H~ -> (norm` (R -v z)) e. RR)
43	25, 42	anim12i 268	. . . . 5 |- (((D -v y) e. H~ /\ (R -v z) e. H~) -> ((norm` (D -v y)) e. RR /\ (norm` (R -v z)) e. RR))
44		normge0t 5077	. . . . . 6 |- ((D -v y) e. H~ -> 0 <_ (norm` (D -v y))