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 𝐵 = ( Base ‘ 𝐺 )
gsummptres.1 0 = ( 0g𝐺 )
gsummptres.2 ( 𝜑𝐺 ∈ CMnd )
gsummptres.3 ( 𝜑𝐴 ∈ Fin )
gsummptres.4 ( ( 𝜑𝑥𝐴 ) → 𝐶𝐵 )
gsummptres.5 ( ( 𝜑𝑥 ∈ ( 𝐴𝐷 ) ) → 𝐶 = 0 )
Assertion gsummptres ( 𝜑 → ( 𝐺 Σg ( 𝑥𝐴𝐶 ) ) = ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴𝐷 ) ↦ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 gsummptres.0 𝐵 = ( Base ‘ 𝐺 )
2 gsummptres.1 0 = ( 0g𝐺 )
3 gsummptres.2 ( 𝜑𝐺 ∈ CMnd )
4 gsummptres.3 ( 𝜑𝐴 ∈ Fin )
5 gsummptres.4 ( ( 𝜑𝑥𝐴 ) → 𝐶𝐵 )
6 gsummptres.5 ( ( 𝜑𝑥 ∈ ( 𝐴𝐷 ) ) → 𝐶 = 0 )
7 eqid ( +g𝐺 ) = ( +g𝐺 )
8 eqid ( 𝑥𝐴𝐶 ) = ( 𝑥𝐴𝐶 )
9 2 fvexi 0 ∈ V
10 9 a1i ( 𝜑0 ∈ V )
11 8 4 5 10 fsuppmptdm ( 𝜑 → ( 𝑥𝐴𝐶 ) finSupp 0 )
12 inindif ( ( 𝐴𝐷 ) ∩ ( 𝐴𝐷 ) ) = ∅
13 12 a1i ( 𝜑 → ( ( 𝐴𝐷 ) ∩ ( 𝐴𝐷 ) ) = ∅ )
14 inundif ( ( 𝐴𝐷 ) ∪ ( 𝐴𝐷 ) ) = 𝐴
15 14 eqcomi 𝐴 = ( ( 𝐴𝐷 ) ∪ ( 𝐴𝐷 ) )
16 15 a1i ( 𝜑𝐴 = ( ( 𝐴𝐷 ) ∪ ( 𝐴𝐷 ) ) )
17 1 2 7 3 4 5 11 13 16 gsumsplit2 ( 𝜑 → ( 𝐺 Σg ( 𝑥𝐴𝐶 ) ) = ( ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴𝐷 ) ↦ 𝐶 ) ) ( +g𝐺 ) ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴𝐷 ) ↦ 𝐶 ) ) ) )
18 6 mpteq2dva ( 𝜑 → ( 𝑥 ∈ ( 𝐴𝐷 ) ↦ 𝐶 ) = ( 𝑥 ∈ ( 𝐴𝐷 ) ↦ 0 ) )
19 18 oveq2d ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴𝐷 ) ↦ 𝐶 ) ) = ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴𝐷 ) ↦ 0 ) ) )
20 cmnmnd ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
21 3 20 syl ( 𝜑𝐺 ∈ Mnd )
22 diffi ( 𝐴 ∈ Fin → ( 𝐴𝐷 ) ∈ Fin )
23 4 22 syl ( 𝜑 → ( 𝐴𝐷 ) ∈ Fin )
24 2 gsumz ( ( 𝐺 ∈ Mnd ∧ ( 𝐴𝐷 ) ∈ Fin ) → ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴𝐷 ) ↦ 0 ) ) = 0 )
25 21 23 24 syl2anc ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴𝐷 ) ↦ 0 ) ) = 0 )
26 19 25 eqtrd ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴𝐷 ) ↦ 𝐶 ) ) = 0 )
27 26 oveq2d ( 𝜑 → ( ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴𝐷 ) ↦ 𝐶 ) ) ( +g𝐺 ) ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴𝐷 ) ↦ 𝐶 ) ) ) = ( ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴𝐷 ) ↦ 𝐶 ) ) ( +g𝐺 ) 0 ) )
28 infi ( 𝐴 ∈ Fin → ( 𝐴𝐷 ) ∈ Fin )
29 4 28 syl ( 𝜑 → ( 𝐴𝐷 ) ∈ Fin )
30 inss1 ( 𝐴𝐷 ) ⊆ 𝐴
31 30 sseli ( 𝑥 ∈ ( 𝐴𝐷 ) → 𝑥𝐴 )
32 31 5 sylan2 ( ( 𝜑𝑥 ∈ ( 𝐴𝐷 ) ) → 𝐶𝐵 )
33 32 ralrimiva ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴𝐷 ) 𝐶𝐵 )
34 1 3 29 33 gsummptcl ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴𝐷 ) ↦ 𝐶 ) ) ∈ 𝐵 )
35 1 7 2 mndrid ( ( 𝐺 ∈ Mnd ∧ ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴𝐷 ) ↦ 𝐶 ) ) ∈ 𝐵 ) → ( ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴𝐷 ) ↦ 𝐶 ) ) ( +g𝐺 ) 0 ) = ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴𝐷 ) ↦ 𝐶 ) ) )
36 21 34 35 syl2anc ( 𝜑 → ( ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴𝐷 ) ↦ 𝐶 ) ) ( +g𝐺 ) 0 ) = ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴𝐷 ) ↦ 𝐶 ) ) )
37 27 36 eqtrd ( 𝜑 → ( ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴𝐷 ) ↦ 𝐶 ) ) ( +g𝐺 ) ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴𝐷 ) ↦ 𝐶 ) ) ) = ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴𝐷 ) ↦ 𝐶 ) ) )
38 17 37 eqtrd ( 𝜑 → ( 𝐺 Σg ( 𝑥𝐴𝐶 ) ) = ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴𝐷 ) ↦ 𝐶 ) ) )