Metamath Proof Explorer


Theorem sylow3lem3

Description: Lemma for sylow3 , first part. The number of Sylow subgroups is the same as the index (number of cosets) of the normalizer of the Sylow subgroup K . (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 sylow3lem3 φ P pSyl G = X / G ~ QG N

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 pwfi X Fin 𝒫 X Fin
12 3 11 sylib φ 𝒫 X Fin
13 slwsubg x P pSyl G x SubGrp G
14 1 subgss x SubGrp G x X
15 13 14 syl x P pSyl G x X
16 13 15 elpwd x P pSyl G x 𝒫 X
17 16 ssriv P pSyl G 𝒫 X
18 ssfi 𝒫 X Fin P pSyl G 𝒫 X P pSyl G Fin
19 12 17 18 sylancl φ P pSyl G Fin
20 hashcl P pSyl G Fin P pSyl G 0
21 19 20 syl φ P pSyl G 0
22 21 nn0cnd φ P pSyl G
23 10 1 5 nmzsubg G Grp N SubGrp G
24 eqid G ~ QG N = G ~ QG N
25 1 24 eqger N SubGrp G G ~ QG N Er X
26 2 23 25 3syl φ G ~ QG N Er X
27 26 qsss φ X / G ~ QG N 𝒫 X
28 12 27 ssfid φ X / G ~ QG N Fin
29 hashcl X / G ~ QG N Fin X / G ~ QG N 0
30 28 29 syl φ X / G ~ QG N 0
31 30 nn0cnd φ X / G ~ QG N
32 2 23 syl φ N SubGrp G
33 eqid 0 G = 0 G
34 33 subg0cl N SubGrp G 0 G N
35 ne0i 0 G N N
36 32 34 35 3syl φ N
37 1 subgss N SubGrp G N X
38 2 23 37 3syl φ N X
39 3 38 ssfid φ N Fin
40 hashnncl N Fin N N
41 39 40 syl φ N N
42 36 41 mpbird φ N
43 42 nncnd φ N
44 42 nnne0d φ N 0
45 1 2 3 4 5 6 7 sylow3lem1 φ ˙ G GrpAct P pSyl G
46 eqid G ~ QG H = G ~ QG H
47 eqid x y | x y P pSyl G g X g ˙ x = y = x y | x y P pSyl G g X g ˙ x = y
48 1 9 46 47 orbsta2 ˙ G GrpAct P pSyl G K P pSyl G X Fin X = K x y | x y P pSyl G g X g ˙ x = y H
49 45 8 3 48 syl21anc φ X = K x y | x y P pSyl G g X g ˙ x = y H
50 1 24 32 3 lagsubg2 φ X = X / G ~ QG N N
51 47 1 gaorber ˙ G GrpAct P pSyl G x y | x y P pSyl G g X g ˙ x = y Er P pSyl G
52 45 51 syl φ x y | x y P pSyl G g X g ˙ x = y Er P pSyl G
53 52 ecss φ K x y | x y P pSyl G g X g ˙ x = y P pSyl G
54 8 adantr φ h P pSyl G K P pSyl G
55 simpr φ h P pSyl G h P pSyl G
56 3 adantr φ h P pSyl G X Fin
57 1 56 55 54 5 6 sylow2 φ h P pSyl G u X h = ran z K u + ˙ z - ˙ u
58 eqcom u ˙ K = h h = u ˙ K
59 simpr φ h P pSyl G u X u X
60 54 adantr φ h P pSyl G u X K P pSyl G
61 mptexg K P pSyl G z K u + ˙ z - ˙ u V
62 rnexg z K u + ˙ z - ˙ u V ran z K u + ˙ z - ˙ u V
63 60 61 62 3syl φ h P pSyl G u X ran z K u + ˙ z - ˙ u V
64 simpr x = u y = K y = K
65 simpl x = u y = K x = u
66 65 oveq1d x = u y = K x + ˙ z = u + ˙ z
67 66 65 oveq12d x = u y = K x + ˙ z - ˙ x = u + ˙ z - ˙ u
68 64 67 mpteq12dv x = u y = K z y x + ˙ z - ˙ x = z K u + ˙ z - ˙ u
69 68 rneqd x = u y = K ran z y x + ˙ z - ˙ x = ran z K u + ˙ z - ˙ u
70 69 7 ovmpoga u X K P pSyl G ran z K u + ˙ z - ˙ u V u ˙ K = ran z K u + ˙ z - ˙ u
71 59 60 63 70 syl3anc φ h P pSyl G u X u ˙ K = ran z K u + ˙ z - ˙ u
72 71 eqeq2d φ h P pSyl G u X h = u ˙ K h = ran z K u + ˙ z - ˙ u
73 58 72 syl5bb φ h P pSyl G u X u ˙ K = h h = ran z K u + ˙ z - ˙ u
74 73 rexbidva φ h P pSyl G u X u ˙ K = h u X h = ran z K u + ˙ z - ˙ u
75 57 74 mpbird φ h P pSyl G u X u ˙ K = h
76 47 gaorb K x y | x y P pSyl G g X g ˙ x = y h K P pSyl G h P pSyl G u X u ˙ K = h
77 54 55 75 76 syl3anbrc φ h P pSyl G K x y | x y P pSyl G g X g ˙ x = y h
78 elecg h P pSyl G K P pSyl G h K x y | x y P pSyl G g X g ˙ x = y K x y | x y P pSyl G g X g ˙ x = y h
79 55 54 78 syl2anc φ h P pSyl G h K x y | x y P pSyl G g X g ˙ x = y K x y | x y P pSyl G g X g ˙ x = y h
80 77 79 mpbird φ h P pSyl G h K x y | x y P pSyl G g X g ˙ x = y
81 53 80 eqelssd φ K x y | x y P pSyl G g X g ˙ x = y = P pSyl G
82 81 fveq2d φ K x y | x y P pSyl G g X g ˙ x = y = P pSyl G
83 1 2 3 4 5 6 7 8 9 10 sylow3lem2 φ H = N
84 83 fveq2d φ H = N
85 82 84 oveq12d φ K x y | x y P pSyl G g X g ˙ x = y H = P pSyl G N
86 49 50 85 3eqtr3rd φ P pSyl G N = X / G ~ QG N N
87 22 31 43 44 86 mulcan2ad φ P pSyl G = X / G ~ QG N