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 ˙ = 0 G
gsummptres2.g φ G CMnd
gsummptres2.a φ A V
gsummptres2.0 φ x A S Y = 0 ˙
gsummptres2.1 φ S Fin
gsummptres2.y φ x A Y B
gsummptres2.2 φ S A
Assertion gsummptres2 φ G x A Y = G x S Y

Proof

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