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={\mathrm{Base}}_M$$
	gsumncl.w	$$⊢\phi \to M\in \mathrm{Mnd}$$
	gsumncl.p	$$⊢\phi \to P\in {\mathbb{Z}}_{\ge N}$$
	gsumncl.b	$$⊢\left(\phi \wedge k\in \left(N\dots P\right)\right)\to B\in K$$
Assertion	gsumncl	$$⊢\phi \to \underset{k=N}{\overset{P}{{\sum }_M}}B\in K$$

Proof

Step	Hyp	Ref	Expression
1		gsumncl.k	$$⊢K={\mathrm{Base}}_M$$
2		gsumncl.w	$$⊢\phi \to M\in \mathrm{Mnd}$$
3		gsumncl.p	$$⊢\phi \to P\in {\mathbb{Z}}_{\ge N}$$
4		gsumncl.b	$$⊢\left(\phi \wedge k\in \left(N\dots P\right)\right)\to B\in K$$
5		eqid	$$⊢{+}_M={+}_M$$
6	4	fmpttd	$$⊢\phi \to \left(k\in \left(N\dots P\right)⟼B\right):\left(N\dots P\right)⟶K$$
7	1 5 2 3 6	gsumval2	$$⊢\phi \to \underset{k=N}{\overset{P}{{\sum }_M}}B=seqN\left({+}_M,\left(k\in \left(N\dots P\right)⟼B\right)\right)\left(P\right)$$
8	6	ffvelrnda	$$⊢\left(\phi \wedge x\in \left(N\dots P\right)\right)\to \left(k\in \left(N\dots P\right)⟼B\right)\left(x\right)\in K$$
9	2	adantr	$$⊢\left(\phi \wedge \left(x\in K\wedge y\in K\right)\right)\to M\in \mathrm{Mnd}$$
10		simprl	$$⊢\left(\phi \wedge \left(x\in K\wedge y\in K\right)\right)\to x\in K$$
11		simprr	$$⊢\left(\phi \wedge \left(x\in K\wedge y\in K\right)\right)\to y\in K$$
12	1 5	mndcl	$$⊢\left(M\in \mathrm{Mnd}\wedge x\in K\wedge y\in K\right)\to x{+}_{M}y\in K$$
13	9 10 11 12	syl3anc	$$⊢\left(\phi \wedge \left(x\in K\wedge y\in K\right)\right)\to x{+}_{M}y\in K$$
14	3 8 13	seqcl	$$⊢\phi \to seqN\left({+}_M,\left(k\in \left(N\dots P\right)⟼B\right)\right)\left(P\right)\in K$$
15	7 14	eqeltrd	$$⊢\phi \to \underset{k=N}{\overset{P}{{\sum }_M}}B\in K$$