Metamath Proof Explorer

Theorem pjhthlem1

Description: Lemma for pjhth . (Contributed by NM, 10-Oct-1999) (Revised by Mario Carneiro, 15-May-2014) (Proof shortened by AV, 10-Jul-2022) (New usage is discouraged.)

Ref Expression
Hypotheses pjhth.1 
|- H e. CH
pjhth.2 
|- ( ph -> A e. ~H )
pjhth.3 
|- ( ph -> B e. H )
pjhth.4 
|- ( ph -> C e. H )
pjhth.5 
|- ( ph -> A. x e. H ( normh ` ( A -h B ) ) <_ ( normh ` ( A -h x ) ) )
pjhth.6 
|- T = ( ( ( A -h B ) .ih C ) / ( ( C .ih C ) + 1 ) )
Assertion pjhthlem1 
|- ( ph -> ( ( A -h B ) .ih C ) = 0 )

Proof

Step Hyp Ref Expression
1 pjhth.1 
 |-  H e. CH
2 pjhth.2 
 |-  ( ph -> A e. ~H )
3 pjhth.3 
 |-  ( ph -> B e. H )
4 pjhth.4 
 |-  ( ph -> C e. H )
5 pjhth.5 
 |-  ( ph -> A. x e. H ( normh ` ( A -h B ) ) <_ ( normh ` ( A -h x ) ) )
6 pjhth.6 
 |-  T = ( ( ( A -h B ) .ih C ) / ( ( C .ih C ) + 1 ) )
7 1 cheli 
 |-  ( B e. H -> B e. ~H )
8 3 7 syl 
 |-  ( ph -> B e. ~H )
9 hvsubcl 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A -h B ) e. ~H )
10 2 8 9 syl2anc 
 |-  ( ph -> ( A -h B ) e. ~H )
11 1 cheli 
 |-  ( C e. H -> C e. ~H )
12 4 11 syl 
 |-  ( ph -> C e. ~H )
13 hicl 
 |-  ( ( ( A -h B ) e. ~H /\ C e. ~H ) -> ( ( A -h B ) .ih C ) e. CC )
14 10 12 13 syl2anc 
 |-  ( ph -> ( ( A -h B ) .ih C ) e. CC )
15 14 abscld 
 |-  ( ph -> ( abs ` ( ( A -h B ) .ih C ) ) e. RR )
16 15 recnd 
 |-  ( ph -> ( abs ` ( ( A -h B ) .ih C ) ) e. CC )
17 15 resqcld 
 |-  ( ph -> ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) e. RR )
18 17 renegcld 
 |-  ( ph -> -u ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) e. RR )
19 hiidrcl 
 |-  ( C e. ~H -> ( C .ih C ) e. RR )
20 12 19 syl 
 |-  ( ph -> ( C .ih C ) e. RR )
21 2re 
 |-  2 e. RR
22 readdcl 
 |-  ( ( ( C .ih C ) e. RR /\ 2 e. RR ) -> ( ( C .ih C ) + 2 ) e. RR )
23 20 21 22 sylancl 
 |-  ( ph -> ( ( C .ih C ) + 2 ) e. RR )
24 0red 
 |-  ( ph -> 0 e. RR )
25 peano2re 
 |-  ( ( C .ih C ) e. RR -> ( ( C .ih C ) + 1 ) e. RR )
26 20 25 syl 
 |-  ( ph -> ( ( C .ih C ) + 1 ) e. RR )
27 hiidge0 
 |-  ( C e. ~H -> 0 <_ ( C .ih C ) )
28 12 27 syl 
 |-  ( ph -> 0 <_ ( C .ih C ) )
29 20 ltp1d 
 |-  ( ph -> ( C .ih C ) < ( ( C .ih C ) + 1 ) )
30 24 20 26 28 29 lelttrd 
 |-  ( ph -> 0 < ( ( C .ih C ) + 1 ) )
31 26 ltp1d 
 |-  ( ph -> ( ( C .ih C ) + 1 ) < ( ( ( C .ih C ) + 1 ) + 1 ) )
32 df-2 
 |-  2 = ( 1 + 1 )
33 32 oveq2i 
 |-  ( ( C .ih C ) + 2 ) = ( ( C .ih C ) + ( 1 + 1 ) )
34 20 recnd 
 |-  ( ph -> ( C .ih C ) e. CC )
35 ax-1cn 
 |-  1 e. CC
36 addass 
 |-  ( ( ( C .ih C ) e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( ( ( C .ih C ) + 1 ) + 1 ) = ( ( C .ih C ) + ( 1 + 1 ) ) )
37 35 35 36 mp3an23 
 |-  ( ( C .ih C ) e. CC -> ( ( ( C .ih C ) + 1 ) + 1 ) = ( ( C .ih C ) + ( 1 + 1 ) ) )
38 34 37 syl 
 |-  ( ph -> ( ( ( C .ih C ) + 1 ) + 1 ) = ( ( C .ih C ) + ( 1 + 1 ) ) )
39 33 38 eqtr4id 
 |-  ( ph -> ( ( C .ih C ) + 2 ) = ( ( ( C .ih C ) + 1 ) + 1 ) )
40 31 39 breqtrrd 
 |-  ( ph -> ( ( C .ih C ) + 1 ) < ( ( C .ih C ) + 2 ) )
41 24 26 23 30 40 lttrd 
 |-  ( ph -> 0 < ( ( C .ih C ) + 2 ) )
42 23 41 elrpd 
 |-  ( ph -> ( ( C .ih C ) + 2 ) e. RR+ )
43 oveq2 
 |-  ( x = ( B +h ( T .h C ) ) -> ( A -h x ) = ( A -h ( B +h ( T .h C ) ) ) )
44 43 fveq2d 
 |-  ( x = ( B +h ( T .h C ) ) -> ( normh ` ( A -h x ) ) = ( normh ` ( A -h ( B +h ( T .h C ) ) ) ) )
45 44 breq2d 
 |-  ( x = ( B +h ( T .h C ) ) -> ( ( normh ` ( A -h B ) ) <_ ( normh ` ( A -h x ) ) <-> ( normh ` ( A -h B ) ) <_ ( normh ` ( A -h ( B +h ( T .h C ) ) ) ) ) )
46 1 chshii 
 |-  H e. SH
47 46 a1i 
 |-  ( ph -> H e. SH )
48 26 recnd 
 |-  ( ph -> ( ( C .ih C ) + 1 ) e. CC )
49 20 28 ge0p1rpd 
 |-  ( ph -> ( ( C .ih C ) + 1 ) e. RR+ )
50 49 rpne0d 
 |-  ( ph -> ( ( C .ih C ) + 1 ) =/= 0 )
51 14 48 50 divcld 
 |-  ( ph -> ( ( ( A -h B ) .ih C ) / ( ( C .ih C ) + 1 ) ) e. CC )
52 6 51 eqeltrid 
 |-  ( ph -> T e. CC )
53 shmulcl 
 |-  ( ( H e. SH /\ T e. CC /\ C e. H ) -> ( T .h C ) e. H )
54 47 52 4 53 syl3anc 
 |-  ( ph -> ( T .h C ) e. H )
55 shaddcl 
 |-  ( ( H e. SH /\ B e. H /\ ( T .h C ) e. H ) -> ( B +h ( T .h C ) ) e. H )
56 47 3 54 55 syl3anc 
 |-  ( ph -> ( B +h ( T .h C ) ) e. H )
57 45 5 56 rspcdva 
 |-  ( ph -> ( normh ` ( A -h B ) ) <_ ( normh ` ( A -h ( B +h ( T .h C ) ) ) ) )
58 1 cheli 
 |-  ( ( T .h C ) e. H -> ( T .h C ) e. ~H )
59 54 58 syl 
 |-  ( ph -> ( T .h C ) e. ~H )
60 hvsubass 
 |-  ( ( A e. ~H /\ B e. ~H /\ ( T .h C ) e. ~H ) -> ( ( A -h B ) -h ( T .h C ) ) = ( A -h ( B +h ( T .h C ) ) ) )
61 2 8 59 60 syl3anc 
 |-  ( ph -> ( ( A -h B ) -h ( T .h C ) ) = ( A -h ( B +h ( T .h C ) ) ) )
62 61 fveq2d 
 |-  ( ph -> ( normh ` ( ( A -h B ) -h ( T .h C ) ) ) = ( normh ` ( A -h ( B +h ( T .h C ) ) ) ) )
63 57 62 breqtrrd 
 |-  ( ph -> ( normh ` ( A -h B ) ) <_ ( normh ` ( ( A -h B ) -h ( T .h C ) ) ) )
64 normcl 
 |-  ( ( A -h B ) e. ~H -> ( normh ` ( A -h B ) ) e. RR )
65 10 64 syl 
 |-  ( ph -> ( normh ` ( A -h B ) ) e. RR )
66 hvsubcl 
 |-  ( ( ( A -h B ) e. ~H /\ ( T .h C ) e. ~H ) -> ( ( A -h B ) -h ( T .h C ) ) e. ~H )
67 10 59 66 syl2anc 
 |-  ( ph -> ( ( A -h B ) -h ( T .h C ) ) e. ~H )
68 normcl 
 |-  ( ( ( A -h B ) -h ( T .h C ) ) e. ~H -> ( normh ` ( ( A -h B ) -h ( T .h C ) ) ) e. RR )
69 67 68 syl 
 |-  ( ph -> ( normh ` ( ( A -h B ) -h ( T .h C ) ) ) e. RR )
70 normge0 
 |-  ( ( A -h B ) e. ~H -> 0 <_ ( normh ` ( A -h B ) ) )
71 10 70 syl 
 |-  ( ph -> 0 <_ ( normh ` ( A -h B ) ) )
72 24 65 69 71 63 letrd 
 |-  ( ph -> 0 <_ ( normh ` ( ( A -h B ) -h ( T .h C ) ) ) )
73 65 69 71 72 le2sqd 
 |-  ( ph -> ( ( normh ` ( A -h B ) ) <_ ( normh ` ( ( A -h B ) -h ( T .h C ) ) ) <-> ( ( normh ` ( A -h B ) ) ^ 2 ) <_ ( ( normh ` ( ( A -h B ) -h ( T .h C ) ) ) ^ 2 ) ) )
74 63 73 mpbid 
 |-  ( ph -> ( ( normh ` ( A -h B ) ) ^ 2 ) <_ ( ( normh ` ( ( A -h B ) -h ( T .h C ) ) ) ^ 2 ) )
75 69 resqcld 
 |-  ( ph -> ( ( normh ` ( ( A -h B ) -h ( T .h C ) ) ) ^ 2 ) e. RR )
76 65 resqcld 
 |-  ( ph -> ( ( normh ` ( A -h B ) ) ^ 2 ) e. RR )
77 75 76 subge0d 
 |-  ( ph -> ( 0 <_ ( ( ( normh ` ( ( A -h B ) -h ( T .h C ) ) ) ^ 2 ) - ( ( normh ` ( A -h B ) ) ^ 2 ) ) <-> ( ( normh ` ( A -h B ) ) ^ 2 ) <_ ( ( normh ` ( ( A -h B ) -h ( T .h C ) ) ) ^ 2 ) ) )
78 74 77 mpbird 
 |-  ( ph -> 0 <_ ( ( ( normh ` ( ( A -h B ) -h ( T .h C ) ) ) ^ 2 ) - ( ( normh ` ( A -h B ) ) ^ 2 ) ) )
79 2z 
 |-  2 e. ZZ
80 rpexpcl 
 |-  ( ( ( ( C .ih C ) + 1 ) e. RR+ /\ 2 e. ZZ ) -> ( ( ( C .ih C ) + 1 ) ^ 2 ) e. RR+ )
81 49 79 80 sylancl 
 |-  ( ph -> ( ( ( C .ih C ) + 1 ) ^ 2 ) e. RR+ )
82 17 81 rerpdivcld 
 |-  ( ph -> ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) e. RR )
83 82 23 remulcld 
 |-  ( ph -> ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 2 ) ) e. RR )
84 83 recnd 
 |-  ( ph -> ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 2 ) ) e. CC )
85 84 negcld 
 |-  ( ph -> -u ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 2 ) ) e. CC )
86 hicl 
 |-  ( ( ( A -h B ) e. ~H /\ ( A -h B ) e. ~H ) -> ( ( A -h B ) .ih ( A -h B ) ) e. CC )
87 10 10 86 syl2anc 
 |-  ( ph -> ( ( A -h B ) .ih ( A -h B ) ) e. CC )
88 85 87 pncand 
 |-  ( ph -> ( ( -u ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 2 ) ) + ( ( A -h B ) .ih ( A -h B ) ) ) - ( ( A -h B ) .ih ( A -h B ) ) ) = -u ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 2 ) ) )
89 normsq 
 |-  ( ( ( A -h B ) -h ( T .h C ) ) e. ~H -> ( ( normh ` ( ( A -h B ) -h ( T .h C ) ) ) ^ 2 ) = ( ( ( A -h B ) -h ( T .h C ) ) .ih ( ( A -h B ) -h ( T .h C ) ) ) )
90 67 89 syl 
 |-  ( ph -> ( ( normh ` ( ( A -h B ) -h ( T .h C ) ) ) ^ 2 ) = ( ( ( A -h B ) -h ( T .h C ) ) .ih ( ( A -h B ) -h ( T .h C ) ) ) )
91 his2sub 
 |-  ( ( ( A -h B ) e. ~H /\ ( T .h C ) e. ~H /\ ( ( A -h B ) -h ( T .h C ) ) e. ~H ) -> ( ( ( A -h B ) -h ( T .h C ) ) .ih ( ( A -h B ) -h ( T .h C ) ) ) = ( ( ( A -h B ) .ih ( ( A -h B ) -h ( T .h C ) ) ) - ( ( T .h C ) .ih ( ( A -h B ) -h ( T .h C ) ) ) ) )
92 10 59 67 91 syl3anc 
 |-  ( ph -> ( ( ( A -h B ) -h ( T .h C ) ) .ih ( ( A -h B ) -h ( T .h C ) ) ) = ( ( ( A -h B ) .ih ( ( A -h B ) -h ( T .h C ) ) ) - ( ( T .h C ) .ih ( ( A -h B ) -h ( T .h C ) ) ) ) )
93 his2sub2 
 |-  ( ( ( A -h B ) e. ~H /\ ( A -h B ) e. ~H /\ ( T .h C ) e. ~H ) -> ( ( A -h B ) .ih ( ( A -h B ) -h ( T .h C ) ) ) = ( ( ( A -h B ) .ih ( A -h B ) ) - ( ( A -h B ) .ih ( T .h C ) ) ) )
94 10 10 59 93 syl3anc 
 |-  ( ph -> ( ( A -h B ) .ih ( ( A -h B ) -h ( T .h C ) ) ) = ( ( ( A -h B ) .ih ( A -h B ) ) - ( ( A -h B ) .ih ( T .h C ) ) ) )
95 94 oveq1d 
 |-  ( ph -> ( ( ( A -h B ) .ih ( ( A -h B ) -h ( T .h C ) ) ) - ( ( T .h C ) .ih ( ( A -h B ) -h ( T .h C ) ) ) ) = ( ( ( ( A -h B ) .ih ( A -h B ) ) - ( ( A -h B ) .ih ( T .h C ) ) ) - ( ( T .h C ) .ih ( ( A -h B ) -h ( T .h C ) ) ) ) )
96 hicl 
 |-  ( ( ( A -h B ) e. ~H /\ ( T .h C ) e. ~H ) -> ( ( A -h B ) .ih ( T .h C ) ) e. CC )
97 10 59 96 syl2anc 
 |-  ( ph -> ( ( A -h B ) .ih ( T .h C ) ) e. CC )
98 his2sub2 
 |-  ( ( ( T .h C ) e. ~H /\ ( A -h B ) e. ~H /\ ( T .h C ) e. ~H ) -> ( ( T .h C ) .ih ( ( A -h B ) -h ( T .h C ) ) ) = ( ( ( T .h C ) .ih ( A -h B ) ) - ( ( T .h C ) .ih ( T .h C ) ) ) )
99 59 10 59 98 syl3anc 
 |-  ( ph -> ( ( T .h C ) .ih ( ( A -h B ) -h ( T .h C ) ) ) = ( ( ( T .h C ) .ih ( A -h B ) ) - ( ( T .h C ) .ih ( T .h C ) ) ) )
100 hicl 
 |-  ( ( ( T .h C ) e. ~H /\ ( A -h B ) e. ~H ) -> ( ( T .h C ) .ih ( A -h B ) ) e. CC )
101 59 10 100 syl2anc 
 |-  ( ph -> ( ( T .h C ) .ih ( A -h B ) ) e. CC )
102 hicl 
 |-  ( ( ( T .h C ) e. ~H /\ ( T .h C ) e. ~H ) -> ( ( T .h C ) .ih ( T .h C ) ) e. CC )
103 59 59 102 syl2anc 
 |-  ( ph -> ( ( T .h C ) .ih ( T .h C ) ) e. CC )
104 101 103 subcld 
 |-  ( ph -> ( ( ( T .h C ) .ih ( A -h B ) ) - ( ( T .h C ) .ih ( T .h C ) ) ) e. CC )
105 99 104 eqeltrd 
 |-  ( ph -> ( ( T .h C ) .ih ( ( A -h B ) -h ( T .h C ) ) ) e. CC )
106 87 97 105 subsub4d 
 |-  ( ph -> ( ( ( ( A -h B ) .ih ( A -h B ) ) - ( ( A -h B ) .ih ( T .h C ) ) ) - ( ( T .h C ) .ih ( ( A -h B ) -h ( T .h C ) ) ) ) = ( ( ( A -h B ) .ih ( A -h B ) ) - ( ( ( A -h B ) .ih ( T .h C ) ) + ( ( T .h C ) .ih ( ( A -h B ) -h ( T .h C ) ) ) ) ) )
107 82 recnd 
 |-  ( ph -> ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) e. CC )
108 35 a1i 
 |-  ( ph -> 1 e. CC )
109 107 48 108 adddid 
 |-  ( ph -> ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( ( C .ih C ) + 1 ) + 1 ) ) = ( ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 1 ) ) + ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. 1 ) ) )
110 39 oveq2d 
 |-  ( ph -> ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 2 ) ) = ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( ( C .ih C ) + 1 ) + 1 ) ) )
111 his5 
 |-  ( ( T e. CC /\ ( A -h B ) e. ~H /\ C e. ~H ) -> ( ( A -h B ) .ih ( T .h C ) ) = ( ( * ` T ) x. ( ( A -h B ) .ih C ) ) )
112 52 10 12 111 syl3anc 
 |-  ( ph -> ( ( A -h B ) .ih ( T .h C ) ) = ( ( * ` T ) x. ( ( A -h B ) .ih C ) ) )
113 52 cjcld 
 |-  ( ph -> ( * ` T ) e. CC )
114 113 14 mulcomd 
 |-  ( ph -> ( ( * ` T ) x. ( ( A -h B ) .ih C ) ) = ( ( ( A -h B ) .ih C ) x. ( * ` T ) ) )
115 14 cjcld 
 |-  ( ph -> ( * ` ( ( A -h B ) .ih C ) ) e. CC )
116 14 115 48 50 divassd 
 |-  ( ph -> ( ( ( ( A -h B ) .ih C ) x. ( * ` ( ( A -h B ) .ih C ) ) ) / ( ( C .ih C ) + 1 ) ) = ( ( ( A -h B ) .ih C ) x. ( ( * ` ( ( A -h B ) .ih C ) ) / ( ( C .ih C ) + 1 ) ) ) )
117 14 absvalsqd 
 |-  ( ph -> ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) = ( ( ( A -h B ) .ih C ) x. ( * ` ( ( A -h B ) .ih C ) ) ) )
118 117 oveq1d 
 |-  ( ph -> ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( C .ih C ) + 1 ) ) = ( ( ( ( A -h B ) .ih C ) x. ( * ` ( ( A -h B ) .ih C ) ) ) / ( ( C .ih C ) + 1 ) ) )
119 6 fveq2i 
 |-  ( * ` T ) = ( * ` ( ( ( A -h B ) .ih C ) / ( ( C .ih C ) + 1 ) ) )
120 14 48 50 cjdivd 
 |-  ( ph -> ( * ` ( ( ( A -h B ) .ih C ) / ( ( C .ih C ) + 1 ) ) ) = ( ( * ` ( ( A -h B ) .ih C ) ) / ( * ` ( ( C .ih C ) + 1 ) ) ) )
121 26 cjred 
 |-  ( ph -> ( * ` ( ( C .ih C ) + 1 ) ) = ( ( C .ih C ) + 1 ) )
122 121 oveq2d 
 |-  ( ph -> ( ( * ` ( ( A -h B ) .ih C ) ) / ( * ` ( ( C .ih C ) + 1 ) ) ) = ( ( * ` ( ( A -h B ) .ih C ) ) / ( ( C .ih C ) + 1 ) ) )
123 120 122 eqtrd 
 |-  ( ph -> ( * ` ( ( ( A -h B ) .ih C ) / ( ( C .ih C ) + 1 ) ) ) = ( ( * ` ( ( A -h B ) .ih C ) ) / ( ( C .ih C ) + 1 ) ) )
124 119 123 eqtrid 
 |-  ( ph -> ( * ` T ) = ( ( * ` ( ( A -h B ) .ih C ) ) / ( ( C .ih C ) + 1 ) ) )
125 124 oveq2d 
 |-  ( ph -> ( ( ( A -h B ) .ih C ) x. ( * ` T ) ) = ( ( ( A -h B ) .ih C ) x. ( ( * ` ( ( A -h B ) .ih C ) ) / ( ( C .ih C ) + 1 ) ) ) )
126 116 118 125 3eqtr4rd 
 |-  ( ph -> ( ( ( A -h B ) .ih C ) x. ( * ` T ) ) = ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( C .ih C ) + 1 ) ) )
127 112 114 126 3eqtrd 
 |-  ( ph -> ( ( A -h B ) .ih ( T .h C ) ) = ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( C .ih C ) + 1 ) ) )
128 17 recnd 
 |-  ( ph -> ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) e. CC )
129 128 48 mulcomd 
 |-  ( ph -> ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) x. ( ( C .ih C ) + 1 ) ) = ( ( ( C .ih C ) + 1 ) x. ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) ) )
130 48 sqvald 
 |-  ( ph -> ( ( ( C .ih C ) + 1 ) ^ 2 ) = ( ( ( C .ih C ) + 1 ) x. ( ( C .ih C ) + 1 ) ) )
131 129 130 oveq12d 
 |-  ( ph -> ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) x. ( ( C .ih C ) + 1 ) ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) = ( ( ( ( C .ih C ) + 1 ) x. ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) ) / ( ( ( C .ih C ) + 1 ) x. ( ( C .ih C ) + 1 ) ) ) )
132 128 48 48 50 50 divcan5d 
 |-  ( ph -> ( ( ( ( C .ih C ) + 1 ) x. ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) ) / ( ( ( C .ih C ) + 1 ) x. ( ( C .ih C ) + 1 ) ) ) = ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( C .ih C ) + 1 ) ) )
133 131 132 eqtr2d 
 |-  ( ph -> ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( C .ih C ) + 1 ) ) = ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) x. ( ( C .ih C ) + 1 ) ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) )
134 26 resqcld 
 |-  ( ph -> ( ( ( C .ih C ) + 1 ) ^ 2 ) e. RR )
135 134 recnd 
 |-  ( ph -> ( ( ( C .ih C ) + 1 ) ^ 2 ) e. CC )
136 81 rpne0d 
 |-  ( ph -> ( ( ( C .ih C ) + 1 ) ^ 2 ) =/= 0 )
137 128 48 135 136 div23d 
 |-  ( ph -> ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) x. ( ( C .ih C ) + 1 ) ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) = ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 1 ) ) )
138 127 133 137 3eqtrd 
 |-  ( ph -> ( ( A -h B ) .ih ( T .h C ) ) = ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 1 ) ) )
139 82 26 remulcld 
 |-  ( ph -> ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 1 ) ) e. RR )
140 138 139 eqeltrd 
 |-  ( ph -> ( ( A -h B ) .ih ( T .h C ) ) e. RR )
141 hire 
 |-  ( ( ( A -h B ) e. ~H /\ ( T .h C ) e. ~H ) -> ( ( ( A -h B ) .ih ( T .h C ) ) e. RR <-> ( ( A -h B ) .ih ( T .h C ) ) = ( ( T .h C ) .ih ( A -h B ) ) ) )
142 10 59 141 syl2anc 
 |-  ( ph -> ( ( ( A -h B ) .ih ( T .h C ) ) e. RR <-> ( ( A -h B ) .ih ( T .h C ) ) = ( ( T .h C ) .ih ( A -h B ) ) ) )
143 140 142 mpbid 
 |-  ( ph -> ( ( A -h B ) .ih ( T .h C ) ) = ( ( T .h C ) .ih ( A -h B ) ) )
144 143 138 eqtr3d 
 |-  ( ph -> ( ( T .h C ) .ih ( A -h B ) ) = ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 1 ) ) )
145 his35 
 |-  ( ( ( T e. CC /\ T e. CC ) /\ ( C e. ~H /\ C e. ~H ) ) -> ( ( T .h C ) .ih ( T .h C ) ) = ( ( T x. ( * ` T ) ) x. ( C .ih C ) ) )
146 52 52 12 12 145 syl22anc 
 |-  ( ph -> ( ( T .h C ) .ih ( T .h C ) ) = ( ( T x. ( * ` T ) ) x. ( C .ih C ) ) )
147 6 fveq2i 
 |-  ( abs ` T ) = ( abs ` ( ( ( A -h B ) .ih C ) / ( ( C .ih C ) + 1 ) ) )
148 14 48 50 absdivd 
 |-  ( ph -> ( abs ` ( ( ( A -h B ) .ih C ) / ( ( C .ih C ) + 1 ) ) ) = ( ( abs ` ( ( A -h B ) .ih C ) ) / ( abs ` ( ( C .ih C ) + 1 ) ) ) )
149 49 rpge0d 
 |-  ( ph -> 0 <_ ( ( C .ih C ) + 1 ) )
150 26 149 absidd 
 |-  ( ph -> ( abs ` ( ( C .ih C ) + 1 ) ) = ( ( C .ih C ) + 1 ) )
151 150 oveq2d 
 |-  ( ph -> ( ( abs ` ( ( A -h B ) .ih C ) ) / ( abs ` ( ( C .ih C ) + 1 ) ) ) = ( ( abs ` ( ( A -h B ) .ih C ) ) / ( ( C .ih C ) + 1 ) ) )
152 148 151 eqtrd 
 |-  ( ph -> ( abs ` ( ( ( A -h B ) .ih C ) / ( ( C .ih C ) + 1 ) ) ) = ( ( abs ` ( ( A -h B ) .ih C ) ) / ( ( C .ih C ) + 1 ) ) )
153 147 152 eqtrid 
 |-  ( ph -> ( abs ` T ) = ( ( abs ` ( ( A -h B ) .ih C ) ) / ( ( C .ih C ) + 1 ) ) )
154 153 oveq1d 
 |-  ( ph -> ( ( abs ` T ) ^ 2 ) = ( ( ( abs ` ( ( A -h B ) .ih C ) ) / ( ( C .ih C ) + 1 ) ) ^ 2 ) )
155 52 absvalsqd 
 |-  ( ph -> ( ( abs ` T ) ^ 2 ) = ( T x. ( * ` T ) ) )
156 16 48 50 sqdivd 
 |-  ( ph -> ( ( ( abs ` ( ( A -h B ) .ih C ) ) / ( ( C .ih C ) + 1 ) ) ^ 2 ) = ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) )
157 154 155 156 3eqtr3d 
 |-  ( ph -> ( T x. ( * ` T ) ) = ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) )
158 157 oveq1d 
 |-  ( ph -> ( ( T x. ( * ` T ) ) x. ( C .ih C ) ) = ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( C .ih C ) ) )
159 146 158 eqtrd 
 |-  ( ph -> ( ( T .h C ) .ih ( T .h C ) ) = ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( C .ih C ) ) )
160 144 159 oveq12d 
 |-  ( ph -> ( ( ( T .h C ) .ih ( A -h B ) ) - ( ( T .h C ) .ih ( T .h C ) ) ) = ( ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 1 ) ) - ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( C .ih C ) ) ) )
161 pncan2 
 |-  ( ( ( C .ih C ) e. CC /\ 1 e. CC ) -> ( ( ( C .ih C ) + 1 ) - ( C .ih C ) ) = 1 )
162 34 35 161 sylancl 
 |-  ( ph -> ( ( ( C .ih C ) + 1 ) - ( C .ih C ) ) = 1 )
163 162 oveq2d 
 |-  ( ph -> ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( ( C .ih C ) + 1 ) - ( C .ih C ) ) ) = ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. 1 ) )
164 107 48 34 subdid 
 |-  ( ph -> ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( ( C .ih C ) + 1 ) - ( C .ih C ) ) ) = ( ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 1 ) ) - ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( C .ih C ) ) ) )
165 163 164 eqtr3d 
 |-  ( ph -> ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. 1 ) = ( ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 1 ) ) - ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( C .ih C ) ) ) )
166 160 99 165 3eqtr4d 
 |-  ( ph -> ( ( T .h C ) .ih ( ( A -h B ) -h ( T .h C ) ) ) = ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. 1 ) )
167 138 166 oveq12d 
 |-  ( ph -> ( ( ( A -h B ) .ih ( T .h C ) ) + ( ( T .h C ) .ih ( ( A -h B ) -h ( T .h C ) ) ) ) = ( ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 1 ) ) + ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. 1 ) ) )
168 109 110 167 3eqtr4rd 
 |-  ( ph -> ( ( ( A -h B ) .ih ( T .h C ) ) + ( ( T .h C ) .ih ( ( A -h B ) -h ( T .h C ) ) ) ) = ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 2 ) ) )
169 168 oveq2d 
 |-  ( ph -> ( ( ( A -h B ) .ih ( A -h B ) ) - ( ( ( A -h B ) .ih ( T .h C ) ) + ( ( T .h C ) .ih ( ( A -h B ) -h ( T .h C ) ) ) ) ) = ( ( ( A -h B ) .ih ( A -h B ) ) - ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 2 ) ) ) )
170 95 106 169 3eqtrd 
 |-  ( ph -> ( ( ( A -h B ) .ih ( ( A -h B ) -h ( T .h C ) ) ) - ( ( T .h C ) .ih ( ( A -h B ) -h ( T .h C ) ) ) ) = ( ( ( A -h B ) .ih ( A -h B ) ) - ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 2 ) ) ) )
171 90 92 170 3eqtrd 
 |-  ( ph -> ( ( normh ` ( ( A -h B ) -h ( T .h C ) ) ) ^ 2 ) = ( ( ( A -h B ) .ih ( A -h B ) ) - ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 2 ) ) ) )
172 87 84 negsubd 
 |-  ( ph -> ( ( ( A -h B ) .ih ( A -h B ) ) + -u ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 2 ) ) ) = ( ( ( A -h B ) .ih ( A -h B ) ) - ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 2 ) ) ) )
173 87 85 addcomd 
 |-  ( ph -> ( ( ( A -h B ) .ih ( A -h B ) ) + -u ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 2 ) ) ) = ( -u ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 2 ) ) + ( ( A -h B ) .ih ( A -h B ) ) ) )
174 171 172 173 3eqtr2d 
 |-  ( ph -> ( ( normh ` ( ( A -h B ) -h ( T .h C ) ) ) ^ 2 ) = ( -u ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 2 ) ) + ( ( A -h B ) .ih ( A -h B ) ) ) )
175 normsq 
 |-  ( ( A -h B ) e. ~H -> ( ( normh ` ( A -h B ) ) ^ 2 ) = ( ( A -h B ) .ih ( A -h B ) ) )
176 10 175 syl 
 |-  ( ph -> ( ( normh ` ( A -h B ) ) ^ 2 ) = ( ( A -h B ) .ih ( A -h B ) ) )
177 174 176 oveq12d 
 |-  ( ph -> ( ( ( normh ` ( ( A -h B ) -h ( T .h C ) ) ) ^ 2 ) - ( ( normh ` ( A -h B ) ) ^ 2 ) ) = ( ( -u ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 2 ) ) + ( ( A -h B ) .ih ( A -h B ) ) ) - ( ( A -h B ) .ih ( A -h B ) ) ) )
178 23 renegcld 
 |-  ( ph -> -u ( ( C .ih C ) + 2 ) e. RR )
179 178 recnd 
 |-  ( ph -> -u ( ( C .ih C ) + 2 ) e. CC )
180 128 179 135 136 div23d 
 |-  ( ph -> ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) x. -u ( ( C .ih C ) + 2 ) ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) = ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. -u ( ( C .ih C ) + 2 ) ) )
181 23 recnd 
 |-  ( ph -> ( ( C .ih C ) + 2 ) e. CC )
182 107 181 mulneg2d 
 |-  ( ph -> ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. -u ( ( C .ih C ) + 2 ) ) = -u ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 2 ) ) )
183 180 182 eqtrd 
 |-  ( ph -> ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) x. -u ( ( C .ih C ) + 2 ) ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) = -u ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) x. ( ( C .ih C ) + 2 ) ) )
184 88 177 183 3eqtr4rd 
 |-  ( ph -> ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) x. -u ( ( C .ih C ) + 2 ) ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) = ( ( ( normh ` ( ( A -h B ) -h ( T .h C ) ) ) ^ 2 ) - ( ( normh ` ( A -h B ) ) ^ 2 ) ) )
185 78 184 breqtrrd 
 |-  ( ph -> 0 <_ ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) x. -u ( ( C .ih C ) + 2 ) ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) )
186 17 178 remulcld 
 |-  ( ph -> ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) x. -u ( ( C .ih C ) + 2 ) ) e. RR )
187 186 81 ge0divd 
 |-  ( ph -> ( 0 <_ ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) x. -u ( ( C .ih C ) + 2 ) ) <-> 0 <_ ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) x. -u ( ( C .ih C ) + 2 ) ) / ( ( ( C .ih C ) + 1 ) ^ 2 ) ) ) )
188 185 187 mpbird 
 |-  ( ph -> 0 <_ ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) x. -u ( ( C .ih C ) + 2 ) ) )
189 mulneg12 
 |-  ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) e. CC /\ ( ( C .ih C ) + 2 ) e. CC ) -> ( -u ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) x. ( ( C .ih C ) + 2 ) ) = ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) x. -u ( ( C .ih C ) + 2 ) ) )
190 128 181 189 syl2anc 
 |-  ( ph -> ( -u ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) x. ( ( C .ih C ) + 2 ) ) = ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) x. -u ( ( C .ih C ) + 2 ) ) )
191 188 190 breqtrrd 
 |-  ( ph -> 0 <_ ( -u ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) x. ( ( C .ih C ) + 2 ) ) )
192 18 42 191 prodge0ld 
 |-  ( ph -> 0 <_ -u ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) )
193 17 le0neg1d 
 |-  ( ph -> ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) <_ 0 <-> 0 <_ -u ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) ) )
194 192 193 mpbird 
 |-  ( ph -> ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) <_ 0 )
195 15 sqge0d 
 |-  ( ph -> 0 <_ ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) )
196 0re 
 |-  0 e. RR
197 letri3 
 |-  ( ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) e. RR /\ 0 e. RR ) -> ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) = 0 <-> ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) <_ 0 /\ 0 <_ ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) ) ) )
198 17 196 197 sylancl 
 |-  ( ph -> ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) = 0 <-> ( ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) <_ 0 /\ 0 <_ ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) ) ) )
199 194 195 198 mpbir2and 
 |-  ( ph -> ( ( abs ` ( ( A -h B ) .ih C ) ) ^ 2 ) = 0 )
200 16 199 sqeq0d 
 |-  ( ph -> ( abs ` ( ( A -h B ) .ih C ) ) = 0 )
201 14 200 abs00d 
 |-  ( ph -> ( ( A -h B ) .ih C ) = 0 )