Step | Hyp | Ref
| Expression |
1 | | df-3an 1090 |
. . . 4
β’ (({ 0 } β
(LIdealβπ
) β§ {
0 } β
(Baseβπ
) β§
βπ₯ β
(Baseβπ
)βπ¦ β (Baseβπ
)((π₯(.rβπ
)π¦) β { 0 } β (π₯ β { 0 } β¨ π¦ β { 0 }))) β (({ 0 } β
(LIdealβπ
) β§ {
0 } β
(Baseβπ
)) β§
βπ₯ β
(Baseβπ
)βπ¦ β (Baseβπ
)((π₯(.rβπ
)π¦) β { 0 } β (π₯ β { 0 } β¨ π¦ β { 0 })))) |
2 | | crngring 19900 |
. . . . . . . . . . . 12
β’ (π
β CRing β π
β Ring) |
3 | 2 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π
β CRing β§ { 0 } β
(LIdealβπ
)) β§
Β¬ π
β NzRing)
β π
β
Ring) |
4 | | 0ringnnzr 20662 |
. . . . . . . . . . . . 13
β’ (π
β Ring β
((β―β(Baseβπ
)) = 1 β Β¬ π
β NzRing)) |
5 | 4 | biimpar 479 |
. . . . . . . . . . . 12
β’ ((π
β Ring β§ Β¬ π
β NzRing) β
(β―β(Baseβπ
)) = 1) |
6 | 3, 5 | sylancom 589 |
. . . . . . . . . . 11
β’ (((π
β CRing β§ { 0 } β
(LIdealβπ
)) β§
Β¬ π
β NzRing)
β (β―β(Baseβπ
)) = 1) |
7 | | eqid 2738 |
. . . . . . . . . . . 12
β’
(Baseβπ
) =
(Baseβπ
) |
8 | | prmidl0.1 |
. . . . . . . . . . . 12
β’ 0 =
(0gβπ
) |
9 | 7, 8 | 0ring 20663 |
. . . . . . . . . . 11
β’ ((π
β Ring β§
(β―β(Baseβπ
)) = 1) β (Baseβπ
) = { 0 }) |
10 | 3, 6, 9 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π
β CRing β§ { 0 } β
(LIdealβπ
)) β§
Β¬ π
β NzRing)
β (Baseβπ
) = {
0
}) |
11 | 10 | eqcomd 2744 |
. . . . . . . . 9
β’ (((π
β CRing β§ { 0 } β
(LIdealβπ
)) β§
Β¬ π
β NzRing)
β { 0 } = (Baseβπ
)) |
12 | 11 | ex 414 |
. . . . . . . 8
β’ ((π
β CRing β§ { 0 } β
(LIdealβπ
)) β
(Β¬ π
β NzRing
β { 0 } = (Baseβπ
))) |
13 | 12 | necon1ad 2959 |
. . . . . . 7
β’ ((π
β CRing β§ { 0 } β
(LIdealβπ
)) β ({
0 } β
(Baseβπ
) β π
β
NzRing)) |
14 | 13 | impr 456 |
. . . . . 6
β’ ((π
β CRing β§ ({ 0 } β
(LIdealβπ
) β§ {
0 } β
(Baseβπ
))) β
π
β
NzRing) |
15 | | nzrring 20654 |
. . . . . . . . 9
β’ (π
β NzRing β π
β Ring) |
16 | | eqid 2738 |
. . . . . . . . . 10
β’
(LIdealβπ
) =
(LIdealβπ
) |
17 | 16, 8 | lidl0 20612 |
. . . . . . . . 9
β’ (π
β Ring β { 0 } β
(LIdealβπ
)) |
18 | 15, 17 | syl 17 |
. . . . . . . 8
β’ (π
β NzRing β { 0 } β
(LIdealβπ
)) |
19 | 8 | fvexi 6852 |
. . . . . . . . . . . . 13
β’ 0 β
V |
20 | | hashsng 14197 |
. . . . . . . . . . . . 13
β’ ( 0 β V
β (β―β{ 0 }) = 1) |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . . . 12
β’
(β―β{ 0 }) = 1 |
22 | | 1re 11089 |
. . . . . . . . . . . 12
β’ 1 β
β |
23 | 21, 22 | eqeltri 2835 |
. . . . . . . . . . 11
β’
(β―β{ 0 }) β
β |
24 | 23 | a1i 11 |
. . . . . . . . . 10
β’ (π
β NzRing β
(β―β{ 0 }) β
β) |
25 | 7 | isnzr2hash 20657 |
. . . . . . . . . . . 12
β’ (π
β NzRing β (π
β Ring β§ 1 <
(β―β(Baseβπ
)))) |
26 | 25 | simprbi 498 |
. . . . . . . . . . 11
β’ (π
β NzRing β 1 <
(β―β(Baseβπ
))) |
27 | 21, 26 | eqbrtrid 5139 |
. . . . . . . . . 10
β’ (π
β NzRing β
(β―β{ 0 }) <
(β―β(Baseβπ
))) |
28 | 24, 27 | ltned 11225 |
. . . . . . . . 9
β’ (π
β NzRing β
(β―β{ 0 }) β
(β―β(Baseβπ
))) |
29 | | fveq2 6838 |
. . . . . . . . . 10
β’ ({ 0 } =
(Baseβπ
) β
(β―β{ 0 }) =
(β―β(Baseβπ
))) |
30 | 29 | necon3i 2975 |
. . . . . . . . 9
β’
((β―β{ 0 }) β
(β―β(Baseβπ
)) β { 0 } β (Baseβπ
)) |
31 | 28, 30 | syl 17 |
. . . . . . . 8
β’ (π
β NzRing β { 0 } β
(Baseβπ
)) |
32 | 18, 31 | jca 513 |
. . . . . . 7
β’ (π
β NzRing β ({ 0 } β
(LIdealβπ
) β§ {
0 } β
(Baseβπ
))) |
33 | 32 | adantl 483 |
. . . . . 6
β’ ((π
β CRing β§ π
β NzRing) β ({ 0 } β
(LIdealβπ
) β§ {
0 } β
(Baseβπ
))) |
34 | 14, 33 | impbida 800 |
. . . . 5
β’ (π
β CRing β (({ 0 } β
(LIdealβπ
) β§ {
0 } β
(Baseβπ
)) β
π
β
NzRing)) |
35 | 19 | elsn2 4624 |
. . . . . . . 8
β’ ((π₯(.rβπ
)π¦) β { 0 } β (π₯(.rβπ
)π¦) = 0 ) |
36 | | velsn 4601 |
. . . . . . . . 9
β’ (π₯ β { 0 } β π₯ = 0 ) |
37 | | velsn 4601 |
. . . . . . . . 9
β’ (π¦ β { 0 } β π¦ = 0 ) |
38 | 36, 37 | orbi12i 914 |
. . . . . . . 8
β’ ((π₯ β { 0 } β¨ π¦ β { 0 }) β (π₯ = 0 β¨ π¦ = 0 )) |
39 | 35, 38 | imbi12i 351 |
. . . . . . 7
β’ (((π₯(.rβπ
)π¦) β { 0 } β (π₯ β { 0 } β¨ π¦ β { 0 })) β ((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 ))) |
40 | 39 | 2ralbii 3126 |
. . . . . 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 632 |
. . . 4
β’ (π
β CRing β ((({ 0 } β
(LIdealβπ
) β§ {
0 } β
(Baseβπ
)) β§
βπ₯ β
(Baseβπ
)βπ¦ β (Baseβπ
)((π₯(.rβπ
)π¦) β { 0 } β (π₯ β { 0 } β¨ π¦ β { 0 }))) β (π
β NzRing β§
βπ₯ β
(Baseβπ
)βπ¦ β (Baseβπ
)((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 ))))) |
43 | 1, 42 | bitrid 283 |
. . 3
β’ (π
β CRing β (({ 0 } β
(LIdealβπ
) β§ {
0 } β
(Baseβπ
) β§
βπ₯ β
(Baseβπ
)βπ¦ β (Baseβπ
)((π₯(.rβπ
)π¦) β { 0 } β (π₯ β { 0 } β¨ π¦ β { 0 }))) β (π
β NzRing β§
βπ₯ β
(Baseβπ
)βπ¦ β (Baseβπ
)((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 ))))) |
44 | 43 | pm5.32i 576 |
. 2
β’ ((π
β CRing β§ ({ 0 } β
(LIdealβπ
) β§ {
0 } β
(Baseβπ
) β§
βπ₯ β
(Baseβπ
)βπ¦ β (Baseβπ
)((π₯(.rβπ
)π¦) β { 0 } β (π₯ β { 0 } β¨ π¦ β { 0 })))) β (π
β CRing β§ (π
β NzRing β§
βπ₯ β
(Baseβπ
)βπ¦ β (Baseβπ
)((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 ))))) |
45 | | eqid 2738 |
. . . 4
β’
(.rβπ
) = (.rβπ
) |
46 | 7, 45 | isprmidlc 31997 |
. . 3
β’ (π
β CRing β ({ 0 } β
(PrmIdealβπ
) β
({ 0 }
β (LIdealβπ
)
β§ { 0
} β (Baseβπ
) β§
βπ₯ β
(Baseβπ
)βπ¦ β (Baseβπ
)((π₯(.rβπ
)π¦) β { 0 } β (π₯ β { 0 } β¨ π¦ β { 0 }))))) |
47 | 46 | pm5.32i 576 |
. 2
β’ ((π
β CRing β§ { 0 } β
(PrmIdealβπ
)) β
(π
β CRing β§ ({
0 }
β (LIdealβπ
)
β§ { 0
} β (Baseβπ
) β§
βπ₯ β
(Baseβπ
)βπ¦ β (Baseβπ
)((π₯(.rβπ
)π¦) β { 0 } β (π₯ β { 0 } β¨ π¦ β { 0 }))))) |
48 | | df-idom 20678 |
. . . 4
β’ IDomn =
(CRing β© Domn) |
49 | 48 | eleq2i 2830 |
. . 3
β’ (π
β IDomn β π
β (CRing β©
Domn)) |
50 | | elin 3925 |
. . 3
β’ (π
β (CRing β© Domn)
β (π
β CRing
β§ π
β
Domn)) |
51 | 7, 45, 8 | isdomn 20687 |
. . . 4
β’ (π
β Domn β (π
β NzRing β§
βπ₯ β
(Baseβπ
)βπ¦ β (Baseβπ
)((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 )))) |
52 | 51 | anbi2i 624 |
. . 3
β’ ((π
β CRing β§ π
β Domn) β (π
β CRing β§ (π
β NzRing β§
βπ₯ β
(Baseβπ
)βπ¦ β (Baseβπ
)((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 ))))) |
53 | 49, 50, 52 | 3bitri 297 |
. 2
β’ (π
β IDomn β (π
β CRing β§ (π
β NzRing β§
βπ₯ β
(Baseβπ
)βπ¦ β (Baseβπ
)((π₯(.rβπ
)π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 ))))) |
54 | 44, 47, 53 | 3bitr4i 303 |
1
β’ ((π
β CRing β§ { 0 } β
(PrmIdealβπ
)) β
π
β
IDomn) |