This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem slmdlema

Description: Lemma for properties of a semimodule. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014) (Revised by Thierry Arnoux, 1-Apr-2018)

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

Proof

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