Database
BASIC ALGEBRAIC STRUCTURES
Groups
Abelian groups
Group sum operation
gsummulg
Metamath Proof Explorer
Description: Nonnegative multiple of a group sum. (Contributed by Mario Carneiro , 15-Dec-2014) (Revised by Mario Carneiro , 7-Jan-2015) (Revised by AV , 6-Jun-2019)
Ref
Expression
Hypotheses
gsummulg.b
⊢ 𝐵 = ( Base ‘ 𝐺 )
gsummulg.z
⊢ 0 = ( 0g ‘ 𝐺 )
gsummulg.t
⊢ · = ( .g ‘ 𝐺 )
gsummulg.a
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsummulg.f
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
gsummulg.w
⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) finSupp 0 )
gsummulg.g
⊢ ( 𝜑 → 𝐺 ∈ CMnd )
gsummulg.n
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion
gsummulg
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝑁 · 𝑋 ) ) ) = ( 𝑁 · ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) ) )
Proof
Step
Hyp
Ref
Expression
1
gsummulg.b
⊢ 𝐵 = ( Base ‘ 𝐺 )
2
gsummulg.z
⊢ 0 = ( 0g ‘ 𝐺 )
3
gsummulg.t
⊢ · = ( .g ‘ 𝐺 )
4
gsummulg.a
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5
gsummulg.f
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
6
gsummulg.w
⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) finSupp 0 )
7
gsummulg.g
⊢ ( 𝜑 → 𝐺 ∈ CMnd )
8
gsummulg.n
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
9
8
nn0zd
⊢ ( 𝜑 → 𝑁 ∈ ℤ )
10
8
olcd
⊢ ( 𝜑 → ( 𝐺 ∈ Abel ∨ 𝑁 ∈ ℕ0 ) )
11
1 2 3 4 5 6 7 9 10
gsummulglem
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝑁 · 𝑋 ) ) ) = ( 𝑁 · ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) ) )