| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . 2
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) → (𝑅 ↾s 𝐴) ∈ Ring) | 
| 2 |  | ringgrp 20235 | . . . 4
⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp) | 
| 3 | 2 | adantl 481 | . . 3
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) → (𝑅 ↾s 𝐴) ∈ Grp) | 
| 4 |  | orngogrp 33331 | . . . . 5
⊢ (𝑅 ∈ oRing → 𝑅 ∈ oGrp) | 
| 5 |  | isogrp 33079 | . . . . . 6
⊢ (𝑅 ∈ oGrp ↔ (𝑅 ∈ Grp ∧ 𝑅 ∈ oMnd)) | 
| 6 | 5 | simprbi 496 | . . . . 5
⊢ (𝑅 ∈ oGrp → 𝑅 ∈ oMnd) | 
| 7 | 4, 6 | syl 17 | . . . 4
⊢ (𝑅 ∈ oRing → 𝑅 ∈ oMnd) | 
| 8 |  | ringmnd 20240 | . . . 4
⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Mnd) | 
| 9 |  | submomnd 33087 | . . . 4
⊢ ((𝑅 ∈ oMnd ∧ (𝑅 ↾s 𝐴) ∈ Mnd) → (𝑅 ↾s 𝐴) ∈ oMnd) | 
| 10 | 7, 8, 9 | syl2an 596 | . . 3
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) → (𝑅 ↾s 𝐴) ∈ oMnd) | 
| 11 |  | isogrp 33079 | . . 3
⊢ ((𝑅 ↾s 𝐴) ∈ oGrp ↔ ((𝑅 ↾s 𝐴) ∈ Grp ∧ (𝑅 ↾s 𝐴) ∈ oMnd)) | 
| 12 | 3, 10, 11 | sylanbrc 583 | . 2
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) → (𝑅 ↾s 𝐴) ∈ oGrp) | 
| 13 |  | simp-4l 783 | . . . . . . 7
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → 𝑅 ∈ oRing) | 
| 14 |  | reldmress 17276 | . . . . . . . . . . . . . . 15
⊢ Rel dom
↾s | 
| 15 | 14 | ovprc2 7471 | . . . . . . . . . . . . . 14
⊢ (¬
𝐴 ∈ V → (𝑅 ↾s 𝐴) = ∅) | 
| 16 | 15 | fveq2d 6910 | . . . . . . . . . . . . 13
⊢ (¬
𝐴 ∈ V →
(Base‘(𝑅
↾s 𝐴)) =
(Base‘∅)) | 
| 17 | 16 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ ¬ 𝐴 ∈ V) →
(Base‘(𝑅
↾s 𝐴)) =
(Base‘∅)) | 
| 18 |  | base0 17252 | . . . . . . . . . . . 12
⊢ ∅ =
(Base‘∅) | 
| 19 | 17, 18 | eqtr4di 2795 | . . . . . . . . . . 11
⊢ (((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ ¬ 𝐴 ∈ V) →
(Base‘(𝑅
↾s 𝐴)) =
∅) | 
| 20 |  | eqid 2737 | . . . . . . . . . . . . . . 15
⊢
(Base‘(𝑅
↾s 𝐴)) =
(Base‘(𝑅
↾s 𝐴)) | 
| 21 |  | eqid 2737 | . . . . . . . . . . . . . . 15
⊢
(1r‘(𝑅 ↾s 𝐴)) = (1r‘(𝑅 ↾s 𝐴)) | 
| 22 | 20, 21 | ringidcl 20262 | . . . . . . . . . . . . . 14
⊢ ((𝑅 ↾s 𝐴) ∈ Ring →
(1r‘(𝑅
↾s 𝐴))
∈ (Base‘(𝑅
↾s 𝐴))) | 
| 23 | 22 | ne0d 4342 | . . . . . . . . . . . . 13
⊢ ((𝑅 ↾s 𝐴) ∈ Ring →
(Base‘(𝑅
↾s 𝐴))
≠ ∅) | 
| 24 | 23 | ad2antlr 727 | . . . . . . . . . . . 12
⊢ (((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ ¬ 𝐴 ∈ V) →
(Base‘(𝑅
↾s 𝐴))
≠ ∅) | 
| 25 | 24 | neneqd 2945 | . . . . . . . . . . 11
⊢ (((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ ¬ 𝐴 ∈ V) → ¬
(Base‘(𝑅
↾s 𝐴)) =
∅) | 
| 26 | 19, 25 | condan 818 | . . . . . . . . . 10
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) → 𝐴 ∈ V) | 
| 27 |  | eqid 2737 | . . . . . . . . . . . 12
⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴) | 
| 28 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 29 | 27, 28 | ressbas 17280 | . . . . . . . . . . 11
⊢ (𝐴 ∈ V → (𝐴 ∩ (Base‘𝑅)) = (Base‘(𝑅 ↾s 𝐴))) | 
| 30 |  | inss2 4238 | . . . . . . . . . . 11
⊢ (𝐴 ∩ (Base‘𝑅)) ⊆ (Base‘𝑅) | 
| 31 | 29, 30 | eqsstrrdi 4029 | . . . . . . . . . 10
⊢ (𝐴 ∈ V →
(Base‘(𝑅
↾s 𝐴))
⊆ (Base‘𝑅)) | 
| 32 | 26, 31 | syl 17 | . . . . . . . . 9
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) →
(Base‘(𝑅
↾s 𝐴))
⊆ (Base‘𝑅)) | 
| 33 | 32 | ad3antrrr 730 | . . . . . . . 8
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → (Base‘(𝑅 ↾s 𝐴)) ⊆ (Base‘𝑅)) | 
| 34 |  | simpllr 776 | . . . . . . . 8
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → 𝑎 ∈ (Base‘(𝑅 ↾s 𝐴))) | 
| 35 | 33, 34 | sseldd 3984 | . . . . . . 7
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → 𝑎 ∈ (Base‘𝑅)) | 
| 36 |  | simprl 771 | . . . . . . . 8
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎) | 
| 37 |  | orngring 33330 | . . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ oRing → 𝑅 ∈ Ring) | 
| 38 |  | ringgrp 20235 | . . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) | 
| 39 | 37, 38 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ oRing → 𝑅 ∈ Grp) | 
| 40 | 39 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) → 𝑅 ∈ Grp) | 
| 41 | 28 | ressinbas 17291 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ V → (𝑅 ↾s 𝐴) = (𝑅 ↾s (𝐴 ∩ (Base‘𝑅)))) | 
| 42 | 29 | oveq2d 7447 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ V → (𝑅 ↾s (𝐴 ∩ (Base‘𝑅))) = (𝑅 ↾s (Base‘(𝑅 ↾s 𝐴)))) | 
| 43 | 41, 42 | eqtrd 2777 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ V → (𝑅 ↾s 𝐴) = (𝑅 ↾s (Base‘(𝑅 ↾s 𝐴)))) | 
| 44 | 26, 43 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) → (𝑅 ↾s 𝐴) = (𝑅 ↾s (Base‘(𝑅 ↾s 𝐴)))) | 
| 45 | 44, 3 | eqeltrrd 2842 | . . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) → (𝑅 ↾s
(Base‘(𝑅
↾s 𝐴)))
∈ Grp) | 
| 46 | 28 | issubg 19144 | . . . . . . . . . . . . . 14
⊢
((Base‘(𝑅
↾s 𝐴))
∈ (SubGrp‘𝑅)
↔ (𝑅 ∈ Grp ∧
(Base‘(𝑅
↾s 𝐴))
⊆ (Base‘𝑅)
∧ (𝑅
↾s (Base‘(𝑅 ↾s 𝐴))) ∈ Grp)) | 
| 47 | 40, 32, 45, 46 | syl3anbrc 1344 | . . . . . . . . . . . . 13
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) →
(Base‘(𝑅
↾s 𝐴))
∈ (SubGrp‘𝑅)) | 
| 48 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢ (𝑅 ↾s
(Base‘(𝑅
↾s 𝐴))) =
(𝑅 ↾s
(Base‘(𝑅
↾s 𝐴))) | 
| 49 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 50 | 48, 49 | subg0 19150 | . . . . . . . . . . . . 13
⊢
((Base‘(𝑅
↾s 𝐴))
∈ (SubGrp‘𝑅)
→ (0g‘𝑅) = (0g‘(𝑅 ↾s (Base‘(𝑅 ↾s 𝐴))))) | 
| 51 | 47, 50 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) →
(0g‘𝑅) =
(0g‘(𝑅
↾s (Base‘(𝑅 ↾s 𝐴))))) | 
| 52 | 44 | fveq2d 6910 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) →
(0g‘(𝑅
↾s 𝐴)) =
(0g‘(𝑅
↾s (Base‘(𝑅 ↾s 𝐴))))) | 
| 53 | 51, 52 | eqtr4d 2780 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) →
(0g‘𝑅) =
(0g‘(𝑅
↾s 𝐴))) | 
| 54 | 53 | ad2antrr 726 | . . . . . . . . . 10
⊢ ((((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ 𝑎 ∈ (Base‘(𝑅 ↾s 𝐴))) ∧ 𝑏 ∈ (Base‘(𝑅 ↾s 𝐴))) → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝐴))) | 
| 55 | 26 | ad2antrr 726 | . . . . . . . . . . 11
⊢ ((((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ 𝑎 ∈ (Base‘(𝑅 ↾s 𝐴))) ∧ 𝑏 ∈ (Base‘(𝑅 ↾s 𝐴))) → 𝐴 ∈ V) | 
| 56 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(le‘𝑅) =
(le‘𝑅) | 
| 57 | 27, 56 | ressle 17424 | . . . . . . . . . . 11
⊢ (𝐴 ∈ V → (le‘𝑅) = (le‘(𝑅 ↾s 𝐴))) | 
| 58 | 55, 57 | syl 17 | . . . . . . . . . 10
⊢ ((((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ 𝑎 ∈ (Base‘(𝑅 ↾s 𝐴))) ∧ 𝑏 ∈ (Base‘(𝑅 ↾s 𝐴))) → (le‘𝑅) = (le‘(𝑅 ↾s 𝐴))) | 
| 59 |  | eqidd 2738 | . . . . . . . . . 10
⊢ ((((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ 𝑎 ∈ (Base‘(𝑅 ↾s 𝐴))) ∧ 𝑏 ∈ (Base‘(𝑅 ↾s 𝐴))) → 𝑎 = 𝑎) | 
| 60 | 54, 58, 59 | breq123d 5157 | . . . . . . . . 9
⊢ ((((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ 𝑎 ∈ (Base‘(𝑅 ↾s 𝐴))) ∧ 𝑏 ∈ (Base‘(𝑅 ↾s 𝐴))) → ((0g‘𝑅)(le‘𝑅)𝑎 ↔ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎)) | 
| 61 | 60 | adantr 480 | . . . . . . . 8
⊢
(((((𝑅 ∈ 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 257 | . . . . . . 7
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → (0g‘𝑅)(le‘𝑅)𝑎) | 
| 63 |  | simplr 769 | . . . . . . . 8
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → 𝑏 ∈ (Base‘(𝑅 ↾s 𝐴))) | 
| 64 | 33, 63 | sseldd 3984 | . . . . . . 7
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → 𝑏 ∈ (Base‘𝑅)) | 
| 65 |  | simprr 773 | . . . . . . . 8
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏) | 
| 66 |  | eqidd 2738 | . . . . . . . . . 10
⊢ ((((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ 𝑎 ∈ (Base‘(𝑅 ↾s 𝐴))) ∧ 𝑏 ∈ (Base‘(𝑅 ↾s 𝐴))) → 𝑏 = 𝑏) | 
| 67 | 54, 58, 66 | breq123d 5157 | . . . . . . . . 9
⊢ ((((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ 𝑎 ∈ (Base‘(𝑅 ↾s 𝐴))) ∧ 𝑏 ∈ (Base‘(𝑅 ↾s 𝐴))) → ((0g‘𝑅)(le‘𝑅)𝑏 ↔ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) | 
| 68 | 67 | adantr 480 | . . . . . . . 8
⊢
(((((𝑅 ∈ 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 257 | . . . . . . 7
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → (0g‘𝑅)(le‘𝑅)𝑏) | 
| 70 |  | eqid 2737 | . . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 71 | 28, 56, 49, 70 | orngmul 33333 | . . . . . . 7
⊢ ((𝑅 ∈ oRing ∧ (𝑎 ∈ (Base‘𝑅) ∧
(0g‘𝑅)(le‘𝑅)𝑎) ∧ (𝑏 ∈ (Base‘𝑅) ∧ (0g‘𝑅)(le‘𝑅)𝑏)) → (0g‘𝑅)(le‘𝑅)(𝑎(.r‘𝑅)𝑏)) | 
| 72 | 13, 35, 62, 64, 69, 71 | syl122anc 1381 | . . . . . 6
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → (0g‘𝑅)(le‘𝑅)(𝑎(.r‘𝑅)𝑏)) | 
| 73 | 54 | adantr 480 | . . . . . . 7
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝐴))) | 
| 74 | 58 | adantr 480 | . . . . . . 7
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → (le‘𝑅) = (le‘(𝑅 ↾s 𝐴))) | 
| 75 | 55 | adantr 480 | . . . . . . . . 9
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → 𝐴 ∈ V) | 
| 76 | 27, 70 | ressmulr 17351 | . . . . . . . . 9
⊢ (𝐴 ∈ V →
(.r‘𝑅) =
(.r‘(𝑅
↾s 𝐴))) | 
| 77 | 75, 76 | syl 17 | . . . . . . . 8
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → (.r‘𝑅) = (.r‘(𝑅 ↾s 𝐴))) | 
| 78 | 77 | oveqd 7448 | . . . . . . 7
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → (𝑎(.r‘𝑅)𝑏) = (𝑎(.r‘(𝑅 ↾s 𝐴))𝑏)) | 
| 79 | 73, 74, 78 | breq123d 5157 | . . . . . 6
⊢
(((((𝑅 ∈ 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 232 | . . . . 5
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))(𝑎(.r‘(𝑅 ↾s 𝐴))𝑏)) | 
| 81 | 80 | ex 412 | . . . 4
⊢ ((((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ 𝑎 ∈ (Base‘(𝑅 ↾s 𝐴))) ∧ 𝑏 ∈ (Base‘(𝑅 ↾s 𝐴))) → (((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏) → (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))(𝑎(.r‘(𝑅 ↾s 𝐴))𝑏))) | 
| 82 | 81 | anasss 466 | . . 3
⊢ (((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝑎 ∈ (Base‘(𝑅 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑅 ↾s 𝐴)))) → (((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏) → (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))(𝑎(.r‘(𝑅 ↾s 𝐴))𝑏))) | 
| 83 | 82 | ralrimivva 3202 | . 2
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) →
∀𝑎 ∈
(Base‘(𝑅
↾s 𝐴))∀𝑏 ∈ (Base‘(𝑅 ↾s 𝐴))(((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏) → (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))(𝑎(.r‘(𝑅 ↾s 𝐴))𝑏))) | 
| 84 |  | eqid 2737 | . . 3
⊢
(0g‘(𝑅 ↾s 𝐴)) = (0g‘(𝑅 ↾s 𝐴)) | 
| 85 |  | eqid 2737 | . . 3
⊢
(.r‘(𝑅 ↾s 𝐴)) = (.r‘(𝑅 ↾s 𝐴)) | 
| 86 |  | eqid 2737 | . . 3
⊢
(le‘(𝑅
↾s 𝐴)) =
(le‘(𝑅
↾s 𝐴)) | 
| 87 | 20, 84, 85, 86 | isorng 33329 | . 2
⊢ ((𝑅 ↾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 1344 | 1
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) → (𝑅 ↾s 𝐴) ∈ oRing) |