Metamath Proof Explorer

Theorem sylow1lem5

Description: Lemma for sylow1 . Using Lagrange's theorem and the orbit-stabilizer theorem, show that there is a subgroup with size exactly P ^ N . (Contributed by Mario Carneiro, 16-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 }
sylow1lem5.l 
|- ( ph -> ( P pCnt ( # ` [ B ] .~ ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) )
Assertion sylow1lem5 
|- ( ph -> E. h e. ( SubGrp ` G ) ( # ` 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 sylow1lem5.l 
 |-  ( ph -> ( P pCnt ( # ` [ B ] .~ ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) )
14 1 2 3 4 5 6 7 8 9 sylow1lem2 
 |-  ( ph -> .(+) e. ( G GrpAct S ) )
15 1 12 gastacl 
 |-  ( ( .(+) e. ( G GrpAct S ) /\ B e. S ) -> H e. ( SubGrp ` G ) )
16 14 11 15 syl2anc 
 |-  ( ph -> H e. ( SubGrp ` G ) )
17 1 2 3 4 5 6 7 8 9 10 11 12 sylow1lem4 
 |-  ( ph -> ( # ` H ) <_ ( P ^ N ) )
18 10 1 gaorber 
 |-  ( .(+) e. ( G GrpAct S ) -> .~ Er S )
19 14 18 syl 
 |-  ( ph -> .~ Er S )
20 erdm 
 |-  ( .~ Er S -> dom .~ = S )
21 19 20 syl 
 |-  ( ph -> dom .~ = S )
22 11 21 eleqtrrd 
 |-  ( ph -> B e. dom .~ )
23 ecdmn0 
 |-  ( B e. dom .~ <-> [ B ] .~ =/= (/) )
24 22 23 sylib 
 |-  ( ph -> [ B ] .~ =/= (/) )
25 pwfi 
 |-  ( X e. Fin <-> ~P X e. Fin )
26 3 25 sylib 
 |-  ( ph -> ~P X e. Fin )
27 8 ssrab3 
 |-  S C_ ~P X
28 ssfi 
 |-  ( ( ~P X e. Fin /\ S C_ ~P X ) -> S e. Fin )
29 26 27 28 sylancl 
 |-  ( ph -> S e. Fin )
30 19 ecss 
 |-  ( ph -> [ B ] .~ C_ S )
31 29 30 ssfid 
 |-  ( ph -> [ B ] .~ e. Fin )
32 hashnncl 
 |-  ( [ B ] .~ e. Fin -> ( ( # ` [ B ] .~ ) e. NN <-> [ B ] .~ =/= (/) ) )
33 31 32 syl 
 |-  ( ph -> ( ( # ` [ B ] .~ ) e. NN <-> [ B ] .~ =/= (/) ) )
34 24 33 mpbird 
 |-  ( ph -> ( # ` [ B ] .~ ) e. NN )
35 4 34 pccld 
 |-  ( ph -> ( P pCnt ( # ` [ B ] .~ ) ) e. NN0 )
36 35 nn0red 
 |-  ( ph -> ( P pCnt ( # ` [ B ] .~ ) ) e. RR )
37 5 nn0red 
 |-  ( ph -> N e. RR )
38 1 grpbn0 
 |-  ( G e. Grp -> X =/= (/) )
39 2 38 syl 
 |-  ( ph -> X =/= (/) )
40 hashnncl 
 |-  ( X e. Fin -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
41 3 40 syl 
 |-  ( ph -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
42 39 41 mpbird 
 |-  ( ph -> ( # ` X ) e. NN )
43 4 42 pccld 
 |-  ( ph -> ( P pCnt ( # ` X ) ) e. NN0 )
44 43 nn0red 
 |-  ( ph -> ( P pCnt ( # ` X ) ) e. RR )
45 leaddsub 
 |-  ( ( ( P pCnt ( # ` [ B ] .~ ) ) e. RR /\ N e. RR /\ ( P pCnt ( # ` X ) ) e. RR ) -> ( ( ( P pCnt ( # ` [ B ] .~ ) ) + N ) <_ ( P pCnt ( # ` X ) ) <-> ( P pCnt ( # ` [ B ] .~ ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) )
46 36 37 44 45 syl3anc 
 |-  ( ph -> ( ( ( P pCnt ( # ` [ B ] .~ ) ) + N ) <_ ( P pCnt ( # ` X ) ) <-> ( P pCnt ( # ` [ B ] .~ ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) )
47 13 46 mpbird 
 |-  ( ph -> ( ( P pCnt ( # ` [ B ] .~ ) ) + N ) <_ ( P pCnt ( # ` X ) ) )
48 eqid 
 |-  ( G ~QG H ) = ( G ~QG H )
49 1 12 48 10 orbsta2 
 |-  ( ( ( .(+) e. ( G GrpAct S ) /\ B e. S ) /\ X e. Fin ) -> ( # ` X ) = ( ( # ` [ B ] .~ ) x. ( # ` H ) ) )
50 14 11 3 49 syl21anc 
 |-  ( ph -> ( # ` X ) = ( ( # ` [ B ] .~ ) x. ( # ` H ) ) )
51 50 oveq2d 
 |-  ( ph -> ( P pCnt ( # ` X ) ) = ( P pCnt ( ( # ` [ B ] .~ ) x. ( # ` H ) ) ) )
52 34 nnzd 
 |-  ( ph -> ( # ` [ B ] .~ ) e. ZZ )
53 34 nnne0d 
 |-  ( ph -> ( # ` [ B ] .~ ) =/= 0 )
54 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
55 54 subg0cl 
 |-  ( H e. ( SubGrp ` G ) -> ( 0g ` G ) e. H )
56 16 55 syl 
 |-  ( ph -> ( 0g ` G ) e. H )
57 56 ne0d 
 |-  ( ph -> H =/= (/) )
58 12 ssrab3 
 |-  H C_ X
59 ssfi 
 |-  ( ( X e. Fin /\ H C_ X ) -> H e. Fin )
60 3 58 59 sylancl 
 |-  ( ph -> H e. Fin )
61 hashnncl 
 |-  ( H e. Fin -> ( ( # ` H ) e. NN <-> H =/= (/) ) )
62 60 61 syl 
 |-  ( ph -> ( ( # ` H ) e. NN <-> H =/= (/) ) )
63 57 62 mpbird 
 |-  ( ph -> ( # ` H ) e. NN )
64 63 nnzd 
 |-  ( ph -> ( # ` H ) e. ZZ )
65 63 nnne0d 
 |-  ( ph -> ( # ` H ) =/= 0 )
66 pcmul 
 |-  ( ( P e. Prime /\ ( ( # ` [ B ] .~ ) e. ZZ /\ ( # ` [ B ] .~ ) =/= 0 ) /\ ( ( # ` H ) e. ZZ /\ ( # ` H ) =/= 0 ) ) -> ( P pCnt ( ( # ` [ B ] .~ ) x. ( # ` H ) ) ) = ( ( P pCnt ( # ` [ B ] .~ ) ) + ( P pCnt ( # ` H ) ) ) )
67 4 52 53 64 65 66 syl122anc 
 |-  ( ph -> ( P pCnt ( ( # ` [ B ] .~ ) x. ( # ` H ) ) ) = ( ( P pCnt ( # ` [ B ] .~ ) ) + ( P pCnt ( # ` H ) ) ) )
68 51 67 eqtrd 
 |-  ( ph -> ( P pCnt ( # ` X ) ) = ( ( P pCnt ( # ` [ B ] .~ ) ) + ( P pCnt ( # ` H ) ) ) )
69 47 68 breqtrd 
 |-  ( ph -> ( ( P pCnt ( # ` [ B ] .~ ) ) + N ) <_ ( ( P pCnt ( # ` [ B ] .~ ) ) + ( P pCnt ( # ` H ) ) ) )
70 4 63 pccld 
 |-  ( ph -> ( P pCnt ( # ` H ) ) e. NN0 )
71 70 nn0red 
 |-  ( ph -> ( P pCnt ( # ` H ) ) e. RR )
72 37 71 36 leadd2d 
 |-  ( ph -> ( N <_ ( P pCnt ( # ` H ) ) <-> ( ( P pCnt ( # ` [ B ] .~ ) ) + N ) <_ ( ( P pCnt ( # ` [ B ] .~ ) ) + ( P pCnt ( # ` H ) ) ) ) )
73 69 72 mpbird 
 |-  ( ph -> N <_ ( P pCnt ( # ` H ) ) )
74 pcdvdsb 
 |-  ( ( P e. Prime /\ ( # ` H ) e. ZZ /\ N e. NN0 ) -> ( N <_ ( P pCnt ( # ` H ) ) <-> ( P ^ N ) || ( # ` H ) ) )
75 4 64 5 74 syl3anc 
 |-  ( ph -> ( N <_ ( P pCnt ( # ` H ) ) <-> ( P ^ N ) || ( # ` H ) ) )
76 73 75 mpbid 
 |-  ( ph -> ( P ^ N ) || ( # ` H ) )
77 prmnn 
 |-  ( P e. Prime -> P e. NN )
78 4 77 syl 
 |-  ( ph -> P e. NN )
79 78 5 nnexpcld 
 |-  ( ph -> ( P ^ N ) e. NN )
80 79 nnzd 
 |-  ( ph -> ( P ^ N ) e. ZZ )
81 dvdsle 
 |-  ( ( ( P ^ N ) e. ZZ /\ ( # ` H ) e. NN ) -> ( ( P ^ N ) || ( # ` H ) -> ( P ^ N ) <_ ( # ` H ) ) )
82 80 63 81 syl2anc 
 |-  ( ph -> ( ( P ^ N ) || ( # ` H ) -> ( P ^ N ) <_ ( # ` H ) ) )
83 76 82 mpd 
 |-  ( ph -> ( P ^ N ) <_ ( # ` H ) )
84 hashcl 
 |-  ( H e. Fin -> ( # ` H ) e. NN0 )
85 60 84 syl 
 |-  ( ph -> ( # ` H ) e. NN0 )
86 85 nn0red 
 |-  ( ph -> ( # ` H ) e. RR )
87 79 nnred 
 |-  ( ph -> ( P ^ N ) e. RR )
88 86 87 letri3d 
 |-  ( ph -> ( ( # ` H ) = ( P ^ N ) <-> ( ( # ` H ) <_ ( P ^ N ) /\ ( P ^ N ) <_ ( # ` H ) ) ) )
89 17 83 88 mpbir2and 
 |-  ( ph -> ( # ` H ) = ( P ^ N ) )
90 fveqeq2 
 |-  ( h = H -> ( ( # ` h ) = ( P ^ N ) <-> ( # ` H ) = ( P ^ N ) ) )
91 90 rspcev 
 |-  ( ( H e. ( SubGrp ` G ) /\ ( # ` H ) = ( P ^ N ) ) -> E. h e. ( SubGrp ` G ) ( # ` h ) = ( P ^ N ) )
92 16 89 91 syl2anc 
 |-  ( ph -> E. h e. ( SubGrp ` G ) ( # ` h ) = ( P ^ N ) )