HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version
Theorem osumlem3 9575
Description: Lemma for osum 9581.
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 +h D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +h y))))
Assertion
Ref Expression
osumlem3 |- (ph -> (normh` (D -h y)) <_ (normh` (R -h z)))
Proof of Theorem osumlem3
StepHypRef Expression
1 osumlem1.4 . 2 |- (ph <-> (((C e. A /\ D e. B) /\ R = (C +h D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +h y))))
2 osumlem1.1 . . . . . . 7 |- A e. CH
3 osumlem1.2 . . . . . . 7 |- B e. CH
4 osumlem1.3 . . . . . . 7 |- B (_ (_|_` A)
5 pm4.2 170 . . . . . . 7 |- ((((C e. A /\ D e. B) /\ R = (C +h D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +h y))) <-> (((C e. A /\ D e. B) /\ R = (C +h D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +h y))))
62, 3, 4, 5osumlem1 9573 . . . . . 6 |- ((((C e. A /\ D e. B) /\ R = (C +h D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +h y))) -> (((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)))
7 hvsubclt 8882 . . . . . . . . 9 |- ((C e. H~ /\ x e. H~) -> (C -h x) e. H~)
87ad2ant2r 411 . . . . . . . 8 |- (((C e. H~ /\ D e. H~) /\ (x e. H~ /\ y e. H~)) -> (C -h x) e. H~)
98ad2ant2r 411 . . . . . . 7 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> (C -h x) e. H~)
10 normclt 8986 . . . . . . 7 |- ((C -h x) e. H~ -> (normh` (C -h x)) e. RR)
119, 10syl 10 . . . . . 6 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> (normh` (C -h x)) e. RR)
12 sqge0t 6634 . . . . . 6 |- ((normh` (C -h x)) e. RR -> 0 <_ ((normh` (C -h x))^2))
136, 11, 123syl 20 . . . . 5 |- ((((C e. A /\ D e. B) /\ R = (C +h D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +h y))) -> 0 <_ ((normh` (C -h x))^2))
14 0re 5452 . . . . . . . 8 |- 0 e. RR
1514a1i 8 . . . . . . 7 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> 0 e. RR)
16 resqclt 6622 . . . . . . . 8 |- ((normh` (C -h x)) e. RR -> ((normh` (C -h x))^2) e. RR)
179, 10, 163syl 20 . . . . . . 7 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> ((normh` (C -h x))^2) e. RR)
18 hvsubclt 8882 . . . . . . . . . 10 |- ((D e. H~ /\ y e. H~) -> (D -h y) e. H~)
1918ad2ant2l 410 . . . . . . . . 9 |- (((C e. H~ /\ D e. H~) /\ (x e. H~ /\ y e. H~)) -> (D -h y) e. H~)
2019ad2ant2r 411 . . . . . . . 8 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> (D -h y) e. H~)
21 normclt 8986 . . . . . . . 8 |- ((D -h y) e. H~ -> (normh` (D -h y)) e. RR)
22 resqclt 6622 . . . . . . . 8 |- ((normh` (D -h y)) e. RR -> ((normh` (D -h y))^2) e. RR)
2320, 21, 223syl 20 . . . . . . 7 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> ((normh` (D -h y))^2) e. RR)
2415, 17, 233jca 821 . . . . . 6 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> (0 e. RR /\ ((normh` (C -h x))^2) e. RR /\ ((normh` (D -h y))^2) e. RR))
25 leadd1t 5637 . . . . . 6 |- ((0 e. RR /\ ((normh` (C -h x))^2) e. RR /\ ((normh` (D -h y))^2) e. RR) -> (0 <_ ((normh` (C -h x))^2) <-> (0 + ((normh` (D -h y))^2)) <_ (((normh` (C -h x))^2) + ((normh` (D -h y))^2))))
266, 24, 253syl 20 . . . . 5 |- ((((C e. A /\ D e. B) /\ R = (C +h D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +h y))) -> (0 <_ ((normh` (C -h x))^2) <-> (0 + ((normh` (D -h y))^2)) <_ (((normh` (C -h x))^2) + ((normh` (D -h y))^2))))
2713, 26mpbid 195 . . . 4 |- ((((C e. A /\ D e. B) /\ R = (C +h D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +h y))) -> (0 + ((normh` (D -h y))^2)) <_ (((normh` (C -h x))^2) + ((normh` (D -h y))^2)))
2823recnd 5327 . . . . 5 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> ((normh` (D -h y))^2) e. CC)
29 addid2t 5341 . . . . 5 |- (((normh` (D -h y))^2) e. CC -> (0 + ((normh` (D -h y))^2)) = ((normh` (D -h y))^2))
306, 28, 293syl 20 . . . 4 |- ((((C e. A /\ D e. B) /\ R = (C +h D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +h y))) -> (0 + ((normh` (D -h y))^2)) = ((normh` (D -h y))^2))
312, 3, 4, 5osumlem2 9574 . . . 4 |- ((((C e. A /\ D e. B) /\ R = (C +h D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +h y))) -> (((normh` (C -h x))^2) + ((normh` (D -h y))^2)) = ((normh` (R -h z))^2))
3227, 30, 313brtr3d 2649 . . 3 |- ((((C e. A /\ D e. B) /\ R = (C +h D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +h y))) -> ((normh` (D -h y))^2) <_ ((normh` (R -h z))^2))
33 hvsubclt 8882 . . . . . 6 |- ((R e. H~ /\ z e. H~) -> (R -h z) e. H~)
3433ad2ant2l 410 . . . . 5 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> (R -h z) e. H~)
3520, 34jca 288 . . . 4 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> ((D -h y) e. H~ /\ (R -h z) e. H~))
36 le2sqt 6632 . . . . 5 |- ((((normh` (D -h y)) e. RR /\ 0 <_ (normh` (D -h y))) /\ ((normh` (R -h z)) e. RR /\ 0 <_ (normh` (R -h z)))) -> ((normh` (D -h y)) <_ (normh` (R -h z)) <-> ((normh` (D -h y))^2) <_ ((normh` (R -h z))^2)))
37 normge0t 8987 . . . . . 6 |- ((D -h y) e. H~ -> 0 <_ (normh` (D -h y)))
3821, 37jca 288 . . . . 5 |- ((D -h y) e. H~ -> ((normh` (D -h y)) e. RR /\ 0 <_ (normh` (D -h y))))
39 normclt 8986 . . . . . 6 |- ((R -h z) e. H~ -> (normh` (R -h z)) e. RR)
40 normge0t 8987 . . . . . 6 |- ((R -h z) e. H~ -> 0 <_ (normh` (R -h z)))
4139, 40jca 288 . . . . 5 |- ((R -h z) e. H~ -> ((normh` (R -h z)) e. RR /\ 0 <_ (normh` (R -h z))))
4236, 38, 41syl2an 456 . . . 4 |- (((D -h y) e. H~ /\ (R -h z) e. H~) -> ((normh` (D -h y)) <_ (normh` (R -h z)) <-> ((normh` (D -h y))^2) <_ ((normh` (R -h z))^2)))
436, 35, 423syl 20 . . 3 |- ((