Step |
Hyp |
Ref |
Expression |
1 |
|
slmdvsdi.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
2 |
|
slmdvsdi.a |
⊢ + = ( +g ‘ 𝑊 ) |
3 |
|
slmdvsdi.f |
⊢ 𝐹 = ( Scalar ‘ 𝑊 ) |
4 |
|
slmdvsdi.s |
⊢ · = ( ·𝑠 ‘ 𝑊 ) |
5 |
|
slmdvsdi.k |
⊢ 𝐾 = ( Base ‘ 𝐹 ) |
6 |
|
eqid |
⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 ) |
7 |
|
eqid |
⊢ ( +g ‘ 𝐹 ) = ( +g ‘ 𝐹 ) |
8 |
|
eqid |
⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 ) |
9 |
|
eqid |
⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 ) |
10 |
|
eqid |
⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 ) |
11 |
1 2 4 6 3 5 7 8 9 10
|
slmdlema |
⊢ ( ( 𝑊 ∈ SLMod ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( ( 𝑅 · 𝑋 ) ∈ 𝑉 ∧ ( 𝑅 · ( 𝑋 + 𝑌 ) ) = ( ( 𝑅 · 𝑋 ) + ( 𝑅 · 𝑌 ) ) ∧ ( ( 𝑅 ( +g ‘ 𝐹 ) 𝑅 ) · 𝑋 ) = ( ( 𝑅 · 𝑋 ) + ( 𝑅 · 𝑋 ) ) ) ∧ ( ( ( 𝑅 ( .r ‘ 𝐹 ) 𝑅 ) · 𝑋 ) = ( 𝑅 · ( 𝑅 · 𝑋 ) ) ∧ ( ( 1r ‘ 𝐹 ) · 𝑋 ) = 𝑋 ∧ ( ( 0g ‘ 𝐹 ) · 𝑋 ) = ( 0g ‘ 𝑊 ) ) ) ) |
12 |
11
|
simpld |
⊢ ( ( 𝑊 ∈ SLMod ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑅 · 𝑋 ) ∈ 𝑉 ∧ ( 𝑅 · ( 𝑋 + 𝑌 ) ) = ( ( 𝑅 · 𝑋 ) + ( 𝑅 · 𝑌 ) ) ∧ ( ( 𝑅 ( +g ‘ 𝐹 ) 𝑅 ) · 𝑋 ) = ( ( 𝑅 · 𝑋 ) + ( 𝑅 · 𝑋 ) ) ) ) |
13 |
12
|
simp2d |
⊢ ( ( 𝑊 ∈ SLMod ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑅 · ( 𝑋 + 𝑌 ) ) = ( ( 𝑅 · 𝑋 ) + ( 𝑅 · 𝑌 ) ) ) |
14 |
13
|
3expia |
⊢ ( ( 𝑊 ∈ SLMod ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ) ) → ( ( 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑅 · ( 𝑋 + 𝑌 ) ) = ( ( 𝑅 · 𝑋 ) + ( 𝑅 · 𝑌 ) ) ) ) |
15 |
14
|
anabsan2 |
⊢ ( ( 𝑊 ∈ SLMod ∧ 𝑅 ∈ 𝐾 ) → ( ( 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑅 · ( 𝑋 + 𝑌 ) ) = ( ( 𝑅 · 𝑋 ) + ( 𝑅 · 𝑌 ) ) ) ) |
16 |
15
|
exp4b |
⊢ ( 𝑊 ∈ SLMod → ( 𝑅 ∈ 𝐾 → ( 𝑌 ∈ 𝑉 → ( 𝑋 ∈ 𝑉 → ( 𝑅 · ( 𝑋 + 𝑌 ) ) = ( ( 𝑅 · 𝑋 ) + ( 𝑅 · 𝑌 ) ) ) ) ) ) |
17 |
16
|
com34 |
⊢ ( 𝑊 ∈ SLMod → ( 𝑅 ∈ 𝐾 → ( 𝑋 ∈ 𝑉 → ( 𝑌 ∈ 𝑉 → ( 𝑅 · ( 𝑋 + 𝑌 ) ) = ( ( 𝑅 · 𝑋 ) + ( 𝑅 · 𝑌 ) ) ) ) ) ) |
18 |
17
|
3imp2 |
⊢ ( ( 𝑊 ∈ SLMod ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑅 · ( 𝑋 + 𝑌 ) ) = ( ( 𝑅 · 𝑋 ) + ( 𝑅 · 𝑌 ) ) ) |