Metamath Proof Explorer

Theorem gsummptfzsplitla

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 Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses gsummptfzsplita.b 
|- B = ( Base ` G )
gsummptfzsplita.p 
|- .+ = ( +g ` G )
gsummptfzsplita.g 
|- ( ph -> G e. CMnd )
gsummptfzsplita.n 
|- ( ph -> N e. ( ZZ>= ` M ) )
gsummptfzsplita.y 
|- ( ( ph /\ k e. ( M ... N ) ) -> Y e. B )
gsummptfzsplitla.1 
|- ( ( ph /\ k = M ) -> Y = X )
Assertion gsummptfzsplitla 
|- ( ph -> ( G gsum ( k e. ( M ... N ) |-> Y ) ) = ( X .+ ( G gsum ( k e. ( ( M + 1 ) ... N ) |-> Y ) ) ) )

Proof

Step Hyp Ref Expression
1 gsummptfzsplita.b 
 |-  B = ( Base ` G )
2 gsummptfzsplita.p 
 |-  .+ = ( +g ` G )
3 gsummptfzsplita.g 
 |-  ( ph -> G e. CMnd )
4 gsummptfzsplita.n 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
5 gsummptfzsplita.y 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> Y e. B )
6 gsummptfzsplitla.1 
 |-  ( ( ph /\ k = M ) -> Y = X )
7 fzfid 
 |-  ( ph -> ( M ... N ) e. Fin )
8 fzpreddisj 
 |-  ( N e. ( ZZ>= ` M ) -> ( { M } i^i ( ( M + 1 ) ... N ) ) = (/) )
9 4 8 syl 
 |-  ( ph -> ( { M } i^i ( ( M + 1 ) ... N ) ) = (/) )
10 fzpred 
 |-  ( N e. ( ZZ>= ` M ) -> ( M ... N ) = ( { M } u. ( ( M + 1 ) ... N ) ) )
11 4 10 syl 
 |-  ( ph -> ( M ... N ) = ( { M } u. ( ( M + 1 ) ... N ) ) )
12 1 2 3 7 5 9 11 gsummptfidmsplit 
 |-  ( ph -> ( G gsum ( k e. ( M ... N ) |-> Y ) ) = ( ( G gsum ( k e. { M } |-> Y ) ) .+ ( G gsum ( k e. ( ( M + 1 ) ... N ) |-> Y ) ) ) )
13 3 cmnmndd 
 |-  ( ph -> G e. Mnd )
14 4 elfvexd 
 |-  ( ph -> M e. _V )
15 14 6 csbied 
 |-  ( ph -> [_ M / k ]_ Y = X )
16 eluzfz1 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
17 4 16 syl 
 |-  ( ph -> M e. ( M ... N ) )
18 5 ralrimiva 
 |-  ( ph -> A. k e. ( M ... N ) Y e. B )
19 rspcsbela 
 |-  ( ( M e. ( M ... N ) /\ A. k e. ( M ... N ) Y e. B ) -> [_ M / k ]_ Y e. B )
20 17 18 19 syl2anc 
 |-  ( ph -> [_ M / k ]_ Y e. B )
21 15 20 eqeltrrd 
 |-  ( ph -> X e. B )
22 1 13 14 21 6 gsumsnd 
 |-  ( ph -> ( G gsum ( k e. { M } |-> Y ) ) = X )
23 22 oveq1d 
 |-  ( ph -> ( ( G gsum ( k e. { M } |-> Y ) ) .+ ( G gsum ( k e. ( ( M + 1 ) ... N ) |-> Y ) ) ) = ( X .+ ( G gsum ( k e. ( ( M + 1 ) ... N ) |-> Y ) ) ) )
24 12 23 eqtrd 
 |-  ( ph -> ( G gsum ( k e. ( M ... N ) |-> Y ) ) = ( X .+ ( G gsum ( k e. ( ( M + 1 ) ... N ) |-> Y ) ) ) )