Theorem mulgnncl

Description: Closure of the group multiple (exponentiation) operation for a positive multiplier in a magma. (Contributed by Mario Carneiro, 11-Dec-2014) (Revised by AV, 29-Aug-2021)

	Ref	Expression
Hypotheses	mulgnncl.b	$$⊢B={\mathrm{Base}}_G$$
	mulgnncl.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
Assertion	mulgnncl	$$⊢\left(G\in \mathrm{Mgm}\wedge N\in \mathbb{N}\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{Mgm}\to G\in \mathrm{Mgm}$$
5		ssidd	$$⊢G\in \mathrm{Mgm}\to B\subseteq B$$
6	1 3	mgmcl	$$⊢\left(G\in \mathrm{Mgm}\wedge x\in B\wedge y\in B\right)\to x{+}_{G}y\in B$$
7	1 2 3 4 5 6	mulgnnsubcl	$$⊢\left(G\in \mathrm{Mgm}\wedge N\in \mathbb{N}\wedge X\in B\right)\to N\underset{\dot{}}{·}X\in B$$