Metamath Proof Explorer

Theorem sylow2a

Description: A named lemma of Sylow's second and third theorems. If G is a finite P -group that acts on the finite set Y , then the set Z of all points of Y fixed by every element of G has cardinality equivalent to the cardinality of Y , mod P . (Contributed by Mario Carneiro, 17-Jan-2015)

Ref Expression
Hypotheses sylow2a.x 
|- X = ( Base ` G )
sylow2a.m 
|- ( ph -> .(+) e. ( G GrpAct Y ) )
sylow2a.p 
|- ( ph -> P pGrp G )
sylow2a.f 
|- ( ph -> X e. Fin )
sylow2a.y 
|- ( ph -> Y e. Fin )
sylow2a.z 
|- Z = { u e. Y | A. h e. X ( h .(+) u ) = u }
sylow2a.r 
|- .~ = { <. x , y >. | ( { x , y } C_ Y /\ E. g e. X ( g .(+) x ) = y ) }
Assertion sylow2a 
|- ( ph -> P || ( ( # ` Y ) - ( # ` Z ) ) )

Proof

Step Hyp Ref Expression
1 sylow2a.x 
 |-  X = ( Base ` G )
2 sylow2a.m 
 |-  ( ph -> .(+) e. ( G GrpAct Y ) )
3 sylow2a.p 
 |-  ( ph -> P pGrp G )
4 sylow2a.f 
 |-  ( ph -> X e. Fin )
5 sylow2a.y 
 |-  ( ph -> Y e. Fin )
6 sylow2a.z 
 |-  Z = { u e. Y | A. h e. X ( h .(+) u ) = u }
7 sylow2a.r 
 |-  .~ = { <. x , y >. | ( { x , y } C_ Y /\ E. g e. X ( g .(+) x ) = y ) }
8 1 2 3 4 5 6 7 sylow2alem2 
 |-  ( ph -> P || sum_ z e. ( ( Y /. .~ ) \ ~P Z ) ( # ` z ) )
9 inass 
 |-  ( ( ( Y /. .~ ) i^i ~P Z ) i^i ( ( Y /. .~ ) \ ~P Z ) ) = ( ( Y /. .~ ) i^i ( ~P Z i^i ( ( Y /. .~ ) \ ~P Z ) ) )
10 disjdif 
 |-  ( ~P Z i^i ( ( Y /. .~ ) \ ~P Z ) ) = (/)
11 10 ineq2i 
 |-  ( ( Y /. .~ ) i^i ( ~P Z i^i ( ( Y /. .~ ) \ ~P Z ) ) ) = ( ( Y /. .~ ) i^i (/) )
12 in0 
 |-  ( ( Y /. .~ ) i^i (/) ) = (/)
13 9 11 12 3eqtri 
 |-  ( ( ( Y /. .~ ) i^i ~P Z ) i^i ( ( Y /. .~ ) \ ~P Z ) ) = (/)
14 13 a1i 
 |-  ( ph -> ( ( ( Y /. .~ ) i^i ~P Z ) i^i ( ( Y /. .~ ) \ ~P Z ) ) = (/) )
15 inundif 
 |-  ( ( ( Y /. .~ ) i^i ~P Z ) u. ( ( Y /. .~ ) \ ~P Z ) ) = ( Y /. .~ )
16 15 eqcomi 
 |-  ( Y /. .~ ) = ( ( ( Y /. .~ ) i^i ~P Z ) u. ( ( Y /. .~ ) \ ~P Z ) )
17 16 a1i 
 |-  ( ph -> ( Y /. .~ ) = ( ( ( Y /. .~ ) i^i ~P Z ) u. ( ( Y /. .~ ) \ ~P Z ) ) )
18 pwfi 
 |-  ( Y e. Fin <-> ~P Y e. Fin )
19 5 18 sylib 
 |-  ( ph -> ~P Y e. Fin )
20 7 1 gaorber 
 |-  ( .(+) e. ( G GrpAct Y ) -> .~ Er Y )
21 2 20 syl 
 |-  ( ph -> .~ Er Y )
22 21 qsss 
 |-  ( ph -> ( Y /. .~ ) C_ ~P Y )
23 19 22 ssfid 
 |-  ( ph -> ( Y /. .~ ) e. Fin )
24 5 adantr 
 |-  ( ( ph /\ z e. ( Y /. .~ ) ) -> Y e. Fin )
25 22 sselda 
 |-  ( ( ph /\ z e. ( Y /. .~ ) ) -> z e. ~P Y )
26 25 elpwid 
 |-  ( ( ph /\ z e. ( Y /. .~ ) ) -> z C_ Y )
27 24 26 ssfid 
 |-  ( ( ph /\ z e. ( Y /. .~ ) ) -> z e. Fin )
28 hashcl 
 |-  ( z e. Fin -> ( # ` z ) e. NN0 )
29 27 28 syl 
 |-  ( ( ph /\ z e. ( Y /. .~ ) ) -> ( # ` z ) e. NN0 )
30 29 nn0cnd 
 |-  ( ( ph /\ z e. ( Y /. .~ ) ) -> ( # ` z ) e. CC )
31 14 17 23 30 fsumsplit 
 |-  ( ph -> sum_ z e. ( Y /. .~ ) ( # ` z ) = ( sum_ z e. ( ( Y /. .~ ) i^i ~P Z ) ( # ` z ) + sum_ z e. ( ( Y /. .~ ) \ ~P Z ) ( # ` z ) ) )
32 21 5 qshash 
 |-  ( ph -> ( # ` Y ) = sum_ z e. ( Y /. .~ ) ( # ` z ) )
33 inss1 
 |-  ( ( Y /. .~ ) i^i ~P Z ) C_ ( Y /. .~ )
34 ssfi 
 |-  ( ( ( Y /. .~ ) e. Fin /\ ( ( Y /. .~ ) i^i ~P Z ) C_ ( Y /. .~ ) ) -> ( ( Y /. .~ ) i^i ~P Z ) e. Fin )
35 23 33 34 sylancl 
 |-  ( ph -> ( ( Y /. .~ ) i^i ~P Z ) e. Fin )
36 ax-1cn 
 |-  1 e. CC
37 fsumconst 
 |-  ( ( ( ( Y /. .~ ) i^i ~P Z ) e. Fin /\ 1 e. CC ) -> sum_ z e. ( ( Y /. .~ ) i^i ~P Z ) 1 = ( ( # ` ( ( Y /. .~ ) i^i ~P Z ) ) x. 1 ) )
38 35 36 37 sylancl 
 |-  ( ph -> sum_ z e. ( ( Y /. .~ ) i^i ~P Z ) 1 = ( ( # ` ( ( Y /. .~ ) i^i ~P Z ) ) x. 1 ) )
39 elin 
 |-  ( z e. ( ( Y /. .~ ) i^i ~P Z ) <-> ( z e. ( Y /. .~ ) /\ z e. ~P Z ) )
40 eqid 
 |-  ( Y /. .~ ) = ( Y /. .~ )
41 sseq1 
 |-  ( [ w ] .~ = z -> ( [ w ] .~ C_ Z <-> z C_ Z ) )
42 velpw 
 |-  ( z e. ~P Z <-> z C_ Z )
43 41 42 bitr4di 
 |-  ( [ w ] .~ = z -> ( [ w ] .~ C_ Z <-> z e. ~P Z ) )
44 breq1 
 |-  ( [ w ] .~ = z -> ( [ w ] .~ ~~ 1o <-> z ~~ 1o ) )
45 43 44 imbi12d 
 |-  ( [ w ] .~ = z -> ( ( [ w ] .~ C_ Z -> [ w ] .~ ~~ 1o ) <-> ( z e. ~P Z -> z ~~ 1o ) ) )
46 21 adantr 
 |-  ( ( ph /\ w e. Y ) -> .~ Er Y )
47 simpr 
 |-  ( ( ph /\ w e. Y ) -> w e. Y )
48 46 47 erref 
 |-  ( ( ph /\ w e. Y ) -> w .~ w )
49 vex 
 |-  w e. _V
50 49 49 elec 
 |-  ( w e. [ w ] .~ <-> w .~ w )
51 48 50 sylibr 
 |-  ( ( ph /\ w e. Y ) -> w e. [ w ] .~ )
52 ssel 
 |-  ( [ w ] .~ C_ Z -> ( w e. [ w ] .~ -> w e. Z ) )
53 51 52 syl5com 
 |-  ( ( ph /\ w e. Y ) -> ( [ w ] .~ C_ Z -> w e. Z ) )
54 1 2 3 4 5 6 7 sylow2alem1 
 |-  ( ( ph /\ w e. Z ) -> [ w ] .~ = { w } )
55 49 ensn1 
 |-  { w } ~~ 1o
56 54 55 eqbrtrdi 
 |-  ( ( ph /\ w e. Z ) -> [ w ] .~ ~~ 1o )
57 56 ex 
 |-  ( ph -> ( w e. Z -> [ w ] .~ ~~ 1o ) )
58 57 adantr 
 |-  ( ( ph /\ w e. Y ) -> ( w e. Z -> [ w ] .~ ~~ 1o ) )
59 53 58 syld 
 |-  ( ( ph /\ w e. Y ) -> ( [ w ] .~ C_ Z -> [ w ] .~ ~~ 1o ) )
60 40 45 59 ectocld 
 |-  ( ( ph /\ z e. ( Y /. .~ ) ) -> ( z e. ~P Z -> z ~~ 1o ) )
61 60 impr 
 |-  ( ( ph /\ ( z e. ( Y /. .~ ) /\ z e. ~P Z ) ) -> z ~~ 1o )
62 39 61 sylan2b 
 |-  ( ( ph /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) -> z ~~ 1o )
63 en1b 
 |-  ( z ~~ 1o <-> z = { U. z } )
64 62 63 sylib 
 |-  ( ( ph /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) -> z = { U. z } )
65 64 fveq2d 
 |-  ( ( ph /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) -> ( # ` z ) = ( # ` { U. z } ) )
66 vuniex 
 |-  U. z e. _V
67 hashsng 
 |-  ( U. z e. _V -> ( # ` { U. z } ) = 1 )
68 66 67 ax-mp 
 |-  ( # ` { U. z } ) = 1
69 65 68 eqtrdi 
 |-  ( ( ph /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) -> ( # ` z ) = 1 )
70 69 sumeq2dv 
 |-  ( ph -> sum_ z e. ( ( Y /. .~ ) i^i ~P Z ) ( # ` z ) = sum_ z e. ( ( Y /. .~ ) i^i ~P Z ) 1 )
71 6 ssrab3 
 |-  Z C_ Y
72 ssfi 
 |-  ( ( Y e. Fin /\ Z C_ Y ) -> Z e. Fin )
73 5 71 72 sylancl 
 |-  ( ph -> Z e. Fin )
74 hashcl 
 |-  ( Z e. Fin -> ( # ` Z ) e. NN0 )
75 73 74 syl 
 |-  ( ph -> ( # ` Z ) e. NN0 )
76 75 nn0cnd 
 |-  ( ph -> ( # ` Z ) e. CC )
77 76 mulid1d 
 |-  ( ph -> ( ( # ` Z ) x. 1 ) = ( # ` Z ) )
78 6 5 rabexd 
 |-  ( ph -> Z e. _V )
79 eqid 
 |-  ( w e. Z |-> { w } ) = ( w e. Z |-> { w } )
80 7 relopabiv 
 |-  Rel .~
81 relssdmrn 
 |-  ( Rel .~ -> .~ C_ ( dom .~ X. ran .~ ) )
82 80 81 ax-mp 
 |-  .~ C_ ( dom .~ X. ran .~ )
83 erdm 
 |-  ( .~ Er Y -> dom .~ = Y )
84 21 83 syl 
 |-  ( ph -> dom .~ = Y )
85 84 5 eqeltrd 
 |-  ( ph -> dom .~ e. Fin )
86 errn 
 |-  ( .~ Er Y -> ran .~ = Y )
87 21 86 syl 
 |-  ( ph -> ran .~ = Y )
88 87 5 eqeltrd 
 |-  ( ph -> ran .~ e. Fin )
89 85 88 xpexd 
 |-  ( ph -> ( dom .~ X. ran .~ ) e. _V )
90 ssexg 
 |-  ( ( .~ C_ ( dom .~ X. ran .~ ) /\ ( dom .~ X. ran .~ ) e. _V ) -> .~ e. _V )
91 82 89 90 sylancr 
 |-  ( ph -> .~ e. _V )
92 simpr 
 |-  ( ( ph /\ w e. Z ) -> w e. Z )
93 71 92 sseldi 
 |-  ( ( ph /\ w e. Z ) -> w e. Y )
94 ecelqsg 
 |-  ( ( .~ e. _V /\ w e. Y ) -> [ w ] .~ e. ( Y /. .~ ) )
95 91 93 94 syl2an2r 
 |-  ( ( ph /\ w e. Z ) -> [ w ] .~ e. ( Y /. .~ ) )
96 54 95 eqeltrrd 
 |-  ( ( ph /\ w e. Z ) -> { w } e. ( Y /. .~ ) )
97 snelpwi 
 |-  ( w e. Z -> { w } e. ~P Z )
98 97 adantl 
 |-  ( ( ph /\ w e. Z ) -> { w } e. ~P Z )
99 96 98 elind 
 |-  ( ( ph /\ w e. Z ) -> { w } e. ( ( Y /. .~ ) i^i ~P Z ) )
100 simpr 
 |-  ( ( ph /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) -> z e. ( ( Y /. .~ ) i^i ~P Z ) )
101 100 elin2d 
 |-  ( ( ph /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) -> z e. ~P Z )
102 101 elpwid 
 |-  ( ( ph /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) -> z C_ Z )
103 64 102 eqsstrrd 
 |-  ( ( ph /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) -> { U. z } C_ Z )
104 66 snss 
 |-  ( U. z e. Z <-> { U. z } C_ Z )
105 103 104 sylibr 
 |-  ( ( ph /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) -> U. z e. Z )
106 sneq 
 |-  ( w = U. z -> { w } = { U. z } )
107 106 eqeq2d 
 |-  ( w = U. z -> ( z = { w } <-> z = { U. z } ) )
108 64 107 syl5ibrcom 
 |-  ( ( ph /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) -> ( w = U. z -> z = { w } ) )
109 108 adantrl 
 |-  ( ( ph /\ ( w e. Z /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) ) -> ( w = U. z -> z = { w } ) )
110 unieq 
 |-  ( z = { w } -> U. z = U. { w } )
111 49 unisn 
 |-  U. { w } = w
112 110 111 eqtr2di 
 |-  ( z = { w } -> w = U. z )
113 109 112 impbid1 
 |-  ( ( ph /\ ( w e. Z /\ z e. ( ( Y /. .~ ) i^i ~P Z ) ) ) -> ( w = U. z <-> z = { w } ) )
114 79 99 105 113 f1o2d 
 |-  ( ph -> ( w e. Z |-> { w } ) : Z -1-1-onto-> ( ( Y /. .~ ) i^i ~P Z ) )
115 78 114 hasheqf1od 
 |-  ( ph -> ( # ` Z ) = ( # ` ( ( Y /. .~ ) i^i ~P Z ) ) )
116 115 oveq1d 
 |-  ( ph -> ( ( # ` Z ) x. 1 ) = ( ( # ` ( ( Y /. .~ ) i^i ~P Z ) ) x. 1 ) )
117 77 116 eqtr3d 
 |-  ( ph -> ( # ` Z ) = ( ( # ` ( ( Y /. .~ ) i^i ~P Z ) ) x. 1 ) )
118 38 70 117 3eqtr4rd 
 |-  ( ph -> ( # ` Z ) = sum_ z e. ( ( Y /. .~ ) i^i ~P Z ) ( # ` z ) )
119 118 oveq1d 
 |-  ( ph -> ( ( # ` Z ) + sum_ z e. ( ( Y /. .~ ) \ ~P Z ) ( # ` z ) ) = ( sum_ z e. ( ( Y /. .~ ) i^i ~P Z ) ( # ` z ) + sum_ z e. ( ( Y /. .~ ) \ ~P Z ) ( # ` z ) ) )
120 31 32 119 3eqtr4rd 
 |-  ( ph -> ( ( # ` Z ) + sum_ z e. ( ( Y /. .~ ) \ ~P Z ) ( # ` z ) ) = ( # ` Y ) )
121 hashcl 
 |-  ( Y e. Fin -> ( # ` Y ) e. NN0 )
122 5 121 syl 
 |-  ( ph -> ( # ` Y ) e. NN0 )
123 122 nn0cnd 
 |-  ( ph -> ( # ` Y ) e. CC )
124 diffi 
 |-  ( ( Y /. .~ ) e. Fin -> ( ( Y /. .~ ) \ ~P Z ) e. Fin )
125 23 124 syl 
 |-  ( ph -> ( ( Y /. .~ ) \ ~P Z ) e. Fin )
126 eldifi 
 |-  ( z e. ( ( Y /. .~ ) \ ~P Z ) -> z e. ( Y /. .~ ) )
127 126 30 sylan2 
 |-  ( ( ph /\ z e. ( ( Y /. .~ ) \ ~P Z ) ) -> ( # ` z ) e. CC )
128 125 127 fsumcl 
 |-  ( ph -> sum_ z e. ( ( Y /. .~ ) \ ~P Z ) ( # ` z ) e. CC )
129 123 76 128 subaddd 
 |-  ( ph -> ( ( ( # ` Y ) - ( # ` Z ) ) = sum_ z e. ( ( Y /. .~ ) \ ~P Z ) ( # ` z ) <-> ( ( # ` Z ) + sum_ z e. ( ( Y /. .~ ) \ ~P Z ) ( # ` z ) ) = ( # ` Y ) ) )
130 120 129 mpbird 
 |-  ( ph -> ( ( # ` Y ) - ( # ` Z ) ) = sum_ z e. ( ( Y /. .~ ) \ ~P Z ) ( # ` z ) )
131 8 130 breqtrrd 
 |-  ( ph -> P || ( ( # ` Y ) - ( # ` Z ) ) )