Metamath Proof Explorer


Theorem gsumzcl

Description: Closure of a finite group sum. (Contributed by Mario Carneiro, 24-Apr-2016) (Revised by AV, 1-Jun-2019)

Ref Expression
Hypotheses gsumzcl.b 𝐵 = ( Base ‘ 𝐺 )
gsumzcl.0 0 = ( 0g𝐺 )
gsumzcl.z 𝑍 = ( Cntz ‘ 𝐺 )
gsumzcl.g ( 𝜑𝐺 ∈ Mnd )
gsumzcl.a ( 𝜑𝐴𝑉 )
gsumzcl.f ( 𝜑𝐹 : 𝐴𝐵 )
gsumzcl.c ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
gsumzcl.w ( 𝜑𝐹 finSupp 0 )
Assertion gsumzcl ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 gsumzcl.b 𝐵 = ( Base ‘ 𝐺 )
2 gsumzcl.0 0 = ( 0g𝐺 )
3 gsumzcl.z 𝑍 = ( Cntz ‘ 𝐺 )
4 gsumzcl.g ( 𝜑𝐺 ∈ Mnd )
5 gsumzcl.a ( 𝜑𝐴𝑉 )
6 gsumzcl.f ( 𝜑𝐹 : 𝐴𝐵 )
7 gsumzcl.c ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
8 gsumzcl.w ( 𝜑𝐹 finSupp 0 )
9 8 fsuppimpd ( 𝜑 → ( 𝐹 supp 0 ) ∈ Fin )
10 1 2 3 4 5 6 7 9 gsumzcl2 ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ 𝐵 )