This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )