Metamath Proof Explorer


Theorem frlmphl

Description: Conditions for a free module to be a pre-Hilbert space. (Contributed by Thierry Arnoux, 21-Jun-2019) (Proof shortened by AV, 21-Jul-2019)

Ref Expression
Hypotheses frlmphl.y Y = R freeLMod I
frlmphl.b B = Base R
frlmphl.t · ˙ = R
frlmphl.v V = Base Y
frlmphl.j , ˙ = 𝑖 Y
frlmphl.o O = 0 Y
frlmphl.0 0 ˙ = 0 R
frlmphl.s ˙ = * R
frlmphl.f φ R Field
frlmphl.m φ g V g , ˙ g = 0 ˙ g = O
frlmphl.u φ x B ˙ x = x
frlmphl.i φ I W
Assertion frlmphl φ Y PreHil

Proof

Step Hyp Ref Expression
1 frlmphl.y Y = R freeLMod I
2 frlmphl.b B = Base R
3 frlmphl.t · ˙ = R
4 frlmphl.v V = Base Y
5 frlmphl.j , ˙ = 𝑖 Y
6 frlmphl.o O = 0 Y
7 frlmphl.0 0 ˙ = 0 R
8 frlmphl.s ˙ = * R
9 frlmphl.f φ R Field
10 frlmphl.m φ g V g , ˙ g = 0 ˙ g = O
11 frlmphl.u φ x B ˙ x = x
12 frlmphl.i φ I W
13 4 a1i φ V = Base Y
14 eqidd φ + Y = + Y
15 eqidd φ Y = Y
16 5 a1i φ , ˙ = 𝑖 Y
17 6 a1i φ O = 0 Y
18 isfld R Field R DivRing R CRing
19 9 18 sylib φ R DivRing R CRing
20 19 simpld φ R DivRing
21 1 frlmsca R DivRing I W R = Scalar Y
22 20 12 21 syl2anc φ R = Scalar Y
23 2 a1i φ B = Base R
24 eqidd φ + R = + R
25 3 a1i φ · ˙ = R
26 8 a1i φ ˙ = * R
27 7 a1i φ 0 ˙ = 0 R
28 drngring R DivRing R Ring
29 20 28 syl φ R Ring
30 1 frlmlmod R Ring I W Y LMod
31 29 12 30 syl2anc φ Y LMod
32 22 20 eqeltrrd φ Scalar Y DivRing
33 eqid Scalar Y = Scalar Y
34 33 islvec Y LVec Y LMod Scalar Y DivRing
35 31 32 34 sylanbrc φ Y LVec
36 19 simprd φ R CRing
37 2 8 36 11 idsrngd φ R *-Ring
38 12 3ad2ant1 φ g V h V I W
39 29 3ad2ant1 φ g V h V R Ring
40 simp2 φ g V h V g V
41 simp3 φ g V h V h V
42 1 2 3 4 5 frlmipval I W R Ring g V h V g , ˙ h = R g · ˙ f h
43 38 39 40 41 42 syl22anc φ g V h V g , ˙ h = R g · ˙ f h
44 1 2 4 frlmbasmap I W g V g B I
45 38 40 44 syl2anc φ g V h V g B I
46 elmapi g B I g : I B
47 45 46 syl φ g V h V g : I B
48 47 ffnd φ g V h V g Fn I
49 1 2 4 frlmbasmap I W h V h B I
50 38 41 49 syl2anc φ g V h V h B I
51 elmapi h B I h : I B
52 50 51 syl φ g V h V h : I B
53 52 ffnd φ g V h V h Fn I
54 inidm I I = I
55 eqidd φ g V h V x I g x = g x
56 eqidd φ g V h V x I h x = h x
57 48 53 38 38 54 55 56 offval φ g V h V g · ˙ f h = x I g x · ˙ h x
58 57 oveq2d φ g V h V R g · ˙ f h = R x I g x · ˙ h x
59 43 58 eqtrd φ g V h V g , ˙ h = R x I g x · ˙ h x
60 ringcmn R Ring R CMnd
61 29 60 syl φ R CMnd
62 61 3ad2ant1 φ g V h V R CMnd
63 39 adantr φ g V h V x I R Ring
64 47 ffvelrnda φ g V h V x I g x B
65 52 ffvelrnda φ g V h V x I h x B
66 2 3 ringcl R Ring g x B h x B g x · ˙ h x B
67 63 64 65 66 syl3anc φ g V h V x I g x · ˙ h x B
68 67 fmpttd φ g V h V x I g x · ˙ h x : I B
69 1 2 3 4 5 6 7 8 9 10 11 12 frlmphllem φ g V h V finSupp 0 ˙ x I g x · ˙ h x
70 2 7 62 38 68 69 gsumcl φ g V h V R x I g x · ˙ h x B
71 59 70 eqeltrd φ g V h V g , ˙ h B
72 eqid + R = + R
73 61 3ad2ant1 φ k B g V h V i V R CMnd
74 12 3ad2ant1 φ k B g V h V i V I W
75 29 3ad2ant1 φ k B g V h V i V R Ring
76 75 adantr φ k B g V h V i V x I R Ring
77 simp2 φ k B g V h V i V k B
78 77 adantr φ k B g V h V i V x I k B
79 simp31 φ k B g V h V i V g V
80 74 79 44 syl2anc φ k B g V h V i V g B I
81 80 46 syl φ k B g V h V i V g : I B
82 81 ffvelrnda φ k B g V h V i V x I g x B
83 simp33 φ k B g V h V i V i V
84 1 2 4 frlmbasmap I W i V i B I
85 74 83 84 syl2anc φ k B g V h V i V i B I
86 elmapi i B I i : I B
87 85 86 syl φ k B g V h V i V i : I B
88 87 ffvelrnda φ k B g V h V i V x I i x B
89 2 3 ringcl R Ring g x B i x B g x · ˙ i x B
90 76 82 88 89 syl3anc φ k B g V h V i V x I g x · ˙ i x B
91 2 3 ringcl R Ring k B g x · ˙ i x B k · ˙ g x · ˙ i x B
92 76 78 90 91 syl3anc φ k B g V h V i V x I k · ˙ g x · ˙ i x B
93 simp32 φ k B g V h V i V h V
94 74 93 49 syl2anc φ k B g V h V i V h B I
95 94 51 syl φ k B g V h V i V h : I B
96 95 ffvelrnda φ k B g V h V i V x I h x B
97 2 3 ringcl R Ring h x B i x B h x · ˙ i x B
98 76 96 88 97 syl3anc φ k B g V h V i V x I h x · ˙ i x B
99 eqidd φ k B g V h V i V x I k · ˙ g x · ˙ i x = x I k · ˙ g x · ˙ i x
100 eqidd φ k B g V h V i V x I h x · ˙ i x = x I h x · ˙ i x
101 fveq2 x = y g x = g y
102 101 oveq2d x = y k · ˙ g x = k · ˙ g y
103 102 cbvmptv x I k · ˙ g x = y I k · ˙ g y
104 103 oveq1i x I k · ˙ g x · ˙ f i = y I k · ˙ g y · ˙ f i
105 2 3 ringcl R Ring k B g x B k · ˙ g x B
106 76 78 82 105 syl3anc φ k B g V h V i V x I k · ˙ g x B
107 106 fmpttd φ k B g V h V i V x I k · ˙ g x : I B
108 107 ffnd φ k B g V h V i V x I k · ˙ g x Fn I
109 103 fneq1i x I k · ˙ g x Fn I y I k · ˙ g y Fn I
110 108 109 sylib φ k B g V h V i V y I k · ˙ g y Fn I
111 87 ffnd φ k B g V h V i V i Fn I
112 eqidd φ k B g V h V i V x I y I k · ˙ g y = y I k · ˙ g y
113 simpr φ k B g V h V i V x I y = x y = x
114 113 fveq2d φ k B g V h V i V x I y = x g y = g x
115 114 oveq2d φ k B g V h V i V x I y = x k · ˙ g y = k · ˙ g x
116 simpr φ k B g V h V i V x I x I
117 ovexd φ k B g V h V i V x I k · ˙ g x V
118 112 115 116 117 fvmptd φ k B g V h V i V x I y I k · ˙ g y x = k · ˙ g x
119 eqidd φ k B g V h V i V x I i x = i x
120 110 111 74 74 54 118 119 offval φ k B g V h V i V y I k · ˙ g y · ˙ f i = x I k · ˙ g x · ˙ i x
121 2 3 ringass R Ring k B g x B i x B k · ˙ g x · ˙ i x = k · ˙ g x · ˙ i x
122 76 78 82 88 121 syl13anc φ k B g V h V i V x I k · ˙ g x · ˙ i x = k · ˙ g x · ˙ i x
123 122 mpteq2dva φ k B g V h V i V x I k · ˙ g x · ˙ i x = x I k · ˙ g x · ˙ i x
124 120 123 eqtrd φ k B g V h V i V y I k · ˙ g y · ˙ f i = x I k · ˙ g x · ˙ i x
125 104 124 syl5eq φ k B g V h V i V x I k · ˙ g x · ˙ f i = x I k · ˙ g x · ˙ i x
126 ovexd φ k B g V h V i V x I k · ˙ g x · ˙ f i V
127 funmpt Fun z I x I k · ˙ g x z · ˙ i z
128 eqidd φ k B g V h V i V z I x I k · ˙ g x z = x I k · ˙ g x z
129 eqidd φ k B g V h V i V z I i z = i z
130 108 111 74 74 54 128 129 offval φ k B g V h V i V x I k · ˙ g x · ˙ f i = z I x I k · ˙ g x z · ˙ i z
131 130 funeqd φ k B g V h V i V Fun x I k · ˙ g x · ˙ f i Fun z I x I k · ˙ g x z · ˙ i z
132 127 131 mpbiri φ k B g V h V i V Fun x I k · ˙ g x · ˙ f i
133 simp3 g V h V i V i V
134 12 133 anim12i φ g V h V i V I W i V
135 134 3adant2 φ k B g V h V i V I W i V
136 1 7 4 frlmbasfsupp I W i V finSupp 0 ˙ i
137 135 136 syl φ k B g V h V i V finSupp 0 ˙ i
138 2 7 ring0cl R Ring 0 ˙ B
139 75 138 syl φ k B g V h V i V 0 ˙ B
140 2 3 7 ringrz R Ring y B y · ˙ 0 ˙ = 0 ˙
141 75 140 sylan φ k B g V h V i V y B y · ˙ 0 ˙ = 0 ˙
142 74 139 107 87 141 suppofss2d φ k B g V h V i V x I k · ˙ g x · ˙ f i supp 0 ˙ i supp 0 ˙
143 fsuppsssupp x I k · ˙ g x · ˙ f i V Fun x I k · ˙ g x · ˙ f i finSupp 0 ˙ i x I k · ˙ g x · ˙ f i supp 0 ˙ i supp 0 ˙ finSupp 0 ˙ x I k · ˙ g x · ˙ f i
144 126 132 137 142 143 syl22anc φ k B g V h V i V finSupp 0 ˙ x I k · ˙ g x · ˙ f i
145 125 144 eqbrtrrd φ k B g V h V i V finSupp 0 ˙ x I k · ˙ g x · ˙ i x
146 simp1 φ k B g V h V i V φ
147 eleq1w g = h g V h V
148 id g = h g = h
149 148 148 oveq12d g = h g , ˙ g = h , ˙ h
150 149 eqeq1d g = h g , ˙ g = 0 ˙ h , ˙ h = 0 ˙
151 147 150 3anbi23d g = h φ g V g , ˙ g = 0 ˙ φ h V h , ˙ h = 0 ˙
152 eqeq1 g = h g = O h = O
153 151 152 imbi12d g = h φ g V g , ˙ g = 0 ˙ g = O φ h V h , ˙ h = 0 ˙ h = O
154 153 10 chvarvv φ h V h , ˙ h = 0 ˙ h = O
155 1 2 3 4 5 6 7 8 9 154 11 12 frlmphllem φ h V i V finSupp 0 ˙ x I h x · ˙ i x
156 146 93 83 155 syl3anc φ k B g V h V i V finSupp 0 ˙ x I h x · ˙ i x
157 2 7 72 73 74 92 98 99 100 145 156 gsummptfsadd φ k B g V h V i V R x I k · ˙ g x · ˙ i x + R h x · ˙ i x = R x I k · ˙ g x · ˙ i x + R R x I h x · ˙ i x
158 1 2 3 frlmip I W R DivRing g B I , h B I R x I g x · ˙ h x = 𝑖 Y
159 12 20 158 syl2anc φ g B I , h B I R x I g x · ˙ h x = 𝑖 Y
160 5 159 eqtr4id φ , ˙ = g B I , h B I R x I g x · ˙ h x
161 fveq1 e = g e x = g x
162 161 oveq1d e = g e x · ˙ f x = g x · ˙ f x
163 162 mpteq2dv e = g x I e x · ˙ f x = x I g x · ˙ f x
164 163 oveq2d e = g R x I e x · ˙ f x = R x I g x · ˙ f x
165 fveq1 f = h f x = h x
166 165 oveq2d f = h g x · ˙ f x = g x · ˙ h x
167 166 mpteq2dv f = h x I g x · ˙ f x = x I g x · ˙ h x
168 167 oveq2d f = h R x I g x · ˙ f x = R x I g x · ˙ h x
169 164 168 cbvmpov e B I , f B I R x I e x · ˙ f x = g B I , h B I R x I g x · ˙ h x
170 160 169 eqtr4di φ , ˙ = e B I , f B I R x I e x · ˙ f x
171 170 3ad2ant1 φ k B g V h V i V , ˙ = e B I , f B I R x I e x · ˙ f x
172 simprl φ k B g V h V i V e = k Y g + Y h f = i e = k Y g + Y h
173 172 fveq1d φ k B g V h V i V e = k Y g + Y h f = i e x = k Y g + Y h x
174 simprr φ k B g V h V i V e = k Y g + Y h f = i f = i
175 174 fveq1d φ k B g V h V i V e = k Y g + Y h f = i f x = i x
176 173 175 oveq12d φ k B g V h V i V e = k Y g + Y h f = i e x · ˙ f x = k Y g + Y h x · ˙ i x
177 176 mpteq2dv φ k B g V h V i V e = k Y g + Y h f = i x I e x · ˙ f x = x I k Y g + Y h x · ˙ i x
178 177 oveq2d φ k B g V h V i V e = k Y g + Y h f = i R x I e x · ˙ f x = R x I k Y g + Y h x · ˙ i x
179 31 3ad2ant1 φ k B g V h V i V Y LMod
180 22 3ad2ant1 φ k B g V h V i V R = Scalar Y
181 180 fveq2d φ k B g V h V i V Base R = Base Scalar Y
182 2 181 syl5eq φ k B g V h V i V B = Base Scalar Y
183 77 182 eleqtrd φ k B g V h V i V k Base Scalar Y
184 eqid Y = Y
185 eqid Base Scalar Y = Base Scalar Y
186 4 33 184 185 lmodvscl Y LMod k Base Scalar Y g V k Y g V
187 179 183 79 186 syl3anc φ k B g V h V i V k Y g V
188 eqid + Y = + Y
189 4 188 lmodvacl Y LMod k Y g V h V k Y g + Y h V
190 179 187 93 189 syl3anc φ k B g V h V i V k Y g + Y h V
191 1 2 4 frlmbasmap I W k Y g + Y h V k Y g + Y h B I
192 74 190 191 syl2anc φ k B g V h V i V k Y g + Y h B I
193 ovexd φ k B g V h V i V R x I k Y g + Y h x · ˙ i x V
194 171 178 192 85 193 ovmpod φ k B g V h V i V k Y g + Y h , ˙ i = R x I k Y g + Y h x · ˙ i x
195 1 4 75 74 187 93 72 188 frlmplusgval φ k B g V h V i V k Y g + Y h = k Y g + R f h
196 1 2 4 frlmbasmap I W k Y g V k Y g B I
197 74 187 196 syl2anc φ k B g V h V i V k Y g B I
198 elmapi k Y g B I k Y g : I B
199 ffn k Y g : I B k Y g Fn I
200 197 198 199 3syl φ k B g V h V i V k Y g Fn I
201 95 ffnd φ k B g V h V i V h Fn I
202 74 adantr φ k B g V h V i V x I I W
203 79 adantr φ k B g V h V i V x I g V
204 1 4 2 202 78 203 116 184 3 frlmvscaval φ k B g V h V i V x I k Y g x = k · ˙ g x
205 eqidd φ k B g V h V i V x I h x = h x
206 200 201 74 74 54 204 205 offval φ k B g V h V i V k Y g + R f h = x I k · ˙ g x + R h x
207 195 206 eqtrd φ k B g V h V i V k Y g + Y h = x I k · ˙ g x + R h x
208 ovexd φ k B g V h V i V x I k · ˙ g x + R h x V
209 207 208 fvmpt2d φ k B g V h V i V x I k Y g + Y h x = k · ˙ g x + R h x
210 209 oveq1d φ k B g V h V i V x I k Y g + Y h x · ˙ i x = k · ˙ g x + R h x · ˙ i x
211 2 72 3 ringdir R Ring k · ˙ g x B h x B i x B k · ˙ g x + R h x · ˙ i x = k · ˙ g x · ˙ i x + R h x · ˙ i x
212 76 106 96 88 211 syl13anc φ k B g V h V i V x I k · ˙ g x + R h x · ˙ i x = k · ˙ g x · ˙ i x + R h x · ˙ i x
213 122 oveq1d φ k B g V h V i V x I k · ˙ g x · ˙ i x + R h x · ˙ i x = k · ˙ g x · ˙ i x + R h x · ˙ i x
214 210 212 213 3eqtrd φ k B g V h V i V x I k Y g + Y h x · ˙ i x = k · ˙ g x · ˙ i x + R h x · ˙ i x
215 214 mpteq2dva φ k B g V h V i V x I k Y g + Y h x · ˙ i x = x I k · ˙ g x · ˙ i x + R h x · ˙ i x
216 215 oveq2d φ k B g V h V i V R x I k Y g + Y h x · ˙ i x = R x I k · ˙ g x · ˙ i x + R h x · ˙ i x
217 194 216 eqtrd φ k B g V h V i V k Y g + Y h , ˙ i = R x I k · ˙ g x · ˙ i x + R h x · ˙ i x
218 simprl φ k B g V h V i V e = g f = i e = g
219 218 fveq1d φ k B g V h V i V e = g f = i e x = g x
220 simprr φ k B g V h V i V e = g f = i f = i
221 220 fveq1d φ k B g V h V i V e = g f = i f x = i x
222 219 221 oveq12d φ k B g V h V i V e = g f = i e x · ˙ f x = g x · ˙ i x
223 222 mpteq2dv φ k B g V h V i V e = g f = i x I e x · ˙ f x = x I g x · ˙ i x
224 223 oveq2d φ k B g V h V i V e = g f = i R x I e x · ˙ f x = R x I g x · ˙ i x
225 ovexd φ k B g V h V i V R x I g x · ˙ i x V
226 171 224 80 85 225 ovmpod φ k B g V h V i V g , ˙ i = R x I g x · ˙ i x
227 226 oveq2d φ k B g V h V i V k · ˙ g , ˙ i = k · ˙ R x I g x · ˙ i x
228 1 2 3 4 5 6 7 8 9 10 11 12 frlmphllem φ g V i V finSupp 0 ˙ x I g x · ˙ i x
229 146 79 83 228 syl3anc φ k B g V h V i V finSupp 0 ˙ x I g x · ˙ i x
230 2 7 72 3 75 74 77 90 229 gsummulc2 φ k B g V h V i V R x I k · ˙ g x · ˙ i x = k · ˙ R x I g x · ˙ i x
231 227 230 eqtr4d φ k B g V h V i V k · ˙ g , ˙ i = R x I k · ˙ g x · ˙ i x
232 simprl φ k B g V h V i V e = h f = i e = h
233 232 fveq1d φ k B g V h V i V e = h f = i e x = h x
234 simprr φ k B g V h V i V e = h f = i f = i
235 234 fveq1d φ k B g V h V i V e = h f = i f x = i x
236 233 235 oveq12d φ k B g V h V i V e = h f = i e x · ˙ f x = h x · ˙ i x
237 236 mpteq2dv φ k B g V h V i V e = h f = i x I e x · ˙ f x = x I h x · ˙ i x
238 237 oveq2d φ k B g V h V i V e = h f = i R x I e x · ˙ f x = R x I h x · ˙ i x
239 ovexd φ k B g V h V i V R x I h x · ˙ i x V
240 171 238 94 85 239 ovmpod φ k B g V h V i V h , ˙ i = R x I h x · ˙ i x
241 231 240 oveq12d φ k B g V h V i V k · ˙ g , ˙ i + R h , ˙ i = R x I k · ˙ g x · ˙ i x + R R x I h x · ˙ i x
242 157 217 241 3eqtr4d φ k B g V h V i V k Y g + Y h , ˙ i = k · ˙ g , ˙ i + R h , ˙ i
243 36 3ad2ant1 φ g V h V R CRing
244 243 adantr φ g V h V x I R CRing
245 2 3 crngcom R CRing h x B g x B h x · ˙ g x = g x · ˙ h x
246 244 65 64 245 syl3anc φ g V h V x I h x · ˙ g x = g x · ˙ h x
247 246 mpteq2dva φ g V h V x I h x · ˙ g x = x I g x · ˙ h x
248 247 oveq2d φ g V h V R x I h x · ˙ g x = R x I g x · ˙ h x
249 170 3ad2ant1 φ g V h V , ˙ = e B I , f B I R x I e x · ˙ f x
250 simprl φ g V h V e = h f = g e = h
251 250 fveq1d φ g V h V e = h f = g e x = h x
252 simprr φ g V h V e = h f = g f = g
253 252 fveq1d φ g V h V e = h f = g f x = g x
254 251 253 oveq12d φ g V h V e = h f = g e x · ˙ f x = h x · ˙ g x
255 254 mpteq2dv φ g V h V e = h f = g x I e x · ˙ f x = x I h x · ˙ g x
256 255 oveq2d φ g V h V e = h f = g R x I e x · ˙ f x = R x I h x · ˙ g x
257 ovexd φ g V h V R x I h x · ˙ g x V
258 249 256 50 45 257 ovmpod φ g V h V h , ˙ g = R x I h x · ˙ g x
259 fveq2 x = g , ˙ h ˙ x = ˙ g , ˙ h
260 id x = g , ˙ h x = g , ˙ h
261 259 260 eqeq12d x = g , ˙ h ˙ x = x ˙ g , ˙ h = g , ˙ h
262 11 ralrimiva φ x B ˙ x = x
263 262 3ad2ant1 φ g V h V x B ˙ x = x
264 261 263 71 rspcdva φ g V h V ˙ g , ˙ h = g , ˙ h
265 264 59 eqtrd φ g V h V ˙ g , ˙ h = R x I g x · ˙ h x
266 248 258 265 3eqtr4rd φ g V h V ˙ g , ˙ h = h , ˙ g
267 13 14 15 16 17 22 23 24 25 26 27 35 37 71 242 10 266 isphld φ Y PreHil