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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsummptres2.z ⊢ 0 = ( 0g ‘ 𝐺 )
gsummptres2.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
gsummptres2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsummptres2.0 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑆 ) ) → 𝑌 = 0 )
gsummptres2.1 ⊢ ( 𝜑 → 𝑆 ∈ Fin )
gsummptres2.y ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑌 ∈ 𝐵 )
gsummptres2.2 ⊢ ( 𝜑 → 𝑆 ⊆ 𝐴 )
Assertion gsummptres2 ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 𝑌 ) ) = ( 𝐺 Σg ( 𝑥 ∈ 𝑆 ↦ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 gsummptres2.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsummptres2.z ⊢ 0 = ( 0g ‘ 𝐺 )
3 gsummptres2.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4 gsummptres2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5 gsummptres2.0 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑆 ) ) → 𝑌 = 0 )
6 gsummptres2.1 ⊢ ( 𝜑 → 𝑆 ∈ Fin )
7 gsummptres2.y ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑌 ∈ 𝐵 )
8 gsummptres2.2 ⊢ ( 𝜑 → 𝑆 ⊆ 𝐴 )
9 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
10 4 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑌 ) ∈ V )
11 funmpt ⊢ Fun ( 𝑥 ∈ 𝐴 ↦ 𝑌 )
12 11 a1i ⊢ ( 𝜑 → Fun ( 𝑥 ∈ 𝐴 ↦ 𝑌 ) )
13 2 fvexi ⊢ 0 ∈ V
14 13 a1i ⊢ ( 𝜑 → 0 ∈ V )
15 5 4 suppss2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝑌 ) supp 0 ) ⊆ 𝑆 )
16 suppssfifsupp ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑌 ) ∈ V ∧ Fun ( 𝑥 ∈ 𝐴 ↦ 𝑌 ) ∧ 0 ∈ V ) ∧ ( 𝑆 ∈ Fin ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑌 ) supp 0 ) ⊆ 𝑆 ) ) → ( 𝑥 ∈ 𝐴 ↦ 𝑌 ) finSupp 0 )
17 10 12 14 6 15 16 syl32anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑌 ) finSupp 0 )
18 disjdif ⊢ ( 𝑆 ∩ ( 𝐴 ∖ 𝑆 ) ) = ∅
19 18 a1i ⊢ ( 𝜑 → ( 𝑆 ∩ ( 𝐴 ∖ 𝑆 ) ) = ∅ )
20 undif ⊢ ( 𝑆 ⊆ 𝐴 ↔ ( 𝑆 ∪ ( 𝐴 ∖ 𝑆 ) ) = 𝐴 )
21 8 20 sylib ⊢ ( 𝜑 → ( 𝑆 ∪ ( 𝐴 ∖ 𝑆 ) ) = 𝐴 )
22 21 eqcomd ⊢ ( 𝜑 → 𝐴 = ( 𝑆 ∪ ( 𝐴 ∖ 𝑆 ) ) )
23 1 2 9 3 4 7 17 19 22 gsumsplit2 ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 𝑌 ) ) = ( ( 𝐺 Σg ( 𝑥 ∈ 𝑆 ↦ 𝑌 ) ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∖ 𝑆 ) ↦ 𝑌 ) ) ) )
24 5 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∖ 𝑆 ) ↦ 𝑌 ) = ( 𝑥 ∈ ( 𝐴 ∖ 𝑆 ) ↦ 0 ) )
25 24 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∖ 𝑆 ) ↦ 𝑌 ) ) = ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∖ 𝑆 ) ↦ 0 ) ) )
26 3 cmnmndd ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
27 4 difexd ⊢ ( 𝜑 → ( 𝐴 ∖ 𝑆 ) ∈ V )
28 2 gsumz ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝐴 ∖ 𝑆 ) ∈ V ) → ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∖ 𝑆 ) ↦ 0 ) ) = 0 )
29 26 27 28 syl2anc ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∖ 𝑆 ) ↦ 0 ) ) = 0 )
30 25 29 eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∖ 𝑆 ) ↦ 𝑌 ) ) = 0 )
31 30 oveq2d ⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝑥 ∈ 𝑆 ↦ 𝑌 ) ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∖ 𝑆 ) ↦ 𝑌 ) ) ) = ( ( 𝐺 Σg ( 𝑥 ∈ 𝑆 ↦ 𝑌 ) ) ( +g ‘ 𝐺 ) 0 ) )
32 7 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑌 ∈ 𝐵 )
33 ssralv ⊢ ( 𝑆 ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝑌 ∈ 𝐵 → ∀ 𝑥 ∈ 𝑆 𝑌 ∈ 𝐵 ) )
34 8 32 33 sylc ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 𝑌 ∈ 𝐵 )
35 1 3 6 34 gsummptcl ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝑆 ↦ 𝑌 ) ) ∈ 𝐵 )
36 1 9 2 mndrid ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝐺 Σg ( 𝑥 ∈ 𝑆 ↦ 𝑌 ) ) ∈ 𝐵 ) → ( ( 𝐺 Σg ( 𝑥 ∈ 𝑆 ↦ 𝑌 ) ) ( +g ‘ 𝐺 ) 0 ) = ( 𝐺 Σg ( 𝑥 ∈ 𝑆 ↦ 𝑌 ) ) )
37 26 35 36 syl2anc ⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝑥 ∈ 𝑆 ↦ 𝑌 ) ) ( +g ‘ 𝐺 ) 0 ) = ( 𝐺 Σg ( 𝑥 ∈ 𝑆 ↦ 𝑌 ) ) )
38 23 31 37 3eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 𝑌 ) ) = ( 𝐺 Σg ( 𝑥 ∈ 𝑆 ↦ 𝑌 ) ) )