Database
BASIC ALGEBRAIC STRUCTURES
Groups
Group multiple operation
mulgnn0cld
Metamath Proof Explorer
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
⊢ ( 𝜑 → ( 𝑁 · 𝑋 ) ∈ 𝐵 )