Theorem slmdlema 30824

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 30823	. . . . 5 ⊢ (𝑊 ∈ SLMod ↔ (𝑊 ∈ CMnd ∧ 𝐹 ∈ SRing ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
12	11	simp3bi 1142	. . . 4 ⊢ (𝑊 ∈ SLMod → ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )))
13		oveq1 7155	. . . . . . . . . 10 ⊢ (𝑞 = 𝑄 → (𝑞 ⨣ 𝑟) = (𝑄 ⨣ 𝑟))
14	13	oveq1d 7163	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑄 ⨣ 𝑟) · 𝑤))
15		oveq1 7155	. . . . . . . . . 10 ⊢ (𝑞 = 𝑄 → (𝑞 · 𝑤) = (𝑄 · 𝑤))
16	15	oveq1d 7163	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → ((𝑞 · 𝑤) + (𝑟 · 𝑤)) = ((𝑄 · 𝑤) + (𝑟 · 𝑤)))
17	14, 16	eqeq12d 2835	. . . . . . . 8 ⊢ (𝑞 = 𝑄 → (((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤)) ↔ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))))
18	17	3anbi3d 1436	. . . . . . 7 ⊢ (𝑞 = 𝑄 → (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ↔ ((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤)))))
19		oveq1 7155	. . . . . . . . . 10 ⊢ (𝑞 = 𝑄 → (𝑞 × 𝑟) = (𝑄 × 𝑟))
20	19	oveq1d 7163	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → ((𝑞 × 𝑟) · 𝑤) = ((𝑄 × 𝑟) · 𝑤))
21		oveq1 7155	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → (𝑞 · (𝑟 · 𝑤)) = (𝑄 · (𝑟 · 𝑤)))
22	20, 21	eqeq12d 2835	. . . . . . . 8 ⊢ (𝑞 = 𝑄 → (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ↔ ((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤))))
23	22	3anbi1d 1434	. . . . . . 7 ⊢ (𝑞 = 𝑄 → ((((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ) ↔ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )))
24	18, 23	anbi12d 632	. . . . . 6 ⊢ (𝑞 = 𝑄 → ((((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )) ↔ (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
25	24	2ralbidv 3197	. . . . 5 ⊢ (𝑞 = 𝑄 → (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )) ↔ ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
26		oveq1 7155	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (𝑟 · 𝑤) = (𝑅 · 𝑤))
27	26	eleq1d 2895	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ((𝑟 · 𝑤) ∈ 𝑉 ↔ (𝑅 · 𝑤) ∈ 𝑉))
28		oveq1 7155	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (𝑟 · (𝑤 + 𝑥)) = (𝑅 · (𝑤 + 𝑥)))
29		oveq1 7155	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (𝑟 · 𝑥) = (𝑅 · 𝑥))
30	26, 29	oveq12d 7166	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ((𝑟 · 𝑤) + (𝑟 · 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)))
31	28, 30	eqeq12d 2835	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ((𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ↔ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥))))
32		oveq2 7156	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (𝑄 ⨣ 𝑟) = (𝑄 ⨣ 𝑅))
33	32	oveq1d 7163	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 ⨣ 𝑅) · 𝑤))
34	26	oveq2d 7164	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ((𝑄 · 𝑤) + (𝑟 · 𝑤)) = ((𝑄 · 𝑤) + (𝑅 · 𝑤)))
35	33, 34	eqeq12d 2835	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤)) ↔ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))))
36	27, 31, 35	3anbi123d 1430	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ↔ ((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤)))))
37		oveq2 7156	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (𝑄 × 𝑟) = (𝑄 × 𝑅))
38	37	oveq1d 7163	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ((𝑄 × 𝑟) · 𝑤) = ((𝑄 × 𝑅) · 𝑤))
39	26	oveq2d 7164	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (𝑄 · (𝑟 · 𝑤)) = (𝑄 · (𝑅 · 𝑤)))
40	38, 39	eqeq12d 2835	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ↔ ((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤))))
41	40	3anbi1d 1434	. . . . . . 7 ⊢ (𝑟 = 𝑅 → ((((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ) ↔ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )))
42	36, 41	anbi12d 632	. . . . . 6 ⊢ (𝑟 = 𝑅 → ((((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )) ↔ (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
43	42	2ralbidv 3197	. . . . 5 ⊢ (𝑟 = 𝑅 → (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )) ↔ ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
44	25, 43	rspc2v 3631	. . . 4 ⊢ ((𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) → (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )) → ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
45	12, 44	mpan9 509	. . 3 ⊢ ((𝑊 ∈ SLMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) → ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )))
46		oveq2 7156	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (𝑤 + 𝑥) = (𝑤 + 𝑋))
47	46	oveq2d 7164	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝑅 · (𝑤 + 𝑥)) = (𝑅 · (𝑤 + 𝑋)))
48		oveq2 7156	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (𝑅 · 𝑥) = (𝑅 · 𝑋))
49	48	oveq2d 7164	. . . . . . 7 ⊢ (𝑥 = 𝑋 → ((𝑅 · 𝑤) + (𝑅 · 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)))
50	47, 49	eqeq12d 2835	. . . . . 6 ⊢ (𝑥 = 𝑋 → ((𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ↔ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋))))
51	50	3anbi2d 1435	. . . . 5 ⊢ (𝑥 = 𝑋 → (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ↔ ((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤)))))
52	51	anbi1d 631	. . . 4 ⊢ (𝑥 = 𝑋 → ((((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )) ↔ (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
53		oveq2 7156	. . . . . . 7 ⊢ (𝑤 = 𝑌 → (𝑅 · 𝑤) = (𝑅 · 𝑌))
54	53	eleq1d 2895	. . . . . 6 ⊢ (𝑤 = 𝑌 → ((𝑅 · 𝑤) ∈ 𝑉 ↔ (𝑅 · 𝑌) ∈ 𝑉))
55		oveq1 7155	. . . . . . . 8 ⊢ (𝑤 = 𝑌 → (𝑤 + 𝑋) = (𝑌 + 𝑋))
56	55	oveq2d 7164	. . . . . . 7 ⊢ (𝑤 = 𝑌 → (𝑅 · (𝑤 + 𝑋)) = (𝑅 · (𝑌 + 𝑋)))
57	53	oveq1d 7163	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ((𝑅 · 𝑤) + (𝑅 · 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)))
58	56, 57	eqeq12d 2835	. . . . . 6 ⊢ (𝑤 = 𝑌 → ((𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ↔ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋))))
59		oveq2 7156	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 ⨣ 𝑅) · 𝑌))
60		oveq2 7156	. . . . . . . 8 ⊢ (𝑤 = 𝑌 → (𝑄 · 𝑤) = (𝑄 · 𝑌))
61	60, 53	oveq12d 7166	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ((𝑄 · 𝑤) + (𝑅 · 𝑤)) = ((𝑄 · 𝑌) + (𝑅 · 𝑌)))
62	59, 61	eqeq12d 2835	. . . . . 6 ⊢ (𝑤 = 𝑌 → (((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤)) ↔ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))))
63	54, 58, 62	3anbi123d 1430	. . . . 5 ⊢ (𝑤 = 𝑌 → (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ↔ ((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌)))))
64		oveq2 7156	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ((𝑄 × 𝑅) · 𝑤) = ((𝑄 × 𝑅) · 𝑌))
65	53	oveq2d 7164	. . . . . . 7 ⊢ (𝑤 = 𝑌 → (𝑄 · (𝑅 · 𝑤)) = (𝑄 · (𝑅 · 𝑌)))
66	64, 65	eqeq12d 2835	. . . . . 6 ⊢ (𝑤 = 𝑌 → (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ↔ ((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌))))
67		oveq2 7156	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ( 1 · 𝑤) = ( 1 · 𝑌))
68		id 22	. . . . . . 7 ⊢ (𝑤 = 𝑌 → 𝑤 = 𝑌)
69	67, 68	eqeq12d 2835	. . . . . 6 ⊢ (𝑤 = 𝑌 → (( 1 · 𝑤) = 𝑤 ↔ ( 1 · 𝑌) = 𝑌))
70		oveq2 7156	. . . . . . 7 ⊢ (𝑤 = 𝑌 → (𝑂 · 𝑤) = (𝑂 · 𝑌))
71	70	eqeq1d 2821	. . . . . 6 ⊢ (𝑤 = 𝑌 → ((𝑂 · 𝑤) = 0 ↔ (𝑂 · 𝑌) = 0 ))
72	66, 69, 71	3anbi123d 1430	. . . . 5 ⊢ (𝑤 = 𝑌 → ((((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ) ↔ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌 ∧ (𝑂 · 𝑌) = 0 )))
73	63, 72	anbi12d 632	. . . 4 ⊢ (𝑤 = 𝑌 → ((((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )) ↔ (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌 ∧ (𝑂 · 𝑌) = 0 ))))
74	52, 73	rspc2v 3631	. . 3 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )) → (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌 ∧ (𝑂 · 𝑌) = 0 ))))
75	45, 74	syl5com 31	. 2 ⊢ ((𝑊 ∈ SLMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌 ∧ (𝑂 · 𝑌) = 0 ))))
76	75	3impia 1112	1 ⊢ ((𝑊 ∈ SLMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌 ∧ (𝑂 · 𝑌) = 0 )))

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1082   = wceq 1531   ∈ wcel 2108  ∀wral 3136  ‘cfv 6348  (class class class)co 7148  Basecbs 16475  +_gcplusg 16557  ._rcmulr 16558  Scalarcsca 16560   ·_𝑠 cvsca 16561  0_gc0g 16705  CMndccmn 18898  1_rcur 19243  SRingcsrg 19247  SLModcslmd 30821

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-nul 5201

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7151  df-slmd 30822

This theorem is referenced by:  slmdvscl  30835  slmdvsdi  30836  slmdvsdir  30837  slmdvsass  30838  slmdvs1  30841  slmd0vs  30845