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 B = Base G
gsummptfzsplit.p + ˙ = + G
gsummptfzsplit.g φ G CMnd
gsummptfzsplit.n φ N 0
gsummptfzsplitl.y φ k 0 N Y B
Assertion gsummptfzsplitl φ G k = 0 N Y = G k = 1 N Y + ˙ G k 0 Y

Proof

Step Hyp Ref Expression
1 gsummptfzsplit.b B = Base G
2 gsummptfzsplit.p + ˙ = + G
3 gsummptfzsplit.g φ G CMnd
4 gsummptfzsplit.n φ N 0
5 gsummptfzsplitl.y φ k 0 N Y B
6 fzfid φ 0 N Fin
7 incom 1 N 0 = 0 1 N
8 7 a1i φ 1 N 0 = 0 1 N
9 1e0p1 1 = 0 + 1
10 9 oveq1i 1 N = 0 + 1 N
11 10 a1i φ 1 N = 0 + 1 N
12 11 ineq2d φ 0 1 N = 0 0 + 1 N
13 elnn0uz N 0 N 0
14 13 biimpi N 0 N 0
15 fzpreddisj N 0 0 0 + 1 N =
16 4 14 15 3syl φ 0 0 + 1 N =
17 8 12 16 3eqtrd φ 1 N 0 =
18 fzpred N 0 0 N = 0 0 + 1 N
19 4 14 18 3syl φ 0 N = 0 0 + 1 N
20 uncom 0 0 + 1 N = 0 + 1 N 0
21 0p1e1 0 + 1 = 1
22 21 oveq1i 0 + 1 N = 1 N
23 22 uneq1i 0 + 1 N 0 = 1 N 0
24 20 23 eqtri 0 0 + 1 N = 1 N 0
25 19 24 eqtrdi φ 0 N = 1 N 0
26 1 2 3 6 5 17 25 gsummptfidmsplit φ G k = 0 N Y = G k = 1 N Y + ˙ G k 0 Y