Metamath Proof Explorer

Theorem gsummptrev

Description: Revert ordering in a group sum. See also gsumwrev . (Contributed by Thierry Arnoux, 15-Feb-2026)

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

Proof

Step Hyp Ref Expression
1 gsummptrev.1 
 |-  B = ( Base ` M )
2 gsummptrev.2 
 |-  ( ph -> M e. CMnd )
3 gsummptrev.3 
 |-  ( ph -> N e. NN0 )
4 gsummptrev.4 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> X e. B )
5 gsummptrev.5 
 |-  ( ( ( ph /\ l e. ( 0 ... N ) ) /\ k = ( N - l ) ) -> X = Y )
6 nfcv 
 |-  F/_ k Y
7 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
8 fzfid 
 |-  ( ph -> ( 0 ... N ) e. Fin )
9 ssidd 
 |-  ( ph -> B C_ B )
10 fznn0sub2 
 |-  ( l e. ( 0 ... N ) -> ( N - l ) e. ( 0 ... N ) )
11 10 adantl 
 |-  ( ( ph /\ l e. ( 0 ... N ) ) -> ( N - l ) e. ( 0 ... N ) )
12 fznn0sub2 
 |-  ( k e. ( 0 ... N ) -> ( N - k ) e. ( 0 ... N ) )
13 12 adantl 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( N - k ) e. ( 0 ... N ) )
14 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
15 14 ad2antlr 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ l e. ( 0 ... N ) ) -> k e. NN0 )
16 15 nn0cnd 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ l e. ( 0 ... N ) ) -> k e. CC )
17 elfznn0 
 |-  ( l e. ( 0 ... N ) -> l e. NN0 )
18 17 adantl 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ l e. ( 0 ... N ) ) -> l e. NN0 )
19 18 nn0cnd 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ l e. ( 0 ... N ) ) -> l e. CC )
20 3 ad2antrr 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ l e. ( 0 ... N ) ) -> N e. NN0 )
21 20 nn0cnd 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ l e. ( 0 ... N ) ) -> N e. CC )
22 16 19 21 subexsub 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ l e. ( 0 ... N ) ) -> ( k = ( N - l ) <-> l = ( N - k ) ) )
23 13 22 reu6dv 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> E! l e. ( 0 ... N ) k = ( N - l ) )
24 6 1 7 5 2 8 9 4 11 23 gsummptf1od 
 |-  ( ph -> ( M gsum ( k e. ( 0 ... N ) |-> X ) ) = ( M gsum ( l e. ( 0 ... N ) |-> Y ) ) )