isslmd - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > isslmd		Structured version Visualization version GIF version

Theorem isslmd 29086

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 = (0_g‘𝑊)
isslmd.f	⊢ 𝐹 = (Scalar‘𝑊)
isslmd.k	⊢ 𝐾 = (Base‘𝐹)
isslmd.p	⊢ ⨣ = (+_g‘𝐹)
isslmd.t	⊢ × = (._r‘𝐹)
isslmd.u	⊢ 1 = (1_r‘𝐹)
isslmd.o	⊢ 𝑂 = (0_g‘𝐹)

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

Colors of variables: wff setvar class

Syntax hints: ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ∀wral 2896 [wsbc 3402 ‘cfv 5804 (class class class)co 6549 Basecbs 15695 +_gcplusg 15768 ._rcmulr 15769 Scalarcsca 15771 ·_𝑠 cvsca 15772 0_gc0g 15923 CMndccmn 18016 1_rcur 18324 SRingcsrg 18328 SLModcslmd 29084

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-nul 4717

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-sbc 3403 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-iota 5768 df-fv 5812 df-ov 6552 df-slmd 29085

This theorem is referenced by: slmdlema 29087 lmodslmd 29088 slmdcmn 29089 slmdsrg 29091 xrge0slmod 29175

W3C validator