# Metamath Proof Explorer

## Theorem omndmul

Description: In a commutative ordered monoid, the ordering is compatible with group power. (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Hypotheses omndmul.0 ${⊢}{B}={\mathrm{Base}}_{{M}}$
omndmul.1
omndmul.2
omndmul.o ${⊢}{\phi }\to {M}\in \mathrm{oMnd}$
omndmul.c ${⊢}{\phi }\to {M}\in \mathrm{CMnd}$
omndmul.x ${⊢}{\phi }\to {X}\in {B}$
omndmul.y ${⊢}{\phi }\to {Y}\in {B}$
omndmul.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
omndmul.l
Assertion omndmul

### Proof

Step Hyp Ref Expression
1 omndmul.0 ${⊢}{B}={\mathrm{Base}}_{{M}}$
2 omndmul.1
3 omndmul.2
4 omndmul.o ${⊢}{\phi }\to {M}\in \mathrm{oMnd}$
5 omndmul.c ${⊢}{\phi }\to {M}\in \mathrm{CMnd}$
6 omndmul.x ${⊢}{\phi }\to {X}\in {B}$
7 omndmul.y ${⊢}{\phi }\to {Y}\in {B}$
8 omndmul.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
9 omndmul.l
10 oveq1
11 oveq1
12 10 11 breq12d
13 oveq1
14 oveq1
15 13 14 breq12d
16 oveq1
17 oveq1
18 16 17 breq12d
19 oveq1
20 oveq1
21 19 20 breq12d
22 omndtos ${⊢}{M}\in \mathrm{oMnd}\to {M}\in \mathrm{Toset}$
23 tospos ${⊢}{M}\in \mathrm{Toset}\to {M}\in \mathrm{Poset}$
24 4 22 23 3syl ${⊢}{\phi }\to {M}\in \mathrm{Poset}$
25 eqid ${⊢}{0}_{{M}}={0}_{{M}}$
26 1 25 3 mulg0
27 7 26 syl
28 omndmnd ${⊢}{M}\in \mathrm{oMnd}\to {M}\in \mathrm{Mnd}$
29 1 25 mndidcl ${⊢}{M}\in \mathrm{Mnd}\to {0}_{{M}}\in {B}$
30 4 28 29 3syl ${⊢}{\phi }\to {0}_{{M}}\in {B}$
31 27 30 eqeltrd
32 1 2 posref
33 24 31 32 syl2anc
34 1 25 3 mulg0
37 35 36 eqtr4d
38 37 breq1d
39 6 7 38 syl2anc
40 33 39 mpbird
41 eqid ${⊢}{+}_{{M}}={+}_{{M}}$
44 42 28 syl
45 simplr
47 1 3 mulgnn0cl
48 44 45 46 47 syl3anc
49 1 3 mulgnn0cl
50 44 45 43 49 syl3anc
51 simpr