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 = ( Base ` M )
omndmul.1
|- .<_ = ( le ` M )
omndmul3.m
|- .x. = ( .g ` M )
omndmul3.0
|- .0. = ( 0g ` M )
omndmul3.o
|- ( ph -> M e. oMnd )
omndmul3.1
|- ( ph -> N e. NN0 )
omndmul3.2
|- ( ph -> P e. NN0 )
omndmul3.3
|- ( ph -> N <_ P )
omndmul3.4
|- ( ph -> X e. B )
omndmul3.5
|- ( ph -> .0. .<_ X )
Assertion omndmul3
|- ( ph -> ( N .x. X ) .<_ ( P .x. X ) )

Proof

Step Hyp Ref Expression
1 omndmul.0
 |-  B = ( Base ` M )
2 omndmul.1
 |-  .<_ = ( le ` M )
3 omndmul3.m
 |-  .x. = ( .g ` M )
4 omndmul3.0
 |-  .0. = ( 0g ` M )
5 omndmul3.o
 |-  ( ph -> M e. oMnd )
6 omndmul3.1
 |-  ( ph -> N e. NN0 )
7 omndmul3.2
 |-  ( ph -> P e. NN0 )
8 omndmul3.3
 |-  ( ph -> N <_ P )
9 omndmul3.4
 |-  ( ph -> X e. B )
10 omndmul3.5
 |-  ( ph -> .0. .<_ X )
11 omndmnd
 |-  ( M e. oMnd -> M e. Mnd )
12 5 11 syl
 |-  ( ph -> M e. Mnd )
13 1 4 mndidcl
 |-  ( M e. Mnd -> .0. e. B )
14 12 13 syl
 |-  ( ph -> .0. e. B )
15 nn0sub
 |-  ( ( N e. NN0 /\ P e. NN0 ) -> ( N <_ P <-> ( P - N ) e. NN0 ) )
16 15 biimpa
 |-  ( ( ( N e. NN0 /\ P e. NN0 ) /\ N <_ P ) -> ( P - N ) e. NN0 )
17 6 7 8 16 syl21anc
 |-  ( ph -> ( P - N ) e. NN0 )
18 1 3 mulgnn0cl
 |-  ( ( M e. Mnd /\ ( P - N ) e. NN0 /\ X e. B ) -> ( ( P - N ) .x. X ) e. B )
19 12 17 9 18 syl3anc
 |-  ( ph -> ( ( P - N ) .x. X ) e. B )
20 1 3 mulgnn0cl
 |-  ( ( M e. Mnd /\ N e. NN0 /\ X e. B ) -> ( N .x. X ) e. B )
21 12 6 9 20 syl3anc
 |-  ( ph -> ( N .x. X ) e. B )
22 1 2 3 4 omndmul2
 |-  ( ( M e. oMnd /\ ( X e. B /\ ( P - N ) e. NN0 ) /\ .0. .<_ X ) -> .0. .<_ ( ( P - N ) .x. X ) )
23 5 9 17 10 22 syl121anc
 |-  ( ph -> .0. .<_ ( ( P - N ) .x. X ) )
24 eqid
 |-  ( +g ` M ) = ( +g ` M )
25 1 2 24 omndadd
 |-  ( ( M e. oMnd /\ ( .0. e. B /\ ( ( P - N ) .x. X ) e. B /\ ( N .x. X ) e. B ) /\ .0. .<_ ( ( P - N ) .x. X ) ) -> ( .0. ( +g ` M ) ( N .x. X ) ) .<_ ( ( ( P - N ) .x. X ) ( +g ` M ) ( N .x. X ) ) )
26 5 14 19 21 23 25 syl131anc
 |-  ( ph -> ( .0. ( +g ` M ) ( N .x. X ) ) .<_ ( ( ( P - N ) .x. X ) ( +g ` M ) ( N .x. X ) ) )
27 1 24 4 mndlid
 |-  ( ( M e. Mnd /\ ( N .x. X ) e. B ) -> ( .0. ( +g ` M ) ( N .x. X ) ) = ( N .x. X ) )
28 12 21 27 syl2anc
 |-  ( ph -> ( .0. ( +g ` M ) ( N .x. X ) ) = ( N .x. X ) )
29 1 3 24 mulgnn0dir
 |-  ( ( M e. Mnd /\ ( ( P - N ) e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( ( ( P - N ) + N ) .x. X ) = ( ( ( P - N ) .x. X ) ( +g ` M ) ( N .x. X ) ) )
30 12 17 6 9 29 syl13anc
 |-  ( ph -> ( ( ( P - N ) + N ) .x. X ) = ( ( ( P - N ) .x. X ) ( +g ` M ) ( N .x. X ) ) )
31 7 nn0cnd
 |-  ( ph -> P e. CC )
32 6 nn0cnd
 |-  ( ph -> N e. CC )
33 31 32 npcand
 |-  ( ph -> ( ( P - N ) + N ) = P )
34 33 oveq1d
 |-  ( ph -> ( ( ( P - N ) + N ) .x. X ) = ( P .x. X ) )
35 30 34 eqtr3d
 |-  ( ph -> ( ( ( P - N ) .x. X ) ( +g ` M ) ( N .x. X ) ) = ( P .x. X ) )
36 26 28 35 3brtr3d
 |-  ( ph -> ( N .x. X ) .<_ ( P .x. X ) )