| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > mulgnn0cld | Structured version Visualization version GIF version | ||
| Description: Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. Deduction associated with mulgnn0cl 19108. (Contributed by SN, 1-Feb-2025.) |
| Ref | Expression |
|---|---|
| mulgnn0cld.b | ⊢ 𝐵 = (Base‘𝐺) |
| mulgnn0cld.t | ⊢ · = (.g‘𝐺) |
| mulgnn0cld.m | ⊢ (𝜑 → 𝐺 ∈ Mnd) |
| mulgnn0cld.n | ⊢ (𝜑 → 𝑁 ∈ ℕ0) |
| mulgnn0cld.x | ⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| Ref | Expression |
|---|---|
| mulgnn0cld | ⊢ (𝜑 → (𝑁 · 𝑋) ∈ 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mulgnn0cld.m | . 2 ⊢ (𝜑 → 𝐺 ∈ Mnd) | |
| 2 | mulgnn0cld.n | . 2 ⊢ (𝜑 → 𝑁 ∈ ℕ0) | |
| 3 | mulgnn0cld.x | . 2 ⊢ (𝜑 → 𝑋 ∈ 𝐵) | |
| 4 | mulgnn0cld.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
| 5 | mulgnn0cld.t | . . 3 ⊢ · = (.g‘𝐺) | |
| 6 | 4, 5 | mulgnn0cl 19108 | . 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵) |
| 7 | 1, 2, 3, 6 | syl3anc 1373 | 1 ⊢ (𝜑 → (𝑁 · 𝑋) ∈ 𝐵) |
| Copyright terms: Public domain | W3C validator |