gsummptfsres

Description: Extend a finitely supported group sum by padding outside with zeroes. (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	gsummptfsres.1	$⊢ B = {Base}_{G}$
	gsummptfsres.2	$⊢ \underset{˙}{0} = 0_{G}$
	gsummptfsres.3	$⊢ φ \to G \in CMnd$
	gsummptfsres.4	$⊢ φ \to A \in V$
	gsummptfsres.5	$⊢ (φ \land x \in (A ∖ S)) \to Y = \underset{˙}{0}$
	gsummptfsres.6	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((x \in A ⟼ Y))$
	gsummptfsres.7	$⊢ (φ \land x \in A) \to Y \in B$
	gsummptfsres.8	$⊢ φ \to S \subseteq A$
Assertion	gsummptfsres	$⊢ φ \to \underset{x \in A}{\sum_{G}} Y = \underset{x \in S}{\sum_{G}} Y$

Step	Hyp	Ref	Expression
1		gsummptfsres.1	$⊢ B = {Base}_{G}$
2		gsummptfsres.2	$⊢ \underset{˙}{0} = 0_{G}$
3		gsummptfsres.3	$⊢ φ \to G \in CMnd$
4		gsummptfsres.4	$⊢ φ \to A \in V$
5		gsummptfsres.5	$⊢ (φ \land x \in (A ∖ S)) \to Y = \underset{˙}{0}$
6		gsummptfsres.6	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((x \in A ⟼ Y))$
7		gsummptfsres.7	$⊢ (φ \land x \in A) \to Y \in B$
8		gsummptfsres.8	$⊢ φ \to S \subseteq A$
9	7	fmpttd	$⊢ φ \to (x \in A ⟼ Y) : A ⟶ B$
10	5 4	suppss2	$⊢ φ \to (x \in A ⟼ Y) supp \underset{˙}{0} \subseteq S$
11	1 2 3 4 9 10 6	gsumres	$⊢ φ \to \sum_{G} ({(x \in A ⟼ Y) ↾}_{S}) = \underset{x \in A}{\sum_{G}} Y$
12	8	resmptd	$⊢ φ \to {(x \in A ⟼ Y) ↾}_{S} = (x \in S ⟼ Y)$
13	12	oveq2d	$⊢ φ \to \sum_{G} ({(x \in A ⟼ Y) ↾}_{S}) = \underset{x \in S}{\sum_{G}} Y$
14	11 13	eqtr3d	$⊢ φ \to \underset{x \in A}{\sum_{G}} Y = \underset{x \in S}{\sum_{G}} Y$

Metamath Proof Explorer