Step | Hyp | Ref
| Expression |
1 | | dchrghm.g |
. . . . . 6
β’ πΊ = (DChrβπ) |
2 | | dchrghm.z |
. . . . . 6
β’ π =
(β€/nβ€βπ) |
3 | | dchrghm.b |
. . . . . 6
β’ π· = (BaseβπΊ) |
4 | 1, 2, 3 | dchrmhm 26605 |
. . . . 5
β’ π· β ((mulGrpβπ) MndHom
(mulGrpββfld)) |
5 | | dchrghm.x |
. . . . 5
β’ (π β π β π·) |
6 | 4, 5 | sselid 3947 |
. . . 4
β’ (π β π β ((mulGrpβπ) MndHom
(mulGrpββfld))) |
7 | 1, 3 | dchrrcl 26604 |
. . . . . . . . 9
β’ (π β π· β π β β) |
8 | 5, 7 | syl 17 |
. . . . . . . 8
β’ (π β π β β) |
9 | 8 | nnnn0d 12480 |
. . . . . . 7
β’ (π β π β
β0) |
10 | 2 | zncrng 20967 |
. . . . . . 7
β’ (π β β0
β π β
CRing) |
11 | 9, 10 | syl 17 |
. . . . . 6
β’ (π β π β CRing) |
12 | | crngring 19983 |
. . . . . 6
β’ (π β CRing β π β Ring) |
13 | 11, 12 | syl 17 |
. . . . 5
β’ (π β π β Ring) |
14 | | dchrghm.u |
. . . . . 6
β’ π = (Unitβπ) |
15 | | eqid 2737 |
. . . . . 6
β’
(mulGrpβπ) =
(mulGrpβπ) |
16 | 14, 15 | unitsubm 20106 |
. . . . 5
β’ (π β Ring β π β
(SubMndβ(mulGrpβπ))) |
17 | 13, 16 | syl 17 |
. . . 4
β’ (π β π β (SubMndβ(mulGrpβπ))) |
18 | | dchrghm.h |
. . . . 5
β’ π» = ((mulGrpβπ) βΎs π) |
19 | 18 | resmhm 18638 |
. . . 4
β’ ((π β ((mulGrpβπ) MndHom
(mulGrpββfld)) β§ π β (SubMndβ(mulGrpβπ))) β (π βΎ π) β (π» MndHom
(mulGrpββfld))) |
20 | 6, 17, 19 | syl2anc 585 |
. . 3
β’ (π β (π βΎ π) β (π» MndHom
(mulGrpββfld))) |
21 | | cnring 20835 |
. . . . 5
β’
βfld β Ring |
22 | | cnfldbas 20816 |
. . . . . . 7
β’ β =
(Baseββfld) |
23 | | cnfld0 20837 |
. . . . . . 7
β’ 0 =
(0gββfld) |
24 | | cndrng 20842 |
. . . . . . 7
β’
βfld β DivRing |
25 | 22, 23, 24 | drngui 20205 |
. . . . . 6
β’ (β
β {0}) = (Unitββfld) |
26 | | eqid 2737 |
. . . . . 6
β’
(mulGrpββfld) =
(mulGrpββfld) |
27 | 25, 26 | unitsubm 20106 |
. . . . 5
β’
(βfld β Ring β (β β {0}) β
(SubMndβ(mulGrpββfld))) |
28 | 21, 27 | ax-mp 5 |
. . . 4
β’ (β
β {0}) β
(SubMndβ(mulGrpββfld)) |
29 | | df-ima 5651 |
. . . . 5
β’ (π β π) = ran (π βΎ π) |
30 | | eqid 2737 |
. . . . . . . . . 10
β’
(Baseβπ) =
(Baseβπ) |
31 | 1, 2, 3, 30, 5 | dchrf 26606 |
. . . . . . . . 9
β’ (π β π:(Baseβπ)βΆβ) |
32 | 30, 14 | unitss 20096 |
. . . . . . . . . 10
β’ π β (Baseβπ) |
33 | 32 | sseli 3945 |
. . . . . . . . 9
β’ (π₯ β π β π₯ β (Baseβπ)) |
34 | | ffvelcdm 7037 |
. . . . . . . . 9
β’ ((π:(Baseβπ)βΆβ β§ π₯ β (Baseβπ)) β (πβπ₯) β β) |
35 | 31, 33, 34 | syl2an 597 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β (πβπ₯) β β) |
36 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β π₯ β π) |
37 | 5 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β π β π·) |
38 | 33 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β π₯ β (Baseβπ)) |
39 | 1, 2, 3, 30, 14, 37, 38 | dchrn0 26614 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β ((πβπ₯) β 0 β π₯ β π)) |
40 | 36, 39 | mpbird 257 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β (πβπ₯) β 0) |
41 | | eldifsn 4752 |
. . . . . . . 8
β’ ((πβπ₯) β (β β {0}) β ((πβπ₯) β β β§ (πβπ₯) β 0)) |
42 | 35, 40, 41 | sylanbrc 584 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (πβπ₯) β (β β
{0})) |
43 | 42 | ralrimiva 3144 |
. . . . . 6
β’ (π β βπ₯ β π (πβπ₯) β (β β
{0})) |
44 | 31 | ffund 6677 |
. . . . . . 7
β’ (π β Fun π) |
45 | 31 | fdmd 6684 |
. . . . . . . 8
β’ (π β dom π = (Baseβπ)) |
46 | 32, 45 | sseqtrrid 4002 |
. . . . . . 7
β’ (π β π β dom π) |
47 | | funimass4 6912 |
. . . . . . 7
β’ ((Fun
π β§ π β dom π) β ((π β π) β (β β {0}) β
βπ₯ β π (πβπ₯) β (β β
{0}))) |
48 | 44, 46, 47 | syl2anc 585 |
. . . . . 6
β’ (π β ((π β π) β (β β {0}) β
βπ₯ β π (πβπ₯) β (β β
{0}))) |
49 | 43, 48 | mpbird 257 |
. . . . 5
β’ (π β (π β π) β (β β
{0})) |
50 | 29, 49 | eqsstrrid 3998 |
. . . 4
β’ (π β ran (π βΎ π) β (β β
{0})) |
51 | | dchrghm.m |
. . . . 5
β’ π =
((mulGrpββfld) βΎs (β β
{0})) |
52 | 51 | resmhm2b 18640 |
. . . 4
β’
(((β β {0}) β
(SubMndβ(mulGrpββfld)) β§ ran (π βΎ π) β (β β {0})) β
((π βΎ π) β (π» MndHom
(mulGrpββfld)) β (π βΎ π) β (π» MndHom π))) |
53 | 28, 50, 52 | sylancr 588 |
. . 3
β’ (π β ((π βΎ π) β (π» MndHom
(mulGrpββfld)) β (π βΎ π) β (π» MndHom π))) |
54 | 20, 53 | mpbid 231 |
. 2
β’ (π β (π βΎ π) β (π» MndHom π)) |
55 | 14, 18 | unitgrp 20103 |
. . . 4
β’ (π β Ring β π» β Grp) |
56 | 13, 55 | syl 17 |
. . 3
β’ (π β π» β Grp) |
57 | 51 | cnmgpabl 20874 |
. . . 4
β’ π β Abel |
58 | | ablgrp 19574 |
. . . 4
β’ (π β Abel β π β Grp) |
59 | 57, 58 | ax-mp 5 |
. . 3
β’ π β Grp |
60 | | ghmmhmb 19026 |
. . 3
β’ ((π» β Grp β§ π β Grp) β (π» GrpHom π) = (π» MndHom π)) |
61 | 56, 59, 60 | sylancl 587 |
. 2
β’ (π β (π» GrpHom π) = (π» MndHom π)) |
62 | 54, 61 | eleqtrrd 2841 |
1
β’ (π β (π βΎ π) β (π» GrpHom π)) |