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=toCPreHilW
tcphcph.v V=BaseW
tcphcph.f F=ScalarW
tcphcph.1 φWPreHil
tcphcph.2 φF=fld𝑠K
tcphcph.h ,˙=𝑖W
tcphcph.3 φxKx0xxK
tcphcph.4 φxV0x,˙x
tcphcph.k K=BaseF
ipcau2.n N=normG
ipcau2.c C=Y,˙XY,˙Y
ipcau2.3 φXV
ipcau2.4 φYV
Assertion ipcau2 φX,˙YNXNY

Proof

Step Hyp Ref Expression
1 tcphval.n G=toCPreHilW
2 tcphcph.v V=BaseW
3 tcphcph.f F=ScalarW
4 tcphcph.1 φWPreHil
5 tcphcph.2 φF=fld𝑠K
6 tcphcph.h ,˙=𝑖W
7 tcphcph.3 φxKx0xxK
8 tcphcph.4 φxV0x,˙x
9 tcphcph.k K=BaseF
10 ipcau2.n N=normG
11 ipcau2.c C=Y,˙XY,˙Y
12 ipcau2.3 φXV
13 ipcau2.4 φYV
14 oveq2 Y=0WX,˙Y=X,˙0W
15 14 oveq1d Y=0WX,˙YY,˙X=X,˙0WY,˙X
16 15 breq1d Y=0WX,˙YY,˙XX,˙XY,˙YX,˙0WY,˙XX,˙XY,˙Y
17 1 2 3 4 5 phclm φWCMod
18 3 9 clmsscn WCModK
19 17 18 syl φK
20 3 6 2 9 ipcl WPreHilXVYVX,˙YK
21 4 12 13 20 syl3anc φX,˙YK
22 19 21 sseldd φX,˙Y
23 22 adantr φY0WX,˙Y
24 3 6 2 9 ipcl WPreHilYVXVY,˙XK
25 4 13 12 24 syl3anc φY,˙XK
26 19 25 sseldd φY,˙X
27 26 adantr φY0WY,˙X
28 1 2 3 4 5 6 tcphcphlem3 φYVY,˙Y
29 13 28 mpdan φY,˙Y
30 29 recnd φY,˙Y
31 30 adantr φY0WY,˙Y
32 3 clm0 WCMod0=0F
33 17 32 syl φ0=0F
34 33 eqeq2d φY,˙Y=0Y,˙Y=0F
35 eqid 0F=0F
36 eqid 0W=0W
37 3 6 2 35 36 ipeq0 WPreHilYVY,˙Y=0FY=0W
38 4 13 37 syl2anc φY,˙Y=0FY=0W
39 34 38 bitrd φY,˙Y=0Y=0W
40 39 necon3bid φY,˙Y0Y0W
41 40 biimpar φY0WY,˙Y0
42 23 27 31 41 divassd φY0WX,˙YY,˙XY,˙Y=X,˙YY,˙XY,˙Y
43 11 oveq2i X,˙YC=X,˙YY,˙XY,˙Y
44 42 43 eqtr4di φY0WX,˙YY,˙XY,˙Y=X,˙YC
45 oveq12 x=X-WCWYx=X-WCWYx,˙x=X-WCWY,˙X-WCWY
46 45 anidms x=X-WCWYx,˙x=X-WCWY,˙X-WCWY
47 46 breq2d x=X-WCWY0x,˙x0X-WCWY,˙X-WCWY
48 8 ralrimiva φxV0x,˙x
49 48 adantr φY0WxV0x,˙x
50 phllmod WPreHilWLMod
51 4 50 syl φWLMod
52 51 adantr φY0WWLMod
53 12 adantr φY0WXV
54 11 fveq2i C=Y,˙XY,˙Y
55 27 31 41 cjdivd φY0WY,˙XY,˙Y=Y,˙XY,˙Y
56 54 55 eqtrid φY0WC=Y,˙XY,˙Y
57 5 fveq2d φ*F=*fld𝑠K
58 9 fvexi KV
59 eqid fld𝑠K=fld𝑠K
60 cnfldcj *=*fld
61 59 60 ressstarv KV*=*fld𝑠K
62 58 61 ax-mp *=*fld𝑠K
63 57 62 eqtr4di φ*F=*
64 63 fveq1d φX,˙Y*F=X,˙Y
65 eqid *F=*F
66 3 6 2 65 ipcj WPreHilXVYVX,˙Y*F=Y,˙X
67 4 12 13 66 syl3anc φX,˙Y*F=Y,˙X
68 64 67 eqtr3d φX,˙Y=Y,˙X
69 68 adantr φY0WX,˙Y=Y,˙X
70 69 fveq2d φY0WX,˙Y=Y,˙X
71 23 cjcjd φY0WX,˙Y=X,˙Y
72 70 71 eqtr3d φY0WY,˙X=X,˙Y
73 29 adantr φY0WY,˙Y
74 73 cjred φY0WY,˙Y=Y,˙Y
75 72 74 oveq12d φY0WY,˙XY,˙Y=X,˙YY,˙Y
76 23 31 41 divrecd φY0WX,˙YY,˙Y=X,˙Y1Y,˙Y
77 56 75 76 3eqtrd φY0WC=X,˙Y1Y,˙Y
78 17 adantr φY0WWCMod
79 21 adantr φY0WX,˙YK
80 3 6 2 9 ipcl WPreHilYVYVY,˙YK
81 4 13 13 80 syl3anc φY,˙YK
82 81 adantr φY0WY,˙YK
83 5 adantr φY0WF=fld𝑠K
84 phllvec WPreHilWLVec
85 4 84 syl φWLVec
86 3 lvecdrng WLVecFDivRing
87 85 86 syl φFDivRing
88 87 adantr φY0WFDivRing
89 9 83 88 cphreccllem φY0WY,˙YKY,˙Y01Y,˙YK
90 82 41 89 mpd3an23 φY0W1Y,˙YK
91 3 9 clmmcl WCModX,˙YK1Y,˙YKX,˙Y1Y,˙YK
92 78 79 90 91 syl3anc φY0WX,˙Y1Y,˙YK
93 77 92 eqeltrd φY0WCK
94 13 adantr φY0WYV
95 eqid W=W
96 2 3 95 9 lmodvscl WLModCKYVCWYV
97 52 93 94 96 syl3anc φY0WCWYV
98 eqid -W=-W
99 2 98 lmodvsubcl WLModXVCWYVX-WCWYV
100 52 53 97 99 syl3anc φY0WX-WCWYV
101 47 49 100 rspcdva φY0W0X-WCWY,˙X-WCWY
102 eqid -F=-F
103 eqid +F=+F
104 4 adantr φY0WWPreHil
105 3 6 2 98 102 103 104 53 97 53 97 ip2subdi φY0WX-WCWY,˙X-WCWY=X,˙X+FCWY,˙CWY-FX,˙CWY+FCWY,˙X
106 83 fveq2d φY0W+F=+fld𝑠K
107 cnfldadd +=+fld
108 59 107 ressplusg KV+=+fld𝑠K
109 58 108 ax-mp +=+fld𝑠K
110 106 109 eqtr4di φY0W+F=+
111 eqidd φY0WX,˙X=X,˙X
112 eqid F=F
113 3 6 2 9 95 112 ipass WPreHilCKYVCWYVCWY,˙CWY=CFY,˙CWY
114 104 93 94 97 113 syl13anc φY0WCWY,˙CWY=CFY,˙CWY
115 83 fveq2d φY0WF=fld𝑠K
116 cnfldmul ×=fld
117 59 116 ressmulr KV×=fld𝑠K
118 58 117 ax-mp ×=fld𝑠K
119 115 118 eqtr4di φY0WF=×
120 eqidd φY0WC=C
121 27 31 41 divrecd φY0WY,˙XY,˙Y=Y,˙X1Y,˙Y
122 11 121 eqtrid φY0WC=Y,˙X1Y,˙Y
123 25 adantr φY0WY,˙XK
124 3 9 clmmcl WCModY,˙XK1Y,˙YKY,˙X1Y,˙YK
125 78 123 90 124 syl3anc φY0WY,˙X1Y,˙YK
126 122 125 eqeltrd φY0WCK
127 3 6 2 9 95 112 65 ipassr2 WPreHilYVYVCKY,˙YFC=Y,˙C*FWY
128 104 94 94 126 127 syl13anc φY0WY,˙YFC=Y,˙C*FWY
129 119 oveqd φY0WY,˙YFC=Y,˙YC
130 11 oveq2i Y,˙YC=Y,˙YY,˙XY,˙Y
131 27 31 41 divcan2d φY0WY,˙YY,˙XY,˙Y=Y,˙X
132 130 131 eqtrid φY0WY,˙YC=Y,˙X
133 129 132 eqtrd φY0WY,˙YFC=Y,˙X
134 63 adantr φY0W*F=*
135 134 fveq1d φY0WC*F=C
136 135 oveq1d φY0WC*FWY=CWY
137 136 oveq2d φY0WY,˙C*FWY=Y,˙CWY
138 128 133 137 3eqtr3rd φY0WY,˙CWY=Y,˙X
139 119 120 138 oveq123d φY0WCFY,˙CWY=CY,˙X
140 114 139 eqtrd φY0WCWY,˙CWY=CY,˙X
141 110 111 140 oveq123d φY0WX,˙X+FCWY,˙CWY=X,˙X+CY,˙X
142 3 6 2 9 95 112 65 ipassr2 WPreHilXVYVCKX,˙YFC=X,˙C*FWY
143 104 53 94 126 142 syl13anc φY0WX,˙YFC=X,˙C*FWY
144 119 oveqd φY0WX,˙YFC=X,˙YC
145 136 oveq2d φY0WX,˙C*FWY=X,˙CWY
146 143 144 145 3eqtr3rd φY0WX,˙CWY=X,˙YC
147 3 6 2 9 95 112 ipass WPreHilCKYVXVCWY,˙X=CFY,˙X
148 104 93 94 53 147 syl13anc φY0WCWY,˙X=CFY,˙X
149 119 oveqd φY0WCFY,˙X=CY,˙X
150 148 149 eqtrd φY0WCWY,˙X=CY,˙X
151 110 146 150 oveq123d φY0WX,˙CWY+FCWY,˙X=X,˙YC+CY,˙X
152 141 151 oveq12d φY0WX,˙X+FCWY,˙CWY-FX,˙CWY+FCWY,˙X=X,˙X+CY,˙X-FX,˙YC+CY,˙X
153 3 6 2 9 ipcl WPreHilXVXVX,˙XK
154 104 53 53 153 syl3anc φY0WX,˙XK
155 3 9 clmmcl WCModCKY,˙XKCY,˙XK
156 78 93 123 155 syl3anc φY0WCY,˙XK
157 3 9 clmacl WCModX,˙XKCY,˙XKX,˙X+CY,˙XK
158 78 154 156 157 syl3anc φY0WX,˙X+CY,˙XK
159 3 9 clmmcl WCModX,˙YKCKX,˙YCK
160 78 79 126 159 syl3anc φY0WX,˙YCK
161 3 9 clmacl WCModX,˙YCKCY,˙XKX,˙YC+CY,˙XK
162 78 160 156 161 syl3anc φY0WX,˙YC+CY,˙XK
163 3 9 clmsub WCModX,˙X+CY,˙XKX,˙YC+CY,˙XKX,˙X+CY,˙X-X,˙YC+CY,˙X=X,˙X+CY,˙X-FX,˙YC+CY,˙X
164 78 158 162 163 syl3anc φY0WX,˙X+CY,˙X-X,˙YC+CY,˙X=X,˙X+CY,˙X-FX,˙YC+CY,˙X
165 1 2 3 4 5 6 tcphcphlem3 φXVX,˙X
166 12 165 mpdan φX,˙X
167 166 recnd φX,˙X
168 167 adantr φY0WX,˙X
169 22 absvalsqd φX,˙Y2=X,˙YX,˙Y
170 68 oveq2d φX,˙YX,˙Y=X,˙YY,˙X
171 169 170 eqtrd φX,˙Y2=X,˙YY,˙X
172 22 abscld φX,˙Y
173 172 resqcld φX,˙Y2
174 171 173 eqeltrrd φX,˙YY,˙X
175 174 adantr φY0WX,˙YY,˙X
176 175 73 41 redivcld φY0WX,˙YY,˙XY,˙Y
177 44 176 eqeltrrd φY0WX,˙YC
178 177 recnd φY0WX,˙YC
179 78 18 syl φY0WK
180 179 156 sseldd φY0WCY,˙X
181 168 178 180 pnpcan2d φY0WX,˙X+CY,˙X-X,˙YC+CY,˙X=X,˙XX,˙YC
182 164 181 eqtr3d φY0WX,˙X+CY,˙X-FX,˙YC+CY,˙X=X,˙XX,˙YC
183 105 152 182 3eqtrd φY0WX-WCWY,˙X-WCWY=X,˙XX,˙YC
184 101 183 breqtrd φY0W0X,˙XX,˙YC
185 166 adantr φY0WX,˙X
186 185 177 subge0d φY0W0X,˙XX,˙YCX,˙YCX,˙X
187 184 186 mpbid φY0WX,˙YCX,˙X
188 44 187 eqbrtrd φY0WX,˙YY,˙XY,˙YX,˙X
189 oveq12 x=Yx=Yx,˙x=Y,˙Y
190 189 anidms x=Yx,˙x=Y,˙Y
191 190 breq2d x=Y0x,˙x0Y,˙Y
192 191 48 13 rspcdva φ0Y,˙Y
193 192 adantr φY0W0Y,˙Y
194 73 193 41 ne0gt0d φY0W0<Y,˙Y
195 ledivmul2 X,˙YY,˙XX,˙XY,˙Y0<Y,˙YX,˙YY,˙XY,˙YX,˙XX,˙YY,˙XX,˙XY,˙Y
196 175 185 73 194 195 syl112anc φY0WX,˙YY,˙XY,˙YX,˙XX,˙YY,˙XX,˙XY,˙Y
197 188 196 mpbid φY0WX,˙YY,˙XX,˙XY,˙Y
198 3 6 2 35 36 ip0r WPreHilXVX,˙0W=0F
199 4 12 198 syl2anc φX,˙0W=0F
200 199 33 eqtr4d φX,˙0W=0
201 200 oveq1d φX,˙0WY,˙X=0Y,˙X
202 26 mul02d φ0Y,˙X=0
203 201 202 eqtrd φX,˙0WY,˙X=0
204 oveq12 x=Xx=Xx,˙x=X,˙X
205 204 anidms x=Xx,˙x=X,˙X
206 205 breq2d x=X0x,˙x0X,˙X
207 206 48 12 rspcdva φ0X,˙X
208 166 29 207 192 mulge0d φ0X,˙XY,˙Y
209 203 208 eqbrtrd φX,˙0WY,˙XX,˙XY,˙Y
210 16 197 209 pm2.61ne φX,˙YY,˙XX,˙XY,˙Y
211 166 207 resqrtcld φX,˙X
212 211 recnd φX,˙X
213 29 192 resqrtcld φY,˙Y
214 213 recnd φY,˙Y
215 212 214 sqmuld φX,˙XY,˙Y2=X,˙X2Y,˙Y2
216 167 sqsqrtd φX,˙X2=X,˙X
217 30 sqsqrtd φY,˙Y2=Y,˙Y
218 216 217 oveq12d φX,˙X2Y,˙Y2=X,˙XY,˙Y
219 215 218 eqtrd φX,˙XY,˙Y2=X,˙XY,˙Y
220 210 171 219 3brtr4d φX,˙Y2X,˙XY,˙Y2
221 211 213 remulcld φX,˙XY,˙Y
222 22 absge0d φ0X,˙Y
223 166 207 sqrtge0d φ0X,˙X
224 29 192 sqrtge0d φ0Y,˙Y
225 211 213 223 224 mulge0d φ0X,˙XY,˙Y
226 172 221 222 225 le2sqd φX,˙YX,˙XY,˙YX,˙Y2X,˙XY,˙Y2
227 220 226 mpbird φX,˙YX,˙XY,˙Y
228 lmodgrp WLModWGrp
229 51 228 syl φWGrp
230 1 10 2 6 tcphnmval WGrpXVNX=X,˙X
231 229 12 230 syl2anc φNX=X,˙X
232 1 10 2 6 tcphnmval WGrpYVNY=Y,˙Y
233 229 13 232 syl2anc φNY=Y,˙Y
234 231 233 oveq12d φNXNY=X,˙XY,˙Y
235 227 234 breqtrrd φX,˙YNXNY