Metamath Proof Explorer


Theorem sylow3lem4

Description: Lemma for sylow3 , first part. The number of Sylow subgroups is a divisor of the size of G reduced by the size of a Sylow subgroup of G . (Contributed by Mario Carneiro, 19-Jan-2015)

Ref Expression
Hypotheses sylow3.x X = Base G
sylow3.g φ G Grp
sylow3.xf φ X Fin
sylow3.p φ P
sylow3lem1.a + ˙ = + G
sylow3lem1.d - ˙ = - G
sylow3lem1.m ˙ = x X , y P pSyl G ran z y x + ˙ z - ˙ x
sylow3lem2.k φ K P pSyl G
sylow3lem2.h H = u X | u ˙ K = K
sylow3lem2.n N = x X | y X x + ˙ y K y + ˙ x K
Assertion sylow3lem4 φ P pSyl G X P P pCnt X

Proof

Step Hyp Ref Expression
1 sylow3.x X = Base G
2 sylow3.g φ G Grp
3 sylow3.xf φ X Fin
4 sylow3.p φ P
5 sylow3lem1.a + ˙ = + G
6 sylow3lem1.d - ˙ = - G
7 sylow3lem1.m ˙ = x X , y P pSyl G ran z y x + ˙ z - ˙ x
8 sylow3lem2.k φ K P pSyl G
9 sylow3lem2.h H = u X | u ˙ K = K
10 sylow3lem2.n N = x X | y X x + ˙ y K y + ˙ x K
11 1 2 3 4 5 6 7 8 9 10 sylow3lem3 φ P pSyl G = X / G ~ QG N
12 slwsubg K P pSyl G K SubGrp G
13 8 12 syl φ K SubGrp G
14 eqid G 𝑠 N = G 𝑠 N
15 10 1 5 14 nmznsg K SubGrp G K NrmSGrp G 𝑠 N
16 nsgsubg K NrmSGrp G 𝑠 N K SubGrp G 𝑠 N
17 15 16 syl K SubGrp G K SubGrp G 𝑠 N
18 13 17 syl φ K SubGrp G 𝑠 N
19 10 1 5 nmzsubg G Grp N SubGrp G
20 2 19 syl φ N SubGrp G
21 14 subgbas N SubGrp G N = Base G 𝑠 N
22 20 21 syl φ N = Base G 𝑠 N
23 1 subgss N SubGrp G N X
24 20 23 syl φ N X
25 3 24 ssfid φ N Fin
26 22 25 eqeltrrd φ Base G 𝑠 N Fin
27 eqid Base G 𝑠 N = Base G 𝑠 N
28 27 lagsubg K SubGrp G 𝑠 N Base G 𝑠 N Fin K Base G 𝑠 N
29 18 26 28 syl2anc φ K Base G 𝑠 N
30 22 fveq2d φ N = Base G 𝑠 N
31 29 30 breqtrrd φ K N
32 eqid 0 G = 0 G
33 32 subg0cl K SubGrp G 0 G K
34 13 33 syl φ 0 G K
35 34 ne0d φ K
36 1 subgss K SubGrp G K X
37 13 36 syl φ K X
38 3 37 ssfid φ K Fin
39 hashnncl K Fin K K
40 38 39 syl φ K K
41 35 40 mpbird φ K
42 41 nnzd φ K
43 hashcl N Fin N 0
44 25 43 syl φ N 0
45 44 nn0zd φ N
46 pwfi X Fin 𝒫 X Fin
47 3 46 sylib φ 𝒫 X Fin
48 eqid G ~ QG N = G ~ QG N
49 1 48 eqger N SubGrp G G ~ QG N Er X
50 20 49 syl φ G ~ QG N Er X
51 50 qsss φ X / G ~ QG N 𝒫 X
52 47 51 ssfid φ X / G ~ QG N Fin
53 hashcl X / G ~ QG N Fin X / G ~ QG N 0
54 52 53 syl φ X / G ~ QG N 0
55 54 nn0zd φ X / G ~ QG N
56 dvdscmul K N X / G ~ QG N K N X / G ~ QG N K X / G ~ QG N N
57 42 45 55 56 syl3anc φ K N X / G ~ QG N K X / G ~ QG N N
58 31 57 mpd φ X / G ~ QG N K X / G ~ QG N N
59 hashcl X Fin X 0
60 3 59 syl φ X 0
61 60 nn0cnd φ X
62 41 nncnd φ K
63 41 nnne0d φ K 0
64 61 62 63 divcan1d φ X K K = X
65 1 48 20 3 lagsubg2 φ X = X / G ~ QG N N
66 64 65 eqtrd φ X K K = X / G ~ QG N N
67 58 66 breqtrrd φ X / G ~ QG N K X K K
68 1 lagsubg K SubGrp G X Fin K X
69 13 3 68 syl2anc φ K X
70 60 nn0zd φ X
71 dvdsval2 K K 0 X K X X K
72 42 63 70 71 syl3anc φ K X X K
73 69 72 mpbid φ X K
74 dvdsmulcr X / G ~ QG N X K K K 0 X / G ~ QG N K X K K X / G ~ QG N X K
75 55 73 42 63 74 syl112anc φ X / G ~ QG N K X K K X / G ~ QG N X K
76 67 75 mpbid φ X / G ~ QG N X K
77 1 3 8 slwhash φ K = P P pCnt X
78 77 oveq2d φ X K = X P P pCnt X
79 76 78 breqtrd φ X / G ~ QG N X P P pCnt X
80 11 79 eqbrtrd φ P pSyl G X P P pCnt X