Theorem slmdlema 31456

Description: Lemma for properties of a semimodule. (Contributed by NM, 8-Dec-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
slmdlema	⊢ ((𝑊 ∈ SLMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌 ∧ (𝑂 · 𝑌) = 0 )))

Proof of Theorem slmdlema

Dummy variables 𝑞 𝑟 𝑤 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isslmd.v	. . . . . 6 ⊢ 𝑉 = (Base‘𝑊)
2		isslmd.a	. . . . . 6 ⊢ + = (+g‘𝑊)
3		isslmd.s	. . . . . 6 ⊢ · = ( ·𝑠 ‘𝑊)
4		isslmd.0	. . . . . 6 ⊢ 0 = (0g‘𝑊)
5		isslmd.f	. . . . . 6 ⊢ 𝐹 = (Scalar‘𝑊)
6		isslmd.k	. . . . . 6 ⊢ 𝐾 = (Base‘𝐹)
7		isslmd.p	. . . . . 6 ⊢ ⨣ = (+g‘𝐹)
8		isslmd.t	. . . . . 6 ⊢ × = (.r‘𝐹)
9		isslmd.u	. . . . . 6 ⊢ 1 = (1r‘𝐹)
10		isslmd.o	. . . . . 6 ⊢ 𝑂 = (0g‘𝐹)
11	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	isslmd 31455	. . . . 5 ⊢ (𝑊 ∈ SLMod ↔ (𝑊 ∈ CMnd ∧ 𝐹 ∈ SRing ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
12	11	simp3bi 1146	. . . 4 ⊢ (𝑊 ∈ SLMod → ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )))
13		oveq1 7282	. . . . . . . . . 10 ⊢ (𝑞 = 𝑄 → (𝑞 ⨣ 𝑟) = (𝑄 ⨣ 𝑟))
14	13	oveq1d 7290	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑄 ⨣ 𝑟) · 𝑤))
15		oveq1 7282	. . . . . . . . . 10 ⊢ (𝑞 = 𝑄 → (𝑞 · 𝑤) = (𝑄 · 𝑤))
16	15	oveq1d 7290	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → ((𝑞 · 𝑤) + (𝑟 · 𝑤)) = ((𝑄 · 𝑤) + (𝑟 · 𝑤)))
17	14, 16	eqeq12d 2754	. . . . . . . 8 ⊢ (𝑞 = 𝑄 → (((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤)) ↔ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))))
18	17	3anbi3d 1441	. . . . . . 7 ⊢ (𝑞 = 𝑄 → (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ↔ ((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤)))))
19		oveq1 7282	. . . . . . . . . 10 ⊢ (𝑞 = 𝑄 → (𝑞 × 𝑟) = (𝑄 × 𝑟))
20	19	oveq1d 7290	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → ((𝑞 × 𝑟) · 𝑤) = ((𝑄 × 𝑟) · 𝑤))
21		oveq1 7282	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → (𝑞 · (𝑟 · 𝑤)) = (𝑄 · (𝑟 · 𝑤)))
22	20, 21	eqeq12d 2754	. . . . . . . 8 ⊢ (𝑞 = 𝑄 → (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ↔ ((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤))))
23	22	3anbi1d 1439	. . . . . . 7 ⊢ (𝑞 = 𝑄 → ((((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ) ↔ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )))
24	18, 23	anbi12d 631	. . . . . 6 ⊢ (𝑞 = 𝑄 → ((((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )) ↔ (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
25	24	2ralbidv 3129	. . . . 5 ⊢ (𝑞 = 𝑄 → (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )) ↔ ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
26		oveq1 7282	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (𝑟 · 𝑤) = (𝑅 · 𝑤))
27	26	eleq1d 2823	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ((𝑟 · 𝑤) ∈ 𝑉 ↔ (𝑅 · 𝑤) ∈ 𝑉))
28		oveq1 7282	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (𝑟 · (𝑤 + 𝑥)) = (𝑅 · (𝑤 + 𝑥)))
29		oveq1 7282	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (𝑟 · 𝑥) = (𝑅 · 𝑥))
30	26, 29	oveq12d 7293	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ((𝑟 · 𝑤) + (𝑟 · 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)))
31	28, 30	eqeq12d 2754	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ((𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ↔ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥))))
32		oveq2 7283	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (𝑄 ⨣ 𝑟) = (𝑄 ⨣ 𝑅))
33	32	oveq1d 7290	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 ⨣ 𝑅) · 𝑤))
34	26	oveq2d 7291	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ((𝑄 · 𝑤) + (𝑟 · 𝑤)) = ((𝑄 · 𝑤) + (𝑅 · 𝑤)))
35	33, 34	eqeq12d 2754	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤)) ↔ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))))
36	27, 31, 35	3anbi123d 1435	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ↔ ((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤)))))
37		oveq2 7283	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (𝑄 × 𝑟) = (𝑄 × 𝑅))
38	37	oveq1d 7290	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ((𝑄 × 𝑟) · 𝑤) = ((𝑄 × 𝑅) · 𝑤))
39	26	oveq2d 7291	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (𝑄 · (𝑟 · 𝑤)) = (𝑄 · (𝑅 · 𝑤)))
40	38, 39	eqeq12d 2754	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ↔ ((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤))))
41	40	3anbi1d 1439	. . . . . . 7 ⊢ (𝑟 = 𝑅 → ((((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ) ↔ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )))
42	36, 41	anbi12d 631	. . . . . 6 ⊢ (𝑟 = 𝑅 → ((((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )) ↔ (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
43	42	2ralbidv 3129	. . . . 5 ⊢ (𝑟 = 𝑅 → (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )) ↔ ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
44	25, 43	rspc2v 3570	. . . 4 ⊢ ((𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) → (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )) → ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
45	12, 44	mpan9 507	. . 3 ⊢ ((𝑊 ∈ SLMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) → ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )))
46		oveq2 7283	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (𝑤 + 𝑥) = (𝑤 + 𝑋))
47	46	oveq2d 7291	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝑅 · (𝑤 + 𝑥)) = (𝑅 · (𝑤 + 𝑋)))
48		oveq2 7283	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (𝑅 · 𝑥) = (𝑅 · 𝑋))
49	48	oveq2d 7291	. . . . . . 7 ⊢ (𝑥 = 𝑋 → ((𝑅 · 𝑤) + (𝑅 · 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)))
50	47, 49	eqeq12d 2754	. . . . . 6 ⊢ (𝑥 = 𝑋 → ((𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ↔ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋))))
51	50	3anbi2d 1440	. . . . 5 ⊢ (𝑥 = 𝑋 → (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ↔ ((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤)))))
52	51	anbi1d 630	. . . 4 ⊢ (𝑥 = 𝑋 → ((((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )) ↔ (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
53		oveq2 7283	. . . . . . 7 ⊢ (𝑤 = 𝑌 → (𝑅 · 𝑤) = (𝑅 · 𝑌))
54	53	eleq1d 2823	. . . . . 6 ⊢ (𝑤 = 𝑌 → ((𝑅 · 𝑤) ∈ 𝑉 ↔ (𝑅 · 𝑌) ∈ 𝑉))
55		oveq1 7282	. . . . . . . 8 ⊢ (𝑤 = 𝑌 → (𝑤 + 𝑋) = (𝑌 + 𝑋))
56	55	oveq2d 7291	. . . . . . 7 ⊢ (𝑤 = 𝑌 → (𝑅 · (𝑤 + 𝑋)) = (𝑅 · (𝑌 + 𝑋)))
57	53	oveq1d 7290	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ((𝑅 · 𝑤) + (𝑅 · 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)))
58	56, 57	eqeq12d 2754	. . . . . 6 ⊢ (𝑤 = 𝑌 → ((𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ↔ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋))))
59		oveq2 7283	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 ⨣ 𝑅) · 𝑌))
60		oveq2 7283	. . . . . . . 8 ⊢ (𝑤 = 𝑌 → (𝑄 · 𝑤) = (𝑄 · 𝑌))
61	60, 53	oveq12d 7293	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ((𝑄 · 𝑤) + (𝑅 · 𝑤)) = ((𝑄 · 𝑌) + (𝑅 · 𝑌)))
62	59, 61	eqeq12d 2754	. . . . . 6 ⊢ (𝑤 = 𝑌 → (((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤)) ↔ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))))
63	54, 58, 62	3anbi123d 1435	. . . . 5 ⊢ (𝑤 = 𝑌 → (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ↔ ((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌)))))
64		oveq2 7283	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ((𝑄 × 𝑅) · 𝑤) = ((𝑄 × 𝑅) · 𝑌))
65	53	oveq2d 7291	. . . . . . 7 ⊢ (𝑤 = 𝑌 → (𝑄 · (𝑅 · 𝑤)) = (𝑄 · (𝑅 · 𝑌)))
66	64, 65	eqeq12d 2754	. . . . . 6 ⊢ (𝑤 = 𝑌 → (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ↔ ((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌))))
67		oveq2 7283	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ( 1 · 𝑤) = ( 1 · 𝑌))
68		id 22	. . . . . . 7 ⊢ (𝑤 = 𝑌 → 𝑤 = 𝑌)
69	67, 68	eqeq12d 2754	. . . . . 6 ⊢ (𝑤 = 𝑌 → (( 1 · 𝑤) = 𝑤 ↔ ( 1 · 𝑌) = 𝑌))
70		oveq2 7283	. . . . . . 7 ⊢ (𝑤 = 𝑌 → (𝑂 · 𝑤) = (𝑂 · 𝑌))
71	70	eqeq1d 2740	. . . . . 6 ⊢ (𝑤 = 𝑌 → ((𝑂 · 𝑤) = 0 ↔ (𝑂 · 𝑌) = 0 ))
72	66, 69, 71	3anbi123d 1435	. . . . 5 ⊢ (𝑤 = 𝑌 → ((((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ) ↔ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌 ∧ (𝑂 · 𝑌) = 0 )))
73	63, 72	anbi12d 631	. . . 4 ⊢ (𝑤 = 𝑌 → ((((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )) ↔ (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌 ∧ (𝑂 · 𝑌) = 0 ))))
74	52, 73	rspc2v 3570	. . 3 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )) → (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌 ∧ (𝑂 · 𝑌) = 0 ))))
75	45, 74	syl5com 31	. 2 ⊢ ((𝑊 ∈ SLMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌 ∧ (𝑂 · 𝑌) = 0 ))))
76	75	3impia 1116	1 ⊢ ((𝑊 ∈ SLMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌 ∧ (𝑂 · 𝑌) = 0 )))

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106  ∀wral 3064  ‘cfv 6433  (class class class)co 7275  Basecbs 16912  +_gcplusg 16962  ._rcmulr 16963  Scalarcsca 16965   ·_𝑠 cvsca 16966  0_gc0g 17150  CMndccmn 19386  1_rcur 19737  SRingcsrg 19741  SLModcslmd 31453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-nul 5230

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-ov 7278  df-slmd 31454

This theorem is referenced by:  slmdvscl  31467  slmdvsdi  31468  slmdvsdir  31469  slmdvsass  31470  slmdvs1  31473  slmd0vs  31477