Theorem mulgnn0cl

Description: Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. (Contributed by Mario Carneiro, 11-Dec-2014)

	Ref	Expression
Hypotheses	mulgnncl.b	$$⊢B={\mathrm{Base}}_G$$
	mulgnncl.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
Assertion	mulgnn0cl	$$⊢\left(G\in \mathrm{Mnd}\wedge N\in {\mathbb{N}}_0\wedge X\in B\right)\to N\underset{\dot{}}{·}X\in B$$

Proof

Step	Hyp	Ref	Expression
1		mulgnncl.b	$$⊢B={\mathrm{Base}}_G$$
2		mulgnncl.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		eqid	$$⊢{+}_G={+}_G$$
4		id	$$⊢G\in \mathrm{Mnd}\to G\in \mathrm{Mnd}$$
5		ssidd	$$⊢G\in \mathrm{Mnd}\to B\subseteq B$$
6	1 3	mndcl	$$⊢\left(G\in \mathrm{Mnd}\wedge x\in B\wedge y\in B\right)\to x{+}_{G}y\in B$$
7		eqid	$$⊢0_G=0_G$$
8	1 7	mndidcl	$$⊢G\in \mathrm{Mnd}\to 0_G\in B$$
9	1 2 3 4 5 6 7 8	mulgnn0subcl	$$⊢\left(G\in \mathrm{Mnd}\wedge N\in {\mathbb{N}}_0\wedge X\in B\right)\to N\underset{\dot{}}{·}X\in B$$