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 )