Step | Hyp | Ref
| Expression |
1 | | sylow3.x |
. . 3
โข ๐ = (Baseโ๐บ) |
2 | | sylow3.g |
. . 3
โข (๐ โ ๐บ โ Grp) |
3 | | sylow3.xf |
. . 3
โข (๐ โ ๐ โ Fin) |
4 | | sylow3.p |
. . 3
โข (๐ โ ๐ โ โ) |
5 | | sylow3lem1.a |
. . 3
โข + =
(+gโ๐บ) |
6 | | sylow3lem1.d |
. . 3
โข โ =
(-gโ๐บ) |
7 | | sylow3lem1.m |
. . 3
โข โ =
(๐ฅ โ ๐, ๐ฆ โ (๐ pSyl ๐บ) โฆ ran (๐ง โ ๐ฆ โฆ ((๐ฅ + ๐ง) โ ๐ฅ))) |
8 | | sylow3lem2.k |
. . 3
โข (๐ โ ๐พ โ (๐ pSyl ๐บ)) |
9 | | sylow3lem2.h |
. . 3
โข ๐ป = {๐ข โ ๐ โฃ (๐ข โ ๐พ) = ๐พ} |
10 | | sylow3lem2.n |
. . 3
โข ๐ = {๐ฅ โ ๐ โฃ โ๐ฆ โ ๐ ((๐ฅ + ๐ฆ) โ ๐พ โ (๐ฆ + ๐ฅ) โ ๐พ)} |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | sylow3lem3 19491 |
. 2
โข (๐ โ (โฏโ(๐ pSyl ๐บ)) = (โฏโ(๐ / (๐บ ~QG ๐)))) |
12 | | slwsubg 19472 |
. . . . . . . . . 10
โข (๐พ โ (๐ pSyl ๐บ) โ ๐พ โ (SubGrpโ๐บ)) |
13 | 8, 12 | syl 17 |
. . . . . . . . 9
โข (๐ โ ๐พ โ (SubGrpโ๐บ)) |
14 | | eqid 2732 |
. . . . . . . . . . 11
โข (๐บ โพs ๐) = (๐บ โพs ๐) |
15 | 10, 1, 5, 14 | nmznsg 19042 |
. . . . . . . . . 10
โข (๐พ โ (SubGrpโ๐บ) โ ๐พ โ (NrmSGrpโ(๐บ โพs ๐))) |
16 | | nsgsubg 19032 |
. . . . . . . . . 10
โข (๐พ โ (NrmSGrpโ(๐บ โพs ๐)) โ ๐พ โ (SubGrpโ(๐บ โพs ๐))) |
17 | 15, 16 | syl 17 |
. . . . . . . . 9
โข (๐พ โ (SubGrpโ๐บ) โ ๐พ โ (SubGrpโ(๐บ โพs ๐))) |
18 | 13, 17 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐พ โ (SubGrpโ(๐บ โพs ๐))) |
19 | 10, 1, 5 | nmzsubg 19039 |
. . . . . . . . . . 11
โข (๐บ โ Grp โ ๐ โ (SubGrpโ๐บ)) |
20 | 2, 19 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ๐ โ (SubGrpโ๐บ)) |
21 | 14 | subgbas 19004 |
. . . . . . . . . 10
โข (๐ โ (SubGrpโ๐บ) โ ๐ = (Baseโ(๐บ โพs ๐))) |
22 | 20, 21 | syl 17 |
. . . . . . . . 9
โข (๐ โ ๐ = (Baseโ(๐บ โพs ๐))) |
23 | 1 | subgss 19001 |
. . . . . . . . . . 11
โข (๐ โ (SubGrpโ๐บ) โ ๐ โ ๐) |
24 | 20, 23 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ๐ โ ๐) |
25 | 3, 24 | ssfid 9263 |
. . . . . . . . 9
โข (๐ โ ๐ โ Fin) |
26 | 22, 25 | eqeltrrd 2834 |
. . . . . . . 8
โข (๐ โ (Baseโ(๐บ โพs ๐)) โ Fin) |
27 | | eqid 2732 |
. . . . . . . . 9
โข
(Baseโ(๐บ
โพs ๐)) =
(Baseโ(๐บ
โพs ๐)) |
28 | 27 | lagsubg 19066 |
. . . . . . . 8
โข ((๐พ โ (SubGrpโ(๐บ โพs ๐)) โง (Baseโ(๐บ โพs ๐)) โ Fin) โ
(โฏโ๐พ) โฅ
(โฏโ(Baseโ(๐บ โพs ๐)))) |
29 | 18, 26, 28 | syl2anc 584 |
. . . . . . 7
โข (๐ โ (โฏโ๐พ) โฅ
(โฏโ(Baseโ(๐บ โพs ๐)))) |
30 | 22 | fveq2d 6892 |
. . . . . . 7
โข (๐ โ (โฏโ๐) =
(โฏโ(Baseโ(๐บ โพs ๐)))) |
31 | 29, 30 | breqtrrd 5175 |
. . . . . 6
โข (๐ โ (โฏโ๐พ) โฅ (โฏโ๐)) |
32 | | eqid 2732 |
. . . . . . . . . . . 12
โข
(0gโ๐บ) = (0gโ๐บ) |
33 | 32 | subg0cl 19008 |
. . . . . . . . . . 11
โข (๐พ โ (SubGrpโ๐บ) โ
(0gโ๐บ)
โ ๐พ) |
34 | 13, 33 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (0gโ๐บ) โ ๐พ) |
35 | 34 | ne0d 4334 |
. . . . . . . . 9
โข (๐ โ ๐พ โ โ
) |
36 | 1 | subgss 19001 |
. . . . . . . . . . . 12
โข (๐พ โ (SubGrpโ๐บ) โ ๐พ โ ๐) |
37 | 13, 36 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ๐พ โ ๐) |
38 | 3, 37 | ssfid 9263 |
. . . . . . . . . 10
โข (๐ โ ๐พ โ Fin) |
39 | | hashnncl 14322 |
. . . . . . . . . 10
โข (๐พ โ Fin โ
((โฏโ๐พ) โ
โ โ ๐พ โ
โ
)) |
40 | 38, 39 | syl 17 |
. . . . . . . . 9
โข (๐ โ ((โฏโ๐พ) โ โ โ ๐พ โ โ
)) |
41 | 35, 40 | mpbird 256 |
. . . . . . . 8
โข (๐ โ (โฏโ๐พ) โ
โ) |
42 | 41 | nnzd 12581 |
. . . . . . 7
โข (๐ โ (โฏโ๐พ) โ
โค) |
43 | | hashcl 14312 |
. . . . . . . . 9
โข (๐ โ Fin โ
(โฏโ๐) โ
โ0) |
44 | 25, 43 | syl 17 |
. . . . . . . 8
โข (๐ โ (โฏโ๐) โ
โ0) |
45 | 44 | nn0zd 12580 |
. . . . . . 7
โข (๐ โ (โฏโ๐) โ
โค) |
46 | | pwfi 9174 |
. . . . . . . . . . 11
โข (๐ โ Fin โ ๐ซ
๐ โ
Fin) |
47 | 3, 46 | sylib 217 |
. . . . . . . . . 10
โข (๐ โ ๐ซ ๐ โ Fin) |
48 | | eqid 2732 |
. . . . . . . . . . . . 13
โข (๐บ ~QG ๐) = (๐บ ~QG ๐) |
49 | 1, 48 | eqger 19052 |
. . . . . . . . . . . 12
โข (๐ โ (SubGrpโ๐บ) โ (๐บ ~QG ๐) Er ๐) |
50 | 20, 49 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (๐บ ~QG ๐) Er ๐) |
51 | 50 | qsss 8768 |
. . . . . . . . . 10
โข (๐ โ (๐ / (๐บ ~QG ๐)) โ ๐ซ ๐) |
52 | 47, 51 | ssfid 9263 |
. . . . . . . . 9
โข (๐ โ (๐ / (๐บ ~QG ๐)) โ Fin) |
53 | | hashcl 14312 |
. . . . . . . . 9
โข ((๐ / (๐บ ~QG ๐)) โ Fin โ (โฏโ(๐ / (๐บ ~QG ๐))) โ
โ0) |
54 | 52, 53 | syl 17 |
. . . . . . . 8
โข (๐ โ (โฏโ(๐ / (๐บ ~QG ๐))) โ
โ0) |
55 | 54 | nn0zd 12580 |
. . . . . . 7
โข (๐ โ (โฏโ(๐ / (๐บ ~QG ๐))) โ โค) |
56 | | dvdscmul 16222 |
. . . . . . 7
โข
(((โฏโ๐พ)
โ โค โง (โฏโ๐) โ โค โง (โฏโ(๐ / (๐บ ~QG ๐))) โ โค) โ
((โฏโ๐พ) โฅ
(โฏโ๐) โ
((โฏโ(๐ /
(๐บ ~QG
๐))) ยท
(โฏโ๐พ)) โฅ
((โฏโ(๐ /
(๐บ ~QG
๐))) ยท
(โฏโ๐)))) |
57 | 42, 45, 55, 56 | syl3anc 1371 |
. . . . . 6
โข (๐ โ ((โฏโ๐พ) โฅ (โฏโ๐) โ ((โฏโ(๐ / (๐บ ~QG ๐))) ยท (โฏโ๐พ)) โฅ
((โฏโ(๐ /
(๐บ ~QG
๐))) ยท
(โฏโ๐)))) |
58 | 31, 57 | mpd 15 |
. . . . 5
โข (๐ โ ((โฏโ(๐ / (๐บ ~QG ๐))) ยท (โฏโ๐พ)) โฅ
((โฏโ(๐ /
(๐บ ~QG
๐))) ยท
(โฏโ๐))) |
59 | | hashcl 14312 |
. . . . . . . . 9
โข (๐ โ Fin โ
(โฏโ๐) โ
โ0) |
60 | 3, 59 | syl 17 |
. . . . . . . 8
โข (๐ โ (โฏโ๐) โ
โ0) |
61 | 60 | nn0cnd 12530 |
. . . . . . 7
โข (๐ โ (โฏโ๐) โ
โ) |
62 | 41 | nncnd 12224 |
. . . . . . 7
โข (๐ โ (โฏโ๐พ) โ
โ) |
63 | 41 | nnne0d 12258 |
. . . . . . 7
โข (๐ โ (โฏโ๐พ) โ 0) |
64 | 61, 62, 63 | divcan1d 11987 |
. . . . . 6
โข (๐ โ (((โฏโ๐) / (โฏโ๐พ)) ยท (โฏโ๐พ)) = (โฏโ๐)) |
65 | 1, 48, 20, 3 | lagsubg2 19065 |
. . . . . 6
โข (๐ โ (โฏโ๐) = ((โฏโ(๐ / (๐บ ~QG ๐))) ยท (โฏโ๐))) |
66 | 64, 65 | eqtrd 2772 |
. . . . 5
โข (๐ โ (((โฏโ๐) / (โฏโ๐พ)) ยท (โฏโ๐พ)) = ((โฏโ(๐ / (๐บ ~QG ๐))) ยท (โฏโ๐))) |
67 | 58, 66 | breqtrrd 5175 |
. . . 4
โข (๐ โ ((โฏโ(๐ / (๐บ ~QG ๐))) ยท (โฏโ๐พ)) โฅ
(((โฏโ๐) /
(โฏโ๐พ)) ยท
(โฏโ๐พ))) |
68 | 1 | lagsubg 19066 |
. . . . . . 7
โข ((๐พ โ (SubGrpโ๐บ) โง ๐ โ Fin) โ (โฏโ๐พ) โฅ (โฏโ๐)) |
69 | 13, 3, 68 | syl2anc 584 |
. . . . . 6
โข (๐ โ (โฏโ๐พ) โฅ (โฏโ๐)) |
70 | 60 | nn0zd 12580 |
. . . . . . 7
โข (๐ โ (โฏโ๐) โ
โค) |
71 | | dvdsval2 16196 |
. . . . . . 7
โข
(((โฏโ๐พ)
โ โค โง (โฏโ๐พ) โ 0 โง (โฏโ๐) โ โค) โ
((โฏโ๐พ) โฅ
(โฏโ๐) โ
((โฏโ๐) /
(โฏโ๐พ)) โ
โค)) |
72 | 42, 63, 70, 71 | syl3anc 1371 |
. . . . . 6
โข (๐ โ ((โฏโ๐พ) โฅ (โฏโ๐) โ ((โฏโ๐) / (โฏโ๐พ)) โ
โค)) |
73 | 69, 72 | mpbid 231 |
. . . . 5
โข (๐ โ ((โฏโ๐) / (โฏโ๐พ)) โ
โค) |
74 | | dvdsmulcr 16225 |
. . . . 5
โข
(((โฏโ(๐
/ (๐บ
~QG ๐)))
โ โค โง ((โฏโ๐) / (โฏโ๐พ)) โ โค โง
((โฏโ๐พ) โ
โค โง (โฏโ๐พ) โ 0)) โ (((โฏโ(๐ / (๐บ ~QG ๐))) ยท (โฏโ๐พ)) โฅ
(((โฏโ๐) /
(โฏโ๐พ)) ยท
(โฏโ๐พ)) โ
(โฏโ(๐ /
(๐บ ~QG
๐))) โฅ
((โฏโ๐) /
(โฏโ๐พ)))) |
75 | 55, 73, 42, 63, 74 | syl112anc 1374 |
. . . 4
โข (๐ โ (((โฏโ(๐ / (๐บ ~QG ๐))) ยท (โฏโ๐พ)) โฅ
(((โฏโ๐) /
(โฏโ๐พ)) ยท
(โฏโ๐พ)) โ
(โฏโ(๐ /
(๐บ ~QG
๐))) โฅ
((โฏโ๐) /
(โฏโ๐พ)))) |
76 | 67, 75 | mpbid 231 |
. . 3
โข (๐ โ (โฏโ(๐ / (๐บ ~QG ๐))) โฅ ((โฏโ๐) / (โฏโ๐พ))) |
77 | 1, 3, 8 | slwhash 19486 |
. . . 4
โข (๐ โ (โฏโ๐พ) = (๐โ(๐ pCnt (โฏโ๐)))) |
78 | 77 | oveq2d 7421 |
. . 3
โข (๐ โ ((โฏโ๐) / (โฏโ๐พ)) = ((โฏโ๐) / (๐โ(๐ pCnt (โฏโ๐))))) |
79 | 76, 78 | breqtrd 5173 |
. 2
โข (๐ โ (โฏโ(๐ / (๐บ ~QG ๐))) โฅ ((โฏโ๐) / (๐โ(๐ pCnt (โฏโ๐))))) |
80 | 11, 79 | eqbrtrd 5169 |
1
โข (๐ โ (โฏโ(๐ pSyl ๐บ)) โฅ ((โฏโ๐) / (๐โ(๐ pCnt (โฏโ๐))))) |