Metamath Proof Explorer


Theorem sylow1lem4

Description: Lemma for sylow1 . The stabilizer subgroup of any element of S is at most P ^ N in size. (Contributed by Mario Carneiro, 15-Jan-2015)

Ref Expression
Hypotheses sylow1.x X = Base G
sylow1.g φ G Grp
sylow1.f φ X Fin
sylow1.p φ P
sylow1.n φ N 0
sylow1.d φ P N X
sylow1lem.a + ˙ = + G
sylow1lem.s S = s 𝒫 X | s = P N
sylow1lem.m ˙ = x X , y S ran z y x + ˙ z
sylow1lem3.1 ˙ = x y | x y S g X g ˙ x = y
sylow1lem4.b φ B S
sylow1lem4.h H = u X | u ˙ B = B
Assertion sylow1lem4 φ H P N

Proof

Step Hyp Ref Expression
1 sylow1.x X = Base G
2 sylow1.g φ G Grp
3 sylow1.f φ X Fin
4 sylow1.p φ P
5 sylow1.n φ N 0
6 sylow1.d φ P N X
7 sylow1lem.a + ˙ = + G
8 sylow1lem.s S = s 𝒫 X | s = P N
9 sylow1lem.m ˙ = x X , y S ran z y x + ˙ z
10 sylow1lem3.1 ˙ = x y | x y S g X g ˙ x = y
11 sylow1lem4.b φ B S
12 sylow1lem4.h H = u X | u ˙ B = B
13 fveqeq2 s = B s = P N B = P N
14 13 8 elrab2 B S B 𝒫 X B = P N
15 11 14 sylib φ B 𝒫 X B = P N
16 15 simprd φ B = P N
17 prmnn P P
18 4 17 syl φ P
19 18 5 nnexpcld φ P N
20 16 19 eqeltrd φ B
21 20 nnne0d φ B 0
22 hasheq0 B S B = 0 B =
23 22 necon3bid B S B 0 B
24 11 23 syl φ B 0 B
25 21 24 mpbid φ B
26 n0 B a a B
27 25 26 sylib φ a a B
28 11 adantr φ a B B S
29 simplr φ a B b H a B
30 oveq2 z = a b + ˙ z = b + ˙ a
31 eqid z B b + ˙ z = z B b + ˙ z
32 ovex b + ˙ a V
33 30 31 32 fvmpt a B z B b + ˙ z a = b + ˙ a
34 29 33 syl φ a B b H z B b + ˙ z a = b + ˙ a
35 ovex b + ˙ z V
36 35 31 fnmpti z B b + ˙ z Fn B
37 fnfvelrn z B b + ˙ z Fn B a B z B b + ˙ z a ran z B b + ˙ z
38 36 29 37 sylancr φ a B b H z B b + ˙ z a ran z B b + ˙ z
39 34 38 eqeltrrd φ a B b H b + ˙ a ran z B b + ˙ z
40 12 ssrab3 H X
41 simpr φ a B b H b H
42 40 41 sselid φ a B b H b X
43 11 ad2antrr φ a B b H B S
44 mptexg B S z B b + ˙ z V
45 rnexg z B b + ˙ z V ran z B b + ˙ z V
46 43 44 45 3syl φ a B b H ran z B b + ˙ z V
47 simpr x = b y = B y = B
48 simpl x = b y = B x = b
49 48 oveq1d x = b y = B x + ˙ z = b + ˙ z
50 47 49 mpteq12dv x = b y = B z y x + ˙ z = z B b + ˙ z
51 50 rneqd x = b y = B ran z y x + ˙ z = ran z B b + ˙ z
52 51 9 ovmpoga b X B S ran z B b + ˙ z V b ˙ B = ran z B b + ˙ z
53 42 43 46 52 syl3anc φ a B b H b ˙ B = ran z B b + ˙ z
54 39 53 eleqtrrd φ a B b H b + ˙ a b ˙ B
55 oveq1 u = b u ˙ B = b ˙ B
56 55 eqeq1d u = b u ˙ B = B b ˙ B = B
57 56 12 elrab2 b H b X b ˙ B = B
58 57 simprbi b H b ˙ B = B
59 58 adantl φ a B b H b ˙ B = B
60 54 59 eleqtrd φ a B b H b + ˙ a B
61 60 ex φ a B b H b + ˙ a B
62 2 ad2antrr φ a B b H c H G Grp
63 simprl φ a B b H c H b H
64 40 63 sselid φ a B b H c H b X
65 simprr φ a B b H c H c H
66 40 65 sselid φ a B b H c H c X
67 15 simpld φ B 𝒫 X
68 67 elpwid φ B X
69 68 sselda φ a B a X
70 69 adantr φ a B b H c H a X
71 1 7 grprcan G Grp b X c X a X b + ˙ a = c + ˙ a b = c
72 62 64 66 70 71 syl13anc φ a B b H c H b + ˙ a = c + ˙ a b = c
73 72 ex φ a B b H c H b + ˙ a = c + ˙ a b = c
74 61 73 dom2d φ a B B S H B
75 28 74 mpd φ a B H B
76 27 75 exlimddv φ H B
77 ssfi X Fin H X H Fin
78 3 40 77 sylancl φ H Fin
79 3 68 ssfid φ B Fin
80 hashdom H Fin B Fin H B H B
81 78 79 80 syl2anc φ H B H B
82 76 81 mpbird φ H B
83 82 16 breqtrd φ H P N