Metamath Proof Explorer

Theorem isomnd

Description: A (left) ordered monoid is a monoid with a total ordering compatible with its operation. (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Hypotheses isomnd.0 
|- B = ( Base ` M )
isomnd.1 
|- .+ = ( +g ` M )
isomnd.2 
|- .<_ = ( le ` M )
Assertion isomnd 
|- ( M e. oMnd <-> ( M e. Mnd /\ M e. Toset /\ A. a e. B A. b e. B A. c e. B ( a .<_ b -> ( a .+ c ) .<_ ( b .+ c ) ) ) )

Proof

Step Hyp Ref Expression
1 isomnd.0 
 |-  B = ( Base ` M )
2 isomnd.1 
 |-  .+ = ( +g ` M )
3 isomnd.2 
 |-  .<_ = ( le ` M )
4 fvexd 
 |-  ( m = M -> ( Base ` m ) e. _V )
5 simpr 
 |-  ( ( m = M /\ v = ( Base ` m ) ) -> v = ( Base ` m ) )
6 fveq2 
 |-  ( m = M -> ( Base ` m ) = ( Base ` M ) )
7 6 adantr 
 |-  ( ( m = M /\ v = ( Base ` m ) ) -> ( Base ` m ) = ( Base ` M ) )
8 5 7 eqtrd 
 |-  ( ( m = M /\ v = ( Base ` m ) ) -> v = ( Base ` M ) )
9 8 1 eqtr4di 
 |-  ( ( m = M /\ v = ( Base ` m ) ) -> v = B )
10 raleq 
 |-  ( v = B -> ( A. c e. v ( a l b -> ( a p c ) l ( b p c ) ) <-> A. c e. B ( a l b -> ( a p c ) l ( b p c ) ) ) )
11 10 raleqbi1dv 
 |-  ( v = B -> ( A. b e. v A. c e. v ( a l b -> ( a p c ) l ( b p c ) ) <-> A. b e. B A. c e. B ( a l b -> ( a p c ) l ( b p c ) ) ) )
12 11 raleqbi1dv 
 |-  ( v = B -> ( A. a e. v A. b e. v A. c e. v ( a l b -> ( a p c ) l ( b p c ) ) <-> A. a e. B A. b e. B A. c e. B ( a l b -> ( a p c ) l ( b p c ) ) ) )
13 9 12 syl 
 |-  ( ( m = M /\ v = ( Base ` m ) ) -> ( A. a e. v A. b e. v A. c e. v ( a l b -> ( a p c ) l ( b p c ) ) <-> A. a e. B A. b e. B A. c e. B ( a l b -> ( a p c ) l ( b p c ) ) ) )
14 13 anbi2d 
 |-  ( ( m = M /\ v = ( Base ` m ) ) -> ( ( m e. Toset /\ A. a e. v A. b e. v A. c e. v ( a l b -> ( a p c ) l ( b p c ) ) ) <-> ( m e. Toset /\ A. a e. B A. b e. B A. c e. B ( a l b -> ( a p c ) l ( b p c ) ) ) ) )
15 14 sbcbidv 
 |-  ( ( m = M /\ v = ( Base ` m ) ) -> ( [. ( le ` m ) / l ]. ( m e. Toset /\ A. a e. v A. b e. v A. c e. v ( a l b -> ( a p c ) l ( b p c ) ) ) <-> [. ( le ` m ) / l ]. ( m e. Toset /\ A. a e. B A. b e. B A. c e. B ( a l b -> ( a p c ) l ( b p c ) ) ) ) )
16 15 sbcbidv 
 |-  ( ( m = M /\ v = ( Base ` m ) ) -> ( [. ( +g ` m ) / p ]. [. ( le ` m ) / l ]. ( m e. Toset /\ A. a e. v A. b e. v A. c e. v ( a l b -> ( a p c ) l ( b p c ) ) ) <-> [. ( +g ` m ) / p ]. [. ( le ` m ) / l ]. ( m e. Toset /\ A. a e. B A. b e. B A. c e. B ( a l b -> ( a p c ) l ( b p c ) ) ) ) )
17 4 16 sbcied 
 |-  ( m = M -> ( [. ( Base ` m ) / v ]. [. ( +g ` m ) / p ]. [. ( le ` m ) / l ]. ( m e. Toset /\ A. a e. v A. b e. v A. c e. v ( a l b -> ( a p c ) l ( b p c ) ) ) <-> [. ( +g ` m ) / p ]. [. ( le ` m ) / l ]. ( m e. Toset /\ A. a e. B A. b e. B A. c e. B ( a l b -> ( a p c ) l ( b p c ) ) ) ) )
18 fvexd 
 |-  ( m = M -> ( +g ` m ) e. _V )
19 simpr 
 |-  ( ( m = M /\ p = ( +g ` m ) ) -> p = ( +g ` m ) )
20 fveq2 
 |-  ( m = M -> ( +g ` m ) = ( +g ` M ) )
21 20 adantr 
 |-  ( ( m = M /\ p = ( +g ` m ) ) -> ( +g ` m ) = ( +g ` M ) )
22 19 21 eqtrd 
 |-  ( ( m = M /\ p = ( +g ` m ) ) -> p = ( +g ` M ) )
23 22 2 eqtr4di 
 |-  ( ( m = M /\ p = ( +g ` m ) ) -> p = .+ )
24 23 oveqd 
 |-  ( ( m = M /\ p = ( +g ` m ) ) -> ( a p c ) = ( a .+ c ) )
25 23 oveqd 
 |-  ( ( m = M /\ p = ( +g ` m ) ) -> ( b p c ) = ( b .+ c ) )
26 24 25 breq12d 
 |-  ( ( m = M /\ p = ( +g ` m ) ) -> ( ( a p c ) l ( b p c ) <-> ( a .+ c ) l ( b .+ c ) ) )
27 26 imbi2d 
 |-  ( ( m = M /\ p = ( +g ` m ) ) -> ( ( a l b -> ( a p c ) l ( b p c ) ) <-> ( a l b -> ( a .+ c ) l ( b .+ c ) ) ) )
28 27 ralbidv 
 |-  ( ( m = M /\ p = ( +g ` m ) ) -> ( A. c e. B ( a l b -> ( a p c ) l ( b p c ) ) <-> A. c e. B ( a l b -> ( a .+ c ) l ( b .+ c ) ) ) )
29 28 2ralbidv 
 |-  ( ( m = M /\ p = ( +g ` m ) ) -> ( A. a e. B A. b e. B A. c e. B ( a l b -> ( a p c ) l ( b p c ) ) <-> A. a e. B A. b e. B A. c e. B ( a l b -> ( a .+ c ) l ( b .+ c ) ) ) )
30 29 anbi2d 
 |-  ( ( m = M /\ p = ( +g ` m ) ) -> ( ( m e. Toset /\ A. a e. B A. b e. B A. c e. B ( a l b -> ( a p c ) l ( b p c ) ) ) <-> ( m e. Toset /\ A. a e. B A. b e. B A. c e. B ( a l b -> ( a .+ c ) l ( b .+ c ) ) ) ) )
31 30 sbcbidv 
 |-  ( ( m = M /\ p = ( +g ` m ) ) -> ( [. ( le ` m ) / l ]. ( m e. Toset /\ A. a e. B A. b e. B A. c e. B ( a l b -> ( a p c ) l ( b p c ) ) ) <-> [. ( le ` m ) / l ]. ( m e. Toset /\ A. a e. B A. b e. B A. c e. B ( a l b -> ( a .+ c ) l ( b .+ c ) ) ) ) )
32 18 31 sbcied 
 |-  ( m = M -> ( [. ( +g ` m ) / p ]. [. ( le ` m ) / l ]. ( m e. Toset /\ A. a e. B A. b e. B A. c e. B ( a l b -> ( a p c ) l ( b p c ) ) ) <-> [. ( le ` m ) / l ]. ( m e. Toset /\ A. a e. B A. b e. B A. c e. B ( a l b -> ( a .+ c ) l ( b .+ c ) ) ) ) )
33 fvexd 
 |-  ( m = M -> ( le ` m ) e. _V )
34 simpr 
 |-  ( ( m = M /\ l = ( le ` m ) ) -> l = ( le ` m ) )
35 simpl 
 |-  ( ( m = M /\ l = ( le ` m ) ) -> m = M )
36 35 fveq2d 
 |-  ( ( m = M /\ l = ( le ` m ) ) -> ( le ` m ) = ( le ` M ) )
37 34 36 eqtrd 
 |-  ( ( m = M /\ l = ( le ` m ) ) -> l = ( le ` M ) )
38 37 3 eqtr4di 
 |-  ( ( m = M /\ l = ( le ` m ) ) -> l = .<_ )
39 38 breqd 
 |-  ( ( m = M /\ l = ( le ` m ) ) -> ( a l b <-> a .<_ b ) )
40 38 breqd 
 |-  ( ( m = M /\ l = ( le ` m ) ) -> ( ( a .+ c ) l ( b .+ c ) <-> ( a .+ c ) .<_ ( b .+ c ) ) )
41 39 40 imbi12d 
 |-  ( ( m = M /\ l = ( le ` m ) ) -> ( ( a l b -> ( a .+ c ) l ( b .+ c ) ) <-> ( a .<_ b -> ( a .+ c ) .<_ ( b .+ c ) ) ) )
42 41 ralbidv 
 |-  ( ( m = M /\ l = ( le ` m ) ) -> ( A. c e. B ( a l b -> ( a .+ c ) l ( b .+ c ) ) <-> A. c e. B ( a .<_ b -> ( a .+ c ) .<_ ( b .+ c ) ) ) )
43 42 2ralbidv 
 |-  ( ( m = M /\ l = ( le ` m ) ) -> ( A. a e. B A. b e. B A. c e. B ( a l b -> ( a .+ c ) l ( b .+ c ) ) <-> A. a e. B A. b e. B A. c e. B ( a .<_ b -> ( a .+ c ) .<_ ( b .+ c ) ) ) )
44 43 anbi2d 
 |-  ( ( m = M /\ l = ( le ` m ) ) -> ( ( m e. Toset /\ A. a e. B A. b e. B A. c e. B ( a l b -> ( a .+ c ) l ( b .+ c ) ) ) <-> ( m e. Toset /\ A. a e. B A. b e. B A. c e. B ( a .<_ b -> ( a .+ c ) .<_ ( b .+ c ) ) ) ) )
45 33 44 sbcied 
 |-  ( m = M -> ( [. ( le ` m ) / l ]. ( m e. Toset /\ A. a e. B A. b e. B A. c e. B ( a l b -> ( a .+ c ) l ( b .+ c ) ) ) <-> ( m e. Toset /\ A. a e. B A. b e. B A. c e. B ( a .<_ b -> ( a .+ c ) .<_ ( b .+ c ) ) ) ) )
46 eleq1 
 |-  ( m = M -> ( m e. Toset <-> M e. Toset ) )
47 46 anbi1d 
 |-  ( m = M -> ( ( m e. Toset /\ A. a e. B A. b e. B A. c e. B ( a .<_ b -> ( a .+ c ) .<_ ( b .+ c ) ) ) <-> ( M e. Toset /\ A. a e. B A. b e. B A. c e. B ( a .<_ b -> ( a .+ c ) .<_ ( b .+ c ) ) ) ) )
48 45 47 bitrd 
 |-  ( m = M -> ( [. ( le ` m ) / l ]. ( m e. Toset /\ A. a e. B A. b e. B A. c e. B ( a l b -> ( a .+ c ) l ( b .+ c ) ) ) <-> ( M e. Toset /\ A. a e. B A. b e. B A. c e. B ( a .<_ b -> ( a .+ c ) .<_ ( b .+ c ) ) ) ) )
49 17 32 48 3bitrd 
 |-  ( m = M -> ( [. ( Base ` m ) / v ]. [. ( +g ` m ) / p ]. [. ( le ` m ) / l ]. ( m e. Toset /\ A. a e. v A. b e. v A. c e. v ( a l b -> ( a p c ) l ( b p c ) ) ) <-> ( M e. Toset /\ A. a e. B A. b e. B A. c e. B ( a .<_ b -> ( a .+ c ) .<_ ( b .+ c ) ) ) ) )
50 df-omnd 
 |-  oMnd = { m e. Mnd | [. ( Base ` m ) / v ]. [. ( +g ` m ) / p ]. [. ( le ` m ) / l ]. ( m e. Toset /\ A. a e. v A. b e. v A. c e. v ( a l b -> ( a p c ) l ( b p c ) ) ) }
51 49 50 elrab2 
 |-  ( M e. oMnd <-> ( M e. Mnd /\ ( M e. Toset /\ A. a e. B A. b e. B A. c e. B ( a .<_ b -> ( a .+ c ) .<_ ( b .+ c ) ) ) ) )
52 3anass 
 |-  ( ( M e. Mnd /\ M e. Toset /\ A. a e. B A. b e. B A. c e. B ( a .<_ b -> ( a .+ c ) .<_ ( b .+ c ) ) ) <-> ( M e. Mnd /\ ( M e. Toset /\ A. a e. B A. b e. B A. c e. B ( a .<_ b -> ( a .+ c ) .<_ ( b .+ c ) ) ) ) )
53 51 52 bitr4i 
 |-  ( M e. oMnd <-> ( M e. Mnd /\ M e. Toset /\ A. a e. B A. b e. B A. c e. B ( a .<_ b -> ( a .+ c ) .<_ ( b .+ c ) ) ) )