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 12 17 9 mulgnn0cld 
 |-  ( ph -> ( ( P - N ) .x. X ) e. B )
19 1 3 12 6 9 mulgnn0cld 
 |-  ( ph -> ( N .x. X ) e. B )
20 1 2 3 4 omndmul2 
 |-  ( ( M e. oMnd /\ ( X e. B /\ ( P - N ) e. NN0 ) /\ .0. .<_ X ) -> .0. .<_ ( ( P - N ) .x. X ) )
21 5 9 17 10 20 syl121anc 
 |-  ( ph -> .0. .<_ ( ( P - N ) .x. X ) )
22 eqid 
 |-  ( +g ` M ) = ( +g ` M )
23 1 2 22 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 ) ) )
24 5 14 18 19 21 23 syl131anc 
 |-  ( ph -> ( .0. ( +g ` M ) ( N .x. X ) ) .<_ ( ( ( P - N ) .x. X ) ( +g ` M ) ( N .x. X ) ) )
25 1 22 4 mndlid 
 |-  ( ( M e. Mnd /\ ( N .x. X ) e. B ) -> ( .0. ( +g ` M ) ( N .x. X ) ) = ( N .x. X ) )
26 12 19 25 syl2anc 
 |-  ( ph -> ( .0. ( +g ` M ) ( N .x. X ) ) = ( N .x. X ) )
27 1 3 22 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 ) ) )
28 12 17 6 9 27 syl13anc 
 |-  ( ph -> ( ( ( P - N ) + N ) .x. X ) = ( ( ( P - N ) .x. X ) ( +g ` M ) ( N .x. X ) ) )
29 7 nn0cnd 
 |-  ( ph -> P e. CC )
30 6 nn0cnd 
 |-  ( ph -> N e. CC )
31 29 30 npcand 
 |-  ( ph -> ( ( P - N ) + N ) = P )
32 31 oveq1d 
 |-  ( ph -> ( ( ( P - N ) + N ) .x. X ) = ( P .x. X ) )
33 28 32 eqtr3d 
 |-  ( ph -> ( ( ( P - N ) .x. X ) ( +g ` M ) ( N .x. X ) ) = ( P .x. X ) )
34 24 26 33 3brtr3d 
 |-  ( ph -> ( N .x. X ) .<_ ( P .x. X ) )