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 𝐵 = ( Base ‘ 𝐺 )
mulgnn0cld.t · = ( .g𝐺 )
mulgnn0cld.m ( 𝜑𝐺 ∈ Mnd )
mulgnn0cld.n ( 𝜑𝑁 ∈ ℕ0 )
mulgnn0cld.x ( 𝜑𝑋𝐵 )
Assertion mulgnn0cld ( 𝜑 → ( 𝑁 · 𝑋 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 mulgnn0cld.b 𝐵 = ( Base ‘ 𝐺 )
2 mulgnn0cld.t · = ( .g𝐺 )
3 mulgnn0cld.m ( 𝜑𝐺 ∈ Mnd )
4 mulgnn0cld.n ( 𝜑𝑁 ∈ ℕ0 )
5 mulgnn0cld.x ( 𝜑𝑋𝐵 )
6 1 2 mulgnn0cl ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0𝑋𝐵 ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
7 3 4 5 6 syl3anc ( 𝜑 → ( 𝑁 · 𝑋 ) ∈ 𝐵 )