Theorem mulgcl

Description: Closure of the group multiple (exponentiation) operation. (Contributed by Mario Carneiro, 11-Dec-2014)

	Ref	Expression
Hypotheses	mulgnncl.b	$$⊢B={\mathrm{Base}}_G$$
	mulgnncl.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
Assertion	mulgcl	$$⊢\left(G\in \mathrm{Grp}\wedge N\in \mathbb{Z}\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{Grp}\to G\in \mathrm{Grp}$$
5		ssidd	$$⊢G\in \mathrm{Grp}\to B\subseteq B$$
6	1 3	grpcl	$$⊢\left(G\in \mathrm{Grp}\wedge x\in B\wedge y\in B\right)\to x{+}_{G}y\in B$$
7		eqid	$$⊢0_G=0_G$$
8	1 7	grpidcl	$$⊢G\in \mathrm{Grp}\to 0_G\in B$$
9		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
10	1 9	grpinvcl	$$⊢\left(G\in \mathrm{Grp}\wedge x\in B\right)\to {inv}_g\left(G\right)\left(x\right)\in B$$
11	1 2 3 4 5 6 7 8 9 10	mulgsubcl	$$⊢\left(G\in \mathrm{Grp}\wedge N\in \mathbb{Z}\wedge X\in B\right)\to N\underset{\dot{}}{·}X\in B$$