Metamath Proof Explorer

Theorem submomnd

Description: A submonoid of an ordered monoid is also ordered. (Contributed by Thierry Arnoux, 23-Mar-2018)

Ref Expression
Assertion submomnd ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd → M ↾ 𝑠 A ∈ oMnd

Proof

Step Hyp Ref Expression
1 simpr ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd → M ↾ 𝑠 A ∈ Mnd
2 omndtos ⊢ M ∈ oMnd → M ∈ Toset
3 2 adantr ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd → M ∈ Toset
4 reldmress ⊢ Rel ⁡ dom ⁡ ↾ 𝑠
5 4 ovprc2 ⊢ ¬ A ∈ V → M ↾ 𝑠 A = ∅
6 5 fveq2d ⊢ ¬ A ∈ V → Base M ↾ 𝑠 A = Base ∅
7 6 adantl ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ ¬ A ∈ V → Base M ↾ 𝑠 A = Base ∅
8 base0 ⊢ ∅ = Base ∅
9 7 8 eqtr4di ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ ¬ A ∈ V → Base M ↾ 𝑠 A = ∅
10 eqid ⊢ Base M ↾ 𝑠 A = Base M ↾ 𝑠 A
11 eqid ⊢ 0 M ↾ 𝑠 A = 0 M ↾ 𝑠 A
12 10 11 mndidcl ⊢ M ↾ 𝑠 A ∈ Mnd → 0 M ↾ 𝑠 A ∈ Base M ↾ 𝑠 A
13 12 ne0d ⊢ M ↾ 𝑠 A ∈ Mnd → Base M ↾ 𝑠 A ≠ ∅
14 13 ad2antlr ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ ¬ A ∈ V → Base M ↾ 𝑠 A ≠ ∅
15 14 neneqd ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ ¬ A ∈ V → ¬ Base M ↾ 𝑠 A = ∅
16 9 15 condan ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd → A ∈ V
17 resstos ⊢ M ∈ Toset ∧ A ∈ V → M ↾ 𝑠 A ∈ Toset
18 3 16 17 syl2anc ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd → M ↾ 𝑠 A ∈ Toset
19 simplll ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ a ∈ Base M ↾ 𝑠 A ∧ b ∈ Base M ↾ 𝑠 A ∧ c ∈ Base M ↾ 𝑠 A ∧ a ≤ M ↾ 𝑠 A b → M ∈ oMnd
20 eqid ⊢ M ↾ 𝑠 A = M ↾ 𝑠 A
21 eqid ⊢ Base M = Base M
22 20 21 ressbas ⊢ A ∈ V → A ∩ Base M = Base M ↾ 𝑠 A
23 inss2 ⊢ A ∩ Base M ⊆ Base M
24 22 23 eqsstrrdi ⊢ A ∈ V → Base M ↾ 𝑠 A ⊆ Base M
25 16 24 syl ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd → Base M ↾ 𝑠 A ⊆ Base M
26 25 ad2antrr ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ a ∈ Base M ↾ 𝑠 A ∧ b ∈ Base M ↾ 𝑠 A ∧ c ∈ Base M ↾ 𝑠 A ∧ a ≤ M ↾ 𝑠 A b → Base M ↾ 𝑠 A ⊆ Base M
27 simplr1 ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ a ∈ Base M ↾ 𝑠 A ∧ b ∈ Base M ↾ 𝑠 A ∧ c ∈ Base M ↾ 𝑠 A ∧ a ≤ M ↾ 𝑠 A b → a ∈ Base M ↾ 𝑠 A
28 26 27 sseldd ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ a ∈ Base M ↾ 𝑠 A ∧ b ∈ Base M ↾ 𝑠 A ∧ c ∈ Base M ↾ 𝑠 A ∧ a ≤ M ↾ 𝑠 A b → a ∈ Base M
29 simplr2 ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ a ∈ Base M ↾ 𝑠 A ∧ b ∈ Base M ↾ 𝑠 A ∧ c ∈ Base M ↾ 𝑠 A ∧ a ≤ M ↾ 𝑠 A b → b ∈ Base M ↾ 𝑠 A
30 26 29 sseldd ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ a ∈ Base M ↾ 𝑠 A ∧ b ∈ Base M ↾ 𝑠 A ∧ c ∈ Base M ↾ 𝑠 A ∧ a ≤ M ↾ 𝑠 A b → b ∈ Base M
31 simplr3 ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ a ∈ Base M ↾ 𝑠 A ∧ b ∈ Base M ↾ 𝑠 A ∧ c ∈ Base M ↾ 𝑠 A ∧ a ≤ M ↾ 𝑠 A b → c ∈ Base M ↾ 𝑠 A
32 26 31 sseldd ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ a ∈ Base M ↾ 𝑠 A ∧ b ∈ Base M ↾ 𝑠 A ∧ c ∈ Base M ↾ 𝑠 A ∧ a ≤ M ↾ 𝑠 A b → c ∈ Base M
33 eqid ⊢ ≤ M = ≤ M
34 20 33 ressle ⊢ A ∈ V → ≤ M = ≤ M ↾ 𝑠 A
35 16 34 syl ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd → ≤ M = ≤ M ↾ 𝑠 A
36 35 adantr ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ a ∈ Base M ↾ 𝑠 A ∧ b ∈ Base M ↾ 𝑠 A ∧ c ∈ Base M ↾ 𝑠 A → ≤ M = ≤ M ↾ 𝑠 A
37 36 breqd ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ a ∈ Base M ↾ 𝑠 A ∧ b ∈ Base M ↾ 𝑠 A ∧ c ∈ Base M ↾ 𝑠 A → a ≤ M b ↔ a ≤ M ↾ 𝑠 A b
38 37 biimpar ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ a ∈ Base M ↾ 𝑠 A ∧ b ∈ Base M ↾ 𝑠 A ∧ c ∈ Base M ↾ 𝑠 A ∧ a ≤ M ↾ 𝑠 A b → a ≤ M b
39 eqid ⊢ + M = + M
40 21 33 39 omndadd ⊢ M ∈ oMnd ∧ a ∈ Base M ∧ b ∈ Base M ∧ c ∈ Base M ∧ a ≤ M b → a + M c ≤ M b + M c
41 19 28 30 32 38 40 syl131anc ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ a ∈ Base M ↾ 𝑠 A ∧ b ∈ Base M ↾ 𝑠 A ∧ c ∈ Base M ↾ 𝑠 A ∧ a ≤ M ↾ 𝑠 A b → a + M c ≤ M b + M c
42 16 adantr ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ a ∈ Base M ↾ 𝑠 A ∧ b ∈ Base M ↾ 𝑠 A ∧ c ∈ Base M ↾ 𝑠 A → A ∈ V
43 20 39 ressplusg ⊢ A ∈ V → + M = + M ↾ 𝑠 A
44 42 43 syl ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ a ∈ Base M ↾ 𝑠 A ∧ b ∈ Base M ↾ 𝑠 A ∧ c ∈ Base M ↾ 𝑠 A → + M = + M ↾ 𝑠 A
45 44 oveqd ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ a ∈ Base M ↾ 𝑠 A ∧ b ∈ Base M ↾ 𝑠 A ∧ c ∈ Base M ↾ 𝑠 A → a + M c = a + M ↾ 𝑠 A c
46 42 34 syl ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ a ∈ Base M ↾ 𝑠 A ∧ b ∈ Base M ↾ 𝑠 A ∧ c ∈ Base M ↾ 𝑠 A → ≤ M = ≤ M ↾ 𝑠 A
47 44 oveqd ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ a ∈ Base M ↾ 𝑠 A ∧ b ∈ Base M ↾ 𝑠 A ∧ c ∈ Base M ↾ 𝑠 A → b + M c = b + M ↾ 𝑠 A c
48 45 46 47 breq123d ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ a ∈ Base M ↾ 𝑠 A ∧ b ∈ Base M ↾ 𝑠 A ∧ c ∈ Base M ↾ 𝑠 A → a + M c ≤ M b + M c ↔ a + M ↾ 𝑠 A c ≤ M ↾ 𝑠 A b + M ↾ 𝑠 A c
49 48 adantr ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ a ∈ Base M ↾ 𝑠 A ∧ b ∈ Base M ↾ 𝑠 A ∧ c ∈ Base M ↾ 𝑠 A ∧ a ≤ M ↾ 𝑠 A b → a + M c ≤ M b + M c ↔ a + M ↾ 𝑠 A c ≤ M ↾ 𝑠 A b + M ↾ 𝑠 A c
50 41 49 mpbid ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ a ∈ Base M ↾ 𝑠 A ∧ b ∈ Base M ↾ 𝑠 A ∧ c ∈ Base M ↾ 𝑠 A ∧ a ≤ M ↾ 𝑠 A b → a + M ↾ 𝑠 A c ≤ M ↾ 𝑠 A b + M ↾ 𝑠 A c
51 50 ex ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd ∧ a ∈ Base M ↾ 𝑠 A ∧ b ∈ Base M ↾ 𝑠 A ∧ c ∈ Base M ↾ 𝑠 A → a ≤ M ↾ 𝑠 A b → a + M ↾ 𝑠 A c ≤ M ↾ 𝑠 A b + M ↾ 𝑠 A c
52 51 ralrimivvva ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd → ∀ a ∈ Base M ↾ 𝑠 A ∀ b ∈ Base M ↾ 𝑠 A ∀ c ∈ Base M ↾ 𝑠 A a ≤ M ↾ 𝑠 A b → a + M ↾ 𝑠 A c ≤ M ↾ 𝑠 A b + M ↾ 𝑠 A c
53 eqid ⊢ + M ↾ 𝑠 A = + M ↾ 𝑠 A
54 eqid ⊢ ≤ M ↾ 𝑠 A = ≤ M ↾ 𝑠 A
55 10 53 54 isomnd ⊢ M ↾ 𝑠 A ∈ oMnd ↔ M ↾ 𝑠 A ∈ Mnd ∧ M ↾ 𝑠 A ∈ Toset ∧ ∀ a ∈ Base M ↾ 𝑠 A ∀ b ∈ Base M ↾ 𝑠 A ∀ c ∈ Base M ↾ 𝑠 A a ≤ M ↾ 𝑠 A b → a + M ↾ 𝑠 A c ≤ M ↾ 𝑠 A b + M ↾ 𝑠 A c
56 1 18 52 55 syl3anbrc ⊢ M ∈ oMnd ∧ M ↾ 𝑠 A ∈ Mnd → M ↾ 𝑠 A ∈ oMnd