Theorem mulgcl

Description: Closure of the group multiple (exponentiation) operation. (Contributed by Mario Carneiro, 11-Dec-2014)

	Ref	Expression
Hypotheses	mulgnncl.b	|- B = ( Base ` G )
	mulgnncl.t	|- .x. = ( .g ` G )
Assertion	mulgcl	|- ( ( G e. Grp /\ N e. ZZ /\ 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. Grp -> G e. Grp )
5		ssidd	|- ( G e. Grp -> B C_ B )
6	1 3	grpcl	|- ( ( G e. Grp /\ x e. B /\ y e. B ) -> ( x ( +g ` G ) y ) e. B )
7		eqid	|- ( 0g ` G ) = ( 0g ` G )
8	1 7	grpidcl	|- ( G e. Grp -> ( 0g ` G ) e. B )
9		eqid	|- ( invg ` G ) = ( invg ` G )
10	1 9	grpinvcl	|- ( ( G e. Grp /\ x e. B ) -> ( ( invg ` G ) ` x ) e. B )
11	1 2 3 4 5 6 7 8 9 10	mulgsubcl	|- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( N .x. X ) e. B )