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 ` G )
gsummptfzsplit.g
|- ( ph -> G e. CMnd )
gsummptfzsplit.n
|- ( ph -> N e. NN0 )
gsummptfzsplitl.y
|- ( ( ph /\ k e. ( 0 ... N ) ) -> Y e. B )
Assertion gsummptfzsplitl
|- ( ph -> ( G gsum ( k e. ( 0 ... N ) |-> Y ) ) = ( ( G gsum ( k e. ( 1 ... N ) |-> Y ) ) .+ ( G gsum ( k e. { 0 } |-> Y ) ) ) )

Proof

Step Hyp Ref Expression
1 gsummptfzsplit.b
 |-  B = ( Base ` G )
2 gsummptfzsplit.p
 |-  .+ = ( +g ` G )
3 gsummptfzsplit.g
 |-  ( ph -> G e. CMnd )
4 gsummptfzsplit.n
 |-  ( ph -> N e. NN0 )
5 gsummptfzsplitl.y
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> Y e. B )
6 fzfid
 |-  ( ph -> ( 0 ... N ) e. Fin )
7 incom
 |-  ( ( 1 ... N ) i^i { 0 } ) = ( { 0 } i^i ( 1 ... N ) )
8 7 a1i
 |-  ( ph -> ( ( 1 ... N ) i^i { 0 } ) = ( { 0 } i^i ( 1 ... N ) ) )
9 1e0p1
 |-  1 = ( 0 + 1 )
10 9 oveq1i
 |-  ( 1 ... N ) = ( ( 0 + 1 ) ... N )
11 10 a1i
 |-  ( ph -> ( 1 ... N ) = ( ( 0 + 1 ) ... N ) )
12 11 ineq2d
 |-  ( ph -> ( { 0 } i^i ( 1 ... N ) ) = ( { 0 } i^i ( ( 0 + 1 ) ... N ) ) )
13 elnn0uz
 |-  ( N e. NN0 <-> N e. ( ZZ>= ` 0 ) )
14 13 biimpi
 |-  ( N e. NN0 -> N e. ( ZZ>= ` 0 ) )
15 fzpreddisj
 |-  ( N e. ( ZZ>= ` 0 ) -> ( { 0 } i^i ( ( 0 + 1 ) ... N ) ) = (/) )
16 4 14 15 3syl
 |-  ( ph -> ( { 0 } i^i ( ( 0 + 1 ) ... N ) ) = (/) )
17 8 12 16 3eqtrd
 |-  ( ph -> ( ( 1 ... N ) i^i { 0 } ) = (/) )
18 fzpred
 |-  ( N e. ( ZZ>= ` 0 ) -> ( 0 ... N ) = ( { 0 } u. ( ( 0 + 1 ) ... N ) ) )
19 4 14 18 3syl
 |-  ( ph -> ( 0 ... N ) = ( { 0 } u. ( ( 0 + 1 ) ... N ) ) )
20 uncom
 |-  ( { 0 } u. ( ( 0 + 1 ) ... N ) ) = ( ( ( 0 + 1 ) ... N ) u. { 0 } )
21 0p1e1
 |-  ( 0 + 1 ) = 1
22 21 oveq1i
 |-  ( ( 0 + 1 ) ... N ) = ( 1 ... N )
23 22 uneq1i
 |-  ( ( ( 0 + 1 ) ... N ) u. { 0 } ) = ( ( 1 ... N ) u. { 0 } )
24 20 23 eqtri
 |-  ( { 0 } u. ( ( 0 + 1 ) ... N ) ) = ( ( 1 ... N ) u. { 0 } )
25 19 24 eqtrdi
 |-  ( ph -> ( 0 ... N ) = ( ( 1 ... N ) u. { 0 } ) )
26 1 2 3 6 5 17 25 gsummptfidmsplit
 |-  ( ph -> ( G gsum ( k e. ( 0 ... N ) |-> Y ) ) = ( ( G gsum ( k e. ( 1 ... N ) |-> Y ) ) .+ ( G gsum ( k e. { 0 } |-> Y ) ) ) )