Metamath Proof Explorer


Theorem gsumncl

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 )
Assertion gsumncl
|- ( ph -> ( M gsum ( k e. ( N ... P ) |-> B ) ) e. K )

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 eqid
 |-  ( +g ` M ) = ( +g ` M )
6 4 fmpttd
 |-  ( ph -> ( k e. ( N ... P ) |-> B ) : ( N ... P ) --> K )
7 1 5 2 3 6 gsumval2
 |-  ( ph -> ( M gsum ( k e. ( N ... P ) |-> B ) ) = ( seq N ( ( +g ` M ) , ( k e. ( N ... P ) |-> B ) ) ` P ) )
8 6 ffvelrnda
 |-  ( ( ph /\ x e. ( N ... P ) ) -> ( ( k e. ( N ... P ) |-> B ) ` x ) e. K )
9 2 adantr
 |-  ( ( ph /\ ( x e. K /\ y e. K ) ) -> M e. Mnd )
10 simprl
 |-  ( ( ph /\ ( x e. K /\ y e. K ) ) -> x e. K )
11 simprr
 |-  ( ( ph /\ ( x e. K /\ y e. K ) ) -> y e. K )
12 1 5 mndcl
 |-  ( ( M e. Mnd /\ x e. K /\ y e. K ) -> ( x ( +g ` M ) y ) e. K )
13 9 10 11 12 syl3anc
 |-  ( ( ph /\ ( x e. K /\ y e. K ) ) -> ( x ( +g ` M ) y ) e. K )
14 3 8 13 seqcl
 |-  ( ph -> ( seq N ( ( +g ` M ) , ( k e. ( N ... P ) |-> B ) ) ` P ) e. K )
15 7 14 eqeltrd
 |-  ( ph -> ( M gsum ( k e. ( N ... P ) |-> B ) ) e. K )