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 ˙ = 0 G
gsummptres.2 φ G CMnd
gsummptres.3 φ A Fin
gsummptres.4 φ x A C B
gsummptres.5 φ x A D C = 0 ˙
Assertion gsummptres φ G x A C = G x A D C

Proof

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