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{˙}{∙} = \cdot_{G}$
	Assertion	submmulgcl	$⊢ (S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \to N \underset{˙}{∙} X \in S$

Step	Hyp	Ref	Expression
1		submmulgcl.t	$⊢ \underset{˙}{∙} = \cdot_{G}$
2		eqid	$⊢ {Base}_{G} = {Base}_{G}$
3		eqid	$⊢ +_{G} = +_{G}$
4		submrcl	$⊢ S \in SubMnd (G) \to G \in Mnd$
5	2	submss	$⊢ S \in SubMnd (G) \to S \subseteq {Base}_{G}$
6	3	submcl	$⊢ (S \in SubMnd (G) \land x \in S \land y \in S) \to x +_{G} y \in S$
7		eqid	$⊢ 0_{G} = 0_{G}$
8	7	subm0cl	$⊢ S \in SubMnd (G) \to 0_{G} \in S$
9	2 1 3 4 5 6 7 8	mulgnn0subcl	$⊢ (S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \to N \underset{˙}{∙} X \in S$

Metamath Proof Explorer