Step | Hyp | Ref
| Expression |
1 | | eqid 2732 |
. . . . . . . . . 10
β’
(Baseβπ
) =
(Baseβπ
) |
2 | | irredn0.z |
. . . . . . . . . 10
β’ 0 =
(0gβπ
) |
3 | 1, 2 | ring0cl 20077 |
. . . . . . . . 9
β’ (π
β Ring β 0 β
(Baseβπ
)) |
4 | 3 | anim1i 615 |
. . . . . . . 8
β’ ((π
β Ring β§ Β¬ 0 β
(Unitβπ
)) β (
0 β
(Baseβπ
) β§ Β¬
0 β
(Unitβπ
))) |
5 | | eldif 3957 |
. . . . . . . 8
β’ ( 0 β
((Baseβπ
) β
(Unitβπ
)) β (
0 β
(Baseβπ
) β§ Β¬
0 β
(Unitβπ
))) |
6 | 4, 5 | sylibr 233 |
. . . . . . 7
β’ ((π
β Ring β§ Β¬ 0 β
(Unitβπ
)) β
0 β
((Baseβπ
) β
(Unitβπ
))) |
7 | | eqid 2732 |
. . . . . . . . . 10
β’
(.rβπ
) = (.rβπ
) |
8 | 1, 7, 2 | ringlz 20100 |
. . . . . . . . 9
β’ ((π
β Ring β§ 0 β
(Baseβπ
)) β (
0
(.rβπ
)
0 ) =
0
) |
9 | 3, 8 | mpdan 685 |
. . . . . . . 8
β’ (π
β Ring β ( 0
(.rβπ
)
0 ) =
0
) |
10 | 9 | adantr 481 |
. . . . . . 7
β’ ((π
β Ring β§ Β¬ 0 β
(Unitβπ
)) β (
0
(.rβπ
)
0 ) =
0
) |
11 | | oveq1 7412 |
. . . . . . . . 9
β’ (π₯ = 0 β (π₯(.rβπ
)π¦) = ( 0 (.rβπ
)π¦)) |
12 | 11 | eqeq1d 2734 |
. . . . . . . 8
β’ (π₯ = 0 β ((π₯(.rβπ
)π¦) = 0 β ( 0
(.rβπ
)π¦) = 0 )) |
13 | | oveq2 7413 |
. . . . . . . . 9
β’ (π¦ = 0 β ( 0
(.rβπ
)π¦) = ( 0 (.rβπ
) 0 )) |
14 | 13 | eqeq1d 2734 |
. . . . . . . 8
β’ (π¦ = 0 β (( 0
(.rβπ
)π¦) = 0 β ( 0
(.rβπ
)
0 ) =
0
)) |
15 | 12, 14 | rspc2ev 3623 |
. . . . . . 7
β’ (( 0 β
((Baseβπ
) β
(Unitβπ
)) β§ 0 β
((Baseβπ
) β
(Unitβπ
)) β§ (
0
(.rβπ
)
0 ) =
0 )
β βπ₯ β
((Baseβπ
) β
(Unitβπ
))βπ¦ β ((Baseβπ
) β (Unitβπ
))(π₯(.rβπ
)π¦) = 0 ) |
16 | 6, 6, 10, 15 | syl3anc 1371 |
. . . . . 6
β’ ((π
β Ring β§ Β¬ 0 β
(Unitβπ
)) β
βπ₯ β
((Baseβπ
) β
(Unitβπ
))βπ¦ β ((Baseβπ
) β (Unitβπ
))(π₯(.rβπ
)π¦) = 0 ) |
17 | 16 | ex 413 |
. . . . 5
β’ (π
β Ring β (Β¬ 0 β
(Unitβπ
) β
βπ₯ β
((Baseβπ
) β
(Unitβπ
))βπ¦ β ((Baseβπ
) β (Unitβπ
))(π₯(.rβπ
)π¦) = 0 )) |
18 | 17 | orrd 861 |
. . . 4
β’ (π
β Ring β ( 0 β
(Unitβπ
) β¨
βπ₯ β
((Baseβπ
) β
(Unitβπ
))βπ¦ β ((Baseβπ
) β (Unitβπ
))(π₯(.rβπ
)π¦) = 0 )) |
19 | | eqid 2732 |
. . . . . 6
β’
(Unitβπ
) =
(Unitβπ
) |
20 | | irredn0.i |
. . . . . 6
β’ πΌ = (Irredβπ
) |
21 | | eqid 2732 |
. . . . . 6
β’
((Baseβπ
)
β (Unitβπ
)) =
((Baseβπ
) β
(Unitβπ
)) |
22 | 1, 19, 20, 21, 7 | isnirred 20226 |
. . . . 5
β’ ( 0 β
(Baseβπ
) β
(Β¬ 0
β πΌ β ( 0 β
(Unitβπ
) β¨
βπ₯ β
((Baseβπ
) β
(Unitβπ
))βπ¦ β ((Baseβπ
) β (Unitβπ
))(π₯(.rβπ
)π¦) = 0 ))) |
23 | 3, 22 | syl 17 |
. . . 4
β’ (π
β Ring β (Β¬ 0 β πΌ β ( 0 β (Unitβπ
) β¨ βπ₯ β ((Baseβπ
) β (Unitβπ
))βπ¦ β ((Baseβπ
) β (Unitβπ
))(π₯(.rβπ
)π¦) = 0 ))) |
24 | 18, 23 | mpbird 256 |
. . 3
β’ (π
β Ring β Β¬ 0 β πΌ) |
25 | 24 | adantr 481 |
. 2
β’ ((π
β Ring β§ π β πΌ) β Β¬ 0 β πΌ) |
26 | | simpr 485 |
. . . 4
β’ ((π
β Ring β§ π β πΌ) β π β πΌ) |
27 | | eleq1 2821 |
. . . 4
β’ (π = 0 β (π β πΌ β 0 β πΌ)) |
28 | 26, 27 | syl5ibcom 244 |
. . 3
β’ ((π
β Ring β§ π β πΌ) β (π = 0 β 0 β πΌ)) |
29 | 28 | necon3bd 2954 |
. 2
β’ ((π
β Ring β§ π β πΌ) β (Β¬ 0 β πΌ β π β 0 )) |
30 | 25, 29 | mpd 15 |
1
β’ ((π
β Ring β§ π β πΌ) β π β 0 ) |