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 ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑊 ) )
isphld.a ⊢ ( 𝜑 → + = ( +g ‘ 𝑊 ) )
isphld.s ⊢ ( 𝜑 → · = ( ·𝑠 ‘ 𝑊 ) )
isphld.i ⊢ ( 𝜑 → 𝐼 = ( ·𝑖 ‘ 𝑊 ) )
isphld.z ⊢ ( 𝜑 → 0 = ( 0g ‘ 𝑊 ) )
isphld.f ⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝑊 ) )
isphld.k ⊢ ( 𝜑 → 𝐾 = ( Base ‘ 𝐹 ) )
isphld.p ⊢ ( 𝜑 → ⨣ = ( +g ‘ 𝐹 ) )
isphld.t ⊢ ( 𝜑 → × = ( .r ‘ 𝐹 ) )
isphld.c ⊢ ( 𝜑 → ∗ = ( *𝑟 ‘ 𝐹 ) )
isphld.o ⊢ ( 𝜑 → 𝑂 = ( 0g ‘ 𝐹 ) )
isphld.l ⊢ ( 𝜑 → 𝑊 ∈ LVec )
isphld.r ⊢ ( 𝜑 → 𝐹 ∈ *-Ring )
isphld.cl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 𝐼 𝑦 ) ∈ 𝐾 )
isphld.d ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐾 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( ( 𝑞 · 𝑥 ) + 𝑦 ) 𝐼 𝑧 ) = ( ( 𝑞 × ( 𝑥 𝐼 𝑧 ) ) ⨣ ( 𝑦 𝐼 𝑧 ) ) )
isphld.ns ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ ( 𝑥 𝐼 𝑥 ) = 𝑂 ) → 𝑥 = 0 )
isphld.cj ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( ∗ ‘ ( 𝑥 𝐼 𝑦 ) ) = ( 𝑦 𝐼 𝑥 ) )
Assertion isphld ( 𝜑 → 𝑊 ∈ PreHil )

Proof

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