Metamath Proof Explorer

Theorem pjthlem1

Description: Lemma for pjth . (Contributed by NM, 10-Oct-1999) (Revised by Mario Carneiro, 17-Oct-2015) (Proof shortened by AV, 10-Jul-2022)

Ref Expression
Hypotheses pjthlem.v 
|- V = ( Base ` W )
pjthlem.n 
|- N = ( norm ` W )
pjthlem.p 
|- .+ = ( +g ` W )
pjthlem.m 
|- .- = ( -g ` W )
pjthlem.h 
|- ., = ( .i ` W )
pjthlem.l 
|- L = ( LSubSp ` W )
pjthlem.1 
|- ( ph -> W e. CHil )
pjthlem.2 
|- ( ph -> U e. L )
pjthlem.4 
|- ( ph -> A e. V )
pjthlem.5 
|- ( ph -> B e. U )
pjthlem.7 
|- ( ph -> A. x e. U ( N ` A ) <_ ( N ` ( A .- x ) ) )
pjthlem.8 
|- T = ( ( A ., B ) / ( ( B ., B ) + 1 ) )
Assertion pjthlem1 
|- ( ph -> ( A ., B ) = 0 )

Proof

Step Hyp Ref Expression
1 pjthlem.v 
 |-  V = ( Base ` W )
2 pjthlem.n 
 |-  N = ( norm ` W )
3 pjthlem.p 
 |-  .+ = ( +g ` W )
4 pjthlem.m 
 |-  .- = ( -g ` W )
5 pjthlem.h 
 |-  ., = ( .i ` W )
6 pjthlem.l 
 |-  L = ( LSubSp ` W )
7 pjthlem.1 
 |-  ( ph -> W e. CHil )
8 pjthlem.2 
 |-  ( ph -> U e. L )
9 pjthlem.4 
 |-  ( ph -> A e. V )
10 pjthlem.5 
 |-  ( ph -> B e. U )
11 pjthlem.7 
 |-  ( ph -> A. x e. U ( N ` A ) <_ ( N ` ( A .- x ) ) )
12 pjthlem.8 
 |-  T = ( ( A ., B ) / ( ( B ., B ) + 1 ) )
13 hlcph 
 |-  ( W e. CHil -> W e. CPreHil )
14 7 13 syl 
 |-  ( ph -> W e. CPreHil )
15 1 6 lssss 
 |-  ( U e. L -> U C_ V )
16 8 15 syl 
 |-  ( ph -> U C_ V )
17 16 10 sseldd 
 |-  ( ph -> B e. V )
18 1 5 cphipcl 
 |-  ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( A ., B ) e. CC )
19 14 9 17 18 syl3anc 
 |-  ( ph -> ( A ., B ) e. CC )
20 19 abscld 
 |-  ( ph -> ( abs ` ( A ., B ) ) e. RR )
21 20 recnd 
 |-  ( ph -> ( abs ` ( A ., B ) ) e. CC )
22 20 resqcld 
 |-  ( ph -> ( ( abs ` ( A ., B ) ) ^ 2 ) e. RR )
23 22 renegcld 
 |-  ( ph -> -u ( ( abs ` ( A ., B ) ) ^ 2 ) e. RR )
24 1 5 reipcl 
 |-  ( ( W e. CPreHil /\ B e. V ) -> ( B ., B ) e. RR )
25 14 17 24 syl2anc 
 |-  ( ph -> ( B ., B ) e. RR )
26 2re 
 |-  2 e. RR
27 readdcl 
 |-  ( ( ( B ., B ) e. RR /\ 2 e. RR ) -> ( ( B ., B ) + 2 ) e. RR )
28 25 26 27 sylancl 
 |-  ( ph -> ( ( B ., B ) + 2 ) e. RR )
29 0red 
 |-  ( ph -> 0 e. RR )
30 peano2re 
 |-  ( ( B ., B ) e. RR -> ( ( B ., B ) + 1 ) e. RR )
31 25 30 syl 
 |-  ( ph -> ( ( B ., B ) + 1 ) e. RR )
32 1 5 ipge0 
 |-  ( ( W e. CPreHil /\ B e. V ) -> 0 <_ ( B ., B ) )
33 14 17 32 syl2anc 
 |-  ( ph -> 0 <_ ( B ., B ) )
34 25 ltp1d 
 |-  ( ph -> ( B ., B ) < ( ( B ., B ) + 1 ) )
35 29 25 31 33 34 lelttrd 
 |-  ( ph -> 0 < ( ( B ., B ) + 1 ) )
36 31 ltp1d 
 |-  ( ph -> ( ( B ., B ) + 1 ) < ( ( ( B ., B ) + 1 ) + 1 ) )
37 df-2 
 |-  2 = ( 1 + 1 )
38 37 oveq2i 
 |-  ( ( B ., B ) + 2 ) = ( ( B ., B ) + ( 1 + 1 ) )
39 25 recnd 
 |-  ( ph -> ( B ., B ) e. CC )
40 ax-1cn 
 |-  1 e. CC
41 addass 
 |-  ( ( ( B ., B ) e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( ( ( B ., B ) + 1 ) + 1 ) = ( ( B ., B ) + ( 1 + 1 ) ) )
42 40 40 41 mp3an23 
 |-  ( ( B ., B ) e. CC -> ( ( ( B ., B ) + 1 ) + 1 ) = ( ( B ., B ) + ( 1 + 1 ) ) )
43 39 42 syl 
 |-  ( ph -> ( ( ( B ., B ) + 1 ) + 1 ) = ( ( B ., B ) + ( 1 + 1 ) ) )
44 38 43 eqtr4id 
 |-  ( ph -> ( ( B ., B ) + 2 ) = ( ( ( B ., B ) + 1 ) + 1 ) )
45 36 44 breqtrrd 
 |-  ( ph -> ( ( B ., B ) + 1 ) < ( ( B ., B ) + 2 ) )
46 29 31 28 35 45 lttrd 
 |-  ( ph -> 0 < ( ( B ., B ) + 2 ) )
47 28 46 elrpd 
 |-  ( ph -> ( ( B ., B ) + 2 ) e. RR+ )
48 oveq2 
 |-  ( x = ( T ( .s ` W ) B ) -> ( A .- x ) = ( A .- ( T ( .s ` W ) B ) ) )
49 48 fveq2d 
 |-  ( x = ( T ( .s ` W ) B ) -> ( N ` ( A .- x ) ) = ( N ` ( A .- ( T ( .s ` W ) B ) ) ) )
50 49 breq2d 
 |-  ( x = ( T ( .s ` W ) B ) -> ( ( N ` A ) <_ ( N ` ( A .- x ) ) <-> ( N ` A ) <_ ( N ` ( A .- ( T ( .s ` W ) B ) ) ) ) )
51 cphlmod 
 |-  ( W e. CPreHil -> W e. LMod )
52 14 51 syl 
 |-  ( ph -> W e. LMod )
53 hlphl 
 |-  ( W e. CHil -> W e. PreHil )
54 7 53 syl 
 |-  ( ph -> W e. PreHil )
55 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
56 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
57 55 5 1 56 ipcl 
 |-  ( ( W e. PreHil /\ A e. V /\ B e. V ) -> ( A ., B ) e. ( Base ` ( Scalar ` W ) ) )
58 54 9 17 57 syl3anc 
 |-  ( ph -> ( A ., B ) e. ( Base ` ( Scalar ` W ) ) )
59 55 56 hlress 
 |-  ( W e. CHil -> RR C_ ( Base ` ( Scalar ` W ) ) )
60 7 59 syl 
 |-  ( ph -> RR C_ ( Base ` ( Scalar ` W ) ) )
61 60 31 sseldd 
 |-  ( ph -> ( ( B ., B ) + 1 ) e. ( Base ` ( Scalar ` W ) ) )
62 25 33 ge0p1rpd 
 |-  ( ph -> ( ( B ., B ) + 1 ) e. RR+ )
63 62 rpne0d 
 |-  ( ph -> ( ( B ., B ) + 1 ) =/= 0 )
64 55 56 cphdivcl 
 |-  ( ( W e. CPreHil /\ ( ( A ., B ) e. ( Base ` ( Scalar ` W ) ) /\ ( ( B ., B ) + 1 ) e. ( Base ` ( Scalar ` W ) ) /\ ( ( B ., B ) + 1 ) =/= 0 ) ) -> ( ( A ., B ) / ( ( B ., B ) + 1 ) ) e. ( Base ` ( Scalar ` W ) ) )
65 14 58 61 63 64 syl13anc 
 |-  ( ph -> ( ( A ., B ) / ( ( B ., B ) + 1 ) ) e. ( Base ` ( Scalar ` W ) ) )
66 12 65 eqeltrid 
 |-  ( ph -> T e. ( Base ` ( Scalar ` W ) ) )
67 eqid 
 |-  ( .s ` W ) = ( .s ` W )
68 55 67 56 6 lssvscl 
 |-  ( ( ( W e. LMod /\ U e. L ) /\ ( T e. ( Base ` ( Scalar ` W ) ) /\ B e. U ) ) -> ( T ( .s ` W ) B ) e. U )
69 52 8 66 10 68 syl22anc 
 |-  ( ph -> ( T ( .s ` W ) B ) e. U )
70 50 11 69 rspcdva 
 |-  ( ph -> ( N ` A ) <_ ( N ` ( A .- ( T ( .s ` W ) B ) ) ) )
71 cphngp 
 |-  ( W e. CPreHil -> W e. NrmGrp )
72 14 71 syl 
 |-  ( ph -> W e. NrmGrp )
73 1 2 nmcl 
 |-  ( ( W e. NrmGrp /\ A e. V ) -> ( N ` A ) e. RR )
74 72 9 73 syl2anc 
 |-  ( ph -> ( N ` A ) e. RR )
75 1 55 67 56 lmodvscl 
 |-  ( ( W e. LMod /\ T e. ( Base ` ( Scalar ` W ) ) /\ B e. V ) -> ( T ( .s ` W ) B ) e. V )
76 52 66 17 75 syl3anc 
 |-  ( ph -> ( T ( .s ` W ) B ) e. V )
77 1 4 lmodvsubcl 
 |-  ( ( W e. LMod /\ A e. V /\ ( T ( .s ` W ) B ) e. V ) -> ( A .- ( T ( .s ` W ) B ) ) e. V )
78 52 9 76 77 syl3anc 
 |-  ( ph -> ( A .- ( T ( .s ` W ) B ) ) e. V )
79 1 2 nmcl 
 |-  ( ( W e. NrmGrp /\ ( A .- ( T ( .s ` W ) B ) ) e. V ) -> ( N ` ( A .- ( T ( .s ` W ) B ) ) ) e. RR )
80 72 78 79 syl2anc 
 |-  ( ph -> ( N ` ( A .- ( T ( .s ` W ) B ) ) ) e. RR )
81 1 2 nmge0 
 |-  ( ( W e. NrmGrp /\ A e. V ) -> 0 <_ ( N ` A ) )
82 72 9 81 syl2anc 
 |-  ( ph -> 0 <_ ( N ` A ) )
83 1 2 nmge0 
 |-  ( ( W e. NrmGrp /\ ( A .- ( T ( .s ` W ) B ) ) e. V ) -> 0 <_ ( N ` ( A .- ( T ( .s ` W ) B ) ) ) )
84 72 78 83 syl2anc 
 |-  ( ph -> 0 <_ ( N ` ( A .- ( T ( .s ` W ) B ) ) ) )
85 74 80 82 84 le2sqd 
 |-  ( ph -> ( ( N ` A ) <_ ( N ` ( A .- ( T ( .s ` W ) B ) ) ) <-> ( ( N ` A ) ^ 2 ) <_ ( ( N ` ( A .- ( T ( .s ` W ) B ) ) ) ^ 2 ) ) )
86 70 85 mpbid 
 |-  ( ph -> ( ( N ` A ) ^ 2 ) <_ ( ( N ` ( A .- ( T ( .s ` W ) B ) ) ) ^ 2 ) )
87 80 resqcld 
 |-  ( ph -> ( ( N ` ( A .- ( T ( .s ` W ) B ) ) ) ^ 2 ) e. RR )
88 74 resqcld 
 |-  ( ph -> ( ( N ` A ) ^ 2 ) e. RR )
89 87 88 subge0d 
 |-  ( ph -> ( 0 <_ ( ( ( N ` ( A .- ( T ( .s ` W ) B ) ) ) ^ 2 ) - ( ( N ` A ) ^ 2 ) ) <-> ( ( N ` A ) ^ 2 ) <_ ( ( N ` ( A .- ( T ( .s ` W ) B ) ) ) ^ 2 ) ) )
90 86 89 mpbird 
 |-  ( ph -> 0 <_ ( ( ( N ` ( A .- ( T ( .s ` W ) B ) ) ) ^ 2 ) - ( ( N ` A ) ^ 2 ) ) )
91 2z 
 |-  2 e. ZZ
92 rpexpcl 
 |-  ( ( ( ( B ., B ) + 1 ) e. RR+ /\ 2 e. ZZ ) -> ( ( ( B ., B ) + 1 ) ^ 2 ) e. RR+ )
93 62 91 92 sylancl 
 |-  ( ph -> ( ( ( B ., B ) + 1 ) ^ 2 ) e. RR+ )
94 22 93 rerpdivcld 
 |-  ( ph -> ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) e. RR )
95 94 28 remulcld 
 |-  ( ph -> ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 2 ) ) e. RR )
96 95 recnd 
 |-  ( ph -> ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 2 ) ) e. CC )
97 96 negcld 
 |-  ( ph -> -u ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 2 ) ) e. CC )
98 1 5 cphipcl 
 |-  ( ( W e. CPreHil /\ A e. V /\ A e. V ) -> ( A ., A ) e. CC )
99 14 9 9 98 syl3anc 
 |-  ( ph -> ( A ., A ) e. CC )
100 97 99 pncand 
 |-  ( ph -> ( ( -u ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 2 ) ) + ( A ., A ) ) - ( A ., A ) ) = -u ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 2 ) ) )
101 1 5 2 nmsq 
 |-  ( ( W e. CPreHil /\ ( A .- ( T ( .s ` W ) B ) ) e. V ) -> ( ( N ` ( A .- ( T ( .s ` W ) B ) ) ) ^ 2 ) = ( ( A .- ( T ( .s ` W ) B ) ) ., ( A .- ( T ( .s ` W ) B ) ) ) )
102 14 78 101 syl2anc 
 |-  ( ph -> ( ( N ` ( A .- ( T ( .s ` W ) B ) ) ) ^ 2 ) = ( ( A .- ( T ( .s ` W ) B ) ) ., ( A .- ( T ( .s ` W ) B ) ) ) )
103 5 1 4 cphsubdir 
 |-  ( ( W e. CPreHil /\ ( A e. V /\ ( T ( .s ` W ) B ) e. V /\ ( A .- ( T ( .s ` W ) B ) ) e. V ) ) -> ( ( A .- ( T ( .s ` W ) B ) ) ., ( A .- ( T ( .s ` W ) B ) ) ) = ( ( A ., ( A .- ( T ( .s ` W ) B ) ) ) - ( ( T ( .s ` W ) B ) ., ( A .- ( T ( .s ` W ) B ) ) ) ) )
104 14 9 76 78 103 syl13anc 
 |-  ( ph -> ( ( A .- ( T ( .s ` W ) B ) ) ., ( A .- ( T ( .s ` W ) B ) ) ) = ( ( A ., ( A .- ( T ( .s ` W ) B ) ) ) - ( ( T ( .s ` W ) B ) ., ( A .- ( T ( .s ` W ) B ) ) ) ) )
105 5 1 4 cphsubdi 
 |-  ( ( W e. CPreHil /\ ( A e. V /\ A e. V /\ ( T ( .s ` W ) B ) e. V ) ) -> ( A ., ( A .- ( T ( .s ` W ) B ) ) ) = ( ( A ., A ) - ( A ., ( T ( .s ` W ) B ) ) ) )
106 14 9 9 76 105 syl13anc 
 |-  ( ph -> ( A ., ( A .- ( T ( .s ` W ) B ) ) ) = ( ( A ., A ) - ( A ., ( T ( .s ` W ) B ) ) ) )
107 106 oveq1d 
 |-  ( ph -> ( ( A ., ( A .- ( T ( .s ` W ) B ) ) ) - ( ( T ( .s ` W ) B ) ., ( A .- ( T ( .s ` W ) B ) ) ) ) = ( ( ( A ., A ) - ( A ., ( T ( .s ` W ) B ) ) ) - ( ( T ( .s ` W ) B ) ., ( A .- ( T ( .s ` W ) B ) ) ) ) )
108 1 5 cphipcl 
 |-  ( ( W e. CPreHil /\ A e. V /\ ( T ( .s ` W ) B ) e. V ) -> ( A ., ( T ( .s ` W ) B ) ) e. CC )
109 14 9 76 108 syl3anc 
 |-  ( ph -> ( A ., ( T ( .s ` W ) B ) ) e. CC )
110 5 1 4 cphsubdi 
 |-  ( ( W e. CPreHil /\ ( ( T ( .s ` W ) B ) e. V /\ A e. V /\ ( T ( .s ` W ) B ) e. V ) ) -> ( ( T ( .s ` W ) B ) ., ( A .- ( T ( .s ` W ) B ) ) ) = ( ( ( T ( .s ` W ) B ) ., A ) - ( ( T ( .s ` W ) B ) ., ( T ( .s ` W ) B ) ) ) )
111 14 76 9 76 110 syl13anc 
 |-  ( ph -> ( ( T ( .s ` W ) B ) ., ( A .- ( T ( .s ` W ) B ) ) ) = ( ( ( T ( .s ` W ) B ) ., A ) - ( ( T ( .s ` W ) B ) ., ( T ( .s ` W ) B ) ) ) )
112 1 5 cphipcl 
 |-  ( ( W e. CPreHil /\ ( T ( .s ` W ) B ) e. V /\ A e. V ) -> ( ( T ( .s ` W ) B ) ., A ) e. CC )
113 14 76 9 112 syl3anc 
 |-  ( ph -> ( ( T ( .s ` W ) B ) ., A ) e. CC )
114 1 5 cphipcl 
 |-  ( ( W e. CPreHil /\ ( T ( .s ` W ) B ) e. V /\ ( T ( .s ` W ) B ) e. V ) -> ( ( T ( .s ` W ) B ) ., ( T ( .s ` W ) B ) ) e. CC )
115 14 76 76 114 syl3anc 
 |-  ( ph -> ( ( T ( .s ` W ) B ) ., ( T ( .s ` W ) B ) ) e. CC )
116 113 115 subcld 
 |-  ( ph -> ( ( ( T ( .s ` W ) B ) ., A ) - ( ( T ( .s ` W ) B ) ., ( T ( .s ` W ) B ) ) ) e. CC )
117 111 116 eqeltrd 
 |-  ( ph -> ( ( T ( .s ` W ) B ) ., ( A .- ( T ( .s ` W ) B ) ) ) e. CC )
118 99 109 117 subsub4d 
 |-  ( ph -> ( ( ( A ., A ) - ( A ., ( T ( .s ` W ) B ) ) ) - ( ( T ( .s ` W ) B ) ., ( A .- ( T ( .s ` W ) B ) ) ) ) = ( ( A ., A ) - ( ( A ., ( T ( .s ` W ) B ) ) + ( ( T ( .s ` W ) B ) ., ( A .- ( T ( .s ` W ) B ) ) ) ) ) )
119 94 recnd 
 |-  ( ph -> ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) e. CC )
120 31 recnd 
 |-  ( ph -> ( ( B ., B ) + 1 ) e. CC )
121 1cnd 
 |-  ( ph -> 1 e. CC )
122 119 120 121 adddid 
 |-  ( ph -> ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( ( B ., B ) + 1 ) + 1 ) ) = ( ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 1 ) ) + ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. 1 ) ) )
123 44 oveq2d 
 |-  ( ph -> ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 2 ) ) = ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( ( B ., B ) + 1 ) + 1 ) ) )
124 5 1 55 56 67 cphassr 
 |-  ( ( W e. CPreHil /\ ( T e. ( Base ` ( Scalar ` W ) ) /\ A e. V /\ B e. V ) ) -> ( A ., ( T ( .s ` W ) B ) ) = ( ( * ` T ) x. ( A ., B ) ) )
125 14 66 9 17 124 syl13anc 
 |-  ( ph -> ( A ., ( T ( .s ` W ) B ) ) = ( ( * ` T ) x. ( A ., B ) ) )
126 19 120 63 divcld 
 |-  ( ph -> ( ( A ., B ) / ( ( B ., B ) + 1 ) ) e. CC )
127 12 126 eqeltrid 
 |-  ( ph -> T e. CC )
128 127 cjcld 
 |-  ( ph -> ( * ` T ) e. CC )
129 128 19 mulcomd 
 |-  ( ph -> ( ( * ` T ) x. ( A ., B ) ) = ( ( A ., B ) x. ( * ` T ) ) )
130 19 cjcld 
 |-  ( ph -> ( * ` ( A ., B ) ) e. CC )
131 19 130 120 63 divassd 
 |-  ( ph -> ( ( ( A ., B ) x. ( * ` ( A ., B ) ) ) / ( ( B ., B ) + 1 ) ) = ( ( A ., B ) x. ( ( * ` ( A ., B ) ) / ( ( B ., B ) + 1 ) ) ) )
132 19 absvalsqd 
 |-  ( ph -> ( ( abs ` ( A ., B ) ) ^ 2 ) = ( ( A ., B ) x. ( * ` ( A ., B ) ) ) )
133 132 oveq1d 
 |-  ( ph -> ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( B ., B ) + 1 ) ) = ( ( ( A ., B ) x. ( * ` ( A ., B ) ) ) / ( ( B ., B ) + 1 ) ) )
134 12 fveq2i 
 |-  ( * ` T ) = ( * ` ( ( A ., B ) / ( ( B ., B ) + 1 ) ) )
135 19 120 63 cjdivd 
 |-  ( ph -> ( * ` ( ( A ., B ) / ( ( B ., B ) + 1 ) ) ) = ( ( * ` ( A ., B ) ) / ( * ` ( ( B ., B ) + 1 ) ) ) )
136 31 cjred 
 |-  ( ph -> ( * ` ( ( B ., B ) + 1 ) ) = ( ( B ., B ) + 1 ) )
137 136 oveq2d 
 |-  ( ph -> ( ( * ` ( A ., B ) ) / ( * ` ( ( B ., B ) + 1 ) ) ) = ( ( * ` ( A ., B ) ) / ( ( B ., B ) + 1 ) ) )
138 135 137 eqtrd 
 |-  ( ph -> ( * ` ( ( A ., B ) / ( ( B ., B ) + 1 ) ) ) = ( ( * ` ( A ., B ) ) / ( ( B ., B ) + 1 ) ) )
139 134 138 syl5eq 
 |-  ( ph -> ( * ` T ) = ( ( * ` ( A ., B ) ) / ( ( B ., B ) + 1 ) ) )
140 139 oveq2d 
 |-  ( ph -> ( ( A ., B ) x. ( * ` T ) ) = ( ( A ., B ) x. ( ( * ` ( A ., B ) ) / ( ( B ., B ) + 1 ) ) ) )
141 131 133 140 3eqtr4rd 
 |-  ( ph -> ( ( A ., B ) x. ( * ` T ) ) = ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( B ., B ) + 1 ) ) )
142 125 129 141 3eqtrd 
 |-  ( ph -> ( A ., ( T ( .s ` W ) B ) ) = ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( B ., B ) + 1 ) ) )
143 22 recnd 
 |-  ( ph -> ( ( abs ` ( A ., B ) ) ^ 2 ) e. CC )
144 143 120 mulcomd 
 |-  ( ph -> ( ( ( abs ` ( A ., B ) ) ^ 2 ) x. ( ( B ., B ) + 1 ) ) = ( ( ( B ., B ) + 1 ) x. ( ( abs ` ( A ., B ) ) ^ 2 ) ) )
145 120 sqvald 
 |-  ( ph -> ( ( ( B ., B ) + 1 ) ^ 2 ) = ( ( ( B ., B ) + 1 ) x. ( ( B ., B ) + 1 ) ) )
146 144 145 oveq12d 
 |-  ( ph -> ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) x. ( ( B ., B ) + 1 ) ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) = ( ( ( ( B ., B ) + 1 ) x. ( ( abs ` ( A ., B ) ) ^ 2 ) ) / ( ( ( B ., B ) + 1 ) x. ( ( B ., B ) + 1 ) ) ) )
147 143 120 120 63 63 divcan5d 
 |-  ( ph -> ( ( ( ( B ., B ) + 1 ) x. ( ( abs ` ( A ., B ) ) ^ 2 ) ) / ( ( ( B ., B ) + 1 ) x. ( ( B ., B ) + 1 ) ) ) = ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( B ., B ) + 1 ) ) )
148 146 147 eqtr2d 
 |-  ( ph -> ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( B ., B ) + 1 ) ) = ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) x. ( ( B ., B ) + 1 ) ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) )
149 93 rpcnd 
 |-  ( ph -> ( ( ( B ., B ) + 1 ) ^ 2 ) e. CC )
150 93 rpne0d 
 |-  ( ph -> ( ( ( B ., B ) + 1 ) ^ 2 ) =/= 0 )
151 143 120 149 150 div23d 
 |-  ( ph -> ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) x. ( ( B ., B ) + 1 ) ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) = ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 1 ) ) )
152 142 148 151 3eqtrd 
 |-  ( ph -> ( A ., ( T ( .s ` W ) B ) ) = ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 1 ) ) )
153 94 31 remulcld 
 |-  ( ph -> ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 1 ) ) e. RR )
154 152 153 eqeltrd 
 |-  ( ph -> ( A ., ( T ( .s ` W ) B ) ) e. RR )
155 154 cjred 
 |-  ( ph -> ( * ` ( A ., ( T ( .s ` W ) B ) ) ) = ( A ., ( T ( .s ` W ) B ) ) )
156 5 1 cphipcj 
 |-  ( ( W e. CPreHil /\ A e. V /\ ( T ( .s ` W ) B ) e. V ) -> ( * ` ( A ., ( T ( .s ` W ) B ) ) ) = ( ( T ( .s ` W ) B ) ., A ) )
157 14 9 76 156 syl3anc 
 |-  ( ph -> ( * ` ( A ., ( T ( .s ` W ) B ) ) ) = ( ( T ( .s ` W ) B ) ., A ) )
158 155 157 152 3eqtr3d 
 |-  ( ph -> ( ( T ( .s ` W ) B ) ., A ) = ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 1 ) ) )
159 5 1 55 56 67 cph2ass 
 |-  ( ( W e. CPreHil /\ ( T e. ( Base ` ( Scalar ` W ) ) /\ T e. ( Base ` ( Scalar ` W ) ) ) /\ ( B e. V /\ B e. V ) ) -> ( ( T ( .s ` W ) B ) ., ( T ( .s ` W ) B ) ) = ( ( T x. ( * ` T ) ) x. ( B ., B ) ) )
160 14 66 66 17 17 159 syl122anc 
 |-  ( ph -> ( ( T ( .s ` W ) B ) ., ( T ( .s ` W ) B ) ) = ( ( T x. ( * ` T ) ) x. ( B ., B ) ) )
161 12 fveq2i 
 |-  ( abs ` T ) = ( abs ` ( ( A ., B ) / ( ( B ., B ) + 1 ) ) )
162 19 120 63 absdivd 
 |-  ( ph -> ( abs ` ( ( A ., B ) / ( ( B ., B ) + 1 ) ) ) = ( ( abs ` ( A ., B ) ) / ( abs ` ( ( B ., B ) + 1 ) ) ) )
163 62 rpge0d 
 |-  ( ph -> 0 <_ ( ( B ., B ) + 1 ) )
164 31 163 absidd 
 |-  ( ph -> ( abs ` ( ( B ., B ) + 1 ) ) = ( ( B ., B ) + 1 ) )
165 164 oveq2d 
 |-  ( ph -> ( ( abs ` ( A ., B ) ) / ( abs ` ( ( B ., B ) + 1 ) ) ) = ( ( abs ` ( A ., B ) ) / ( ( B ., B ) + 1 ) ) )
166 162 165 eqtrd 
 |-  ( ph -> ( abs ` ( ( A ., B ) / ( ( B ., B ) + 1 ) ) ) = ( ( abs ` ( A ., B ) ) / ( ( B ., B ) + 1 ) ) )
167 161 166 syl5eq 
 |-  ( ph -> ( abs ` T ) = ( ( abs ` ( A ., B ) ) / ( ( B ., B ) + 1 ) ) )
168 167 oveq1d 
 |-  ( ph -> ( ( abs ` T ) ^ 2 ) = ( ( ( abs ` ( A ., B ) ) / ( ( B ., B ) + 1 ) ) ^ 2 ) )
169 127 absvalsqd 
 |-  ( ph -> ( ( abs ` T ) ^ 2 ) = ( T x. ( * ` T ) ) )
170 21 120 63 sqdivd 
 |-  ( ph -> ( ( ( abs ` ( A ., B ) ) / ( ( B ., B ) + 1 ) ) ^ 2 ) = ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) )
171 168 169 170 3eqtr3d 
 |-  ( ph -> ( T x. ( * ` T ) ) = ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) )
172 171 oveq1d 
 |-  ( ph -> ( ( T x. ( * ` T ) ) x. ( B ., B ) ) = ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( B ., B ) ) )
173 160 172 eqtrd 
 |-  ( ph -> ( ( T ( .s ` W ) B ) ., ( T ( .s ` W ) B ) ) = ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( B ., B ) ) )
174 158 173 oveq12d 
 |-  ( ph -> ( ( ( T ( .s ` W ) B ) ., A ) - ( ( T ( .s ` W ) B ) ., ( T ( .s ` W ) B ) ) ) = ( ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 1 ) ) - ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( B ., B ) ) ) )
175 pncan2 
 |-  ( ( ( B ., B ) e. CC /\ 1 e. CC ) -> ( ( ( B ., B ) + 1 ) - ( B ., B ) ) = 1 )
176 39 40 175 sylancl 
 |-  ( ph -> ( ( ( B ., B ) + 1 ) - ( B ., B ) ) = 1 )
177 176 oveq2d 
 |-  ( ph -> ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( ( B ., B ) + 1 ) - ( B ., B ) ) ) = ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. 1 ) )
178 119 120 39 subdid 
 |-  ( ph -> ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( ( B ., B ) + 1 ) - ( B ., B ) ) ) = ( ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 1 ) ) - ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( B ., B ) ) ) )
179 177 178 eqtr3d 
 |-  ( ph -> ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. 1 ) = ( ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 1 ) ) - ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( B ., B ) ) ) )
180 174 111 179 3eqtr4d 
 |-  ( ph -> ( ( T ( .s ` W ) B ) ., ( A .- ( T ( .s ` W ) B ) ) ) = ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. 1 ) )
181 152 180 oveq12d 
 |-  ( ph -> ( ( A ., ( T ( .s ` W ) B ) ) + ( ( T ( .s ` W ) B ) ., ( A .- ( T ( .s ` W ) B ) ) ) ) = ( ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 1 ) ) + ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. 1 ) ) )
182 122 123 181 3eqtr4rd 
 |-  ( ph -> ( ( A ., ( T ( .s ` W ) B ) ) + ( ( T ( .s ` W ) B ) ., ( A .- ( T ( .s ` W ) B ) ) ) ) = ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 2 ) ) )
183 182 oveq2d 
 |-  ( ph -> ( ( A ., A ) - ( ( A ., ( T ( .s ` W ) B ) ) + ( ( T ( .s ` W ) B ) ., ( A .- ( T ( .s ` W ) B ) ) ) ) ) = ( ( A ., A ) - ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 2 ) ) ) )
184 107 118 183 3eqtrd 
 |-  ( ph -> ( ( A ., ( A .- ( T ( .s ` W ) B ) ) ) - ( ( T ( .s ` W ) B ) ., ( A .- ( T ( .s ` W ) B ) ) ) ) = ( ( A ., A ) - ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 2 ) ) ) )
185 102 104 184 3eqtrd 
 |-  ( ph -> ( ( N ` ( A .- ( T ( .s ` W ) B ) ) ) ^ 2 ) = ( ( A ., A ) - ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 2 ) ) ) )
186 99 96 negsubd 
 |-  ( ph -> ( ( A ., A ) + -u ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 2 ) ) ) = ( ( A ., A ) - ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 2 ) ) ) )
187 99 97 addcomd 
 |-  ( ph -> ( ( A ., A ) + -u ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 2 ) ) ) = ( -u ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 2 ) ) + ( A ., A ) ) )
188 185 186 187 3eqtr2d 
 |-  ( ph -> ( ( N ` ( A .- ( T ( .s ` W ) B ) ) ) ^ 2 ) = ( -u ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 2 ) ) + ( A ., A ) ) )
189 1 5 2 nmsq 
 |-  ( ( W e. CPreHil /\ A e. V ) -> ( ( N ` A ) ^ 2 ) = ( A ., A ) )
190 14 9 189 syl2anc 
 |-  ( ph -> ( ( N ` A ) ^ 2 ) = ( A ., A ) )
191 188 190 oveq12d 
 |-  ( ph -> ( ( ( N ` ( A .- ( T ( .s ` W ) B ) ) ) ^ 2 ) - ( ( N ` A ) ^ 2 ) ) = ( ( -u ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 2 ) ) + ( A ., A ) ) - ( A ., A ) ) )
192 28 renegcld 
 |-  ( ph -> -u ( ( B ., B ) + 2 ) e. RR )
193 192 recnd 
 |-  ( ph -> -u ( ( B ., B ) + 2 ) e. CC )
194 143 193 149 150 div23d 
 |-  ( ph -> ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) x. -u ( ( B ., B ) + 2 ) ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) = ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. -u ( ( B ., B ) + 2 ) ) )
195 28 recnd 
 |-  ( ph -> ( ( B ., B ) + 2 ) e. CC )
196 119 195 mulneg2d 
 |-  ( ph -> ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. -u ( ( B ., B ) + 2 ) ) = -u ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 2 ) ) )
197 194 196 eqtrd 
 |-  ( ph -> ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) x. -u ( ( B ., B ) + 2 ) ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) = -u ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) x. ( ( B ., B ) + 2 ) ) )
198 100 191 197 3eqtr4rd 
 |-  ( ph -> ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) x. -u ( ( B ., B ) + 2 ) ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) = ( ( ( N ` ( A .- ( T ( .s ` W ) B ) ) ) ^ 2 ) - ( ( N ` A ) ^ 2 ) ) )
199 90 198 breqtrrd 
 |-  ( ph -> 0 <_ ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) x. -u ( ( B ., B ) + 2 ) ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) )
200 22 192 remulcld 
 |-  ( ph -> ( ( ( abs ` ( A ., B ) ) ^ 2 ) x. -u ( ( B ., B ) + 2 ) ) e. RR )
201 200 93 ge0divd 
 |-  ( ph -> ( 0 <_ ( ( ( abs ` ( A ., B ) ) ^ 2 ) x. -u ( ( B ., B ) + 2 ) ) <-> 0 <_ ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) x. -u ( ( B ., B ) + 2 ) ) / ( ( ( B ., B ) + 1 ) ^ 2 ) ) ) )
202 199 201 mpbird 
 |-  ( ph -> 0 <_ ( ( ( abs ` ( A ., B ) ) ^ 2 ) x. -u ( ( B ., B ) + 2 ) ) )
203 mulneg12 
 |-  ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) e. CC /\ ( ( B ., B ) + 2 ) e. CC ) -> ( -u ( ( abs ` ( A ., B ) ) ^ 2 ) x. ( ( B ., B ) + 2 ) ) = ( ( ( abs ` ( A ., B ) ) ^ 2 ) x. -u ( ( B ., B ) + 2 ) ) )
204 143 195 203 syl2anc 
 |-  ( ph -> ( -u ( ( abs ` ( A ., B ) ) ^ 2 ) x. ( ( B ., B ) + 2 ) ) = ( ( ( abs ` ( A ., B ) ) ^ 2 ) x. -u ( ( B ., B ) + 2 ) ) )
205 202 204 breqtrrd 
 |-  ( ph -> 0 <_ ( -u ( ( abs ` ( A ., B ) ) ^ 2 ) x. ( ( B ., B ) + 2 ) ) )
206 23 47 205 prodge0ld 
 |-  ( ph -> 0 <_ -u ( ( abs ` ( A ., B ) ) ^ 2 ) )
207 22 le0neg1d 
 |-  ( ph -> ( ( ( abs ` ( A ., B ) ) ^ 2 ) <_ 0 <-> 0 <_ -u ( ( abs ` ( A ., B ) ) ^ 2 ) ) )
208 206 207 mpbird 
 |-  ( ph -> ( ( abs ` ( A ., B ) ) ^ 2 ) <_ 0 )
209 20 sqge0d 
 |-  ( ph -> 0 <_ ( ( abs ` ( A ., B ) ) ^ 2 ) )
210 0re 
 |-  0 e. RR
211 letri3 
 |-  ( ( ( ( abs ` ( A ., B ) ) ^ 2 ) e. RR /\ 0 e. RR ) -> ( ( ( abs ` ( A ., B ) ) ^ 2 ) = 0 <-> ( ( ( abs ` ( A ., B ) ) ^ 2 ) <_ 0 /\ 0 <_ ( ( abs ` ( A ., B ) ) ^ 2 ) ) ) )
212 22 210 211 sylancl 
 |-  ( ph -> ( ( ( abs ` ( A ., B ) ) ^ 2 ) = 0 <-> ( ( ( abs ` ( A ., B ) ) ^ 2 ) <_ 0 /\ 0 <_ ( ( abs ` ( A ., B ) ) ^ 2 ) ) ) )
213 208 209 212 mpbir2and 
 |-  ( ph -> ( ( abs ` ( A ., B ) ) ^ 2 ) = 0 )
214 21 213 sqeq0d 
 |-  ( ph -> ( abs ` ( A ., B ) ) = 0 )
215 19 214 abs00d 
 |-  ( ph -> ( A ., B ) = 0 )