lmodlema - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > lmodlema		GIF version

Theorem lmodlema 14139

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 14138	. . . . 5 ⊢ (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
10	9	simp3bi 1017	. . . 4 ⊢ (𝑊 ∈ LMod → ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
11		oveq1 5969	. . . . . . . . . 10 ⊢ (𝑞 = 𝑄 → (𝑞 ⨣ 𝑟) = (𝑄 ⨣ 𝑟))
12	11	oveq1d 5977	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑄 ⨣ 𝑟) · 𝑤))
13		oveq1 5969	. . . . . . . . . 10 ⊢ (𝑞 = 𝑄 → (𝑞 · 𝑤) = (𝑄 · 𝑤))
14	13	oveq1d 5977	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → ((𝑞 · 𝑤) + (𝑟 · 𝑤)) = ((𝑄 · 𝑤) + (𝑟 · 𝑤)))
15	12, 14	eqeq12d 2221	. . . . . . . 8 ⊢ (𝑞 = 𝑄 → (((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤)) ↔ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))))
16	15	3anbi3d 1331	. . . . . . 7 ⊢ (𝑞 = 𝑄 → (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ↔ ((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤)))))
17		oveq1 5969	. . . . . . . . . 10 ⊢ (𝑞 = 𝑄 → (𝑞 × 𝑟) = (𝑄 × 𝑟))
18	17	oveq1d 5977	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → ((𝑞 × 𝑟) · 𝑤) = ((𝑄 × 𝑟) · 𝑤))
19		oveq1 5969	. . . . . . . . 9 ⊢ (𝑞 = 𝑄 → (𝑞 · (𝑟 · 𝑤)) = (𝑄 · (𝑟 · 𝑤)))
20	18, 19	eqeq12d 2221	. . . . . . . 8 ⊢ (𝑞 = 𝑄 → (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ↔ ((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤))))
21	20	anbi1d 465	. . . . . . 7 ⊢ (𝑞 = 𝑄 → ((((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤) ↔ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
22	16, 21	anbi12d 473	. . . . . 6 ⊢ (𝑞 = 𝑄 → ((((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
23	22	2ralbidv 2531	. . . . 5 ⊢ (𝑞 = 𝑄 → (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
24		oveq1 5969	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (𝑟 · 𝑤) = (𝑅 · 𝑤))
25	24	eleq1d 2275	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ((𝑟 · 𝑤) ∈ 𝑉 ↔ (𝑅 · 𝑤) ∈ 𝑉))
26		oveq1 5969	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (𝑟 · (𝑤 + 𝑥)) = (𝑅 · (𝑤 + 𝑥)))
27		oveq1 5969	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (𝑟 · 𝑥) = (𝑅 · 𝑥))
28	24, 27	oveq12d 5980	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ((𝑟 · 𝑤) + (𝑟 · 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)))
29	26, 28	eqeq12d 2221	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ((𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ↔ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥))))
30		oveq2 5970	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (𝑄 ⨣ 𝑟) = (𝑄 ⨣ 𝑅))
31	30	oveq1d 5977	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 ⨣ 𝑅) · 𝑤))
32	24	oveq2d 5978	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ((𝑄 · 𝑤) + (𝑟 · 𝑤)) = ((𝑄 · 𝑤) + (𝑅 · 𝑤)))
33	31, 32	eqeq12d 2221	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤)) ↔ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))))
34	25, 29, 33	3anbi123d 1325	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ↔ ((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤)))))
35		oveq2 5970	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (𝑄 × 𝑟) = (𝑄 × 𝑅))
36	35	oveq1d 5977	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ((𝑄 × 𝑟) · 𝑤) = ((𝑄 × 𝑅) · 𝑤))
37	24	oveq2d 5978	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (𝑄 · (𝑟 · 𝑤)) = (𝑄 · (𝑅 · 𝑤)))
38	36, 37	eqeq12d 2221	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ↔ ((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤))))
39	38	anbi1d 465	. . . . . . 7 ⊢ (𝑟 = 𝑅 → ((((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤) ↔ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
40	34, 39	anbi12d 473	. . . . . 6 ⊢ (𝑟 = 𝑅 → ((((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
41	40	2ralbidv 2531	. . . . 5 ⊢ (𝑟 = 𝑅 → (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑄 ⨣ 𝑟) · 𝑤) = ((𝑄 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑄 × 𝑟) · 𝑤) = (𝑄 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
42	23, 41	rspc2v 2894	. . . 4 ⊢ ((𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) → (∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) → ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
43	10, 42	mpan9 281	. . 3 ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) → ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
44		oveq2 5970	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (𝑤 + 𝑥) = (𝑤 + 𝑋))
45	44	oveq2d 5978	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝑅 · (𝑤 + 𝑥)) = (𝑅 · (𝑤 + 𝑋)))
46		oveq2 5970	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (𝑅 · 𝑥) = (𝑅 · 𝑋))
47	46	oveq2d 5978	. . . . . . 7 ⊢ (𝑥 = 𝑋 → ((𝑅 · 𝑤) + (𝑅 · 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)))
48	45, 47	eqeq12d 2221	. . . . . 6 ⊢ (𝑥 = 𝑋 → ((𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ↔ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋))))
49	48	3anbi2d 1330	. . . . 5 ⊢ (𝑥 = 𝑋 → (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ↔ ((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤)))))
50	49	anbi1d 465	. . . 4 ⊢ (𝑥 = 𝑋 → ((((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
51		oveq2 5970	. . . . . . 7 ⊢ (𝑤 = 𝑌 → (𝑅 · 𝑤) = (𝑅 · 𝑌))
52	51	eleq1d 2275	. . . . . 6 ⊢ (𝑤 = 𝑌 → ((𝑅 · 𝑤) ∈ 𝑉 ↔ (𝑅 · 𝑌) ∈ 𝑉))
53		oveq1 5969	. . . . . . . 8 ⊢ (𝑤 = 𝑌 → (𝑤 + 𝑋) = (𝑌 + 𝑋))
54	53	oveq2d 5978	. . . . . . 7 ⊢ (𝑤 = 𝑌 → (𝑅 · (𝑤 + 𝑋)) = (𝑅 · (𝑌 + 𝑋)))
55	51	oveq1d 5977	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ((𝑅 · 𝑤) + (𝑅 · 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)))
56	54, 55	eqeq12d 2221	. . . . . 6 ⊢ (𝑤 = 𝑌 → ((𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ↔ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋))))
57		oveq2 5970	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 ⨣ 𝑅) · 𝑌))
58		oveq2 5970	. . . . . . . 8 ⊢ (𝑤 = 𝑌 → (𝑄 · 𝑤) = (𝑄 · 𝑌))
59	58, 51	oveq12d 5980	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ((𝑄 · 𝑤) + (𝑅 · 𝑤)) = ((𝑄 · 𝑌) + (𝑅 · 𝑌)))
60	57, 59	eqeq12d 2221	. . . . . 6 ⊢ (𝑤 = 𝑌 → (((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤)) ↔ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))))
61	52, 56, 60	3anbi123d 1325	. . . . 5 ⊢ (𝑤 = 𝑌 → (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ↔ ((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌)))))
62		oveq2 5970	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ((𝑄 × 𝑅) · 𝑤) = ((𝑄 × 𝑅) · 𝑌))
63	51	oveq2d 5978	. . . . . . 7 ⊢ (𝑤 = 𝑌 → (𝑄 · (𝑅 · 𝑤)) = (𝑄 · (𝑅 · 𝑌)))
64	62, 63	eqeq12d 2221	. . . . . 6 ⊢ (𝑤 = 𝑌 → (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ↔ ((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌))))
65		oveq2 5970	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ( 1 · 𝑤) = ( 1 · 𝑌))
66		id 19	. . . . . . 7 ⊢ (𝑤 = 𝑌 → 𝑤 = 𝑌)
67	65, 66	eqeq12d 2221	. . . . . 6 ⊢ (𝑤 = 𝑌 → (( 1 · 𝑤) = 𝑤 ↔ ( 1 · 𝑌) = 𝑌))
68	64, 67	anbi12d 473	. . . . 5 ⊢ (𝑤 = 𝑌 → ((((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤) ↔ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌)))
69	61, 68	anbi12d 473	. . . 4 ⊢ (𝑤 = 𝑌 → ((((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑋)) = ((𝑅 · 𝑤) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) ↔ (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌))))
70	50, 69	rspc2v 2894	. . 3 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑅 · 𝑤) ∈ 𝑉 ∧ (𝑅 · (𝑤 + 𝑥)) = ((𝑅 · 𝑤) + (𝑅 · 𝑥)) ∧ ((𝑄 ⨣ 𝑅) · 𝑤) = ((𝑄 · 𝑤) + (𝑅 · 𝑤))) ∧ (((𝑄 × 𝑅) · 𝑤) = (𝑄 · (𝑅 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)) → (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌))))
71	43, 70	syl5com 29	. 2 ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌))))
72	71	3impia 1203	1 ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 981 = wceq 1373 ∈ wcel 2177 ∀wral 2485 ‘cfv 5285 (class class class)co 5962 Basecbs 12917 +_gcplusg 12994 ._rcmulr 12995 Scalarcsca 12997 ·_𝑠 cvsca 12998 Grpcgrp 13417 1_rcur 13806 Ringcrg 13843 LModclmod 14134

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-sep 4173 ax-pow 4229 ax-pr 4264 ax-un 4493 ax-cnex 8046 ax-resscn 8047 ax-1re 8049 ax-addrcl 8052

This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ral 2490 df-rex 2491 df-rab 2494 df-v 2775 df-sbc 3003 df-un 3174 df-in 3176 df-ss 3183 df-pw 3623 df-sn 3644 df-pr 3645 df-op 3647 df-uni 3860 df-int 3895 df-br 4055 df-opab 4117 df-mpt 4118 df-id 4353 df-xp 4694 df-rel 4695 df-cnv 4696 df-co 4697 df-dm 4698 df-rn 4699 df-res 4700 df-iota 5246 df-fun 5287 df-fn 5288 df-fv 5293 df-ov 5965 df-inn 9067 df-2 9125 df-3 9126 df-4 9127 df-5 9128 df-6 9129 df-ndx 12920 df-slot 12921 df-base 12923 df-plusg 13007 df-mulr 13008 df-sca 13010 df-vsca 13011 df-lmod 14136

This theorem is referenced by: lmodvscl 14152 lmodvsdi 14158 lmodvsdir 14159 lmodvsass 14160 lmodvs1 14163

W3C validator