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 
|- ( ph -> G e. Grp )
sylow1.f 
|- ( ph -> X e. Fin )
sylow1.p 
|- ( ph -> P e. Prime )
sylow1.n 
|- ( ph -> N e. NN0 )
sylow1.d 
|- ( ph -> ( P ^ N ) || ( # ` X ) )
sylow1lem.a 
|- .+ = ( +g ` G )
sylow1lem.s 
|- S = { s e. ~P X | ( # ` s ) = ( P ^ N ) }
sylow1lem.m 
|- .(+) = ( x e. X , y e. S |-> ran ( z e. y |-> ( x .+ z ) ) )
sylow1lem3.1 
|- .~ = { <. x , y >. | ( { x , y } C_ S /\ E. g e. X ( g .(+) x ) = y ) }
sylow1lem4.b 
|- ( ph -> B e. S )
sylow1lem4.h 
|- H = { u e. X | ( u .(+) B ) = B }
Assertion sylow1lem4 
|- ( ph -> ( # ` H ) <_ ( P ^ N ) )

Proof

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