Metamath Proof Explorer

Theorem suborng

Description: Every subring of an ordered ring is also an ordered ring. (Contributed by Thierry Arnoux, 21-Jan-2018)

Ref Expression
Assertion suborng 
|- ( ( R e. oRing /\ ( R |`s A ) e. Ring ) -> ( R |`s A ) e. oRing )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( R e. oRing /\ ( R |`s A ) e. Ring ) -> ( R |`s A ) e. Ring )
2 ringgrp 
 |-  ( ( R |`s A ) e. Ring -> ( R |`s A ) e. Grp )
3 2 adantl 
 |-  ( ( R e. oRing /\ ( R |`s A ) e. Ring ) -> ( R |`s A ) e. Grp )
4 orngogrp 
 |-  ( R e. oRing -> R e. oGrp )
5 isogrp 
 |-  ( R e. oGrp <-> ( R e. Grp /\ R e. oMnd ) )
6 5 simprbi 
 |-  ( R e. oGrp -> R e. oMnd )
7 4 6 syl 
 |-  ( R e. oRing -> R e. oMnd )
8 ringmnd 
 |-  ( ( R |`s A ) e. Ring -> ( R |`s A ) e. Mnd )
9 submomnd 
 |-  ( ( R e. oMnd /\ ( R |`s A ) e. Mnd ) -> ( R |`s A ) e. oMnd )
10 7 8 9 syl2an 
 |-  ( ( R e. oRing /\ ( R |`s A ) e. Ring ) -> ( R |`s A ) e. oMnd )
11 isogrp 
 |-  ( ( R |`s A ) e. oGrp <-> ( ( R |`s A ) e. Grp /\ ( R |`s A ) e. oMnd ) )
12 3 10 11 sylanbrc 
 |-  ( ( R e. oRing /\ ( R |`s A ) e. Ring ) -> ( R |`s A ) e. oGrp )
13 simp-4l 
 |-  ( ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) /\ ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) ) -> R e. oRing )
14 reldmress 
 |-  Rel dom |`s
15 14 ovprc2 
 |-  ( -. A e. _V -> ( R |`s A ) = (/) )
16 15 fveq2d 
 |-  ( -. A e. _V -> ( Base ` ( R |`s A ) ) = ( Base ` (/) ) )
17 16 adantl 
 |-  ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ -. A e. _V ) -> ( Base ` ( R |`s A ) ) = ( Base ` (/) ) )
18 base0 
 |-  (/) = ( Base ` (/) )
19 17 18 eqtr4di 
 |-  ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ -. A e. _V ) -> ( Base ` ( R |`s A ) ) = (/) )
20 eqid 
 |-  ( Base ` ( R |`s A ) ) = ( Base ` ( R |`s A ) )
21 eqid 
 |-  ( 1r ` ( R |`s A ) ) = ( 1r ` ( R |`s A ) )
22 20 21 ringidcl 
 |-  ( ( R |`s A ) e. Ring -> ( 1r ` ( R |`s A ) ) e. ( Base ` ( R |`s A ) ) )
23 22 ne0d 
 |-  ( ( R |`s A ) e. Ring -> ( Base ` ( R |`s A ) ) =/= (/) )
24 23 ad2antlr 
 |-  ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ -. A e. _V ) -> ( Base ` ( R |`s A ) ) =/= (/) )
25 24 neneqd 
 |-  ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ -. A e. _V ) -> -. ( Base ` ( R |`s A ) ) = (/) )
26 19 25 condan 
 |-  ( ( R e. oRing /\ ( R |`s A ) e. Ring ) -> A e. _V )
27 eqid 
 |-  ( R |`s A ) = ( R |`s A )
28 eqid 
 |-  ( Base ` R ) = ( Base ` R )
29 27 28 ressbas 
 |-  ( A e. _V -> ( A i^i ( Base ` R ) ) = ( Base ` ( R |`s A ) ) )
30 inss2 
 |-  ( A i^i ( Base ` R ) ) C_ ( Base ` R )
31 29 30 eqsstrrdi 
 |-  ( A e. _V -> ( Base ` ( R |`s A ) ) C_ ( Base ` R ) )
32 26 31 syl 
 |-  ( ( R e. oRing /\ ( R |`s A ) e. Ring ) -> ( Base ` ( R |`s A ) ) C_ ( Base ` R ) )
33 32 ad3antrrr 
 |-  ( ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) /\ ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) ) -> ( Base ` ( R |`s A ) ) C_ ( Base ` R ) )
34 simpllr 
 |-  ( ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) /\ ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) ) -> a e. ( Base ` ( R |`s A ) ) )
35 33 34 sseldd 
 |-  ( ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) /\ ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) ) -> a e. ( Base ` R ) )
36 simprl 
 |-  ( ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) /\ ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) ) -> ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a )
37 orngring 
 |-  ( R e. oRing -> R e. Ring )
38 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
39 37 38 syl 
 |-  ( R e. oRing -> R e. Grp )
40 39 adantr 
 |-  ( ( R e. oRing /\ ( R |`s A ) e. Ring ) -> R e. Grp )
41 28 ressinbas 
 |-  ( A e. _V -> ( R |`s A ) = ( R |`s ( A i^i ( Base ` R ) ) ) )
42 29 oveq2d 
 |-  ( A e. _V -> ( R |`s ( A i^i ( Base ` R ) ) ) = ( R |`s ( Base ` ( R |`s A ) ) ) )
43 41 42 eqtrd 
 |-  ( A e. _V -> ( R |`s A ) = ( R |`s ( Base ` ( R |`s A ) ) ) )
44 26 43 syl 
 |-  ( ( R e. oRing /\ ( R |`s A ) e. Ring ) -> ( R |`s A ) = ( R |`s ( Base ` ( R |`s A ) ) ) )
45 44 3 eqeltrrd 
 |-  ( ( R e. oRing /\ ( R |`s A ) e. Ring ) -> ( R |`s ( Base ` ( R |`s A ) ) ) e. Grp )
46 28 issubg 
 |-  ( ( Base ` ( R |`s A ) ) e. ( SubGrp ` R ) <-> ( R e. Grp /\ ( Base ` ( R |`s A ) ) C_ ( Base ` R ) /\ ( R |`s ( Base ` ( R |`s A ) ) ) e. Grp ) )
47 40 32 45 46 syl3anbrc 
 |-  ( ( R e. oRing /\ ( R |`s A ) e. Ring ) -> ( Base ` ( R |`s A ) ) e. ( SubGrp ` R ) )
48 eqid 
 |-  ( R |`s ( Base ` ( R |`s A ) ) ) = ( R |`s ( Base ` ( R |`s A ) ) )
49 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
50 48 49 subg0 
 |-  ( ( Base ` ( R |`s A ) ) e. ( SubGrp ` R ) -> ( 0g ` R ) = ( 0g ` ( R |`s ( Base ` ( R |`s A ) ) ) ) )
51 47 50 syl 
 |-  ( ( R e. oRing /\ ( R |`s A ) e. Ring ) -> ( 0g ` R ) = ( 0g ` ( R |`s ( Base ` ( R |`s A ) ) ) ) )
52 44 fveq2d 
 |-  ( ( R e. oRing /\ ( R |`s A ) e. Ring ) -> ( 0g ` ( R |`s A ) ) = ( 0g ` ( R |`s ( Base ` ( R |`s A ) ) ) ) )
53 51 52 eqtr4d 
 |-  ( ( R e. oRing /\ ( R |`s A ) e. Ring ) -> ( 0g ` R ) = ( 0g ` ( R |`s A ) ) )
54 53 ad2antrr 
 |-  ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) -> ( 0g ` R ) = ( 0g ` ( R |`s A ) ) )
55 26 ad2antrr 
 |-  ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) -> A e. _V )
56 eqid 
 |-  ( le ` R ) = ( le ` R )
57 27 56 ressle 
 |-  ( A e. _V -> ( le ` R ) = ( le ` ( R |`s A ) ) )
58 55 57 syl 
 |-  ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) -> ( le ` R ) = ( le ` ( R |`s A ) ) )
59 eqidd 
 |-  ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) -> a = a )
60 54 58 59 breq123d 
 |-  ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) -> ( ( 0g ` R ) ( le ` R ) a <-> ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a ) )
61 60 adantr 
 |-  ( ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) /\ ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) ) -> ( ( 0g ` R ) ( le ` R ) a <-> ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a ) )
62 36 61 mpbird 
 |-  ( ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) /\ ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) ) -> ( 0g ` R ) ( le ` R ) a )
63 simplr 
 |-  ( ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) /\ ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) ) -> b e. ( Base ` ( R |`s A ) ) )
64 33 63 sseldd 
 |-  ( ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) /\ ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) ) -> b e. ( Base ` R ) )
65 simprr 
 |-  ( ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) /\ ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) ) -> ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b )
66 eqidd 
 |-  ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) -> b = b )
67 54 58 66 breq123d 
 |-  ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) -> ( ( 0g ` R ) ( le ` R ) b <-> ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) )
68 67 adantr 
 |-  ( ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) /\ ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) ) -> ( ( 0g ` R ) ( le ` R ) b <-> ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) )
69 65 68 mpbird 
 |-  ( ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) /\ ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) ) -> ( 0g ` R ) ( le ` R ) b )
70 eqid 
 |-  ( .r ` R ) = ( .r ` R )
71 28 56 49 70 orngmul 
 |-  ( ( R e. oRing /\ ( a e. ( Base ` R ) /\ ( 0g ` R ) ( le ` R ) a ) /\ ( b e. ( Base ` R ) /\ ( 0g ` R ) ( le ` R ) b ) ) -> ( 0g ` R ) ( le ` R ) ( a ( .r ` R ) b ) )
72 13 35 62 64 69 71 syl122anc 
 |-  ( ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) /\ ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) ) -> ( 0g ` R ) ( le ` R ) ( a ( .r ` R ) b ) )
73 54 adantr 
 |-  ( ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) /\ ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) ) -> ( 0g ` R ) = ( 0g ` ( R |`s A ) ) )
74 58 adantr 
 |-  ( ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) /\ ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) ) -> ( le ` R ) = ( le ` ( R |`s A ) ) )
75 55 adantr 
 |-  ( ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) /\ ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) ) -> A e. _V )
76 27 70 ressmulr 
 |-  ( A e. _V -> ( .r ` R ) = ( .r ` ( R |`s A ) ) )
77 75 76 syl 
 |-  ( ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) /\ ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) ) -> ( .r ` R ) = ( .r ` ( R |`s A ) ) )
78 77 oveqd 
 |-  ( ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) /\ ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) ) -> ( a ( .r ` R ) b ) = ( a ( .r ` ( R |`s A ) ) b ) )
79 73 74 78 breq123d 
 |-  ( ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) /\ ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) ) -> ( ( 0g ` R ) ( le ` R ) ( a ( .r ` R ) b ) <-> ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) ( a ( .r ` ( R |`s A ) ) b ) ) )
80 72 79 mpbid 
 |-  ( ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) /\ ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) ) -> ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) ( a ( .r ` ( R |`s A ) ) b ) )
81 80 ex 
 |-  ( ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ a e. ( Base ` ( R |`s A ) ) ) /\ b e. ( Base ` ( R |`s A ) ) ) -> ( ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) -> ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) ( a ( .r ` ( R |`s A ) ) b ) ) )
82 81 anasss 
 |-  ( ( ( R e. oRing /\ ( R |`s A ) e. Ring ) /\ ( a e. ( Base ` ( R |`s A ) ) /\ b e. ( Base ` ( R |`s A ) ) ) ) -> ( ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) -> ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) ( a ( .r ` ( R |`s A ) ) b ) ) )
83 82 ralrimivva 
 |-  ( ( R e. oRing /\ ( R |`s A ) e. Ring ) -> A. a e. ( Base ` ( R |`s A ) ) A. b e. ( Base ` ( R |`s A ) ) ( ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) -> ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) ( a ( .r ` ( R |`s A ) ) b ) ) )
84 eqid 
 |-  ( 0g ` ( R |`s A ) ) = ( 0g ` ( R |`s A ) )
85 eqid 
 |-  ( .r ` ( R |`s A ) ) = ( .r ` ( R |`s A ) )
86 eqid 
 |-  ( le ` ( R |`s A ) ) = ( le ` ( R |`s A ) )
87 20 84 85 86 isorng 
 |-  ( ( R |`s A ) e. oRing <-> ( ( R |`s A ) e. Ring /\ ( R |`s A ) e. oGrp /\ A. a e. ( Base ` ( R |`s A ) ) A. b e. ( Base ` ( R |`s A ) ) ( ( ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) a /\ ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) b ) -> ( 0g ` ( R |`s A ) ) ( le ` ( R |`s A ) ) ( a ( .r ` ( R |`s A ) ) b ) ) ) )
88 1 12 83 87 syl3anbrc 
 |-  ( ( R e. oRing /\ ( R |`s A ) e. Ring ) -> ( R |`s A ) e. oRing )