Theorem mulgnn0cl

Description: Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. (Contributed by Mario Carneiro, 11-Dec-2014)

	Ref	Expression
Hypotheses	mulgnncl.b	|- B = ( Base ` G )
	mulgnncl.t	|- .x. = ( .g ` G )
Assertion	mulgnn0cl	|- ( ( G e. Mnd /\ N e. NN0 /\ X e. B ) -> ( N .x. X ) e. B )

Proof

Step	Hyp	Ref	Expression
1		mulgnncl.b	|- B = ( Base ` G )
2		mulgnncl.t	|- .x. = ( .g ` G )
3		eqid	|- ( +g ` G ) = ( +g ` G )
4		id	|- ( G e. Mnd -> G e. Mnd )
5		ssidd	|- ( G e. Mnd -> B C_ B )
6	1 3	mndcl	|- ( ( G e. Mnd /\ x e. B /\ y e. B ) -> ( x ( +g ` G ) y ) e. B )
7		eqid	|- ( 0g ` G ) = ( 0g ` G )
8	1 7	mndidcl	|- ( G e. Mnd -> ( 0g ` G ) e. B )
9	1 2 3 4 5 6 7 8	mulgnn0subcl	|- ( ( G e. Mnd /\ N e. NN0 /\ X e. B ) -> ( N .x. X ) e. B )