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 | |
|
omndmul.1 | |
||
omndmul3.m | |
||
omndmul3.0 | |
||
omndmul3.o | |
||
omndmul3.1 | |
||
omndmul3.2 | |
||
omndmul3.3 | |
||
omndmul3.4 | |
||
omndmul3.5 | |
||
Assertion | omndmul3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | omndmul.0 | |
|
2 | omndmul.1 | |
|
3 | omndmul3.m | |
|
4 | omndmul3.0 | |
|
5 | omndmul3.o | |
|
6 | omndmul3.1 | |
|
7 | omndmul3.2 | |
|
8 | omndmul3.3 | |
|
9 | omndmul3.4 | |
|
10 | omndmul3.5 | |
|
11 | omndmnd | |
|
12 | 5 11 | syl | |
13 | 1 4 | mndidcl | |
14 | 12 13 | syl | |
15 | nn0sub | |
|
16 | 15 | biimpa | |
17 | 6 7 8 16 | syl21anc | |
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 | |
|
25 | 1 2 24 | omndadd | |
26 | 5 14 19 21 23 25 | syl131anc | |
27 | 1 24 4 | mndlid | |
28 | 12 21 27 | syl2anc | |
29 | 1 3 24 | mulgnn0dir | |
30 | 12 17 6 9 29 | syl13anc | |
31 | 7 | nn0cnd | |
32 | 6 | nn0cnd | |
33 | 31 32 | npcand | |
34 | 33 | oveq1d | |
35 | 30 34 | eqtr3d | |
36 | 26 28 35 | 3brtr3d | |