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 𝑋 = ( Base ‘ 𝐺 )
sylow2a.m ( 𝜑 ∈ ( 𝐺 GrpAct 𝑌 ) )
sylow2a.p ( 𝜑𝑃 pGrp 𝐺 )
sylow2a.f ( 𝜑𝑋 ∈ Fin )
sylow2a.y ( 𝜑𝑌 ∈ Fin )
sylow2a.z 𝑍 = { 𝑢𝑌 ∣ ∀ 𝑋 ( 𝑢 ) = 𝑢 }
sylow2a.r = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑌 ∧ ∃ 𝑔𝑋 ( 𝑔 𝑥 ) = 𝑦 ) }
Assertion sylow2a ( 𝜑𝑃 ∥ ( ( ♯ ‘ 𝑌 ) − ( ♯ ‘ 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 sylow2a.x 𝑋 = ( Base ‘ 𝐺 )
2 sylow2a.m ( 𝜑 ∈ ( 𝐺 GrpAct 𝑌 ) )
3 sylow2a.p ( 𝜑𝑃 pGrp 𝐺 )
4 sylow2a.f ( 𝜑𝑋 ∈ Fin )
5 sylow2a.y ( 𝜑𝑌 ∈ Fin )
6 sylow2a.z 𝑍 = { 𝑢𝑌 ∣ ∀ 𝑋 ( 𝑢 ) = 𝑢 }
7 sylow2a.r = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑌 ∧ ∃ 𝑔𝑋 ( 𝑔 𝑥 ) = 𝑦 ) }
8 1 2 3 4 5 6 7 sylow2alem2 ( 𝜑𝑃 ∥ Σ 𝑧 ∈ ( ( 𝑌 / ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) )
9 inass ( ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ∩ ( ( 𝑌 / ) ∖ 𝒫 𝑍 ) ) = ( ( 𝑌 / ) ∩ ( 𝒫 𝑍 ∩ ( ( 𝑌 / ) ∖ 𝒫 𝑍 ) ) )
10 disjdif ( 𝒫 𝑍 ∩ ( ( 𝑌 / ) ∖ 𝒫 𝑍 ) ) = ∅
11 10 ineq2i ( ( 𝑌 / ) ∩ ( 𝒫 𝑍 ∩ ( ( 𝑌 / ) ∖ 𝒫 𝑍 ) ) ) = ( ( 𝑌 / ) ∩ ∅ )
12 in0 ( ( 𝑌 / ) ∩ ∅ ) = ∅
13 9 11 12 3eqtri ( ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ∩ ( ( 𝑌 / ) ∖ 𝒫 𝑍 ) ) = ∅
14 13 a1i ( 𝜑 → ( ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ∩ ( ( 𝑌 / ) ∖ 𝒫 𝑍 ) ) = ∅ )
15 inundif ( ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ∪ ( ( 𝑌 / ) ∖ 𝒫 𝑍 ) ) = ( 𝑌 / )
16 15 eqcomi ( 𝑌 / ) = ( ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ∪ ( ( 𝑌 / ) ∖ 𝒫 𝑍 ) )
17 16 a1i ( 𝜑 → ( 𝑌 / ) = ( ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ∪ ( ( 𝑌 / ) ∖ 𝒫 𝑍 ) ) )
18 pwfi ( 𝑌 ∈ Fin ↔ 𝒫 𝑌 ∈ Fin )
19 5 18 sylib ( 𝜑 → 𝒫 𝑌 ∈ Fin )
20 7 1 gaorber ( ∈ ( 𝐺 GrpAct 𝑌 ) → Er 𝑌 )
21 2 20 syl ( 𝜑 Er 𝑌 )
22 21 qsss ( 𝜑 → ( 𝑌 / ) ⊆ 𝒫 𝑌 )
23 19 22 ssfid ( 𝜑 → ( 𝑌 / ) ∈ Fin )
24 5 adantr ( ( 𝜑𝑧 ∈ ( 𝑌 / ) ) → 𝑌 ∈ Fin )
25 22 sselda ( ( 𝜑𝑧 ∈ ( 𝑌 / ) ) → 𝑧 ∈ 𝒫 𝑌 )
26 25 elpwid ( ( 𝜑𝑧 ∈ ( 𝑌 / ) ) → 𝑧𝑌 )
27 24 26 ssfid ( ( 𝜑𝑧 ∈ ( 𝑌 / ) ) → 𝑧 ∈ Fin )
28 hashcl ( 𝑧 ∈ Fin → ( ♯ ‘ 𝑧 ) ∈ ℕ0 )
29 27 28 syl ( ( 𝜑𝑧 ∈ ( 𝑌 / ) ) → ( ♯ ‘ 𝑧 ) ∈ ℕ0 )
30 29 nn0cnd ( ( 𝜑𝑧 ∈ ( 𝑌 / ) ) → ( ♯ ‘ 𝑧 ) ∈ ℂ )
31 14 17 23 30 fsumsplit ( 𝜑 → Σ 𝑧 ∈ ( 𝑌 / ) ( ♯ ‘ 𝑧 ) = ( Σ 𝑧 ∈ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) + Σ 𝑧 ∈ ( ( 𝑌 / ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ) )
32 21 5 qshash ( 𝜑 → ( ♯ ‘ 𝑌 ) = Σ 𝑧 ∈ ( 𝑌 / ) ( ♯ ‘ 𝑧 ) )
33 inss1 ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ⊆ ( 𝑌 / )
34 ssfi ( ( ( 𝑌 / ) ∈ Fin ∧ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ⊆ ( 𝑌 / ) ) → ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ∈ Fin )
35 23 33 34 sylancl ( 𝜑 → ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ∈ Fin )
36 ax-1cn 1 ∈ ℂ
37 fsumconst ( ( ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑧 ∈ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) 1 = ( ( ♯ ‘ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ) · 1 ) )
38 35 36 37 sylancl ( 𝜑 → Σ 𝑧 ∈ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) 1 = ( ( ♯ ‘ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ) · 1 ) )
39 elin ( 𝑧 ∈ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ↔ ( 𝑧 ∈ ( 𝑌 / ) ∧ 𝑧 ∈ 𝒫 𝑍 ) )
40 eqid ( 𝑌 / ) = ( 𝑌 / )
41 sseq1 ( [ 𝑤 ] = 𝑧 → ( [ 𝑤 ] 𝑍𝑧𝑍 ) )
42 velpw ( 𝑧 ∈ 𝒫 𝑍𝑧𝑍 )
43 41 42 bitr4di ( [ 𝑤 ] = 𝑧 → ( [ 𝑤 ] 𝑍𝑧 ∈ 𝒫 𝑍 ) )
44 breq1 ( [ 𝑤 ] = 𝑧 → ( [ 𝑤 ] ≈ 1o𝑧 ≈ 1o ) )
45 43 44 imbi12d ( [ 𝑤 ] = 𝑧 → ( ( [ 𝑤 ] 𝑍 → [ 𝑤 ] ≈ 1o ) ↔ ( 𝑧 ∈ 𝒫 𝑍𝑧 ≈ 1o ) ) )
46 21 adantr ( ( 𝜑𝑤𝑌 ) → Er 𝑌 )
47 simpr ( ( 𝜑𝑤𝑌 ) → 𝑤𝑌 )
48 46 47 erref ( ( 𝜑𝑤𝑌 ) → 𝑤 𝑤 )
49 vex 𝑤 ∈ V
50 49 49 elec ( 𝑤 ∈ [ 𝑤 ] 𝑤 𝑤 )
51 48 50 sylibr ( ( 𝜑𝑤𝑌 ) → 𝑤 ∈ [ 𝑤 ] )
52 ssel ( [ 𝑤 ] 𝑍 → ( 𝑤 ∈ [ 𝑤 ] 𝑤𝑍 ) )
53 51 52 syl5com ( ( 𝜑𝑤𝑌 ) → ( [ 𝑤 ] 𝑍𝑤𝑍 ) )
54 1 2 3 4 5 6 7 sylow2alem1 ( ( 𝜑𝑤𝑍 ) → [ 𝑤 ] = { 𝑤 } )
55 49 ensn1 { 𝑤 } ≈ 1o
56 54 55 eqbrtrdi ( ( 𝜑𝑤𝑍 ) → [ 𝑤 ] ≈ 1o )
57 56 ex ( 𝜑 → ( 𝑤𝑍 → [ 𝑤 ] ≈ 1o ) )
58 57 adantr ( ( 𝜑𝑤𝑌 ) → ( 𝑤𝑍 → [ 𝑤 ] ≈ 1o ) )
59 53 58 syld ( ( 𝜑𝑤𝑌 ) → ( [ 𝑤 ] 𝑍 → [ 𝑤 ] ≈ 1o ) )
60 40 45 59 ectocld ( ( 𝜑𝑧 ∈ ( 𝑌 / ) ) → ( 𝑧 ∈ 𝒫 𝑍𝑧 ≈ 1o ) )
61 60 impr ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝑌 / ) ∧ 𝑧 ∈ 𝒫 𝑍 ) ) → 𝑧 ≈ 1o )
62 39 61 sylan2b ( ( 𝜑𝑧 ∈ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ) → 𝑧 ≈ 1o )
63 en1b ( 𝑧 ≈ 1o𝑧 = { 𝑧 } )
64 62 63 sylib ( ( 𝜑𝑧 ∈ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ) → 𝑧 = { 𝑧 } )
65 64 fveq2d ( ( 𝜑𝑧 ∈ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ) → ( ♯ ‘ 𝑧 ) = ( ♯ ‘ { 𝑧 } ) )
66 vuniex 𝑧 ∈ V
67 hashsng ( 𝑧 ∈ V → ( ♯ ‘ { 𝑧 } ) = 1 )
68 66 67 ax-mp ( ♯ ‘ { 𝑧 } ) = 1
69 65 68 eqtrdi ( ( 𝜑𝑧 ∈ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ) → ( ♯ ‘ 𝑧 ) = 1 )
70 69 sumeq2dv ( 𝜑 → Σ 𝑧 ∈ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) = Σ 𝑧 ∈ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) 1 )
71 6 ssrab3 𝑍𝑌
72 ssfi ( ( 𝑌 ∈ Fin ∧ 𝑍𝑌 ) → 𝑍 ∈ Fin )
73 5 71 72 sylancl ( 𝜑𝑍 ∈ Fin )
74 hashcl ( 𝑍 ∈ Fin → ( ♯ ‘ 𝑍 ) ∈ ℕ0 )
75 73 74 syl ( 𝜑 → ( ♯ ‘ 𝑍 ) ∈ ℕ0 )
76 75 nn0cnd ( 𝜑 → ( ♯ ‘ 𝑍 ) ∈ ℂ )
77 76 mulid1d ( 𝜑 → ( ( ♯ ‘ 𝑍 ) · 1 ) = ( ♯ ‘ 𝑍 ) )
78 6 5 rabexd ( 𝜑𝑍 ∈ V )
79 eqid ( 𝑤𝑍 ↦ { 𝑤 } ) = ( 𝑤𝑍 ↦ { 𝑤 } )
80 7 relopabiv Rel
81 relssdmrn ( Rel ⊆ ( dom × ran ) )
82 80 81 ax-mp ⊆ ( dom × ran )
83 erdm ( Er 𝑌 → dom = 𝑌 )
84 21 83 syl ( 𝜑 → dom = 𝑌 )
85 84 5 eqeltrd ( 𝜑 → dom ∈ Fin )
86 errn ( Er 𝑌 → ran = 𝑌 )
87 21 86 syl ( 𝜑 → ran = 𝑌 )
88 87 5 eqeltrd ( 𝜑 → ran ∈ Fin )
89 85 88 xpexd ( 𝜑 → ( dom × ran ) ∈ V )
90 ssexg ( ( ⊆ ( dom × ran ) ∧ ( dom × ran ) ∈ V ) → ∈ V )
91 82 89 90 sylancr ( 𝜑 ∈ V )
92 simpr ( ( 𝜑𝑤𝑍 ) → 𝑤𝑍 )
93 71 92 sselid ( ( 𝜑𝑤𝑍 ) → 𝑤𝑌 )
94 ecelqsg ( ( ∈ V ∧ 𝑤𝑌 ) → [ 𝑤 ] ∈ ( 𝑌 / ) )
95 91 93 94 syl2an2r ( ( 𝜑𝑤𝑍 ) → [ 𝑤 ] ∈ ( 𝑌 / ) )
96 54 95 eqeltrrd ( ( 𝜑𝑤𝑍 ) → { 𝑤 } ∈ ( 𝑌 / ) )
97 snelpwi ( 𝑤𝑍 → { 𝑤 } ∈ 𝒫 𝑍 )
98 97 adantl ( ( 𝜑𝑤𝑍 ) → { 𝑤 } ∈ 𝒫 𝑍 )
99 96 98 elind ( ( 𝜑𝑤𝑍 ) → { 𝑤 } ∈ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) )
100 simpr ( ( 𝜑𝑧 ∈ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ) → 𝑧 ∈ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) )
101 100 elin2d ( ( 𝜑𝑧 ∈ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ) → 𝑧 ∈ 𝒫 𝑍 )
102 101 elpwid ( ( 𝜑𝑧 ∈ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ) → 𝑧𝑍 )
103 64 102 eqsstrrd ( ( 𝜑𝑧 ∈ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ) → { 𝑧 } ⊆ 𝑍 )
104 66 snss ( 𝑧𝑍 ↔ { 𝑧 } ⊆ 𝑍 )
105 103 104 sylibr ( ( 𝜑𝑧 ∈ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ) → 𝑧𝑍 )
106 sneq ( 𝑤 = 𝑧 → { 𝑤 } = { 𝑧 } )
107 106 eqeq2d ( 𝑤 = 𝑧 → ( 𝑧 = { 𝑤 } ↔ 𝑧 = { 𝑧 } ) )
108 64 107 syl5ibrcom ( ( 𝜑𝑧 ∈ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ) → ( 𝑤 = 𝑧𝑧 = { 𝑤 } ) )
109 108 adantrl ( ( 𝜑 ∧ ( 𝑤𝑍𝑧 ∈ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ) ) → ( 𝑤 = 𝑧𝑧 = { 𝑤 } ) )
110 unieq ( 𝑧 = { 𝑤 } → 𝑧 = { 𝑤 } )
111 49 unisn { 𝑤 } = 𝑤
112 110 111 eqtr2di ( 𝑧 = { 𝑤 } → 𝑤 = 𝑧 )
113 109 112 impbid1 ( ( 𝜑 ∧ ( 𝑤𝑍𝑧 ∈ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ) ) → ( 𝑤 = 𝑧𝑧 = { 𝑤 } ) )
114 79 99 105 113 f1o2d ( 𝜑 → ( 𝑤𝑍 ↦ { 𝑤 } ) : 𝑍1-1-onto→ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) )
115 78 114 hasheqf1od ( 𝜑 → ( ♯ ‘ 𝑍 ) = ( ♯ ‘ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ) )
116 115 oveq1d ( 𝜑 → ( ( ♯ ‘ 𝑍 ) · 1 ) = ( ( ♯ ‘ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ) · 1 ) )
117 77 116 eqtr3d ( 𝜑 → ( ♯ ‘ 𝑍 ) = ( ( ♯ ‘ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ) · 1 ) )
118 38 70 117 3eqtr4rd ( 𝜑 → ( ♯ ‘ 𝑍 ) = Σ 𝑧 ∈ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) )
119 118 oveq1d ( 𝜑 → ( ( ♯ ‘ 𝑍 ) + Σ 𝑧 ∈ ( ( 𝑌 / ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ) = ( Σ 𝑧 ∈ ( ( 𝑌 / ) ∩ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) + Σ 𝑧 ∈ ( ( 𝑌 / ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ) )
120 31 32 119 3eqtr4rd ( 𝜑 → ( ( ♯ ‘ 𝑍 ) + Σ 𝑧 ∈ ( ( 𝑌 / ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ) = ( ♯ ‘ 𝑌 ) )
121 hashcl ( 𝑌 ∈ Fin → ( ♯ ‘ 𝑌 ) ∈ ℕ0 )
122 5 121 syl ( 𝜑 → ( ♯ ‘ 𝑌 ) ∈ ℕ0 )
123 122 nn0cnd ( 𝜑 → ( ♯ ‘ 𝑌 ) ∈ ℂ )
124 diffi ( ( 𝑌 / ) ∈ Fin → ( ( 𝑌 / ) ∖ 𝒫 𝑍 ) ∈ Fin )
125 23 124 syl ( 𝜑 → ( ( 𝑌 / ) ∖ 𝒫 𝑍 ) ∈ Fin )
126 eldifi ( 𝑧 ∈ ( ( 𝑌 / ) ∖ 𝒫 𝑍 ) → 𝑧 ∈ ( 𝑌 / ) )
127 126 30 sylan2 ( ( 𝜑𝑧 ∈ ( ( 𝑌 / ) ∖ 𝒫 𝑍 ) ) → ( ♯ ‘ 𝑧 ) ∈ ℂ )
128 125 127 fsumcl ( 𝜑 → Σ 𝑧 ∈ ( ( 𝑌 / ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ∈ ℂ )
129 123 76 128 subaddd ( 𝜑 → ( ( ( ♯ ‘ 𝑌 ) − ( ♯ ‘ 𝑍 ) ) = Σ 𝑧 ∈ ( ( 𝑌 / ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ↔ ( ( ♯ ‘ 𝑍 ) + Σ 𝑧 ∈ ( ( 𝑌 / ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ) = ( ♯ ‘ 𝑌 ) ) )
130 120 129 mpbird ( 𝜑 → ( ( ♯ ‘ 𝑌 ) − ( ♯ ‘ 𝑍 ) ) = Σ 𝑧 ∈ ( ( 𝑌 / ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) )
131 8 130 breqtrrd ( 𝜑𝑃 ∥ ( ( ♯ ‘ 𝑌 ) − ( ♯ ‘ 𝑍 ) ) )