Theorem submmulgcl

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

	Ref	Expression
Hypothesis	submmulgcl.t	|- .xb = ( .g ` G )
Assertion	submmulgcl	|- ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) -> ( N .xb X ) e. S )

Proof

Step	Hyp	Ref	Expression
1		submmulgcl.t	|- .xb = ( .g ` G )
2		eqid	|- ( Base ` G ) = ( Base ` G )
3		eqid	|- ( +g ` G ) = ( +g ` G )
4		submrcl	|- ( S e. ( SubMnd ` G ) -> G e. Mnd )
5	2	submss	|- ( S e. ( SubMnd ` G ) -> S C_ ( Base ` G ) )
6	3	submcl	|- ( ( S e. ( SubMnd ` G ) /\ x e. S /\ y e. S ) -> ( x ( +g ` G ) y ) e. S )
7		eqid	|- ( 0g ` G ) = ( 0g ` G )
8	7	subm0cl	|- ( S e. ( SubMnd ` G ) -> ( 0g ` G ) e. S )
9	2 1 3 4 5 6 7 8	mulgnn0subcl	|- ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) -> ( N .xb X ) e. S )