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

Metamath Proof Explorer

Theorem gsumres

Description: Extend a finite group sum by padding outside with zeroes. (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$
		gsumres.s	$⊢ φ \to F supp \underset{˙}{0} \subseteq W$
		gsumres.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
	Assertion	gsumres	$⊢ φ \to \sum_{G} ({F ↾}_{W}) = \sum_{G} F$

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		gsumres.s	$⊢ φ \to F supp \underset{˙}{0} \subseteq W$
7		gsumres.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
8		eqid	$⊢ Cntz (G) = Cntz (G)$
9		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
10	3 9	syl	$⊢ φ \to G \in Mnd$
11	1 8 3 5	cntzcmnf	$⊢ φ \to ran F \subseteq Cntz (G) (ran F)$
12	1 2 8 10 4 5 11 6 7	gsumzres	$⊢ φ \to \sum_{G} ({F ↾}_{W}) = \sum_{G} F$