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=BaseM
isomnd.1 ⊢+˙=+M
isomnd.2 ⊢≤˙=≤M
Assertion isomnd ⊢M∈oMnd↔M∈Mnd∧M∈Toset∧∀a∈B∀b∈B∀c∈Ba≤˙b→a+˙c≤˙b+˙c

Proof

Step Hyp Ref Expression
1 isomnd.0 ⊢B=BaseM
2 isomnd.1 ⊢+˙=+M
3 isomnd.2 ⊢≤˙=≤M
4 fvexd ⊢m=M→Basem∈V
5 simpr ⊢m=M∧v=Basem→v=Basem
6 fveq2 ⊢m=M→Basem=BaseM
7 6 adantr ⊢m=M∧v=Basem→Basem=BaseM
8 5 7 eqtrd ⊢m=M∧v=Basem→v=BaseM
9 8 1 eqtr4di ⊢m=M∧v=Basem→v=B
10 raleq ⊢v=B→∀c∈valb→apclbpc↔∀c∈Balb→apclbpc
11 10 raleqbi1dv ⊢v=B→∀b∈v∀c∈valb→apclbpc↔∀b∈B∀c∈Balb→apclbpc
12 11 raleqbi1dv ⊢v=B→∀a∈v∀b∈v∀c∈valb→apclbpc↔∀a∈B∀b∈B∀c∈Balb→apclbpc
13 9 12 syl ⊢m=M∧v=Basem→∀a∈v∀b∈v∀c∈valb→apclbpc↔∀a∈B∀b∈B∀c∈Balb→apclbpc
14 13 anbi2d ⊢m=M∧v=Basem→m∈Toset∧∀a∈v∀b∈v∀c∈valb→apclbpc↔m∈Toset∧∀a∈B∀b∈B∀c∈Balb→apclbpc
15 14 sbcbidv ⊢m=M∧v=Basem→[˙≤m/l]˙m∈Toset∧∀a∈v∀b∈v∀c∈valb→apclbpc↔[˙≤m/l]˙m∈Toset∧∀a∈B∀b∈B∀c∈Balb→apclbpc
16 15 sbcbidv ⊢m=M∧v=Basem→[˙+m/p]˙[˙≤m/l]˙m∈Toset∧∀a∈v∀b∈v∀c∈valb→apclbpc↔[˙+m/p]˙[˙≤m/l]˙m∈Toset∧∀a∈B∀b∈B∀c∈Balb→apclbpc
17 4 16 sbcied ⊢m=M→[˙Basem/v]˙[˙+m/p]˙[˙≤m/l]˙m∈Toset∧∀a∈v∀b∈v∀c∈valb→apclbpc↔[˙+m/p]˙[˙≤m/l]˙m∈Toset∧∀a∈B∀b∈B∀c∈Balb→apclbpc
18 fvexd ⊢m=M→+m∈V
19 simpr ⊢m=M∧p=+m→p=+m
20 fveq2 ⊢m=M→+m=+M
21 20 adantr ⊢m=M∧p=+m→+m=+M
22 19 21 eqtrd ⊢m=M∧p=+m→p=+M
23 22 2 eqtr4di ⊢m=M∧p=+m→p=+˙
24 23 oveqd ⊢m=M∧p=+m→apc=a+˙c
25 23 oveqd ⊢m=M∧p=+m→bpc=b+˙c
26 24 25 breq12d ⊢m=M∧p=+m→apclbpc↔a+˙clb+˙c
27 26 imbi2d ⊢m=M∧p=+m→alb→apclbpc↔alb→a+˙clb+˙c
28 27 ralbidv ⊢m=M∧p=+m→∀c∈Balb→apclbpc↔∀c∈Balb→a+˙clb+˙c
29 28 2ralbidv ⊢m=M∧p=+m→∀a∈B∀b∈B∀c∈Balb→apclbpc↔∀a∈B∀b∈B∀c∈Balb→a+˙clb+˙c
30 29 anbi2d ⊢m=M∧p=+m→m∈Toset∧∀a∈B∀b∈B∀c∈Balb→apclbpc↔m∈Toset∧∀a∈B∀b∈B∀c∈Balb→a+˙clb+˙c
31 30 sbcbidv ⊢m=M∧p=+m→[˙≤m/l]˙m∈Toset∧∀a∈B∀b∈B∀c∈Balb→apclbpc↔[˙≤m/l]˙m∈Toset∧∀a∈B∀b∈B∀c∈Balb→a+˙clb+˙c
32 18 31 sbcied ⊢m=M→[˙+m/p]˙[˙≤m/l]˙m∈Toset∧∀a∈B∀b∈B∀c∈Balb→apclbpc↔[˙≤m/l]˙m∈Toset∧∀a∈B∀b∈B∀c∈Balb→a+˙clb+˙c
33 fvexd ⊢m=M→≤m∈V
34 simpr ⊢m=M∧l=≤m→l=≤m
35 simpl ⊢m=M∧l=≤m→m=M
36 35 fveq2d ⊢m=M∧l=≤m→≤m=≤M
37 34 36 eqtrd ⊢m=M∧l=≤m→l=≤M
38 37 3 eqtr4di ⊢m=M∧l=≤m→l=≤˙
39 38 breqd ⊢m=M∧l=≤m→alb↔a≤˙b
40 38 breqd ⊢m=M∧l=≤m→a+˙clb+˙c↔a+˙c≤˙b+˙c
41 39 40 imbi12d ⊢m=M∧l=≤m→alb→a+˙clb+˙c↔a≤˙b→a+˙c≤˙b+˙c
42 41 ralbidv ⊢m=M∧l=≤m→∀c∈Balb→a+˙clb+˙c↔∀c∈Ba≤˙b→a+˙c≤˙b+˙c
43 42 2ralbidv ⊢m=M∧l=≤m→∀a∈B∀b∈B∀c∈Balb→a+˙clb+˙c↔∀a∈B∀b∈B∀c∈Ba≤˙b→a+˙c≤˙b+˙c
44 43 anbi2d ⊢m=M∧l=≤m→m∈Toset∧∀a∈B∀b∈B∀c∈Balb→a+˙clb+˙c↔m∈Toset∧∀a∈B∀b∈B∀c∈Ba≤˙b→a+˙c≤˙b+˙c
45 33 44 sbcied ⊢m=M→[˙≤m/l]˙m∈Toset∧∀a∈B∀b∈B∀c∈Balb→a+˙clb+˙c↔m∈Toset∧∀a∈B∀b∈B∀c∈Ba≤˙b→a+˙c≤˙b+˙c
46 eleq1 ⊢m=M→m∈Toset↔M∈Toset
47 46 anbi1d ⊢m=M→m∈Toset∧∀a∈B∀b∈B∀c∈Ba≤˙b→a+˙c≤˙b+˙c↔M∈Toset∧∀a∈B∀b∈B∀c∈Ba≤˙b→a+˙c≤˙b+˙c
48 45 47 bitrd ⊢m=M→[˙≤m/l]˙m∈Toset∧∀a∈B∀b∈B∀c∈Balb→a+˙clb+˙c↔M∈Toset∧∀a∈B∀b∈B∀c∈Ba≤˙b→a+˙c≤˙b+˙c
49 17 32 48 3bitrd ⊢m=M→[˙Basem/v]˙[˙+m/p]˙[˙≤m/l]˙m∈Toset∧∀a∈v∀b∈v∀c∈valb→apclbpc↔M∈Toset∧∀a∈B∀b∈B∀c∈Ba≤˙b→a+˙c≤˙b+˙c
50 df-omnd ⊢oMnd=m∈Mnd|[˙Basem/v]˙[˙+m/p]˙[˙≤m/l]˙m∈Toset∧∀a∈v∀b∈v∀c∈valb→apclbpc
51 49 50 elrab2 ⊢M∈oMnd↔M∈Mnd∧M∈Toset∧∀a∈B∀b∈B∀c∈Ba≤˙b→a+˙c≤˙b+˙c
52 3anass ⊢M∈Mnd∧M∈Toset∧∀a∈B∀b∈B∀c∈Ba≤˙b→a+˙c≤˙b+˙c↔M∈Mnd∧M∈Toset∧∀a∈B∀b∈B∀c∈Ba≤˙b→a+˙c≤˙b+˙c
53 51 52 bitr4i ⊢M∈oMnd↔M∈Mnd∧M∈Toset∧∀a∈B∀b∈B∀c∈Ba≤˙b→a+˙c≤˙b+˙c