Metamath Proof Explorer

Theorem gsummptres

Description: Extend a finite group sum by padding outside with zeroes. Proof generated using OpenAI's proof assistant. (Contributed by Thierry Arnoux, 11-Jul-2020)

Ref Expression
Hypotheses gsummptres.0 
|- B = ( Base ` G )
gsummptres.1 
|- .0. = ( 0g ` G )
gsummptres.2 
|- ( ph -> G e. CMnd )
gsummptres.3 
|- ( ph -> A e. Fin )
gsummptres.4 
|- ( ( ph /\ x e. A ) -> C e. B )
gsummptres.5 
|- ( ( ph /\ x e. ( A \ D ) ) -> C = .0. )
Assertion gsummptres 
|- ( ph -> ( G gsum ( x e. A |-> C ) ) = ( G gsum ( x e. ( A i^i D ) |-> C ) ) )

Proof

Step Hyp Ref Expression
1 gsummptres.0 
 |-  B = ( Base ` G )
2 gsummptres.1 
 |-  .0. = ( 0g ` G )
3 gsummptres.2 
 |-  ( ph -> G e. CMnd )
4 gsummptres.3 
 |-  ( ph -> A e. Fin )
5 gsummptres.4 
 |-  ( ( ph /\ x e. A ) -> C e. B )
6 gsummptres.5 
 |-  ( ( ph /\ x e. ( A \ D ) ) -> C = .0. )
7 eqid 
 |-  ( +g ` G ) = ( +g ` G )
8 eqid 
 |-  ( x e. A |-> C ) = ( x e. A |-> C )
9 2 fvexi 
 |-  .0. e. _V
10 9 a1i 
 |-  ( ph -> .0. e. _V )
11 8 4 5 10 fsuppmptdm 
 |-  ( ph -> ( x e. A |-> C ) finSupp .0. )
12 inindif 
 |-  ( ( A i^i D ) i^i ( A \ D ) ) = (/)
13 12 a1i 
 |-  ( ph -> ( ( A i^i D ) i^i ( A \ D ) ) = (/) )
14 inundif 
 |-  ( ( A i^i D ) u. ( A \ D ) ) = A
15 14 eqcomi 
 |-  A = ( ( A i^i D ) u. ( A \ D ) )
16 15 a1i 
 |-  ( ph -> A = ( ( A i^i D ) u. ( A \ D ) ) )
17 1 2 7 3 4 5 11 13 16 gsumsplit2 
 |-  ( ph -> ( G gsum ( x e. A |-> C ) ) = ( ( G gsum ( x e. ( A i^i D ) |-> C ) ) ( +g ` G ) ( G gsum ( x e. ( A \ D ) |-> C ) ) ) )
18 6 mpteq2dva 
 |-  ( ph -> ( x e. ( A \ D ) |-> C ) = ( x e. ( A \ D ) |-> .0. ) )
19 18 oveq2d 
 |-  ( ph -> ( G gsum ( x e. ( A \ D ) |-> C ) ) = ( G gsum ( x e. ( A \ D ) |-> .0. ) ) )
20 cmnmnd 
 |-  ( G e. CMnd -> G e. Mnd )
21 3 20 syl 
 |-  ( ph -> G e. Mnd )
22 diffi 
 |-  ( A e. Fin -> ( A \ D ) e. Fin )
23 4 22 syl 
 |-  ( ph -> ( A \ D ) e. Fin )
24 2 gsumz 
 |-  ( ( G e. Mnd /\ ( A \ D ) e. Fin ) -> ( G gsum ( x e. ( A \ D ) |-> .0. ) ) = .0. )
25 21 23 24 syl2anc 
 |-  ( ph -> ( G gsum ( x e. ( A \ D ) |-> .0. ) ) = .0. )
26 19 25 eqtrd 
 |-  ( ph -> ( G gsum ( x e. ( A \ D ) |-> C ) ) = .0. )
27 26 oveq2d 
 |-  ( ph -> ( ( G gsum ( x e. ( A i^i D ) |-> C ) ) ( +g ` G ) ( G gsum ( x e. ( A \ D ) |-> C ) ) ) = ( ( G gsum ( x e. ( A i^i D ) |-> C ) ) ( +g ` G ) .0. ) )
28 infi 
 |-  ( A e. Fin -> ( A i^i D ) e. Fin )
29 4 28 syl 
 |-  ( ph -> ( A i^i D ) e. Fin )
30 inss1 
 |-  ( A i^i D ) C_ A
31 30 sseli 
 |-  ( x e. ( A i^i D ) -> x e. A )
32 31 5 sylan2 
 |-  ( ( ph /\ x e. ( A i^i D ) ) -> C e. B )
33 32 ralrimiva 
 |-  ( ph -> A. x e. ( A i^i D ) C e. B )
34 1 3 29 33 gsummptcl 
 |-  ( ph -> ( G gsum ( x e. ( A i^i D ) |-> C ) ) e. B )
35 1 7 2 mndrid 
 |-  ( ( G e. Mnd /\ ( G gsum ( x e. ( A i^i D ) |-> C ) ) e. B ) -> ( ( G gsum ( x e. ( A i^i D ) |-> C ) ) ( +g ` G ) .0. ) = ( G gsum ( x e. ( A i^i D ) |-> C ) ) )
36 21 34 35 syl2anc 
 |-  ( ph -> ( ( G gsum ( x e. ( A i^i D ) |-> C ) ) ( +g ` G ) .0. ) = ( G gsum ( x e. ( A i^i D ) |-> C ) ) )
37 27 36 eqtrd 
 |-  ( ph -> ( ( G gsum ( x e. ( A i^i D ) |-> C ) ) ( +g ` G ) ( G gsum ( x e. ( A \ D ) |-> C ) ) ) = ( G gsum ( x e. ( A i^i D ) |-> C ) ) )
38 17 37 eqtrd 
 |-  ( ph -> ( G gsum ( x e. A |-> C ) ) = ( G gsum ( x e. ( A i^i D ) |-> C ) ) )