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 ˙=G
Assertion submmulgcl SSubMndGN0XSN˙XS

Proof

Step Hyp Ref Expression
1 submmulgcl.t ˙=G
2 eqid BaseG=BaseG
3 eqid +G=+G
4 submrcl SSubMndGGMnd
5 2 submss SSubMndGSBaseG
6 3 submcl SSubMndGxSySx+GyS
7 eqid 0G=0G
8 7 subm0cl SSubMndG0GS
9 2 1 3 4 5 6 7 8 mulgnn0subcl SSubMndGN0XSN˙XS