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 𝐹 ) ∈ 𝐵 )