Metamath Proof Explorer

Theorem ipcau2

Description: The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space built from a pre-Hilbert space with certain properties. The main theorem is ipcau . (Contributed by Mario Carneiro, 11-Oct-2015)

Ref Expression
Hypotheses tcphval.n 
|- G = ( toCPreHil ` W )
tcphcph.v 
|- V = ( Base ` W )
tcphcph.f 
|- F = ( Scalar ` W )
tcphcph.1 
|- ( ph -> W e. PreHil )
tcphcph.2 
|- ( ph -> F = ( CCfld |`s K ) )
tcphcph.h 
|- ., = ( .i ` W )
tcphcph.3 
|- ( ( ph /\ ( x e. K /\ x e. RR /\ 0 <_ x ) ) -> ( sqrt ` x ) e. K )
tcphcph.4 
|- ( ( ph /\ x e. V ) -> 0 <_ ( x ., x ) )
tcphcph.k 
|- K = ( Base ` F )
ipcau2.n 
|- N = ( norm ` G )
ipcau2.c 
|- C = ( ( Y ., X ) / ( Y ., Y ) )
ipcau2.3 
|- ( ph -> X e. V )
ipcau2.4 
|- ( ph -> Y e. V )
Assertion ipcau2 
|- ( ph -> ( abs ` ( X ., Y ) ) <_ ( ( N ` X ) x. ( N ` Y ) ) )

Proof

Step Hyp Ref Expression
1 tcphval.n 
 |-  G = ( toCPreHil ` W )
2 tcphcph.v 
 |-  V = ( Base ` W )
3 tcphcph.f 
 |-  F = ( Scalar ` W )
4 tcphcph.1 
 |-  ( ph -> W e. PreHil )
5 tcphcph.2 
 |-  ( ph -> F = ( CCfld |`s K ) )
6 tcphcph.h 
 |-  ., = ( .i ` W )
7 tcphcph.3 
 |-  ( ( ph /\ ( x e. K /\ x e. RR /\ 0 <_ x ) ) -> ( sqrt ` x ) e. K )
8 tcphcph.4 
 |-  ( ( ph /\ x e. V ) -> 0 <_ ( x ., x ) )
9 tcphcph.k 
 |-  K = ( Base ` F )
10 ipcau2.n 
 |-  N = ( norm ` G )
11 ipcau2.c 
 |-  C = ( ( Y ., X ) / ( Y ., Y ) )
12 ipcau2.3 
 |-  ( ph -> X e. V )
13 ipcau2.4 
 |-  ( ph -> Y e. V )
14 oveq2 
 |-  ( Y = ( 0g ` W ) -> ( X ., Y ) = ( X ., ( 0g ` W ) ) )
15 14 oveq1d 
 |-  ( Y = ( 0g ` W ) -> ( ( X ., Y ) x. ( Y ., X ) ) = ( ( X ., ( 0g ` W ) ) x. ( Y ., X ) ) )
16 15 breq1d 
 |-  ( Y = ( 0g ` W ) -> ( ( ( X ., Y ) x. ( Y ., X ) ) <_ ( ( X ., X ) x. ( Y ., Y ) ) <-> ( ( X ., ( 0g ` W ) ) x. ( Y ., X ) ) <_ ( ( X ., X ) x. ( Y ., Y ) ) ) )
17 1 2 3 4 5 phclm 
 |-  ( ph -> W e. CMod )
18 3 9 clmsscn 
 |-  ( W e. CMod -> K C_ CC )
19 17 18 syl 
 |-  ( ph -> K C_ CC )
20 3 6 2 9 ipcl 
 |-  ( ( W e. PreHil /\ X e. V /\ Y e. V ) -> ( X ., Y ) e. K )
21 4 12 13 20 syl3anc 
 |-  ( ph -> ( X ., Y ) e. K )
22 19 21 sseldd 
 |-  ( ph -> ( X ., Y ) e. CC )
23 22 adantr 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( X ., Y ) e. CC )
24 3 6 2 9 ipcl 
 |-  ( ( W e. PreHil /\ Y e. V /\ X e. V ) -> ( Y ., X ) e. K )
25 4 13 12 24 syl3anc 
 |-  ( ph -> ( Y ., X ) e. K )
26 19 25 sseldd 
 |-  ( ph -> ( Y ., X ) e. CC )
27 26 adantr 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( Y ., X ) e. CC )
28 1 2 3 4 5 6 tcphcphlem3 
 |-  ( ( ph /\ Y e. V ) -> ( Y ., Y ) e. RR )
29 13 28 mpdan 
 |-  ( ph -> ( Y ., Y ) e. RR )
30 29 recnd 
 |-  ( ph -> ( Y ., Y ) e. CC )
31 30 adantr 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( Y ., Y ) e. CC )
32 3 clm0 
 |-  ( W e. CMod -> 0 = ( 0g ` F ) )
33 17 32 syl 
 |-  ( ph -> 0 = ( 0g ` F ) )
34 33 eqeq2d 
 |-  ( ph -> ( ( Y ., Y ) = 0 <-> ( Y ., Y ) = ( 0g ` F ) ) )
35 eqid 
 |-  ( 0g ` F ) = ( 0g ` F )
36 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
37 3 6 2 35 36 ipeq0 
 |-  ( ( W e. PreHil /\ Y e. V ) -> ( ( Y ., Y ) = ( 0g ` F ) <-> Y = ( 0g ` W ) ) )
38 4 13 37 syl2anc 
 |-  ( ph -> ( ( Y ., Y ) = ( 0g ` F ) <-> Y = ( 0g ` W ) ) )
39 34 38 bitrd 
 |-  ( ph -> ( ( Y ., Y ) = 0 <-> Y = ( 0g ` W ) ) )
40 39 necon3bid 
 |-  ( ph -> ( ( Y ., Y ) =/= 0 <-> Y =/= ( 0g ` W ) ) )
41 40 biimpar 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( Y ., Y ) =/= 0 )
42 23 27 31 41 divassd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( X ., Y ) x. ( Y ., X ) ) / ( Y ., Y ) ) = ( ( X ., Y ) x. ( ( Y ., X ) / ( Y ., Y ) ) ) )
43 11 oveq2i 
 |-  ( ( X ., Y ) x. C ) = ( ( X ., Y ) x. ( ( Y ., X ) / ( Y ., Y ) ) )
44 42 43 eqtr4di 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( X ., Y ) x. ( Y ., X ) ) / ( Y ., Y ) ) = ( ( X ., Y ) x. C ) )
45 oveq12 
 |-  ( ( x = ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) /\ x = ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ) -> ( x ., x ) = ( ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ., ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ) )
46 45 anidms 
 |-  ( x = ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) -> ( x ., x ) = ( ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ., ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ) )
47 46 breq2d 
 |-  ( x = ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) -> ( 0 <_ ( x ., x ) <-> 0 <_ ( ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ., ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ) ) )
48 8 ralrimiva 
 |-  ( ph -> A. x e. V 0 <_ ( x ., x ) )
49 48 adantr 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> A. x e. V 0 <_ ( x ., x ) )
50 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
51 4 50 syl 
 |-  ( ph -> W e. LMod )
52 51 adantr 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> W e. LMod )
53 12 adantr 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> X e. V )
54 11 fveq2i 
 |-  ( * ` C ) = ( * ` ( ( Y ., X ) / ( Y ., Y ) ) )
55 27 31 41 cjdivd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( * ` ( ( Y ., X ) / ( Y ., Y ) ) ) = ( ( * ` ( Y ., X ) ) / ( * ` ( Y ., Y ) ) ) )
56 54 55 eqtrid 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( * ` C ) = ( ( * ` ( Y ., X ) ) / ( * ` ( Y ., Y ) ) ) )
57 5 fveq2d 
 |-  ( ph -> ( *r ` F ) = ( *r ` ( CCfld |`s K ) ) )
58 9 fvexi 
 |-  K e. _V
59 eqid 
 |-  ( CCfld |`s K ) = ( CCfld |`s K )
60 cnfldcj 
 |-  * = ( *r ` CCfld )
61 59 60 ressstarv 
 |-  ( K e. _V -> * = ( *r ` ( CCfld |`s K ) ) )
62 58 61 ax-mp 
 |-  * = ( *r ` ( CCfld |`s K ) )
63 57 62 eqtr4di 
 |-  ( ph -> ( *r ` F ) = * )
64 63 fveq1d 
 |-  ( ph -> ( ( *r ` F ) ` ( X ., Y ) ) = ( * ` ( X ., Y ) ) )
65 eqid 
 |-  ( *r ` F ) = ( *r ` F )
66 3 6 2 65 ipcj 
 |-  ( ( W e. PreHil /\ X e. V /\ Y e. V ) -> ( ( *r ` F ) ` ( X ., Y ) ) = ( Y ., X ) )
67 4 12 13 66 syl3anc 
 |-  ( ph -> ( ( *r ` F ) ` ( X ., Y ) ) = ( Y ., X ) )
68 64 67 eqtr3d 
 |-  ( ph -> ( * ` ( X ., Y ) ) = ( Y ., X ) )
69 68 adantr 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( * ` ( X ., Y ) ) = ( Y ., X ) )
70 69 fveq2d 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( * ` ( * ` ( X ., Y ) ) ) = ( * ` ( Y ., X ) ) )
71 23 cjcjd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( * ` ( * ` ( X ., Y ) ) ) = ( X ., Y ) )
72 70 71 eqtr3d 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( * ` ( Y ., X ) ) = ( X ., Y ) )
73 29 adantr 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( Y ., Y ) e. RR )
74 73 cjred 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( * ` ( Y ., Y ) ) = ( Y ., Y ) )
75 72 74 oveq12d 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( * ` ( Y ., X ) ) / ( * ` ( Y ., Y ) ) ) = ( ( X ., Y ) / ( Y ., Y ) ) )
76 23 31 41 divrecd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., Y ) / ( Y ., Y ) ) = ( ( X ., Y ) x. ( 1 / ( Y ., Y ) ) ) )
77 56 75 76 3eqtrd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( * ` C ) = ( ( X ., Y ) x. ( 1 / ( Y ., Y ) ) ) )
78 17 adantr 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> W e. CMod )
79 21 adantr 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( X ., Y ) e. K )
80 3 6 2 9 ipcl 
 |-  ( ( W e. PreHil /\ Y e. V /\ Y e. V ) -> ( Y ., Y ) e. K )
81 4 13 13 80 syl3anc 
 |-  ( ph -> ( Y ., Y ) e. K )
82 81 adantr 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( Y ., Y ) e. K )
83 5 adantr 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> F = ( CCfld |`s K ) )
84 phllvec 
 |-  ( W e. PreHil -> W e. LVec )
85 4 84 syl 
 |-  ( ph -> W e. LVec )
86 3 lvecdrng 
 |-  ( W e. LVec -> F e. DivRing )
87 85 86 syl 
 |-  ( ph -> F e. DivRing )
88 87 adantr 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> F e. DivRing )
89 9 83 88 cphreccllem 
 |-  ( ( ( ph /\ Y =/= ( 0g ` W ) ) /\ ( Y ., Y ) e. K /\ ( Y ., Y ) =/= 0 ) -> ( 1 / ( Y ., Y ) ) e. K )
90 82 41 89 mpd3an23 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( 1 / ( Y ., Y ) ) e. K )
91 3 9 clmmcl 
 |-  ( ( W e. CMod /\ ( X ., Y ) e. K /\ ( 1 / ( Y ., Y ) ) e. K ) -> ( ( X ., Y ) x. ( 1 / ( Y ., Y ) ) ) e. K )
92 78 79 90 91 syl3anc 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., Y ) x. ( 1 / ( Y ., Y ) ) ) e. K )
93 77 92 eqeltrd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( * ` C ) e. K )
94 13 adantr 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> Y e. V )
95 eqid 
 |-  ( .s ` W ) = ( .s ` W )
96 2 3 95 9 lmodvscl 
 |-  ( ( W e. LMod /\ ( * ` C ) e. K /\ Y e. V ) -> ( ( * ` C ) ( .s ` W ) Y ) e. V )
97 52 93 94 96 syl3anc 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( * ` C ) ( .s ` W ) Y ) e. V )
98 eqid 
 |-  ( -g ` W ) = ( -g ` W )
99 2 98 lmodvsubcl 
 |-  ( ( W e. LMod /\ X e. V /\ ( ( * ` C ) ( .s ` W ) Y ) e. V ) -> ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) e. V )
100 52 53 97 99 syl3anc 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) e. V )
101 47 49 100 rspcdva 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> 0 <_ ( ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ., ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ) )
102 eqid 
 |-  ( -g ` F ) = ( -g ` F )
103 eqid 
 |-  ( +g ` F ) = ( +g ` F )
104 4 adantr 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> W e. PreHil )
105 3 6 2 98 102 103 104 53 97 53 97 ip2subdi 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ., ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ) = ( ( ( X ., X ) ( +g ` F ) ( ( ( * ` C ) ( .s ` W ) Y ) ., ( ( * ` C ) ( .s ` W ) Y ) ) ) ( -g ` F ) ( ( X ., ( ( * ` C ) ( .s ` W ) Y ) ) ( +g ` F ) ( ( ( * ` C ) ( .s ` W ) Y ) ., X ) ) ) )
106 83 fveq2d 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( +g ` F ) = ( +g ` ( CCfld |`s K ) ) )
107 cnfldadd 
 |-  + = ( +g ` CCfld )
108 59 107 ressplusg 
 |-  ( K e. _V -> + = ( +g ` ( CCfld |`s K ) ) )
109 58 108 ax-mp 
 |-  + = ( +g ` ( CCfld |`s K ) )
110 106 109 eqtr4di 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( +g ` F ) = + )
111 eqidd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( X ., X ) = ( X ., X ) )
112 eqid 
 |-  ( .r ` F ) = ( .r ` F )
113 3 6 2 9 95 112 ipass 
 |-  ( ( W e. PreHil /\ ( ( * ` C ) e. K /\ Y e. V /\ ( ( * ` C ) ( .s ` W ) Y ) e. V ) ) -> ( ( ( * ` C ) ( .s ` W ) Y ) ., ( ( * ` C ) ( .s ` W ) Y ) ) = ( ( * ` C ) ( .r ` F ) ( Y ., ( ( * ` C ) ( .s ` W ) Y ) ) ) )
114 104 93 94 97 113 syl13anc 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( * ` C ) ( .s ` W ) Y ) ., ( ( * ` C ) ( .s ` W ) Y ) ) = ( ( * ` C ) ( .r ` F ) ( Y ., ( ( * ` C ) ( .s ` W ) Y ) ) ) )
115 83 fveq2d 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( .r ` F ) = ( .r ` ( CCfld |`s K ) ) )
116 cnfldmul 
 |-  x. = ( .r ` CCfld )
117 59 116 ressmulr 
 |-  ( K e. _V -> x. = ( .r ` ( CCfld |`s K ) ) )
118 58 117 ax-mp 
 |-  x. = ( .r ` ( CCfld |`s K ) )
119 115 118 eqtr4di 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( .r ` F ) = x. )
120 eqidd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( * ` C ) = ( * ` C ) )
121 27 31 41 divrecd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( Y ., X ) / ( Y ., Y ) ) = ( ( Y ., X ) x. ( 1 / ( Y ., Y ) ) ) )
122 11 121 eqtrid 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> C = ( ( Y ., X ) x. ( 1 / ( Y ., Y ) ) ) )
123 25 adantr 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( Y ., X ) e. K )
124 3 9 clmmcl 
 |-  ( ( W e. CMod /\ ( Y ., X ) e. K /\ ( 1 / ( Y ., Y ) ) e. K ) -> ( ( Y ., X ) x. ( 1 / ( Y ., Y ) ) ) e. K )
125 78 123 90 124 syl3anc 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( Y ., X ) x. ( 1 / ( Y ., Y ) ) ) e. K )
126 122 125 eqeltrd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> C e. K )
127 3 6 2 9 95 112 65 ipassr2 
 |-  ( ( W e. PreHil /\ ( Y e. V /\ Y e. V /\ C e. K ) ) -> ( ( Y ., Y ) ( .r ` F ) C ) = ( Y ., ( ( ( *r ` F ) ` C ) ( .s ` W ) Y ) ) )
128 104 94 94 126 127 syl13anc 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( Y ., Y ) ( .r ` F ) C ) = ( Y ., ( ( ( *r ` F ) ` C ) ( .s ` W ) Y ) ) )
129 119 oveqd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( Y ., Y ) ( .r ` F ) C ) = ( ( Y ., Y ) x. C ) )
130 11 oveq2i 
 |-  ( ( Y ., Y ) x. C ) = ( ( Y ., Y ) x. ( ( Y ., X ) / ( Y ., Y ) ) )
131 27 31 41 divcan2d 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( Y ., Y ) x. ( ( Y ., X ) / ( Y ., Y ) ) ) = ( Y ., X ) )
132 130 131 eqtrid 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( Y ., Y ) x. C ) = ( Y ., X ) )
133 129 132 eqtrd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( Y ., Y ) ( .r ` F ) C ) = ( Y ., X ) )
134 63 adantr 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( *r ` F ) = * )
135 134 fveq1d 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( *r ` F ) ` C ) = ( * ` C ) )
136 135 oveq1d 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( *r ` F ) ` C ) ( .s ` W ) Y ) = ( ( * ` C ) ( .s ` W ) Y ) )
137 136 oveq2d 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( Y ., ( ( ( *r ` F ) ` C ) ( .s ` W ) Y ) ) = ( Y ., ( ( * ` C ) ( .s ` W ) Y ) ) )
138 128 133 137 3eqtr3rd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( Y ., ( ( * ` C ) ( .s ` W ) Y ) ) = ( Y ., X ) )
139 119 120 138 oveq123d 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( * ` C ) ( .r ` F ) ( Y ., ( ( * ` C ) ( .s ` W ) Y ) ) ) = ( ( * ` C ) x. ( Y ., X ) ) )
140 114 139 eqtrd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( * ` C ) ( .s ` W ) Y ) ., ( ( * ` C ) ( .s ` W ) Y ) ) = ( ( * ` C ) x. ( Y ., X ) ) )
141 110 111 140 oveq123d 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., X ) ( +g ` F ) ( ( ( * ` C ) ( .s ` W ) Y ) ., ( ( * ` C ) ( .s ` W ) Y ) ) ) = ( ( X ., X ) + ( ( * ` C ) x. ( Y ., X ) ) ) )
142 3 6 2 9 95 112 65 ipassr2 
 |-  ( ( W e. PreHil /\ ( X e. V /\ Y e. V /\ C e. K ) ) -> ( ( X ., Y ) ( .r ` F ) C ) = ( X ., ( ( ( *r ` F ) ` C ) ( .s ` W ) Y ) ) )
143 104 53 94 126 142 syl13anc 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., Y ) ( .r ` F ) C ) = ( X ., ( ( ( *r ` F ) ` C ) ( .s ` W ) Y ) ) )
144 119 oveqd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., Y ) ( .r ` F ) C ) = ( ( X ., Y ) x. C ) )
145 136 oveq2d 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( X ., ( ( ( *r ` F ) ` C ) ( .s ` W ) Y ) ) = ( X ., ( ( * ` C ) ( .s ` W ) Y ) ) )
146 143 144 145 3eqtr3rd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( X ., ( ( * ` C ) ( .s ` W ) Y ) ) = ( ( X ., Y ) x. C ) )
147 3 6 2 9 95 112 ipass 
 |-  ( ( W e. PreHil /\ ( ( * ` C ) e. K /\ Y e. V /\ X e. V ) ) -> ( ( ( * ` C ) ( .s ` W ) Y ) ., X ) = ( ( * ` C ) ( .r ` F ) ( Y ., X ) ) )
148 104 93 94 53 147 syl13anc 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( * ` C ) ( .s ` W ) Y ) ., X ) = ( ( * ` C ) ( .r ` F ) ( Y ., X ) ) )
149 119 oveqd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( * ` C ) ( .r ` F ) ( Y ., X ) ) = ( ( * ` C ) x. ( Y ., X ) ) )
150 148 149 eqtrd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( * ` C ) ( .s ` W ) Y ) ., X ) = ( ( * ` C ) x. ( Y ., X ) ) )
151 110 146 150 oveq123d 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., ( ( * ` C ) ( .s ` W ) Y ) ) ( +g ` F ) ( ( ( * ` C ) ( .s ` W ) Y ) ., X ) ) = ( ( ( X ., Y ) x. C ) + ( ( * ` C ) x. ( Y ., X ) ) ) )
152 141 151 oveq12d 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( X ., X ) ( +g ` F ) ( ( ( * ` C ) ( .s ` W ) Y ) ., ( ( * ` C ) ( .s ` W ) Y ) ) ) ( -g ` F ) ( ( X ., ( ( * ` C ) ( .s ` W ) Y ) ) ( +g ` F ) ( ( ( * ` C ) ( .s ` W ) Y ) ., X ) ) ) = ( ( ( X ., X ) + ( ( * ` C ) x. ( Y ., X ) ) ) ( -g ` F ) ( ( ( X ., Y ) x. C ) + ( ( * ` C ) x. ( Y ., X ) ) ) ) )
153 3 6 2 9 ipcl 
 |-  ( ( W e. PreHil /\ X e. V /\ X e. V ) -> ( X ., X ) e. K )
154 104 53 53 153 syl3anc 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( X ., X ) e. K )
155 3 9 clmmcl 
 |-  ( ( W e. CMod /\ ( * ` C ) e. K /\ ( Y ., X ) e. K ) -> ( ( * ` C ) x. ( Y ., X ) ) e. K )
156 78 93 123 155 syl3anc 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( * ` C ) x. ( Y ., X ) ) e. K )
157 3 9 clmacl 
 |-  ( ( W e. CMod /\ ( X ., X ) e. K /\ ( ( * ` C ) x. ( Y ., X ) ) e. K ) -> ( ( X ., X ) + ( ( * ` C ) x. ( Y ., X ) ) ) e. K )
158 78 154 156 157 syl3anc 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., X ) + ( ( * ` C ) x. ( Y ., X ) ) ) e. K )
159 3 9 clmmcl 
 |-  ( ( W e. CMod /\ ( X ., Y ) e. K /\ C e. K ) -> ( ( X ., Y ) x. C ) e. K )
160 78 79 126 159 syl3anc 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., Y ) x. C ) e. K )
161 3 9 clmacl 
 |-  ( ( W e. CMod /\ ( ( X ., Y ) x. C ) e. K /\ ( ( * ` C ) x. ( Y ., X ) ) e. K ) -> ( ( ( X ., Y ) x. C ) + ( ( * ` C ) x. ( Y ., X ) ) ) e. K )
162 78 160 156 161 syl3anc 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( X ., Y ) x. C ) + ( ( * ` C ) x. ( Y ., X ) ) ) e. K )
163 3 9 clmsub 
 |-  ( ( W e. CMod /\ ( ( X ., X ) + ( ( * ` C ) x. ( Y ., X ) ) ) e. K /\ ( ( ( X ., Y ) x. C ) + ( ( * ` C ) x. ( Y ., X ) ) ) e. K ) -> ( ( ( X ., X ) + ( ( * ` C ) x. ( Y ., X ) ) ) - ( ( ( X ., Y ) x. C ) + ( ( * ` C ) x. ( Y ., X ) ) ) ) = ( ( ( X ., X ) + ( ( * ` C ) x. ( Y ., X ) ) ) ( -g ` F ) ( ( ( X ., Y ) x. C ) + ( ( * ` C ) x. ( Y ., X ) ) ) ) )
164 78 158 162 163 syl3anc 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( X ., X ) + ( ( * ` C ) x. ( Y ., X ) ) ) - ( ( ( X ., Y ) x. C ) + ( ( * ` C ) x. ( Y ., X ) ) ) ) = ( ( ( X ., X ) + ( ( * ` C ) x. ( Y ., X ) ) ) ( -g ` F ) ( ( ( X ., Y ) x. C ) + ( ( * ` C ) x. ( Y ., X ) ) ) ) )
165 1 2 3 4 5 6 tcphcphlem3 
 |-  ( ( ph /\ X e. V ) -> ( X ., X ) e. RR )
166 12 165 mpdan 
 |-  ( ph -> ( X ., X ) e. RR )
167 166 recnd 
 |-  ( ph -> ( X ., X ) e. CC )
168 167 adantr 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( X ., X ) e. CC )
169 22 absvalsqd 
 |-  ( ph -> ( ( abs ` ( X ., Y ) ) ^ 2 ) = ( ( X ., Y ) x. ( * ` ( X ., Y ) ) ) )
170 68 oveq2d 
 |-  ( ph -> ( ( X ., Y ) x. ( * ` ( X ., Y ) ) ) = ( ( X ., Y ) x. ( Y ., X ) ) )
171 169 170 eqtrd 
 |-  ( ph -> ( ( abs ` ( X ., Y ) ) ^ 2 ) = ( ( X ., Y ) x. ( Y ., X ) ) )
172 22 abscld 
 |-  ( ph -> ( abs ` ( X ., Y ) ) e. RR )
173 172 resqcld 
 |-  ( ph -> ( ( abs ` ( X ., Y ) ) ^ 2 ) e. RR )
174 171 173 eqeltrrd 
 |-  ( ph -> ( ( X ., Y ) x. ( Y ., X ) ) e. RR )
175 174 adantr 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., Y ) x. ( Y ., X ) ) e. RR )
176 175 73 41 redivcld 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( X ., Y ) x. ( Y ., X ) ) / ( Y ., Y ) ) e. RR )
177 44 176 eqeltrrd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., Y ) x. C ) e. RR )
178 177 recnd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., Y ) x. C ) e. CC )
179 78 18 syl 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> K C_ CC )
180 179 156 sseldd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( * ` C ) x. ( Y ., X ) ) e. CC )
181 168 178 180 pnpcan2d 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( X ., X ) + ( ( * ` C ) x. ( Y ., X ) ) ) - ( ( ( X ., Y ) x. C ) + ( ( * ` C ) x. ( Y ., X ) ) ) ) = ( ( X ., X ) - ( ( X ., Y ) x. C ) ) )
182 164 181 eqtr3d 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( X ., X ) + ( ( * ` C ) x. ( Y ., X ) ) ) ( -g ` F ) ( ( ( X ., Y ) x. C ) + ( ( * ` C ) x. ( Y ., X ) ) ) ) = ( ( X ., X ) - ( ( X ., Y ) x. C ) ) )
183 105 152 182 3eqtrd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ., ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ) = ( ( X ., X ) - ( ( X ., Y ) x. C ) ) )
184 101 183 breqtrd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> 0 <_ ( ( X ., X ) - ( ( X ., Y ) x. C ) ) )
185 166 adantr 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( X ., X ) e. RR )
186 185 177 subge0d 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( 0 <_ ( ( X ., X ) - ( ( X ., Y ) x. C ) ) <-> ( ( X ., Y ) x. C ) <_ ( X ., X ) ) )
187 184 186 mpbid 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., Y ) x. C ) <_ ( X ., X ) )
188 44 187 eqbrtrd 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( X ., Y ) x. ( Y ., X ) ) / ( Y ., Y ) ) <_ ( X ., X ) )
189 oveq12 
 |-  ( ( x = Y /\ x = Y ) -> ( x ., x ) = ( Y ., Y ) )
190 189 anidms 
 |-  ( x = Y -> ( x ., x ) = ( Y ., Y ) )
191 190 breq2d 
 |-  ( x = Y -> ( 0 <_ ( x ., x ) <-> 0 <_ ( Y ., Y ) ) )
192 191 48 13 rspcdva 
 |-  ( ph -> 0 <_ ( Y ., Y ) )
193 192 adantr 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> 0 <_ ( Y ., Y ) )
194 73 193 41 ne0gt0d 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> 0 < ( Y ., Y ) )
195 ledivmul2 
 |-  ( ( ( ( X ., Y ) x. ( Y ., X ) ) e. RR /\ ( X ., X ) e. RR /\ ( ( Y ., Y ) e. RR /\ 0 < ( Y ., Y ) ) ) -> ( ( ( ( X ., Y ) x. ( Y ., X ) ) / ( Y ., Y ) ) <_ ( X ., X ) <-> ( ( X ., Y ) x. ( Y ., X ) ) <_ ( ( X ., X ) x. ( Y ., Y ) ) ) )
196 175 185 73 194 195 syl112anc 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( ( X ., Y ) x. ( Y ., X ) ) / ( Y ., Y ) ) <_ ( X ., X ) <-> ( ( X ., Y ) x. ( Y ., X ) ) <_ ( ( X ., X ) x. ( Y ., Y ) ) ) )
197 188 196 mpbid 
 |-  ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., Y ) x. ( Y ., X ) ) <_ ( ( X ., X ) x. ( Y ., Y ) ) )
198 3 6 2 35 36 ip0r 
 |-  ( ( W e. PreHil /\ X e. V ) -> ( X ., ( 0g ` W ) ) = ( 0g ` F ) )
199 4 12 198 syl2anc 
 |-  ( ph -> ( X ., ( 0g ` W ) ) = ( 0g ` F ) )
200 199 33 eqtr4d 
 |-  ( ph -> ( X ., ( 0g ` W ) ) = 0 )
201 200 oveq1d 
 |-  ( ph -> ( ( X ., ( 0g ` W ) ) x. ( Y ., X ) ) = ( 0 x. ( Y ., X ) ) )
202 26 mul02d 
 |-  ( ph -> ( 0 x. ( Y ., X ) ) = 0 )
203 201 202 eqtrd 
 |-  ( ph -> ( ( X ., ( 0g ` W ) ) x. ( Y ., X ) ) = 0 )
204 oveq12 
 |-  ( ( x = X /\ x = X ) -> ( x ., x ) = ( X ., X ) )
205 204 anidms 
 |-  ( x = X -> ( x ., x ) = ( X ., X ) )
206 205 breq2d 
 |-  ( x = X -> ( 0 <_ ( x ., x ) <-> 0 <_ ( X ., X ) ) )
207 206 48 12 rspcdva 
 |-  ( ph -> 0 <_ ( X ., X ) )
208 166 29 207 192 mulge0d 
 |-  ( ph -> 0 <_ ( ( X ., X ) x. ( Y ., Y ) ) )
209 203 208 eqbrtrd 
 |-  ( ph -> ( ( X ., ( 0g ` W ) ) x. ( Y ., X ) ) <_ ( ( X ., X ) x. ( Y ., Y ) ) )
210 16 197 209 pm2.61ne 
 |-  ( ph -> ( ( X ., Y ) x. ( Y ., X ) ) <_ ( ( X ., X ) x. ( Y ., Y ) ) )
211 166 207 resqrtcld 
 |-  ( ph -> ( sqrt ` ( X ., X ) ) e. RR )
212 211 recnd 
 |-  ( ph -> ( sqrt ` ( X ., X ) ) e. CC )
213 29 192 resqrtcld 
 |-  ( ph -> ( sqrt ` ( Y ., Y ) ) e. RR )
214 213 recnd 
 |-  ( ph -> ( sqrt ` ( Y ., Y ) ) e. CC )
215 212 214 sqmuld 
 |-  ( ph -> ( ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ^ 2 ) = ( ( ( sqrt ` ( X ., X ) ) ^ 2 ) x. ( ( sqrt ` ( Y ., Y ) ) ^ 2 ) ) )
216 167 sqsqrtd 
 |-  ( ph -> ( ( sqrt ` ( X ., X ) ) ^ 2 ) = ( X ., X ) )
217 30 sqsqrtd 
 |-  ( ph -> ( ( sqrt ` ( Y ., Y ) ) ^ 2 ) = ( Y ., Y ) )
218 216 217 oveq12d 
 |-  ( ph -> ( ( ( sqrt ` ( X ., X ) ) ^ 2 ) x. ( ( sqrt ` ( Y ., Y ) ) ^ 2 ) ) = ( ( X ., X ) x. ( Y ., Y ) ) )
219 215 218 eqtrd 
 |-  ( ph -> ( ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ^ 2 ) = ( ( X ., X ) x. ( Y ., Y ) ) )
220 210 171 219 3brtr4d 
 |-  ( ph -> ( ( abs ` ( X ., Y ) ) ^ 2 ) <_ ( ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ^ 2 ) )
221 211 213 remulcld 
 |-  ( ph -> ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) e. RR )
222 22 absge0d 
 |-  ( ph -> 0 <_ ( abs ` ( X ., Y ) ) )
223 166 207 sqrtge0d 
 |-  ( ph -> 0 <_ ( sqrt ` ( X ., X ) ) )
224 29 192 sqrtge0d 
 |-  ( ph -> 0 <_ ( sqrt ` ( Y ., Y ) ) )
225 211 213 223 224 mulge0d 
 |-  ( ph -> 0 <_ ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) )
226 172 221 222 225 le2sqd 
 |-  ( ph -> ( ( abs ` ( X ., Y ) ) <_ ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) <-> ( ( abs ` ( X ., Y ) ) ^ 2 ) <_ ( ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ^ 2 ) ) )
227 220 226 mpbird 
 |-  ( ph -> ( abs ` ( X ., Y ) ) <_ ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) )
228 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
229 51 228 syl 
 |-  ( ph -> W e. Grp )
230 1 10 2 6 tcphnmval 
 |-  ( ( W e. Grp /\ X e. V ) -> ( N ` X ) = ( sqrt ` ( X ., X ) ) )
231 229 12 230 syl2anc 
 |-  ( ph -> ( N ` X ) = ( sqrt ` ( X ., X ) ) )
232 1 10 2 6 tcphnmval 
 |-  ( ( W e. Grp /\ Y e. V ) -> ( N ` Y ) = ( sqrt ` ( Y ., Y ) ) )
233 229 13 232 syl2anc 
 |-  ( ph -> ( N ` Y ) = ( sqrt ` ( Y ., Y ) ) )
234 231 233 oveq12d 
 |-  ( ph -> ( ( N ` X ) x. ( N ` Y ) ) = ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) )
235 227 234 breqtrrd 
 |-  ( ph -> ( abs ` ( X ., Y ) ) <_ ( ( N ` X ) x. ( N ` Y ) ) )