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

Metamath Proof Explorer

Theorem gsummptres2

Description: Extend a finite group sum by padding outside with zeroes. (Contributed by Thierry Arnoux, 22-Jun-2024)

Ref Expression
Hypotheses gsummptres2.b 
|- B = ( Base ` G )
gsummptres2.z 
|- .0. = ( 0g ` G )
gsummptres2.g 
|- ( ph -> G e. CMnd )
gsummptres2.a 
|- ( ph -> A e. V )
gsummptres2.0 
|- ( ( ph /\ x e. ( A \ S ) ) -> Y = .0. )
gsummptres2.1 
|- ( ph -> S e. Fin )
gsummptres2.y 
|- ( ( ph /\ x e. A ) -> Y e. B )
gsummptres2.2 
|- ( ph -> S C_ A )
Assertion gsummptres2 
|- ( ph -> ( G gsum ( x e. A |-> Y ) ) = ( G gsum ( x e. S |-> Y ) ) )

Proof

Step Hyp Ref Expression
1 gsummptres2.b 
 |-  B = ( Base ` G )
2 gsummptres2.z 
 |-  .0. = ( 0g ` G )
3 gsummptres2.g 
 |-  ( ph -> G e. CMnd )
4 gsummptres2.a 
 |-  ( ph -> A e. V )
5 gsummptres2.0 
 |-  ( ( ph /\ x e. ( A \ S ) ) -> Y = .0. )
6 gsummptres2.1 
 |-  ( ph -> S e. Fin )
7 gsummptres2.y 
 |-  ( ( ph /\ x e. A ) -> Y e. B )
8 gsummptres2.2 
 |-  ( ph -> S C_ A )
9 eqid 
 |-  ( +g ` G ) = ( +g ` G )
10 4 mptexd 
 |-  ( ph -> ( x e. A |-> Y ) e. _V )
11 funmpt 
 |-  Fun ( x e. A |-> Y )
12 11 a1i 
 |-  ( ph -> Fun ( x e. A |-> Y ) )
13 2 fvexi 
 |-  .0. e. _V
14 13 a1i 
 |-  ( ph -> .0. e. _V )
15 5 4 suppss2 
 |-  ( ph -> ( ( x e. A |-> Y ) supp .0. ) C_ S )
16 suppssfifsupp 
 |-  ( ( ( ( x e. A |-> Y ) e. _V /\ Fun ( x e. A |-> Y ) /\ .0. e. _V ) /\ ( S e. Fin /\ ( ( x e. A |-> Y ) supp .0. ) C_ S ) ) -> ( x e. A |-> Y ) finSupp .0. )
17 10 12 14 6 15 16 syl32anc 
 |-  ( ph -> ( x e. A |-> Y ) finSupp .0. )
18 disjdif 
 |-  ( S i^i ( A \ S ) ) = (/)
19 18 a1i 
 |-  ( ph -> ( S i^i ( A \ S ) ) = (/) )
20 undif 
 |-  ( S C_ A <-> ( S u. ( A \ S ) ) = A )
21 8 20 sylib 
 |-  ( ph -> ( S u. ( A \ S ) ) = A )
22 21 eqcomd 
 |-  ( ph -> A = ( S u. ( A \ S ) ) )
23 1 2 9 3 4 7 17 19 22 gsumsplit2 
 |-  ( ph -> ( G gsum ( x e. A |-> Y ) ) = ( ( G gsum ( x e. S |-> Y ) ) ( +g ` G ) ( G gsum ( x e. ( A \ S ) |-> Y ) ) ) )
24 5 mpteq2dva 
 |-  ( ph -> ( x e. ( A \ S ) |-> Y ) = ( x e. ( A \ S ) |-> .0. ) )
25 24 oveq2d 
 |-  ( ph -> ( G gsum ( x e. ( A \ S ) |-> Y ) ) = ( G gsum ( x e. ( A \ S ) |-> .0. ) ) )
26 3 cmnmndd 
 |-  ( ph -> G e. Mnd )
27 4 difexd 
 |-  ( ph -> ( A \ S ) e. _V )
28 2 gsumz 
 |-  ( ( G e. Mnd /\ ( A \ S ) e. _V ) -> ( G gsum ( x e. ( A \ S ) |-> .0. ) ) = .0. )
29 26 27 28 syl2anc 
 |-  ( ph -> ( G gsum ( x e. ( A \ S ) |-> .0. ) ) = .0. )
30 25 29 eqtrd 
 |-  ( ph -> ( G gsum ( x e. ( A \ S ) |-> Y ) ) = .0. )
31 30 oveq2d 
 |-  ( ph -> ( ( G gsum ( x e. S |-> Y ) ) ( +g ` G ) ( G gsum ( x e. ( A \ S ) |-> Y ) ) ) = ( ( G gsum ( x e. S |-> Y ) ) ( +g ` G ) .0. ) )
32 7 ralrimiva 
 |-  ( ph -> A. x e. A Y e. B )
33 ssralv 
 |-  ( S C_ A -> ( A. x e. A Y e. B -> A. x e. S Y e. B ) )
34 8 32 33 sylc 
 |-  ( ph -> A. x e. S Y e. B )
35 1 3 6 34 gsummptcl 
 |-  ( ph -> ( G gsum ( x e. S |-> Y ) ) e. B )
36 1 9 2 mndrid 
 |-  ( ( G e. Mnd /\ ( G gsum ( x e. S |-> Y ) ) e. B ) -> ( ( G gsum ( x e. S |-> Y ) ) ( +g ` G ) .0. ) = ( G gsum ( x e. S |-> Y ) ) )
37 26 35 36 syl2anc 
 |-  ( ph -> ( ( G gsum ( x e. S |-> Y ) ) ( +g ` G ) .0. ) = ( G gsum ( x e. S |-> Y ) ) )
38 23 31 37 3eqtrd 
 |-  ( ph -> ( G gsum ( x e. A |-> Y ) ) = ( G gsum ( x e. S |-> Y ) ) )