Step | Hyp | Ref
| Expression |
1 | | nnnn0 12428 |
. . . . . . 7
β’ (π β β β π β
β0) |
2 | | znchr.y |
. . . . . . . 8
β’ π =
(β€/nβ€βπ) |
3 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
4 | | eqid 2733 |
. . . . . . . 8
β’
(β€RHomβπ) = (β€RHomβπ) |
5 | 2, 3, 4 | znzrhfo 20977 |
. . . . . . 7
β’ (π β β0
β (β€RHomβπ):β€βontoβ(Baseβπ)) |
6 | 1, 5 | syl 17 |
. . . . . 6
β’ (π β β β
(β€RHomβπ):β€βontoβ(Baseβπ)) |
7 | | znrrg.e |
. . . . . . . 8
β’ πΈ = (RLRegβπ) |
8 | 7, 3 | rrgss 20785 |
. . . . . . 7
β’ πΈ β (Baseβπ) |
9 | 8 | sseli 3944 |
. . . . . 6
β’ (π₯ β πΈ β π₯ β (Baseβπ)) |
10 | | foelrn 7060 |
. . . . . 6
β’
(((β€RHomβπ):β€βontoβ(Baseβπ) β§ π₯ β (Baseβπ)) β βπ β β€ π₯ = ((β€RHomβπ)βπ)) |
11 | 6, 9, 10 | syl2an 597 |
. . . . 5
β’ ((π β β β§ π₯ β πΈ) β βπ β β€ π₯ = ((β€RHomβπ)βπ)) |
12 | 11 | ex 414 |
. . . 4
β’ (π β β β (π₯ β πΈ β βπ β β€ π₯ = ((β€RHomβπ)βπ))) |
13 | | nncn 12169 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β) |
14 | 13 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β π β β) |
15 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β π β β€) |
16 | | nnz 12528 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β π β
β€) |
17 | 16 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β π β β€) |
18 | | nnne0 12195 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β π β 0) |
19 | 18 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β π β 0) |
20 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π = 0 β§ π = 0) β π = 0) |
21 | 20 | necon3ai 2965 |
. . . . . . . . . . . . . . . . . 18
β’ (π β 0 β Β¬ (π = 0 β§ π = 0)) |
22 | 19, 21 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β Β¬ (π = 0 β§ π = 0)) |
23 | | gcdn0cl 16390 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β€ β§ π β β€) β§ Β¬
(π = 0 β§ π = 0)) β (π gcd π) β β) |
24 | 15, 17, 22, 23 | syl21anc 837 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β (π gcd π) β β) |
25 | 24 | nncnd 12177 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β (π gcd π) β β) |
26 | 24 | nnne0d 12211 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β (π gcd π) β 0) |
27 | 14, 25, 26 | divcan2d 11941 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β ((π gcd π) Β· (π / (π gcd π))) = π) |
28 | | gcddvds 16391 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β€ β§ π β β€) β ((π gcd π) β₯ π β§ (π gcd π) β₯ π)) |
29 | 15, 17, 28 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β ((π gcd π) β₯ π β§ (π gcd π) β₯ π)) |
30 | 29 | simpld 496 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β (π gcd π) β₯ π) |
31 | 24 | nnzd 12534 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β (π gcd π) β β€) |
32 | 29 | simprd 497 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β (π gcd π) β₯ π) |
33 | | simpll 766 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β π β β) |
34 | | nndivdvds 16153 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ (π gcd π) β β) β ((π gcd π) β₯ π β (π / (π gcd π)) β β)) |
35 | 33, 24, 34 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β ((π gcd π) β₯ π β (π / (π gcd π)) β β)) |
36 | 32, 35 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β (π / (π gcd π)) β β) |
37 | 36 | nnzd 12534 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β (π / (π gcd π)) β β€) |
38 | | dvdsmulc 16174 |
. . . . . . . . . . . . . . . 16
β’ (((π gcd π) β β€ β§ π β β€ β§ (π / (π gcd π)) β β€) β ((π gcd π) β₯ π β ((π gcd π) Β· (π / (π gcd π))) β₯ (π Β· (π / (π gcd π))))) |
39 | 31, 15, 37, 38 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β ((π gcd π) β₯ π β ((π gcd π) Β· (π / (π gcd π))) β₯ (π Β· (π / (π gcd π))))) |
40 | 30, 39 | mpd 15 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β ((π gcd π) Β· (π / (π gcd π))) β₯ (π Β· (π / (π gcd π)))) |
41 | 27, 40 | eqbrtrrd 5133 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β π β₯ (π Β· (π / (π gcd π)))) |
42 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β ((β€RHomβπ)βπ) β πΈ) |
43 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β π β
β0) |
44 | 43, 5 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β (β€RHomβπ):β€βontoβ(Baseβπ)) |
45 | | fof 6760 |
. . . . . . . . . . . . . . . . 17
β’
((β€RHomβπ):β€βontoβ(Baseβπ) β (β€RHomβπ):β€βΆ(Baseβπ)) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β (β€RHomβπ):β€βΆ(Baseβπ)) |
47 | 46, 37 | ffvelcdmd 7040 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β ((β€RHomβπ)β(π / (π gcd π))) β (Baseβπ)) |
48 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(.rβπ) = (.rβπ) |
49 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(0gβπ) = (0gβπ) |
50 | 7, 3, 48, 49 | rrgeq0i 20782 |
. . . . . . . . . . . . . . 15
β’
((((β€RHomβπ)βπ) β πΈ β§ ((β€RHomβπ)β(π / (π gcd π))) β (Baseβπ)) β ((((β€RHomβπ)βπ)(.rβπ)((β€RHomβπ)β(π / (π gcd π)))) = (0gβπ) β
((β€RHomβπ)β(π / (π gcd π))) = (0gβπ))) |
51 | 42, 47, 50 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β ((((β€RHomβπ)βπ)(.rβπ)((β€RHomβπ)β(π / (π gcd π)))) = (0gβπ) β
((β€RHomβπ)β(π / (π gcd π))) = (0gβπ))) |
52 | 2 | zncrng 20974 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β0
β π β
CRing) |
53 | 1, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β π β CRing) |
54 | | crngring 19984 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β CRing β π β Ring) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β π β Ring) |
56 | 55 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β π β Ring) |
57 | 4 | zrhrhm 20935 |
. . . . . . . . . . . . . . . . . 18
β’ (π β Ring β
(β€RHomβπ)
β (β€ring RingHom π)) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β (β€RHomβπ) β (β€ring
RingHom π)) |
59 | | zringbas 20898 |
. . . . . . . . . . . . . . . . . 18
β’ β€ =
(Baseββ€ring) |
60 | | zringmulr 20901 |
. . . . . . . . . . . . . . . . . 18
β’ Β·
= (.rββ€ring) |
61 | 59, 60, 48 | rhmmul 20169 |
. . . . . . . . . . . . . . . . 17
β’
(((β€RHomβπ) β (β€ring RingHom
π) β§ π β β€ β§ (π / (π gcd π)) β β€) β
((β€RHomβπ)β(π Β· (π / (π gcd π)))) = (((β€RHomβπ)βπ)(.rβπ)((β€RHomβπ)β(π / (π gcd π))))) |
62 | 58, 15, 37, 61 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β ((β€RHomβπ)β(π Β· (π / (π gcd π)))) = (((β€RHomβπ)βπ)(.rβπ)((β€RHomβπ)β(π / (π gcd π))))) |
63 | 62 | eqeq1d 2735 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β (((β€RHomβπ)β(π Β· (π / (π gcd π)))) = (0gβπ) β
(((β€RHomβπ)βπ)(.rβπ)((β€RHomβπ)β(π / (π gcd π)))) = (0gβπ))) |
64 | 15, 37 | zmulcld 12621 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β (π Β· (π / (π gcd π))) β β€) |
65 | 2, 4, 49 | zndvds0 20980 |
. . . . . . . . . . . . . . . 16
β’ ((π β β0
β§ (π Β· (π / (π gcd π))) β β€) β
(((β€RHomβπ)β(π Β· (π / (π gcd π)))) = (0gβπ) β π β₯ (π Β· (π / (π gcd π))))) |
66 | 43, 64, 65 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β (((β€RHomβπ)β(π Β· (π / (π gcd π)))) = (0gβπ) β π β₯ (π Β· (π / (π gcd π))))) |
67 | 63, 66 | bitr3d 281 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β ((((β€RHomβπ)βπ)(.rβπ)((β€RHomβπ)β(π / (π gcd π)))) = (0gβπ) β π β₯ (π Β· (π / (π gcd π))))) |
68 | 2, 4, 49 | zndvds0 20980 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ (π / (π gcd π)) β β€) β
(((β€RHomβπ)β(π / (π gcd π))) = (0gβπ) β π β₯ (π / (π gcd π)))) |
69 | 43, 37, 68 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β (((β€RHomβπ)β(π / (π gcd π))) = (0gβπ) β π β₯ (π / (π gcd π)))) |
70 | 51, 67, 69 | 3imtr3d 293 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β (π β₯ (π Β· (π / (π gcd π))) β π β₯ (π / (π gcd π)))) |
71 | 41, 70 | mpd 15 |
. . . . . . . . . . . 12
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β π β₯ (π / (π gcd π))) |
72 | 14, 25, 26 | divcan1d 11940 |
. . . . . . . . . . . 12
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β ((π / (π gcd π)) Β· (π gcd π)) = π) |
73 | 36 | nncnd 12177 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β (π / (π gcd π)) β β) |
74 | 73 | mulid1d 11180 |
. . . . . . . . . . . 12
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β ((π / (π gcd π)) Β· 1) = (π / (π gcd π))) |
75 | 71, 72, 74 | 3brtr4d 5141 |
. . . . . . . . . . 11
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β ((π / (π gcd π)) Β· (π gcd π)) β₯ ((π / (π gcd π)) Β· 1)) |
76 | | 1zzd 12542 |
. . . . . . . . . . . 12
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β 1 β β€) |
77 | 36 | nnne0d 12211 |
. . . . . . . . . . . 12
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β (π / (π gcd π)) β 0) |
78 | | dvdscmulr 16175 |
. . . . . . . . . . . 12
β’ (((π gcd π) β β€ β§ 1 β β€
β§ ((π / (π gcd π)) β β€ β§ (π / (π gcd π)) β 0)) β (((π / (π gcd π)) Β· (π gcd π)) β₯ ((π / (π gcd π)) Β· 1) β (π gcd π) β₯ 1)) |
79 | 31, 76, 37, 77, 78 | syl112anc 1375 |
. . . . . . . . . . 11
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β (((π / (π gcd π)) Β· (π gcd π)) β₯ ((π / (π gcd π)) Β· 1) β (π gcd π) β₯ 1)) |
80 | 75, 79 | mpbid 231 |
. . . . . . . . . 10
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β (π gcd π) β₯ 1) |
81 | 15, 17 | gcdcld 16396 |
. . . . . . . . . . 11
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β (π gcd π) β
β0) |
82 | | dvds1 16209 |
. . . . . . . . . . 11
β’ ((π gcd π) β β0 β ((π gcd π) β₯ 1 β (π gcd π) = 1)) |
83 | 81, 82 | syl 17 |
. . . . . . . . . 10
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β ((π gcd π) β₯ 1 β (π gcd π) = 1)) |
84 | 80, 83 | mpbid 231 |
. . . . . . . . 9
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β (π gcd π) = 1) |
85 | | znunit.u |
. . . . . . . . . . 11
β’ π = (Unitβπ) |
86 | 2, 85, 4 | znunit 20993 |
. . . . . . . . . 10
β’ ((π β β0
β§ π β β€)
β (((β€RHomβπ)βπ) β π β (π gcd π) = 1)) |
87 | 43, 15, 86 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β (((β€RHomβπ)βπ) β π β (π gcd π) = 1)) |
88 | 84, 87 | mpbird 257 |
. . . . . . . 8
β’ (((π β β β§ π β β€) β§
((β€RHomβπ)βπ) β πΈ) β ((β€RHomβπ)βπ) β π) |
89 | 88 | ex 414 |
. . . . . . 7
β’ ((π β β β§ π β β€) β
(((β€RHomβπ)βπ) β πΈ β ((β€RHomβπ)βπ) β π)) |
90 | | eleq1 2822 |
. . . . . . . 8
β’ (π₯ = ((β€RHomβπ)βπ) β (π₯ β πΈ β ((β€RHomβπ)βπ) β πΈ)) |
91 | | eleq1 2822 |
. . . . . . . 8
β’ (π₯ = ((β€RHomβπ)βπ) β (π₯ β π β ((β€RHomβπ)βπ) β π)) |
92 | 90, 91 | imbi12d 345 |
. . . . . . 7
β’ (π₯ = ((β€RHomβπ)βπ) β ((π₯ β πΈ β π₯ β π) β (((β€RHomβπ)βπ) β πΈ β ((β€RHomβπ)βπ) β π))) |
93 | 89, 92 | syl5ibrcom 247 |
. . . . . 6
β’ ((π β β β§ π β β€) β (π₯ = ((β€RHomβπ)βπ) β (π₯ β πΈ β π₯ β π))) |
94 | 93 | rexlimdva 3149 |
. . . . 5
β’ (π β β β
(βπ β β€
π₯ =
((β€RHomβπ)βπ) β (π₯ β πΈ β π₯ β π))) |
95 | 94 | com23 86 |
. . . 4
β’ (π β β β (π₯ β πΈ β (βπ β β€ π₯ = ((β€RHomβπ)βπ) β π₯ β π))) |
96 | 12, 95 | mpdd 43 |
. . 3
β’ (π β β β (π₯ β πΈ β π₯ β π)) |
97 | 96 | ssrdv 3954 |
. 2
β’ (π β β β πΈ β π) |
98 | 7, 85 | unitrrg 20786 |
. . 3
β’ (π β Ring β π β πΈ) |
99 | 55, 98 | syl 17 |
. 2
β’ (π β β β π β πΈ) |
100 | 97, 99 | eqssd 3965 |
1
β’ (π β β β πΈ = π) |