Metamath Proof Explorer


Theorem mulgnn0cld

Description: Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. Deduction associated with mulgnn0cl . (Contributed by SN, 1-Feb-2025)

Ref Expression
Hypotheses mulgnn0cld.b B = Base G
mulgnn0cld.t · ˙ = G
mulgnn0cld.m φ G Mnd
mulgnn0cld.n φ N 0
mulgnn0cld.x φ X B
Assertion mulgnn0cld φ N · ˙ X B

Proof

Step Hyp Ref Expression
1 mulgnn0cld.b B = Base G
2 mulgnn0cld.t · ˙ = G
3 mulgnn0cld.m φ G Mnd
4 mulgnn0cld.n φ N 0
5 mulgnn0cld.x φ X B
6 1 2 mulgnn0cl G Mnd N 0 X B N · ˙ X B
7 3 4 5 6 syl3anc φ N · ˙ X B