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 oRing R 𝑠 A Ring R 𝑠 A oRing

Proof

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