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 syl5eq
 |-  ( ( 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 syl5eq
 |-  ( ( 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 syl5eq
 |-  ( ( 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 ) ) )