Theorem lmodlema

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

	Ref	Expression
Hypotheses	islmod.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	islmod.a	⊢ + = ( +g ‘ 𝑊 )
	islmod.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	islmod.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	islmod.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	islmod.p	⊢ ⨣ = ( +g ‘ 𝐹 )
	islmod.t	⊢ × = ( .r ‘ 𝐹 )
	islmod.u	⊢ 1 = ( 1r ‘ 𝐹 )
Assertion	lmodlema	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 𝑅 · 𝑌 ) ∈ 𝑉 ∧ ( 𝑅 · ( 𝑌 + 𝑋 ) ) = ( ( 𝑅 · 𝑌 ) + ( 𝑅 · 𝑋 ) ) ∧ ( ( 𝑄 ⨣ 𝑅 ) · 𝑌 ) = ( ( 𝑄 · 𝑌 ) + ( 𝑅 · 𝑌 ) ) ) ∧ ( ( ( 𝑄 × 𝑅 ) · 𝑌 ) = ( 𝑄 · ( 𝑅 · 𝑌 ) ) ∧ ( 1 · 𝑌 ) = 𝑌 ) ) )

Proof

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