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 eqtrdi ( 𝜑 → ( 0 ... 𝑁 ) = ( ( 1 ... 𝑁 ) ∪ { 0 } ) )
26 1 2 3 6 5 17 25 gsummptfidmsplit ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ 𝑌 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ 𝑌 ) ) + ( 𝐺 Σg ( 𝑘 ∈ { 0 } ↦ 𝑌 ) ) ) )