Metamath Proof Explorer

Theorem sylow1lem3

Description: Lemma for sylow1 . One of the orbits of the group action has p-adic valuation less than the prime count of the set S . (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 ) }
Assertion sylow1lem3 
|- ( ph -> E. w e. S ( P pCnt ( # ` [ w ] .~ ) ) <_ ( ( P pCnt ( # ` X ) ) - 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 1 2 3 4 5 6 7 8 sylow1lem1 
 |-  ( ph -> ( ( # ` S ) e. NN /\ ( P pCnt ( # ` S ) ) = ( ( P pCnt ( # ` X ) ) - N ) ) )
12 11 simpld 
 |-  ( ph -> ( # ` S ) e. NN )
13 pcndvds 
 |-  ( ( P e. Prime /\ ( # ` S ) e. NN ) -> -. ( P ^ ( ( P pCnt ( # ` S ) ) + 1 ) ) || ( # ` S ) )
14 4 12 13 syl2anc 
 |-  ( ph -> -. ( P ^ ( ( P pCnt ( # ` S ) ) + 1 ) ) || ( # ` S ) )
15 11 simprd 
 |-  ( ph -> ( P pCnt ( # ` S ) ) = ( ( P pCnt ( # ` X ) ) - N ) )
16 15 oveq1d 
 |-  ( ph -> ( ( P pCnt ( # ` S ) ) + 1 ) = ( ( ( P pCnt ( # ` X ) ) - N ) + 1 ) )
17 16 oveq2d 
 |-  ( ph -> ( P ^ ( ( P pCnt ( # ` S ) ) + 1 ) ) = ( P ^ ( ( ( P pCnt ( # ` X ) ) - N ) + 1 ) ) )
18 1 2 3 4 5 6 7 8 9 sylow1lem2 
 |-  ( ph -> .(+) e. ( G GrpAct S ) )
19 10 1 gaorber 
 |-  ( .(+) e. ( G GrpAct S ) -> .~ Er S )
20 18 19 syl 
 |-  ( ph -> .~ Er S )
21 pwfi 
 |-  ( X e. Fin <-> ~P X e. Fin )
22 3 21 sylib 
 |-  ( ph -> ~P X e. Fin )
23 8 ssrab3 
 |-  S C_ ~P X
24 ssfi 
 |-  ( ( ~P X e. Fin /\ S C_ ~P X ) -> S e. Fin )
25 22 23 24 sylancl 
 |-  ( ph -> S e. Fin )
26 20 25 qshash 
 |-  ( ph -> ( # ` S ) = sum_ z e. ( S /. .~ ) ( # ` z ) )
27 17 26 breq12d 
 |-  ( ph -> ( ( P ^ ( ( P pCnt ( # ` S ) ) + 1 ) ) || ( # ` S ) <-> ( P ^ ( ( ( P pCnt ( # ` X ) ) - N ) + 1 ) ) || sum_ z e. ( S /. .~ ) ( # ` z ) ) )
28 14 27 mtbid 
 |-  ( ph -> -. ( P ^ ( ( ( P pCnt ( # ` X ) ) - N ) + 1 ) ) || sum_ z e. ( S /. .~ ) ( # ` z ) )
29 pwfi 
 |-  ( S e. Fin <-> ~P S e. Fin )
30 25 29 sylib 
 |-  ( ph -> ~P S e. Fin )
31 20 qsss 
 |-  ( ph -> ( S /. .~ ) C_ ~P S )
32 30 31 ssfid 
 |-  ( ph -> ( S /. .~ ) e. Fin )
33 32 adantr 
 |-  ( ( ph /\ A. a e. ( S /. .~ ) -. ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) -> ( S /. .~ ) e. Fin )
34 prmnn 
 |-  ( P e. Prime -> P e. NN )
35 4 34 syl 
 |-  ( ph -> P e. NN )
36 4 12 pccld 
 |-  ( ph -> ( P pCnt ( # ` S ) ) e. NN0 )
37 15 36 eqeltrrd 
 |-  ( ph -> ( ( P pCnt ( # ` X ) ) - N ) e. NN0 )
38 peano2nn0 
 |-  ( ( ( P pCnt ( # ` X ) ) - N ) e. NN0 -> ( ( ( P pCnt ( # ` X ) ) - N ) + 1 ) e. NN0 )
39 37 38 syl 
 |-  ( ph -> ( ( ( P pCnt ( # ` X ) ) - N ) + 1 ) e. NN0 )
40 35 39 nnexpcld 
 |-  ( ph -> ( P ^ ( ( ( P pCnt ( # ` X ) ) - N ) + 1 ) ) e. NN )
41 40 nnzd 
 |-  ( ph -> ( P ^ ( ( ( P pCnt ( # ` X ) ) - N ) + 1 ) ) e. ZZ )
42 41 adantr 
 |-  ( ( ph /\ A. a e. ( S /. .~ ) -. ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) -> ( P ^ ( ( ( P pCnt ( # ` X ) ) - N ) + 1 ) ) e. ZZ )
43 erdm 
 |-  ( .~ Er S -> dom .~ = S )
44 20 43 syl 
 |-  ( ph -> dom .~ = S )
45 elqsn0 
 |-  ( ( dom .~ = S /\ z e. ( S /. .~ ) ) -> z =/= (/) )
46 44 45 sylan 
 |-  ( ( ph /\ z e. ( S /. .~ ) ) -> z =/= (/) )
47 25 adantr 
 |-  ( ( ph /\ z e. ( S /. .~ ) ) -> S e. Fin )
48 31 sselda 
 |-  ( ( ph /\ z e. ( S /. .~ ) ) -> z e. ~P S )
49 48 elpwid 
 |-  ( ( ph /\ z e. ( S /. .~ ) ) -> z C_ S )
50 47 49 ssfid 
 |-  ( ( ph /\ z e. ( S /. .~ ) ) -> z e. Fin )
51 hashnncl 
 |-  ( z e. Fin -> ( ( # ` z ) e. NN <-> z =/= (/) ) )
52 50 51 syl 
 |-  ( ( ph /\ z e. ( S /. .~ ) ) -> ( ( # ` z ) e. NN <-> z =/= (/) ) )
53 46 52 mpbird 
 |-  ( ( ph /\ z e. ( S /. .~ ) ) -> ( # ` z ) e. NN )
54 53 adantlr 
 |-  ( ( ( ph /\ A. a e. ( S /. .~ ) -. ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) /\ z e. ( S /. .~ ) ) -> ( # ` z ) e. NN )
55 54 nnzd 
 |-  ( ( ( ph /\ A. a e. ( S /. .~ ) -. ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) /\ z e. ( S /. .~ ) ) -> ( # ` z ) e. ZZ )
56 fveq2 
 |-  ( a = z -> ( # ` a ) = ( # ` z ) )
57 56 oveq2d 
 |-  ( a = z -> ( P pCnt ( # ` a ) ) = ( P pCnt ( # ` z ) ) )
58 57 breq1d 
 |-  ( a = z -> ( ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) <-> ( P pCnt ( # ` z ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) )
59 58 notbid 
 |-  ( a = z -> ( -. ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) <-> -. ( P pCnt ( # ` z ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) )
60 59 rspccva 
 |-  ( ( A. a e. ( S /. .~ ) -. ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) /\ z e. ( S /. .~ ) ) -> -. ( P pCnt ( # ` z ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) )
61 60 adantll 
 |-  ( ( ( ph /\ A. a e. ( S /. .~ ) -. ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) /\ z e. ( S /. .~ ) ) -> -. ( P pCnt ( # ` z ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) )
62 1 grpbn0 
 |-  ( G e. Grp -> X =/= (/) )
63 2 62 syl 
 |-  ( ph -> X =/= (/) )
64 hashnncl 
 |-  ( X e. Fin -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
65 3 64 syl 
 |-  ( ph -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
66 63 65 mpbird 
 |-  ( ph -> ( # ` X ) e. NN )
67 4 66 pccld 
 |-  ( ph -> ( P pCnt ( # ` X ) ) e. NN0 )
68 67 nn0zd 
 |-  ( ph -> ( P pCnt ( # ` X ) ) e. ZZ )
69 5 nn0zd 
 |-  ( ph -> N e. ZZ )
70 68 69 zsubcld 
 |-  ( ph -> ( ( P pCnt ( # ` X ) ) - N ) e. ZZ )
71 70 ad2antrr 
 |-  ( ( ( ph /\ A. a e. ( S /. .~ ) -. ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) /\ z e. ( S /. .~ ) ) -> ( ( P pCnt ( # ` X ) ) - N ) e. ZZ )
72 71 zred 
 |-  ( ( ( ph /\ A. a e. ( S /. .~ ) -. ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) /\ z e. ( S /. .~ ) ) -> ( ( P pCnt ( # ` X ) ) - N ) e. RR )
73 4 ad2antrr 
 |-  ( ( ( ph /\ A. a e. ( S /. .~ ) -. ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) /\ z e. ( S /. .~ ) ) -> P e. Prime )
74 73 54 pccld 
 |-  ( ( ( ph /\ A. a e. ( S /. .~ ) -. ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) /\ z e. ( S /. .~ ) ) -> ( P pCnt ( # ` z ) ) e. NN0 )
75 74 nn0zd 
 |-  ( ( ( ph /\ A. a e. ( S /. .~ ) -. ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) /\ z e. ( S /. .~ ) ) -> ( P pCnt ( # ` z ) ) e. ZZ )
76 75 zred 
 |-  ( ( ( ph /\ A. a e. ( S /. .~ ) -. ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) /\ z e. ( S /. .~ ) ) -> ( P pCnt ( # ` z ) ) e. RR )
77 72 76 ltnled 
 |-  ( ( ( ph /\ A. a e. ( S /. .~ ) -. ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) /\ z e. ( S /. .~ ) ) -> ( ( ( P pCnt ( # ` X ) ) - N ) < ( P pCnt ( # ` z ) ) <-> -. ( P pCnt ( # ` z ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) )
78 61 77 mpbird 
 |-  ( ( ( ph /\ A. a e. ( S /. .~ ) -. ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) /\ z e. ( S /. .~ ) ) -> ( ( P pCnt ( # ` X ) ) - N ) < ( P pCnt ( # ` z ) ) )
79 zltp1le 
 |-  ( ( ( ( P pCnt ( # ` X ) ) - N ) e. ZZ /\ ( P pCnt ( # ` z ) ) e. ZZ ) -> ( ( ( P pCnt ( # ` X ) ) - N ) < ( P pCnt ( # ` z ) ) <-> ( ( ( P pCnt ( # ` X ) ) - N ) + 1 ) <_ ( P pCnt ( # ` z ) ) ) )
80 71 75 79 syl2anc 
 |-  ( ( ( ph /\ A. a e. ( S /. .~ ) -. ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) /\ z e. ( S /. .~ ) ) -> ( ( ( P pCnt ( # ` X ) ) - N ) < ( P pCnt ( # ` z ) ) <-> ( ( ( P pCnt ( # ` X ) ) - N ) + 1 ) <_ ( P pCnt ( # ` z ) ) ) )
81 78 80 mpbid 
 |-  ( ( ( ph /\ A. a e. ( S /. .~ ) -. ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) /\ z e. ( S /. .~ ) ) -> ( ( ( P pCnt ( # ` X ) ) - N ) + 1 ) <_ ( P pCnt ( # ` z ) ) )
82 39 ad2antrr 
 |-  ( ( ( ph /\ A. a e. ( S /. .~ ) -. ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) /\ z e. ( S /. .~ ) ) -> ( ( ( P pCnt ( # ` X ) ) - N ) + 1 ) e. NN0 )
83 pcdvdsb 
 |-  ( ( P e. Prime /\ ( # ` z ) e. ZZ /\ ( ( ( P pCnt ( # ` X ) ) - N ) + 1 ) e. NN0 ) -> ( ( ( ( P pCnt ( # ` X ) ) - N ) + 1 ) <_ ( P pCnt ( # ` z ) ) <-> ( P ^ ( ( ( P pCnt ( # ` X ) ) - N ) + 1 ) ) || ( # ` z ) ) )
84 73 55 82 83 syl3anc 
 |-  ( ( ( ph /\ A. a e. ( S /. .~ ) -. ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) /\ z e. ( S /. .~ ) ) -> ( ( ( ( P pCnt ( # ` X ) ) - N ) + 1 ) <_ ( P pCnt ( # ` z ) ) <-> ( P ^ ( ( ( P pCnt ( # ` X ) ) - N ) + 1 ) ) || ( # ` z ) ) )
85 81 84 mpbid 
 |-  ( ( ( ph /\ A. a e. ( S /. .~ ) -. ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) /\ z e. ( S /. .~ ) ) -> ( P ^ ( ( ( P pCnt ( # ` X ) ) - N ) + 1 ) ) || ( # ` z ) )
86 33 42 55 85 fsumdvds 
 |-  ( ( ph /\ A. a e. ( S /. .~ ) -. ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) -> ( P ^ ( ( ( P pCnt ( # ` X ) ) - N ) + 1 ) ) || sum_ z e. ( S /. .~ ) ( # ` z ) )
87 28 86 mtand 
 |-  ( ph -> -. A. a e. ( S /. .~ ) -. ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) )
88 dfrex2 
 |-  ( E. a e. ( S /. .~ ) ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) <-> -. A. a e. ( S /. .~ ) -. ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) )
89 87 88 sylibr 
 |-  ( ph -> E. a e. ( S /. .~ ) ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) )
90 eqid 
 |-  ( S /. .~ ) = ( S /. .~ )
91 fveq2 
 |-  ( [ z ] .~ = a -> ( # ` [ z ] .~ ) = ( # ` a ) )
92 91 oveq2d 
 |-  ( [ z ] .~ = a -> ( P pCnt ( # ` [ z ] .~ ) ) = ( P pCnt ( # ` a ) ) )
93 92 breq1d 
 |-  ( [ z ] .~ = a -> ( ( P pCnt ( # ` [ z ] .~ ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) <-> ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) )
94 93 imbi1d 
 |-  ( [ z ] .~ = a -> ( ( ( P pCnt ( # ` [ z ] .~ ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) -> E. w e. S ( P pCnt ( # ` [ w ] .~ ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) <-> ( ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) -> E. w e. S ( P pCnt ( # ` [ w ] .~ ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) ) )
95 eceq1 
 |-  ( w = z -> [ w ] .~ = [ z ] .~ )
96 95 fveq2d 
 |-  ( w = z -> ( # ` [ w ] .~ ) = ( # ` [ z ] .~ ) )
97 96 oveq2d 
 |-  ( w = z -> ( P pCnt ( # ` [ w ] .~ ) ) = ( P pCnt ( # ` [ z ] .~ ) ) )
98 97 breq1d 
 |-  ( w = z -> ( ( P pCnt ( # ` [ w ] .~ ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) <-> ( P pCnt ( # ` [ z ] .~ ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) )
99 98 rspcev 
 |-  ( ( z e. S /\ ( P pCnt ( # ` [ z ] .~ ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) -> E. w e. S ( P pCnt ( # ` [ w ] .~ ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) )
100 99 ex 
 |-  ( z e. S -> ( ( P pCnt ( # ` [ z ] .~ ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) -> E. w e. S ( P pCnt ( # ` [ w ] .~ ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) )
101 100 adantl 
 |-  ( ( ph /\ z e. S ) -> ( ( P pCnt ( # ` [ z ] .~ ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) -> E. w e. S ( P pCnt ( # ` [ w ] .~ ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) )
102 90 94 101 ectocld 
 |-  ( ( ph /\ a e. ( S /. .~ ) ) -> ( ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) -> E. w e. S ( P pCnt ( # ` [ w ] .~ ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) )
103 102 rexlimdva 
 |-  ( ph -> ( E. a e. ( S /. .~ ) ( P pCnt ( # ` a ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) -> E. w e. S ( P pCnt ( # ` [ w ] .~ ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) ) )
104 89 103 mpd 
 |-  ( ph -> E. w e. S ( P pCnt ( # ` [ w ] .~ ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) )