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{˙}{\cdot} = \cdot_{G}$
	Assertion	subgmulgcl	$⊢ (S \in SubGrp (G) \land N \in ℤ \land X \in S) \to N \underset{˙}{\cdot} X \in S$

Step	Hyp	Ref	Expression
1		subgmulgcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
2		eqid	$⊢ {Base}_{G} = {Base}_{G}$
3		eqid	$⊢ +_{G} = +_{G}$
4		subgrcl	$⊢ S \in SubGrp (G) \to G \in Grp$
5	2	subgss	$⊢ S \in SubGrp (G) \to S \subseteq {Base}_{G}$
6	3	subgcl	$⊢ (S \in SubGrp (G) \land x \in S \land y \in S) \to x +_{G} y \in S$
7		eqid	$⊢ 0_{G} = 0_{G}$
8	7	subg0cl	$⊢ S \in SubGrp (G) \to 0_{G} \in S$
9		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
10	9	subginvcl	$⊢ (S \in SubGrp (G) \land x \in S) \to {inv}_{g} (G) (x) \in S$
11	2 1 3 4 5 6 7 8 9 10	mulgsubcl	$⊢ (S \in SubGrp (G) \land N \in ℤ \land X \in S) \to N \underset{˙}{\cdot} X \in S$

Metamath Proof Explorer