Step |
Hyp |
Ref |
Expression |
1 |
|
slmdvsass.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
2 |
|
slmdvsass.f |
⊢ 𝐹 = ( Scalar ‘ 𝑊 ) |
3 |
|
slmdvsass.s |
⊢ · = ( ·𝑠 ‘ 𝑊 ) |
4 |
|
slmdvsass.k |
⊢ 𝐾 = ( Base ‘ 𝐹 ) |
5 |
|
slmdvsass.t |
⊢ × = ( .r ‘ 𝐹 ) |
6 |
|
eqid |
⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 ) |
7 |
|
eqid |
⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 ) |
8 |
|
eqid |
⊢ ( +g ‘ 𝐹 ) = ( +g ‘ 𝐹 ) |
9 |
|
eqid |
⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 ) |
10 |
|
eqid |
⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 ) |
11 |
1 6 3 7 2 4 8 5 9 10
|
slmdlema |
⊢ ( ( 𝑊 ∈ SLMod ∧ ( 𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( ( 𝑅 · 𝑋 ) ∈ 𝑉 ∧ ( 𝑅 · ( 𝑋 ( +g ‘ 𝑊 ) 𝑋 ) ) = ( ( 𝑅 · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑅 · 𝑋 ) ) ∧ ( ( 𝑄 ( +g ‘ 𝐹 ) 𝑅 ) · 𝑋 ) = ( ( 𝑄 · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑅 · 𝑋 ) ) ) ∧ ( ( ( 𝑄 × 𝑅 ) · 𝑋 ) = ( 𝑄 · ( 𝑅 · 𝑋 ) ) ∧ ( ( 1r ‘ 𝐹 ) · 𝑋 ) = 𝑋 ∧ ( ( 0g ‘ 𝐹 ) · 𝑋 ) = ( 0g ‘ 𝑊 ) ) ) ) |
12 |
11
|
simprd |
⊢ ( ( 𝑊 ∈ SLMod ∧ ( 𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( ( 𝑄 × 𝑅 ) · 𝑋 ) = ( 𝑄 · ( 𝑅 · 𝑋 ) ) ∧ ( ( 1r ‘ 𝐹 ) · 𝑋 ) = 𝑋 ∧ ( ( 0g ‘ 𝐹 ) · 𝑋 ) = ( 0g ‘ 𝑊 ) ) ) |
13 |
12
|
simp1d |
⊢ ( ( 𝑊 ∈ SLMod ∧ ( 𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑄 × 𝑅 ) · 𝑋 ) = ( 𝑄 · ( 𝑅 · 𝑋 ) ) ) |
14 |
13
|
3expa |
⊢ ( ( ( 𝑊 ∈ SLMod ∧ ( 𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑄 × 𝑅 ) · 𝑋 ) = ( 𝑄 · ( 𝑅 · 𝑋 ) ) ) |
15 |
14
|
anabsan2 |
⊢ ( ( ( 𝑊 ∈ SLMod ∧ ( 𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑄 × 𝑅 ) · 𝑋 ) = ( 𝑄 · ( 𝑅 · 𝑋 ) ) ) |
16 |
15
|
exp42 |
⊢ ( 𝑊 ∈ SLMod → ( 𝑄 ∈ 𝐾 → ( 𝑅 ∈ 𝐾 → ( 𝑋 ∈ 𝑉 → ( ( 𝑄 × 𝑅 ) · 𝑋 ) = ( 𝑄 · ( 𝑅 · 𝑋 ) ) ) ) ) ) |
17 |
16
|
3imp2 |
⊢ ( ( 𝑊 ∈ SLMod ∧ ( 𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑄 × 𝑅 ) · 𝑋 ) = ( 𝑄 · ( 𝑅 · 𝑋 ) ) ) |