Theorem 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	|- .0. = ( 0g ` G )
	gsummptfsres.3	|- ( ph -> G e. CMnd )
	gsummptfsres.4	|- ( ph -> A e. V )
	gsummptfsres.5	|- ( ( ph /\ x e. ( A \ S ) ) -> Y = .0. )
	gsummptfsres.6	|- ( ph -> ( x e. A |-> Y ) finSupp .0. )
	gsummptfsres.7	|- ( ( ph /\ x e. A ) -> Y e. B )
	gsummptfsres.8	|- ( ph -> S C_ A )
Assertion	gsummptfsres	|- ( ph -> ( G gsum ( x e. A |-> Y ) ) = ( G gsum ( x e. S |-> Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummptfsres.1	|- B = ( Base ` G )
2		gsummptfsres.2	|- .0. = ( 0g ` G )
3		gsummptfsres.3	|- ( ph -> G e. CMnd )
4		gsummptfsres.4	|- ( ph -> A e. V )
5		gsummptfsres.5	|- ( ( ph /\ x e. ( A \ S ) ) -> Y = .0. )
6		gsummptfsres.6	|- ( ph -> ( x e. A |-> Y ) finSupp .0. )
7		gsummptfsres.7	|- ( ( ph /\ x e. A ) -> Y e. B )
8		gsummptfsres.8	|- ( ph -> S C_ A )
9	7	fmpttd	|- ( ph -> ( x e. A |-> Y ) : A --> B )
10	5 4	suppss2	|- ( ph -> ( ( x e. A |-> Y ) supp .0. ) C_ S )
11	1 2 3 4 9 10 6	gsumres	|- ( ph -> ( G gsum ( ( x e. A |-> Y ) |` S ) ) = ( G gsum ( x e. A |-> Y ) ) )
12	8	resmptd	|- ( ph -> ( ( x e. A |-> Y ) |` S ) = ( x e. S |-> Y ) )
13	12	oveq2d	|- ( ph -> ( G gsum ( ( x e. A |-> Y ) |` S ) ) = ( G gsum ( x e. S |-> Y ) ) )
14	11 13	eqtr3d	|- ( ph -> ( G gsum ( x e. A |-> Y ) ) = ( G gsum ( x e. S |-> Y ) ) )