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