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 30496

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 6514	. . . . 5 ⊢ (Base‘𝑔) ∈ V
2		fvex 6514	. . . . 5 ⊢ (+_g‘𝑔) ∈ V
3		fvex 6514	. . . . . . 7 ⊢ ( ·_𝑠 ‘𝑔) ∈ V
4		fvex 6514	. . . . . . 7 ⊢ (Scalar‘𝑔) ∈ V
5		fvex 6514	. . . . . . . . 9 ⊢ (Base‘𝑓) ∈ V
6		fvex 6514	. . . . . . . . 9 ⊢ (+_g‘𝑓) ∈ V
7		fvex 6514	. . . . . . . . 9 ⊢ (._r‘𝑓) ∈ V
8		simp1 1116	. . . . . . . . . . 11 ⊢ ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+_g‘𝑓) ∧ 𝑡 = (._r‘𝑓)) → 𝑘 = (Base‘𝑓))
9		simp2 1117	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+_g‘𝑓) ∧ 𝑡 = (._r‘𝑓)) → 𝑝 = (+_g‘𝑓))
10	9	oveqd 6995	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+_g‘𝑓) ∧ 𝑡 = (._r‘𝑓)) → (𝑞𝑝𝑟) = (𝑞(+_g‘𝑓)𝑟))
11	10	oveq1d 6993	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+_g‘𝑓) ∧ 𝑡 = (._r‘𝑓)) → ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞(+_g‘𝑓)𝑟)𝑠𝑤))
12	11	eqeq1d 2780	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+_g‘𝑓) ∧ 𝑡 = (._r‘𝑓)) → (((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)) ↔ ((𝑞(+_g‘𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))))
13	12	3anbi3d 1421	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+_g‘𝑓) ∧ 𝑡 = (._r‘𝑓)) → (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ↔ ((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+_g‘𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)))))
14		simp3 1118	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+_g‘𝑓) ∧ 𝑡 = (._r‘𝑓)) → 𝑡 = (._r‘𝑓))
15	14	oveqd 6995	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+_g‘𝑓) ∧ 𝑡 = (._r‘𝑓)) → (𝑞𝑡𝑟) = (𝑞(._r‘𝑓)𝑟))
16	15	oveq1d 6993	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+_g‘𝑓) ∧ 𝑡 = (._r‘𝑓)) → ((𝑞𝑡𝑟)𝑠𝑤) = ((𝑞(._r‘𝑓)𝑟)𝑠𝑤))
17	16	eqeq1d 2780	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+_g‘𝑓) ∧ 𝑡 = (._r‘𝑓)) → (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ↔ ((𝑞(._r‘𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤))))
18	17	3anbi1d 1419	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+_g‘𝑓) ∧ 𝑡 = (._r‘𝑓)) → ((((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1_r‘𝑓)𝑠𝑤) = 𝑤 ∧ ((0_g‘𝑓)𝑠𝑤) = (0_g‘𝑔)) ↔ (((𝑞(._r‘𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1_r‘𝑓)𝑠𝑤) = 𝑤 ∧ ((0_g‘𝑓)𝑠𝑤) = (0_g‘𝑔))))
19	13, 18	anbi12d 621	. . . . . . . . . . . . 13 ⊢ ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+_g‘𝑓) ∧ 𝑡 = (._r‘𝑓)) → ((((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1_r‘𝑓)𝑠𝑤) = 𝑤 ∧ ((0_g‘𝑓)𝑠𝑤) = (0_g‘𝑔))) ↔ (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+_g‘𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(._r‘𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1_r‘𝑓)𝑠𝑤) = 𝑤 ∧ ((0_g‘𝑓)𝑠𝑤) = (0_g‘𝑔)))))
20	19	2ralbidv 3149	. . . . . . . . . . . 12 ⊢ ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+_g‘𝑓) ∧ 𝑡 = (._r‘𝑓)) → (∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1_r‘𝑓)𝑠𝑤) = 𝑤 ∧ ((0_g‘𝑓)𝑠𝑤) = (0_g‘𝑔))) ↔ ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+_g‘𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(._r‘𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1_r‘𝑓)𝑠𝑤) = 𝑤 ∧ ((0_g‘𝑓)𝑠𝑤) = (0_g‘𝑔)))))
21	8, 20	raleqbidv 3341	. . . . . . . . . . 11 ⊢ ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+_g‘𝑓) ∧ 𝑡 = (._r‘𝑓)) → (∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1_r‘𝑓)𝑠𝑤) = 𝑤 ∧ ((0_g‘𝑓)𝑠𝑤) = (0_g‘𝑔))) ↔ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+_g‘𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(._r‘𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1_r‘𝑓)𝑠𝑤) = 𝑤 ∧ ((0_g‘𝑓)𝑠𝑤) = (0_g‘𝑔)))))
22	8, 21	raleqbidv 3341	. . . . . . . . . 10 ⊢ ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+_g‘𝑓) ∧ 𝑡 = (._r‘𝑓)) → (∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1_r‘𝑓)𝑠𝑤) = 𝑤 ∧ ((0_g‘𝑓)𝑠𝑤) = (0_g‘𝑔))) ↔ ∀𝑞 ∈ (Base‘𝑓)∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+_g‘𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(._r‘𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1_r‘𝑓)𝑠𝑤) = 𝑤 ∧ ((0_g‘𝑓)𝑠𝑤) = (0_g‘𝑔)))))
23	22	anbi2d 619	. . . . . . . . 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 3757	. . . . . . . 8 ⊢ ([(Base‘𝑓) / 𝑘][(+_g‘𝑓) / 𝑝][(._r‘𝑓) / 𝑡](𝑓 ∈ SRing ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1_r‘𝑓)𝑠𝑤) = 𝑤 ∧ ((0_g‘𝑓)𝑠𝑤) = (0_g‘𝑔)))) ↔ (𝑓 ∈ SRing ∧ ∀𝑞 ∈ (Base‘𝑓)∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+_g‘𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(._r‘𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1_r‘𝑓)𝑠𝑤) = 𝑤 ∧ ((0_g‘𝑓)𝑠𝑤) = (0_g‘𝑔)))))
25		simpr 477	. . . . . . . . . 10 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → 𝑓 = (Scalar‘𝑔))
26	25	eleq1d 2850	. . . . . . . . 9 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑓 ∈ SRing ↔ (Scalar‘𝑔) ∈ SRing))
27	25	fveq2d 6505	. . . . . . . . . 10 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (Base‘𝑓) = (Base‘(Scalar‘𝑔)))
28		simpl 475	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → 𝑠 = ( ·_𝑠 ‘𝑔))
29	28	oveqd 6995	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑟𝑠𝑤) = (𝑟( ·_𝑠 ‘𝑔)𝑤))
30	29	eleq1d 2850	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((𝑟𝑠𝑤) ∈ 𝑣 ↔ (𝑟( ·_𝑠 ‘𝑔)𝑤) ∈ 𝑣))
31	28	oveqd 6995	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑟𝑠(𝑤𝑎𝑥)) = (𝑟( ·_𝑠 ‘𝑔)(𝑤𝑎𝑥)))
32	28	oveqd 6995	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑟𝑠𝑥) = (𝑟( ·_𝑠 ‘𝑔)𝑥))
33	29, 32	oveq12d 6996	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) = ((𝑟( ·_𝑠 ‘𝑔)𝑤)𝑎(𝑟( ·_𝑠 ‘𝑔)𝑥)))
34	31, 33	eqeq12d 2793	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ↔ (𝑟( ·_𝑠 ‘𝑔)(𝑤𝑎𝑥)) = ((𝑟( ·_𝑠 ‘𝑔)𝑤)𝑎(𝑟( ·_𝑠 ‘𝑔)𝑥))))
35	25	fveq2d 6505	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (+_g‘𝑓) = (+_g‘(Scalar‘𝑔)))
36	35	oveqd 6995	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑞(+_g‘𝑓)𝑟) = (𝑞(+_g‘(Scalar‘𝑔))𝑟))
37		eqidd 2779	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → 𝑤 = 𝑤)
38	28, 36, 37	oveq123d 6999	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((𝑞(+_g‘𝑓)𝑟)𝑠𝑤) = ((𝑞(+_g‘(Scalar‘𝑔))𝑟)( ·_𝑠 ‘𝑔)𝑤))
39	28	oveqd 6995	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑞𝑠𝑤) = (𝑞( ·_𝑠 ‘𝑔)𝑤))
40	39, 29	oveq12d 6996	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)) = ((𝑞( ·_𝑠 ‘𝑔)𝑤)𝑎(𝑟( ·_𝑠 ‘𝑔)𝑤)))
41	38, 40	eqeq12d 2793	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (((𝑞(+_g‘𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)) ↔ ((𝑞(+_g‘(Scalar‘𝑔))𝑟)( ·_𝑠 ‘𝑔)𝑤) = ((𝑞( ·_𝑠 ‘𝑔)𝑤)𝑎(𝑟( ·_𝑠 ‘𝑔)𝑤))))
42	30, 34, 41	3anbi123d 1415	. . . . . . . . . . . . 13 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+_g‘𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ↔ ((𝑟( ·_𝑠 ‘𝑔)𝑤) ∈ 𝑣 ∧ (𝑟( ·_𝑠 ‘𝑔)(𝑤𝑎𝑥)) = ((𝑟( ·_𝑠 ‘𝑔)𝑤)𝑎(𝑟( ·_𝑠 ‘𝑔)𝑥)) ∧ ((𝑞(+_g‘(Scalar‘𝑔))𝑟)( ·_𝑠 ‘𝑔)𝑤) = ((𝑞( ·_𝑠 ‘𝑔)𝑤)𝑎(𝑟( ·_𝑠 ‘𝑔)𝑤)))))
43	25	fveq2d 6505	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (._r‘𝑓) = (._r‘(Scalar‘𝑔)))
44	43	oveqd 6995	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑞(._r‘𝑓)𝑟) = (𝑞(._r‘(Scalar‘𝑔))𝑟))
45	28, 44, 37	oveq123d 6999	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((𝑞(._r‘𝑓)𝑟)𝑠𝑤) = ((𝑞(._r‘(Scalar‘𝑔))𝑟)( ·_𝑠 ‘𝑔)𝑤))
46		eqidd 2779	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → 𝑞 = 𝑞)
47	28, 46, 29	oveq123d 6999	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑞𝑠(𝑟𝑠𝑤)) = (𝑞( ·_𝑠 ‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑤)))
48	45, 47	eqeq12d 2793	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (((𝑞(._r‘𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ↔ ((𝑞(._r‘(Scalar‘𝑔))𝑟)( ·_𝑠 ‘𝑔)𝑤) = (𝑞( ·_𝑠 ‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑤))))
49	25	fveq2d 6505	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (1_r‘𝑓) = (1_r‘(Scalar‘𝑔)))
50	28, 49, 37	oveq123d 6999	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((1_r‘𝑓)𝑠𝑤) = ((1_r‘(Scalar‘𝑔))( ·_𝑠 ‘𝑔)𝑤))
51	50	eqeq1d 2780	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (((1_r‘𝑓)𝑠𝑤) = 𝑤 ↔ ((1_r‘(Scalar‘𝑔))( ·_𝑠 ‘𝑔)𝑤) = 𝑤))
52	25	fveq2d 6505	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (0_g‘𝑓) = (0_g‘(Scalar‘𝑔)))
53	28, 52, 37	oveq123d 6999	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((0_g‘𝑓)𝑠𝑤) = ((0_g‘(Scalar‘𝑔))( ·_𝑠 ‘𝑔)𝑤))
54	53	eqeq1d 2780	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (((0_g‘𝑓)𝑠𝑤) = (0_g‘𝑔) ↔ ((0_g‘(Scalar‘𝑔))( ·_𝑠 ‘𝑔)𝑤) = (0_g‘𝑔)))
55	48, 51, 54	3anbi123d 1415	. . . . . . . . . . . . 13 ⊢ ((𝑠 = ( ·_𝑠 ‘𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((((𝑞(._r‘𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1_r‘𝑓)𝑠𝑤) = 𝑤 ∧ ((0_g‘𝑓)𝑠𝑤) = (0_g‘𝑔)) ↔ (((𝑞(._r‘(Scalar‘𝑔))𝑟)( ·_𝑠 ‘𝑔)𝑤) = (𝑞( ·_𝑠 ‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑤)) ∧ ((1_r‘(Scalar‘𝑔))( ·_𝑠 ‘𝑔)𝑤) = 𝑤 ∧ ((0_g‘(Scalar‘𝑔))( ·_𝑠 ‘𝑔)𝑤) = (0_g‘𝑔))))
56	42, 55	anbi12d 621	. . . . . . . . . . . 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 3149	. . . . . . . . . . 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 3341	. . . . . . . . . 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 3341	. . . . . . . . 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 621	. . . . . . . 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 275	. . . . . . 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 3755	. . . . . 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 475	. . . . . . . . 9 ⊢ ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+_g‘𝑔)) → 𝑣 = (Base‘𝑔))
64	63	eleq2d 2851	. . . . . . . . . . . 12 ⊢ ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+_g‘𝑔)) → ((𝑟( ·_𝑠 ‘𝑔)𝑤) ∈ 𝑣 ↔ (𝑟( ·_𝑠 ‘𝑔)𝑤) ∈ (Base‘𝑔)))
65		simpr 477	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+_g‘𝑔)) → 𝑎 = (+_g‘𝑔))
66	65	oveqd 6995	. . . . . . . . . . . . . 14 ⊢ ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+_g‘𝑔)) → (𝑤𝑎𝑥) = (𝑤(+_g‘𝑔)𝑥))
67	66	oveq2d 6994	. . . . . . . . . . . . 13 ⊢ ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+_g‘𝑔)) → (𝑟( ·_𝑠 ‘𝑔)(𝑤𝑎𝑥)) = (𝑟( ·_𝑠 ‘𝑔)(𝑤(+_g‘𝑔)𝑥)))
68	65	oveqd 6995	. . . . . . . . . . . . 13 ⊢ ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+_g‘𝑔)) → ((𝑟( ·_𝑠 ‘𝑔)𝑤)𝑎(𝑟( ·_𝑠 ‘𝑔)𝑥)) = ((𝑟( ·_𝑠 ‘𝑔)𝑤)(+_g‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑥)))
69	67, 68	eqeq12d 2793	. . . . . . . . . . . 12 ⊢ ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+_g‘𝑔)) → ((𝑟( ·_𝑠 ‘𝑔)(𝑤𝑎𝑥)) = ((𝑟( ·_𝑠 ‘𝑔)𝑤)𝑎(𝑟( ·_𝑠 ‘𝑔)𝑥)) ↔ (𝑟( ·_𝑠 ‘𝑔)(𝑤(+_g‘𝑔)𝑥)) = ((𝑟( ·_𝑠 ‘𝑔)𝑤)(+_g‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑥))))
70	65	oveqd 6995	. . . . . . . . . . . . 13 ⊢ ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+_g‘𝑔)) → ((𝑞( ·_𝑠 ‘𝑔)𝑤)𝑎(𝑟( ·_𝑠 ‘𝑔)𝑤)) = ((𝑞( ·_𝑠 ‘𝑔)𝑤)(+_g‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑤)))
71	70	eqeq2d 2788	. . . . . . . . . . . 12 ⊢ ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+_g‘𝑔)) → (((𝑞(+_g‘(Scalar‘𝑔))𝑟)( ·_𝑠 ‘𝑔)𝑤) = ((𝑞( ·_𝑠 ‘𝑔)𝑤)𝑎(𝑟( ·_𝑠 ‘𝑔)𝑤)) ↔ ((𝑞(+_g‘(Scalar‘𝑔))𝑟)( ·_𝑠 ‘𝑔)𝑤) = ((𝑞( ·_𝑠 ‘𝑔)𝑤)(+_g‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑤))))
72	64, 69, 71	3anbi123d 1415	. . . . . . . . . . 11 ⊢ ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+_g‘𝑔)) → (((𝑟( ·_𝑠 ‘𝑔)𝑤) ∈ 𝑣 ∧ (𝑟( ·_𝑠 ‘𝑔)(𝑤𝑎𝑥)) = ((𝑟( ·_𝑠 ‘𝑔)𝑤)𝑎(𝑟( ·_𝑠 ‘𝑔)𝑥)) ∧ ((𝑞(+_g‘(Scalar‘𝑔))𝑟)( ·_𝑠 ‘𝑔)𝑤) = ((𝑞( ·_𝑠 ‘𝑔)𝑤)𝑎(𝑟( ·_𝑠 ‘𝑔)𝑤))) ↔ ((𝑟( ·_𝑠 ‘𝑔)𝑤) ∈ (Base‘𝑔) ∧ (𝑟( ·_𝑠 ‘𝑔)(𝑤(+_g‘𝑔)𝑥)) = ((𝑟( ·_𝑠 ‘𝑔)𝑤)(+_g‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑥)) ∧ ((𝑞(+_g‘(Scalar‘𝑔))𝑟)( ·_𝑠 ‘𝑔)𝑤) = ((𝑞( ·_𝑠 ‘𝑔)𝑤)(+_g‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑤)))))
73	72	anbi1d 620	. . . . . . . . . 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 3341	. . . . . . . . 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 3341	. . . . . . . 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 3149	. . . . . . 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 619	. . . . . 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 275	. . . . 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 3755	. . . 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 6501	. . . . . . 7 ⊢ (𝑔 = 𝑊 → (Scalar‘𝑔) = (Scalar‘𝑊))
81		isslmd.f	. . . . . . 7 ⊢ 𝐹 = (Scalar‘𝑊)
82	80, 81	syl6eqr 2832	. . . . . 6 ⊢ (𝑔 = 𝑊 → (Scalar‘𝑔) = 𝐹)
83	82	eleq1d 2850	. . . . 5 ⊢ (𝑔 = 𝑊 → ((Scalar‘𝑔) ∈ SRing ↔ 𝐹 ∈ SRing))
84	82	fveq2d 6505	. . . . . . 7 ⊢ (𝑔 = 𝑊 → (Base‘(Scalar‘𝑔)) = (Base‘𝐹))
85		isslmd.k	. . . . . . 7 ⊢ 𝐾 = (Base‘𝐹)
86	84, 85	syl6eqr 2832	. . . . . 6 ⊢ (𝑔 = 𝑊 → (Base‘(Scalar‘𝑔)) = 𝐾)
87		fveq2 6501	. . . . . . . . 9 ⊢ (𝑔 = 𝑊 → (Base‘𝑔) = (Base‘𝑊))
88		isslmd.v	. . . . . . . . 9 ⊢ 𝑉 = (Base‘𝑊)
89	87, 88	syl6eqr 2832	. . . . . . . 8 ⊢ (𝑔 = 𝑊 → (Base‘𝑔) = 𝑉)
90		fveq2 6501	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑊 → ( ·_𝑠 ‘𝑔) = ( ·_𝑠 ‘𝑊))
91		isslmd.s	. . . . . . . . . . . . . 14 ⊢ · = ( ·_𝑠 ‘𝑊)
92	90, 91	syl6eqr 2832	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑊 → ( ·_𝑠 ‘𝑔) = · )
93	92	oveqd 6995	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑊 → (𝑟( ·_𝑠 ‘𝑔)𝑤) = (𝑟 · 𝑤))
94	93, 89	eleq12d 2860	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑊 → ((𝑟( ·_𝑠 ‘𝑔)𝑤) ∈ (Base‘𝑔) ↔ (𝑟 · 𝑤) ∈ 𝑉))
95		eqidd 2779	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑊 → 𝑟 = 𝑟)
96		fveq2 6501	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑊 → (+_g‘𝑔) = (+_g‘𝑊))
97		isslmd.a	. . . . . . . . . . . . . . 15 ⊢ + = (+_g‘𝑊)
98	96, 97	syl6eqr 2832	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑊 → (+_g‘𝑔) = + )
99	98	oveqd 6995	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑊 → (𝑤(+_g‘𝑔)𝑥) = (𝑤 + 𝑥))
100	92, 95, 99	oveq123d 6999	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑊 → (𝑟( ·_𝑠 ‘𝑔)(𝑤(+_g‘𝑔)𝑥)) = (𝑟 · (𝑤 + 𝑥)))
101	92	oveqd 6995	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑊 → (𝑟( ·_𝑠 ‘𝑔)𝑥) = (𝑟 · 𝑥))
102	98, 93, 101	oveq123d 6999	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑊 → ((𝑟( ·_𝑠 ‘𝑔)𝑤)(+_g‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)))
103	100, 102	eqeq12d 2793	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑊 → ((𝑟( ·_𝑠 ‘𝑔)(𝑤(+_g‘𝑔)𝑥)) = ((𝑟( ·_𝑠 ‘𝑔)𝑤)(+_g‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑥)) ↔ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥))))
104	82	fveq2d 6505	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑊 → (+_g‘(Scalar‘𝑔)) = (+_g‘𝐹))
105		isslmd.p	. . . . . . . . . . . . . . 15 ⊢ ⨣ = (+_g‘𝐹)
106	104, 105	syl6eqr 2832	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑊 → (+_g‘(Scalar‘𝑔)) = ⨣ )
107	106	oveqd 6995	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑊 → (𝑞(+_g‘(Scalar‘𝑔))𝑟) = (𝑞 ⨣ 𝑟))
108		eqidd 2779	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑊 → 𝑤 = 𝑤)
109	92, 107, 108	oveq123d 6999	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑊 → ((𝑞(+_g‘(Scalar‘𝑔))𝑟)( ·_𝑠 ‘𝑔)𝑤) = ((𝑞 ⨣ 𝑟) · 𝑤))
110	92	oveqd 6995	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑊 → (𝑞( ·_𝑠 ‘𝑔)𝑤) = (𝑞 · 𝑤))
111	98, 110, 93	oveq123d 6999	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑊 → ((𝑞( ·_𝑠 ‘𝑔)𝑤)(+_g‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑤)) = ((𝑞 · 𝑤) + (𝑟 · 𝑤)))
112	109, 111	eqeq12d 2793	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑊 → (((𝑞(+_g‘(Scalar‘𝑔))𝑟)( ·_𝑠 ‘𝑔)𝑤) = ((𝑞( ·_𝑠 ‘𝑔)𝑤)(+_g‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑤)) ↔ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))))
113	94, 103, 112	3anbi123d 1415	. . . . . . . . . 10 ⊢ (𝑔 = 𝑊 → (((𝑟( ·_𝑠 ‘𝑔)𝑤) ∈ (Base‘𝑔) ∧ (𝑟( ·_𝑠 ‘𝑔)(𝑤(+_g‘𝑔)𝑥)) = ((𝑟( ·_𝑠 ‘𝑔)𝑤)(+_g‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑥)) ∧ ((𝑞(+_g‘(Scalar‘𝑔))𝑟)( ·_𝑠 ‘𝑔)𝑤) = ((𝑞( ·_𝑠 ‘𝑔)𝑤)(+_g‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑤))) ↔ ((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤)))))
114	82	fveq2d 6505	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑊 → (._r‘(Scalar‘𝑔)) = (._r‘𝐹))
115		isslmd.t	. . . . . . . . . . . . . . 15 ⊢ × = (._r‘𝐹)
116	114, 115	syl6eqr 2832	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑊 → (._r‘(Scalar‘𝑔)) = × )
117	116	oveqd 6995	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑊 → (𝑞(._r‘(Scalar‘𝑔))𝑟) = (𝑞 × 𝑟))
118	92, 117, 108	oveq123d 6999	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑊 → ((𝑞(._r‘(Scalar‘𝑔))𝑟)( ·_𝑠 ‘𝑔)𝑤) = ((𝑞 × 𝑟) · 𝑤))
119		eqidd 2779	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑊 → 𝑞 = 𝑞)
120	92, 119, 93	oveq123d 6999	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑊 → (𝑞( ·_𝑠 ‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑤)) = (𝑞 · (𝑟 · 𝑤)))
121	118, 120	eqeq12d 2793	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑊 → (((𝑞(._r‘(Scalar‘𝑔))𝑟)( ·_𝑠 ‘𝑔)𝑤) = (𝑞( ·_𝑠 ‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑤)) ↔ ((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤))))
122	82	fveq2d 6505	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑊 → (1_r‘(Scalar‘𝑔)) = (1_r‘𝐹))
123		isslmd.u	. . . . . . . . . . . . . 14 ⊢ 1 = (1_r‘𝐹)
124	122, 123	syl6eqr 2832	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑊 → (1_r‘(Scalar‘𝑔)) = 1 )
125	92, 124, 108	oveq123d 6999	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑊 → ((1_r‘(Scalar‘𝑔))( ·_𝑠 ‘𝑔)𝑤) = ( 1 · 𝑤))
126	125	eqeq1d 2780	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑊 → (((1_r‘(Scalar‘𝑔))( ·_𝑠 ‘𝑔)𝑤) = 𝑤 ↔ ( 1 · 𝑤) = 𝑤))
127	82	fveq2d 6505	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑊 → (0_g‘(Scalar‘𝑔)) = (0_g‘𝐹))
128		isslmd.o	. . . . . . . . . . . . . 14 ⊢ 𝑂 = (0_g‘𝐹)
129	127, 128	syl6eqr 2832	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑊 → (0_g‘(Scalar‘𝑔)) = 𝑂)
130	92, 129, 108	oveq123d 6999	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑊 → ((0_g‘(Scalar‘𝑔))( ·_𝑠 ‘𝑔)𝑤) = (𝑂 · 𝑤))
131		fveq2 6501	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑊 → (0_g‘𝑔) = (0_g‘𝑊))
132		isslmd.0	. . . . . . . . . . . . 13 ⊢ 0 = (0_g‘𝑊)
133	131, 132	syl6eqr 2832	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑊 → (0_g‘𝑔) = 0 )
134	130, 133	eqeq12d 2793	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑊 → (((0_g‘(Scalar‘𝑔))( ·_𝑠 ‘𝑔)𝑤) = (0_g‘𝑔) ↔ (𝑂 · 𝑤) = 0 ))
135	121, 126, 134	3anbi123d 1415	. . . . . . . . . 10 ⊢ (𝑔 = 𝑊 → ((((𝑞(._r‘(Scalar‘𝑔))𝑟)( ·_𝑠 ‘𝑔)𝑤) = (𝑞( ·_𝑠 ‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑤)) ∧ ((1_r‘(Scalar‘𝑔))( ·_𝑠 ‘𝑔)𝑤) = 𝑤 ∧ ((0_g‘(Scalar‘𝑔))( ·_𝑠 ‘𝑔)𝑤) = (0_g‘𝑔)) ↔ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )))
136	113, 135	anbi12d 621	. . . . . . . . 9 ⊢ (𝑔 = 𝑊 → ((((𝑟( ·_𝑠 ‘𝑔)𝑤) ∈ (Base‘𝑔) ∧ (𝑟( ·_𝑠 ‘𝑔)(𝑤(+_g‘𝑔)𝑥)) = ((𝑟( ·_𝑠 ‘𝑔)𝑤)(+_g‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑥)) ∧ ((𝑞(+_g‘(Scalar‘𝑔))𝑟)( ·_𝑠 ‘𝑔)𝑤) = ((𝑞( ·_𝑠 ‘𝑔)𝑤)(+_g‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑤))) ∧ (((𝑞(._r‘(Scalar‘𝑔))𝑟)( ·_𝑠 ‘𝑔)𝑤) = (𝑞( ·_𝑠 ‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑤)) ∧ ((1_r‘(Scalar‘𝑔))( ·_𝑠 ‘𝑔)𝑤) = 𝑤 ∧ ((0_g‘(Scalar‘𝑔))( ·_𝑠 ‘𝑔)𝑤) = (0_g‘𝑔))) ↔ (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
137	89, 136	raleqbidv 3341	. . . . . . . 8 ⊢ (𝑔 = 𝑊 → (∀𝑤 ∈ (Base‘𝑔)(((𝑟( ·_𝑠 ‘𝑔)𝑤) ∈ (Base‘𝑔) ∧ (𝑟( ·_𝑠 ‘𝑔)(𝑤(+_g‘𝑔)𝑥)) = ((𝑟( ·_𝑠 ‘𝑔)𝑤)(+_g‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑥)) ∧ ((𝑞(+_g‘(Scalar‘𝑔))𝑟)( ·_𝑠 ‘𝑔)𝑤) = ((𝑞( ·_𝑠 ‘𝑔)𝑤)(+_g‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑤))) ∧ (((𝑞(._r‘(Scalar‘𝑔))𝑟)( ·_𝑠 ‘𝑔)𝑤) = (𝑞( ·_𝑠 ‘𝑔)(𝑟( ·_𝑠 ‘𝑔)𝑤)) ∧ ((1_r‘(Scalar‘𝑔))( ·_𝑠 ‘𝑔)𝑤) = 𝑤 ∧ ((0_g‘(Scalar‘𝑔))( ·_𝑠 ‘𝑔)𝑤) = (0_g‘𝑔))) ↔ ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
138	89, 137	raleqbidv 3341	. . . . . . 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 3341	. . . . . 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 3341	. . . . 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 621	. . . 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 275	. . 3 ⊢ (𝑔 = 𝑊 → ([(Base‘𝑔) / 𝑣][(+_g‘𝑔) / 𝑎][( ·_𝑠 ‘𝑔) / 𝑠][(Scalar‘𝑔) / 𝑓][(Base‘𝑓) / 𝑘][(+_g‘𝑓) / 𝑝][(._r‘𝑓) / 𝑡](𝑓 ∈ SRing ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1_r‘𝑓)𝑠𝑤) = 𝑤 ∧ ((0_g‘𝑓)𝑠𝑤) = (0_g‘𝑔)))) ↔ (𝐹 ∈ SRing ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )))))
143		df-slmd 30495	. . 3 ⊢ SLMod = {𝑔 ∈ CMnd ∣ [(Base‘𝑔) / 𝑣][(+_g‘𝑔) / 𝑎][( ·_𝑠 ‘𝑔) / 𝑠][(Scalar‘𝑔) / 𝑓][(Base‘𝑓) / 𝑘][(+_g‘𝑓) / 𝑝][(._r‘𝑓) / 𝑡](𝑓 ∈ SRing ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1_r‘𝑓)𝑠𝑤) = 𝑤 ∧ ((0_g‘𝑓)𝑠𝑤) = (0_g‘𝑔))))}
144	142, 143	elrab2 3599	. 2 ⊢ (𝑊 ∈ SLMod ↔ (𝑊 ∈ CMnd ∧ (𝐹 ∈ SRing ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )))))
145		3anass 1076	. 2 ⊢ ((𝑊 ∈ CMnd ∧ 𝐹 ∈ SRing ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))) ↔ (𝑊 ∈ CMnd ∧ (𝐹 ∈ SRing ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )))))
146	144, 145	bitr4i 270	1 ⊢ (𝑊 ∈ SLMod ↔ (𝑊 ∈ CMnd ∧ 𝐹 ∈ SRing ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 198 ∧ wa 387 ∧ w3a 1068 = wceq 1507 ∈ wcel 2050 ∀wral 3088 [wsbc 3683 ‘cfv 6190 (class class class)co 6978 Basecbs 16342 +_gcplusg 16424 ._rcmulr 16425 Scalarcsca 16427 ·_𝑠 cvsca 16428 0_gc0g 16572 CMndccmn 18669 1_rcur 18977 SRingcsrg 18981 SLModcslmd 30494

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 ax-nul 5068

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2583 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-sbc 3684 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-nul 4181 df-if 4352 df-sn 4443 df-pr 4445 df-op 4449 df-uni 4714 df-br 4931 df-iota 6154 df-fv 6198 df-ov 6981 df-slmd 30495

This theorem is referenced by: slmdlema 30497 lmodslmd 30498 slmdcmn 30499 slmdsrg 30501 xrge0slmod 30596

W3C validator