# 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 ${⊢}{\phi }\to {V}={\mathrm{Base}}_{{W}}$
isphld.a
isphld.s
isphld.i ${⊢}{\phi }\to {I}={\cdot }_{𝑖}\left({W}\right)$
isphld.z
isphld.f ${⊢}{\phi }\to {F}=\mathrm{Scalar}\left({W}\right)$
isphld.k ${⊢}{\phi }\to {K}={\mathrm{Base}}_{{F}}$
isphld.p
isphld.t
isphld.c
isphld.o ${⊢}{\phi }\to {O}={0}_{{F}}$
isphld.l ${⊢}{\phi }\to {W}\in \mathrm{LVec}$
isphld.r ${⊢}{\phi }\to {F}\in \mathrm{*-Ring}$
isphld.cl ${⊢}\left({\phi }\wedge {x}\in {V}\wedge {y}\in {V}\right)\to {x}{I}{y}\in {K}$
isphld.d
isphld.ns
isphld.cj
Assertion isphld ${⊢}{\phi }\to {W}\in \mathrm{PreHil}$

### Proof

Step Hyp Ref Expression
1 isphld.v ${⊢}{\phi }\to {V}={\mathrm{Base}}_{{W}}$
2 isphld.a
3 isphld.s
4 isphld.i ${⊢}{\phi }\to {I}={\cdot }_{𝑖}\left({W}\right)$
5 isphld.z
6 isphld.f ${⊢}{\phi }\to {F}=\mathrm{Scalar}\left({W}\right)$
7 isphld.k ${⊢}{\phi }\to {K}={\mathrm{Base}}_{{F}}$
8 isphld.p
9 isphld.t
10 isphld.c
11 isphld.o ${⊢}{\phi }\to {O}={0}_{{F}}$
12 isphld.l ${⊢}{\phi }\to {W}\in \mathrm{LVec}$
13 isphld.r ${⊢}{\phi }\to {F}\in \mathrm{*-Ring}$
14 isphld.cl ${⊢}\left({\phi }\wedge {x}\in {V}\wedge {y}\in {V}\right)\to {x}{I}{y}\in {K}$
15 isphld.d
16 isphld.ns
17 isphld.cj
18 6 13 eqeltrrd ${⊢}{\phi }\to \mathrm{Scalar}\left({W}\right)\in \mathrm{*-Ring}$
19 oveq1 ${⊢}{y}={w}\to {y}{\cdot }_{𝑖}\left({W}\right){x}={w}{\cdot }_{𝑖}\left({W}\right){x}$
20 19 cbvmptv ${⊢}\left({y}\in {\mathrm{Base}}_{{W}}⟼{y}{\cdot }_{𝑖}\left({W}\right){x}\right)=\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){x}\right)$
21 14 3expib ${⊢}{\phi }\to \left(\left({x}\in {V}\wedge {y}\in {V}\right)\to {x}{I}{y}\in {K}\right)$
22 1 eleq2d ${⊢}{\phi }\to \left({x}\in {V}↔{x}\in {\mathrm{Base}}_{{W}}\right)$
23 1 eleq2d ${⊢}{\phi }\to \left({y}\in {V}↔{y}\in {\mathrm{Base}}_{{W}}\right)$
24 22 23 anbi12d ${⊢}{\phi }\to \left(\left({x}\in {V}\wedge {y}\in {V}\right)↔\left({x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\right)$
25 4 oveqd ${⊢}{\phi }\to {x}{I}{y}={x}{\cdot }_{𝑖}\left({W}\right){y}$
26 6 fveq2d ${⊢}{\phi }\to {\mathrm{Base}}_{{F}}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
27 7 26 eqtrd ${⊢}{\phi }\to {K}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
28 25 27 eleq12d ${⊢}{\phi }\to \left({x}{I}{y}\in {K}↔{x}{\cdot }_{𝑖}\left({W}\right){y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)$
29 21 24 28 3imtr3d ${⊢}{\phi }\to \left(\left({x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\to {x}{\cdot }_{𝑖}\left({W}\right){y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)$
30 29 impl ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{W}}\right)\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\to {x}{\cdot }_{𝑖}\left({W}\right){y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
31 30 an32s ${⊢}\left(\left({\phi }\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\wedge {x}\in {\mathrm{Base}}_{{W}}\right)\to {x}{\cdot }_{𝑖}\left({W}\right){y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
32 oveq1 ${⊢}{w}={x}\to {w}{\cdot }_{𝑖}\left({W}\right){y}={x}{\cdot }_{𝑖}\left({W}\right){y}$
33 32 cbvmptv ${⊢}\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){y}\right)=\left({x}\in {\mathrm{Base}}_{{W}}⟼{x}{\cdot }_{𝑖}\left({W}\right){y}\right)$
34 31 33 fmptd ${⊢}\left({\phi }\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\to \left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){y}\right):{\mathrm{Base}}_{{W}}⟶{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
35 34 ralrimiva ${⊢}{\phi }\to \forall {y}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){y}\right):{\mathrm{Base}}_{{W}}⟶{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
36 oveq2 ${⊢}{y}={z}\to {w}{\cdot }_{𝑖}\left({W}\right){y}={w}{\cdot }_{𝑖}\left({W}\right){z}$
37 36 mpteq2dv ${⊢}{y}={z}\to \left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){y}\right)=\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)$
38 37 feq1d ${⊢}{y}={z}\to \left(\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){y}\right):{\mathrm{Base}}_{{W}}⟶{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}↔\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right):{\mathrm{Base}}_{{W}}⟶{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)$
39 38 rspccva ${⊢}\left(\forall {y}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){y}\right):{\mathrm{Base}}_{{W}}⟶{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\to \left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right):{\mathrm{Base}}_{{W}}⟶{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
40 35 39 sylan ${⊢}\left({\phi }\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\to \left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right):{\mathrm{Base}}_{{W}}⟶{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
41 eqidd ${⊢}\left({\phi }\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\to \mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
42 15 3exp
43 27 eleq2d ${⊢}{\phi }\to \left({q}\in {K}↔{q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)$
44 3anrot ${⊢}\left({z}\in {V}\wedge {x}\in {V}\wedge {y}\in {V}\right)↔\left({x}\in {V}\wedge {y}\in {V}\wedge {z}\in {V}\right)$
45 1 eleq2d ${⊢}{\phi }\to \left({z}\in {V}↔{z}\in {\mathrm{Base}}_{{W}}\right)$
46 45 22 23 3anbi123d ${⊢}{\phi }\to \left(\left({z}\in {V}\wedge {x}\in {V}\wedge {y}\in {V}\right)↔\left({z}\in {\mathrm{Base}}_{{W}}\wedge {x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\right)$
47 44 46 syl5bbr ${⊢}{\phi }\to \left(\left({x}\in {V}\wedge {y}\in {V}\wedge {z}\in {V}\right)↔\left({z}\in {\mathrm{Base}}_{{W}}\wedge {x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\right)$
48 3 oveqd
49 eqidd ${⊢}{\phi }\to {y}={y}$
50 2 48 49 oveq123d
51 eqidd ${⊢}{\phi }\to {z}={z}$
52 4 50 51 oveq123d
53 6 fveq2d ${⊢}{\phi }\to {+}_{{F}}={+}_{\mathrm{Scalar}\left({W}\right)}$
54 8 53 eqtrd
55 6 fveq2d ${⊢}{\phi }\to {\cdot }_{{F}}={\cdot }_{\mathrm{Scalar}\left({W}\right)}$
56 9 55 eqtrd
57 eqidd ${⊢}{\phi }\to {q}={q}$
58 4 oveqd ${⊢}{\phi }\to {x}{I}{z}={x}{\cdot }_{𝑖}\left({W}\right){z}$
59 56 57 58 oveq123d
60 4 oveqd ${⊢}{\phi }\to {y}{I}{z}={y}{\cdot }_{𝑖}\left({W}\right){z}$
61 54 59 60 oveq123d
62 52 61 eqeq12d
63 47 62 imbi12d
64 42 43 63 3imtr3d ${⊢}{\phi }\to \left({q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\to \left(\left({z}\in {\mathrm{Base}}_{{W}}\wedge {x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\to \left(\left({q}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\right){\cdot }_{𝑖}\left({W}\right){z}=\left({q}{\cdot }_{\mathrm{Scalar}\left({W}\right)}\left({x}{\cdot }_{𝑖}\left({W}\right){z}\right)\right){+}_{\mathrm{Scalar}\left({W}\right)}\left({y}{\cdot }_{𝑖}\left({W}\right){z}\right)\right)\right)$
65 64 imp31 ${⊢}\left(\left({\phi }\wedge {q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({z}\in {\mathrm{Base}}_{{W}}\wedge {x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\right)\to \left(\left({q}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\right){\cdot }_{𝑖}\left({W}\right){z}=\left({q}{\cdot }_{\mathrm{Scalar}\left({W}\right)}\left({x}{\cdot }_{𝑖}\left({W}\right){z}\right)\right){+}_{\mathrm{Scalar}\left({W}\right)}\left({y}{\cdot }_{𝑖}\left({W}\right){z}\right)$
66 65 3exp2 ${⊢}\left({\phi }\wedge {q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\to \left({z}\in {\mathrm{Base}}_{{W}}\to \left({x}\in {\mathrm{Base}}_{{W}}\to \left({y}\in {\mathrm{Base}}_{{W}}\to \left(\left({q}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\right){\cdot }_{𝑖}\left({W}\right){z}=\left({q}{\cdot }_{\mathrm{Scalar}\left({W}\right)}\left({x}{\cdot }_{𝑖}\left({W}\right){z}\right)\right){+}_{\mathrm{Scalar}\left({W}\right)}\left({y}{\cdot }_{𝑖}\left({W}\right){z}\right)\right)\right)\right)$
67 66 impancom ${⊢}\left({\phi }\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\to \left({q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\to \left({x}\in {\mathrm{Base}}_{{W}}\to \left({y}\in {\mathrm{Base}}_{{W}}\to \left(\left({q}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\right){\cdot }_{𝑖}\left({W}\right){z}=\left({q}{\cdot }_{\mathrm{Scalar}\left({W}\right)}\left({x}{\cdot }_{𝑖}\left({W}\right){z}\right)\right){+}_{\mathrm{Scalar}\left({W}\right)}\left({y}{\cdot }_{𝑖}\left({W}\right){z}\right)\right)\right)\right)$
68 67 3imp2 ${⊢}\left(\left({\phi }\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\wedge \left({q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\right)\to \left(\left({q}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\right){\cdot }_{𝑖}\left({W}\right){z}=\left({q}{\cdot }_{\mathrm{Scalar}\left({W}\right)}\left({x}{\cdot }_{𝑖}\left({W}\right){z}\right)\right){+}_{\mathrm{Scalar}\left({W}\right)}\left({y}{\cdot }_{𝑖}\left({W}\right){z}\right)$
69 lveclmod ${⊢}{W}\in \mathrm{LVec}\to {W}\in \mathrm{LMod}$
70 12 69 syl ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
71 70 adantr ${⊢}\left({\phi }\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\to {W}\in \mathrm{LMod}$
72 71 adantr ${⊢}\left(\left({\phi }\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\wedge \left({q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\right)\to {W}\in \mathrm{LMod}$
73 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
74 eqid ${⊢}\mathrm{LSubSp}\left({W}\right)=\mathrm{LSubSp}\left({W}\right)$
75 73 74 lss1 ${⊢}{W}\in \mathrm{LMod}\to {\mathrm{Base}}_{{W}}\in \mathrm{LSubSp}\left({W}\right)$
76 72 75 syl ${⊢}\left(\left({\phi }\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\wedge \left({q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\right)\to {\mathrm{Base}}_{{W}}\in \mathrm{LSubSp}\left({W}\right)$
77 eqid ${⊢}\mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
78 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
79 eqid ${⊢}{+}_{{W}}={+}_{{W}}$
80 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
81 77 78 79 80 74 lsscl ${⊢}\left({\mathrm{Base}}_{{W}}\in \mathrm{LSubSp}\left({W}\right)\wedge \left({q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\right)\to \left({q}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\in {\mathrm{Base}}_{{W}}$
82 76 81 sylancom ${⊢}\left(\left({\phi }\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\wedge \left({q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\right)\to \left({q}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\in {\mathrm{Base}}_{{W}}$
83 oveq1 ${⊢}{w}=\left({q}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\to {w}{\cdot }_{𝑖}\left({W}\right){z}=\left(\left({q}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\right){\cdot }_{𝑖}\left({W}\right){z}$
84 eqid ${⊢}\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)=\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)$
85 ovex ${⊢}{w}{\cdot }_{𝑖}\left({W}\right){z}\in \mathrm{V}$
86 83 84 85 fvmpt3i ${⊢}\left({q}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\in {\mathrm{Base}}_{{W}}\to \left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\left(\left({q}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\right)=\left(\left({q}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\right){\cdot }_{𝑖}\left({W}\right){z}$
87 82 86 syl ${⊢}\left(\left({\phi }\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\wedge \left({q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\right)\to \left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\left(\left({q}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\right)=\left(\left({q}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\right){\cdot }_{𝑖}\left({W}\right){z}$
88 simpr2 ${⊢}\left(\left({\phi }\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\wedge \left({q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\right)\to {x}\in {\mathrm{Base}}_{{W}}$
89 oveq1 ${⊢}{w}={x}\to {w}{\cdot }_{𝑖}\left({W}\right){z}={x}{\cdot }_{𝑖}\left({W}\right){z}$
90 89 84 85 fvmpt3i ${⊢}{x}\in {\mathrm{Base}}_{{W}}\to \left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\left({x}\right)={x}{\cdot }_{𝑖}\left({W}\right){z}$
91 88 90 syl ${⊢}\left(\left({\phi }\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\wedge \left({q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\right)\to \left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\left({x}\right)={x}{\cdot }_{𝑖}\left({W}\right){z}$
92 91 oveq2d ${⊢}\left(\left({\phi }\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\wedge \left({q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\right)\to {q}{\cdot }_{\mathrm{Scalar}\left({W}\right)}\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\left({x}\right)={q}{\cdot }_{\mathrm{Scalar}\left({W}\right)}\left({x}{\cdot }_{𝑖}\left({W}\right){z}\right)$
93 simpr3 ${⊢}\left(\left({\phi }\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\wedge \left({q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\right)\to {y}\in {\mathrm{Base}}_{{W}}$
94 oveq1 ${⊢}{w}={y}\to {w}{\cdot }_{𝑖}\left({W}\right){z}={y}{\cdot }_{𝑖}\left({W}\right){z}$
95 94 84 85 fvmpt3i ${⊢}{y}\in {\mathrm{Base}}_{{W}}\to \left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\left({y}\right)={y}{\cdot }_{𝑖}\left({W}\right){z}$
96 93 95 syl ${⊢}\left(\left({\phi }\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\wedge \left({q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\right)\to \left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\left({y}\right)={y}{\cdot }_{𝑖}\left({W}\right){z}$
97 92 96 oveq12d ${⊢}\left(\left({\phi }\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\wedge \left({q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\right)\to \left({q}{\cdot }_{\mathrm{Scalar}\left({W}\right)}\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\left({x}\right)\right){+}_{\mathrm{Scalar}\left({W}\right)}\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\left({y}\right)=\left({q}{\cdot }_{\mathrm{Scalar}\left({W}\right)}\left({x}{\cdot }_{𝑖}\left({W}\right){z}\right)\right){+}_{\mathrm{Scalar}\left({W}\right)}\left({y}{\cdot }_{𝑖}\left({W}\right){z}\right)$
98 68 87 97 3eqtr4d ${⊢}\left(\left({\phi }\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\wedge \left({q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\right)\to \left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\left(\left({q}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\right)=\left({q}{\cdot }_{\mathrm{Scalar}\left({W}\right)}\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\left({x}\right)\right){+}_{\mathrm{Scalar}\left({W}\right)}\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\left({y}\right)$
99 98 ralrimivvva ${⊢}\left({\phi }\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\to \forall {q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\phantom{\rule{.4em}{0ex}}\forall {x}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\left(\left({q}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\right)=\left({q}{\cdot }_{\mathrm{Scalar}\left({W}\right)}\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\left({x}\right)\right){+}_{\mathrm{Scalar}\left({W}\right)}\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\left({y}\right)$
100 77 lmodring ${⊢}{W}\in \mathrm{LMod}\to \mathrm{Scalar}\left({W}\right)\in \mathrm{Ring}$
101 rlmlmod ${⊢}\mathrm{Scalar}\left({W}\right)\in \mathrm{Ring}\to \mathrm{ringLMod}\left(\mathrm{Scalar}\left({W}\right)\right)\in \mathrm{LMod}$
102 70 100 101 3syl ${⊢}{\phi }\to \mathrm{ringLMod}\left(\mathrm{Scalar}\left({W}\right)\right)\in \mathrm{LMod}$
103 102 adantr ${⊢}\left({\phi }\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\to \mathrm{ringLMod}\left(\mathrm{Scalar}\left({W}\right)\right)\in \mathrm{LMod}$
104 rlmbas ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}={\mathrm{Base}}_{\mathrm{ringLMod}\left(\mathrm{Scalar}\left({W}\right)\right)}$
105 fvex ${⊢}\mathrm{Scalar}\left({W}\right)\in \mathrm{V}$
106 rlmsca ${⊢}\mathrm{Scalar}\left({W}\right)\in \mathrm{V}\to \mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left(\mathrm{Scalar}\left({W}\right)\right)\right)$
107 105 106 ax-mp ${⊢}\mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left(\mathrm{Scalar}\left({W}\right)\right)\right)$
108 rlmplusg ${⊢}{+}_{\mathrm{Scalar}\left({W}\right)}={+}_{\mathrm{ringLMod}\left(\mathrm{Scalar}\left({W}\right)\right)}$
109 rlmvsca ${⊢}{\cdot }_{\mathrm{Scalar}\left({W}\right)}={\cdot }_{\mathrm{ringLMod}\left(\mathrm{Scalar}\left({W}\right)\right)}$
110 73 104 77 107 78 79 108 80 109 islmhm2 ${⊢}\left({W}\in \mathrm{LMod}\wedge \mathrm{ringLMod}\left(\mathrm{Scalar}\left({W}\right)\right)\in \mathrm{LMod}\right)\to \left(\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\in \left({W}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({W}\right)\right)\right)↔\left(\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right):{\mathrm{Base}}_{{W}}⟶{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge \mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)\wedge \forall {q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\phantom{\rule{.4em}{0ex}}\forall {x}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\left(\left({q}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\right)=\left({q}{\cdot }_{\mathrm{Scalar}\left({W}\right)}\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\left({x}\right)\right){+}_{\mathrm{Scalar}\left({W}\right)}\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\left({y}\right)\right)\right)$
111 71 103 110 syl2anc ${⊢}\left({\phi }\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\to \left(\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\in \left({W}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({W}\right)\right)\right)↔\left(\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right):{\mathrm{Base}}_{{W}}⟶{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge \mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)\wedge \forall {q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\phantom{\rule{.4em}{0ex}}\forall {x}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\left(\left({q}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\right)=\left({q}{\cdot }_{\mathrm{Scalar}\left({W}\right)}\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\left({x}\right)\right){+}_{\mathrm{Scalar}\left({W}\right)}\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\left({y}\right)\right)\right)$
112 40 41 99 111 mpbir3and ${⊢}\left({\phi }\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\to \left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\in \left({W}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({W}\right)\right)\right)$
113 112 ralrimiva ${⊢}{\phi }\to \forall {z}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\in \left({W}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({W}\right)\right)\right)$
114 oveq2 ${⊢}{z}={x}\to {w}{\cdot }_{𝑖}\left({W}\right){z}={w}{\cdot }_{𝑖}\left({W}\right){x}$
115 114 mpteq2dv ${⊢}{z}={x}\to \left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)=\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){x}\right)$
116 115 eleq1d ${⊢}{z}={x}\to \left(\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\in \left({W}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({W}\right)\right)\right)↔\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){x}\right)\in \left({W}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({W}\right)\right)\right)\right)$
117 116 rspccva ${⊢}\left(\forall {z}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}\left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){z}\right)\in \left({W}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({W}\right)\right)\right)\wedge {x}\in {\mathrm{Base}}_{{W}}\right)\to \left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){x}\right)\in \left({W}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({W}\right)\right)\right)$
118 113 117 sylan ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{W}}\right)\to \left({w}\in {\mathrm{Base}}_{{W}}⟼{w}{\cdot }_{𝑖}\left({W}\right){x}\right)\in \left({W}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({W}\right)\right)\right)$
119 20 118 eqeltrid ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{W}}\right)\to \left({y}\in {\mathrm{Base}}_{{W}}⟼{y}{\cdot }_{𝑖}\left({W}\right){x}\right)\in \left({W}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({W}\right)\right)\right)$
120 16 3exp
121 4 oveqd ${⊢}{\phi }\to {x}{I}{x}={x}{\cdot }_{𝑖}\left({W}\right){x}$
122 6 fveq2d ${⊢}{\phi }\to {0}_{{F}}={0}_{\mathrm{Scalar}\left({W}\right)}$
123 11 122 eqtrd ${⊢}{\phi }\to {O}={0}_{\mathrm{Scalar}\left({W}\right)}$
124 121 123 eqeq12d ${⊢}{\phi }\to \left({x}{I}{x}={O}↔{x}{\cdot }_{𝑖}\left({W}\right){x}={0}_{\mathrm{Scalar}\left({W}\right)}\right)$
125 5 eqeq2d
126 124 125 imbi12d
127 120 22 126 3imtr3d ${⊢}{\phi }\to \left({x}\in {\mathrm{Base}}_{{W}}\to \left({x}{\cdot }_{𝑖}\left({W}\right){x}={0}_{\mathrm{Scalar}\left({W}\right)}\to {x}={0}_{{W}}\right)\right)$
128 127 imp ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{W}}\right)\to \left({x}{\cdot }_{𝑖}\left({W}\right){x}={0}_{\mathrm{Scalar}\left({W}\right)}\to {x}={0}_{{W}}\right)$
129 17 3expib
130 6 fveq2d ${⊢}{\phi }\to {*}_{{F}}={*}_{\mathrm{Scalar}\left({W}\right)}$
131 10 130 eqtrd
132 131 25 fveq12d
133 4 oveqd ${⊢}{\phi }\to {y}{I}{x}={y}{\cdot }_{𝑖}\left({W}\right){x}$
134 132 133 eqeq12d
135 129 24 134 3imtr3d ${⊢}{\phi }\to \left(\left({x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\to {\left({x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{{*}_{\mathrm{Scalar}\left({W}\right)}}={y}{\cdot }_{𝑖}\left({W}\right){x}\right)$
136 135 expdimp ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{W}}\right)\to \left({y}\in {\mathrm{Base}}_{{W}}\to {\left({x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{{*}_{\mathrm{Scalar}\left({W}\right)}}={y}{\cdot }_{𝑖}\left({W}\right){x}\right)$
137 136 ralrimiv ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{W}}\right)\to \forall {y}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}{\left({x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{{*}_{\mathrm{Scalar}\left({W}\right)}}={y}{\cdot }_{𝑖}\left({W}\right){x}$
138 119 128 137 3jca ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{W}}\right)\to \left(\left({y}\in {\mathrm{Base}}_{{W}}⟼{y}{\cdot }_{𝑖}\left({W}\right){x}\right)\in \left({W}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({W}\right)\right)\right)\wedge \left({x}{\cdot }_{𝑖}\left({W}\right){x}={0}_{\mathrm{Scalar}\left({W}\right)}\to {x}={0}_{{W}}\right)\wedge \forall {y}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}{\left({x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{{*}_{\mathrm{Scalar}\left({W}\right)}}={y}{\cdot }_{𝑖}\left({W}\right){x}\right)$
139 138 ralrimiva ${⊢}{\phi }\to \forall {x}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}\left(\left({y}\in {\mathrm{Base}}_{{W}}⟼{y}{\cdot }_{𝑖}\left({W}\right){x}\right)\in \left({W}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({W}\right)\right)\right)\wedge \left({x}{\cdot }_{𝑖}\left({W}\right){x}={0}_{\mathrm{Scalar}\left({W}\right)}\to {x}={0}_{{W}}\right)\wedge \forall {y}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}{\left({x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{{*}_{\mathrm{Scalar}\left({W}\right)}}={y}{\cdot }_{𝑖}\left({W}\right){x}\right)$
140 eqid ${⊢}{\cdot }_{𝑖}\left({W}\right)={\cdot }_{𝑖}\left({W}\right)$
141 eqid ${⊢}{0}_{{W}}={0}_{{W}}$
142 eqid ${⊢}{*}_{\mathrm{Scalar}\left({W}\right)}={*}_{\mathrm{Scalar}\left({W}\right)}$
143 eqid ${⊢}{0}_{\mathrm{Scalar}\left({W}\right)}={0}_{\mathrm{Scalar}\left({W}\right)}$
144 73 77 140 141 142 143 isphl ${⊢}{W}\in \mathrm{PreHil}↔\left({W}\in \mathrm{LVec}\wedge \mathrm{Scalar}\left({W}\right)\in \mathrm{*-Ring}\wedge \forall {x}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}\left(\left({y}\in {\mathrm{Base}}_{{W}}⟼{y}{\cdot }_{𝑖}\left({W}\right){x}\right)\in \left({W}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({W}\right)\right)\right)\wedge \left({x}{\cdot }_{𝑖}\left({W}\right){x}={0}_{\mathrm{Scalar}\left({W}\right)}\to {x}={0}_{{W}}\right)\wedge \forall {y}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}{\left({x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{{*}_{\mathrm{Scalar}\left({W}\right)}}={y}{\cdot }_{𝑖}\left({W}\right){x}\right)\right)$
145 12 18 139 144 syl3anbrc ${⊢}{\phi }\to {W}\in \mathrm{PreHil}$