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 syl5bb ( ( 𝑠 = ( ·𝑠𝑔 ) ∧ 𝑓 = ( 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 syl5bb ( ( 𝑣 = ( 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 syl5bb ( 𝑔 = 𝑊 → ( [ ( 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 ) ) ) )