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

Proof

Step Hyp Ref Expression
1 isomnd.0 ⊢ B = Base M
2 isomnd.1 ⊢ + ˙ = + M
3 isomnd.2 ⊢ ≤ ˙ = ≤ M
4 fvexd ⊢ m = M → Base m ∈ 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 → ∀ c ∈ v a l b → a p c l b p c ↔ ∀ c ∈ B a l b → a p c l b p c
11 10 raleqbi1dv ⊢ v = B → ∀ b ∈ v ∀ c ∈ v a l b → a p c l b p c ↔ ∀ b ∈ B ∀ c ∈ B a l b → a p c l b p c
12 11 raleqbi1dv ⊢ v = B → ∀ a ∈ v ∀ b ∈ v ∀ c ∈ v a l b → a p c l b p c ↔ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a l b → a p c l b p c
13 9 12 syl ⊢ m = M ∧ v = Base m → ∀ a ∈ v ∀ b ∈ v ∀ c ∈ v a l b → a p c l b p c ↔ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a l b → a p c l b p c
14 13 anbi2d ⊢ m = M ∧ v = Base m → m ∈ Toset ∧ ∀ a ∈ v ∀ b ∈ v ∀ c ∈ v a l b → a p c l b p c ↔ m ∈ Toset ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a l b → a p c l b p c
15 14 sbcbidv ⊢ m = M ∧ v = Base m → [˙≤ m / l]˙ m ∈ Toset ∧ ∀ a ∈ v ∀ b ∈ v ∀ c ∈ v a l b → a p c l b p c ↔ [˙≤ m / l]˙ m ∈ Toset ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a l b → a p c l b p c
16 15 sbcbidv ⊢ m = M ∧ v = Base m → [˙+ m / p]˙ [˙≤ m / l]˙ m ∈ Toset ∧ ∀ a ∈ v ∀ b ∈ v ∀ c ∈ v a l b → a p c l b p c ↔ [˙+ m / p]˙ [˙≤ m / l]˙ m ∈ Toset ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a l b → a p c l b p c
17 4 16 sbcied ⊢ m = M → [˙Base m / v]˙ [˙+ m / p]˙ [˙≤ m / l]˙ m ∈ Toset ∧ ∀ a ∈ v ∀ b ∈ v ∀ c ∈ v a l b → a p c l b p c ↔ [˙+ m / p]˙ [˙≤ m / l]˙ m ∈ Toset ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a l b → a p c l b p c
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 → a p c = a + ˙ c
25 23 oveqd ⊢ m = M ∧ p = + m → b p c = b + ˙ c
26 24 25 breq12d ⊢ m = M ∧ p = + m → a p c l b p c ↔ a + ˙ c l b + ˙ c
27 26 imbi2d ⊢ m = M ∧ p = + 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 = + m → ∀ c ∈ B a l b → a p c l b p c ↔ ∀ c ∈ B a l b → a + ˙ c l b + ˙ c
29 28 2ralbidv ⊢ m = M ∧ p = + m → ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a l b → a p c l b p c ↔ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a l b → a + ˙ c l b + ˙ c
30 29 anbi2d ⊢ m = M ∧ p = + m → m ∈ Toset ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a l b → a p c l b p c ↔ m ∈ Toset ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a l b → a + ˙ c l b + ˙ c
31 30 sbcbidv ⊢ m = M ∧ p = + m → [˙≤ m / l]˙ m ∈ Toset ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a l b → a p c l b p c ↔ [˙≤ m / l]˙ m ∈ Toset ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a l b → a + ˙ c l b + ˙ c
32 18 31 sbcied ⊢ m = M → [˙+ m / p]˙ [˙≤ m / l]˙ m ∈ Toset ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a l b → a p c l b p c ↔ [˙≤ m / l]˙ m ∈ Toset ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a l b → a + ˙ c l b + ˙ 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 → a l b ↔ a ≤ ˙ b
40 38 breqd ⊢ m = M ∧ l = ≤ m → a + ˙ c l b + ˙ c ↔ a + ˙ c ≤ ˙ b + ˙ c
41 39 40 imbi12d ⊢ m = M ∧ l = ≤ m → a l b → a + ˙ c l b + ˙ c ↔ a ≤ ˙ b → a + ˙ c ≤ ˙ b + ˙ c
42 41 ralbidv ⊢ m = M ∧ l = ≤ m → ∀ c ∈ B a l b → a + ˙ c l b + ˙ c ↔ ∀ c ∈ B a ≤ ˙ b → a + ˙ c ≤ ˙ b + ˙ c
43 42 2ralbidv ⊢ m = M ∧ l = ≤ m → ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a l b → a + ˙ c l b + ˙ c ↔ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a ≤ ˙ b → a + ˙ c ≤ ˙ b + ˙ c
44 43 anbi2d ⊢ m = M ∧ l = ≤ m → m ∈ Toset ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a l b → a + ˙ c l b + ˙ c ↔ m ∈ Toset ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a ≤ ˙ b → a + ˙ c ≤ ˙ b + ˙ c
45 33 44 sbcied ⊢ m = M → [˙≤ m / l]˙ m ∈ Toset ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a l b → a + ˙ c l b + ˙ c ↔ m ∈ Toset ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a ≤ ˙ 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 ∈ B a ≤ ˙ b → a + ˙ c ≤ ˙ b + ˙ c ↔ M ∈ Toset ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a ≤ ˙ b → a + ˙ c ≤ ˙ b + ˙ c
48 45 47 bitrd ⊢ m = M → [˙≤ m / l]˙ m ∈ Toset ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a l b → a + ˙ c l b + ˙ c ↔ M ∈ Toset ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a ≤ ˙ b → a + ˙ c ≤ ˙ b + ˙ c
49 17 32 48 3bitrd ⊢ m = M → [˙Base m / v]˙ [˙+ m / p]˙ [˙≤ m / l]˙ m ∈ Toset ∧ ∀ a ∈ v ∀ b ∈ v ∀ c ∈ v a l b → a p c l b p c ↔ M ∈ Toset ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a ≤ ˙ b → a + ˙ c ≤ ˙ b + ˙ c
50 df-omnd ⊢ oMnd = m ∈ Mnd | [˙Base m / v]˙ [˙+ m / p]˙ [˙≤ m / l]˙ m ∈ Toset ∧ ∀ a ∈ v ∀ b ∈ v ∀ c ∈ v a l b → a p c l b p c
51 49 50 elrab2 ⊢ M ∈ oMnd ↔ M ∈ Mnd ∧ M ∈ Toset ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a ≤ ˙ b → a + ˙ c ≤ ˙ b + ˙ c
52 3anass ⊢ M ∈ Mnd ∧ M ∈ Toset ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a ≤ ˙ b → a + ˙ c ≤ ˙ b + ˙ c ↔ M ∈ Mnd ∧ M ∈ Toset ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a ≤ ˙ b → a + ˙ c ≤ ˙ b + ˙ c
53 51 52 bitr4i ⊢ M ∈ oMnd ↔ M ∈ Mnd ∧ M ∈ Toset ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a ≤ ˙ b → a + ˙ c ≤ ˙ b + ˙ c