| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | subrdom.1 | . . . 4
⊢ (𝜑 → 𝑅 ∈ Domn) | 
| 2 |  | domnnzr 20706 | . . . 4
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) | 
| 3 | 1, 2 | syl 17 | . . 3
⊢ (𝜑 → 𝑅 ∈ NzRing) | 
| 4 |  | subrdom.2 | . . 3
⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) | 
| 5 |  | eqid 2737 | . . . 4
⊢ (𝑅 ↾s 𝑆) = (𝑅 ↾s 𝑆) | 
| 6 | 5 | subrgnzr 20594 | . . 3
⊢ ((𝑅 ∈ NzRing ∧ 𝑆 ∈ (SubRing‘𝑅)) → (𝑅 ↾s 𝑆) ∈ NzRing) | 
| 7 | 3, 4, 6 | syl2anc 584 | . 2
⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ NzRing) | 
| 8 | 1 | ad3antrrr 730 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ (𝑥(.r‘(𝑅 ↾s 𝑆))𝑦) = (0g‘(𝑅 ↾s 𝑆))) → 𝑅 ∈ Domn) | 
| 9 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 10 | 9 | subrgss 20572 | . . . . . . . . . 10
⊢ (𝑆 ∈ (SubRing‘𝑅) → 𝑆 ⊆ (Base‘𝑅)) | 
| 11 | 4, 10 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑅)) | 
| 12 | 11 | ad3antrrr 730 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ (𝑥(.r‘(𝑅 ↾s 𝑆))𝑦) = (0g‘(𝑅 ↾s 𝑆))) → 𝑆 ⊆ (Base‘𝑅)) | 
| 13 |  | simpllr 776 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ (𝑥(.r‘(𝑅 ↾s 𝑆))𝑦) = (0g‘(𝑅 ↾s 𝑆))) → 𝑥 ∈ (Base‘(𝑅 ↾s 𝑆))) | 
| 14 | 5, 9 | ressbas2 17283 | . . . . . . . . . . 11
⊢ (𝑆 ⊆ (Base‘𝑅) → 𝑆 = (Base‘(𝑅 ↾s 𝑆))) | 
| 15 | 11, 14 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝑆 = (Base‘(𝑅 ↾s 𝑆))) | 
| 16 | 15 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ (𝑥(.r‘(𝑅 ↾s 𝑆))𝑦) = (0g‘(𝑅 ↾s 𝑆))) → 𝑆 = (Base‘(𝑅 ↾s 𝑆))) | 
| 17 | 13, 16 | eleqtrrd 2844 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ (𝑥(.r‘(𝑅 ↾s 𝑆))𝑦) = (0g‘(𝑅 ↾s 𝑆))) → 𝑥 ∈ 𝑆) | 
| 18 | 12, 17 | sseldd 3984 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ (𝑥(.r‘(𝑅 ↾s 𝑆))𝑦) = (0g‘(𝑅 ↾s 𝑆))) → 𝑥 ∈ (Base‘𝑅)) | 
| 19 |  | simplr 769 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ (𝑥(.r‘(𝑅 ↾s 𝑆))𝑦) = (0g‘(𝑅 ↾s 𝑆))) → 𝑦 ∈ (Base‘(𝑅 ↾s 𝑆))) | 
| 20 | 19, 16 | eleqtrrd 2844 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ (𝑥(.r‘(𝑅 ↾s 𝑆))𝑦) = (0g‘(𝑅 ↾s 𝑆))) → 𝑦 ∈ 𝑆) | 
| 21 | 12, 20 | sseldd 3984 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ (𝑥(.r‘(𝑅 ↾s 𝑆))𝑦) = (0g‘(𝑅 ↾s 𝑆))) → 𝑦 ∈ (Base‘𝑅)) | 
| 22 |  | simpr 484 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ (𝑥(.r‘(𝑅 ↾s 𝑆))𝑦) = (0g‘(𝑅 ↾s 𝑆))) → (𝑥(.r‘(𝑅 ↾s 𝑆))𝑦) = (0g‘(𝑅 ↾s 𝑆))) | 
| 23 | 4 | elexd 3504 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ V) | 
| 24 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 25 | 5, 24 | ressmulr 17351 | . . . . . . . . . . 11
⊢ (𝑆 ∈ V →
(.r‘𝑅) =
(.r‘(𝑅
↾s 𝑆))) | 
| 26 | 23, 25 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (.r‘𝑅) = (.r‘(𝑅 ↾s 𝑆))) | 
| 27 | 26 | oveqd 7448 | . . . . . . . . 9
⊢ (𝜑 → (𝑥(.r‘𝑅)𝑦) = (𝑥(.r‘(𝑅 ↾s 𝑆))𝑦)) | 
| 28 | 27 | ad3antrrr 730 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ (𝑥(.r‘(𝑅 ↾s 𝑆))𝑦) = (0g‘(𝑅 ↾s 𝑆))) → (𝑥(.r‘𝑅)𝑦) = (𝑥(.r‘(𝑅 ↾s 𝑆))𝑦)) | 
| 29 |  | subrgrcl 20576 | . . . . . . . . . . 11
⊢ (𝑆 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring) | 
| 30 |  | ringmnd 20240 | . . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) | 
| 31 | 4, 29, 30 | 3syl 18 | . . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Mnd) | 
| 32 |  | subrgsubg 20577 | . . . . . . . . . . 11
⊢ (𝑆 ∈ (SubRing‘𝑅) → 𝑆 ∈ (SubGrp‘𝑅)) | 
| 33 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 34 | 33 | subg0cl 19152 | . . . . . . . . . . 11
⊢ (𝑆 ∈ (SubGrp‘𝑅) →
(0g‘𝑅)
∈ 𝑆) | 
| 35 | 4, 32, 34 | 3syl 18 | . . . . . . . . . 10
⊢ (𝜑 → (0g‘𝑅) ∈ 𝑆) | 
| 36 | 5, 9, 33 | ress0g 18775 | . . . . . . . . . 10
⊢ ((𝑅 ∈ Mnd ∧
(0g‘𝑅)
∈ 𝑆 ∧ 𝑆 ⊆ (Base‘𝑅)) →
(0g‘𝑅) =
(0g‘(𝑅
↾s 𝑆))) | 
| 37 | 31, 35, 11, 36 | syl3anc 1373 | . . . . . . . . 9
⊢ (𝜑 → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝑆))) | 
| 38 | 37 | ad3antrrr 730 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ (𝑥(.r‘(𝑅 ↾s 𝑆))𝑦) = (0g‘(𝑅 ↾s 𝑆))) → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝑆))) | 
| 39 | 22, 28, 38 | 3eqtr4d 2787 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ (𝑥(.r‘(𝑅 ↾s 𝑆))𝑦) = (0g‘(𝑅 ↾s 𝑆))) → (𝑥(.r‘𝑅)𝑦) = (0g‘𝑅)) | 
| 40 | 9, 24, 33 | domneq0 20708 | . . . . . . . 8
⊢ ((𝑅 ∈ Domn ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → ((𝑥(.r‘𝑅)𝑦) = (0g‘𝑅) ↔ (𝑥 = (0g‘𝑅) ∨ 𝑦 = (0g‘𝑅)))) | 
| 41 | 40 | biimpa 476 | . . . . . . 7
⊢ (((𝑅 ∈ Domn ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥(.r‘𝑅)𝑦) = (0g‘𝑅)) → (𝑥 = (0g‘𝑅) ∨ 𝑦 = (0g‘𝑅))) | 
| 42 | 8, 18, 21, 39, 41 | syl31anc 1375 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ (𝑥(.r‘(𝑅 ↾s 𝑆))𝑦) = (0g‘(𝑅 ↾s 𝑆))) → (𝑥 = (0g‘𝑅) ∨ 𝑦 = (0g‘𝑅))) | 
| 43 | 38 | eqeq2d 2748 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ (𝑥(.r‘(𝑅 ↾s 𝑆))𝑦) = (0g‘(𝑅 ↾s 𝑆))) → (𝑥 = (0g‘𝑅) ↔ 𝑥 = (0g‘(𝑅 ↾s 𝑆)))) | 
| 44 | 38 | eqeq2d 2748 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ (𝑥(.r‘(𝑅 ↾s 𝑆))𝑦) = (0g‘(𝑅 ↾s 𝑆))) → (𝑦 = (0g‘𝑅) ↔ 𝑦 = (0g‘(𝑅 ↾s 𝑆)))) | 
| 45 | 43, 44 | orbi12d 919 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ (𝑥(.r‘(𝑅 ↾s 𝑆))𝑦) = (0g‘(𝑅 ↾s 𝑆))) → ((𝑥 = (0g‘𝑅) ∨ 𝑦 = (0g‘𝑅)) ↔ (𝑥 = (0g‘(𝑅 ↾s 𝑆)) ∨ 𝑦 = (0g‘(𝑅 ↾s 𝑆))))) | 
| 46 | 42, 45 | mpbid 232 | . . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ (𝑥(.r‘(𝑅 ↾s 𝑆))𝑦) = (0g‘(𝑅 ↾s 𝑆))) → (𝑥 = (0g‘(𝑅 ↾s 𝑆)) ∨ 𝑦 = (0g‘(𝑅 ↾s 𝑆)))) | 
| 47 | 46 | ex 412 | . . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘(𝑅 ↾s 𝑆))) ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑆))) → ((𝑥(.r‘(𝑅 ↾s 𝑆))𝑦) = (0g‘(𝑅 ↾s 𝑆)) → (𝑥 = (0g‘(𝑅 ↾s 𝑆)) ∨ 𝑦 = (0g‘(𝑅 ↾s 𝑆))))) | 
| 48 | 47 | anasss 466 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(𝑅 ↾s 𝑆)) ∧ 𝑦 ∈ (Base‘(𝑅 ↾s 𝑆)))) → ((𝑥(.r‘(𝑅 ↾s 𝑆))𝑦) = (0g‘(𝑅 ↾s 𝑆)) → (𝑥 = (0g‘(𝑅 ↾s 𝑆)) ∨ 𝑦 = (0g‘(𝑅 ↾s 𝑆))))) | 
| 49 | 48 | ralrimivva 3202 | . 2
⊢ (𝜑 → ∀𝑥 ∈ (Base‘(𝑅 ↾s 𝑆))∀𝑦 ∈ (Base‘(𝑅 ↾s 𝑆))((𝑥(.r‘(𝑅 ↾s 𝑆))𝑦) = (0g‘(𝑅 ↾s 𝑆)) → (𝑥 = (0g‘(𝑅 ↾s 𝑆)) ∨ 𝑦 = (0g‘(𝑅 ↾s 𝑆))))) | 
| 50 |  | eqid 2737 | . . 3
⊢
(Base‘(𝑅
↾s 𝑆)) =
(Base‘(𝑅
↾s 𝑆)) | 
| 51 |  | eqid 2737 | . . 3
⊢
(.r‘(𝑅 ↾s 𝑆)) = (.r‘(𝑅 ↾s 𝑆)) | 
| 52 |  | eqid 2737 | . . 3
⊢
(0g‘(𝑅 ↾s 𝑆)) = (0g‘(𝑅 ↾s 𝑆)) | 
| 53 | 50, 51, 52 | isdomn 20705 | . 2
⊢ ((𝑅 ↾s 𝑆) ∈ Domn ↔ ((𝑅 ↾s 𝑆) ∈ NzRing ∧
∀𝑥 ∈
(Base‘(𝑅
↾s 𝑆))∀𝑦 ∈ (Base‘(𝑅 ↾s 𝑆))((𝑥(.r‘(𝑅 ↾s 𝑆))𝑦) = (0g‘(𝑅 ↾s 𝑆)) → (𝑥 = (0g‘(𝑅 ↾s 𝑆)) ∨ 𝑦 = (0g‘(𝑅 ↾s 𝑆)))))) | 
| 54 | 7, 49, 53 | sylanbrc 583 | 1
⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ Domn) |