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 ( ( 𝑅 ∈ oRing ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) → ( 𝑅 ↾s 𝐴 ) ∈ oRing )

Proof

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