Theorem isslmd

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

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

Proof

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