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 e. oMnd /\ ( M |`s A ) e. Mnd ) -> ( M |`s A ) e. oMnd )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) -> ( M |`s A ) e. Mnd )
2 omndtos 
 |-  ( M e. oMnd -> M e. Toset )
3 2 adantr 
 |-  ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) -> M e. Toset )
4 reldmress 
 |-  Rel dom |`s
5 4 ovprc2 
 |-  ( -. A e. _V -> ( M |`s A ) = (/) )
6 5 fveq2d 
 |-  ( -. A e. _V -> ( Base ` ( M |`s A ) ) = ( Base ` (/) ) )
7 6 adantl 
 |-  ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ -. A e. _V ) -> ( Base ` ( M |`s A ) ) = ( Base ` (/) ) )
8 base0 
 |-  (/) = ( Base ` (/) )
9 7 8 eqtr4di 
 |-  ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ -. A e. _V ) -> ( Base ` ( M |`s A ) ) = (/) )
10 eqid 
 |-  ( Base ` ( M |`s A ) ) = ( Base ` ( M |`s A ) )
11 eqid 
 |-  ( 0g ` ( M |`s A ) ) = ( 0g ` ( M |`s A ) )
12 10 11 mndidcl 
 |-  ( ( M |`s A ) e. Mnd -> ( 0g ` ( M |`s A ) ) e. ( Base ` ( M |`s A ) ) )
13 12 ne0d 
 |-  ( ( M |`s A ) e. Mnd -> ( Base ` ( M |`s A ) ) =/= (/) )
14 13 ad2antlr 
 |-  ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ -. A e. _V ) -> ( Base ` ( M |`s A ) ) =/= (/) )
15 14 neneqd 
 |-  ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ -. A e. _V ) -> -. ( Base ` ( M |`s A ) ) = (/) )
16 9 15 condan 
 |-  ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) -> A e. _V )
17 resstos 
 |-  ( ( M e. Toset /\ A e. _V ) -> ( M |`s A ) e. Toset )
18 3 16 17 syl2anc 
 |-  ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) -> ( M |`s A ) e. Toset )
19 simplll 
 |-  ( ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ ( a e. ( Base ` ( M |`s A ) ) /\ b e. ( Base ` ( M |`s A ) ) /\ c e. ( Base ` ( M |`s A ) ) ) ) /\ a ( le ` ( M |`s A ) ) b ) -> M e. oMnd )
20 eqid 
 |-  ( M |`s A ) = ( M |`s A )
21 eqid 
 |-  ( Base ` M ) = ( Base ` M )
22 20 21 ressbas 
 |-  ( A e. _V -> ( A i^i ( Base ` M ) ) = ( Base ` ( M |`s A ) ) )
23 inss2 
 |-  ( A i^i ( Base ` M ) ) C_ ( Base ` M )
24 22 23 eqsstrrdi 
 |-  ( A e. _V -> ( Base ` ( M |`s A ) ) C_ ( Base ` M ) )
25 16 24 syl 
 |-  ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) -> ( Base ` ( M |`s A ) ) C_ ( Base ` M ) )
26 25 ad2antrr 
 |-  ( ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ ( a e. ( Base ` ( M |`s A ) ) /\ b e. ( Base ` ( M |`s A ) ) /\ c e. ( Base ` ( M |`s A ) ) ) ) /\ a ( le ` ( M |`s A ) ) b ) -> ( Base ` ( M |`s A ) ) C_ ( Base ` M ) )
27 simplr1 
 |-  ( ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ ( a e. ( Base ` ( M |`s A ) ) /\ b e. ( Base ` ( M |`s A ) ) /\ c e. ( Base ` ( M |`s A ) ) ) ) /\ a ( le ` ( M |`s A ) ) b ) -> a e. ( Base ` ( M |`s A ) ) )
28 26 27 sseldd 
 |-  ( ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ ( a e. ( Base ` ( M |`s A ) ) /\ b e. ( Base ` ( M |`s A ) ) /\ c e. ( Base ` ( M |`s A ) ) ) ) /\ a ( le ` ( M |`s A ) ) b ) -> a e. ( Base ` M ) )
29 simplr2 
 |-  ( ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ ( a e. ( Base ` ( M |`s A ) ) /\ b e. ( Base ` ( M |`s A ) ) /\ c e. ( Base ` ( M |`s A ) ) ) ) /\ a ( le ` ( M |`s A ) ) b ) -> b e. ( Base ` ( M |`s A ) ) )
30 26 29 sseldd 
 |-  ( ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ ( a e. ( Base ` ( M |`s A ) ) /\ b e. ( Base ` ( M |`s A ) ) /\ c e. ( Base ` ( M |`s A ) ) ) ) /\ a ( le ` ( M |`s A ) ) b ) -> b e. ( Base ` M ) )
31 simplr3 
 |-  ( ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ ( a e. ( Base ` ( M |`s A ) ) /\ b e. ( Base ` ( M |`s A ) ) /\ c e. ( Base ` ( M |`s A ) ) ) ) /\ a ( le ` ( M |`s A ) ) b ) -> c e. ( Base ` ( M |`s A ) ) )
32 26 31 sseldd 
 |-  ( ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ ( a e. ( Base ` ( M |`s A ) ) /\ b e. ( Base ` ( M |`s A ) ) /\ c e. ( Base ` ( M |`s A ) ) ) ) /\ a ( le ` ( M |`s A ) ) b ) -> c e. ( Base ` M ) )
33 eqid 
 |-  ( le ` M ) = ( le ` M )
34 20 33 ressle 
 |-  ( A e. _V -> ( le ` M ) = ( le ` ( M |`s A ) ) )
35 16 34 syl 
 |-  ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) -> ( le ` M ) = ( le ` ( M |`s A ) ) )
36 35 adantr 
 |-  ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ ( a e. ( Base ` ( M |`s A ) ) /\ b e. ( Base ` ( M |`s A ) ) /\ c e. ( Base ` ( M |`s A ) ) ) ) -> ( le ` M ) = ( le ` ( M |`s A ) ) )
37 36 breqd 
 |-  ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ ( a e. ( Base ` ( M |`s A ) ) /\ b e. ( Base ` ( M |`s A ) ) /\ c e. ( Base ` ( M |`s A ) ) ) ) -> ( a ( le ` M ) b <-> a ( le ` ( M |`s A ) ) b ) )
38 37 biimpar 
 |-  ( ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ ( a e. ( Base ` ( M |`s A ) ) /\ b e. ( Base ` ( M |`s A ) ) /\ c e. ( Base ` ( M |`s A ) ) ) ) /\ a ( le ` ( M |`s A ) ) b ) -> a ( le ` M ) b )
39 eqid 
 |-  ( +g ` M ) = ( +g ` M )
40 21 33 39 omndadd 
 |-  ( ( M e. oMnd /\ ( a e. ( Base ` M ) /\ b e. ( Base ` M ) /\ c e. ( Base ` M ) ) /\ a ( le ` M ) b ) -> ( a ( +g ` M ) c ) ( le ` M ) ( b ( +g ` M ) c ) )
41 19 28 30 32 38 40 syl131anc 
 |-  ( ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ ( a e. ( Base ` ( M |`s A ) ) /\ b e. ( Base ` ( M |`s A ) ) /\ c e. ( Base ` ( M |`s A ) ) ) ) /\ a ( le ` ( M |`s A ) ) b ) -> ( a ( +g ` M ) c ) ( le ` M ) ( b ( +g ` M ) c ) )
42 16 adantr 
 |-  ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ ( a e. ( Base ` ( M |`s A ) ) /\ b e. ( Base ` ( M |`s A ) ) /\ c e. ( Base ` ( M |`s A ) ) ) ) -> A e. _V )
43 20 39 ressplusg 
 |-  ( A e. _V -> ( +g ` M ) = ( +g ` ( M |`s A ) ) )
44 42 43 syl 
 |-  ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ ( a e. ( Base ` ( M |`s A ) ) /\ b e. ( Base ` ( M |`s A ) ) /\ c e. ( Base ` ( M |`s A ) ) ) ) -> ( +g ` M ) = ( +g ` ( M |`s A ) ) )
45 44 oveqd 
 |-  ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ ( a e. ( Base ` ( M |`s A ) ) /\ b e. ( Base ` ( M |`s A ) ) /\ c e. ( Base ` ( M |`s A ) ) ) ) -> ( a ( +g ` M ) c ) = ( a ( +g ` ( M |`s A ) ) c ) )
46 42 34 syl 
 |-  ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ ( a e. ( Base ` ( M |`s A ) ) /\ b e. ( Base ` ( M |`s A ) ) /\ c e. ( Base ` ( M |`s A ) ) ) ) -> ( le ` M ) = ( le ` ( M |`s A ) ) )
47 44 oveqd 
 |-  ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ ( a e. ( Base ` ( M |`s A ) ) /\ b e. ( Base ` ( M |`s A ) ) /\ c e. ( Base ` ( M |`s A ) ) ) ) -> ( b ( +g ` M ) c ) = ( b ( +g ` ( M |`s A ) ) c ) )
48 45 46 47 breq123d 
 |-  ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ ( a e. ( Base ` ( M |`s A ) ) /\ b e. ( Base ` ( M |`s A ) ) /\ c e. ( Base ` ( M |`s A ) ) ) ) -> ( ( a ( +g ` M ) c ) ( le ` M ) ( b ( +g ` M ) c ) <-> ( a ( +g ` ( M |`s A ) ) c ) ( le ` ( M |`s A ) ) ( b ( +g ` ( M |`s A ) ) c ) ) )
49 48 adantr 
 |-  ( ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ ( a e. ( Base ` ( M |`s A ) ) /\ b e. ( Base ` ( M |`s A ) ) /\ c e. ( Base ` ( M |`s A ) ) ) ) /\ a ( le ` ( M |`s A ) ) b ) -> ( ( a ( +g ` M ) c ) ( le ` M ) ( b ( +g ` M ) c ) <-> ( a ( +g ` ( M |`s A ) ) c ) ( le ` ( M |`s A ) ) ( b ( +g ` ( M |`s A ) ) c ) ) )
50 41 49 mpbid 
 |-  ( ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ ( a e. ( Base ` ( M |`s A ) ) /\ b e. ( Base ` ( M |`s A ) ) /\ c e. ( Base ` ( M |`s A ) ) ) ) /\ a ( le ` ( M |`s A ) ) b ) -> ( a ( +g ` ( M |`s A ) ) c ) ( le ` ( M |`s A ) ) ( b ( +g ` ( M |`s A ) ) c ) )
51 50 ex 
 |-  ( ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) /\ ( a e. ( Base ` ( M |`s A ) ) /\ b e. ( Base ` ( M |`s A ) ) /\ c e. ( Base ` ( M |`s A ) ) ) ) -> ( a ( le ` ( M |`s A ) ) b -> ( a ( +g ` ( M |`s A ) ) c ) ( le ` ( M |`s A ) ) ( b ( +g ` ( M |`s A ) ) c ) ) )
52 51 ralrimivvva 
 |-  ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) -> A. a e. ( Base ` ( M |`s A ) ) A. b e. ( Base ` ( M |`s A ) ) A. c e. ( Base ` ( M |`s A ) ) ( a ( le ` ( M |`s A ) ) b -> ( a ( +g ` ( M |`s A ) ) c ) ( le ` ( M |`s A ) ) ( b ( +g ` ( M |`s A ) ) c ) ) )
53 eqid 
 |-  ( +g ` ( M |`s A ) ) = ( +g ` ( M |`s A ) )
54 eqid 
 |-  ( le ` ( M |`s A ) ) = ( le ` ( M |`s A ) )
55 10 53 54 isomnd 
 |-  ( ( M |`s A ) e. oMnd <-> ( ( M |`s A ) e. Mnd /\ ( M |`s A ) e. Toset /\ A. a e. ( Base ` ( M |`s A ) ) A. b e. ( Base ` ( M |`s A ) ) A. c e. ( Base ` ( M |`s A ) ) ( a ( le ` ( M |`s A ) ) b -> ( a ( +g ` ( M |`s A ) ) c ) ( le ` ( M |`s A ) ) ( b ( +g ` ( M |`s A ) ) c ) ) ) )
56 1 18 52 55 syl3anbrc 
 |-  ( ( M e. oMnd /\ ( M |`s A ) e. Mnd ) -> ( M |`s A ) e. oMnd )