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 ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
phlssphl.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion phlssphl ( ( 𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ PreHil )

Proof

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