Step | Hyp | Ref
| Expression |
1 | | df-3an 1087 |
. . . 4
⊢ (({ 0 } ∈
(LIdeal‘𝑅) ∧ {
0 } ≠
(Base‘𝑅) ∧
∀𝑥 ∈
(Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) ∈ { 0 } → (𝑥 ∈ { 0 } ∨ 𝑦 ∈ { 0 }))) ↔ (({ 0 } ∈
(LIdeal‘𝑅) ∧ {
0 } ≠
(Base‘𝑅)) ∧
∀𝑥 ∈
(Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) ∈ { 0 } → (𝑥 ∈ { 0 } ∨ 𝑦 ∈ { 0 })))) |
2 | | crngring 19362 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
3 | 2 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ { 0 } ∈
(LIdeal‘𝑅)) ∧
¬ 𝑅 ∈ NzRing)
→ 𝑅 ∈
Ring) |
4 | | 0ringnnzr 20095 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Ring →
((♯‘(Base‘𝑅)) = 1 ↔ ¬ 𝑅 ∈ NzRing)) |
5 | 4 | biimpar 482 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ ¬ 𝑅 ∈ NzRing) →
(♯‘(Base‘𝑅)) = 1) |
6 | 3, 5 | sylancom 592 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ { 0 } ∈
(LIdeal‘𝑅)) ∧
¬ 𝑅 ∈ NzRing)
→ (♯‘(Base‘𝑅)) = 1) |
7 | | eqid 2759 |
. . . . . . . . . . . 12
⊢
(Base‘𝑅) =
(Base‘𝑅) |
8 | | prmidl0.1 |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘𝑅) |
9 | 7, 8 | 0ring 20096 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧
(♯‘(Base‘𝑅)) = 1) → (Base‘𝑅) = { 0 }) |
10 | 3, 6, 9 | syl2anc 588 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ { 0 } ∈
(LIdeal‘𝑅)) ∧
¬ 𝑅 ∈ NzRing)
→ (Base‘𝑅) = {
0
}) |
11 | 10 | eqcomd 2765 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ { 0 } ∈
(LIdeal‘𝑅)) ∧
¬ 𝑅 ∈ NzRing)
→ { 0 } = (Base‘𝑅)) |
12 | 11 | ex 417 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ { 0 } ∈
(LIdeal‘𝑅)) →
(¬ 𝑅 ∈ NzRing
→ { 0 } = (Base‘𝑅))) |
13 | 12 | necon1ad 2966 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ { 0 } ∈
(LIdeal‘𝑅)) → ({
0 } ≠
(Base‘𝑅) → 𝑅 ∈
NzRing)) |
14 | 13 | impr 459 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ ({ 0 } ∈
(LIdeal‘𝑅) ∧ {
0 } ≠
(Base‘𝑅))) →
𝑅 ∈
NzRing) |
15 | | nzrring 20087 |
. . . . . . . . 9
⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring) |
16 | | eqid 2759 |
. . . . . . . . . 10
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
17 | 16, 8 | lidl0 20045 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → { 0 } ∈
(LIdeal‘𝑅)) |
18 | 15, 17 | syl 17 |
. . . . . . . 8
⊢ (𝑅 ∈ NzRing → { 0 } ∈
(LIdeal‘𝑅)) |
19 | 8 | fvexi 6665 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
20 | | hashsng 13765 |
. . . . . . . . . . . . 13
⊢ ( 0 ∈ V
→ (♯‘{ 0 }) = 1) |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(♯‘{ 0 }) = 1 |
22 | | 1re 10664 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
23 | 21, 22 | eqeltri 2847 |
. . . . . . . . . . 11
⊢
(♯‘{ 0 }) ∈
ℝ |
24 | 23 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑅 ∈ NzRing →
(♯‘{ 0 }) ∈
ℝ) |
25 | 7 | isnzr2hash 20090 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅)))) |
26 | 25 | simprbi 501 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ NzRing → 1 <
(♯‘(Base‘𝑅))) |
27 | 21, 26 | eqbrtrid 5060 |
. . . . . . . . . 10
⊢ (𝑅 ∈ NzRing →
(♯‘{ 0 }) <
(♯‘(Base‘𝑅))) |
28 | 24, 27 | ltned 10799 |
. . . . . . . . 9
⊢ (𝑅 ∈ NzRing →
(♯‘{ 0 }) ≠
(♯‘(Base‘𝑅))) |
29 | | fveq2 6651 |
. . . . . . . . . 10
⊢ ({ 0 } =
(Base‘𝑅) →
(♯‘{ 0 }) =
(♯‘(Base‘𝑅))) |
30 | 29 | necon3i 2981 |
. . . . . . . . 9
⊢
((♯‘{ 0 }) ≠
(♯‘(Base‘𝑅)) → { 0 } ≠ (Base‘𝑅)) |
31 | 28, 30 | syl 17 |
. . . . . . . 8
⊢ (𝑅 ∈ NzRing → { 0 } ≠
(Base‘𝑅)) |
32 | 18, 31 | jca 516 |
. . . . . . 7
⊢ (𝑅 ∈ NzRing → ({ 0 } ∈
(LIdeal‘𝑅) ∧ {
0 } ≠
(Base‘𝑅))) |
33 | 32 | adantl 486 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing) → ({ 0 } ∈
(LIdeal‘𝑅) ∧ {
0 } ≠
(Base‘𝑅))) |
34 | 14, 33 | impbida 801 |
. . . . 5
⊢ (𝑅 ∈ CRing → (({ 0 } ∈
(LIdeal‘𝑅) ∧ {
0 } ≠
(Base‘𝑅)) ↔
𝑅 ∈
NzRing)) |
35 | 19 | elsn2 4554 |
. . . . . . . 8
⊢ ((𝑥(.r‘𝑅)𝑦) ∈ { 0 } ↔ (𝑥(.r‘𝑅)𝑦) = 0 ) |
36 | | velsn 4531 |
. . . . . . . . 9
⊢ (𝑥 ∈ { 0 } ↔ 𝑥 = 0 ) |
37 | | velsn 4531 |
. . . . . . . . 9
⊢ (𝑦 ∈ { 0 } ↔ 𝑦 = 0 ) |
38 | 36, 37 | orbi12i 913 |
. . . . . . . 8
⊢ ((𝑥 ∈ { 0 } ∨ 𝑦 ∈ { 0 }) ↔ (𝑥 = 0 ∨ 𝑦 = 0 )) |
39 | 35, 38 | imbi12i 355 |
. . . . . . 7
⊢ (((𝑥(.r‘𝑅)𝑦) ∈ { 0 } → (𝑥 ∈ { 0 } ∨ 𝑦 ∈ { 0 })) ↔ ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))) |
40 | 39 | 2ralbii 3096 |
. . . . . 6
⊢
(∀𝑥 ∈
(Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) ∈ { 0 } → (𝑥 ∈ { 0 } ∨ 𝑦 ∈ { 0 })) ↔ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))) |
41 | 40 | a1i 11 |
. . . . 5
⊢ (𝑅 ∈ CRing →
(∀𝑥 ∈
(Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) ∈ { 0 } → (𝑥 ∈ { 0 } ∨ 𝑦 ∈ { 0 })) ↔ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )))) |
42 | 34, 41 | anbi12d 634 |
. . . 4
⊢ (𝑅 ∈ CRing → ((({ 0 } ∈
(LIdeal‘𝑅) ∧ {
0 } ≠
(Base‘𝑅)) ∧
∀𝑥 ∈
(Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) ∈ { 0 } → (𝑥 ∈ { 0 } ∨ 𝑦 ∈ { 0 }))) ↔ (𝑅 ∈ NzRing ∧
∀𝑥 ∈
(Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))) |
43 | 1, 42 | syl5bb 286 |
. . 3
⊢ (𝑅 ∈ CRing → (({ 0 } ∈
(LIdeal‘𝑅) ∧ {
0 } ≠
(Base‘𝑅) ∧
∀𝑥 ∈
(Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) ∈ { 0 } → (𝑥 ∈ { 0 } ∨ 𝑦 ∈ { 0 }))) ↔ (𝑅 ∈ NzRing ∧
∀𝑥 ∈
(Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))) |
44 | 43 | pm5.32i 579 |
. 2
⊢ ((𝑅 ∈ CRing ∧ ({ 0 } ∈
(LIdeal‘𝑅) ∧ {
0 } ≠
(Base‘𝑅) ∧
∀𝑥 ∈
(Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) ∈ { 0 } → (𝑥 ∈ { 0 } ∨ 𝑦 ∈ { 0 })))) ↔ (𝑅 ∈ CRing ∧ (𝑅 ∈ NzRing ∧
∀𝑥 ∈
(Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))) |
45 | | eqid 2759 |
. . . 4
⊢
(.r‘𝑅) = (.r‘𝑅) |
46 | 7, 45 | isprmidlc 31129 |
. . 3
⊢ (𝑅 ∈ CRing → ({ 0 } ∈
(PrmIdeal‘𝑅) ↔
({ 0 }
∈ (LIdeal‘𝑅)
∧ { 0
} ≠ (Base‘𝑅) ∧
∀𝑥 ∈
(Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) ∈ { 0 } → (𝑥 ∈ { 0 } ∨ 𝑦 ∈ { 0 }))))) |
47 | 46 | pm5.32i 579 |
. 2
⊢ ((𝑅 ∈ CRing ∧ { 0 } ∈
(PrmIdeal‘𝑅)) ↔
(𝑅 ∈ CRing ∧ ({
0 }
∈ (LIdeal‘𝑅)
∧ { 0
} ≠ (Base‘𝑅) ∧
∀𝑥 ∈
(Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) ∈ { 0 } → (𝑥 ∈ { 0 } ∨ 𝑦 ∈ { 0 }))))) |
48 | | df-idom 20111 |
. . . 4
⊢ IDomn =
(CRing ∩ Domn) |
49 | 48 | eleq2i 2842 |
. . 3
⊢ (𝑅 ∈ IDomn ↔ 𝑅 ∈ (CRing ∩
Domn)) |
50 | | elin 3870 |
. . 3
⊢ (𝑅 ∈ (CRing ∩ Domn)
↔ (𝑅 ∈ CRing
∧ 𝑅 ∈
Domn)) |
51 | 7, 45, 8 | isdomn 20120 |
. . . 4
⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧
∀𝑥 ∈
(Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )))) |
52 | 51 | anbi2i 626 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝑅 ∈ Domn) ↔ (𝑅 ∈ CRing ∧ (𝑅 ∈ NzRing ∧
∀𝑥 ∈
(Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))) |
53 | 49, 50, 52 | 3bitri 301 |
. 2
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ (𝑅 ∈ NzRing ∧
∀𝑥 ∈
(Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))) |
54 | 44, 47, 53 | 3bitr4i 307 |
1
⊢ ((𝑅 ∈ CRing ∧ { 0 } ∈
(PrmIdeal‘𝑅)) ↔
𝑅 ∈
IDomn) |