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 fzssp1 
 |-  ( N ... P ) C_ ( N ... ( P + 1 ) )
25 resmpt 
 |-  ( ( N ... P ) C_ ( N ... ( P + 1 ) ) -> ( ( k e. ( N ... ( P + 1 ) ) |-> B ) |` ( N ... P ) ) = ( k e. ( N ... P ) |-> B ) )
26 24 25 ax-mp 
 |-  ( ( k e. ( N ... ( P + 1 ) ) |-> B ) |` ( N ... P ) ) = ( k e. ( N ... P ) |-> B )
27 26 fveq1i 
 |-  ( ( ( k e. ( N ... ( P + 1 ) ) |-> B ) |` ( N ... P ) ) ` i ) = ( ( k e. ( N ... P ) |-> B ) ` i )
28 fvres 
 |-  ( i e. ( N ... P ) -> ( ( ( k e. ( N ... ( P + 1 ) ) |-> B ) |` ( N ... P ) ) ` i ) = ( ( k e. ( N ... ( P + 1 ) ) |-> B ) ` i ) )
29 28 adantl 
 |-  ( ( ph /\ i e. ( N ... P ) ) -> ( ( ( k e. ( N ... ( P + 1 ) ) |-> B ) |` ( N ... P ) ) ` i ) = ( ( k e. ( N ... ( P + 1 ) ) |-> B ) ` i ) )
30 27 29 syl5reqr 
 |-  ( ( 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 ) )