# Metamath Proof Explorer

## Theorem omndmul3

Description: In an ordered monoid, the ordering is compatible with group power. This version does not require the monoid to be commutative. (Contributed by Thierry Arnoux, 23-Mar-2018)

Ref Expression
Hypotheses omndmul.0 ${⊢}{B}={\mathrm{Base}}_{{M}}$
omndmul.1
omndmul3.m
omndmul3.0
omndmul3.o ${⊢}{\phi }\to {M}\in \mathrm{oMnd}$
omndmul3.1 ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
omndmul3.2 ${⊢}{\phi }\to {P}\in {ℕ}_{0}$
omndmul3.3 ${⊢}{\phi }\to {N}\le {P}$
omndmul3.4 ${⊢}{\phi }\to {X}\in {B}$
omndmul3.5
Assertion omndmul3

### Proof

Step Hyp Ref Expression
1 omndmul.0 ${⊢}{B}={\mathrm{Base}}_{{M}}$
2 omndmul.1
3 omndmul3.m
4 omndmul3.0
5 omndmul3.o ${⊢}{\phi }\to {M}\in \mathrm{oMnd}$
6 omndmul3.1 ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
7 omndmul3.2 ${⊢}{\phi }\to {P}\in {ℕ}_{0}$
8 omndmul3.3 ${⊢}{\phi }\to {N}\le {P}$
9 omndmul3.4 ${⊢}{\phi }\to {X}\in {B}$
10 omndmul3.5
11 omndmnd ${⊢}{M}\in \mathrm{oMnd}\to {M}\in \mathrm{Mnd}$
12 5 11 syl ${⊢}{\phi }\to {M}\in \mathrm{Mnd}$
13 1 4 mndidcl
14 12 13 syl
15 nn0sub ${⊢}\left({N}\in {ℕ}_{0}\wedge {P}\in {ℕ}_{0}\right)\to \left({N}\le {P}↔{P}-{N}\in {ℕ}_{0}\right)$
16 15 biimpa ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge {P}\in {ℕ}_{0}\right)\wedge {N}\le {P}\right)\to {P}-{N}\in {ℕ}_{0}$
17 6 7 8 16 syl21anc ${⊢}{\phi }\to {P}-{N}\in {ℕ}_{0}$
18 1 3 mulgnn0cl
19 12 17 9 18 syl3anc
20 1 3 mulgnn0cl
21 12 6 9 20 syl3anc
22 1 2 3 4 omndmul2
23 5 9 17 10 22 syl121anc
24 eqid ${⊢}{+}_{{M}}={+}_{{M}}$
31 7 nn0cnd ${⊢}{\phi }\to {P}\in ℂ$
32 6 nn0cnd ${⊢}{\phi }\to {N}\in ℂ$
33 31 32 npcand ${⊢}{\phi }\to {P}-{N}+{N}={P}$