Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. 2
β’
(CntzβπΊ) =
(CntzβπΊ) |
2 | | eqid 2737 |
. 2
β’
(0gβπΊ) = (0gβπΊ) |
3 | | eqid 2737 |
. 2
β’
(mrClsβ(SubGrpβπΊ)) = (mrClsβ(SubGrpβπΊ)) |
4 | | ablfac1.g |
. . 3
β’ (π β πΊ β Abel) |
5 | | ablgrp 19574 |
. . 3
β’ (πΊ β Abel β πΊ β Grp) |
6 | 4, 5 | syl 17 |
. 2
β’ (π β πΊ β Grp) |
7 | | ablfac1.1 |
. . 3
β’ (π β π΄ β β) |
8 | | prmex 16560 |
. . . 4
β’ β
β V |
9 | 8 | ssex 5283 |
. . 3
β’ (π΄ β β β π΄ β V) |
10 | 7, 9 | syl 17 |
. 2
β’ (π β π΄ β V) |
11 | 4 | adantr 482 |
. . . 4
β’ ((π β§ π β π΄) β πΊ β Abel) |
12 | 7 | sselda 3949 |
. . . . . . 7
β’ ((π β§ π β π΄) β π β β) |
13 | | prmnn 16557 |
. . . . . . 7
β’ (π β β β π β
β) |
14 | 12, 13 | syl 17 |
. . . . . 6
β’ ((π β§ π β π΄) β π β β) |
15 | | ablfac1.b |
. . . . . . . . . . 11
β’ π΅ = (BaseβπΊ) |
16 | 15 | grpbn0 18786 |
. . . . . . . . . 10
β’ (πΊ β Grp β π΅ β β
) |
17 | 6, 16 | syl 17 |
. . . . . . . . 9
β’ (π β π΅ β β
) |
18 | | ablfac1.f |
. . . . . . . . . 10
β’ (π β π΅ β Fin) |
19 | | hashnncl 14273 |
. . . . . . . . . 10
β’ (π΅ β Fin β
((β―βπ΅) β
β β π΅ β
β
)) |
20 | 18, 19 | syl 17 |
. . . . . . . . 9
β’ (π β ((β―βπ΅) β β β π΅ β β
)) |
21 | 17, 20 | mpbird 257 |
. . . . . . . 8
β’ (π β (β―βπ΅) β
β) |
22 | 21 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π΄) β (β―βπ΅) β β) |
23 | 12, 22 | pccld 16729 |
. . . . . 6
β’ ((π β§ π β π΄) β (π pCnt (β―βπ΅)) β
β0) |
24 | 14, 23 | nnexpcld 14155 |
. . . . 5
β’ ((π β§ π β π΄) β (πβ(π pCnt (β―βπ΅))) β β) |
25 | 24 | nnzd 12533 |
. . . 4
β’ ((π β§ π β π΄) β (πβ(π pCnt (β―βπ΅))) β β€) |
26 | | ablfac1.o |
. . . . 5
β’ π = (odβπΊ) |
27 | 26, 15 | oddvdssubg 19640 |
. . . 4
β’ ((πΊ β Abel β§ (πβ(π pCnt (β―βπ΅))) β β€) β {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))} β (SubGrpβπΊ)) |
28 | 11, 25, 27 | syl2anc 585 |
. . 3
β’ ((π β§ π β π΄) β {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))} β (SubGrpβπΊ)) |
29 | | ablfac1.s |
. . 3
β’ π = (π β π΄ β¦ {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) |
30 | 28, 29 | fmptd 7067 |
. 2
β’ (π β π:π΄βΆ(SubGrpβπΊ)) |
31 | 4 | adantr 482 |
. . 3
β’ ((π β§ (π β π΄ β§ π β π΄ β§ π β π)) β πΊ β Abel) |
32 | 30 | adantr 482 |
. . . 4
β’ ((π β§ (π β π΄ β§ π β π΄ β§ π β π)) β π:π΄βΆ(SubGrpβπΊ)) |
33 | | simpr1 1195 |
. . . 4
β’ ((π β§ (π β π΄ β§ π β π΄ β§ π β π)) β π β π΄) |
34 | 32, 33 | ffvelcdmd 7041 |
. . 3
β’ ((π β§ (π β π΄ β§ π β π΄ β§ π β π)) β (πβπ) β (SubGrpβπΊ)) |
35 | | simpr2 1196 |
. . . 4
β’ ((π β§ (π β π΄ β§ π β π΄ β§ π β π)) β π β π΄) |
36 | 32, 35 | ffvelcdmd 7041 |
. . 3
β’ ((π β§ (π β π΄ β§ π β π΄ β§ π β π)) β (πβπ) β (SubGrpβπΊ)) |
37 | 1, 31, 34, 36 | ablcntzd 19642 |
. 2
β’ ((π β§ (π β π΄ β§ π β π΄ β§ π β π)) β (πβπ) β ((CntzβπΊ)β(πβπ))) |
38 | | id 22 |
. . . . . . . . . 10
β’ (π = π β π = π) |
39 | | oveq1 7369 |
. . . . . . . . . 10
β’ (π = π β (π pCnt (β―βπ΅)) = (π pCnt (β―βπ΅))) |
40 | 38, 39 | oveq12d 7380 |
. . . . . . . . 9
β’ (π = π β (πβ(π pCnt (β―βπ΅))) = (πβ(π pCnt (β―βπ΅)))) |
41 | 40 | breq2d 5122 |
. . . . . . . 8
β’ (π = π β ((πβπ₯) β₯ (πβ(π pCnt (β―βπ΅))) β (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅))))) |
42 | 41 | rabbidv 3418 |
. . . . . . 7
β’ (π = π β {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))} = {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) |
43 | 15 | fvexi 6861 |
. . . . . . . 8
β’ π΅ β V |
44 | 43 | rabex 5294 |
. . . . . . 7
β’ {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))} β V |
45 | 42, 29, 44 | fvmpt3i 6958 |
. . . . . 6
β’ (π β π΄ β (πβπ) = {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) |
46 | 45 | adantl 483 |
. . . . 5
β’ ((π β§ π β π΄) β (πβπ) = {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) |
47 | | eqimss 4005 |
. . . . 5
β’ ((πβπ) = {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))} β (πβπ) β {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) |
48 | 46, 47 | syl 17 |
. . . 4
β’ ((π β§ π β π΄) β (πβπ) β {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) |
49 | 4 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π΄) β πΊ β Abel) |
50 | | eqid 2737 |
. . . . . . 7
β’
(BaseβπΊ) =
(BaseβπΊ) |
51 | 50 | subgacs 18970 |
. . . . . 6
β’ (πΊ β Grp β
(SubGrpβπΊ) β
(ACSβ(BaseβπΊ))) |
52 | | acsmre 17539 |
. . . . . 6
β’
((SubGrpβπΊ)
β (ACSβ(BaseβπΊ)) β (SubGrpβπΊ) β (Mooreβ(BaseβπΊ))) |
53 | 49, 5, 51, 52 | 4syl 19 |
. . . . 5
β’ ((π β§ π β π΄) β (SubGrpβπΊ) β (Mooreβ(BaseβπΊ))) |
54 | | df-ima 5651 |
. . . . . . 7
β’ (π β (π΄ β {π})) = ran (π βΎ (π΄ β {π})) |
55 | 7 | sselda 3949 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π΄) β π β β) |
56 | 55 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β π β β) |
57 | 21 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β (β―βπ΅) β β) |
58 | | pcdvds 16743 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§
(β―βπ΅) β
β) β (πβ(π pCnt (β―βπ΅))) β₯ (β―βπ΅)) |
59 | 56, 57, 58 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β (πβ(π pCnt (β―βπ΅))) β₯ (β―βπ΅)) |
60 | 7 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β π΄ β β) |
61 | | eldifi 4091 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π΄ β {π}) β π β π΄) |
62 | 61 | ad2antlr 726 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β π β π΄) |
63 | 60, 62 | sseldd 3950 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β π β β) |
64 | | pcdvds 16743 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§
(β―βπ΅) β
β) β (πβ(π pCnt (β―βπ΅))) β₯ (β―βπ΅)) |
65 | 63, 57, 64 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β (πβ(π pCnt (β―βπ΅))) β₯ (β―βπ΅)) |
66 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πβ(π pCnt (β―βπ΅))) = (πβ(π pCnt (β―βπ΅))) |
67 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((β―βπ΅) /
(πβ(π pCnt (β―βπ΅)))) = ((β―βπ΅) / (πβ(π pCnt (β―βπ΅)))) |
68 | 15, 26, 29, 4, 18, 7, 66, 67 | ablfac1lem 19854 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β π΄) β (((πβ(π pCnt (β―βπ΅))) β β β§
((β―βπ΅) / (πβ(π pCnt (β―βπ΅)))) β β) β§ ((πβ(π pCnt (β―βπ΅))) gcd ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))) = 1 β§ (β―βπ΅) = ((πβ(π pCnt (β―βπ΅))) Β· ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))))) |
69 | 68 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β π΄) β ((πβ(π pCnt (β―βπ΅))) β β β§
((β―βπ΅) / (πβ(π pCnt (β―βπ΅)))) β β)) |
70 | 69 | simpld 496 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π΄) β (πβ(π pCnt (β―βπ΅))) β β) |
71 | 70 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β (πβ(π pCnt (β―βπ΅))) β β) |
72 | 71 | nnzd 12533 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β (πβ(π pCnt (β―βπ΅))) β β€) |
73 | 63, 13 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β π β β) |
74 | 63, 57 | pccld 16729 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β (π pCnt (β―βπ΅)) β
β0) |
75 | 73, 74 | nnexpcld 14155 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β (πβ(π pCnt (β―βπ΅))) β β) |
76 | 75 | nnzd 12533 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β (πβ(π pCnt (β―βπ΅))) β β€) |
77 | 57 | nnzd 12533 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β (β―βπ΅) β β€) |
78 | | eldifsni 4755 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π΄ β {π}) β π β π) |
79 | 78 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β π β π) |
80 | 79 | necomd 3000 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β π β π) |
81 | | prmrp 16595 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β β) β ((π gcd π) = 1 β π β π)) |
82 | 56, 63, 81 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β ((π gcd π) = 1 β π β π)) |
83 | 80, 82 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β (π gcd π) = 1) |
84 | | prmz 16558 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β π β
β€) |
85 | 56, 84 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β π β β€) |
86 | | prmz 16558 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β π β
β€) |
87 | 63, 86 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β π β β€) |
88 | 56, 57 | pccld 16729 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β (π pCnt (β―βπ΅)) β
β0) |
89 | | rpexp12i 16607 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β€ β§ π β β€ β§ ((π pCnt (β―βπ΅)) β β0
β§ (π pCnt
(β―βπ΅)) β
β0)) β ((π gcd π) = 1 β ((πβ(π pCnt (β―βπ΅))) gcd (πβ(π pCnt (β―βπ΅)))) = 1)) |
90 | 85, 87, 88, 74, 89 | syl112anc 1375 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β ((π gcd π) = 1 β ((πβ(π pCnt (β―βπ΅))) gcd (πβ(π pCnt (β―βπ΅)))) = 1)) |
91 | 83, 90 | mpd 15 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β ((πβ(π pCnt (β―βπ΅))) gcd (πβ(π pCnt (β―βπ΅)))) = 1) |
92 | | coprmdvds2 16537 |
. . . . . . . . . . . . . . . 16
β’ ((((πβ(π pCnt (β―βπ΅))) β β€ β§ (πβ(π pCnt (β―βπ΅))) β β€ β§
(β―βπ΅) β
β€) β§ ((πβ(π pCnt (β―βπ΅))) gcd (πβ(π pCnt (β―βπ΅)))) = 1) β (((πβ(π pCnt (β―βπ΅))) β₯ (β―βπ΅) β§ (πβ(π pCnt (β―βπ΅))) β₯ (β―βπ΅)) β ((πβ(π pCnt (β―βπ΅))) Β· (πβ(π pCnt (β―βπ΅)))) β₯ (β―βπ΅))) |
93 | 72, 76, 77, 91, 92 | syl31anc 1374 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β (((πβ(π pCnt (β―βπ΅))) β₯ (β―βπ΅) β§ (πβ(π pCnt (β―βπ΅))) β₯ (β―βπ΅)) β ((πβ(π pCnt (β―βπ΅))) Β· (πβ(π pCnt (β―βπ΅)))) β₯ (β―βπ΅))) |
94 | 59, 65, 93 | mp2and 698 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β ((πβ(π pCnt (β―βπ΅))) Β· (πβ(π pCnt (β―βπ΅)))) β₯ (β―βπ΅)) |
95 | 68 | simp3d 1145 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΄) β (β―βπ΅) = ((πβ(π pCnt (β―βπ΅))) Β· ((β―βπ΅) / (πβ(π pCnt (β―βπ΅)))))) |
96 | 95 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β (β―βπ΅) = ((πβ(π pCnt (β―βπ΅))) Β· ((β―βπ΅) / (πβ(π pCnt (β―βπ΅)))))) |
97 | 94, 96 | breqtrd 5136 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β ((πβ(π pCnt (β―βπ΅))) Β· (πβ(π pCnt (β―βπ΅)))) β₯ ((πβ(π pCnt (β―βπ΅))) Β· ((β―βπ΅) / (πβ(π pCnt (β―βπ΅)))))) |
98 | 69 | simprd 497 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π΄) β ((β―βπ΅) / (πβ(π pCnt (β―βπ΅)))) β β) |
99 | 98 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β ((β―βπ΅) / (πβ(π pCnt (β―βπ΅)))) β β) |
100 | 99 | nnzd 12533 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β ((β―βπ΅) / (πβ(π pCnt (β―βπ΅)))) β β€) |
101 | 71 | nnne0d 12210 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β (πβ(π pCnt (β―βπ΅))) β 0) |
102 | | dvdscmulr 16174 |
. . . . . . . . . . . . . 14
β’ (((πβ(π pCnt (β―βπ΅))) β β€ β§
((β―βπ΅) / (πβ(π pCnt (β―βπ΅)))) β β€ β§ ((πβ(π pCnt (β―βπ΅))) β β€ β§ (πβ(π pCnt (β―βπ΅))) β 0)) β (((πβ(π pCnt (β―βπ΅))) Β· (πβ(π pCnt (β―βπ΅)))) β₯ ((πβ(π pCnt (β―βπ΅))) Β· ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))) β (πβ(π pCnt (β―βπ΅))) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅)))))) |
103 | 76, 100, 72, 101, 102 | syl112anc 1375 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β (((πβ(π pCnt (β―βπ΅))) Β· (πβ(π pCnt (β―βπ΅)))) β₯ ((πβ(π pCnt (β―βπ΅))) Β· ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))) β (πβ(π pCnt (β―βπ΅))) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅)))))) |
104 | 97, 103 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β (πβ(π pCnt (β―βπ΅))) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))) |
105 | 15, 26 | odcl 19325 |
. . . . . . . . . . . . . . 15
β’ (π₯ β π΅ β (πβπ₯) β
β0) |
106 | 105 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β (πβπ₯) β
β0) |
107 | 106 | nn0zd 12532 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β (πβπ₯) β β€) |
108 | | dvdstr 16183 |
. . . . . . . . . . . . 13
β’ (((πβπ₯) β β€ β§ (πβ(π pCnt (β―βπ΅))) β β€ β§
((β―βπ΅) / (πβ(π pCnt (β―βπ΅)))) β β€) β (((πβπ₯) β₯ (πβ(π pCnt (β―βπ΅))) β§ (πβ(π pCnt (β―βπ΅))) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))) β (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅)))))) |
109 | 107, 76, 100, 108 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β (((πβπ₯) β₯ (πβ(π pCnt (β―βπ΅))) β§ (πβ(π pCnt (β―βπ΅))) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))) β (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅)))))) |
110 | 104, 109 | mpan2d 693 |
. . . . . . . . . . 11
β’ ((((π β§ π β π΄) β§ π β (π΄ β {π})) β§ π₯ β π΅) β ((πβπ₯) β₯ (πβ(π pCnt (β―βπ΅))) β (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅)))))) |
111 | 110 | ss2rabdv 4038 |
. . . . . . . . . 10
β’ (((π β§ π β π΄) β§ π β (π΄ β {π})) β {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))} β {π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))}) |
112 | 44 | elpw 4569 |
. . . . . . . . . 10
β’ ({π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))} β π« {π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))} β {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))} β {π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))}) |
113 | 111, 112 | sylibr 233 |
. . . . . . . . 9
β’ (((π β§ π β π΄) β§ π β (π΄ β {π})) β {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))} β π« {π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))}) |
114 | 29 | reseq1i 5938 |
. . . . . . . . . 10
β’ (π βΎ (π΄ β {π})) = ((π β π΄ β¦ {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) βΎ (π΄ β {π})) |
115 | | difss 4096 |
. . . . . . . . . . 11
β’ (π΄ β {π}) β π΄ |
116 | | resmpt 5996 |
. . . . . . . . . . 11
β’ ((π΄ β {π}) β π΄ β ((π β π΄ β¦ {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) βΎ (π΄ β {π})) = (π β (π΄ β {π}) β¦ {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))})) |
117 | 115, 116 | ax-mp 5 |
. . . . . . . . . 10
β’ ((π β π΄ β¦ {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) βΎ (π΄ β {π})) = (π β (π΄ β {π}) β¦ {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) |
118 | 114, 117 | eqtri 2765 |
. . . . . . . . 9
β’ (π βΎ (π΄ β {π})) = (π β (π΄ β {π}) β¦ {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) |
119 | 113, 118 | fmptd 7067 |
. . . . . . . 8
β’ ((π β§ π β π΄) β (π βΎ (π΄ β {π})):(π΄ β {π})βΆπ« {π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))}) |
120 | 119 | frnd 6681 |
. . . . . . 7
β’ ((π β§ π β π΄) β ran (π βΎ (π΄ β {π})) β π« {π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))}) |
121 | 54, 120 | eqsstrid 3997 |
. . . . . 6
β’ ((π β§ π β π΄) β (π β (π΄ β {π})) β π« {π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))}) |
122 | | sspwuni 5065 |
. . . . . 6
β’ ((π β (π΄ β {π})) β π« {π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))} β βͺ
(π β (π΄ β {π})) β {π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))}) |
123 | 121, 122 | sylib 217 |
. . . . 5
β’ ((π β§ π β π΄) β βͺ (π β (π΄ β {π})) β {π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))}) |
124 | 98 | nnzd 12533 |
. . . . . 6
β’ ((π β§ π β π΄) β ((β―βπ΅) / (πβ(π pCnt (β―βπ΅)))) β β€) |
125 | 26, 15 | oddvdssubg 19640 |
. . . . . 6
β’ ((πΊ β Abel β§
((β―βπ΅) / (πβ(π pCnt (β―βπ΅)))) β β€) β {π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))} β (SubGrpβπΊ)) |
126 | 49, 124, 125 | syl2anc 585 |
. . . . 5
β’ ((π β§ π β π΄) β {π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))} β (SubGrpβπΊ)) |
127 | 3 | mrcsscl 17507 |
. . . . 5
β’
(((SubGrpβπΊ)
β (Mooreβ(BaseβπΊ)) β§ βͺ (π β (π΄ β {π})) β {π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))} β§ {π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))} β (SubGrpβπΊ)) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (π΄ β {π}))) β {π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))}) |
128 | 53, 123, 126, 127 | syl3anc 1372 |
. . . 4
β’ ((π β§ π β π΄) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (π΄ β {π}))) β {π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))}) |
129 | | ss2in 4201 |
. . . 4
β’ (((πβπ) β {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))} β§ ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (π΄ β {π}))) β {π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))}) β ((πβπ) β© ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (π΄ β {π})))) β ({π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))} β© {π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))})) |
130 | 48, 128, 129 | syl2anc 585 |
. . 3
β’ ((π β§ π β π΄) β ((πβπ) β© ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (π΄ β {π})))) β ({π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))} β© {π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))})) |
131 | | eqid 2737 |
. . . . 5
β’ {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))} = {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))} |
132 | | eqid 2737 |
. . . . 5
β’ {π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))} = {π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))} |
133 | 68 | simp2d 1144 |
. . . . 5
β’ ((π β§ π β π΄) β ((πβ(π pCnt (β―βπ΅))) gcd ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))) = 1) |
134 | | eqid 2737 |
. . . . 5
β’
(LSSumβπΊ) =
(LSSumβπΊ) |
135 | 15, 26, 131, 132, 49, 70, 98, 133, 95, 2, 134 | ablfacrp 19852 |
. . . 4
β’ ((π β§ π β π΄) β (({π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))} β© {π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))}) = {(0gβπΊ)} β§ ({π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))} (LSSumβπΊ){π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))}) = π΅)) |
136 | 135 | simpld 496 |
. . 3
β’ ((π β§ π β π΄) β ({π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))} β© {π₯ β π΅ β£ (πβπ₯) β₯ ((β―βπ΅) / (πβ(π pCnt (β―βπ΅))))}) = {(0gβπΊ)}) |
137 | 130, 136 | sseqtrd 3989 |
. 2
β’ ((π β§ π β π΄) β ((πβπ) β© ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (π΄ β {π})))) β
{(0gβπΊ)}) |
138 | 1, 2, 3, 6, 10, 30, 37, 137 | dmdprdd 19785 |
1
β’ (π β πΊdom DProd π) |