Metamath Proof Explorer

Theorem omndmul2

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 )
omndmul2.2 
|- .x. = ( .g ` M )
omndmul2.3 
|- .0. = ( 0g ` M )
Assertion omndmul2 
|- ( ( M e. oMnd /\ ( X e. B /\ N e. NN0 ) /\ .0. .<_ X ) -> .0. .<_ ( N .x. X ) )

Proof

Step Hyp Ref Expression
1 omndmul.0 
 |-  B = ( Base ` M )
2 omndmul.1 
 |-  .<_ = ( le ` M )
3 omndmul2.2 
 |-  .x. = ( .g ` M )
4 omndmul2.3 
 |-  .0. = ( 0g ` M )
5 df-3an 
 |-  ( ( M e. oMnd /\ ( X e. B /\ N e. NN0 ) /\ .0. .<_ X ) <-> ( ( M e. oMnd /\ ( X e. B /\ N e. NN0 ) ) /\ .0. .<_ X ) )
6 anass 
 |-  ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) <-> ( M e. oMnd /\ ( X e. B /\ N e. NN0 ) ) )
7 6 anbi1i 
 |-  ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) <-> ( ( M e. oMnd /\ ( X e. B /\ N e. NN0 ) ) /\ .0. .<_ X ) )
8 5 7 bitr4i 
 |-  ( ( M e. oMnd /\ ( X e. B /\ N e. NN0 ) /\ .0. .<_ X ) <-> ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) )
9 simplr 
 |-  ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) -> N e. NN0 )
10 oveq1 
 |-  ( m = 0 -> ( m .x. X ) = ( 0 .x. X ) )
11 10 breq2d 
 |-  ( m = 0 -> ( .0. .<_ ( m .x. X ) <-> .0. .<_ ( 0 .x. X ) ) )
12 oveq1 
 |-  ( m = n -> ( m .x. X ) = ( n .x. X ) )
13 12 breq2d 
 |-  ( m = n -> ( .0. .<_ ( m .x. X ) <-> .0. .<_ ( n .x. X ) ) )
14 oveq1 
 |-  ( m = ( n + 1 ) -> ( m .x. X ) = ( ( n + 1 ) .x. X ) )
15 14 breq2d 
 |-  ( m = ( n + 1 ) -> ( .0. .<_ ( m .x. X ) <-> .0. .<_ ( ( n + 1 ) .x. X ) ) )
16 oveq1 
 |-  ( m = N -> ( m .x. X ) = ( N .x. X ) )
17 16 breq2d 
 |-  ( m = N -> ( .0. .<_ ( m .x. X ) <-> .0. .<_ ( N .x. X ) ) )
18 omndtos 
 |-  ( M e. oMnd -> M e. Toset )
19 tospos 
 |-  ( M e. Toset -> M e. Poset )
20 18 19 syl 
 |-  ( M e. oMnd -> M e. Poset )
21 omndmnd 
 |-  ( M e. oMnd -> M e. Mnd )
22 1 4 mndidcl 
 |-  ( M e. Mnd -> .0. e. B )
23 21 22 syl 
 |-  ( M e. oMnd -> .0. e. B )
24 1 2 posref 
 |-  ( ( M e. Poset /\ .0. e. B ) -> .0. .<_ .0. )
25 20 23 24 syl2anc 
 |-  ( M e. oMnd -> .0. .<_ .0. )
26 25 ad3antrrr 
 |-  ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) -> .0. .<_ .0. )
27 1 4 3 mulg0 
 |-  ( X e. B -> ( 0 .x. X ) = .0. )
28 27 ad3antlr 
 |-  ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) -> ( 0 .x. X ) = .0. )
29 26 28 breqtrrd 
 |-  ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) -> .0. .<_ ( 0 .x. X ) )
30 20 ad5antr 
 |-  ( ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) /\ .0. .<_ ( n .x. X ) ) -> M e. Poset )
31 21 ad5antr 
 |-  ( ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) /\ .0. .<_ ( n .x. X ) ) -> M e. Mnd )
32 31 22 syl 
 |-  ( ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) /\ .0. .<_ ( n .x. X ) ) -> .0. e. B )
33 simplr 
 |-  ( ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) /\ .0. .<_ ( n .x. X ) ) -> n e. NN0 )
34 simp-5r 
 |-  ( ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) /\ .0. .<_ ( n .x. X ) ) -> X e. B )
35 1 3 31 33 34 mulgnn0cld 
 |-  ( ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) /\ .0. .<_ ( n .x. X ) ) -> ( n .x. X ) e. B )
36 simpr32 
 |-  ( ( M e. oMnd /\ ( X e. B /\ N e. NN0 /\ ( .0. .<_ X /\ n e. NN0 /\ .0. .<_ ( n .x. X ) ) ) ) -> n e. NN0 )
37 1nn0 
 |-  1 e. NN0
38 37 a1i 
 |-  ( ( M e. oMnd /\ ( X e. B /\ N e. NN0 /\ ( .0. .<_ X /\ n e. NN0 /\ .0. .<_ ( n .x. X ) ) ) ) -> 1 e. NN0 )
39 36 38 nn0addcld 
 |-  ( ( M e. oMnd /\ ( X e. B /\ N e. NN0 /\ ( .0. .<_ X /\ n e. NN0 /\ .0. .<_ ( n .x. X ) ) ) ) -> ( n + 1 ) e. NN0 )
40 39 3anassrs 
 |-  ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ ( .0. .<_ X /\ n e. NN0 /\ .0. .<_ ( n .x. X ) ) ) -> ( n + 1 ) e. NN0 )
41 40 3anassrs 
 |-  ( ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) /\ .0. .<_ ( n .x. X ) ) -> ( n + 1 ) e. NN0 )
42 1 3 31 41 34 mulgnn0cld 
 |-  ( ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) /\ .0. .<_ ( n .x. X ) ) -> ( ( n + 1 ) .x. X ) e. B )
43 32 35 42 3jca 
 |-  ( ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) /\ .0. .<_ ( n .x. X ) ) -> ( .0. e. B /\ ( n .x. X ) e. B /\ ( ( n + 1 ) .x. X ) e. B ) )
44 simpr 
 |-  ( ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) /\ .0. .<_ ( n .x. X ) ) -> .0. .<_ ( n .x. X ) )
45 simp-4l 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> M e. oMnd )
46 21 ad4antr 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> M e. Mnd )
47 46 22 syl 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> .0. e. B )
48 simp-4r 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> X e. B )
49 simpr 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> n e. NN0 )
50 1 3 46 49 48 mulgnn0cld 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> ( n .x. X ) e. B )
51 simplr 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> .0. .<_ X )
52 eqid 
 |-  ( +g ` M ) = ( +g ` M )
53 1 2 52 omndadd 
 |-  ( ( M e. oMnd /\ ( .0. e. B /\ X e. B /\ ( n .x. X ) e. B ) /\ .0. .<_ X ) -> ( .0. ( +g ` M ) ( n .x. X ) ) .<_ ( X ( +g ` M ) ( n .x. X ) ) )
54 45 47 48 50 51 53 syl131anc 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> ( .0. ( +g ` M ) ( n .x. X ) ) .<_ ( X ( +g ` M ) ( n .x. X ) ) )
55 1 52 4 mndlid 
 |-  ( ( M e. Mnd /\ ( n .x. X ) e. B ) -> ( .0. ( +g ` M ) ( n .x. X ) ) = ( n .x. X ) )
56 46 50 55 syl2anc 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> ( .0. ( +g ` M ) ( n .x. X ) ) = ( n .x. X ) )
57 37 a1i 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> 1 e. NN0 )
58 1 3 52 mulgnn0dir 
 |-  ( ( M e. Mnd /\ ( 1 e. NN0 /\ n e. NN0 /\ X e. B ) ) -> ( ( 1 + n ) .x. X ) = ( ( 1 .x. X ) ( +g ` M ) ( n .x. X ) ) )
59 46 57 49 48 58 syl13anc 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> ( ( 1 + n ) .x. X ) = ( ( 1 .x. X ) ( +g ` M ) ( n .x. X ) ) )
60 1cnd 
 |-  ( ( ( M e. oMnd /\ X e. B ) /\ ( N e. NN0 /\ .0. .<_ X /\ n e. NN0 ) ) -> 1 e. CC )
61 simpr3 
 |-  ( ( ( M e. oMnd /\ X e. B ) /\ ( N e. NN0 /\ .0. .<_ X /\ n e. NN0 ) ) -> n e. NN0 )
62 61 nn0cnd 
 |-  ( ( ( M e. oMnd /\ X e. B ) /\ ( N e. NN0 /\ .0. .<_ X /\ n e. NN0 ) ) -> n e. CC )
63 60 62 addcomd 
 |-  ( ( ( M e. oMnd /\ X e. B ) /\ ( N e. NN0 /\ .0. .<_ X /\ n e. NN0 ) ) -> ( 1 + n ) = ( n + 1 ) )
64 63 3anassrs 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> ( 1 + n ) = ( n + 1 ) )
65 64 oveq1d 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> ( ( 1 + n ) .x. X ) = ( ( n + 1 ) .x. X ) )
66 1 3 mulg1 
 |-  ( X e. B -> ( 1 .x. X ) = X )
67 48 66 syl 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> ( 1 .x. X ) = X )
68 67 oveq1d 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> ( ( 1 .x. X ) ( +g ` M ) ( n .x. X ) ) = ( X ( +g ` M ) ( n .x. X ) ) )
69 59 65 68 3eqtr3rd 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> ( X ( +g ` M ) ( n .x. X ) ) = ( ( n + 1 ) .x. X ) )
70 54 56 69 3brtr3d 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> ( n .x. X ) .<_ ( ( n + 1 ) .x. X ) )
71 70 adantr 
 |-  ( ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) /\ .0. .<_ ( n .x. X ) ) -> ( n .x. X ) .<_ ( ( n + 1 ) .x. X ) )
72 1 2 postr 
 |-  ( ( M e. Poset /\ ( .0. e. B /\ ( n .x. X ) e. B /\ ( ( n + 1 ) .x. X ) e. B ) ) -> ( ( .0. .<_ ( n .x. X ) /\ ( n .x. X ) .<_ ( ( n + 1 ) .x. X ) ) -> .0. .<_ ( ( n + 1 ) .x. X ) ) )
73 72 imp 
 |-  ( ( ( M e. Poset /\ ( .0. e. B /\ ( n .x. X ) e. B /\ ( ( n + 1 ) .x. X ) e. B ) ) /\ ( .0. .<_ ( n .x. X ) /\ ( n .x. X ) .<_ ( ( n + 1 ) .x. X ) ) ) -> .0. .<_ ( ( n + 1 ) .x. X ) )
74 30 43 44 71 73 syl22anc 
 |-  ( ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) /\ .0. .<_ ( n .x. X ) ) -> .0. .<_ ( ( n + 1 ) .x. X ) )
75 11 13 15 17 29 74 nn0indd 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ N e. NN0 ) -> .0. .<_ ( N .x. X ) )
76 9 75 mpdan 
 |-  ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) -> .0. .<_ ( N .x. X ) )
77 8 76 sylbi 
 |-  ( ( M e. oMnd /\ ( X e. B /\ N e. NN0 ) /\ .0. .<_ X ) -> .0. .<_ ( N .x. X ) )