Metamath Proof Explorer

Theorem phlssphl

Description: A subspace of an inner product space (pre-Hilbert space) is an inner product space. (Contributed by AV, 25-Sep-2022)

Ref Expression
Hypotheses phlssphl.x ${⊢}{X}={W}{↾}_{𝑠}{U}$
phlssphl.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
Assertion phlssphl ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {X}\in \mathrm{PreHil}$

Proof

Step Hyp Ref Expression
1 phlssphl.x ${⊢}{X}={W}{↾}_{𝑠}{U}$
2 phlssphl.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
3 eqidd ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {\mathrm{Base}}_{{X}}={\mathrm{Base}}_{{X}}$
4 eqidd ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {+}_{{X}}={+}_{{X}}$
5 eqidd ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {\cdot }_{{X}}={\cdot }_{{X}}$
6 eqidd ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {\cdot }_{𝑖}\left({X}\right)={\cdot }_{𝑖}\left({X}\right)$
7 phllmod ${⊢}{W}\in \mathrm{PreHil}\to {W}\in \mathrm{LMod}$
8 eqid ${⊢}{0}_{{W}}={0}_{{W}}$
9 eqid ${⊢}{0}_{{X}}={0}_{{X}}$
10 1 8 9 2 lss0v ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {0}_{{X}}={0}_{{W}}$
11 7 10 sylan ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {0}_{{X}}={0}_{{W}}$
12 11 eqcomd ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {0}_{{W}}={0}_{{X}}$
13 eqidd ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to \mathrm{Scalar}\left({X}\right)=\mathrm{Scalar}\left({X}\right)$
14 eqidd ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}$
15 eqidd ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {+}_{\mathrm{Scalar}\left({X}\right)}={+}_{\mathrm{Scalar}\left({X}\right)}$
16 eqidd ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {\cdot }_{\mathrm{Scalar}\left({X}\right)}={\cdot }_{\mathrm{Scalar}\left({X}\right)}$
17 eqidd ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {*}_{\mathrm{Scalar}\left({X}\right)}={*}_{\mathrm{Scalar}\left({X}\right)}$
18 eqidd ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {0}_{\mathrm{Scalar}\left({X}\right)}={0}_{\mathrm{Scalar}\left({X}\right)}$
19 phllvec ${⊢}{W}\in \mathrm{PreHil}\to {W}\in \mathrm{LVec}$
20 1 2 lsslvec ${⊢}\left({W}\in \mathrm{LVec}\wedge {U}\in {S}\right)\to {X}\in \mathrm{LVec}$
21 19 20 sylan ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {X}\in \mathrm{LVec}$
22 eqid ${⊢}\mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
23 1 22 resssca ${⊢}{U}\in {S}\to \mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({X}\right)$
24 23 eqcomd ${⊢}{U}\in {S}\to \mathrm{Scalar}\left({X}\right)=\mathrm{Scalar}\left({W}\right)$
25 24 adantl ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to \mathrm{Scalar}\left({X}\right)=\mathrm{Scalar}\left({W}\right)$
26 22 phlsrng ${⊢}{W}\in \mathrm{PreHil}\to \mathrm{Scalar}\left({W}\right)\in \mathrm{*-Ring}$
27 26 adantr ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to \mathrm{Scalar}\left({W}\right)\in \mathrm{*-Ring}$
28 25 27 eqeltrd ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to \mathrm{Scalar}\left({X}\right)\in \mathrm{*-Ring}$
29 simpl ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {W}\in \mathrm{PreHil}$
30 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
31 1 30 ressbasss ${⊢}{\mathrm{Base}}_{{X}}\subseteq {\mathrm{Base}}_{{W}}$
32 31 sseli ${⊢}{x}\in {\mathrm{Base}}_{{X}}\to {x}\in {\mathrm{Base}}_{{W}}$
33 31 sseli ${⊢}{y}\in {\mathrm{Base}}_{{X}}\to {y}\in {\mathrm{Base}}_{{W}}$
34 eqid ${⊢}{\cdot }_{𝑖}\left({W}\right)={\cdot }_{𝑖}\left({W}\right)$
35 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
36 22 34 30 35 ipcl ${⊢}\left({W}\in \mathrm{PreHil}\wedge {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)}$
37 29 32 33 36 syl3an ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\right)\to {x}{\cdot }_{𝑖}\left({W}\right){y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
38 24 fveq2d ${⊢}{U}\in {S}\to {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
39 38 eleq2d ${⊢}{U}\in {S}\to \left({x}{\cdot }_{𝑖}\left({W}\right){y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}↔{x}{\cdot }_{𝑖}\left({W}\right){y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)$
40 39 adantl ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to \left({x}{\cdot }_{𝑖}\left({W}\right){y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}↔{x}{\cdot }_{𝑖}\left({W}\right){y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)$
41 40 3ad2ant1 ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\right)\to \left({x}{\cdot }_{𝑖}\left({W}\right){y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}↔{x}{\cdot }_{𝑖}\left({W}\right){y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)$
42 37 41 mpbird ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\right)\to {x}{\cdot }_{𝑖}\left({W}\right){y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}$
43 eqid ${⊢}{\cdot }_{𝑖}\left({X}\right)={\cdot }_{𝑖}\left({X}\right)$
44 1 34 43 ssipeq ${⊢}{U}\in {S}\to {\cdot }_{𝑖}\left({X}\right)={\cdot }_{𝑖}\left({W}\right)$
45 44 oveqd ${⊢}{U}\in {S}\to {x}{\cdot }_{𝑖}\left({X}\right){y}={x}{\cdot }_{𝑖}\left({W}\right){y}$
46 45 eleq1d ${⊢}{U}\in {S}\to \left({x}{\cdot }_{𝑖}\left({X}\right){y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}↔{x}{\cdot }_{𝑖}\left({W}\right){y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}\right)$
47 46 adantl ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to \left({x}{\cdot }_{𝑖}\left({X}\right){y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}↔{x}{\cdot }_{𝑖}\left({W}\right){y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}\right)$
48 47 3ad2ant1 ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\right)\to \left({x}{\cdot }_{𝑖}\left({X}\right){y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}↔{x}{\cdot }_{𝑖}\left({W}\right){y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}\right)$
49 42 48 mpbird ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\right)\to {x}{\cdot }_{𝑖}\left({X}\right){y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}$
50 29 3ad2ant1 ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}\wedge \left({x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\wedge {z}\in {\mathrm{Base}}_{{X}}\right)\right)\to {W}\in \mathrm{PreHil}$
51 7 adantr ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {W}\in \mathrm{LMod}$
52 51 3ad2ant1 ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}\wedge \left({x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\wedge {z}\in {\mathrm{Base}}_{{X}}\right)\right)\to {W}\in \mathrm{LMod}$
53 25 fveq2d ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
54 53 eleq2d ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to \left({q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}↔{q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)$
55 54 biimpa ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}\right)\to {q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
56 55 3adant3 ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}\wedge \left({x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\wedge {z}\in {\mathrm{Base}}_{{X}}\right)\right)\to {q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
57 32 3ad2ant1 ${⊢}\left({x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\wedge {z}\in {\mathrm{Base}}_{{X}}\right)\to {x}\in {\mathrm{Base}}_{{W}}$
58 57 3ad2ant3 ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}\wedge \left({x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\wedge {z}\in {\mathrm{Base}}_{{X}}\right)\right)\to {x}\in {\mathrm{Base}}_{{W}}$
59 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
60 30 22 59 35 lmodvscl ${⊢}\left({W}\in \mathrm{LMod}\wedge {q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {x}\in {\mathrm{Base}}_{{W}}\right)\to {q}{\cdot }_{{W}}{x}\in {\mathrm{Base}}_{{W}}$
61 52 56 58 60 syl3anc ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}\wedge \left({x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\wedge {z}\in {\mathrm{Base}}_{{X}}\right)\right)\to {q}{\cdot }_{{W}}{x}\in {\mathrm{Base}}_{{W}}$
62 33 3ad2ant2 ${⊢}\left({x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\wedge {z}\in {\mathrm{Base}}_{{X}}\right)\to {y}\in {\mathrm{Base}}_{{W}}$
63 62 3ad2ant3 ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}\wedge \left({x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\wedge {z}\in {\mathrm{Base}}_{{X}}\right)\right)\to {y}\in {\mathrm{Base}}_{{W}}$
64 31 sseli ${⊢}{z}\in {\mathrm{Base}}_{{X}}\to {z}\in {\mathrm{Base}}_{{W}}$
65 64 3ad2ant3 ${⊢}\left({x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\wedge {z}\in {\mathrm{Base}}_{{X}}\right)\to {z}\in {\mathrm{Base}}_{{W}}$
66 65 3ad2ant3 ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}\wedge \left({x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\wedge {z}\in {\mathrm{Base}}_{{X}}\right)\right)\to {z}\in {\mathrm{Base}}_{{W}}$
67 eqid ${⊢}{+}_{{W}}={+}_{{W}}$
68 eqid ${⊢}{+}_{\mathrm{Scalar}\left({W}\right)}={+}_{\mathrm{Scalar}\left({W}\right)}$
69 22 34 30 67 68 ipdir ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({q}{\cdot }_{{W}}{x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\right)\to \left(\left({q}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\right){\cdot }_{𝑖}\left({W}\right){z}=\left(\left({q}{\cdot }_{{W}}{x}\right){\cdot }_{𝑖}\left({W}\right){z}\right){+}_{\mathrm{Scalar}\left({W}\right)}\left({y}{\cdot }_{𝑖}\left({W}\right){z}\right)$
70 50 61 63 66 69 syl13anc ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}\wedge \left({x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\wedge {z}\in {\mathrm{Base}}_{{X}}\right)\right)\to \left(\left({q}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\right){\cdot }_{𝑖}\left({W}\right){z}=\left(\left({q}{\cdot }_{{W}}{x}\right){\cdot }_{𝑖}\left({W}\right){z}\right){+}_{\mathrm{Scalar}\left({W}\right)}\left({y}{\cdot }_{𝑖}\left({W}\right){z}\right)$
71 eqid ${⊢}{\cdot }_{\mathrm{Scalar}\left({W}\right)}={\cdot }_{\mathrm{Scalar}\left({W}\right)}$
72 22 34 30 35 59 71 ipass ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {x}\in {\mathrm{Base}}_{{W}}\wedge {z}\in {\mathrm{Base}}_{{W}}\right)\right)\to \left({q}{\cdot }_{{W}}{x}\right){\cdot }_{𝑖}\left({W}\right){z}={q}{\cdot }_{\mathrm{Scalar}\left({W}\right)}\left({x}{\cdot }_{𝑖}\left({W}\right){z}\right)$
73 50 56 58 66 72 syl13anc ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}\wedge \left({x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\wedge {z}\in {\mathrm{Base}}_{{X}}\right)\right)\to \left({q}{\cdot }_{{W}}{x}\right){\cdot }_{𝑖}\left({W}\right){z}={q}{\cdot }_{\mathrm{Scalar}\left({W}\right)}\left({x}{\cdot }_{𝑖}\left({W}\right){z}\right)$
74 73 oveq1d ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}\wedge \left({x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\wedge {z}\in {\mathrm{Base}}_{{X}}\right)\right)\to \left(\left({q}{\cdot }_{{W}}{x}\right){\cdot }_{𝑖}\left({W}\right){z}\right){+}_{\mathrm{Scalar}\left({W}\right)}\left({y}{\cdot }_{𝑖}\left({W}\right){z}\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)$
75 70 74 eqtrd ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}\wedge \left({x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\wedge {z}\in {\mathrm{Base}}_{{X}}\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)$
76 1 67 ressplusg ${⊢}{U}\in {S}\to {+}_{{W}}={+}_{{X}}$
77 76 eqcomd ${⊢}{U}\in {S}\to {+}_{{X}}={+}_{{W}}$
78 1 59 ressvsca ${⊢}{U}\in {S}\to {\cdot }_{{W}}={\cdot }_{{X}}$
79 78 eqcomd ${⊢}{U}\in {S}\to {\cdot }_{{X}}={\cdot }_{{W}}$
80 79 oveqd ${⊢}{U}\in {S}\to {q}{\cdot }_{{X}}{x}={q}{\cdot }_{{W}}{x}$
81 eqidd ${⊢}{U}\in {S}\to {y}={y}$
82 77 80 81 oveq123d ${⊢}{U}\in {S}\to \left({q}{\cdot }_{{X}}{x}\right){+}_{{X}}{y}=\left({q}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}$
83 eqidd ${⊢}{U}\in {S}\to {z}={z}$
84 44 82 83 oveq123d ${⊢}{U}\in {S}\to \left(\left({q}{\cdot }_{{X}}{x}\right){+}_{{X}}{y}\right){\cdot }_{𝑖}\left({X}\right){z}=\left(\left({q}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\right){\cdot }_{𝑖}\left({W}\right){z}$
85 24 fveq2d ${⊢}{U}\in {S}\to {+}_{\mathrm{Scalar}\left({X}\right)}={+}_{\mathrm{Scalar}\left({W}\right)}$
86 24 fveq2d ${⊢}{U}\in {S}\to {\cdot }_{\mathrm{Scalar}\left({X}\right)}={\cdot }_{\mathrm{Scalar}\left({W}\right)}$
87 eqidd ${⊢}{U}\in {S}\to {q}={q}$
88 44 oveqd ${⊢}{U}\in {S}\to {x}{\cdot }_{𝑖}\left({X}\right){z}={x}{\cdot }_{𝑖}\left({W}\right){z}$
89 86 87 88 oveq123d ${⊢}{U}\in {S}\to {q}{\cdot }_{\mathrm{Scalar}\left({X}\right)}\left({x}{\cdot }_{𝑖}\left({X}\right){z}\right)={q}{\cdot }_{\mathrm{Scalar}\left({W}\right)}\left({x}{\cdot }_{𝑖}\left({W}\right){z}\right)$
90 44 oveqd ${⊢}{U}\in {S}\to {y}{\cdot }_{𝑖}\left({X}\right){z}={y}{\cdot }_{𝑖}\left({W}\right){z}$
91 85 89 90 oveq123d ${⊢}{U}\in {S}\to \left({q}{\cdot }_{\mathrm{Scalar}\left({X}\right)}\left({x}{\cdot }_{𝑖}\left({X}\right){z}\right)\right){+}_{\mathrm{Scalar}\left({X}\right)}\left({y}{\cdot }_{𝑖}\left({X}\right){z}\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)$
92 84 91 eqeq12d ${⊢}{U}\in {S}\to \left(\left(\left({q}{\cdot }_{{X}}{x}\right){+}_{{X}}{y}\right){\cdot }_{𝑖}\left({X}\right){z}=\left({q}{\cdot }_{\mathrm{Scalar}\left({X}\right)}\left({x}{\cdot }_{𝑖}\left({X}\right){z}\right)\right){+}_{\mathrm{Scalar}\left({X}\right)}\left({y}{\cdot }_{𝑖}\left({X}\right){z}\right)↔\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)$
93 92 adantl ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to \left(\left(\left({q}{\cdot }_{{X}}{x}\right){+}_{{X}}{y}\right){\cdot }_{𝑖}\left({X}\right){z}=\left({q}{\cdot }_{\mathrm{Scalar}\left({X}\right)}\left({x}{\cdot }_{𝑖}\left({X}\right){z}\right)\right){+}_{\mathrm{Scalar}\left({X}\right)}\left({y}{\cdot }_{𝑖}\left({X}\right){z}\right)↔\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)$
94 93 3ad2ant1 ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}\wedge \left({x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\wedge {z}\in {\mathrm{Base}}_{{X}}\right)\right)\to \left(\left(\left({q}{\cdot }_{{X}}{x}\right){+}_{{X}}{y}\right){\cdot }_{𝑖}\left({X}\right){z}=\left({q}{\cdot }_{\mathrm{Scalar}\left({X}\right)}\left({x}{\cdot }_{𝑖}\left({X}\right){z}\right)\right){+}_{\mathrm{Scalar}\left({X}\right)}\left({y}{\cdot }_{𝑖}\left({X}\right){z}\right)↔\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)$
95 75 94 mpbird ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}\wedge \left({x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\wedge {z}\in {\mathrm{Base}}_{{X}}\right)\right)\to \left(\left({q}{\cdot }_{{X}}{x}\right){+}_{{X}}{y}\right){\cdot }_{𝑖}\left({X}\right){z}=\left({q}{\cdot }_{\mathrm{Scalar}\left({X}\right)}\left({x}{\cdot }_{𝑖}\left({X}\right){z}\right)\right){+}_{\mathrm{Scalar}\left({X}\right)}\left({y}{\cdot }_{𝑖}\left({X}\right){z}\right)$
96 44 adantl ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {\cdot }_{𝑖}\left({X}\right)={\cdot }_{𝑖}\left({W}\right)$
97 96 oveqdr ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {x}\in {\mathrm{Base}}_{{X}}\right)\to {x}{\cdot }_{𝑖}\left({X}\right){x}={x}{\cdot }_{𝑖}\left({W}\right){x}$
98 24 fveq2d ${⊢}{U}\in {S}\to {0}_{\mathrm{Scalar}\left({X}\right)}={0}_{\mathrm{Scalar}\left({W}\right)}$
99 98 adantl ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {0}_{\mathrm{Scalar}\left({X}\right)}={0}_{\mathrm{Scalar}\left({W}\right)}$
100 99 adantr ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {x}\in {\mathrm{Base}}_{{X}}\right)\to {0}_{\mathrm{Scalar}\left({X}\right)}={0}_{\mathrm{Scalar}\left({W}\right)}$
101 97 100 eqeq12d ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {x}\in {\mathrm{Base}}_{{X}}\right)\to \left({x}{\cdot }_{𝑖}\left({X}\right){x}={0}_{\mathrm{Scalar}\left({X}\right)}↔{x}{\cdot }_{𝑖}\left({W}\right){x}={0}_{\mathrm{Scalar}\left({W}\right)}\right)$
102 eqid ${⊢}{0}_{\mathrm{Scalar}\left({W}\right)}={0}_{\mathrm{Scalar}\left({W}\right)}$
103 22 34 30 102 8 ipeq0 ${⊢}\left({W}\in \mathrm{PreHil}\wedge {x}\in {\mathrm{Base}}_{{W}}\right)\to \left({x}{\cdot }_{𝑖}\left({W}\right){x}={0}_{\mathrm{Scalar}\left({W}\right)}↔{x}={0}_{{W}}\right)$
104 29 32 103 syl2an ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {x}\in {\mathrm{Base}}_{{X}}\right)\to \left({x}{\cdot }_{𝑖}\left({W}\right){x}={0}_{\mathrm{Scalar}\left({W}\right)}↔{x}={0}_{{W}}\right)$
105 104 biimpd ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {x}\in {\mathrm{Base}}_{{X}}\right)\to \left({x}{\cdot }_{𝑖}\left({W}\right){x}={0}_{\mathrm{Scalar}\left({W}\right)}\to {x}={0}_{{W}}\right)$
106 101 105 sylbid ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {x}\in {\mathrm{Base}}_{{X}}\right)\to \left({x}{\cdot }_{𝑖}\left({X}\right){x}={0}_{\mathrm{Scalar}\left({X}\right)}\to {x}={0}_{{W}}\right)$
107 106 3impia ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {x}\in {\mathrm{Base}}_{{X}}\wedge {x}{\cdot }_{𝑖}\left({X}\right){x}={0}_{\mathrm{Scalar}\left({X}\right)}\right)\to {x}={0}_{{W}}$
108 24 fveq2d ${⊢}{U}\in {S}\to {*}_{\mathrm{Scalar}\left({X}\right)}={*}_{\mathrm{Scalar}\left({W}\right)}$
109 108 fveq1d ${⊢}{U}\in {S}\to {\left({x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{{*}_{\mathrm{Scalar}\left({X}\right)}}={\left({x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{{*}_{\mathrm{Scalar}\left({W}\right)}}$
110 109 adantl ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {\left({x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{{*}_{\mathrm{Scalar}\left({X}\right)}}={\left({x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{{*}_{\mathrm{Scalar}\left({W}\right)}}$
111 110 3ad2ant1 ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\right)\to {\left({x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{{*}_{\mathrm{Scalar}\left({X}\right)}}={\left({x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{{*}_{\mathrm{Scalar}\left({W}\right)}}$
112 eqid ${⊢}{*}_{\mathrm{Scalar}\left({W}\right)}={*}_{\mathrm{Scalar}\left({W}\right)}$
113 22 34 30 112 ipcj ${⊢}\left({W}\in \mathrm{PreHil}\wedge {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}$
114 29 32 33 113 syl3an ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\right)\to {\left({x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{{*}_{\mathrm{Scalar}\left({W}\right)}}={y}{\cdot }_{𝑖}\left({W}\right){x}$
115 111 114 eqtrd ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\right)\to {\left({x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{{*}_{\mathrm{Scalar}\left({X}\right)}}={y}{\cdot }_{𝑖}\left({W}\right){x}$
116 45 fveq2d ${⊢}{U}\in {S}\to {\left({x}{\cdot }_{𝑖}\left({X}\right){y}\right)}^{{*}_{\mathrm{Scalar}\left({X}\right)}}={\left({x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{{*}_{\mathrm{Scalar}\left({X}\right)}}$
117 44 oveqd ${⊢}{U}\in {S}\to {y}{\cdot }_{𝑖}\left({X}\right){x}={y}{\cdot }_{𝑖}\left({W}\right){x}$
118 116 117 eqeq12d ${⊢}{U}\in {S}\to \left({\left({x}{\cdot }_{𝑖}\left({X}\right){y}\right)}^{{*}_{\mathrm{Scalar}\left({X}\right)}}={y}{\cdot }_{𝑖}\left({X}\right){x}↔{\left({x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{{*}_{\mathrm{Scalar}\left({X}\right)}}={y}{\cdot }_{𝑖}\left({W}\right){x}\right)$
119 118 adantl ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to \left({\left({x}{\cdot }_{𝑖}\left({X}\right){y}\right)}^{{*}_{\mathrm{Scalar}\left({X}\right)}}={y}{\cdot }_{𝑖}\left({X}\right){x}↔{\left({x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{{*}_{\mathrm{Scalar}\left({X}\right)}}={y}{\cdot }_{𝑖}\left({W}\right){x}\right)$
120 119 3ad2ant1 ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\right)\to \left({\left({x}{\cdot }_{𝑖}\left({X}\right){y}\right)}^{{*}_{\mathrm{Scalar}\left({X}\right)}}={y}{\cdot }_{𝑖}\left({X}\right){x}↔{\left({x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{{*}_{\mathrm{Scalar}\left({X}\right)}}={y}{\cdot }_{𝑖}\left({W}\right){x}\right)$
121 115 120 mpbird ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\wedge {x}\in {\mathrm{Base}}_{{X}}\wedge {y}\in {\mathrm{Base}}_{{X}}\right)\to {\left({x}{\cdot }_{𝑖}\left({X}\right){y}\right)}^{{*}_{\mathrm{Scalar}\left({X}\right)}}={y}{\cdot }_{𝑖}\left({X}\right){x}$
122 3 4 5 6 12 13 14 15 16 17 18 21 28 49 95 107 121 isphld ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {X}\in \mathrm{PreHil}$