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 sselid
 |-  ( ( 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 ) ) )