gsumcl2

Description: Closure of a finite group sum. This theorem has a weaker hypothesis than gsumcl , because it is not required that F is a function (actually, the hypothesis always holds for any proper class F ). (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$
	gsumcl2.w	$⊢ φ \to F supp \underset{˙}{0} \in Fin$
Assertion	gsumcl2	$⊢ φ \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		gsumcl2.w	$⊢ φ \to F supp \underset{˙}{0} \in Fin$
7		eqid	$⊢ Cntz (G) = Cntz (G)$
8		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
9	3 8	syl	$⊢ φ \to G \in Mnd$
10	1 7 3 5	cntzcmnf	$⊢ φ \to ran F \subseteq Cntz (G) (ran F)$
11	1 2 7 9 4 5 10 6	gsumzcl2	$⊢ φ \to \sum_{G} F \in B$

Metamath Proof Explorer

Theorem gsumcl2

Proof