Metamath Proof Explorer

Theorem isslmd

Description: The predicate "is a semimodule". (Contributed by NM, 4-Nov-2013) (Revised by Mario Carneiro, 19-Jun-2014) (Revised by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Hypotheses isslmd.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
isslmd.a ⊢ + = ( +g ‘ 𝑊 )
isslmd.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
isslmd.0 ⊢ 0 = ( 0g ‘ 𝑊 )
isslmd.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
isslmd.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
isslmd.p ⊢ ⨣ = ( +g ‘ 𝐹 )
isslmd.t ⊢ × = ( .r ‘ 𝐹 )
isslmd.u ⊢ 1 = ( 1r ‘ 𝐹 )
isslmd.o ⊢ 𝑂 = ( 0g ‘ 𝐹 )
Assertion isslmd ( 𝑊 ∈ SLMod ↔ ( 𝑊 ∈ CMnd ∧ 𝐹 ∈ SRing ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 isslmd.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 isslmd.a ⊢ + = ( +g ‘ 𝑊 )
3 isslmd.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
4 isslmd.0 ⊢ 0 = ( 0g ‘ 𝑊 )
5 isslmd.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
6 isslmd.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
7 isslmd.p ⊢ ⨣ = ( +g ‘ 𝐹 )
8 isslmd.t ⊢ × = ( .r ‘ 𝐹 )
9 isslmd.u ⊢ 1 = ( 1r ‘ 𝐹 )
10 isslmd.o ⊢ 𝑂 = ( 0g ‘ 𝐹 )
11 fvex ⊢ ( Base ‘ 𝑔 ) ∈ V
12 fvex ⊢ ( +g ‘ 𝑔 ) ∈ V
13 fvex ⊢ ( ·𝑠 ‘ 𝑔 ) ∈ V
14 fvex ⊢ ( Scalar ‘ 𝑔 ) ∈ V
15 fvex ⊢ ( Base ‘ 𝑓 ) ∈ V
16 fvex ⊢ ( +g ‘ 𝑓 ) ∈ V
17 fvex ⊢ ( .r ‘ 𝑓 ) ∈ V
18 simp1 ⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → 𝑘 = ( Base ‘ 𝑓 ) )
19 simp2 ⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → 𝑝 = ( +g ‘ 𝑓 ) )
20 19 oveqd ⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( 𝑞 𝑝 𝑟 ) = ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) )
21 20 oveq1d ⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) )
22 21 eqeq1d ⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ↔ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) )
23 22 3anbi3d ⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ↔ ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ) )
24 simp3 ⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → 𝑡 = ( .r ‘ 𝑓 ) )
25 24 oveqd ⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( 𝑞 𝑡 𝑟 ) = ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) )
26 25 oveq1d ⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) )
27 26 eqeq1d ⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ↔ ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ) )
28 27 3anbi1d ⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ↔ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) )
29 23 28 anbi12d ⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) )
30 29 2ralbidv ⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) )
31 18 30 raleqbidv ⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) )
32 18 31 raleqbidv ⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑞 ∈ ( Base ‘ 𝑓 ) ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) )
33 32 anbi2d ⊢ ( ( 𝑘 = ( Base ‘ 𝑓 ) ∧ 𝑝 = ( +g ‘ 𝑓 ) ∧ 𝑡 = ( .r ‘ 𝑓 ) ) → ( ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ↔ ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ ( Base ‘ 𝑓 ) ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) )
34 15 16 17 33 sbc3ie ⊢ ( [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ↔ ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ ( Base ‘ 𝑓 ) ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) )
35 simpr ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → 𝑓 = ( Scalar ‘ 𝑔 ) )
36 35 eleq1d ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑓 ∈ SRing ↔ ( Scalar ‘ 𝑔 ) ∈ SRing ) )
37 35 fveq2d ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( Base ‘ 𝑓 ) = ( Base ‘ ( Scalar ‘ 𝑔 ) ) )
38 simpl ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → 𝑠 = ( ·𝑠 ‘ 𝑔 ) )
39 38 oveqd ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑟 𝑠 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) )
40 39 eleq1d ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ↔ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ) )
41 38 oveqd ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) )
42 38 oveqd ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑟 𝑠 𝑥 ) = ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) )
43 39 42 oveq12d ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) )
44 41 43 eqeq12d ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ↔ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ) )
45 35 fveq2d ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( +g ‘ 𝑓 ) = ( +g ‘ ( Scalar ‘ 𝑔 ) ) )
46 45 oveqd ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) = ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) )
47 eqidd ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → 𝑤 = 𝑤 )
48 38 46 47 oveq123d ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) )
49 38 oveqd ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑞 𝑠 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) )
50 49 39 oveq12d ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) )
51 48 50 eqeq12d ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ↔ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) )
52 40 44 51 3anbi123d ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ↔ ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ) )
53 35 fveq2d ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( .r ‘ 𝑓 ) = ( .r ‘ ( Scalar ‘ 𝑔 ) ) )
54 53 oveqd ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) = ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) )
55 38 54 47 oveq123d ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) )
56 eqidd ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → 𝑞 = 𝑞 )
57 38 56 39 oveq123d ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) )
58 55 57 eqeq12d ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ↔ ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) )
59 35 fveq2d ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 1r ‘ 𝑓 ) = ( 1r ‘ ( Scalar ‘ 𝑔 ) ) )
60 38 59 47 oveq123d ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) )
61 60 eqeq1d ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ↔ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ) )
62 35 fveq2d ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 0g ‘ 𝑓 ) = ( 0g ‘ ( Scalar ‘ 𝑔 ) ) )
63 38 62 47 oveq123d ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) )
64 63 eqeq1d ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ↔ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) )
65 58 61 64 3anbi123d ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ↔ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) )
66 52 65 anbi12d ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) )
67 66 2ralbidv ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) )
68 37 67 raleqbidv ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) )
69 37 68 raleqbidv ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ∀ 𝑞 ∈ ( Base ‘ 𝑓 ) ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) )
70 36 69 anbi12d ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ ( Base ‘ 𝑓 ) ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝑓 ) 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ↔ ( ( Scalar ‘ 𝑔 ) ∈ SRing ∧ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) )
71 34 70 bitrid ⊢ ( ( 𝑠 = ( ·𝑠 ‘ 𝑔 ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ↔ ( ( Scalar ‘ 𝑔 ) ∈ SRing ∧ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) )
72 13 14 71 sbc2ie ⊢ ( [ ( ·𝑠 ‘ 𝑔 ) / 𝑠 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ↔ ( ( Scalar ‘ 𝑔 ) ∈ SRing ∧ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) )
73 simpl ⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → 𝑣 = ( Base ‘ 𝑔 ) )
74 73 eleq2d ⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ↔ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ) )
75 simpr ⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → 𝑎 = ( +g ‘ 𝑔 ) )
76 75 oveqd ⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( 𝑤 𝑎 𝑥 ) = ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) )
77 76 oveq2d ⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) )
78 75 oveqd ⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) )
79 77 78 eqeq12d ⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ↔ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ) )
80 75 oveqd ⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) )
81 80 eqeq2d ⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ↔ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) )
82 74 79 81 3anbi123d ⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ↔ ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ) )
83 82 anbi1d ⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) )
84 73 83 raleqbidv ⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑤 ∈ ( Base ‘ 𝑔 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) )
85 73 84 raleqbidv ⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∀ 𝑤 ∈ ( Base ‘ 𝑔 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) )
86 85 2ralbidv ⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∀ 𝑤 ∈ ( Base ‘ 𝑔 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) )
87 86 anbi2d ⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( ( ( Scalar ‘ 𝑔 ) ∈ SRing ∧ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) 𝑎 ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ↔ ( ( Scalar ‘ 𝑔 ) ∈ SRing ∧ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∀ 𝑤 ∈ ( Base ‘ 𝑔 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) )
88 72 87 bitrid ⊢ ( ( 𝑣 = ( Base ‘ 𝑔 ) ∧ 𝑎 = ( +g ‘ 𝑔 ) ) → ( [ ( ·𝑠 ‘ 𝑔 ) / 𝑠 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ↔ ( ( Scalar ‘ 𝑔 ) ∈ SRing ∧ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∀ 𝑤 ∈ ( Base ‘ 𝑔 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ) )
89 11 12 88 sbc2ie ⊢ ( [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( +g ‘ 𝑔 ) / 𝑎 ] [ ( ·𝑠 ‘ 𝑔 ) / 𝑠 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ↔ ( ( Scalar ‘ 𝑔 ) ∈ SRing ∧ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∀ 𝑤 ∈ ( Base ‘ 𝑔 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) )
90 fveq2 ⊢ ( 𝑔 = 𝑊 → ( Scalar ‘ 𝑔 ) = ( Scalar ‘ 𝑊 ) )
91 90 5 eqtr4di ⊢ ( 𝑔 = 𝑊 → ( Scalar ‘ 𝑔 ) = 𝐹 )
92 91 eleq1d ⊢ ( 𝑔 = 𝑊 → ( ( Scalar ‘ 𝑔 ) ∈ SRing ↔ 𝐹 ∈ SRing ) )
93 91 fveq2d ⊢ ( 𝑔 = 𝑊 → ( Base ‘ ( Scalar ‘ 𝑔 ) ) = ( Base ‘ 𝐹 ) )
94 93 6 eqtr4di ⊢ ( 𝑔 = 𝑊 → ( Base ‘ ( Scalar ‘ 𝑔 ) ) = 𝐾 )
95 fveq2 ⊢ ( 𝑔 = 𝑊 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝑊 ) )
96 95 1 eqtr4di ⊢ ( 𝑔 = 𝑊 → ( Base ‘ 𝑔 ) = 𝑉 )
97 fveq2 ⊢ ( 𝑔 = 𝑊 → ( ·𝑠 ‘ 𝑔 ) = ( ·𝑠 ‘ 𝑊 ) )
98 97 3 eqtr4di ⊢ ( 𝑔 = 𝑊 → ( ·𝑠 ‘ 𝑔 ) = · )
99 98 oveqd ⊢ ( 𝑔 = 𝑊 → ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑟 · 𝑤 ) )
100 99 96 eleq12d ⊢ ( 𝑔 = 𝑊 → ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ↔ ( 𝑟 · 𝑤 ) ∈ 𝑉 ) )
101 eqidd ⊢ ( 𝑔 = 𝑊 → 𝑟 = 𝑟 )
102 fveq2 ⊢ ( 𝑔 = 𝑊 → ( +g ‘ 𝑔 ) = ( +g ‘ 𝑊 ) )
103 102 2 eqtr4di ⊢ ( 𝑔 = 𝑊 → ( +g ‘ 𝑔 ) = + )
104 103 oveqd ⊢ ( 𝑔 = 𝑊 → ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) = ( 𝑤 + 𝑥 ) )
105 98 101 104 oveq123d ⊢ ( 𝑔 = 𝑊 → ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( 𝑟 · ( 𝑤 + 𝑥 ) ) )
106 98 oveqd ⊢ ( 𝑔 = 𝑊 → ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) = ( 𝑟 · 𝑥 ) )
107 103 99 106 oveq123d ⊢ ( 𝑔 = 𝑊 → ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) )
108 105 107 eqeq12d ⊢ ( 𝑔 = 𝑊 → ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ↔ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ) )
109 91 fveq2d ⊢ ( 𝑔 = 𝑊 → ( +g ‘ ( Scalar ‘ 𝑔 ) ) = ( +g ‘ 𝐹 ) )
110 109 7 eqtr4di ⊢ ( 𝑔 = 𝑊 → ( +g ‘ ( Scalar ‘ 𝑔 ) ) = ⨣ )
111 110 oveqd ⊢ ( 𝑔 = 𝑊 → ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) = ( 𝑞 ⨣ 𝑟 ) )
112 eqidd ⊢ ( 𝑔 = 𝑊 → 𝑤 = 𝑤 )
113 98 111 112 oveq123d ⊢ ( 𝑔 = 𝑊 → ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) )
114 98 oveqd ⊢ ( 𝑔 = 𝑊 → ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 · 𝑤 ) )
115 103 114 99 oveq123d ⊢ ( 𝑔 = 𝑊 → ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) )
116 113 115 eqeq12d ⊢ ( 𝑔 = 𝑊 → ( ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ↔ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) )
117 100 108 116 3anbi123d ⊢ ( 𝑔 = 𝑊 → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ↔ ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ) )
118 91 fveq2d ⊢ ( 𝑔 = 𝑊 → ( .r ‘ ( Scalar ‘ 𝑔 ) ) = ( .r ‘ 𝐹 ) )
119 118 8 eqtr4di ⊢ ( 𝑔 = 𝑊 → ( .r ‘ ( Scalar ‘ 𝑔 ) ) = × )
120 119 oveqd ⊢ ( 𝑔 = 𝑊 → ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) = ( 𝑞 × 𝑟 ) )
121 98 120 112 oveq123d ⊢ ( 𝑔 = 𝑊 → ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 × 𝑟 ) · 𝑤 ) )
122 eqidd ⊢ ( 𝑔 = 𝑊 → 𝑞 = 𝑞 )
123 98 122 99 oveq123d ⊢ ( 𝑔 = 𝑊 → ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) )
124 121 123 eqeq12d ⊢ ( 𝑔 = 𝑊 → ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ↔ ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ) )
125 91 fveq2d ⊢ ( 𝑔 = 𝑊 → ( 1r ‘ ( Scalar ‘ 𝑔 ) ) = ( 1r ‘ 𝐹 ) )
126 125 9 eqtr4di ⊢ ( 𝑔 = 𝑊 → ( 1r ‘ ( Scalar ‘ 𝑔 ) ) = 1 )
127 98 126 112 oveq123d ⊢ ( 𝑔 = 𝑊 → ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 1 · 𝑤 ) )
128 127 eqeq1d ⊢ ( 𝑔 = 𝑊 → ( ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ↔ ( 1 · 𝑤 ) = 𝑤 ) )
129 91 fveq2d ⊢ ( 𝑔 = 𝑊 → ( 0g ‘ ( Scalar ‘ 𝑔 ) ) = ( 0g ‘ 𝐹 ) )
130 129 10 eqtr4di ⊢ ( 𝑔 = 𝑊 → ( 0g ‘ ( Scalar ‘ 𝑔 ) ) = 𝑂 )
131 98 130 112 oveq123d ⊢ ( 𝑔 = 𝑊 → ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑂 · 𝑤 ) )
132 fveq2 ⊢ ( 𝑔 = 𝑊 → ( 0g ‘ 𝑔 ) = ( 0g ‘ 𝑊 ) )
133 132 4 eqtr4di ⊢ ( 𝑔 = 𝑊 → ( 0g ‘ 𝑔 ) = 0 )
134 131 133 eqeq12d ⊢ ( 𝑔 = 𝑊 → ( ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ↔ ( 𝑂 · 𝑤 ) = 0 ) )
135 124 128 134 3anbi123d ⊢ ( 𝑔 = 𝑊 → ( ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ↔ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) )
136 117 135 anbi12d ⊢ ( 𝑔 = 𝑊 → ( ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) )
137 96 136 raleqbidv ⊢ ( 𝑔 = 𝑊 → ( ∀ 𝑤 ∈ ( Base ‘ 𝑔 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) )
138 96 137 raleqbidv ⊢ ( 𝑔 = 𝑊 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∀ 𝑤 ∈ ( Base ‘ 𝑔 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) )
139 94 138 raleqbidv ⊢ ( 𝑔 = 𝑊 → ( ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∀ 𝑤 ∈ ( Base ‘ 𝑔 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) )
140 94 139 raleqbidv ⊢ ( 𝑔 = 𝑊 → ( ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∀ 𝑤 ∈ ( Base ‘ 𝑔 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ↔ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) )
141 92 140 anbi12d ⊢ ( 𝑔 = 𝑊 → ( ( ( Scalar ‘ 𝑔 ) ∈ SRing ∧ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∀ 𝑤 ∈ ( Base ‘ 𝑔 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ∈ ( Base ‘ 𝑔 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑔 ) ( 𝑤 ( +g ‘ 𝑔 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ( +g ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑔 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑔 ) ( 𝑟 ( ·𝑠 ‘ 𝑔 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑔 ) ) ( ·𝑠 ‘ 𝑔 ) 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ↔ ( 𝐹 ∈ SRing ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) ) )
142 89 141 bitrid ⊢ ( 𝑔 = 𝑊 → ( [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( +g ‘ 𝑔 ) / 𝑎 ] [ ( ·𝑠 ‘ 𝑔 ) / 𝑠 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) ↔ ( 𝐹 ∈ SRing ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) ) )
143 df-slmd ⊢ SLMod = { 𝑔 ∈ CMnd ∣ [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( +g ‘ 𝑔 ) / 𝑎 ] [ ( ·𝑠 ‘ 𝑔 ) / 𝑠 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) }
144 142 143 elrab2 ⊢ ( 𝑊 ∈ SLMod ↔ ( 𝑊 ∈ CMnd ∧ ( 𝐹 ∈ SRing ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) ) )
145 3anass ⊢ ( ( 𝑊 ∈ CMnd ∧ 𝐹 ∈ SRing ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) ↔ ( 𝑊 ∈ CMnd ∧ ( 𝐹 ∈ SRing ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) ) )
146 144 145 bitr4i ⊢ ( 𝑊 ∈ SLMod ↔ ( 𝑊 ∈ CMnd ∧ 𝐹 ∈ SRing ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 ⨣ 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ∧ ( 𝑂 · 𝑤 ) = 0 ) ) ) )