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 mulgnn0cl 
 |-  ( ( M e. Mnd /\ n e. NN0 /\ X e. B ) -> ( n .x. X ) e. B )
36 31 33 34 35 syl3anc 
 |-  ( ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) /\ .0. .<_ ( n .x. X ) ) -> ( n .x. X ) e. B )
37 simpr32 
 |-  ( ( M e. oMnd /\ ( X e. B /\ N e. NN0 /\ ( .0. .<_ X /\ n e. NN0 /\ .0. .<_ ( n .x. X ) ) ) ) -> n e. NN0 )
38 1nn0 
 |-  1 e. NN0
39 38 a1i 
 |-  ( ( M e. oMnd /\ ( X e. B /\ N e. NN0 /\ ( .0. .<_ X /\ n e. NN0 /\ .0. .<_ ( n .x. X ) ) ) ) -> 1 e. NN0 )
40 37 39 nn0addcld 
 |-  ( ( 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 41 3anassrs 
 |-  ( ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) /\ .0. .<_ ( n .x. X ) ) -> ( n + 1 ) e. NN0 )
43 1 3 mulgnn0cl 
 |-  ( ( M e. Mnd /\ ( n + 1 ) e. NN0 /\ X e. B ) -> ( ( n + 1 ) .x. X ) e. B )
44 31 42 34 43 syl3anc 
 |-  ( ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) /\ .0. .<_ ( n .x. X ) ) -> ( ( n + 1 ) .x. X ) e. B )
45 32 36 44 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 ) )
46 simpr 
 |-  ( ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) /\ .0. .<_ ( n .x. X ) ) -> .0. .<_ ( n .x. X ) )
47 simp-4l 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> M e. oMnd )
48 21 ad4antr 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> M e. Mnd )
49 48 22 syl 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> .0. e. B )
50 simp-4r 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> X e. B )
51 simpr 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> n e. NN0 )
52 48 51 50 35 syl3anc 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> ( n .x. X ) e. B )
53 simplr 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> .0. .<_ X )
54 eqid 
 |-  ( +g ` M ) = ( +g ` M )
55 1 2 54 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 ) ) )
56 47 49 50 52 53 55 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 ) ) )
57 1 54 4 mndlid 
 |-  ( ( M e. Mnd /\ ( n .x. X ) e. B ) -> ( .0. ( +g ` M ) ( n .x. X ) ) = ( n .x. X ) )
58 48 52 57 syl2anc 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> ( .0. ( +g ` M ) ( n .x. X ) ) = ( n .x. X ) )
59 38 a1i 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> 1 e. NN0 )
60 1 3 54 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 ) ) )
61 48 59 51 50 60 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 ) ) )
62 1cnd 
 |-  ( ( ( M e. oMnd /\ X e. B ) /\ ( N e. NN0 /\ .0. .<_ X /\ n e. NN0 ) ) -> 1 e. CC )
63 simpr3 
 |-  ( ( ( M e. oMnd /\ X e. B ) /\ ( N e. NN0 /\ .0. .<_ X /\ n e. NN0 ) ) -> n e. NN0 )
64 63 nn0cnd 
 |-  ( ( ( M e. oMnd /\ X e. B ) /\ ( N e. NN0 /\ .0. .<_ X /\ n e. NN0 ) ) -> n e. CC )
65 62 64 addcomd 
 |-  ( ( ( M e. oMnd /\ X e. B ) /\ ( N e. NN0 /\ .0. .<_ X /\ n e. NN0 ) ) -> ( 1 + n ) = ( n + 1 ) )
66 65 3anassrs 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> ( 1 + n ) = ( n + 1 ) )
67 66 oveq1d 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> ( ( 1 + n ) .x. X ) = ( ( n + 1 ) .x. X ) )
68 1 3 mulg1 
 |-  ( X e. B -> ( 1 .x. X ) = X )
69 50 68 syl 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> ( 1 .x. X ) = X )
70 69 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 ) ) )
71 61 67 70 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 ) )
72 56 58 71 3brtr3d 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) -> ( n .x. X ) .<_ ( ( n + 1 ) .x. X ) )
73 72 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 ) )
74 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 ) ) )
75 74 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 ) )
76 30 45 46 73 75 syl22anc 
 |-  ( ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ n e. NN0 ) /\ .0. .<_ ( n .x. X ) ) -> .0. .<_ ( ( n + 1 ) .x. X ) )
77 11 13 15 17 29 76 nn0indd 
 |-  ( ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) /\ N e. NN0 ) -> .0. .<_ ( N .x. X ) )
78 9 77 mpdan 
 |-  ( ( ( ( M e. oMnd /\ X e. B ) /\ N e. NN0 ) /\ .0. .<_ X ) -> .0. .<_ ( N .x. X ) )
79 8 78 sylbi 
 |-  ( ( M e. oMnd /\ ( X e. B /\ N e. NN0 ) /\ .0. .<_ X ) -> .0. .<_ ( N .x. X ) )