Step | Hyp | Ref
| Expression |
1 | | snfi 9044 |
. . . 4
β’ {0}
β Fin |
2 | | cnex 11191 |
. . . . . . . . 9
β’ β
β V |
3 | 2 | a1i 11 |
. . . . . . . 8
β’ (π β β β β
β V) |
4 | | ovexd 7444 |
. . . . . . . 8
β’ ((π β β β§ π§ β β) β (π§β(Οβπ)) β V) |
5 | | 1cnd 11209 |
. . . . . . . 8
β’ ((π β β β§ π§ β β) β 1 β
β) |
6 | | eqidd 2734 |
. . . . . . . 8
β’ (π β β β (π§ β β β¦ (π§β(Οβπ))) = (π§ β β β¦ (π§β(Οβπ)))) |
7 | | fconstmpt 5739 |
. . . . . . . . 9
β’ (β
Γ {1}) = (π§ β
β β¦ 1) |
8 | 7 | a1i 11 |
. . . . . . . 8
β’ (π β β β (β
Γ {1}) = (π§ β
β β¦ 1)) |
9 | 3, 4, 5, 6, 8 | offval2 7690 |
. . . . . . 7
β’ (π β β β ((π§ β β β¦ (π§β(Οβπ))) βf β
(β Γ {1})) = (π§
β β β¦ ((π§β(Οβπ)) β 1))) |
10 | | ssid 4005 |
. . . . . . . . . 10
β’ β
β β |
11 | 10 | a1i 11 |
. . . . . . . . 9
β’ (π β β β β
β β) |
12 | | 1cnd 11209 |
. . . . . . . . 9
β’ (π β β β 1 β
β) |
13 | | phicl 16702 |
. . . . . . . . . 10
β’ (π β β β
(Οβπ) β
β) |
14 | 13 | nnnn0d 12532 |
. . . . . . . . 9
β’ (π β β β
(Οβπ) β
β0) |
15 | | plypow 25719 |
. . . . . . . . 9
β’ ((β
β β β§ 1 β β β§ (Οβπ) β β0) β (π§ β β β¦ (π§β(Οβπ))) β
(Polyββ)) |
16 | 11, 12, 14, 15 | syl3anc 1372 |
. . . . . . . 8
β’ (π β β β (π§ β β β¦ (π§β(Οβπ))) β
(Polyββ)) |
17 | | ax-1cn 11168 |
. . . . . . . . 9
β’ 1 β
β |
18 | | plyconst 25720 |
. . . . . . . . 9
β’ ((β
β β β§ 1 β β) β (β Γ {1}) β
(Polyββ)) |
19 | 10, 17, 18 | mp2an 691 |
. . . . . . . 8
β’ (β
Γ {1}) β (Polyββ) |
20 | | plysubcl 25736 |
. . . . . . . 8
β’ (((π§ β β β¦ (π§β(Οβπ))) β (Polyββ)
β§ (β Γ {1}) β (Polyββ)) β ((π§ β β β¦ (π§β(Οβπ))) βf β
(β Γ {1})) β (Polyββ)) |
21 | 16, 19, 20 | sylancl 587 |
. . . . . . 7
β’ (π β β β ((π§ β β β¦ (π§β(Οβπ))) βf β
(β Γ {1})) β (Polyββ)) |
22 | 9, 21 | eqeltrrd 2835 |
. . . . . 6
β’ (π β β β (π§ β β β¦ ((π§β(Οβπ)) β 1)) β
(Polyββ)) |
23 | | 0cn 11206 |
. . . . . . 7
β’ 0 β
β |
24 | | neg1ne0 12328 |
. . . . . . . 8
β’ -1 β
0 |
25 | 13 | 0expd 14104 |
. . . . . . . . . . 11
β’ (π β β β
(0β(Οβπ)) =
0) |
26 | 25 | oveq1d 7424 |
. . . . . . . . . 10
β’ (π β β β
((0β(Οβπ))
β 1) = (0 β 1)) |
27 | | oveq1 7416 |
. . . . . . . . . . . . 13
β’ (π§ = 0 β (π§β(Οβπ)) = (0β(Οβπ))) |
28 | 27 | oveq1d 7424 |
. . . . . . . . . . . 12
β’ (π§ = 0 β ((π§β(Οβπ)) β 1) = ((0β(Οβπ)) β 1)) |
29 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π§ β β β¦ ((π§β(Οβπ)) β 1)) = (π§ β β β¦ ((π§β(Οβπ)) β 1)) |
30 | | ovex 7442 |
. . . . . . . . . . . 12
β’
((0β(Οβπ)) β 1) β V |
31 | 28, 29, 30 | fvmpt 6999 |
. . . . . . . . . . 11
β’ (0 β
β β ((π§ β
β β¦ ((π§β(Οβπ)) β 1))β0) =
((0β(Οβπ))
β 1)) |
32 | 23, 31 | ax-mp 5 |
. . . . . . . . . 10
β’ ((π§ β β β¦ ((π§β(Οβπ)) β 1))β0) =
((0β(Οβπ))
β 1) |
33 | | df-neg 11447 |
. . . . . . . . . 10
β’ -1 = (0
β 1) |
34 | 26, 32, 33 | 3eqtr4g 2798 |
. . . . . . . . 9
β’ (π β β β ((π§ β β β¦ ((π§β(Οβπ)) β 1))β0) =
-1) |
35 | 34 | neeq1d 3001 |
. . . . . . . 8
β’ (π β β β (((π§ β β β¦ ((π§β(Οβπ)) β 1))β0) β 0
β -1 β 0)) |
36 | 24, 35 | mpbiri 258 |
. . . . . . 7
β’ (π β β β ((π§ β β β¦ ((π§β(Οβπ)) β 1))β0) β
0) |
37 | | ne0p 25721 |
. . . . . . 7
β’ ((0
β β β§ ((π§
β β β¦ ((π§β(Οβπ)) β 1))β0) β 0) β
(π§ β β β¦
((π§β(Οβπ)) β 1)) β
0π) |
38 | 23, 36, 37 | sylancr 588 |
. . . . . 6
β’ (π β β β (π§ β β β¦ ((π§β(Οβπ)) β 1)) β
0π) |
39 | 29 | mptiniseg 6239 |
. . . . . . . . 9
β’ (0 β
β β (β‘(π§ β β β¦ ((π§β(Οβπ)) β 1)) β {0}) = {π§ β β β£ ((π§β(Οβπ)) β 1) =
0}) |
40 | 23, 39 | ax-mp 5 |
. . . . . . . 8
β’ (β‘(π§ β β β¦ ((π§β(Οβπ)) β 1)) β {0}) = {π§ β β β£ ((π§β(Οβπ)) β 1) =
0} |
41 | 40 | eqcomi 2742 |
. . . . . . 7
β’ {π§ β β β£ ((π§β(Οβπ)) β 1) = 0} = (β‘(π§ β β β¦ ((π§β(Οβπ)) β 1)) β {0}) |
42 | 41 | fta1 25821 |
. . . . . 6
β’ (((π§ β β β¦ ((π§β(Οβπ)) β 1)) β
(Polyββ) β§ (π§ β β β¦ ((π§β(Οβπ)) β 1)) β 0π)
β ({π§ β β
β£ ((π§β(Οβπ)) β 1) = 0} β Fin β§
(β―β{π§ β
β β£ ((π§β(Οβπ)) β 1) = 0}) β€ (degβ(π§ β β β¦ ((π§β(Οβπ)) β
1))))) |
43 | 22, 38, 42 | syl2anc 585 |
. . . . 5
β’ (π β β β ({π§ β β β£ ((π§β(Οβπ)) β 1) = 0} β Fin
β§ (β―β{π§
β β β£ ((π§β(Οβπ)) β 1) = 0}) β€ (degβ(π§ β β β¦ ((π§β(Οβπ)) β
1))))) |
44 | 43 | simpld 496 |
. . . 4
β’ (π β β β {π§ β β β£ ((π§β(Οβπ)) β 1) = 0} β
Fin) |
45 | | unfi 9172 |
. . . 4
β’ (({0}
β Fin β§ {π§ β
β β£ ((π§β(Οβπ)) β 1) = 0} β Fin) β ({0}
βͺ {π§ β β
β£ ((π§β(Οβπ)) β 1) = 0}) β
Fin) |
46 | 1, 44, 45 | sylancr 588 |
. . 3
β’ (π β β β ({0}
βͺ {π§ β β
β£ ((π§β(Οβπ)) β 1) = 0}) β
Fin) |
47 | | eqid 2733 |
. . . 4
β’
(β€/nβ€βπ) = (β€/nβ€βπ) |
48 | | eqid 2733 |
. . . 4
β’
(Baseβ(β€/nβ€βπ)) =
(Baseβ(β€/nβ€βπ)) |
49 | 47, 48 | znfi 21115 |
. . 3
β’ (π β β β
(Baseβ(β€/nβ€βπ)) β Fin) |
50 | | mapfi 9348 |
. . 3
β’ ((({0}
βͺ {π§ β β
β£ ((π§β(Οβπ)) β 1) = 0}) β Fin β§
(Baseβ(β€/nβ€βπ)) β Fin) β (({0} βͺ {π§ β β β£ ((π§β(Οβπ)) β 1) = 0})
βm (Baseβ(β€/nβ€βπ))) β Fin) |
51 | 46, 49, 50 | syl2anc 585 |
. 2
β’ (π β β β (({0}
βͺ {π§ β β
β£ ((π§β(Οβπ)) β 1) = 0}) βm
(Baseβ(β€/nβ€βπ))) β Fin) |
52 | | dchrabl.g |
. . . . . . . 8
β’ πΊ = (DChrβπ) |
53 | | dchrfi.b |
. . . . . . . 8
β’ π· = (BaseβπΊ) |
54 | | simpr 486 |
. . . . . . . 8
β’ ((π β β β§ π β π·) β π β π·) |
55 | 52, 47, 53, 48, 54 | dchrf 26745 |
. . . . . . 7
β’ ((π β β β§ π β π·) β π:(Baseβ(β€/nβ€βπ))βΆβ) |
56 | 55 | ffnd 6719 |
. . . . . 6
β’ ((π β β β§ π β π·) β π Fn
(Baseβ(β€/nβ€βπ))) |
57 | | df-ne 2942 |
. . . . . . . . . . 11
β’ ((πβπ₯) β 0 β Β¬ (πβπ₯) = 0) |
58 | | fvex 6905 |
. . . . . . . . . . . 12
β’ (πβπ₯) β V |
59 | 58 | elsn 4644 |
. . . . . . . . . . 11
β’ ((πβπ₯) β {0} β (πβπ₯) = 0) |
60 | 57, 59 | xchbinxr 335 |
. . . . . . . . . 10
β’ ((πβπ₯) β 0 β Β¬ (πβπ₯) β {0}) |
61 | | oveq1 7416 |
. . . . . . . . . . . . . 14
β’ (π§ = (πβπ₯) β (π§β(Οβπ)) = ((πβπ₯)β(Οβπ))) |
62 | 61 | oveq1d 7424 |
. . . . . . . . . . . . 13
β’ (π§ = (πβπ₯) β ((π§β(Οβπ)) β 1) = (((πβπ₯)β(Οβπ)) β 1)) |
63 | 62 | eqeq1d 2735 |
. . . . . . . . . . . 12
β’ (π§ = (πβπ₯) β (((π§β(Οβπ)) β 1) = 0 β (((πβπ₯)β(Οβπ)) β 1) = 0)) |
64 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0) β π₯ β
(Baseβ(β€/nβ€βπ))) |
65 | | ffvelcdm 7084 |
. . . . . . . . . . . . 13
β’ ((π:(Baseβ(β€/nβ€βπ))βΆβ β§ π₯ β
(Baseβ(β€/nβ€βπ))) β (πβπ₯) β β) |
66 | 55, 64, 65 | syl2an 597 |
. . . . . . . . . . . 12
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β (πβπ₯) β β) |
67 | 52, 47, 53 | dchrmhm 26744 |
. . . . . . . . . . . . . . . . . 18
β’ π· β
((mulGrpβ(β€/nβ€βπ)) MndHom
(mulGrpββfld)) |
68 | | simplr 768 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β π β π·) |
69 | 67, 68 | sselid 3981 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β π β
((mulGrpβ(β€/nβ€βπ)) MndHom
(mulGrpββfld))) |
70 | 14 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β (Οβπ) β
β0) |
71 | | simprl 770 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β π₯ β
(Baseβ(β€/nβ€βπ))) |
72 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’
(mulGrpβ(β€/nβ€βπ)) =
(mulGrpβ(β€/nβ€βπ)) |
73 | 72, 48 | mgpbas 19993 |
. . . . . . . . . . . . . . . . . 18
β’
(Baseβ(β€/nβ€βπ)) =
(Baseβ(mulGrpβ(β€/nβ€βπ))) |
74 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’
(.gβ(mulGrpβ(β€/nβ€βπ))) =
(.gβ(mulGrpβ(β€/nβ€βπ))) |
75 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’
(.gβ(mulGrpββfld)) =
(.gβ(mulGrpββfld)) |
76 | 73, 74, 75 | mhmmulg 18995 |
. . . . . . . . . . . . . . . . 17
β’ ((π β
((mulGrpβ(β€/nβ€βπ)) MndHom
(mulGrpββfld)) β§ (Οβπ) β β0 β§ π₯ β
(Baseβ(β€/nβ€βπ))) β (πβ((Οβπ)(.gβ(mulGrpβ(β€/nβ€βπ)))π₯)) =
((Οβπ)(.gβ(mulGrpββfld))(πβπ₯))) |
77 | 69, 70, 71, 76 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β (πβ((Οβπ)(.gβ(mulGrpβ(β€/nβ€βπ)))π₯)) =
((Οβπ)(.gβ(mulGrpββfld))(πβπ₯))) |
78 | | nnnn0 12479 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β π β
β0) |
79 | 47 | zncrng 21100 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β0
β (β€/nβ€βπ) β CRing) |
80 | 78, 79 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β
(β€/nβ€βπ) β CRing) |
81 | | crngring 20068 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((β€/nβ€βπ) β CRing β
(β€/nβ€βπ) β Ring) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β
(β€/nβ€βπ) β Ring) |
83 | 82 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β
(β€/nβ€βπ) β Ring) |
84 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(Unitβ(β€/nβ€βπ)) =
(Unitβ(β€/nβ€βπ)) |
85 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ))) =
((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ))) |
86 | 84, 85 | unitgrp 20197 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((β€/nβ€βπ) β Ring β
((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ))) β Grp) |
87 | 83, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β
((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ))) β Grp) |
88 | 47, 84 | znunithash 21120 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β
(β―β(Unitβ(β€/nβ€βπ))) = (Οβπ)) |
89 | 88, 14 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β
(β―β(Unitβ(β€/nβ€βπ))) β
β0) |
90 | | fvex 6905 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(Unitβ(β€/nβ€βπ)) β V |
91 | | hashclb 14318 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((Unitβ(β€/nβ€βπ)) β V β
((Unitβ(β€/nβ€βπ)) β Fin β
(β―β(Unitβ(β€/nβ€βπ))) β
β0)) |
92 | 90, 91 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((Unitβ(β€/nβ€βπ)) β Fin β
(β―β(Unitβ(β€/nβ€βπ))) β
β0) |
93 | 89, 92 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β β
(Unitβ(β€/nβ€βπ)) β Fin) |
94 | 93 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β
(Unitβ(β€/nβ€βπ)) β Fin) |
95 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β (πβπ₯) β 0) |
96 | 52, 47, 53, 48, 84, 68, 71 | dchrn0 26753 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β ((πβπ₯) β 0 β π₯ β
(Unitβ(β€/nβ€βπ)))) |
97 | 95, 96 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β π₯ β
(Unitβ(β€/nβ€βπ))) |
98 | 84, 85 | unitgrpbas 20196 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(Unitβ(β€/nβ€βπ)) =
(Baseβ((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ)))) |
99 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(odβ((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ)))) =
(odβ((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ)))) |
100 | 98, 99 | oddvds2 19434 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ))) β Grp β§
(Unitβ(β€/nβ€βπ)) β Fin β§ π₯ β
(Unitβ(β€/nβ€βπ))) β
((odβ((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ))))βπ₯) β₯
(β―β(Unitβ(β€/nβ€βπ)))) |
101 | 87, 94, 97, 100 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β
((odβ((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ))))βπ₯) β₯
(β―β(Unitβ(β€/nβ€βπ)))) |
102 | 88 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β
(β―β(Unitβ(β€/nβ€βπ))) = (Οβπ)) |
103 | 101, 102 | breqtrd 5175 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β
((odβ((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ))))βπ₯) β₯ (Οβπ)) |
104 | 13 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β (Οβπ) β
β) |
105 | 104 | nnzd 12585 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β (Οβπ) β
β€) |
106 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(.gβ((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ)))) =
(.gβ((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ)))) |
107 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(0gβ((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ)))) =
(0gβ((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ)))) |
108 | 98, 99, 106, 107 | oddvds 19415 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ))) β Grp β§ π₯ β
(Unitβ(β€/nβ€βπ)) β§ (Οβπ) β β€) β
(((odβ((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ))))βπ₯) β₯ (Οβπ) β ((Οβπ)(.gβ((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ))))π₯) =
(0gβ((mulGrpβ(β€/nβ€βπ)) βΎs (Unitβ(β€/nβ€βπ)))))) |
109 | 87, 97, 105, 108 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β
(((odβ((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ))))βπ₯) β₯ (Οβπ) β ((Οβπ)(.gβ((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ))))π₯) =
(0gβ((mulGrpβ(β€/nβ€βπ)) βΎs (Unitβ(β€/nβ€βπ)))))) |
110 | 103, 109 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β ((Οβπ)(.gβ((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ))))π₯) =
(0gβ((mulGrpβ(β€/nβ€βπ)) βΎs (Unitβ(β€/nβ€βπ))))) |
111 | 84, 72 | unitsubm 20200 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β€/nβ€βπ) β Ring β
(Unitβ(β€/nβ€βπ)) β
(SubMndβ(mulGrpβ(β€/nβ€βπ)))) |
112 | 83, 111 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β
(Unitβ(β€/nβ€βπ)) β
(SubMndβ(mulGrpβ(β€/nβ€βπ)))) |
113 | 74, 85, 106 | submmulg 18998 |
. . . . . . . . . . . . . . . . . . 19
β’
(((Unitβ(β€/nβ€βπ)) β
(SubMndβ(mulGrpβ(β€/nβ€βπ))) β§ (Οβπ) β β0 β§ π₯ β
(Unitβ(β€/nβ€βπ))) β ((Οβπ)(.gβ(mulGrpβ(β€/nβ€βπ)))π₯) =
((Οβπ)(.gβ((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ))))π₯)) |
114 | 112, 70, 97, 113 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β ((Οβπ)(.gβ(mulGrpβ(β€/nβ€βπ)))π₯) =
((Οβπ)(.gβ((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ))))π₯)) |
115 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(1rβ(β€/nβ€βπ)) =
(1rβ(β€/nβ€βπ)) |
116 | 72, 115 | ringidval 20006 |
. . . . . . . . . . . . . . . . . . . 20
β’
(1rβ(β€/nβ€βπ)) =
(0gβ(mulGrpβ(β€/nβ€βπ))) |
117 | 85, 116 | subm0 18696 |
. . . . . . . . . . . . . . . . . . 19
β’
((Unitβ(β€/nβ€βπ)) β
(SubMndβ(mulGrpβ(β€/nβ€βπ))) β
(1rβ(β€/nβ€βπ)) =
(0gβ((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ))))) |
118 | 112, 117 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β
(1rβ(β€/nβ€βπ)) =
(0gβ((mulGrpβ(β€/nβ€βπ)) βΎs
(Unitβ(β€/nβ€βπ))))) |
119 | 110, 114,
118 | 3eqtr4d 2783 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β ((Οβπ)(.gβ(mulGrpβ(β€/nβ€βπ)))π₯) =
(1rβ(β€/nβ€βπ))) |
120 | 119 | fveq2d 6896 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β (πβ((Οβπ)(.gβ(mulGrpβ(β€/nβ€βπ)))π₯)) =
(πβ(1rβ(β€/nβ€βπ)))) |
121 | 77, 120 | eqtr3d 2775 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β ((Οβπ)(.gβ(mulGrpββfld))(πβπ₯)) = (πβ(1rβ(β€/nβ€βπ)))) |
122 | | cnfldexp 20978 |
. . . . . . . . . . . . . . . 16
β’ (((πβπ₯) β β β§ (Οβπ) β β0)
β ((Οβπ)(.gβ(mulGrpββfld))(πβπ₯)) = ((πβπ₯)β(Οβπ))) |
123 | 66, 70, 122 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β ((Οβπ)(.gβ(mulGrpββfld))(πβπ₯)) = ((πβπ₯)β(Οβπ))) |
124 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’
(mulGrpββfld) =
(mulGrpββfld) |
125 | | cnfld1 20970 |
. . . . . . . . . . . . . . . . . 18
β’ 1 =
(1rββfld) |
126 | 124, 125 | ringidval 20006 |
. . . . . . . . . . . . . . . . 17
β’ 1 =
(0gβ(mulGrpββfld)) |
127 | 116, 126 | mhm0 18680 |
. . . . . . . . . . . . . . . 16
β’ (π β
((mulGrpβ(β€/nβ€βπ)) MndHom
(mulGrpββfld)) β (πβ(1rβ(β€/nβ€βπ))) = 1) |
128 | 69, 127 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β (πβ(1rβ(β€/nβ€βπ))) = 1) |
129 | 121, 123,
128 | 3eqtr3d 2781 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β ((πβπ₯)β(Οβπ)) = 1) |
130 | 129 | oveq1d 7424 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β (((πβπ₯)β(Οβπ)) β 1) = (1 β
1)) |
131 | | 1m1e0 12284 |
. . . . . . . . . . . . 13
β’ (1
β 1) = 0 |
132 | 130, 131 | eqtrdi 2789 |
. . . . . . . . . . . 12
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β (((πβπ₯)β(Οβπ)) β 1) = 0) |
133 | 63, 66, 132 | elrabd 3686 |
. . . . . . . . . . 11
β’ (((π β β β§ π β π·) β§ (π₯ β
(Baseβ(β€/nβ€βπ)) β§ (πβπ₯) β 0)) β (πβπ₯) β {π§ β β β£ ((π§β(Οβπ)) β 1) = 0}) |
134 | 133 | expr 458 |
. . . . . . . . . 10
β’ (((π β β β§ π β π·) β§ π₯ β
(Baseβ(β€/nβ€βπ))) β ((πβπ₯) β 0 β (πβπ₯) β {π§ β β β£ ((π§β(Οβπ)) β 1) = 0})) |
135 | 60, 134 | biimtrrid 242 |
. . . . . . . . 9
β’ (((π β β β§ π β π·) β§ π₯ β
(Baseβ(β€/nβ€βπ))) β (Β¬ (πβπ₯) β {0} β (πβπ₯) β {π§ β β β£ ((π§β(Οβπ)) β 1) = 0})) |
136 | 135 | orrd 862 |
. . . . . . . 8
β’ (((π β β β§ π β π·) β§ π₯ β
(Baseβ(β€/nβ€βπ))) β ((πβπ₯) β {0} β¨ (πβπ₯) β {π§ β β β£ ((π§β(Οβπ)) β 1) = 0})) |
137 | | elun 4149 |
. . . . . . . 8
β’ ((πβπ₯) β ({0} βͺ {π§ β β β£ ((π§β(Οβπ)) β 1) = 0}) β ((πβπ₯) β {0} β¨ (πβπ₯) β {π§ β β β£ ((π§β(Οβπ)) β 1) = 0})) |
138 | 136, 137 | sylibr 233 |
. . . . . . 7
β’ (((π β β β§ π β π·) β§ π₯ β
(Baseβ(β€/nβ€βπ))) β (πβπ₯) β ({0} βͺ {π§ β β β£ ((π§β(Οβπ)) β 1) = 0})) |
139 | 138 | ralrimiva 3147 |
. . . . . 6
β’ ((π β β β§ π β π·) β βπ₯ β
(Baseβ(β€/nβ€βπ))(πβπ₯) β ({0} βͺ {π§ β β β£ ((π§β(Οβπ)) β 1) = 0})) |
140 | | ffnfv 7118 |
. . . . . 6
β’ (π:(Baseβ(β€/nβ€βπ))βΆ({0} βͺ {π§ β β β£ ((π§β(Οβπ)) β 1) = 0}) β (π Fn
(Baseβ(β€/nβ€βπ)) β§ βπ₯ β
(Baseβ(β€/nβ€βπ))(πβπ₯) β ({0} βͺ {π§ β β β£ ((π§β(Οβπ)) β 1) = 0}))) |
141 | 56, 139, 140 | sylanbrc 584 |
. . . . 5
β’ ((π β β β§ π β π·) β π:(Baseβ(β€/nβ€βπ))βΆ({0} βͺ {π§ β β β£ ((π§β(Οβπ)) β 1) =
0})) |
142 | 141 | ex 414 |
. . . 4
β’ (π β β β (π β π· β π:(Baseβ(β€/nβ€βπ))βΆ({0} βͺ {π§ β β β£ ((π§β(Οβπ)) β 1) =
0}))) |
143 | 46, 49 | elmapd 8834 |
. . . 4
β’ (π β β β (π β (({0} βͺ {π§ β β β£ ((π§β(Οβπ)) β 1) = 0})
βm (Baseβ(β€/nβ€βπ))) β π:(Baseβ(β€/nβ€βπ))βΆ({0} βͺ {π§ β β β£ ((π§β(Οβπ)) β 1) =
0}))) |
144 | 142, 143 | sylibrd 259 |
. . 3
β’ (π β β β (π β π· β π β (({0} βͺ {π§ β β β£ ((π§β(Οβπ)) β 1) = 0}) βm
(Baseβ(β€/nβ€βπ))))) |
145 | 144 | ssrdv 3989 |
. 2
β’ (π β β β π· β (({0} βͺ {π§ β β β£ ((π§β(Οβπ)) β 1) = 0})
βm (Baseβ(β€/nβ€βπ)))) |
146 | 51, 145 | ssfid 9267 |
1
β’ (π β β β π· β Fin) |