Step | Hyp | Ref
| Expression |
1 | | fislw.1 |
. . 3
β’ π = (BaseβπΊ) |
2 | | slwhash.4 |
. . . . 5
β’ (π β π» β (π pSyl πΊ)) |
3 | | slwsubg 19477 |
. . . . 5
β’ (π» β (π pSyl πΊ) β π» β (SubGrpβπΊ)) |
4 | 2, 3 | syl 17 |
. . . 4
β’ (π β π» β (SubGrpβπΊ)) |
5 | | subgrcl 19010 |
. . . 4
β’ (π» β (SubGrpβπΊ) β πΊ β Grp) |
6 | 4, 5 | syl 17 |
. . 3
β’ (π β πΊ β Grp) |
7 | | slwhash.3 |
. . 3
β’ (π β π β Fin) |
8 | | slwprm 19476 |
. . . 4
β’ (π» β (π pSyl πΊ) β π β β) |
9 | 2, 8 | syl 17 |
. . 3
β’ (π β π β β) |
10 | 1 | grpbn0 18850 |
. . . . . 6
β’ (πΊ β Grp β π β β
) |
11 | 6, 10 | syl 17 |
. . . . 5
β’ (π β π β β
) |
12 | | hashnncl 14325 |
. . . . . 6
β’ (π β Fin β
((β―βπ) β
β β π β
β
)) |
13 | 7, 12 | syl 17 |
. . . . 5
β’ (π β ((β―βπ) β β β π β β
)) |
14 | 11, 13 | mpbird 256 |
. . . 4
β’ (π β (β―βπ) β
β) |
15 | 9, 14 | pccld 16782 |
. . 3
β’ (π β (π pCnt (β―βπ)) β
β0) |
16 | | pcdvds 16796 |
. . . 4
β’ ((π β β β§
(β―βπ) β
β) β (πβ(π pCnt (β―βπ))) β₯ (β―βπ)) |
17 | 9, 14, 16 | syl2anc 584 |
. . 3
β’ (π β (πβ(π pCnt (β―βπ))) β₯ (β―βπ)) |
18 | 1, 6, 7, 9, 15, 17 | sylow1 19470 |
. 2
β’ (π β βπ β (SubGrpβπΊ)(β―βπ) = (πβ(π pCnt (β―βπ)))) |
19 | 7 | adantr 481 |
. . . 4
β’ ((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β π β Fin) |
20 | 4 | adantr 481 |
. . . 4
β’ ((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β π» β (SubGrpβπΊ)) |
21 | | simprl 769 |
. . . 4
β’ ((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β π β (SubGrpβπΊ)) |
22 | | eqid 2732 |
. . . 4
β’
(+gβπΊ) = (+gβπΊ) |
23 | | eqid 2732 |
. . . . . . 7
β’ (πΊ βΎs π») = (πΊ βΎs π») |
24 | 23 | slwpgp 19480 |
. . . . . 6
β’ (π» β (π pSyl πΊ) β π pGrp (πΊ βΎs π»)) |
25 | 2, 24 | syl 17 |
. . . . 5
β’ (π β π pGrp (πΊ βΎs π»)) |
26 | 25 | adantr 481 |
. . . 4
β’ ((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β π pGrp (πΊ βΎs π»)) |
27 | | simprr 771 |
. . . 4
β’ ((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β (β―βπ) = (πβ(π pCnt (β―βπ)))) |
28 | | eqid 2732 |
. . . 4
β’
(-gβπΊ) = (-gβπΊ) |
29 | 1, 19, 20, 21, 22, 26, 27, 28 | sylow2b 19490 |
. . 3
β’ ((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β βπ β π π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))) |
30 | | simprr 771 |
. . . . . 6
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))) |
31 | 2 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β π» β (π pSyl πΊ)) |
32 | 31, 8 | syl 17 |
. . . . . . 7
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β π β β) |
33 | 15 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β (π pCnt (β―βπ)) β
β0) |
34 | 21 | adantr 481 |
. . . . . . . . . . . 12
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β π β (SubGrpβπΊ)) |
35 | | simprl 769 |
. . . . . . . . . . . 12
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β π β π) |
36 | | eqid 2732 |
. . . . . . . . . . . . 13
β’ (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)) = (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)) |
37 | 1, 22, 28, 36 | conjsubg 19123 |
. . . . . . . . . . . 12
β’ ((π β (SubGrpβπΊ) β§ π β π) β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)) β (SubGrpβπΊ)) |
38 | 34, 35, 37 | syl2anc 584 |
. . . . . . . . . . 11
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)) β (SubGrpβπΊ)) |
39 | | eqid 2732 |
. . . . . . . . . . . 12
β’ (πΊ βΎs ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))) = (πΊ βΎs ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))) |
40 | 39 | subgbas 19009 |
. . . . . . . . . . 11
β’ (ran
(π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)) β (SubGrpβπΊ) β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)) = (Baseβ(πΊ βΎs ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))))) |
41 | 38, 40 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)) = (Baseβ(πΊ βΎs ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))))) |
42 | 41 | fveq2d 6895 |
. . . . . . . . 9
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β (β―βran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))) = (β―β(Baseβ(πΊ βΎs ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))))) |
43 | 1, 22, 28, 36 | conjsubgen 19124 |
. . . . . . . . . . . 12
β’ ((π β (SubGrpβπΊ) β§ π β π) β π β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))) |
44 | 34, 35, 43 | syl2anc 584 |
. . . . . . . . . . 11
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β π β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))) |
45 | 7 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β π β Fin) |
46 | 1 | subgss 19006 |
. . . . . . . . . . . . . 14
β’ (π β (SubGrpβπΊ) β π β π) |
47 | 34, 46 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β π β π) |
48 | 45, 47 | ssfid 9266 |
. . . . . . . . . . . 12
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β π β Fin) |
49 | 1 | subgss 19006 |
. . . . . . . . . . . . . 14
β’ (ran
(π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)) β (SubGrpβπΊ) β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)) β π) |
50 | 38, 49 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)) β π) |
51 | 45, 50 | ssfid 9266 |
. . . . . . . . . . . 12
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)) β Fin) |
52 | | hashen 14306 |
. . . . . . . . . . . 12
β’ ((π β Fin β§ ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)) β Fin) β ((β―βπ) = (β―βran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))) β π β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) |
53 | 48, 51, 52 | syl2anc 584 |
. . . . . . . . . . 11
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β ((β―βπ) = (β―βran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))) β π β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) |
54 | 44, 53 | mpbird 256 |
. . . . . . . . . 10
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β (β―βπ) = (β―βran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) |
55 | | simplrr 776 |
. . . . . . . . . 10
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β (β―βπ) = (πβ(π pCnt (β―βπ)))) |
56 | 54, 55 | eqtr3d 2774 |
. . . . . . . . 9
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β (β―βran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))) = (πβ(π pCnt (β―βπ)))) |
57 | 42, 56 | eqtr3d 2774 |
. . . . . . . 8
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β (β―β(Baseβ(πΊ βΎs ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))))) = (πβ(π pCnt (β―βπ)))) |
58 | | oveq2 7416 |
. . . . . . . . 9
β’ (π = (π pCnt (β―βπ)) β (πβπ) = (πβ(π pCnt (β―βπ)))) |
59 | 58 | rspceeqv 3633 |
. . . . . . . 8
β’ (((π pCnt (β―βπ)) β β0
β§ (β―β(Baseβ(πΊ βΎs ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))))) = (πβ(π pCnt (β―βπ)))) β βπ β β0
(β―β(Baseβ(πΊ βΎs ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))))) = (πβπ)) |
60 | 33, 57, 59 | syl2anc 584 |
. . . . . . 7
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β βπ β β0
(β―β(Baseβ(πΊ βΎs ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))))) = (πβπ)) |
61 | 39 | subggrp 19008 |
. . . . . . . . 9
β’ (ran
(π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)) β (SubGrpβπΊ) β (πΊ βΎs ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))) β Grp) |
62 | 38, 61 | syl 17 |
. . . . . . . 8
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β (πΊ βΎs ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))) β Grp) |
63 | 41, 51 | eqeltrrd 2834 |
. . . . . . . 8
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β (Baseβ(πΊ βΎs ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β Fin) |
64 | | eqid 2732 |
. . . . . . . . 9
β’
(Baseβ(πΊ
βΎs ran (π₯
β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) = (Baseβ(πΊ βΎs ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) |
65 | 64 | pgpfi 19472 |
. . . . . . . 8
β’ (((πΊ βΎs ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))) β Grp β§ (Baseβ(πΊ βΎs ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β Fin) β (π pGrp (πΊ βΎs ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))) β (π β β β§ βπ β β0
(β―β(Baseβ(πΊ βΎs ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))))) = (πβπ)))) |
66 | 62, 63, 65 | syl2anc 584 |
. . . . . . 7
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β (π pGrp (πΊ βΎs ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))) β (π β β β§ βπ β β0
(β―β(Baseβ(πΊ βΎs ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))))) = (πβπ)))) |
67 | 32, 60, 66 | mpbir2and 711 |
. . . . . 6
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β π pGrp (πΊ βΎs ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) |
68 | 39 | slwispgp 19478 |
. . . . . . 7
β’ ((π» β (π pSyl πΊ) β§ ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)) β (SubGrpβπΊ)) β ((π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)) β§ π pGrp (πΊ βΎs ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β π» = ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) |
69 | 31, 38, 68 | syl2anc 584 |
. . . . . 6
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β ((π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)) β§ π pGrp (πΊ βΎs ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β π» = ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) |
70 | 30, 67, 69 | mpbi2and 710 |
. . . . 5
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β π» = ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π))) |
71 | 70 | fveq2d 6895 |
. . . 4
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β (β―βπ») = (β―βran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) |
72 | 71, 56 | eqtrd 2772 |
. . 3
β’ (((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β§ (π β π β§ π» β ran (π₯ β π β¦ ((π(+gβπΊ)π₯)(-gβπΊ)π)))) β (β―βπ») = (πβ(π pCnt (β―βπ)))) |
73 | 29, 72 | rexlimddv 3161 |
. 2
β’ ((π β§ (π β (SubGrpβπΊ) β§ (β―βπ) = (πβ(π pCnt (β―βπ))))) β (β―βπ») = (πβ(π pCnt (β―βπ)))) |
74 | 18, 73 | rexlimddv 3161 |
1
β’ (π β (β―βπ») = (πβ(π pCnt (β―βπ)))) |