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	bitrid	⊢ ( ( 𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹 ) → ( [ × / 𝑡 ] ( 𝑓 ∈ 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 · 𝑤 ) = 𝑤 ) ) ) )