Metamath Proof Explorer


Theorem gsumnunsn

Description: Closure of a group sum in a non-commutative monoid. (Contributed by Thierry Arnoux, 8-Oct-2018)

Ref Expression
Hypotheses gsumncl.k
|- K = ( Base ` M )
gsumncl.w
|- ( ph -> M e. Mnd )
gsumncl.p
|- ( ph -> P e. ( ZZ>= ` N ) )
gsumncl.b
|- ( ( ph /\ k e. ( N ... P ) ) -> B e. K )
gsumnunsn.a
|- .+ = ( +g ` M )
gsumnunsn.l
|- ( ph -> C e. K )
gsumnunsn.c
|- ( ( ph /\ k = ( P + 1 ) ) -> B = C )
Assertion gsumnunsn
|- ( ph -> ( M gsum ( k e. ( N ... ( P + 1 ) ) |-> B ) ) = ( ( M gsum ( k e. ( N ... P ) |-> B ) ) .+ C ) )

Proof

Step Hyp Ref Expression
1 gsumncl.k
 |-  K = ( Base ` M )
2 gsumncl.w
 |-  ( ph -> M e. Mnd )
3 gsumncl.p
 |-  ( ph -> P e. ( ZZ>= ` N ) )
4 gsumncl.b
 |-  ( ( ph /\ k e. ( N ... P ) ) -> B e. K )
5 gsumnunsn.a
 |-  .+ = ( +g ` M )
6 gsumnunsn.l
 |-  ( ph -> C e. K )
7 gsumnunsn.c
 |-  ( ( ph /\ k = ( P + 1 ) ) -> B = C )
8 seqp1
 |-  ( P e. ( ZZ>= ` N ) -> ( seq N ( .+ , ( k e. ( N ... ( P + 1 ) ) |-> B ) ) ` ( P + 1 ) ) = ( ( seq N ( .+ , ( k e. ( N ... ( P + 1 ) ) |-> B ) ) ` P ) .+ ( ( k e. ( N ... ( P + 1 ) ) |-> B ) ` ( P + 1 ) ) ) )
9 3 8 syl
 |-  ( ph -> ( seq N ( .+ , ( k e. ( N ... ( P + 1 ) ) |-> B ) ) ` ( P + 1 ) ) = ( ( seq N ( .+ , ( k e. ( N ... ( P + 1 ) ) |-> B ) ) ` P ) .+ ( ( k e. ( N ... ( P + 1 ) ) |-> B ) ` ( P + 1 ) ) ) )
10 peano2uz
 |-  ( P e. ( ZZ>= ` N ) -> ( P + 1 ) e. ( ZZ>= ` N ) )
11 3 10 syl
 |-  ( ph -> ( P + 1 ) e. ( ZZ>= ` N ) )
12 4 adantlr
 |-  ( ( ( ph /\ k e. ( N ... ( P + 1 ) ) ) /\ k e. ( N ... P ) ) -> B e. K )
13 7 adantlr
 |-  ( ( ( ph /\ k e. ( N ... ( P + 1 ) ) ) /\ k = ( P + 1 ) ) -> B = C )
14 6 ad2antrr
 |-  ( ( ( ph /\ k e. ( N ... ( P + 1 ) ) ) /\ k = ( P + 1 ) ) -> C e. K )
15 13 14 eqeltrd
 |-  ( ( ( ph /\ k e. ( N ... ( P + 1 ) ) ) /\ k = ( P + 1 ) ) -> B e. K )
16 elfzp1
 |-  ( P e. ( ZZ>= ` N ) -> ( k e. ( N ... ( P + 1 ) ) <-> ( k e. ( N ... P ) \/ k = ( P + 1 ) ) ) )
17 3 16 syl
 |-  ( ph -> ( k e. ( N ... ( P + 1 ) ) <-> ( k e. ( N ... P ) \/ k = ( P + 1 ) ) ) )
18 17 biimpa
 |-  ( ( ph /\ k e. ( N ... ( P + 1 ) ) ) -> ( k e. ( N ... P ) \/ k = ( P + 1 ) ) )
19 12 15 18 mpjaodan
 |-  ( ( ph /\ k e. ( N ... ( P + 1 ) ) ) -> B e. K )
20 19 fmpttd
 |-  ( ph -> ( k e. ( N ... ( P + 1 ) ) |-> B ) : ( N ... ( P + 1 ) ) --> K )
21 1 5 2 11 20 gsumval2
 |-  ( ph -> ( M gsum ( k e. ( N ... ( P + 1 ) ) |-> B ) ) = ( seq N ( .+ , ( k e. ( N ... ( P + 1 ) ) |-> B ) ) ` ( P + 1 ) ) )
22 4 fmpttd
 |-  ( ph -> ( k e. ( N ... P ) |-> B ) : ( N ... P ) --> K )
23 1 5 2 3 22 gsumval2
 |-  ( ph -> ( M gsum ( k e. ( N ... P ) |-> B ) ) = ( seq N ( .+ , ( k e. ( N ... P ) |-> B ) ) ` P ) )
24 fvres
 |-  ( i e. ( N ... P ) -> ( ( ( k e. ( N ... ( P + 1 ) ) |-> B ) |` ( N ... P ) ) ` i ) = ( ( k e. ( N ... ( P + 1 ) ) |-> B ) ` i ) )
25 24 adantl
 |-  ( ( ph /\ i e. ( N ... P ) ) -> ( ( ( k e. ( N ... ( P + 1 ) ) |-> B ) |` ( N ... P ) ) ` i ) = ( ( k e. ( N ... ( P + 1 ) ) |-> B ) ` i ) )
26 fzssp1
 |-  ( N ... P ) C_ ( N ... ( P + 1 ) )
27 resmpt
 |-  ( ( N ... P ) C_ ( N ... ( P + 1 ) ) -> ( ( k e. ( N ... ( P + 1 ) ) |-> B ) |` ( N ... P ) ) = ( k e. ( N ... P ) |-> B ) )
28 26 27 ax-mp
 |-  ( ( k e. ( N ... ( P + 1 ) ) |-> B ) |` ( N ... P ) ) = ( k e. ( N ... P ) |-> B )
29 28 fveq1i
 |-  ( ( ( k e. ( N ... ( P + 1 ) ) |-> B ) |` ( N ... P ) ) ` i ) = ( ( k e. ( N ... P ) |-> B ) ` i )
30 25 29 eqtr3di
 |-  ( ( ph /\ i e. ( N ... P ) ) -> ( ( k e. ( N ... ( P + 1 ) ) |-> B ) ` i ) = ( ( k e. ( N ... P ) |-> B ) ` i ) )
31 3 30 seqfveq
 |-  ( ph -> ( seq N ( .+ , ( k e. ( N ... ( P + 1 ) ) |-> B ) ) ` P ) = ( seq N ( .+ , ( k e. ( N ... P ) |-> B ) ) ` P ) )
32 23 31 eqtr4d
 |-  ( ph -> ( M gsum ( k e. ( N ... P ) |-> B ) ) = ( seq N ( .+ , ( k e. ( N ... ( P + 1 ) ) |-> B ) ) ` P ) )
33 eqidd
 |-  ( ph -> ( k e. ( N ... ( P + 1 ) ) |-> B ) = ( k e. ( N ... ( P + 1 ) ) |-> B ) )
34 eluzfz2
 |-  ( ( P + 1 ) e. ( ZZ>= ` N ) -> ( P + 1 ) e. ( N ... ( P + 1 ) ) )
35 11 34 syl
 |-  ( ph -> ( P + 1 ) e. ( N ... ( P + 1 ) ) )
36 33 7 35 6 fvmptd
 |-  ( ph -> ( ( k e. ( N ... ( P + 1 ) ) |-> B ) ` ( P + 1 ) ) = C )
37 36 eqcomd
 |-  ( ph -> C = ( ( k e. ( N ... ( P + 1 ) ) |-> B ) ` ( P + 1 ) ) )
38 32 37 oveq12d
 |-  ( ph -> ( ( M gsum ( k e. ( N ... P ) |-> B ) ) .+ C ) = ( ( seq N ( .+ , ( k e. ( N ... ( P + 1 ) ) |-> B ) ) ` P ) .+ ( ( k e. ( N ... ( P + 1 ) ) |-> B ) ` ( P + 1 ) ) ) )
39 9 21 38 3eqtr4d
 |-  ( ph -> ( M gsum ( k e. ( N ... ( P + 1 ) ) |-> B ) ) = ( ( M gsum ( k e. ( N ... P ) |-> B ) ) .+ C ) )