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 ( ( 𝑀 ∈ oMnd ∧ ( 𝑀 ↾s 𝐴 ) ∈ Mnd ) → ( 𝑀 ↾s 𝐴 ) ∈ oMnd )

Proof

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