Metamath Proof Explorer


Theorem gsummulg

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 ( 𝑘𝐴𝑋 ) ) ) )