# Metamath Proof Explorer

## Theorem omndmul2

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
omndmul2.2
omndmul2.3
Assertion omndmul2

### Proof

Step Hyp Ref Expression
1 omndmul.0 ${⊢}{B}={\mathrm{Base}}_{{M}}$
2 omndmul.1
3 omndmul2.2
4 omndmul2.3
5 df-3an
6 anass ${⊢}\left(\left({M}\in \mathrm{oMnd}\wedge {X}\in {B}\right)\wedge {N}\in {ℕ}_{0}\right)↔\left({M}\in \mathrm{oMnd}\wedge \left({X}\in {B}\wedge {N}\in {ℕ}_{0}\right)\right)$
7 6 anbi1i
8 5 7 bitr4i
9 simplr
10 oveq1
11 10 breq2d
12 oveq1
13 12 breq2d
14 oveq1
15 14 breq2d
16 oveq1
17 16 breq2d
18 omndtos ${⊢}{M}\in \mathrm{oMnd}\to {M}\in \mathrm{Toset}$
19 tospos ${⊢}{M}\in \mathrm{Toset}\to {M}\in \mathrm{Poset}$
20 18 19 syl ${⊢}{M}\in \mathrm{oMnd}\to {M}\in \mathrm{Poset}$
21 omndmnd ${⊢}{M}\in \mathrm{oMnd}\to {M}\in \mathrm{Mnd}$
22 1 4 mndidcl
23 21 22 syl
24 1 2 posref
25 20 23 24 syl2anc
27 1 4 3 mulg0
29 26 28 breqtrrd
32 31 22 syl
33 simplr
34 simp-5r
35 1 3 mulgnn0cl
36 31 33 34 35 syl3anc
37 simpr32
38 1nn0 ${⊢}1\in {ℕ}_{0}$
39 38 a1i
41 40 3anassrs
42 41 3anassrs
43 1 3 mulgnn0cl
44 31 42 34 43 syl3anc
45 32 36 44 3jca
46 simpr
47 simp-4l
49 48 22 syl
50 simp-4r
51 simpr
52 48 51 50 35 syl3anc
53 simplr
54 eqid ${⊢}{+}_{{M}}={+}_{{M}}$
56 47 49 50 52 53 55 syl131anc
57 1 54 4 mndlid
58 48 52 57 syl2anc
59 38 a1i
60 1 3 54 mulgnn0dir
61 48 59 51 50 60 syl13anc
62 1cnd
63 simpr3
64 63 nn0cnd
66 65 3anassrs
67 66 oveq1d
68 1 3 mulg1
69 50 68 syl
70 69 oveq1d
71 61 67 70 3eqtr3rd
72 56 58 71 3brtr3d