Metamath Proof Explorer


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=BaseG
mulgnncl.t ·˙=G
Assertion mulgnn0cl GMndN0XBN·˙XB

Proof

Step Hyp Ref Expression
1 mulgnncl.b B=BaseG
2 mulgnncl.t ·˙=G
3 eqid +G=+G
4 id GMndGMnd
5 ssidd GMndBB
6 1 3 mndcl GMndxByBx+GyB
7 eqid 0G=0G
8 1 7 mndidcl GMnd0GB
9 1 2 3 4 5 6 7 8 mulgnn0subcl GMndN0XBN·˙XB