lmodlema - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > lmodlema		Structured version Visualization version GIF version

Theorem lmodlema 21102

Description: Lemma for properties of a left module. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)

**Hypotheses**
Ref	Expression
islmod.v	⊢ 𝑉 = (Base‘𝑊)
islmod.a	⊢ + = (+_g‘𝑊)
islmod.s	⊢ · = ( ·_𝑠 ‘𝑊)
islmod.f	⊢ 𝐹 = (Scalar‘𝑊)
islmod.k	⊢ 𝐾 = (Base‘𝐹)
islmod.p	⊢ ⨣ = (+_g‘𝐹)
islmod.t	⊢ × = (._r‘𝐹)
islmod.u	⊢ 1 = (1_r‘𝐹)

**Assertion**
Ref	Expression
lmodlema	⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌)))

Proof of Theorem lmodlema Dummy variables 𝑞 𝑟 𝑤 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		islmod.v	. . . . . 6 ⊢ 𝑉 = (Base‘𝑊)
2		islmod.a	. . . . . 6 ⊢ + = (+_g‘𝑊)
3		islmod.s	. . . . . 6 ⊢ · = ( ·_𝑠 ‘𝑊)
4		islmod.f	. . . . . 6 ⊢ 𝐹 = (Scalar‘𝑊)
5		islmod.k	. . . . . 6 ⊢ 𝐾 = (Base‘𝐹)
6		islmod.p	. . . . . 6 ⊢ ⨣ = (+_g‘𝐹)
7		islmod.t	. . . . . 6 ⊢ × = (._r‘𝐹)
8		islmod.u	. . . . . 6 ⊢ 1 = (1_r‘𝐹)
9	1, 2, 3, 4, 5, 6, 7, 8	islmod 21101	. . . . 5 ⊢ (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
10	9	simp3bi 1165	. . . 4 ⊢ (𝑊 ∈ LMod → ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
11		oveq1 7415	. . . . . . . . . 10 ⊢ (𝑞 = 𝑄 → (𝑞 ⨣ 𝑟) = (𝑄 ⨣ 𝑟))
12	11	oveq1d 7423	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑄 ⨣ 𝑟) · 𝑤))
13		oveq1 7415	. . . . . . . . . 10 ⊢ (𝑞 = 𝑄 → (𝑞 · 𝑤) = (𝑄 · 𝑤))
14	13	oveq1d 7423	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → ((𝑞 · 𝑤) + (𝑟 · 𝑤)) = ((𝑄 · 𝑤) + (𝑟 · 𝑤)))
15	12, 14	eqeq12d 2776	. . . . . . . 8 ⊢ (𝑞 = 𝑄 → (((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤)) ↔ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))))
16	15	3anbi3d 1470	. . . . . . 7 ⊢ (𝑞 = 𝑄 → (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ↔ ((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤)))))
17		oveq1 7415	. . . . . . . . . 10 ⊢ (𝑞 = 𝑄 → (𝑞 × 𝑟) = (𝑄 × 𝑟))
18	17	oveq1d 7423	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → ((𝑞 × 𝑟) · 𝑤) = ((𝑄 × 𝑟) · 𝑤))
19		oveq1 7415	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → (𝑞 · (𝑟 · 𝑤)) = (𝑄 · (𝑟 · 𝑤)))
20	18, 19	eqeq12d 2776	. . . . . . . 8 ⊢ (𝑞 = 𝑄 → (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ↔ ((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤))))
21	20	anbi1d 643	. . . . . . 7 ⊢ (𝑞 = 𝑄 → ((((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤) ↔ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
22	16, 21	anbi12d 644	. . . . . 6 ⊢ (𝑞 = 𝑄 → ((((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
23	22	2ralbidv 3226	. . . . 5 ⊢ (𝑞 = 𝑄 → (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
24		oveq1 7415	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (𝑟 · 𝑤) = (𝑅 · 𝑤))
25	24	eleq1d 2845	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ((𝑟 · 𝑤) ∈ 𝑉 ↔ (𝑅 · 𝑤) ∈ 𝑉))
26		oveq1 7415	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (𝑟 · (𝑤 + 𝑥)) = (𝑅 · (𝑤 + 𝑥)))
27		oveq1 7415	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (𝑟 · 𝑥) = (𝑅 · 𝑥))
28	24, 27	oveq12d 7426	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ((𝑟 · 𝑤) + (𝑟 · 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)))
29	26, 28	eqeq12d 2776	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ((𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ↔ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥))))
30		oveq2 7416	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (𝑄 ⨣ 𝑟) = (𝑄 ⨣ 𝑅))
31	30	oveq1d 7423	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 ⨣ 𝑅) · 𝑤))
32	24	oveq2d 7424	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ((𝑄 · 𝑤) + (𝑟 · 𝑤)) = ((𝑄 · 𝑤) + (𝑅 · 𝑤)))
33	31, 32	eqeq12d 2776	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤)) ↔ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))))
34	25, 29, 33	3anbi123d 1464	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ↔ ((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤)))))
35		oveq2 7416	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (𝑄 × 𝑟) = (𝑄 × 𝑅))
36	35	oveq1d 7423	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ((𝑄 × 𝑟) · 𝑤) = ((𝑄 × 𝑅) · 𝑤))
37	24	oveq2d 7424	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (𝑄 · (𝑟 · 𝑤)) = (𝑄 · (𝑅 · 𝑤)))
38	36, 37	eqeq12d 2776	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ↔ ((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤))))
39	38	anbi1d 643	. . . . . . 7 ⊢ (𝑟 = 𝑅 → ((((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤) ↔ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
40	34, 39	anbi12d 644	. . . . . 6 ⊢ (𝑟 = 𝑅 → ((((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
41	40	2ralbidv 3226	. . . . 5 ⊢ (𝑟 = 𝑅 → (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
42	23, 41	rspc2v 3586	. . . 4 ⊢ ((𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) → (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) → ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
43	10, 42	mpan9 516	. . 3 ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) → ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
44		oveq2 7416	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (𝑤 + 𝑥) = (𝑤 + 𝑋))
45	44	oveq2d 7424	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝑅 · (𝑤 + 𝑥)) = (𝑅 · (𝑤 + 𝑋)))
46		oveq2 7416	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (𝑅 · 𝑥) = (𝑅 · 𝑋))
47	46	oveq2d 7424	. . . . . . 7 ⊢ (𝑥 = 𝑋 → ((𝑅 · 𝑤) + (𝑅 · 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)))
48	45, 47	eqeq12d 2776	. . . . . 6 ⊢ (𝑥 = 𝑋 → ((𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ↔ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋))))
49	48	3anbi2d 1469	. . . . 5 ⊢ (𝑥 = 𝑋 → (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ↔ ((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤)))))
50	49	anbi1d 643	. . . 4 ⊢ (𝑥 = 𝑋 → ((((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
51		oveq2 7416	. . . . . . 7 ⊢ (𝑤 = 𝑌 → (𝑅 · 𝑤) = (𝑅 · 𝑌))
52	51	eleq1d 2845	. . . . . 6 ⊢ (𝑤 = 𝑌 → ((𝑅 · 𝑤) ∈ 𝑉 ↔ (𝑅 · 𝑌) ∈ 𝑉))
53		oveq1 7415	. . . . . . . 8 ⊢ (𝑤 = 𝑌 → (𝑤 + 𝑋) = (𝑌 + 𝑋))
54	53	oveq2d 7424	. . . . . . 7 ⊢ (𝑤 = 𝑌 → (𝑅 · (𝑤 + 𝑋)) = (𝑅 · (𝑌 + 𝑋)))
55	51	oveq1d 7423	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ((𝑅 · 𝑤) + (𝑅 · 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)))
56	54, 55	eqeq12d 2776	. . . . . 6 ⊢ (𝑤 = 𝑌 → ((𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ↔ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋))))
57		oveq2 7416	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 ⨣ 𝑅) · 𝑌))
58		oveq2 7416	. . . . . . . 8 ⊢ (𝑤 = 𝑌 → (𝑄 · 𝑤) = (𝑄 · 𝑌))
59	58, 51	oveq12d 7426	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ((𝑄 · 𝑤) + (𝑅 · 𝑤)) = ((𝑄 · 𝑌) + (𝑅 · 𝑌)))
60	57, 59	eqeq12d 2776	. . . . . 6 ⊢ (𝑤 = 𝑌 → (((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤)) ↔ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))))
61	52, 56, 60	3anbi123d 1464	. . . . 5 ⊢ (𝑤 = 𝑌 → (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ↔ ((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌)))))
62		oveq2 7416	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ((𝑄 × 𝑅) · 𝑤) = ((𝑄 × 𝑅) · 𝑌))
63	51	oveq2d 7424	. . . . . . 7 ⊢ (𝑤 = 𝑌 → (𝑄 · (𝑅 · 𝑤)) = (𝑄 · (𝑅 · 𝑌)))
64	62, 63	eqeq12d 2776	. . . . . 6 ⊢ (𝑤 = 𝑌 → (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ↔ ((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌))))
65		oveq2 7416	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ( 1 · 𝑤) = ( 1 · 𝑌))
66		id 23	. . . . . . 7 ⊢ (𝑤 = 𝑌 → 𝑤 = 𝑌)
67	65, 66	eqeq12d 2776	. . . . . 6 ⊢ (𝑤 = 𝑌 → (( 1 · 𝑤) = 𝑤 ↔ ( 1 · 𝑌) = 𝑌))
68	64, 67	anbi12d 644	. . . . 5 ⊢ (𝑤 = 𝑌 → ((((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤) ↔ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌)))
69	61, 68	anbi12d 644	. . . 4 ⊢ (𝑤 = 𝑌 → ((((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌))))
70	50, 69	rspc2v 3586	. . 3 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) → (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌))))
71	43, 70	syl5com 32	. 2 ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌))))
72	71	3impia 1135	1 ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ∀wral 3076 ‘cfv 6527 (class class class)co 7408 Basecbs 17349 +_gcplusg 17390 ._rcmulr 17391 Scalarcsca 17393 ·_𝑠 cvsca 17394 Grpcgrp 19106 1_rcur 20369 Ringcrg 20421 LModclmod 21097

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-ext 2732 ax-nul 5259

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-sb 2100 df-clab 2739 df-cleq 2752 df-clel 2835 df-ne 2956 df-ral 3077 df-rab 3413 df-v 3452 df-sbc 3739 df-dif 3901 df-un 3903 df-ss 3915 df-nul 4279 df-if 4482 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-br 5103 df-iota 6483 df-fv 6535 df-ov 7411 df-lmod 21099

This theorem is used by: lmodvscl 21115 lmodvsdi 21122 lmodvsdir 21123 lmodvsass 21124 lmodvs1 21127

W3C validator