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=BaseM
omndmul.1 ˙=M
omndmul3.m ·˙=M
omndmul3.0 0˙=0M
omndmul3.o φMoMnd
omndmul3.1 φN0
omndmul3.2 φP0
omndmul3.3 φNP
omndmul3.4 φXB
omndmul3.5 φ0˙˙X
Assertion omndmul3 φN·˙X˙P·˙X

Proof

Step Hyp Ref Expression
1 omndmul.0 B=BaseM
2 omndmul.1 ˙=M
3 omndmul3.m ·˙=M
4 omndmul3.0 0˙=0M
5 omndmul3.o φMoMnd
6 omndmul3.1 φN0
7 omndmul3.2 φP0
8 omndmul3.3 φNP
9 omndmul3.4 φXB
10 omndmul3.5 φ0˙˙X
11 omndmnd MoMndMMnd
12 5 11 syl φMMnd
13 1 4 mndidcl MMnd0˙B
14 12 13 syl φ0˙B
15 nn0sub N0P0NPPN0
16 15 biimpa N0P0NPPN0
17 6 7 8 16 syl21anc φPN0
18 1 3 mulgnn0cl MMndPN0XBPN·˙XB
19 12 17 9 18 syl3anc φPN·˙XB
20 1 3 mulgnn0cl MMndN0XBN·˙XB
21 12 6 9 20 syl3anc φN·˙XB
22 1 2 3 4 omndmul2 MoMndXBPN00˙˙X0˙˙PN·˙X
23 5 9 17 10 22 syl121anc φ0˙˙PN·˙X
24 eqid +M=+M
25 1 2 24 omndadd MoMnd0˙BPN·˙XBN·˙XB0˙˙PN·˙X0˙+MN·˙X˙PN·˙X+MN·˙X
26 5 14 19 21 23 25 syl131anc φ0˙+MN·˙X˙PN·˙X+MN·˙X
27 1 24 4 mndlid MMndN·˙XB0˙+MN·˙X=N·˙X
28 12 21 27 syl2anc φ0˙+MN·˙X=N·˙X
29 1 3 24 mulgnn0dir MMndPN0N0XBP-N+N·˙X=PN·˙X+MN·˙X
30 12 17 6 9 29 syl13anc φP-N+N·˙X=PN·˙X+MN·˙X
31 7 nn0cnd φP
32 6 nn0cnd φN
33 31 32 npcand φP-N+N=P
34 33 oveq1d φP-N+N·˙X=P·˙X
35 30 34 eqtr3d φPN·˙X+MN·˙X=P·˙X
36 26 28 35 3brtr3d φN·˙X˙P·˙X