Theorem subgmulgcl

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

	Ref	Expression
Hypothesis	subgmulgcl.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
Assertion	subgmulgcl	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge N\in \mathbb{Z}\wedge X\in S\right)\to N\underset{\dot{}}{·}X\in S$$

Proof

Step	Hyp	Ref	Expression
1		subgmulgcl.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
2		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
3		eqid	$$⊢{+}_G={+}_G$$
4		subgrcl	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to G\in \mathrm{Grp}$$
5	2	subgss	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to S\subseteq {\mathrm{Base}}_G$$
6	3	subgcl	$$⊢\left(S\in \mathrm{SubGrp}\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	subg0cl	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to 0_G\in S$$
9		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
10	9	subginvcl	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge x\in S\right)\to {inv}_g\left(G\right)\left(x\right)\in S$$
11	2 1 3 4 5 6 7 8 9 10	mulgsubcl	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge N\in \mathbb{Z}\wedge X\in S\right)\to N\underset{\dot{}}{·}X\in S$$