Metamath Proof Explorer

Theorem gsummptfzsplitl

Description: Split a group sum expressed as mapping with a finite set of sequential integers as domain into two parts, , extracting a singleton from the left. (Contributed by AV, 7-Nov-2019)

Ref Expression
Hypotheses gsummptfzsplit.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsummptfzsplit.p ⊢ + = ( +g ‘ 𝐺 )
gsummptfzsplit.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
gsummptfzsplit.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
gsummptfzsplitl.y ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑌 ∈ 𝐵 )
Assertion gsummptfzsplitl ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ 𝑌 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ 𝑌 ) ) + ( 𝐺 Σg ( 𝑘 ∈ { 0 } ↦ 𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 gsummptfzsplit.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsummptfzsplit.p ⊢ + = ( +g ‘ 𝐺 )
3 gsummptfzsplit.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4 gsummptfzsplit.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5 gsummptfzsplitl.y ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑌 ∈ 𝐵 )
6 fzfid ⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ Fin )
7 incom ⊢ ( ( 1 ... 𝑁 ) ∩ { 0 } ) = ( { 0 } ∩ ( 1 ... 𝑁 ) )
8 7 a1i ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∩ { 0 } ) = ( { 0 } ∩ ( 1 ... 𝑁 ) ) )
9 1e0p1 ⊢ 1 = ( 0 + 1 )
10 9 oveq1i ⊢ ( 1 ... 𝑁 ) = ( ( 0 + 1 ) ... 𝑁 )
11 10 a1i ⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( 0 + 1 ) ... 𝑁 ) )
12 11 ineq2d ⊢ ( 𝜑 → ( { 0 } ∩ ( 1 ... 𝑁 ) ) = ( { 0 } ∩ ( ( 0 + 1 ) ... 𝑁 ) ) )
13 elnn0uz ⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
14 13 biimpi ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
15 fzpreddisj ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( { 0 } ∩ ( ( 0 + 1 ) ... 𝑁 ) ) = ∅ )
16 4 14 15 3syl ⊢ ( 𝜑 → ( { 0 } ∩ ( ( 0 + 1 ) ... 𝑁 ) ) = ∅ )
17 8 12 16 3eqtrd ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∩ { 0 } ) = ∅ )
18 fzpred ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( 0 ... 𝑁 ) = ( { 0 } ∪ ( ( 0 + 1 ) ... 𝑁 ) ) )
19 4 14 18 3syl ⊢ ( 𝜑 → ( 0 ... 𝑁 ) = ( { 0 } ∪ ( ( 0 + 1 ) ... 𝑁 ) ) )
20 uncom ⊢ ( { 0 } ∪ ( ( 0 + 1 ) ... 𝑁 ) ) = ( ( ( 0 + 1 ) ... 𝑁 ) ∪ { 0 } )
21 0p1e1 ⊢ ( 0 + 1 ) = 1
22 21 oveq1i ⊢ ( ( 0 + 1 ) ... 𝑁 ) = ( 1 ... 𝑁 )
23 22 uneq1i ⊢ ( ( ( 0 + 1 ) ... 𝑁 ) ∪ { 0 } ) = ( ( 1 ... 𝑁 ) ∪ { 0 } )
24 20 23 eqtri ⊢ ( { 0 } ∪ ( ( 0 + 1 ) ... 𝑁 ) ) = ( ( 1 ... 𝑁 ) ∪ { 0 } )
25 19 24 syl6eq ⊢ ( 𝜑 → ( 0 ... 𝑁 ) = ( ( 1 ... 𝑁 ) ∪ { 0 } ) )
26 1 2 3 6 5 17 25 gsummptfidmsplit ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ 𝑌 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ 𝑌 ) ) + ( 𝐺 Σg ( 𝑘 ∈ { 0 } ↦ 𝑌 ) ) ) )