| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ 𝑖 ≠ 𝐵) ∧ 𝑚 ∈ (MaxIdeal‘𝑅)) ∧ 𝑖 ⊆ 𝑚) → 𝑖 ⊆ 𝑚) | 
| 2 |  | simplr 768 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ 𝑖 ≠ 𝐵) ∧ 𝑚 ∈ (MaxIdeal‘𝑅)) ∧ 𝑖 ⊆ 𝑚) → 𝑚 ∈ (MaxIdeal‘𝑅)) | 
| 3 |  | drngmxidlr.u | . . . . . . . . . . . . 13
⊢ 𝑀 = (MaxIdeal‘𝑅) | 
| 4 | 2, 3 | eleqtrrdi 2851 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ 𝑖 ≠ 𝐵) ∧ 𝑚 ∈ (MaxIdeal‘𝑅)) ∧ 𝑖 ⊆ 𝑚) → 𝑚 ∈ 𝑀) | 
| 5 |  | drngmxidlr.2 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 = {{ 0 }}) | 
| 6 | 5 | ad4antr 732 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ 𝑖 ≠ 𝐵) ∧ 𝑚 ∈ (MaxIdeal‘𝑅)) ∧ 𝑖 ⊆ 𝑚) → 𝑀 = {{ 0 }}) | 
| 7 | 4, 6 | eleqtrd 2842 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ 𝑖 ≠ 𝐵) ∧ 𝑚 ∈ (MaxIdeal‘𝑅)) ∧ 𝑖 ⊆ 𝑚) → 𝑚 ∈ {{ 0 }}) | 
| 8 |  | elsni 4642 | . . . . . . . . . . 11
⊢ (𝑚 ∈ {{ 0 }} → 𝑚 = { 0 }) | 
| 9 | 7, 8 | syl 17 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ 𝑖 ≠ 𝐵) ∧ 𝑚 ∈ (MaxIdeal‘𝑅)) ∧ 𝑖 ⊆ 𝑚) → 𝑚 = { 0 }) | 
| 10 | 1, 9 | sseqtrd 4019 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ 𝑖 ≠ 𝐵) ∧ 𝑚 ∈ (MaxIdeal‘𝑅)) ∧ 𝑖 ⊆ 𝑚) → 𝑖 ⊆ { 0 }) | 
| 11 |  | drngmxidlr.r | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ NzRing) | 
| 12 |  | nzrring 20517 | . . . . . . . . . . . . 13
⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring) | 
| 13 | 11, 12 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 14 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) | 
| 15 |  | drngmxidlr.z | . . . . . . . . . . . . 13
⊢  0 =
(0g‘𝑅) | 
| 16 | 14, 15 | lidl0cl 21231 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅)) → 0 ∈ 𝑖) | 
| 17 | 13, 16 | sylan 580 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (LIdeal‘𝑅)) → 0 ∈ 𝑖) | 
| 18 | 17 | snssd 4808 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (LIdeal‘𝑅)) → { 0 } ⊆ 𝑖) | 
| 19 | 18 | ad3antrrr 730 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ 𝑖 ≠ 𝐵) ∧ 𝑚 ∈ (MaxIdeal‘𝑅)) ∧ 𝑖 ⊆ 𝑚) → { 0 } ⊆ 𝑖) | 
| 20 | 10, 19 | eqssd 4000 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ 𝑖 ≠ 𝐵) ∧ 𝑚 ∈ (MaxIdeal‘𝑅)) ∧ 𝑖 ⊆ 𝑚) → 𝑖 = { 0 }) | 
| 21 | 13 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ 𝑖 ≠ 𝐵) → 𝑅 ∈ Ring) | 
| 22 |  | simplr 768 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ 𝑖 ≠ 𝐵) → 𝑖 ∈ (LIdeal‘𝑅)) | 
| 23 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ 𝑖 ≠ 𝐵) → 𝑖 ≠ 𝐵) | 
| 24 |  | drngmxidlr.b | . . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑅) | 
| 25 | 24 | ssmxidl 33503 | . . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅) ∧ 𝑖 ≠ 𝐵) → ∃𝑚 ∈ (MaxIdeal‘𝑅)𝑖 ⊆ 𝑚) | 
| 26 | 21, 22, 23, 25 | syl3anc 1372 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ 𝑖 ≠ 𝐵) → ∃𝑚 ∈ (MaxIdeal‘𝑅)𝑖 ⊆ 𝑚) | 
| 27 | 20, 26 | r19.29a 3161 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ 𝑖 ≠ 𝐵) → 𝑖 = { 0 }) | 
| 28 |  | simpr 484 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ 𝑖 = 𝐵) → 𝑖 = 𝐵) | 
| 29 |  | exmidne 2949 | . . . . . . . . 9
⊢ (𝑖 = 𝐵 ∨ 𝑖 ≠ 𝐵) | 
| 30 | 29 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (LIdeal‘𝑅)) → (𝑖 = 𝐵 ∨ 𝑖 ≠ 𝐵)) | 
| 31 | 30 | orcomd 871 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (LIdeal‘𝑅)) → (𝑖 ≠ 𝐵 ∨ 𝑖 = 𝐵)) | 
| 32 | 27, 28, 31 | orim12da 32478 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (LIdeal‘𝑅)) → (𝑖 = { 0 } ∨ 𝑖 = 𝐵)) | 
| 33 |  | vex 3483 | . . . . . . 7
⊢ 𝑖 ∈ V | 
| 34 | 33 | elpr 4649 | . . . . . 6
⊢ (𝑖 ∈ {{ 0 }, 𝐵} ↔ (𝑖 = { 0 } ∨ 𝑖 = 𝐵)) | 
| 35 | 32, 34 | sylibr 234 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (LIdeal‘𝑅)) → 𝑖 ∈ {{ 0 }, 𝐵}) | 
| 36 | 35 | ex 412 | . . . 4
⊢ (𝜑 → (𝑖 ∈ (LIdeal‘𝑅) → 𝑖 ∈ {{ 0 }, 𝐵})) | 
| 37 | 36 | ssrdv 3988 | . . 3
⊢ (𝜑 → (LIdeal‘𝑅) ⊆ {{ 0 }, 𝐵}) | 
| 38 | 14, 15 | lidl0 21241 | . . . . 5
⊢ (𝑅 ∈ Ring → { 0 } ∈
(LIdeal‘𝑅)) | 
| 39 | 13, 38 | syl 17 | . . . 4
⊢ (𝜑 → { 0 } ∈
(LIdeal‘𝑅)) | 
| 40 | 14, 24 | lidl1 21244 | . . . . 5
⊢ (𝑅 ∈ Ring → 𝐵 ∈ (LIdeal‘𝑅)) | 
| 41 | 13, 40 | syl 17 | . . . 4
⊢ (𝜑 → 𝐵 ∈ (LIdeal‘𝑅)) | 
| 42 | 39, 41 | prssd 4821 | . . 3
⊢ (𝜑 → {{ 0 }, 𝐵} ⊆ (LIdeal‘𝑅)) | 
| 43 | 37, 42 | eqssd 4000 | . 2
⊢ (𝜑 → (LIdeal‘𝑅) = {{ 0 }, 𝐵}) | 
| 44 | 24, 15, 14 | drngidl 33462 | . . 3
⊢ (𝑅 ∈ NzRing → (𝑅 ∈ DivRing ↔
(LIdeal‘𝑅) = {{ 0 }, 𝐵})) | 
| 45 | 11, 44 | syl 17 | . 2
⊢ (𝜑 → (𝑅 ∈ DivRing ↔ (LIdeal‘𝑅) = {{ 0 }, 𝐵})) | 
| 46 | 43, 45 | mpbird 257 | 1
⊢ (𝜑 → 𝑅 ∈ DivRing) |