Step | Hyp | Ref
| Expression |
1 | | dchrpt.g |
. . . . 5
β’ πΊ = (DChrβπ) |
2 | | dchrpt.z |
. . . . 5
β’ π =
(β€/nβ€βπ) |
3 | | dchrpt.d |
. . . . 5
β’ π· = (BaseβπΊ) |
4 | | dchrpt.b |
. . . . 5
β’ π΅ = (Baseβπ) |
5 | | dchrpt.1 |
. . . . 5
β’ 1 =
(1rβπ) |
6 | | dchrpt.n |
. . . . . 6
β’ (π β π β β) |
7 | 6 | ad3antrrr 729 |
. . . . 5
β’ ((((π β§ π΄ β (Unitβπ)) β§ π€ β Word (Unitβπ)) β§ (((mulGrpβπ) βΎs (Unitβπ))dom DProd (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ)))) β§ (((mulGrpβπ) βΎs (Unitβπ)) DProd (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ))))) = (Unitβπ))) β π β β) |
8 | | dchrpt.n1 |
. . . . . 6
β’ (π β π΄ β 1 ) |
9 | 8 | ad3antrrr 729 |
. . . . 5
β’ ((((π β§ π΄ β (Unitβπ)) β§ π€ β Word (Unitβπ)) β§ (((mulGrpβπ) βΎs (Unitβπ))dom DProd (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ)))) β§ (((mulGrpβπ) βΎs (Unitβπ)) DProd (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ))))) = (Unitβπ))) β π΄ β 1 ) |
10 | | eqid 2737 |
. . . . 5
β’
(Unitβπ) =
(Unitβπ) |
11 | | eqid 2737 |
. . . . 5
β’
((mulGrpβπ)
βΎs (Unitβπ)) = ((mulGrpβπ) βΎs (Unitβπ)) |
12 | | eqid 2737 |
. . . . 5
β’
(.gβ((mulGrpβπ) βΎs (Unitβπ))) =
(.gβ((mulGrpβπ) βΎs (Unitβπ))) |
13 | | oveq1 7369 |
. . . . . . . . 9
β’ (π = π β (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ)) = (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ))) |
14 | 13 | cbvmptv 5223 |
. . . . . . . 8
β’ (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ))) = (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ))) |
15 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π = π β (π€βπ) = (π€βπ)) |
16 | 15 | oveq2d 7378 |
. . . . . . . . 9
β’ (π = π β (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ)) = (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ))) |
17 | 16 | mpteq2dv 5212 |
. . . . . . . 8
β’ (π = π β (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ))) = (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ)))) |
18 | 14, 17 | eqtrid 2789 |
. . . . . . 7
β’ (π = π β (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ))) = (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ)))) |
19 | 18 | rneqd 5898 |
. . . . . 6
β’ (π = π β ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ))) = ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ)))) |
20 | 19 | cbvmptv 5223 |
. . . . 5
β’ (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ)))) = (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ)))) |
21 | | simpllr 775 |
. . . . 5
β’ ((((π β§ π΄ β (Unitβπ)) β§ π€ β Word (Unitβπ)) β§ (((mulGrpβπ) βΎs (Unitβπ))dom DProd (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ)))) β§ (((mulGrpβπ) βΎs (Unitβπ)) DProd (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ))))) = (Unitβπ))) β π΄ β (Unitβπ)) |
22 | | simplr 768 |
. . . . 5
β’ ((((π β§ π΄ β (Unitβπ)) β§ π€ β Word (Unitβπ)) β§ (((mulGrpβπ) βΎs (Unitβπ))dom DProd (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ)))) β§ (((mulGrpβπ) βΎs (Unitβπ)) DProd (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ))))) = (Unitβπ))) β π€ β Word (Unitβπ)) |
23 | | simprl 770 |
. . . . 5
β’ ((((π β§ π΄ β (Unitβπ)) β§ π€ β Word (Unitβπ)) β§ (((mulGrpβπ) βΎs (Unitβπ))dom DProd (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ)))) β§ (((mulGrpβπ) βΎs (Unitβπ)) DProd (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ))))) = (Unitβπ))) β ((mulGrpβπ) βΎs (Unitβπ))dom DProd (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ))))) |
24 | | simprr 772 |
. . . . 5
β’ ((((π β§ π΄ β (Unitβπ)) β§ π€ β Word (Unitβπ)) β§ (((mulGrpβπ) βΎs (Unitβπ))dom DProd (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ)))) β§ (((mulGrpβπ) βΎs (Unitβπ)) DProd (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ))))) = (Unitβπ))) β (((mulGrpβπ) βΎs (Unitβπ)) DProd (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ))))) = (Unitβπ)) |
25 | 1, 2, 3, 4, 5, 7, 9, 10, 11, 12, 20, 21, 22, 23, 24 | dchrptlem3 26630 |
. . . 4
β’ ((((π β§ π΄ β (Unitβπ)) β§ π€ β Word (Unitβπ)) β§ (((mulGrpβπ) βΎs (Unitβπ))dom DProd (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ)))) β§ (((mulGrpβπ) βΎs (Unitβπ)) DProd (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ))))) = (Unitβπ))) β βπ₯ β π· (π₯βπ΄) β 1) |
26 | 25 | 3adantr1 1170 |
. . 3
β’ ((((π β§ π΄ β (Unitβπ)) β§ π€ β Word (Unitβπ)) β§ ((π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ)))):dom π€βΆ{π’ β (SubGrpβ((mulGrpβπ) βΎs
(Unitβπ))) β£
(((mulGrpβπ)
βΎs (Unitβπ)) βΎs π’) β (CycGrp β© ran pGrp )} β§
((mulGrpβπ)
βΎs (Unitβπ))dom DProd (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ)))) β§ (((mulGrpβπ) βΎs (Unitβπ)) DProd (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ))))) = (Unitβπ))) β βπ₯ β π· (π₯βπ΄) β 1) |
27 | 10, 11 | unitgrpbas 20102 |
. . . 4
β’
(Unitβπ) =
(Baseβ((mulGrpβπ) βΎs (Unitβπ))) |
28 | | eqid 2737 |
. . . 4
β’ {π’ β
(SubGrpβ((mulGrpβπ) βΎs (Unitβπ))) β£
(((mulGrpβπ)
βΎs (Unitβπ)) βΎs π’) β (CycGrp β© ran pGrp )} = {π’ β
(SubGrpβ((mulGrpβπ) βΎs (Unitβπ))) β£
(((mulGrpβπ)
βΎs (Unitβπ)) βΎs π’) β (CycGrp β© ran pGrp
)} |
29 | 6 | nnnn0d 12480 |
. . . . . 6
β’ (π β π β
β0) |
30 | 2 | zncrng 20967 |
. . . . . 6
β’ (π β β0
β π β
CRing) |
31 | 10, 11 | unitabl 20104 |
. . . . . 6
β’ (π β CRing β
((mulGrpβπ)
βΎs (Unitβπ)) β Abel) |
32 | 29, 30, 31 | 3syl 18 |
. . . . 5
β’ (π β ((mulGrpβπ) βΎs
(Unitβπ)) β
Abel) |
33 | 32 | adantr 482 |
. . . 4
β’ ((π β§ π΄ β (Unitβπ)) β ((mulGrpβπ) βΎs (Unitβπ)) β Abel) |
34 | 2, 4 | znfi 20982 |
. . . . . . 7
β’ (π β β β π΅ β Fin) |
35 | 6, 34 | syl 17 |
. . . . . 6
β’ (π β π΅ β Fin) |
36 | 4, 10 | unitss 20096 |
. . . . . 6
β’
(Unitβπ)
β π΅ |
37 | | ssfi 9124 |
. . . . . 6
β’ ((π΅ β Fin β§
(Unitβπ) β
π΅) β (Unitβπ) β Fin) |
38 | 35, 36, 37 | sylancl 587 |
. . . . 5
β’ (π β (Unitβπ) β Fin) |
39 | 38 | adantr 482 |
. . . 4
β’ ((π β§ π΄ β (Unitβπ)) β (Unitβπ) β Fin) |
40 | | eqid 2737 |
. . . 4
β’ (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ)))) = (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ)))) |
41 | 27, 28, 33, 39, 12, 40 | ablfac2 19875 |
. . 3
β’ ((π β§ π΄ β (Unitβπ)) β βπ€ β Word (Unitβπ)((π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ)))):dom π€βΆ{π’ β (SubGrpβ((mulGrpβπ) βΎs
(Unitβπ))) β£
(((mulGrpβπ)
βΎs (Unitβπ)) βΎs π’) β (CycGrp β© ran pGrp )} β§
((mulGrpβπ)
βΎs (Unitβπ))dom DProd (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ)))) β§ (((mulGrpβπ) βΎs (Unitβπ)) DProd (π β dom π€ β¦ ran (π β β€ β¦ (π(.gβ((mulGrpβπ) βΎs
(Unitβπ)))(π€βπ))))) = (Unitβπ))) |
42 | 26, 41 | r19.29a 3160 |
. 2
β’ ((π β§ π΄ β (Unitβπ)) β βπ₯ β π· (π₯βπ΄) β 1) |
43 | 1 | dchrabl 26618 |
. . . 4
β’ (π β β β πΊ β Abel) |
44 | | ablgrp 19574 |
. . . 4
β’ (πΊ β Abel β πΊ β Grp) |
45 | | eqid 2737 |
. . . . 5
β’
(0gβπΊ) = (0gβπΊ) |
46 | 3, 45 | grpidcl 18785 |
. . . 4
β’ (πΊ β Grp β
(0gβπΊ)
β π·) |
47 | 6, 43, 44, 46 | 4syl 19 |
. . 3
β’ (π β (0gβπΊ) β π·) |
48 | | 0ne1 12231 |
. . . 4
β’ 0 β
1 |
49 | | dchrpt.a |
. . . . . . . 8
β’ (π β π΄ β π΅) |
50 | 1, 2, 3, 4, 10, 47, 49 | dchrn0 26614 |
. . . . . . 7
β’ (π β
(((0gβπΊ)βπ΄) β 0 β π΄ β (Unitβπ))) |
51 | 50 | necon1bbid 2984 |
. . . . . 6
β’ (π β (Β¬ π΄ β (Unitβπ) β ((0gβπΊ)βπ΄) = 0)) |
52 | 51 | biimpa 478 |
. . . . 5
β’ ((π β§ Β¬ π΄ β (Unitβπ)) β ((0gβπΊ)βπ΄) = 0) |
53 | 52 | neeq1d 3004 |
. . . 4
β’ ((π β§ Β¬ π΄ β (Unitβπ)) β (((0gβπΊ)βπ΄) β 1 β 0 β 1)) |
54 | 48, 53 | mpbiri 258 |
. . 3
β’ ((π β§ Β¬ π΄ β (Unitβπ)) β ((0gβπΊ)βπ΄) β 1) |
55 | | fveq1 6846 |
. . . . 5
β’ (π₯ = (0gβπΊ) β (π₯βπ΄) = ((0gβπΊ)βπ΄)) |
56 | 55 | neeq1d 3004 |
. . . 4
β’ (π₯ = (0gβπΊ) β ((π₯βπ΄) β 1 β ((0gβπΊ)βπ΄) β 1)) |
57 | 56 | rspcev 3584 |
. . 3
β’
(((0gβπΊ) β π· β§ ((0gβπΊ)βπ΄) β 1) β βπ₯ β π· (π₯βπ΄) β 1) |
58 | 47, 54, 57 | syl2an2r 684 |
. 2
β’ ((π β§ Β¬ π΄ β (Unitβπ)) β βπ₯ β π· (π₯βπ΄) β 1) |
59 | 42, 58 | pm2.61dan 812 |
1
β’ (π β βπ₯ β π· (π₯βπ΄) β 1) |