Metamath Proof Explorer


Theorem islmod

Description: The predicate "is a left module". (Contributed by NM, 4-Nov-2013) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses islmod.v 𝑉 = ( Base ‘ 𝑊 )
islmod.a + = ( +g𝑊 )
islmod.s · = ( ·𝑠𝑊 )
islmod.f 𝐹 = ( Scalar ‘ 𝑊 )
islmod.k 𝐾 = ( Base ‘ 𝐹 )
islmod.p = ( +g𝐹 )
islmod.t × = ( .r𝐹 )
islmod.u 1 = ( 1r𝐹 )
Assertion islmod ( 𝑊 ∈ LMod ↔ ( 𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ) ) ) )

Proof

Step Hyp Ref Expression
1 islmod.v 𝑉 = ( Base ‘ 𝑊 )
2 islmod.a + = ( +g𝑊 )
3 islmod.s · = ( ·𝑠𝑊 )
4 islmod.f 𝐹 = ( Scalar ‘ 𝑊 )
5 islmod.k 𝐾 = ( Base ‘ 𝐹 )
6 islmod.p = ( +g𝐹 )
7 islmod.t × = ( .r𝐹 )
8 islmod.u 1 = ( 1r𝐹 )
9 fveq2 ( 𝑔 = 𝑊 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝑊 ) )
10 9 1 eqtr4di ( 𝑔 = 𝑊 → ( Base ‘ 𝑔 ) = 𝑉 )
11 fveq2 ( 𝑔 = 𝑊 → ( +g𝑔 ) = ( +g𝑊 ) )
12 11 2 eqtr4di ( 𝑔 = 𝑊 → ( +g𝑔 ) = + )
13 fveq2 ( 𝑔 = 𝑊 → ( Scalar ‘ 𝑔 ) = ( Scalar ‘ 𝑊 ) )
14 13 4 eqtr4di ( 𝑔 = 𝑊 → ( Scalar ‘ 𝑔 ) = 𝐹 )
15 fveq2 ( 𝑔 = 𝑊 → ( ·𝑠𝑔 ) = ( ·𝑠𝑊 ) )
16 15 3 eqtr4di ( 𝑔 = 𝑊 → ( ·𝑠𝑔 ) = · )
17 16 sbceq1d ( 𝑔 = 𝑊 → ( [ ( ·𝑠𝑔 ) / 𝑠 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g𝑓 ) / 𝑝 ] [ ( .r𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) ↔ [ · / 𝑠 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g𝑓 ) / 𝑝 ] [ ( .r𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) ) )
18 14 17 sbceqbid ( 𝑔 = 𝑊 → ( [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( ·𝑠𝑔 ) / 𝑠 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g𝑓 ) / 𝑝 ] [ ( .r𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) ↔ [ 𝐹 / 𝑓 ] [ · / 𝑠 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g𝑓 ) / 𝑝 ] [ ( .r𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) ) )
19 12 18 sbceqbid ( 𝑔 = 𝑊 → ( [ ( +g𝑔 ) / 𝑎 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( ·𝑠𝑔 ) / 𝑠 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g𝑓 ) / 𝑝 ] [ ( .r𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) ↔ [ + / 𝑎 ] [ 𝐹 / 𝑓 ] [ · / 𝑠 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g𝑓 ) / 𝑝 ] [ ( .r𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) ) )
20 10 19 sbceqbid ( 𝑔 = 𝑊 → ( [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( +g𝑔 ) / 𝑎 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( ·𝑠𝑔 ) / 𝑠 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g𝑓 ) / 𝑝 ] [ ( .r𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) ↔ [ 𝑉 / 𝑣 ] [ + / 𝑎 ] [ 𝐹 / 𝑓 ] [ · / 𝑠 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g𝑓 ) / 𝑝 ] [ ( .r𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) ) )
21 1 fvexi 𝑉 ∈ V
22 2 fvexi + ∈ V
23 4 fvexi 𝐹 ∈ V
24 simp3 ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → 𝑓 = 𝐹 )
25 24 fveq2d ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( Base ‘ 𝑓 ) = ( Base ‘ 𝐹 ) )
26 25 5 eqtr4di ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( Base ‘ 𝑓 ) = 𝐾 )
27 24 fveq2d ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( +g𝑓 ) = ( +g𝐹 ) )
28 27 6 eqtr4di ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( +g𝑓 ) = )
29 24 fveq2d ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( .r𝑓 ) = ( .r𝐹 ) )
30 29 7 eqtr4di ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( .r𝑓 ) = × )
31 30 sbceq1d ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( [ ( .r𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) ↔ [ × / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) ) )
32 7 fvexi × ∈ V
33 oveq ( 𝑡 = × → ( 𝑞 𝑡 𝑟 ) = ( 𝑞 × 𝑟 ) )
34 33 oveq1d ( 𝑡 = × → ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) )
35 34 eqeq1d ( 𝑡 = × → ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ↔ ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ) )
36 35 anbi1d ( 𝑡 = × → ( ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ↔ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) )
37 36 anbi2d ( 𝑡 = × → ( ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ↔ ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) )
38 37 2ralbidv ( 𝑡 = × → ( ∀ 𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) )
39 38 2ralbidv ( 𝑡 = × → ( ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) )
40 39 anbi2d ( 𝑡 = × → ( ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) ↔ ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) ) )
41 32 40 sbcie ( [ × / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) ↔ ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) )
42 24 eleq1d ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( 𝑓 ∈ Ring ↔ 𝐹 ∈ Ring ) )
43 simp1 ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → 𝑣 = 𝑉 )
44 43 eleq2d ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ↔ ( 𝑟 𝑠 𝑤 ) ∈ 𝑉 ) )
45 simp2 ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → 𝑎 = + )
46 45 oveqd ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( 𝑤 𝑎 𝑥 ) = ( 𝑤 + 𝑥 ) )
47 46 oveq2d ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( 𝑟 𝑠 ( 𝑤 + 𝑥 ) ) )
48 45 oveqd ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑥 ) ) )
49 47 48 eqeq12d ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ↔ ( 𝑟 𝑠 ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑥 ) ) ) )
50 45 oveqd ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) = ( ( 𝑞 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑤 ) ) )
51 50 eqeq2d ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ↔ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑤 ) ) ) )
52 44 49 51 3anbi123d ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ↔ ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 𝑠 ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑤 ) ) ) ) )
53 24 fveq2d ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( 1r𝑓 ) = ( 1r𝐹 ) )
54 53 8 eqtr4di ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( 1r𝑓 ) = 1 )
55 54 oveq1d ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( ( 1r𝑓 ) 𝑠 𝑤 ) = ( 1 𝑠 𝑤 ) )
56 55 eqeq1d ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ↔ ( 1 𝑠 𝑤 ) = 𝑤 ) )
57 56 anbi2d ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ↔ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( 1 𝑠 𝑤 ) = 𝑤 ) ) )
58 52 57 anbi12d ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ↔ ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 𝑠 ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( 1 𝑠 𝑤 ) = 𝑤 ) ) ) )
59 43 58 raleqbidv ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( ∀ 𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑤𝑉 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 𝑠 ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( 1 𝑠 𝑤 ) = 𝑤 ) ) ) )
60 43 59 raleqbidv ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( ∀ 𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑥𝑉𝑤𝑉 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 𝑠 ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( 1 𝑠 𝑤 ) = 𝑤 ) ) ) )
61 60 2ralbidv ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 𝑠 ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( 1 𝑠 𝑤 ) = 𝑤 ) ) ) )
62 42 61 anbi12d ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) ↔ ( 𝐹 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 𝑠 ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( 1 𝑠 𝑤 ) = 𝑤 ) ) ) ) )
63 41 62 syl5bb ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( [ × / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) ↔ ( 𝐹 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 𝑠 ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( 1 𝑠 𝑤 ) = 𝑤 ) ) ) ) )
64 31 63 bitrd ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( [ ( .r𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) ↔ ( 𝐹 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 𝑠 ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( 1 𝑠 𝑤 ) = 𝑤 ) ) ) ) )
65 28 64 sbceqbid ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( [ ( +g𝑓 ) / 𝑝 ] [ ( .r𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) ↔ [ / 𝑝 ] ( 𝐹 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 𝑠 ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( 1 𝑠 𝑤 ) = 𝑤 ) ) ) ) )
66 26 65 sbceqbid ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g𝑓 ) / 𝑝 ] [ ( .r𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) ↔ [ 𝐾 / 𝑘 ] [ / 𝑝 ] ( 𝐹 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 𝑠 ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( 1 𝑠 𝑤 ) = 𝑤 ) ) ) ) )
67 66 sbcbidv ( ( 𝑣 = 𝑉𝑎 = +𝑓 = 𝐹 ) → ( [ · / 𝑠 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g𝑓 ) / 𝑝 ] [ ( .r𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) ↔ [ · / 𝑠 ] [ 𝐾 / 𝑘 ] [ / 𝑝 ] ( 𝐹 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 𝑠 ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( 1 𝑠 𝑤 ) = 𝑤 ) ) ) ) )
68 21 22 23 67 sbc3ie ( [ 𝑉 / 𝑣 ] [ + / 𝑎 ] [ 𝐹 / 𝑓 ] [ · / 𝑠 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g𝑓 ) / 𝑝 ] [ ( .r𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) ↔ [ · / 𝑠 ] [ 𝐾 / 𝑘 ] [ / 𝑝 ] ( 𝐹 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 𝑠 ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( 1 𝑠 𝑤 ) = 𝑤 ) ) ) )
69 3 fvexi · ∈ V
70 5 fvexi 𝐾 ∈ V
71 6 fvexi ∈ V
72 simp2 ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → 𝑘 = 𝐾 )
73 simp1 ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → 𝑠 = · )
74 73 oveqd ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( 𝑟 𝑠 𝑤 ) = ( 𝑟 · 𝑤 ) )
75 74 eleq1d ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑉 ↔ ( 𝑟 · 𝑤 ) ∈ 𝑉 ) )
76 73 oveqd ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( 𝑟 𝑠 ( 𝑤 + 𝑥 ) ) = ( 𝑟 · ( 𝑤 + 𝑥 ) ) )
77 73 oveqd ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( 𝑟 𝑠 𝑥 ) = ( 𝑟 · 𝑥 ) )
78 74 77 oveq12d ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( ( 𝑟 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) )
79 76 78 eqeq12d ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( ( 𝑟 𝑠 ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑥 ) ) ↔ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ) )
80 simp3 ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → 𝑝 = )
81 80 oveqd ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( 𝑞 𝑝 𝑟 ) = ( 𝑞 𝑟 ) )
82 81 oveq1d ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑟 ) 𝑠 𝑤 ) )
83 73 oveqd ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( ( 𝑞 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑟 ) · 𝑤 ) )
84 82 83 eqtrd ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑟 ) · 𝑤 ) )
85 73 oveqd ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( 𝑞 𝑠 𝑤 ) = ( 𝑞 · 𝑤 ) )
86 85 74 oveq12d ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( ( 𝑞 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑤 ) ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) )
87 84 86 eqeq12d ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑤 ) ) ↔ ( ( 𝑞 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) )
88 75 79 87 3anbi123d ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 𝑠 ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑤 ) ) ) ↔ ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ) )
89 73 oveqd ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 × 𝑟 ) · 𝑤 ) )
90 74 oveq2d ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) = ( 𝑞 𝑠 ( 𝑟 · 𝑤 ) ) )
91 73 oveqd ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( 𝑞 𝑠 ( 𝑟 · 𝑤 ) ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) )
92 90 91 eqtrd ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) )
93 89 92 eqeq12d ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ↔ ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ) )
94 73 oveqd ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( 1 𝑠 𝑤 ) = ( 1 · 𝑤 ) )
95 94 eqeq1d ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( ( 1 𝑠 𝑤 ) = 𝑤 ↔ ( 1 · 𝑤 ) = 𝑤 ) )
96 93 95 anbi12d ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( 1 𝑠 𝑤 ) = 𝑤 ) ↔ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ) ) )
97 88 96 anbi12d ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 𝑠 ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( 1 𝑠 𝑤 ) = 𝑤 ) ) ↔ ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ) ) ) )
98 97 2ralbidv ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( ∀ 𝑥𝑉𝑤𝑉 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 𝑠 ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( 1 𝑠 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑥𝑉𝑤𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ) ) ) )
99 72 98 raleqbidv ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( ∀ 𝑟𝑘𝑥𝑉𝑤𝑉 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 𝑠 ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( 1 𝑠 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑟𝐾𝑥𝑉𝑤𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ) ) ) )
100 72 99 raleqbidv ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( ∀ 𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 𝑠 ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( 1 𝑠 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ) ) ) )
101 100 anbi2d ( ( 𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( ( 𝐹 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 𝑠 ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( 1 𝑠 𝑤 ) = 𝑤 ) ) ) ↔ ( 𝐹 ∈ Ring ∧ ∀ 𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ) ) ) ) )
102 69 70 71 101 sbc3ie ( [ · / 𝑠 ] [ 𝐾 / 𝑘 ] [ / 𝑝 ] ( 𝐹 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 𝑠 ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) + ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( 1 𝑠 𝑤 ) = 𝑤 ) ) ) ↔ ( 𝐹 ∈ Ring ∧ ∀ 𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ) ) ) )
103 68 102 bitri ( [ 𝑉 / 𝑣 ] [ + / 𝑎 ] [ 𝐹 / 𝑓 ] [ · / 𝑠 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g𝑓 ) / 𝑝 ] [ ( .r𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) ↔ ( 𝐹 ∈ Ring ∧ ∀ 𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ) ) ) )
104 20 103 bitrdi ( 𝑔 = 𝑊 → ( [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( +g𝑔 ) / 𝑎 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( ·𝑠𝑔 ) / 𝑠 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g𝑓 ) / 𝑝 ] [ ( .r𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) ↔ ( 𝐹 ∈ Ring ∧ ∀ 𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ) ) ) ) )
105 df-lmod LMod = { 𝑔 ∈ Grp ∣ [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( +g𝑔 ) / 𝑎 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( ·𝑠𝑔 ) / 𝑠 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g𝑓 ) / 𝑝 ] [ ( .r𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) }
106 104 105 elrab2 ( 𝑊 ∈ LMod ↔ ( 𝑊 ∈ Grp ∧ ( 𝐹 ∈ Ring ∧ ∀ 𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ) ) ) ) )
107 3anass ( ( 𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ) ) ) ↔ ( 𝑊 ∈ Grp ∧ ( 𝐹 ∈ Ring ∧ ∀ 𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ) ) ) ) )
108 106 107 bitr4i ( 𝑊 ∈ LMod ↔ ( 𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 ( ( ( 𝑟 · 𝑤 ) ∈ 𝑉 ∧ ( 𝑟 · ( 𝑤 + 𝑥 ) ) = ( ( 𝑟 · 𝑤 ) + ( 𝑟 · 𝑥 ) ) ∧ ( ( 𝑞 𝑟 ) · 𝑤 ) = ( ( 𝑞 · 𝑤 ) + ( 𝑟 · 𝑤 ) ) ) ∧ ( ( ( 𝑞 × 𝑟 ) · 𝑤 ) = ( 𝑞 · ( 𝑟 · 𝑤 ) ) ∧ ( 1 · 𝑤 ) = 𝑤 ) ) ) )