Metamath Proof Explorer

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 · 𝑌 ) = 𝑌 ) ) )