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

Metamath Proof Explorer

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 ) ) )