Metamath Proof Explorer

Theorem subgmulgcl

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

Ref Expression
Hypothesis subgmulgcl.t 
|- .x. = ( .g ` G )
Assertion subgmulgcl 
|- ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> ( N .x. X ) e. S )

Proof

Step Hyp Ref Expression
1 subgmulgcl.t 
 |-  .x. = ( .g ` G )
2 eqid 
 |-  ( Base ` G ) = ( Base ` G )
3 eqid 
 |-  ( +g ` G ) = ( +g ` G )
4 subgrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
5 2 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ ( Base ` G ) )
6 3 subgcl 
 |-  ( ( S e. ( SubGrp ` G ) /\ x e. S /\ y e. S ) -> ( x ( +g ` G ) y ) e. S )
7 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
8 7 subg0cl 
 |-  ( S e. ( SubGrp ` G ) -> ( 0g ` G ) e. S )
9 eqid 
 |-  ( invg ` G ) = ( invg ` G )
10 9 subginvcl 
 |-  ( ( S e. ( SubGrp ` G ) /\ x e. S ) -> ( ( invg ` G ) ` x ) e. S )
11 2 1 3 4 5 6 7 8 9 10 mulgsubcl 
 |-  ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> ( N .x. X ) e. S )