| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | animorrl 982 | . . . . . 6
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ 𝑎 = { 0 }) → (𝑎 = { 0 } ∨ 𝑎 = 𝐵)) | 
| 2 |  | drngring 20737 | . . . . . . . . . . 11
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) | 
| 3 | 2 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ 𝑎 ≠ { 0 }) → 𝑅 ∈ Ring) | 
| 4 |  | simplr 768 | . . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ 𝑎 ≠ { 0 }) → 𝑎 ∈ 𝑈) | 
| 5 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ 𝑎 ≠ { 0 }) → 𝑎 ≠ { 0 }) | 
| 6 |  | drngnidl.u | . . . . . . . . . . 11
⊢ 𝑈 = (LIdeal‘𝑅) | 
| 7 |  | drngnidl.z | . . . . . . . . . . 11
⊢  0 =
(0g‘𝑅) | 
| 8 | 6, 7 | lidlnz 21253 | . . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ 𝑈 ∧ 𝑎 ≠ { 0 }) → ∃𝑏 ∈ 𝑎 𝑏 ≠ 0 ) | 
| 9 | 3, 4, 5, 8 | syl3anc 1372 | . . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ 𝑎 ≠ { 0 }) → ∃𝑏 ∈ 𝑎 𝑏 ≠ 0 ) | 
| 10 |  | simpll 766 | . . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ (𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 )) → 𝑅 ∈
DivRing) | 
| 11 |  | drngnidl.b | . . . . . . . . . . . . . . . . 17
⊢ 𝐵 = (Base‘𝑅) | 
| 12 | 11, 6 | lidlss 21223 | . . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ 𝑈 → 𝑎 ⊆ 𝐵) | 
| 13 | 12 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) → 𝑎 ⊆ 𝐵) | 
| 14 | 13 | sselda 3982 | . . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ 𝑏 ∈ 𝑎) → 𝑏 ∈ 𝐵) | 
| 15 | 14 | adantrr 717 | . . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ (𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 )) → 𝑏 ∈ 𝐵) | 
| 16 |  | simprr 772 | . . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ (𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 )) → 𝑏 ≠ 0 ) | 
| 17 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 18 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 19 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(invr‘𝑅) = (invr‘𝑅) | 
| 20 | 11, 7, 17, 18, 19 | drnginvrl 20757 | . . . . . . . . . . . . 13
⊢ ((𝑅 ∈ DivRing ∧ 𝑏 ∈ 𝐵 ∧ 𝑏 ≠ 0 ) →
(((invr‘𝑅)‘𝑏)(.r‘𝑅)𝑏) = (1r‘𝑅)) | 
| 21 | 10, 15, 16, 20 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ (𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 )) →
(((invr‘𝑅)‘𝑏)(.r‘𝑅)𝑏) = (1r‘𝑅)) | 
| 22 | 2 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ (𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 )) → 𝑅 ∈ Ring) | 
| 23 |  | simplr 768 | . . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ (𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 )) → 𝑎 ∈ 𝑈) | 
| 24 | 11, 7, 19 | drnginvrcl 20754 | . . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ DivRing ∧ 𝑏 ∈ 𝐵 ∧ 𝑏 ≠ 0 ) →
((invr‘𝑅)‘𝑏) ∈ 𝐵) | 
| 25 | 10, 15, 16, 24 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ (𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 )) →
((invr‘𝑅)‘𝑏) ∈ 𝐵) | 
| 26 |  | simprl 770 | . . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ (𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 )) → 𝑏 ∈ 𝑎) | 
| 27 | 6, 11, 17 | lidlmcl 21236 | . . . . . . . . . . . . 13
⊢ (((𝑅 ∈ Ring ∧ 𝑎 ∈ 𝑈) ∧ (((invr‘𝑅)‘𝑏) ∈ 𝐵 ∧ 𝑏 ∈ 𝑎)) → (((invr‘𝑅)‘𝑏)(.r‘𝑅)𝑏) ∈ 𝑎) | 
| 28 | 22, 23, 25, 26, 27 | syl22anc 838 | . . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ (𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 )) →
(((invr‘𝑅)‘𝑏)(.r‘𝑅)𝑏) ∈ 𝑎) | 
| 29 | 21, 28 | eqeltrrd 2841 | . . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ (𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 )) →
(1r‘𝑅)
∈ 𝑎) | 
| 30 | 29 | rexlimdvaa 3155 | . . . . . . . . . 10
⊢ ((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) → (∃𝑏 ∈ 𝑎 𝑏 ≠ 0 →
(1r‘𝑅)
∈ 𝑎)) | 
| 31 | 30 | imp 406 | . . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ ∃𝑏 ∈ 𝑎 𝑏 ≠ 0 ) →
(1r‘𝑅)
∈ 𝑎) | 
| 32 | 9, 31 | syldan 591 | . . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ 𝑎 ≠ { 0 }) →
(1r‘𝑅)
∈ 𝑎) | 
| 33 | 6, 11, 18 | lidl1el 21237 | . . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ 𝑈) → ((1r‘𝑅) ∈ 𝑎 ↔ 𝑎 = 𝐵)) | 
| 34 | 2, 33 | sylan 580 | . . . . . . . . 9
⊢ ((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) → ((1r‘𝑅) ∈ 𝑎 ↔ 𝑎 = 𝐵)) | 
| 35 | 34 | adantr 480 | . . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ 𝑎 ≠ { 0 }) →
((1r‘𝑅)
∈ 𝑎 ↔ 𝑎 = 𝐵)) | 
| 36 | 32, 35 | mpbid 232 | . . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ 𝑎 ≠ { 0 }) → 𝑎 = 𝐵) | 
| 37 | 36 | olcd 874 | . . . . . 6
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ 𝑎 ≠ { 0 }) → (𝑎 = { 0 } ∨ 𝑎 = 𝐵)) | 
| 38 | 1, 37 | pm2.61dane 3028 | . . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) → (𝑎 = { 0 } ∨ 𝑎 = 𝐵)) | 
| 39 |  | vex 3483 | . . . . . 6
⊢ 𝑎 ∈ V | 
| 40 | 39 | elpr 4649 | . . . . 5
⊢ (𝑎 ∈ {{ 0 }, 𝐵} ↔ (𝑎 = { 0 } ∨ 𝑎 = 𝐵)) | 
| 41 | 38, 40 | sylibr 234 | . . . 4
⊢ ((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) → 𝑎 ∈ {{ 0 }, 𝐵}) | 
| 42 | 41 | ex 412 | . . 3
⊢ (𝑅 ∈ DivRing → (𝑎 ∈ 𝑈 → 𝑎 ∈ {{ 0 }, 𝐵})) | 
| 43 | 42 | ssrdv 3988 | . 2
⊢ (𝑅 ∈ DivRing → 𝑈 ⊆ {{ 0 }, 𝐵}) | 
| 44 | 6, 7 | lidl0 21241 | . . . 4
⊢ (𝑅 ∈ Ring → { 0 } ∈
𝑈) | 
| 45 | 6, 11 | lidl1 21244 | . . . 4
⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑈) | 
| 46 | 44, 45 | prssd 4821 | . . 3
⊢ (𝑅 ∈ Ring → {{ 0 }, 𝐵} ⊆ 𝑈) | 
| 47 | 2, 46 | syl 17 | . 2
⊢ (𝑅 ∈ DivRing → {{ 0 }, 𝐵} ⊆ 𝑈) | 
| 48 | 43, 47 | eqssd 4000 | 1
⊢ (𝑅 ∈ DivRing → 𝑈 = {{ 0 }, 𝐵}) |