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

Metamath Proof Explorer

Theorem gsummptp1

Description: Reindex a zero-based sum as a one-base sum. (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses gsummptp1.1 
|- B = ( Base ` R )
gsummptp1.2 
|- ( ph -> R e. CMnd )
gsummptp1.3 
|- ( ph -> N e. NN0 )
gsummptp1.4 
|- ( ( ph /\ l e. ( 1 ... N ) ) -> Y e. B )
gsummptp1.5 
|- ( ( ( ph /\ k e. ( 0 ..^ N ) ) /\ l = ( k + 1 ) ) -> Y = X )
Assertion gsummptp1 
|- ( ph -> ( R gsum ( k e. ( 0 ..^ N ) |-> X ) ) = ( R gsum ( l e. ( 1 ... N ) |-> Y ) ) )

Proof

Step Hyp Ref Expression
1 gsummptp1.1 
 |-  B = ( Base ` R )
2 gsummptp1.2 
 |-  ( ph -> R e. CMnd )
3 gsummptp1.3 
 |-  ( ph -> N e. NN0 )
4 gsummptp1.4 
 |-  ( ( ph /\ l e. ( 1 ... N ) ) -> Y e. B )
5 gsummptp1.5 
 |-  ( ( ( ph /\ k e. ( 0 ..^ N ) ) /\ l = ( k + 1 ) ) -> Y = X )
6 nfcsb1v 
 |-  F/_ l [_ ( k + 1 ) / l ]_ Y
7 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
8 csbeq1a 
 |-  ( l = ( k + 1 ) -> Y = [_ ( k + 1 ) / l ]_ Y )
9 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
10 ssidd 
 |-  ( ph -> B C_ B )
11 fz0add1fz1 
 |-  ( ( N e. NN0 /\ k e. ( 0 ..^ N ) ) -> ( k + 1 ) e. ( 1 ... N ) )
12 3 11 sylan 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( k + 1 ) e. ( 1 ... N ) )
13 fz1fzo0m1 
 |-  ( l e. ( 1 ... N ) -> ( l - 1 ) e. ( 0 ..^ N ) )
14 13 adantl 
 |-  ( ( ph /\ l e. ( 1 ... N ) ) -> ( l - 1 ) e. ( 0 ..^ N ) )
15 eqcom 
 |-  ( ( k + 1 ) = l <-> l = ( k + 1 ) )
16 elfzonn0 
 |-  ( k e. ( 0 ..^ N ) -> k e. NN0 )
17 16 adantl 
 |-  ( ( ( ph /\ l e. ( 1 ... N ) ) /\ k e. ( 0 ..^ N ) ) -> k e. NN0 )
18 17 nn0cnd 
 |-  ( ( ( ph /\ l e. ( 1 ... N ) ) /\ k e. ( 0 ..^ N ) ) -> k e. CC )
19 1cnd 
 |-  ( ( ( ph /\ l e. ( 1 ... N ) ) /\ k e. ( 0 ..^ N ) ) -> 1 e. CC )
20 elfznn 
 |-  ( l e. ( 1 ... N ) -> l e. NN )
21 20 ad2antlr 
 |-  ( ( ( ph /\ l e. ( 1 ... N ) ) /\ k e. ( 0 ..^ N ) ) -> l e. NN )
22 21 nncnd 
 |-  ( ( ( ph /\ l e. ( 1 ... N ) ) /\ k e. ( 0 ..^ N ) ) -> l e. CC )
23 18 19 22 addlsub 
 |-  ( ( ( ph /\ l e. ( 1 ... N ) ) /\ k e. ( 0 ..^ N ) ) -> ( ( k + 1 ) = l <-> k = ( l - 1 ) ) )
24 15 23 bitr3id 
 |-  ( ( ( ph /\ l e. ( 1 ... N ) ) /\ k e. ( 0 ..^ N ) ) -> ( l = ( k + 1 ) <-> k = ( l - 1 ) ) )
25 14 24 reu6dv 
 |-  ( ( ph /\ l e. ( 1 ... N ) ) -> E! k e. ( 0 ..^ N ) l = ( k + 1 ) )
26 6 1 7 8 2 9 10 4 12 25 gsummptf1o 
 |-  ( ph -> ( R gsum ( l e. ( 1 ... N ) |-> Y ) ) = ( R gsum ( k e. ( 0 ..^ N ) |-> [_ ( k + 1 ) / l ]_ Y ) ) )
27 12 5 csbied 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> [_ ( k + 1 ) / l ]_ Y = X )
28 27 mpteq2dva 
 |-  ( ph -> ( k e. ( 0 ..^ N ) |-> [_ ( k + 1 ) / l ]_ Y ) = ( k e. ( 0 ..^ N ) |-> X ) )
29 28 oveq2d 
 |-  ( ph -> ( R gsum ( k e. ( 0 ..^ N ) |-> [_ ( k + 1 ) / l ]_ Y ) ) = ( R gsum ( k e. ( 0 ..^ N ) |-> X ) ) )
30 26 29 eqtr2d 
 |-  ( ph -> ( R gsum ( k e. ( 0 ..^ N ) |-> X ) ) = ( R gsum ( l e. ( 1 ... N ) |-> Y ) ) )