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 19904

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 19903	. . . . 5 ⊢ (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
10	9	simp3bi 1149	. . . 4 ⊢ (𝑊 ∈ LMod → ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
11		oveq1 7220	. . . . . . . . . 10 ⊢ (𝑞 = 𝑄 → (𝑞 ⨣ 𝑟) = (𝑄 ⨣ 𝑟))
12	11	oveq1d 7228	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑄 ⨣ 𝑟) · 𝑤))
13		oveq1 7220	. . . . . . . . . 10 ⊢ (𝑞 = 𝑄 → (𝑞 · 𝑤) = (𝑄 · 𝑤))
14	13	oveq1d 7228	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → ((𝑞 · 𝑤) + (𝑟 · 𝑤)) = ((𝑄 · 𝑤) + (𝑟 · 𝑤)))
15	12, 14	eqeq12d 2753	. . . . . . . 8 ⊢ (𝑞 = 𝑄 → (((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤)) ↔ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))))
16	15	3anbi3d 1444	. . . . . . 7 ⊢ (𝑞 = 𝑄 → (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ↔ ((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤)))))
17		oveq1 7220	. . . . . . . . . 10 ⊢ (𝑞 = 𝑄 → (𝑞 × 𝑟) = (𝑄 × 𝑟))
18	17	oveq1d 7228	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → ((𝑞 × 𝑟) · 𝑤) = ((𝑄 × 𝑟) · 𝑤))
19		oveq1 7220	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → (𝑞 · (𝑟 · 𝑤)) = (𝑄 · (𝑟 · 𝑤)))
20	18, 19	eqeq12d 2753	. . . . . . . 8 ⊢ (𝑞 = 𝑄 → (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ↔ ((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤))))
21	20	anbi1d 633	. . . . . . 7 ⊢ (𝑞 = 𝑄 → ((((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤) ↔ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
22	16, 21	anbi12d 634	. . . . . 6 ⊢ (𝑞 = 𝑄 → ((((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
23	22	2ralbidv 3120	. . . . 5 ⊢ (𝑞 = 𝑄 → (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
24		oveq1 7220	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (𝑟 · 𝑤) = (𝑅 · 𝑤))
25	24	eleq1d 2822	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ((𝑟 · 𝑤) ∈ 𝑉 ↔ (𝑅 · 𝑤) ∈ 𝑉))
26		oveq1 7220	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (𝑟 · (𝑤 + 𝑥)) = (𝑅 · (𝑤 + 𝑥)))
27		oveq1 7220	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (𝑟 · 𝑥) = (𝑅 · 𝑥))
28	24, 27	oveq12d 7231	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ((𝑟 · 𝑤) + (𝑟 · 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)))
29	26, 28	eqeq12d 2753	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ((𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ↔ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥))))
30		oveq2 7221	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (𝑄 ⨣ 𝑟) = (𝑄 ⨣ 𝑅))
31	30	oveq1d 7228	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 ⨣ 𝑅) · 𝑤))
32	24	oveq2d 7229	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ((𝑄 · 𝑤) + (𝑟 · 𝑤)) = ((𝑄 · 𝑤) + (𝑅 · 𝑤)))
33	31, 32	eqeq12d 2753	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤)) ↔ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))))
34	25, 29, 33	3anbi123d 1438	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ↔ ((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤)))))
35		oveq2 7221	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (𝑄 × 𝑟) = (𝑄 × 𝑅))
36	35	oveq1d 7228	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ((𝑄 × 𝑟) · 𝑤) = ((𝑄 × 𝑅) · 𝑤))
37	24	oveq2d 7229	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (𝑄 · (𝑟 · 𝑤)) = (𝑄 · (𝑅 · 𝑤)))
38	36, 37	eqeq12d 2753	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ↔ ((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤))))
39	38	anbi1d 633	. . . . . . 7 ⊢ (𝑟 = 𝑅 → ((((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤) ↔ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
40	34, 39	anbi12d 634	. . . . . 6 ⊢ (𝑟 = 𝑅 → ((((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
41	40	2ralbidv 3120	. . . . 5 ⊢ (𝑟 = 𝑅 → (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
42	23, 41	rspc2v 3547	. . . 4 ⊢ ((𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) → (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) → ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
43	10, 42	mpan9 510	. . 3 ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) → ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
44		oveq2 7221	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (𝑤 + 𝑥) = (𝑤 + 𝑋))
45	44	oveq2d 7229	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝑅 · (𝑤 + 𝑥)) = (𝑅 · (𝑤 + 𝑋)))
46		oveq2 7221	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (𝑅 · 𝑥) = (𝑅 · 𝑋))
47	46	oveq2d 7229	. . . . . . 7 ⊢ (𝑥 = 𝑋 → ((𝑅 · 𝑤) + (𝑅 · 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)))
48	45, 47	eqeq12d 2753	. . . . . 6 ⊢ (𝑥 = 𝑋 → ((𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ↔ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋))))
49	48	3anbi2d 1443	. . . . 5 ⊢ (𝑥 = 𝑋 → (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ↔ ((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤)))))
50	49	anbi1d 633	. . . 4 ⊢ (𝑥 = 𝑋 → ((((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
51		oveq2 7221	. . . . . . 7 ⊢ (𝑤 = 𝑌 → (𝑅 · 𝑤) = (𝑅 · 𝑌))
52	51	eleq1d 2822	. . . . . 6 ⊢ (𝑤 = 𝑌 → ((𝑅 · 𝑤) ∈ 𝑉 ↔ (𝑅 · 𝑌) ∈ 𝑉))
53		oveq1 7220	. . . . . . . 8 ⊢ (𝑤 = 𝑌 → (𝑤 + 𝑋) = (𝑌 + 𝑋))
54	53	oveq2d 7229	. . . . . . 7 ⊢ (𝑤 = 𝑌 → (𝑅 · (𝑤 + 𝑋)) = (𝑅 · (𝑌 + 𝑋)))
55	51	oveq1d 7228	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ((𝑅 · 𝑤) + (𝑅 · 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)))
56	54, 55	eqeq12d 2753	. . . . . 6 ⊢ (𝑤 = 𝑌 → ((𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ↔ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋))))
57		oveq2 7221	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 ⨣ 𝑅) · 𝑌))
58		oveq2 7221	. . . . . . . 8 ⊢ (𝑤 = 𝑌 → (𝑄 · 𝑤) = (𝑄 · 𝑌))
59	58, 51	oveq12d 7231	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ((𝑄 · 𝑤) + (𝑅 · 𝑤)) = ((𝑄 · 𝑌) + (𝑅 · 𝑌)))
60	57, 59	eqeq12d 2753	. . . . . 6 ⊢ (𝑤 = 𝑌 → (((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤)) ↔ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))))
61	52, 56, 60	3anbi123d 1438	. . . . 5 ⊢ (𝑤 = 𝑌 → (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ↔ ((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌)))))
62		oveq2 7221	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ((𝑄 × 𝑅) · 𝑤) = ((𝑄 × 𝑅) · 𝑌))
63	51	oveq2d 7229	. . . . . . 7 ⊢ (𝑤 = 𝑌 → (𝑄 · (𝑅 · 𝑤)) = (𝑄 · (𝑅 · 𝑌)))
64	62, 63	eqeq12d 2753	. . . . . 6 ⊢ (𝑤 = 𝑌 → (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ↔ ((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌))))
65		oveq2 7221	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ( 1 · 𝑤) = ( 1 · 𝑌))
66		id 22	. . . . . . 7 ⊢ (𝑤 = 𝑌 → 𝑤 = 𝑌)
67	65, 66	eqeq12d 2753	. . . . . 6 ⊢ (𝑤 = 𝑌 → (( 1 · 𝑤) = 𝑤 ↔ ( 1 · 𝑌) = 𝑌))
68	64, 67	anbi12d 634	. . . . 5 ⊢ (𝑤 = 𝑌 → ((((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤) ↔ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌)))
69	61, 68	anbi12d 634	. . . 4 ⊢ (𝑤 = 𝑌 → ((((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌))))
70	50, 69	rspc2v 3547	. . 3 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) → (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌))))
71	43, 70	syl5com 31	. 2 ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌))))
72	71	3impia 1119	1 ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 = wceq 1543 ∈ wcel 2110 ∀wral 3061 ‘cfv 6380 (class class class)co 7213 Basecbs 16760 +_gcplusg 16802 ._rcmulr 16803 Scalarcsca 16805 ·_𝑠 cvsca 16806 Grpcgrp 18365 1_rcur 19516 Ringcrg 19562 LModclmod 19899

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-nul 5199

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3410 df-sbc 3695 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 df-nul 4238 df-if 4440 df-sn 4542 df-pr 4544 df-op 4548 df-uni 4820 df-br 5054 df-iota 6338 df-fv 6388 df-ov 7216 df-lmod 19901

This theorem is referenced by: lmodvscl 19916 lmodvsdi 19922 lmodvsdir 19923 lmodvsass 19924 lmodvs1 19927

W3C validator