Theorem submmulgcl

Description: Closure of the group multiple (exponentiation) operation in a submonoid. (Contributed by Mario Carneiro, 13-Jan-2015)

	Ref	Expression
Hypothesis	submmulgcl.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_G$$
Assertion	submmulgcl	$$⊢\left(S\in \mathrm{SubMnd}\left(G\right)\wedge N\in {\mathbb{N}}_0\wedge X\in S\right)\to N\underset{\dot{}}{\bullet }X\in S$$

Proof

Step	Hyp	Ref	Expression
1		submmulgcl.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_G$$
2		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
3		eqid	$$⊢{+}_G={+}_G$$
4		submrcl	$$⊢S\in \mathrm{SubMnd}\left(G\right)\to G\in \mathrm{Mnd}$$
5	2	submss	$$⊢S\in \mathrm{SubMnd}\left(G\right)\to S\subseteq {\mathrm{Base}}_G$$
6	3	submcl	$$⊢\left(S\in \mathrm{SubMnd}\left(G\right)\wedge x\in S\wedge y\in S\right)\to x{+}_{G}y\in S$$
7		eqid	$$⊢0_G=0_G$$
8	7	subm0cl	$$⊢S\in \mathrm{SubMnd}\left(G\right)\to 0_G\in S$$
9	2 1 3 4 5 6 7 8	mulgnn0subcl	$$⊢\left(S\in \mathrm{SubMnd}\left(G\right)\wedge N\in {\mathbb{N}}_0\wedge X\in S\right)\to N\underset{\dot{}}{\bullet }X\in S$$