Theorem isslmd 32334

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.)

Hypotheses

Ref	Expression
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

Ref	Expression
isslmd	⊢ (𝑊 ∈ SLMod ↔ (𝑊 ∈ CMnd ∧ 𝐹 ∈ SRing ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))

Distinct variable groups:   𝑟,𝑞,𝑤,𝑥, ×   + ,𝑞,𝑟,𝑤,𝑥   ⨣ ,𝑞,𝑟,𝑤,𝑥   1 ,𝑞,𝑟,𝑤,𝑥   · ,𝑞,𝑟,𝑤,𝑥   𝐹,𝑞,𝑟,𝑤,𝑥   𝐾,𝑞,𝑟,𝑤,𝑥   𝑉,𝑞,𝑟,𝑤,𝑥   𝑊,𝑞,𝑟,𝑤,𝑥   0 ,𝑞,𝑟,𝑤,𝑥   𝑂,𝑞,𝑟,𝑤,𝑥

Proof of Theorem isslmd

Dummy variables 𝑓 𝑎 𝑔 𝑘 𝑝 𝑠 𝑡 𝑣 are mutually distinct and distinct from all other variables.

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

Syntax hints:   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ∀wral 3061  [wsbc 3776  ‘cfv 6540  (class class class)co 7405  Basecbs 17140  +_gcplusg 17193  ._rcmulr 17194  Scalarcsca 17196   ·_𝑠 cvsca 17197  0_gc0g 17381  CMndccmn 19642  1_rcur 19998  SRingcsrg 20002  SLModcslmd 32332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-nul 5305

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rab 3433  df-v 3476  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7408  df-slmd 32333

This theorem is referenced by:  slmdlema  32335  lmodslmd  32336  slmdcmn  32337  slmdsrg  32339  xrge0slmod  32451