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
⊢ 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