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	\|- .0. = ( 0g ` G )
	gsumcl.g	\|- ( ph -> G e. CMnd )
	gsumcl.a	\|- ( ph -> A e. V )
	gsumcl.f	\|- ( ph -> F : A --> B )
	gsumcl.w	\|- ( ph -> F finSupp .0. )
Assertion	gsumcl	\|- ( ph -> ( G gsum F ) e. B )

Proof

Step	Hyp	Ref	Expression
1		gsumcl.b	\|- B = ( Base ` G )
2		gsumcl.z	\|- .0. = ( 0g ` G )
3		gsumcl.g	\|- ( ph -> G e. CMnd )
4		gsumcl.a	\|- ( ph -> A e. V )
5		gsumcl.f	\|- ( ph -> F : A --> B )
6		gsumcl.w	\|- ( ph -> F finSupp .0. )
7	6	fsuppimpd	\|- ( ph -> ( F supp .0. ) e. Fin )
8	1 2 3 4 5 7	gsumcl2	\|- ( ph -> ( G gsum F ) e. B )