Step | Hyp | Ref
| Expression |
1 | | df-ne 2942 |
. . 3
β’
((chrβπ
) β
0 β Β¬ (chrβπ
) = 0) |
2 | | domnring 20912 |
. . . . . . . . . 10
β’ (π
β Domn β π
β Ring) |
3 | | eqid 2733 |
. . . . . . . . . . 11
β’
(chrβπ
) =
(chrβπ
) |
4 | 3 | chrcl 21078 |
. . . . . . . . . 10
β’ (π
β Ring β
(chrβπ
) β
β0) |
5 | 2, 4 | syl 17 |
. . . . . . . . 9
β’ (π
β Domn β
(chrβπ
) β
β0) |
6 | 5 | adantr 482 |
. . . . . . . 8
β’ ((π
β Domn β§
(chrβπ
) β 0)
β (chrβπ
) β
β0) |
7 | | simpr 486 |
. . . . . . . 8
β’ ((π
β Domn β§
(chrβπ
) β 0)
β (chrβπ
) β
0) |
8 | | eldifsn 4791 |
. . . . . . . 8
β’
((chrβπ
)
β (β0 β {0}) β ((chrβπ
) β β0 β§
(chrβπ
) β
0)) |
9 | 6, 7, 8 | sylanbrc 584 |
. . . . . . 7
β’ ((π
β Domn β§
(chrβπ
) β 0)
β (chrβπ
) β
(β0 β {0})) |
10 | | dfn2 12485 |
. . . . . . 7
β’ β =
(β0 β {0}) |
11 | 9, 10 | eleqtrrdi 2845 |
. . . . . 6
β’ ((π
β Domn β§
(chrβπ
) β 0)
β (chrβπ
) β
β) |
12 | | domnnzr 20911 |
. . . . . . . 8
β’ (π
β Domn β π
β NzRing) |
13 | | nzrring 20295 |
. . . . . . . . . 10
β’ (π
β NzRing β π
β Ring) |
14 | | chrnzr 21082 |
. . . . . . . . . 10
β’ (π
β Ring β (π
β NzRing β
(chrβπ
) β
1)) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
β’ (π
β NzRing β (π
β NzRing β
(chrβπ
) β
1)) |
16 | 15 | ibi 267 |
. . . . . . . 8
β’ (π
β NzRing β
(chrβπ
) β
1) |
17 | 12, 16 | syl 17 |
. . . . . . 7
β’ (π
β Domn β
(chrβπ
) β
1) |
18 | 17 | adantr 482 |
. . . . . 6
β’ ((π
β Domn β§
(chrβπ
) β 0)
β (chrβπ
) β
1) |
19 | | eluz2b3 12906 |
. . . . . 6
β’
((chrβπ
)
β (β€β₯β2) β ((chrβπ
) β β β§ (chrβπ
) β 1)) |
20 | 11, 18, 19 | sylanbrc 584 |
. . . . 5
β’ ((π
β Domn β§
(chrβπ
) β 0)
β (chrβπ
) β
(β€β₯β2)) |
21 | 2 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π
β Domn β§
(chrβπ
) β 0) β§
(π₯ β β€ β§
π¦ β β€)) β
π
β
Ring) |
22 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(β€RHomβπ
) = (β€RHomβπ
) |
23 | 22 | zrhrhm 21061 |
. . . . . . . . . . . 12
β’ (π
β Ring β
(β€RHomβπ
)
β (β€ring RingHom π
)) |
24 | 21, 23 | syl 17 |
. . . . . . . . . . 11
β’ (((π
β Domn β§
(chrβπ
) β 0) β§
(π₯ β β€ β§
π¦ β β€)) β
(β€RHomβπ
)
β (β€ring RingHom π
)) |
25 | | simprl 770 |
. . . . . . . . . . 11
β’ (((π
β Domn β§
(chrβπ
) β 0) β§
(π₯ β β€ β§
π¦ β β€)) β
π₯ β
β€) |
26 | | simprr 772 |
. . . . . . . . . . 11
β’ (((π
β Domn β§
(chrβπ
) β 0) β§
(π₯ β β€ β§
π¦ β β€)) β
π¦ β
β€) |
27 | | zringbas 21023 |
. . . . . . . . . . . 12
β’ β€ =
(Baseββ€ring) |
28 | | zringmulr 21027 |
. . . . . . . . . . . 12
β’ Β·
= (.rββ€ring) |
29 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(.rβπ
) = (.rβπ
) |
30 | 27, 28, 29 | rhmmul 20264 |
. . . . . . . . . . 11
β’
(((β€RHomβπ
) β (β€ring RingHom
π
) β§ π₯ β β€ β§ π¦ β β€) β
((β€RHomβπ
)β(π₯ Β· π¦)) = (((β€RHomβπ
)βπ₯)(.rβπ
)((β€RHomβπ
)βπ¦))) |
31 | 24, 25, 26, 30 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π
β Domn β§
(chrβπ
) β 0) β§
(π₯ β β€ β§
π¦ β β€)) β
((β€RHomβπ
)β(π₯ Β· π¦)) = (((β€RHomβπ
)βπ₯)(.rβπ
)((β€RHomβπ
)βπ¦))) |
32 | 31 | eqeq1d 2735 |
. . . . . . . . 9
β’ (((π
β Domn β§
(chrβπ
) β 0) β§
(π₯ β β€ β§
π¦ β β€)) β
(((β€RHomβπ
)β(π₯ Β· π¦)) = (0gβπ
) β (((β€RHomβπ
)βπ₯)(.rβπ
)((β€RHomβπ
)βπ¦)) = (0gβπ
))) |
33 | | simpll 766 |
. . . . . . . . . 10
β’ (((π
β Domn β§
(chrβπ
) β 0) β§
(π₯ β β€ β§
π¦ β β€)) β
π
β
Domn) |
34 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(Baseβπ
) =
(Baseβπ
) |
35 | 27, 34 | rhmf 20263 |
. . . . . . . . . . . 12
β’
((β€RHomβπ
) β (β€ring RingHom
π
) β
(β€RHomβπ
):β€βΆ(Baseβπ
)) |
36 | 24, 35 | syl 17 |
. . . . . . . . . . 11
β’ (((π
β Domn β§
(chrβπ
) β 0) β§
(π₯ β β€ β§
π¦ β β€)) β
(β€RHomβπ
):β€βΆ(Baseβπ
)) |
37 | 36, 25 | ffvelcdmd 7088 |
. . . . . . . . . 10
β’ (((π
β Domn β§
(chrβπ
) β 0) β§
(π₯ β β€ β§
π¦ β β€)) β
((β€RHomβπ
)βπ₯) β (Baseβπ
)) |
38 | 36, 26 | ffvelcdmd 7088 |
. . . . . . . . . 10
β’ (((π
β Domn β§
(chrβπ
) β 0) β§
(π₯ β β€ β§
π¦ β β€)) β
((β€RHomβπ
)βπ¦) β (Baseβπ
)) |
39 | | eqid 2733 |
. . . . . . . . . . 11
β’
(0gβπ
) = (0gβπ
) |
40 | 34, 29, 39 | domneq0 20913 |
. . . . . . . . . 10
β’ ((π
β Domn β§
((β€RHomβπ
)βπ₯) β (Baseβπ
) β§ ((β€RHomβπ
)βπ¦) β (Baseβπ
)) β ((((β€RHomβπ
)βπ₯)(.rβπ
)((β€RHomβπ
)βπ¦)) = (0gβπ
) β (((β€RHomβπ
)βπ₯) = (0gβπ
) β¨ ((β€RHomβπ
)βπ¦) = (0gβπ
)))) |
41 | 33, 37, 38, 40 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π
β Domn β§
(chrβπ
) β 0) β§
(π₯ β β€ β§
π¦ β β€)) β
((((β€RHomβπ
)βπ₯)(.rβπ
)((β€RHomβπ
)βπ¦)) = (0gβπ
) β (((β€RHomβπ
)βπ₯) = (0gβπ
) β¨ ((β€RHomβπ
)βπ¦) = (0gβπ
)))) |
42 | 32, 41 | bitrd 279 |
. . . . . . . 8
β’ (((π
β Domn β§
(chrβπ
) β 0) β§
(π₯ β β€ β§
π¦ β β€)) β
(((β€RHomβπ
)β(π₯ Β· π¦)) = (0gβπ
) β (((β€RHomβπ
)βπ₯) = (0gβπ
) β¨ ((β€RHomβπ
)βπ¦) = (0gβπ
)))) |
43 | 42 | biimpd 228 |
. . . . . . 7
β’ (((π
β Domn β§
(chrβπ
) β 0) β§
(π₯ β β€ β§
π¦ β β€)) β
(((β€RHomβπ
)β(π₯ Β· π¦)) = (0gβπ
) β (((β€RHomβπ
)βπ₯) = (0gβπ
) β¨ ((β€RHomβπ
)βπ¦) = (0gβπ
)))) |
44 | | zmulcl 12611 |
. . . . . . . . 9
β’ ((π₯ β β€ β§ π¦ β β€) β (π₯ Β· π¦) β β€) |
45 | 44 | adantl 483 |
. . . . . . . 8
β’ (((π
β Domn β§
(chrβπ
) β 0) β§
(π₯ β β€ β§
π¦ β β€)) β
(π₯ Β· π¦) β
β€) |
46 | 3, 22, 39 | chrdvds 21080 |
. . . . . . . 8
β’ ((π
β Ring β§ (π₯ Β· π¦) β β€) β ((chrβπ
) β₯ (π₯ Β· π¦) β ((β€RHomβπ
)β(π₯ Β· π¦)) = (0gβπ
))) |
47 | 21, 45, 46 | syl2anc 585 |
. . . . . . 7
β’ (((π
β Domn β§
(chrβπ
) β 0) β§
(π₯ β β€ β§
π¦ β β€)) β
((chrβπ
) β₯
(π₯ Β· π¦) β
((β€RHomβπ
)β(π₯ Β· π¦)) = (0gβπ
))) |
48 | 3, 22, 39 | chrdvds 21080 |
. . . . . . . . 9
β’ ((π
β Ring β§ π₯ β β€) β
((chrβπ
) β₯
π₯ β
((β€RHomβπ
)βπ₯) = (0gβπ
))) |
49 | 21, 25, 48 | syl2anc 585 |
. . . . . . . 8
β’ (((π
β Domn β§
(chrβπ
) β 0) β§
(π₯ β β€ β§
π¦ β β€)) β
((chrβπ
) β₯
π₯ β
((β€RHomβπ
)βπ₯) = (0gβπ
))) |
50 | 3, 22, 39 | chrdvds 21080 |
. . . . . . . . 9
β’ ((π
β Ring β§ π¦ β β€) β
((chrβπ
) β₯
π¦ β
((β€RHomβπ
)βπ¦) = (0gβπ
))) |
51 | 21, 26, 50 | syl2anc 585 |
. . . . . . . 8
β’ (((π
β Domn β§
(chrβπ
) β 0) β§
(π₯ β β€ β§
π¦ β β€)) β
((chrβπ
) β₯
π¦ β
((β€RHomβπ
)βπ¦) = (0gβπ
))) |
52 | 49, 51 | orbi12d 918 |
. . . . . . 7
β’ (((π
β Domn β§
(chrβπ
) β 0) β§
(π₯ β β€ β§
π¦ β β€)) β
(((chrβπ
) β₯
π₯ β¨ (chrβπ
) β₯ π¦) β (((β€RHomβπ
)βπ₯) = (0gβπ
) β¨ ((β€RHomβπ
)βπ¦) = (0gβπ
)))) |
53 | 43, 47, 52 | 3imtr4d 294 |
. . . . . 6
β’ (((π
β Domn β§
(chrβπ
) β 0) β§
(π₯ β β€ β§
π¦ β β€)) β
((chrβπ
) β₯
(π₯ Β· π¦) β ((chrβπ
) β₯ π₯ β¨ (chrβπ
) β₯ π¦))) |
54 | 53 | ralrimivva 3201 |
. . . . 5
β’ ((π
β Domn β§
(chrβπ
) β 0)
β βπ₯ β
β€ βπ¦ β
β€ ((chrβπ
)
β₯ (π₯ Β· π¦) β ((chrβπ
) β₯ π₯ β¨ (chrβπ
) β₯ π¦))) |
55 | | isprm6 16651 |
. . . . 5
β’
((chrβπ
)
β β β ((chrβπ
) β (β€β₯β2)
β§ βπ₯ β
β€ βπ¦ β
β€ ((chrβπ
)
β₯ (π₯ Β· π¦) β ((chrβπ
) β₯ π₯ β¨ (chrβπ
) β₯ π¦)))) |
56 | 20, 54, 55 | sylanbrc 584 |
. . . 4
β’ ((π
β Domn β§
(chrβπ
) β 0)
β (chrβπ
) β
β) |
57 | 56 | ex 414 |
. . 3
β’ (π
β Domn β
((chrβπ
) β 0
β (chrβπ
) β
β)) |
58 | 1, 57 | biimtrrid 242 |
. 2
β’ (π
β Domn β (Β¬
(chrβπ
) = 0 β
(chrβπ
) β
β)) |
59 | 58 | orrd 862 |
1
β’ (π
β Domn β
((chrβπ
) = 0 β¨
(chrβπ
) β
β)) |