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={\mathrm{Base}}_G$$
	gsummptfsres.2	$$⊢\underset{\dot{}}{0}=0_G$$
	gsummptfsres.3	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsummptfsres.4	$$⊢\phi \to A\in V$$
	gsummptfsres.5	$$⊢\left(\phi \wedge x\in \left(A\setminus S\right)\right)\to Y=\underset{\dot{}}{0}$$
	gsummptfsres.6	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(x\in A⟼Y\right)\right)$$
	gsummptfsres.7	$$⊢\left(\phi \wedge x\in A\right)\to Y\in B$$
	gsummptfsres.8	$$⊢\phi \to S\subseteq A$$
Assertion	gsummptfsres	$$⊢\phi \to \underset{x\in A}{{\sum }_G}Y=\underset{x\in S}{{\sum }_G}Y$$

Proof

Step	Hyp	Ref	Expression
1		gsummptfsres.1	$$⊢B={\mathrm{Base}}_G$$
2		gsummptfsres.2	$$⊢\underset{\dot{}}{0}=0_G$$
3		gsummptfsres.3	$$⊢\phi \to G\in \mathrm{CMnd}$$
4		gsummptfsres.4	$$⊢\phi \to A\in V$$
5		gsummptfsres.5	$$⊢\left(\phi \wedge x\in \left(A\setminus S\right)\right)\to Y=\underset{\dot{}}{0}$$
6		gsummptfsres.6	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(x\in A⟼Y\right)\right)$$
7		gsummptfsres.7	$$⊢\left(\phi \wedge x\in A\right)\to Y\in B$$
8		gsummptfsres.8	$$⊢\phi \to S\subseteq A$$
9	7	fmpttd	$$⊢\phi \to \left(x\in A⟼Y\right):A⟶B$$
10	5 4	suppss2	$$⊢\phi \to \left(x\in A⟼Y\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq S$$
11	1 2 3 4 9 10 6	gsumres	$$⊢\phi \to {\sum }_G\left({\left(x\in A⟼Y\right)\upharpoonright }_S\right)=\underset{x\in A}{{\sum }_G}Y$$
12	8	resmptd	$$⊢\phi \to {\left(x\in A⟼Y\right)\upharpoonright }_S=\left(x\in S⟼Y\right)$$
13	12	oveq2d	$$⊢\phi \to {\sum }_G\left({\left(x\in A⟼Y\right)\upharpoonright }_S\right)=\underset{x\in S}{{\sum }_G}Y$$
14	11 13	eqtr3d	$$⊢\phi \to \underset{x\in A}{{\sum }_G}Y=\underset{x\in S}{{\sum }_G}Y$$