Metamath Proof Explorer

Theorem gsummptfzsplitra

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 right. (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 )
gsummptfzsplitra.1 
|- ( ( ph /\ k = N ) -> Y = X )
Assertion gsummptfzsplitra 
|- ( ph -> ( G gsum ( k e. ( M ... N ) |-> Y ) ) = ( ( G gsum ( k e. ( M ..^ N ) |-> Y ) ) .+ X ) )

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 gsummptfzsplitra.1 
 |-  ( ( ph /\ k = N ) -> Y = X )
7 fzfid 
 |-  ( ph -> ( M ... N ) e. Fin )
8 fzodisjsn 
 |-  ( ( M ..^ N ) i^i { N } ) = (/)
9 8 a1i 
 |-  ( ph -> ( ( M ..^ N ) i^i { N } ) = (/) )
10 fzisfzounsn 
 |-  ( N e. ( ZZ>= ` M ) -> ( M ... N ) = ( ( M ..^ N ) u. { N } ) )
11 4 10 syl 
 |-  ( ph -> ( M ... N ) = ( ( M ..^ N ) u. { N } ) )
12 1 2 3 7 5 9 11 gsummptfidmsplit 
 |-  ( ph -> ( G gsum ( k e. ( M ... N ) |-> Y ) ) = ( ( G gsum ( k e. ( M ..^ N ) |-> Y ) ) .+ ( G gsum ( k e. { N } |-> Y ) ) ) )
13 3 cmnmndd 
 |-  ( ph -> G e. Mnd )
14 4 6 csbied 
 |-  ( ph -> [_ N / k ]_ Y = X )
15 eluzfz2 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
16 4 15 syl 
 |-  ( ph -> N e. ( M ... N ) )
17 5 ralrimiva 
 |-  ( ph -> A. k e. ( M ... N ) Y e. B )
18 rspcsbela 
 |-  ( ( N e. ( M ... N ) /\ A. k e. ( M ... N ) Y e. B ) -> [_ N / k ]_ Y e. B )
19 16 17 18 syl2anc 
 |-  ( ph -> [_ N / k ]_ Y e. B )
20 14 19 eqeltrrd 
 |-  ( ph -> X e. B )
21 1 13 4 20 6 gsumsnd 
 |-  ( ph -> ( G gsum ( k e. { N } |-> Y ) ) = X )
22 21 oveq2d 
 |-  ( ph -> ( ( G gsum ( k e. ( M ..^ N ) |-> Y ) ) .+ ( G gsum ( k e. { N } |-> Y ) ) ) = ( ( G gsum ( k e. ( M ..^ N ) |-> Y ) ) .+ X ) )
23 12 22 eqtrd 
 |-  ( ph -> ( G gsum ( k e. ( M ... N ) |-> Y ) ) = ( ( G gsum ( k e. ( M ..^ N ) |-> Y ) ) .+ X ) )