Step | Hyp | Ref
| Expression |
1 | | animorrl 981 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ 𝑎 = { 0 }) → (𝑎 = { 0 } ∨ 𝑎 = 𝐵)) |
2 | | drngring 19774 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
3 | 2 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ 𝑎 ≠ { 0 }) → 𝑅 ∈ Ring) |
4 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ 𝑎 ≠ { 0 }) → 𝑎 ∈ 𝑈) |
5 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ 𝑎 ≠ { 0 }) → 𝑎 ≠ { 0 }) |
6 | | drngnidl.u |
. . . . . . . . . . 11
⊢ 𝑈 = (LIdeal‘𝑅) |
7 | | drngnidl.z |
. . . . . . . . . . 11
⊢ 0 =
(0g‘𝑅) |
8 | 6, 7 | lidlnz 20266 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ 𝑈 ∧ 𝑎 ≠ { 0 }) → ∃𝑏 ∈ 𝑎 𝑏 ≠ 0 ) |
9 | 3, 4, 5, 8 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ 𝑎 ≠ { 0 }) → ∃𝑏 ∈ 𝑎 𝑏 ≠ 0 ) |
10 | | simpll 767 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ (𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 )) → 𝑅 ∈
DivRing) |
11 | | drngnidl.b |
. . . . . . . . . . . . . . . . 17
⊢ 𝐵 = (Base‘𝑅) |
12 | 11, 6 | lidlss 20248 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ 𝑈 → 𝑎 ⊆ 𝐵) |
13 | 12 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) → 𝑎 ⊆ 𝐵) |
14 | 13 | sselda 3901 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ 𝑏 ∈ 𝑎) → 𝑏 ∈ 𝐵) |
15 | 14 | adantrr 717 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ (𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 )) → 𝑏 ∈ 𝐵) |
16 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ (𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 )) → 𝑏 ≠ 0 ) |
17 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(.r‘𝑅) = (.r‘𝑅) |
18 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(1r‘𝑅) = (1r‘𝑅) |
19 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(invr‘𝑅) = (invr‘𝑅) |
20 | 11, 7, 17, 18, 19 | drnginvrl 19786 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ DivRing ∧ 𝑏 ∈ 𝐵 ∧ 𝑏 ≠ 0 ) →
(((invr‘𝑅)‘𝑏)(.r‘𝑅)𝑏) = (1r‘𝑅)) |
21 | 10, 15, 16, 20 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ (𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 )) →
(((invr‘𝑅)‘𝑏)(.r‘𝑅)𝑏) = (1r‘𝑅)) |
22 | 2 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ (𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 )) → 𝑅 ∈ Ring) |
23 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ (𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 )) → 𝑎 ∈ 𝑈) |
24 | 11, 7, 19 | drnginvrcl 19784 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ DivRing ∧ 𝑏 ∈ 𝐵 ∧ 𝑏 ≠ 0 ) →
((invr‘𝑅)‘𝑏) ∈ 𝐵) |
25 | 10, 15, 16, 24 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ (𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 )) →
((invr‘𝑅)‘𝑏) ∈ 𝐵) |
26 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ (𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 )) → 𝑏 ∈ 𝑎) |
27 | 6, 11, 17 | lidlmcl 20255 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ Ring ∧ 𝑎 ∈ 𝑈) ∧ (((invr‘𝑅)‘𝑏) ∈ 𝐵 ∧ 𝑏 ∈ 𝑎)) → (((invr‘𝑅)‘𝑏)(.r‘𝑅)𝑏) ∈ 𝑎) |
28 | 22, 23, 25, 26, 27 | syl22anc 839 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ (𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 )) →
(((invr‘𝑅)‘𝑏)(.r‘𝑅)𝑏) ∈ 𝑎) |
29 | 21, 28 | eqeltrrd 2839 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ (𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 )) →
(1r‘𝑅)
∈ 𝑎) |
30 | 29 | rexlimdvaa 3204 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) → (∃𝑏 ∈ 𝑎 𝑏 ≠ 0 →
(1r‘𝑅)
∈ 𝑎)) |
31 | 30 | imp 410 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ ∃𝑏 ∈ 𝑎 𝑏 ≠ 0 ) →
(1r‘𝑅)
∈ 𝑎) |
32 | 9, 31 | syldan 594 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ 𝑎 ≠ { 0 }) →
(1r‘𝑅)
∈ 𝑎) |
33 | 6, 11, 18 | lidl1el 20256 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ 𝑈) → ((1r‘𝑅) ∈ 𝑎 ↔ 𝑎 = 𝐵)) |
34 | 2, 33 | sylan 583 |
. . . . . . . . 9
⊢ ((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) → ((1r‘𝑅) ∈ 𝑎 ↔ 𝑎 = 𝐵)) |
35 | 34 | adantr 484 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ 𝑎 ≠ { 0 }) →
((1r‘𝑅)
∈ 𝑎 ↔ 𝑎 = 𝐵)) |
36 | 32, 35 | mpbid 235 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ 𝑎 ≠ { 0 }) → 𝑎 = 𝐵) |
37 | 36 | olcd 874 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) ∧ 𝑎 ≠ { 0 }) → (𝑎 = { 0 } ∨ 𝑎 = 𝐵)) |
38 | 1, 37 | pm2.61dane 3029 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) → (𝑎 = { 0 } ∨ 𝑎 = 𝐵)) |
39 | | vex 3412 |
. . . . . 6
⊢ 𝑎 ∈ V |
40 | 39 | elpr 4564 |
. . . . 5
⊢ (𝑎 ∈ {{ 0 }, 𝐵} ↔ (𝑎 = { 0 } ∨ 𝑎 = 𝐵)) |
41 | 38, 40 | sylibr 237 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈) → 𝑎 ∈ {{ 0 }, 𝐵}) |
42 | 41 | ex 416 |
. . 3
⊢ (𝑅 ∈ DivRing → (𝑎 ∈ 𝑈 → 𝑎 ∈ {{ 0 }, 𝐵})) |
43 | 42 | ssrdv 3907 |
. 2
⊢ (𝑅 ∈ DivRing → 𝑈 ⊆ {{ 0 }, 𝐵}) |
44 | 6, 7 | lidl0 20257 |
. . . 4
⊢ (𝑅 ∈ Ring → { 0 } ∈
𝑈) |
45 | 6, 11 | lidl1 20258 |
. . . 4
⊢ (𝑅 ∈ Ring → 𝐵 ∈ 𝑈) |
46 | 44, 45 | prssd 4735 |
. . 3
⊢ (𝑅 ∈ Ring → {{ 0 }, 𝐵} ⊆ 𝑈) |
47 | 2, 46 | syl 17 |
. 2
⊢ (𝑅 ∈ DivRing → {{ 0 }, 𝐵} ⊆ 𝑈) |
48 | 43, 47 | eqssd 3918 |
1
⊢ (𝑅 ∈ DivRing → 𝑈 = {{ 0 }, 𝐵}) |