This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) ) )