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→BaseM↾𝑠A=Base∅
7 6 adantl ⊢M∈oMnd∧M↾𝑠A∈Mnd∧¬A∈V→BaseM↾𝑠A=Base∅
8 base0 ⊢∅=Base∅
9 7 8 eqtr4di ⊢M∈oMnd∧M↾𝑠A∈Mnd∧¬A∈V→BaseM↾𝑠A=∅
10 eqid ⊢BaseM↾𝑠A=BaseM↾𝑠A
11 eqid ⊢0M↾𝑠A=0M↾𝑠A
12 10 11 mndidcl ⊢M↾𝑠A∈Mnd→0M↾𝑠A∈BaseM↾𝑠A
13 12 ne0d ⊢M↾𝑠A∈Mnd→BaseM↾𝑠A≠∅
14 13 ad2antlr ⊢M∈oMnd∧M↾𝑠A∈Mnd∧¬A∈V→BaseM↾𝑠A≠∅
15 14 neneqd ⊢M∈oMnd∧M↾𝑠A∈Mnd∧¬A∈V→¬BaseM↾𝑠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∈BaseM↾𝑠A∧b∈BaseM↾𝑠A∧c∈BaseM↾𝑠A∧a≤M↾𝑠Ab→M∈oMnd
20 eqid ⊢M↾𝑠A=M↾𝑠A
21 eqid ⊢BaseM=BaseM
22 20 21 ressbas ⊢A∈V→A∩BaseM=BaseM↾𝑠A
23 inss2 ⊢A∩BaseM⊆BaseM
24 22 23 eqsstrrdi ⊢A∈V→BaseM↾𝑠A⊆BaseM
25 16 24 syl ⊢M∈oMnd∧M↾𝑠A∈Mnd→BaseM↾𝑠A⊆BaseM
26 25 ad2antrr ⊢M∈oMnd∧M↾𝑠A∈Mnd∧a∈BaseM↾𝑠A∧b∈BaseM↾𝑠A∧c∈BaseM↾𝑠A∧a≤M↾𝑠Ab→BaseM↾𝑠A⊆BaseM
27 simplr1 ⊢M∈oMnd∧M↾𝑠A∈Mnd∧a∈BaseM↾𝑠A∧b∈BaseM↾𝑠A∧c∈BaseM↾𝑠A∧a≤M↾𝑠Ab→a∈BaseM↾𝑠A
28 26 27 sseldd ⊢M∈oMnd∧M↾𝑠A∈Mnd∧a∈BaseM↾𝑠A∧b∈BaseM↾𝑠A∧c∈BaseM↾𝑠A∧a≤M↾𝑠Ab→a∈BaseM
29 simplr2 ⊢M∈oMnd∧M↾𝑠A∈Mnd∧a∈BaseM↾𝑠A∧b∈BaseM↾𝑠A∧c∈BaseM↾𝑠A∧a≤M↾𝑠Ab→b∈BaseM↾𝑠A
30 26 29 sseldd ⊢M∈oMnd∧M↾𝑠A∈Mnd∧a∈BaseM↾𝑠A∧b∈BaseM↾𝑠A∧c∈BaseM↾𝑠A∧a≤M↾𝑠Ab→b∈BaseM
31 simplr3 ⊢M∈oMnd∧M↾𝑠A∈Mnd∧a∈BaseM↾𝑠A∧b∈BaseM↾𝑠A∧c∈BaseM↾𝑠A∧a≤M↾𝑠Ab→c∈BaseM↾𝑠A
32 26 31 sseldd ⊢M∈oMnd∧M↾𝑠A∈Mnd∧a∈BaseM↾𝑠A∧b∈BaseM↾𝑠A∧c∈BaseM↾𝑠A∧a≤M↾𝑠Ab→c∈BaseM
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∈BaseM↾𝑠A∧b∈BaseM↾𝑠A∧c∈BaseM↾𝑠A→≤M=≤M↾𝑠A
37 36 breqd ⊢M∈oMnd∧M↾𝑠A∈Mnd∧a∈BaseM↾𝑠A∧b∈BaseM↾𝑠A∧c∈BaseM↾𝑠A→a≤Mb↔a≤M↾𝑠Ab
38 37 biimpar ⊢M∈oMnd∧M↾𝑠A∈Mnd∧a∈BaseM↾𝑠A∧b∈BaseM↾𝑠A∧c∈BaseM↾𝑠A∧a≤M↾𝑠Ab→a≤Mb
39 eqid ⊢+M=+M
40 21 33 39 omndadd ⊢M∈oMnd∧a∈BaseM∧b∈BaseM∧c∈BaseM∧a≤Mb→a+Mc≤Mb+Mc
41 19 28 30 32 38 40 syl131anc ⊢M∈oMnd∧M↾𝑠A∈Mnd∧a∈BaseM↾𝑠A∧b∈BaseM↾𝑠A∧c∈BaseM↾𝑠A∧a≤M↾𝑠Ab→a+Mc≤Mb+Mc
42 16 adantr ⊢M∈oMnd∧M↾𝑠A∈Mnd∧a∈BaseM↾𝑠A∧b∈BaseM↾𝑠A∧c∈BaseM↾𝑠A→A∈V
43 20 39 ressplusg ⊢A∈V→+M=+M↾𝑠A
44 42 43 syl ⊢M∈oMnd∧M↾𝑠A∈Mnd∧a∈BaseM↾𝑠A∧b∈BaseM↾𝑠A∧c∈BaseM↾𝑠A→+M=+M↾𝑠A
45 44 oveqd ⊢M∈oMnd∧M↾𝑠A∈Mnd∧a∈BaseM↾𝑠A∧b∈BaseM↾𝑠A∧c∈BaseM↾𝑠A→a+Mc=a+M↾𝑠Ac
46 42 34 syl ⊢M∈oMnd∧M↾𝑠A∈Mnd∧a∈BaseM↾𝑠A∧b∈BaseM↾𝑠A∧c∈BaseM↾𝑠A→≤M=≤M↾𝑠A
47 44 oveqd ⊢M∈oMnd∧M↾𝑠A∈Mnd∧a∈BaseM↾𝑠A∧b∈BaseM↾𝑠A∧c∈BaseM↾𝑠A→b+Mc=b+M↾𝑠Ac
48 45 46 47 breq123d ⊢M∈oMnd∧M↾𝑠A∈Mnd∧a∈BaseM↾𝑠A∧b∈BaseM↾𝑠A∧c∈BaseM↾𝑠A→a+Mc≤Mb+Mc↔a+M↾𝑠Ac≤M↾𝑠Ab+M↾𝑠Ac
49 48 adantr ⊢M∈oMnd∧M↾𝑠A∈Mnd∧a∈BaseM↾𝑠A∧b∈BaseM↾𝑠A∧c∈BaseM↾𝑠A∧a≤M↾𝑠Ab→a+Mc≤Mb+Mc↔a+M↾𝑠Ac≤M↾𝑠Ab+M↾𝑠Ac
50 41 49 mpbid ⊢M∈oMnd∧M↾𝑠A∈Mnd∧a∈BaseM↾𝑠A∧b∈BaseM↾𝑠A∧c∈BaseM↾𝑠A∧a≤M↾𝑠Ab→a+M↾𝑠Ac≤M↾𝑠Ab+M↾𝑠Ac
51 50 ex ⊢M∈oMnd∧M↾𝑠A∈Mnd∧a∈BaseM↾𝑠A∧b∈BaseM↾𝑠A∧c∈BaseM↾𝑠A→a≤M↾𝑠Ab→a+M↾𝑠Ac≤M↾𝑠Ab+M↾𝑠Ac
52 51 ralrimivvva ⊢M∈oMnd∧M↾𝑠A∈Mnd→∀a∈BaseM↾𝑠A∀b∈BaseM↾𝑠A∀c∈BaseM↾𝑠Aa≤M↾𝑠Ab→a+M↾𝑠Ac≤M↾𝑠Ab+M↾𝑠Ac
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∈BaseM↾𝑠A∀b∈BaseM↾𝑠A∀c∈BaseM↾𝑠Aa≤M↾𝑠Ab→a+M↾𝑠Ac≤M↾𝑠Ab+M↾𝑠Ac
56 1 18 52 55 syl3anbrc ⊢M∈oMnd∧M↾𝑠A∈Mnd→M↾𝑠A∈oMnd