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 ffvelcdmda 
 |-  ( ( 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 )