Metamath Proof Explorer

Theorem omndmul

Description: In a commutative ordered monoid, the ordering is compatible with group power. (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Hypotheses omndmul.0 
|- B = ( Base ` M )
omndmul.1 
|- .<_ = ( le ` M )
omndmul.2 
|- .x. = ( .g ` M )
omndmul.o 
|- ( ph -> M e. oMnd )
omndmul.c 
|- ( ph -> M e. CMnd )
omndmul.x 
|- ( ph -> X e. B )
omndmul.y 
|- ( ph -> Y e. B )
omndmul.n 
|- ( ph -> N e. NN0 )
omndmul.l 
|- ( ph -> X .<_ Y )
Assertion omndmul 
|- ( ph -> ( N .x. X ) .<_ ( N .x. Y ) )

Proof

Step Hyp Ref Expression
1 omndmul.0 
 |-  B = ( Base ` M )
2 omndmul.1 
 |-  .<_ = ( le ` M )
3 omndmul.2 
 |-  .x. = ( .g ` M )
4 omndmul.o 
 |-  ( ph -> M e. oMnd )
5 omndmul.c 
 |-  ( ph -> M e. CMnd )
6 omndmul.x 
 |-  ( ph -> X e. B )
7 omndmul.y 
 |-  ( ph -> Y e. B )
8 omndmul.n 
 |-  ( ph -> N e. NN0 )
9 omndmul.l 
 |-  ( ph -> X .<_ Y )
10 oveq1 
 |-  ( m = 0 -> ( m .x. X ) = ( 0 .x. X ) )
11 oveq1 
 |-  ( m = 0 -> ( m .x. Y ) = ( 0 .x. Y ) )
12 10 11 breq12d 
 |-  ( m = 0 -> ( ( m .x. X ) .<_ ( m .x. Y ) <-> ( 0 .x. X ) .<_ ( 0 .x. Y ) ) )
13 oveq1 
 |-  ( m = n -> ( m .x. X ) = ( n .x. X ) )
14 oveq1 
 |-  ( m = n -> ( m .x. Y ) = ( n .x. Y ) )
15 13 14 breq12d 
 |-  ( m = n -> ( ( m .x. X ) .<_ ( m .x. Y ) <-> ( n .x. X ) .<_ ( n .x. Y ) ) )
16 oveq1 
 |-  ( m = ( n + 1 ) -> ( m .x. X ) = ( ( n + 1 ) .x. X ) )
17 oveq1 
 |-  ( m = ( n + 1 ) -> ( m .x. Y ) = ( ( n + 1 ) .x. Y ) )
18 16 17 breq12d 
 |-  ( m = ( n + 1 ) -> ( ( m .x. X ) .<_ ( m .x. Y ) <-> ( ( n + 1 ) .x. X ) .<_ ( ( n + 1 ) .x. Y ) ) )
19 oveq1 
 |-  ( m = N -> ( m .x. X ) = ( N .x. X ) )
20 oveq1 
 |-  ( m = N -> ( m .x. Y ) = ( N .x. Y ) )
21 19 20 breq12d 
 |-  ( m = N -> ( ( m .x. X ) .<_ ( m .x. Y ) <-> ( N .x. X ) .<_ ( N .x. Y ) ) )
22 omndtos 
 |-  ( M e. oMnd -> M e. Toset )
23 tospos 
 |-  ( M e. Toset -> M e. Poset )
24 4 22 23 3syl 
 |-  ( ph -> M e. Poset )
25 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
26 1 25 3 mulg0 
 |-  ( Y e. B -> ( 0 .x. Y ) = ( 0g ` M ) )
27 7 26 syl 
 |-  ( ph -> ( 0 .x. Y ) = ( 0g ` M ) )
28 omndmnd 
 |-  ( M e. oMnd -> M e. Mnd )
29 1 25 mndidcl 
 |-  ( M e. Mnd -> ( 0g ` M ) e. B )
30 4 28 29 3syl 
 |-  ( ph -> ( 0g ` M ) e. B )
31 27 30 eqeltrd 
 |-  ( ph -> ( 0 .x. Y ) e. B )
32 1 2 posref 
 |-  ( ( M e. Poset /\ ( 0 .x. Y ) e. B ) -> ( 0 .x. Y ) .<_ ( 0 .x. Y ) )
33 24 31 32 syl2anc 
 |-  ( ph -> ( 0 .x. Y ) .<_ ( 0 .x. Y ) )
34 1 25 3 mulg0 
 |-  ( X e. B -> ( 0 .x. X ) = ( 0g ` M ) )
35 34 adantr 
 |-  ( ( X e. B /\ Y e. B ) -> ( 0 .x. X ) = ( 0g ` M ) )
36 26 adantl 
 |-  ( ( X e. B /\ Y e. B ) -> ( 0 .x. Y ) = ( 0g ` M ) )
37 35 36 eqtr4d 
 |-  ( ( X e. B /\ Y e. B ) -> ( 0 .x. X ) = ( 0 .x. Y ) )
38 37 breq1d 
 |-  ( ( X e. B /\ Y e. B ) -> ( ( 0 .x. X ) .<_ ( 0 .x. Y ) <-> ( 0 .x. Y ) .<_ ( 0 .x. Y ) ) )
39 6 7 38 syl2anc 
 |-  ( ph -> ( ( 0 .x. X ) .<_ ( 0 .x. Y ) <-> ( 0 .x. Y ) .<_ ( 0 .x. Y ) ) )
40 33 39 mpbird 
 |-  ( ph -> ( 0 .x. X ) .<_ ( 0 .x. Y ) )
41 eqid 
 |-  ( +g ` M ) = ( +g ` M )
42 4 ad2antrr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( n .x. X ) .<_ ( n .x. Y ) ) -> M e. oMnd )
43 7 ad2antrr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( n .x. X ) .<_ ( n .x. Y ) ) -> Y e. B )
44 42 28 syl 
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( n .x. X ) .<_ ( n .x. Y ) ) -> M e. Mnd )
45 simplr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( n .x. X ) .<_ ( n .x. Y ) ) -> n e. NN0 )
46 6 ad2antrr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( n .x. X ) .<_ ( n .x. Y ) ) -> X e. B )
47 1 3 44 45 46 mulgnn0cld 
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( n .x. X ) .<_ ( n .x. Y ) ) -> ( n .x. X ) e. B )
48 1 3 44 45 43 mulgnn0cld 
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( n .x. X ) .<_ ( n .x. Y ) ) -> ( n .x. Y ) e. B )
49 simpr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( n .x. X ) .<_ ( n .x. Y ) ) -> ( n .x. X ) .<_ ( n .x. Y ) )
50 9 ad2antrr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( n .x. X ) .<_ ( n .x. Y ) ) -> X .<_ Y )
51 5 ad2antrr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( n .x. X ) .<_ ( n .x. Y ) ) -> M e. CMnd )
52 1 2 41 42 43 47 46 48 49 50 51 omndadd2d 
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( n .x. X ) .<_ ( n .x. Y ) ) -> ( ( n .x. X ) ( +g ` M ) X ) .<_ ( ( n .x. Y ) ( +g ` M ) Y ) )
53 1 3 41 mulgnn0p1 
 |-  ( ( M e. Mnd /\ n e. NN0 /\ X e. B ) -> ( ( n + 1 ) .x. X ) = ( ( n .x. X ) ( +g ` M ) X ) )
54 44 45 46 53 syl3anc 
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( n .x. X ) .<_ ( n .x. Y ) ) -> ( ( n + 1 ) .x. X ) = ( ( n .x. X ) ( +g ` M ) X ) )
55 1 3 41 mulgnn0p1 
 |-  ( ( M e. Mnd /\ n e. NN0 /\ Y e. B ) -> ( ( n + 1 ) .x. Y ) = ( ( n .x. Y ) ( +g ` M ) Y ) )
56 44 45 43 55 syl3anc 
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( n .x. X ) .<_ ( n .x. Y ) ) -> ( ( n + 1 ) .x. Y ) = ( ( n .x. Y ) ( +g ` M ) Y ) )
57 52 54 56 3brtr4d 
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( n .x. X ) .<_ ( n .x. Y ) ) -> ( ( n + 1 ) .x. X ) .<_ ( ( n + 1 ) .x. Y ) )
58 12 15 18 21 40 57 nn0indd 
 |-  ( ( ph /\ N e. NN0 ) -> ( N .x. X ) .<_ ( N .x. Y ) )
59 8 58 mpdan 
 |-  ( ph -> ( N .x. X ) .<_ ( N .x. Y ) )