Metamath Proof Explorer


Theorem isphld

Description: Properties that determine a pre-Hilbert (inner product) space. (Contributed by Mario Carneiro, 18-Nov-2013) (Revised by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses isphld.v φV=BaseW
isphld.a φ+˙=+W
isphld.s φ·˙=W
isphld.i φI=𝑖W
isphld.z φ0˙=0W
isphld.f φF=ScalarW
isphld.k φK=BaseF
isphld.p φ˙=+F
isphld.t φ×˙=F
isphld.c φ˙=*F
isphld.o φO=0F
isphld.l φWLVec
isphld.r φF*-Ring
isphld.cl φxVyVxIyK
isphld.d φqKxVyVzVq·˙x+˙yIz=q×˙xIz˙yIz
isphld.ns φxVxIx=Ox=0˙
isphld.cj φxVyV˙xIy=yIx
Assertion isphld φWPreHil

Proof

Step Hyp Ref Expression
1 isphld.v φV=BaseW
2 isphld.a φ+˙=+W
3 isphld.s φ·˙=W
4 isphld.i φI=𝑖W
5 isphld.z φ0˙=0W
6 isphld.f φF=ScalarW
7 isphld.k φK=BaseF
8 isphld.p φ˙=+F
9 isphld.t φ×˙=F
10 isphld.c φ˙=*F
11 isphld.o φO=0F
12 isphld.l φWLVec
13 isphld.r φF*-Ring
14 isphld.cl φxVyVxIyK
15 isphld.d φqKxVyVzVq·˙x+˙yIz=q×˙xIz˙yIz
16 isphld.ns φxVxIx=Ox=0˙
17 isphld.cj φxVyV˙xIy=yIx
18 6 13 eqeltrrd φScalarW*-Ring
19 oveq1 y=wy𝑖Wx=w𝑖Wx
20 19 cbvmptv yBaseWy𝑖Wx=wBaseWw𝑖Wx
21 14 3expib φxVyVxIyK
22 1 eleq2d φxVxBaseW
23 1 eleq2d φyVyBaseW
24 22 23 anbi12d φxVyVxBaseWyBaseW
25 4 oveqd φxIy=x𝑖Wy
26 6 fveq2d φBaseF=BaseScalarW
27 7 26 eqtrd φK=BaseScalarW
28 25 27 eleq12d φxIyKx𝑖WyBaseScalarW
29 21 24 28 3imtr3d φxBaseWyBaseWx𝑖WyBaseScalarW
30 29 impl φxBaseWyBaseWx𝑖WyBaseScalarW
31 30 an32s φyBaseWxBaseWx𝑖WyBaseScalarW
32 oveq1 w=xw𝑖Wy=x𝑖Wy
33 32 cbvmptv wBaseWw𝑖Wy=xBaseWx𝑖Wy
34 31 33 fmptd φyBaseWwBaseWw𝑖Wy:BaseWBaseScalarW
35 34 ralrimiva φyBaseWwBaseWw𝑖Wy:BaseWBaseScalarW
36 oveq2 y=zw𝑖Wy=w𝑖Wz
37 36 mpteq2dv y=zwBaseWw𝑖Wy=wBaseWw𝑖Wz
38 37 feq1d y=zwBaseWw𝑖Wy:BaseWBaseScalarWwBaseWw𝑖Wz:BaseWBaseScalarW
39 38 rspccva yBaseWwBaseWw𝑖Wy:BaseWBaseScalarWzBaseWwBaseWw𝑖Wz:BaseWBaseScalarW
40 35 39 sylan φzBaseWwBaseWw𝑖Wz:BaseWBaseScalarW
41 eqidd φzBaseWScalarW=ScalarW
42 15 3exp φqKxVyVzVq·˙x+˙yIz=q×˙xIz˙yIz
43 27 eleq2d φqKqBaseScalarW
44 3anrot zVxVyVxVyVzV
45 1 eleq2d φzVzBaseW
46 45 22 23 3anbi123d φzVxVyVzBaseWxBaseWyBaseW
47 44 46 bitr3id φxVyVzVzBaseWxBaseWyBaseW
48 3 oveqd φq·˙x=qWx
49 eqidd φy=y
50 2 48 49 oveq123d φq·˙x+˙y=qWx+Wy
51 eqidd φz=z
52 4 50 51 oveq123d φq·˙x+˙yIz=qWx+Wy𝑖Wz
53 6 fveq2d φ+F=+ScalarW
54 8 53 eqtrd φ˙=+ScalarW
55 6 fveq2d φF=ScalarW
56 9 55 eqtrd φ×˙=ScalarW
57 eqidd φq=q
58 4 oveqd φxIz=x𝑖Wz
59 56 57 58 oveq123d φq×˙xIz=qScalarWx𝑖Wz
60 4 oveqd φyIz=y𝑖Wz
61 54 59 60 oveq123d φq×˙xIz˙yIz=qScalarWx𝑖Wz+ScalarWy𝑖Wz
62 52 61 eqeq12d φq·˙x+˙yIz=q×˙xIz˙yIzqWx+Wy𝑖Wz=qScalarWx𝑖Wz+ScalarWy𝑖Wz
63 47 62 imbi12d φxVyVzVq·˙x+˙yIz=q×˙xIz˙yIzzBaseWxBaseWyBaseWqWx+Wy𝑖Wz=qScalarWx𝑖Wz+ScalarWy𝑖Wz
64 42 43 63 3imtr3d φqBaseScalarWzBaseWxBaseWyBaseWqWx+Wy𝑖Wz=qScalarWx𝑖Wz+ScalarWy𝑖Wz
65 64 imp31 φqBaseScalarWzBaseWxBaseWyBaseWqWx+Wy𝑖Wz=qScalarWx𝑖Wz+ScalarWy𝑖Wz
66 65 3exp2 φqBaseScalarWzBaseWxBaseWyBaseWqWx+Wy𝑖Wz=qScalarWx𝑖Wz+ScalarWy𝑖Wz
67 66 impancom φzBaseWqBaseScalarWxBaseWyBaseWqWx+Wy𝑖Wz=qScalarWx𝑖Wz+ScalarWy𝑖Wz
68 67 3imp2 φzBaseWqBaseScalarWxBaseWyBaseWqWx+Wy𝑖Wz=qScalarWx𝑖Wz+ScalarWy𝑖Wz
69 lveclmod WLVecWLMod
70 12 69 syl φWLMod
71 70 adantr φzBaseWWLMod
72 71 adantr φzBaseWqBaseScalarWxBaseWyBaseWWLMod
73 eqid BaseW=BaseW
74 eqid LSubSpW=LSubSpW
75 73 74 lss1 WLModBaseWLSubSpW
76 72 75 syl φzBaseWqBaseScalarWxBaseWyBaseWBaseWLSubSpW
77 eqid ScalarW=ScalarW
78 eqid BaseScalarW=BaseScalarW
79 eqid +W=+W
80 eqid W=W
81 77 78 79 80 74 lsscl BaseWLSubSpWqBaseScalarWxBaseWyBaseWqWx+WyBaseW
82 76 81 sylancom φzBaseWqBaseScalarWxBaseWyBaseWqWx+WyBaseW
83 oveq1 w=qWx+Wyw𝑖Wz=qWx+Wy𝑖Wz
84 eqid wBaseWw𝑖Wz=wBaseWw𝑖Wz
85 ovex w𝑖WzV
86 83 84 85 fvmpt3i qWx+WyBaseWwBaseWw𝑖WzqWx+Wy=qWx+Wy𝑖Wz
87 82 86 syl φzBaseWqBaseScalarWxBaseWyBaseWwBaseWw𝑖WzqWx+Wy=qWx+Wy𝑖Wz
88 simpr2 φzBaseWqBaseScalarWxBaseWyBaseWxBaseW
89 oveq1 w=xw𝑖Wz=x𝑖Wz
90 89 84 85 fvmpt3i xBaseWwBaseWw𝑖Wzx=x𝑖Wz
91 88 90 syl φzBaseWqBaseScalarWxBaseWyBaseWwBaseWw𝑖Wzx=x𝑖Wz
92 91 oveq2d φzBaseWqBaseScalarWxBaseWyBaseWqScalarWwBaseWw𝑖Wzx=qScalarWx𝑖Wz
93 simpr3 φzBaseWqBaseScalarWxBaseWyBaseWyBaseW
94 oveq1 w=yw𝑖Wz=y𝑖Wz
95 94 84 85 fvmpt3i yBaseWwBaseWw𝑖Wzy=y𝑖Wz
96 93 95 syl φzBaseWqBaseScalarWxBaseWyBaseWwBaseWw𝑖Wzy=y𝑖Wz
97 92 96 oveq12d φzBaseWqBaseScalarWxBaseWyBaseWqScalarWwBaseWw𝑖Wzx+ScalarWwBaseWw𝑖Wzy=qScalarWx𝑖Wz+ScalarWy𝑖Wz
98 68 87 97 3eqtr4d φzBaseWqBaseScalarWxBaseWyBaseWwBaseWw𝑖WzqWx+Wy=qScalarWwBaseWw𝑖Wzx+ScalarWwBaseWw𝑖Wzy
99 98 ralrimivvva φzBaseWqBaseScalarWxBaseWyBaseWwBaseWw𝑖WzqWx+Wy=qScalarWwBaseWw𝑖Wzx+ScalarWwBaseWw𝑖Wzy
100 77 lmodring WLModScalarWRing
101 rlmlmod ScalarWRingringLModScalarWLMod
102 70 100 101 3syl φringLModScalarWLMod
103 102 adantr φzBaseWringLModScalarWLMod
104 rlmbas BaseScalarW=BaseringLModScalarW
105 fvex ScalarWV
106 rlmsca ScalarWVScalarW=ScalarringLModScalarW
107 105 106 ax-mp ScalarW=ScalarringLModScalarW
108 rlmplusg +ScalarW=+ringLModScalarW
109 rlmvsca ScalarW=ringLModScalarW
110 73 104 77 107 78 79 108 80 109 islmhm2 WLModringLModScalarWLModwBaseWw𝑖WzWLMHomringLModScalarWwBaseWw𝑖Wz:BaseWBaseScalarWScalarW=ScalarWqBaseScalarWxBaseWyBaseWwBaseWw𝑖WzqWx+Wy=qScalarWwBaseWw𝑖Wzx+ScalarWwBaseWw𝑖Wzy
111 71 103 110 syl2anc φzBaseWwBaseWw𝑖WzWLMHomringLModScalarWwBaseWw𝑖Wz:BaseWBaseScalarWScalarW=ScalarWqBaseScalarWxBaseWyBaseWwBaseWw𝑖WzqWx+Wy=qScalarWwBaseWw𝑖Wzx+ScalarWwBaseWw𝑖Wzy
112 40 41 99 111 mpbir3and φzBaseWwBaseWw𝑖WzWLMHomringLModScalarW
113 112 ralrimiva φzBaseWwBaseWw𝑖WzWLMHomringLModScalarW
114 oveq2 z=xw𝑖Wz=w𝑖Wx
115 114 mpteq2dv z=xwBaseWw𝑖Wz=wBaseWw𝑖Wx
116 115 eleq1d z=xwBaseWw𝑖WzWLMHomringLModScalarWwBaseWw𝑖WxWLMHomringLModScalarW
117 116 rspccva zBaseWwBaseWw𝑖WzWLMHomringLModScalarWxBaseWwBaseWw𝑖WxWLMHomringLModScalarW
118 113 117 sylan φxBaseWwBaseWw𝑖WxWLMHomringLModScalarW
119 20 118 eqeltrid φxBaseWyBaseWy𝑖WxWLMHomringLModScalarW
120 16 3exp φxVxIx=Ox=0˙
121 4 oveqd φxIx=x𝑖Wx
122 6 fveq2d φ0F=0ScalarW
123 11 122 eqtrd φO=0ScalarW
124 121 123 eqeq12d φxIx=Ox𝑖Wx=0ScalarW
125 5 eqeq2d φx=0˙x=0W
126 124 125 imbi12d φxIx=Ox=0˙x𝑖Wx=0ScalarWx=0W
127 120 22 126 3imtr3d φxBaseWx𝑖Wx=0ScalarWx=0W
128 127 imp φxBaseWx𝑖Wx=0ScalarWx=0W
129 17 3expib φxVyV˙xIy=yIx
130 6 fveq2d φ*F=*ScalarW
131 10 130 eqtrd φ˙=*ScalarW
132 131 25 fveq12d φ˙xIy=x𝑖Wy*ScalarW
133 4 oveqd φyIx=y𝑖Wx
134 132 133 eqeq12d φ˙xIy=yIxx𝑖Wy*ScalarW=y𝑖Wx
135 129 24 134 3imtr3d φxBaseWyBaseWx𝑖Wy*ScalarW=y𝑖Wx
136 135 expdimp φxBaseWyBaseWx𝑖Wy*ScalarW=y𝑖Wx
137 136 ralrimiv φxBaseWyBaseWx𝑖Wy*ScalarW=y𝑖Wx
138 119 128 137 3jca φxBaseWyBaseWy𝑖WxWLMHomringLModScalarWx𝑖Wx=0ScalarWx=0WyBaseWx𝑖Wy*ScalarW=y𝑖Wx
139 138 ralrimiva φxBaseWyBaseWy𝑖WxWLMHomringLModScalarWx𝑖Wx=0ScalarWx=0WyBaseWx𝑖Wy*ScalarW=y𝑖Wx
140 eqid 𝑖W=𝑖W
141 eqid 0W=0W
142 eqid *ScalarW=*ScalarW
143 eqid 0ScalarW=0ScalarW
144 73 77 140 141 142 143 isphl WPreHilWLVecScalarW*-RingxBaseWyBaseWy𝑖WxWLMHomringLModScalarWx𝑖Wx=0ScalarWx=0WyBaseWx𝑖Wy*ScalarW=y𝑖Wx
145 12 18 139 144 syl3anbrc φWPreHil