This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gsumcl

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

	Ref	Expression
Hypotheses	gsumcl.b	$⊢ B = {Base}_{G}$
	gsumcl.z	$⊢ \underset{˙}{0} = 0_{G}$
	gsumcl.g	$⊢ φ \to G \in CMnd$
	gsumcl.a	$⊢ φ \to A \in V$
	gsumcl.f	$⊢ φ \to F : A ⟶ B$
	gsumcl.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
Assertion	gsumcl	$⊢ φ \to \sum_{G} F \in B$

Proof

Step	Hyp	Ref	Expression
1		gsumcl.b	$⊢ B = {Base}_{G}$
2		gsumcl.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsumcl.g	$⊢ φ \to G \in CMnd$
4		gsumcl.a	$⊢ φ \to A \in V$
5		gsumcl.f	$⊢ φ \to F : A ⟶ B$
6		gsumcl.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
7	6	fsuppimpd	$⊢ φ \to F supp \underset{˙}{0} \in Fin$
8	1 2 3 4 5 7	gsumcl2	$⊢ φ \to \sum_{G} F \in B$