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 · 𝑤 ) = 𝑤 ) ) ) )