Metamath Proof Explorer


Theorem sylow3lem3

Description: Lemma for sylow3 , first part. The number of Sylow subgroups is the same as the index (number of cosets) of the normalizer of the Sylow subgroup K . (Contributed by Mario Carneiro, 19-Jan-2015)

Ref Expression
Hypotheses sylow3.x 𝑋 = ( Base ‘ 𝐺 )
sylow3.g ( 𝜑𝐺 ∈ Grp )
sylow3.xf ( 𝜑𝑋 ∈ Fin )
sylow3.p ( 𝜑𝑃 ∈ ℙ )
sylow3lem1.a + = ( +g𝐺 )
sylow3lem1.d = ( -g𝐺 )
sylow3lem1.m = ( 𝑥𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧𝑦 ↦ ( ( 𝑥 + 𝑧 ) 𝑥 ) ) )
sylow3lem2.k ( 𝜑𝐾 ∈ ( 𝑃 pSyl 𝐺 ) )
sylow3lem2.h 𝐻 = { 𝑢𝑋 ∣ ( 𝑢 𝐾 ) = 𝐾 }
sylow3lem2.n 𝑁 = { 𝑥𝑋 ∣ ∀ 𝑦𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝐾 ↔ ( 𝑦 + 𝑥 ) ∈ 𝐾 ) }
Assertion sylow3lem3 ( 𝜑 → ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) = ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 sylow3.x 𝑋 = ( Base ‘ 𝐺 )
2 sylow3.g ( 𝜑𝐺 ∈ Grp )
3 sylow3.xf ( 𝜑𝑋 ∈ Fin )
4 sylow3.p ( 𝜑𝑃 ∈ ℙ )
5 sylow3lem1.a + = ( +g𝐺 )
6 sylow3lem1.d = ( -g𝐺 )
7 sylow3lem1.m = ( 𝑥𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧𝑦 ↦ ( ( 𝑥 + 𝑧 ) 𝑥 ) ) )
8 sylow3lem2.k ( 𝜑𝐾 ∈ ( 𝑃 pSyl 𝐺 ) )
9 sylow3lem2.h 𝐻 = { 𝑢𝑋 ∣ ( 𝑢 𝐾 ) = 𝐾 }
10 sylow3lem2.n 𝑁 = { 𝑥𝑋 ∣ ∀ 𝑦𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝐾 ↔ ( 𝑦 + 𝑥 ) ∈ 𝐾 ) }
11 pwfi ( 𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin )
12 3 11 sylib ( 𝜑 → 𝒫 𝑋 ∈ Fin )
13 slwsubg ( 𝑥 ∈ ( 𝑃 pSyl 𝐺 ) → 𝑥 ∈ ( SubGrp ‘ 𝐺 ) )
14 1 subgss ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) → 𝑥𝑋 )
15 13 14 syl ( 𝑥 ∈ ( 𝑃 pSyl 𝐺 ) → 𝑥𝑋 )
16 13 15 elpwd ( 𝑥 ∈ ( 𝑃 pSyl 𝐺 ) → 𝑥 ∈ 𝒫 𝑋 )
17 16 ssriv ( 𝑃 pSyl 𝐺 ) ⊆ 𝒫 𝑋
18 ssfi ( ( 𝒫 𝑋 ∈ Fin ∧ ( 𝑃 pSyl 𝐺 ) ⊆ 𝒫 𝑋 ) → ( 𝑃 pSyl 𝐺 ) ∈ Fin )
19 12 17 18 sylancl ( 𝜑 → ( 𝑃 pSyl 𝐺 ) ∈ Fin )
20 hashcl ( ( 𝑃 pSyl 𝐺 ) ∈ Fin → ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) ∈ ℕ0 )
21 19 20 syl ( 𝜑 → ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) ∈ ℕ0 )
22 21 nn0cnd ( 𝜑 → ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) ∈ ℂ )
23 10 1 5 nmzsubg ( 𝐺 ∈ Grp → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
24 eqid ( 𝐺 ~QG 𝑁 ) = ( 𝐺 ~QG 𝑁 )
25 1 24 eqger ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ~QG 𝑁 ) Er 𝑋 )
26 2 23 25 3syl ( 𝜑 → ( 𝐺 ~QG 𝑁 ) Er 𝑋 )
27 26 qsss ( 𝜑 → ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ⊆ 𝒫 𝑋 )
28 12 27 ssfid ( 𝜑 → ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ∈ Fin )
29 hashcl ( ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ∈ Fin → ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) ∈ ℕ0 )
30 28 29 syl ( 𝜑 → ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) ∈ ℕ0 )
31 30 nn0cnd ( 𝜑 → ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) ∈ ℂ )
32 2 23 syl ( 𝜑𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
33 eqid ( 0g𝐺 ) = ( 0g𝐺 )
34 33 subg0cl ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g𝐺 ) ∈ 𝑁 )
35 ne0i ( ( 0g𝐺 ) ∈ 𝑁𝑁 ≠ ∅ )
36 32 34 35 3syl ( 𝜑𝑁 ≠ ∅ )
37 1 subgss ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → 𝑁𝑋 )
38 2 23 37 3syl ( 𝜑𝑁𝑋 )
39 3 38 ssfid ( 𝜑𝑁 ∈ Fin )
40 hashnncl ( 𝑁 ∈ Fin → ( ( ♯ ‘ 𝑁 ) ∈ ℕ ↔ 𝑁 ≠ ∅ ) )
41 39 40 syl ( 𝜑 → ( ( ♯ ‘ 𝑁 ) ∈ ℕ ↔ 𝑁 ≠ ∅ ) )
42 36 41 mpbird ( 𝜑 → ( ♯ ‘ 𝑁 ) ∈ ℕ )
43 42 nncnd ( 𝜑 → ( ♯ ‘ 𝑁 ) ∈ ℂ )
44 42 nnne0d ( 𝜑 → ( ♯ ‘ 𝑁 ) ≠ 0 )
45 1 2 3 4 5 6 7 sylow3lem1 ( 𝜑 ∈ ( 𝐺 GrpAct ( 𝑃 pSyl 𝐺 ) ) )
46 eqid ( 𝐺 ~QG 𝐻 ) = ( 𝐺 ~QG 𝐻 )
47 eqid { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔𝑋 ( 𝑔 𝑥 ) = 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔𝑋 ( 𝑔 𝑥 ) = 𝑦 ) }
48 1 9 46 47 orbsta2 ( ( ( ∈ ( 𝐺 GrpAct ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ 𝑋 ) = ( ( ♯ ‘ [ 𝐾 ] { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔𝑋 ( 𝑔 𝑥 ) = 𝑦 ) } ) · ( ♯ ‘ 𝐻 ) ) )
49 45 8 3 48 syl21anc ( 𝜑 → ( ♯ ‘ 𝑋 ) = ( ( ♯ ‘ [ 𝐾 ] { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔𝑋 ( 𝑔 𝑥 ) = 𝑦 ) } ) · ( ♯ ‘ 𝐻 ) ) )
50 1 24 32 3 lagsubg2 ( 𝜑 → ( ♯ ‘ 𝑋 ) = ( ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) · ( ♯ ‘ 𝑁 ) ) )
51 47 1 gaorber ( ∈ ( 𝐺 GrpAct ( 𝑃 pSyl 𝐺 ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔𝑋 ( 𝑔 𝑥 ) = 𝑦 ) } Er ( 𝑃 pSyl 𝐺 ) )
52 45 51 syl ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔𝑋 ( 𝑔 𝑥 ) = 𝑦 ) } Er ( 𝑃 pSyl 𝐺 ) )
53 52 ecss ( 𝜑 → [ 𝐾 ] { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔𝑋 ( 𝑔 𝑥 ) = 𝑦 ) } ⊆ ( 𝑃 pSyl 𝐺 ) )
54 8 adantr ( ( 𝜑 ∈ ( 𝑃 pSyl 𝐺 ) ) → 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) )
55 simpr ( ( 𝜑 ∈ ( 𝑃 pSyl 𝐺 ) ) → ∈ ( 𝑃 pSyl 𝐺 ) )
56 3 adantr ( ( 𝜑 ∈ ( 𝑃 pSyl 𝐺 ) ) → 𝑋 ∈ Fin )
57 1 56 55 54 5 6 sylow2 ( ( 𝜑 ∈ ( 𝑃 pSyl 𝐺 ) ) → ∃ 𝑢𝑋 = ran ( 𝑧𝐾 ↦ ( ( 𝑢 + 𝑧 ) 𝑢 ) ) )
58 eqcom ( ( 𝑢 𝐾 ) = = ( 𝑢 𝐾 ) )
59 simpr ( ( ( 𝜑 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑢𝑋 ) → 𝑢𝑋 )
60 54 adantr ( ( ( 𝜑 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑢𝑋 ) → 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) )
61 mptexg ( 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) → ( 𝑧𝐾 ↦ ( ( 𝑢 + 𝑧 ) 𝑢 ) ) ∈ V )
62 rnexg ( ( 𝑧𝐾 ↦ ( ( 𝑢 + 𝑧 ) 𝑢 ) ) ∈ V → ran ( 𝑧𝐾 ↦ ( ( 𝑢 + 𝑧 ) 𝑢 ) ) ∈ V )
63 60 61 62 3syl ( ( ( 𝜑 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑢𝑋 ) → ran ( 𝑧𝐾 ↦ ( ( 𝑢 + 𝑧 ) 𝑢 ) ) ∈ V )
64 simpr ( ( 𝑥 = 𝑢𝑦 = 𝐾 ) → 𝑦 = 𝐾 )
65 simpl ( ( 𝑥 = 𝑢𝑦 = 𝐾 ) → 𝑥 = 𝑢 )
66 65 oveq1d ( ( 𝑥 = 𝑢𝑦 = 𝐾 ) → ( 𝑥 + 𝑧 ) = ( 𝑢 + 𝑧 ) )
67 66 65 oveq12d ( ( 𝑥 = 𝑢𝑦 = 𝐾 ) → ( ( 𝑥 + 𝑧 ) 𝑥 ) = ( ( 𝑢 + 𝑧 ) 𝑢 ) )
68 64 67 mpteq12dv ( ( 𝑥 = 𝑢𝑦 = 𝐾 ) → ( 𝑧𝑦 ↦ ( ( 𝑥 + 𝑧 ) 𝑥 ) ) = ( 𝑧𝐾 ↦ ( ( 𝑢 + 𝑧 ) 𝑢 ) ) )
69 68 rneqd ( ( 𝑥 = 𝑢𝑦 = 𝐾 ) → ran ( 𝑧𝑦 ↦ ( ( 𝑥 + 𝑧 ) 𝑥 ) ) = ran ( 𝑧𝐾 ↦ ( ( 𝑢 + 𝑧 ) 𝑢 ) ) )
70 69 7 ovmpoga ( ( 𝑢𝑋𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ ran ( 𝑧𝐾 ↦ ( ( 𝑢 + 𝑧 ) 𝑢 ) ) ∈ V ) → ( 𝑢 𝐾 ) = ran ( 𝑧𝐾 ↦ ( ( 𝑢 + 𝑧 ) 𝑢 ) ) )
71 59 60 63 70 syl3anc ( ( ( 𝜑 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑢𝑋 ) → ( 𝑢 𝐾 ) = ran ( 𝑧𝐾 ↦ ( ( 𝑢 + 𝑧 ) 𝑢 ) ) )
72 71 eqeq2d ( ( ( 𝜑 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑢𝑋 ) → ( = ( 𝑢 𝐾 ) ↔ = ran ( 𝑧𝐾 ↦ ( ( 𝑢 + 𝑧 ) 𝑢 ) ) ) )
73 58 72 syl5bb ( ( ( 𝜑 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑢𝑋 ) → ( ( 𝑢 𝐾 ) = = ran ( 𝑧𝐾 ↦ ( ( 𝑢 + 𝑧 ) 𝑢 ) ) ) )
74 73 rexbidva ( ( 𝜑 ∈ ( 𝑃 pSyl 𝐺 ) ) → ( ∃ 𝑢𝑋 ( 𝑢 𝐾 ) = ↔ ∃ 𝑢𝑋 = ran ( 𝑧𝐾 ↦ ( ( 𝑢 + 𝑧 ) 𝑢 ) ) ) )
75 57 74 mpbird ( ( 𝜑 ∈ ( 𝑃 pSyl 𝐺 ) ) → ∃ 𝑢𝑋 ( 𝑢 𝐾 ) = )
76 47 gaorb ( 𝐾 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔𝑋 ( 𝑔 𝑥 ) = 𝑦 ) } ↔ ( 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ ∈ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑢𝑋 ( 𝑢 𝐾 ) = ) )
77 54 55 75 76 syl3anbrc ( ( 𝜑 ∈ ( 𝑃 pSyl 𝐺 ) ) → 𝐾 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔𝑋 ( 𝑔 𝑥 ) = 𝑦 ) } )
78 elecg ( ( ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ) → ( ∈ [ 𝐾 ] { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔𝑋 ( 𝑔 𝑥 ) = 𝑦 ) } ↔ 𝐾 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔𝑋 ( 𝑔 𝑥 ) = 𝑦 ) } ) )
79 55 54 78 syl2anc ( ( 𝜑 ∈ ( 𝑃 pSyl 𝐺 ) ) → ( ∈ [ 𝐾 ] { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔𝑋 ( 𝑔 𝑥 ) = 𝑦 ) } ↔ 𝐾 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔𝑋 ( 𝑔 𝑥 ) = 𝑦 ) } ) )
80 77 79 mpbird ( ( 𝜑 ∈ ( 𝑃 pSyl 𝐺 ) ) → ∈ [ 𝐾 ] { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔𝑋 ( 𝑔 𝑥 ) = 𝑦 ) } )
81 53 80 eqelssd ( 𝜑 → [ 𝐾 ] { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔𝑋 ( 𝑔 𝑥 ) = 𝑦 ) } = ( 𝑃 pSyl 𝐺 ) )
82 81 fveq2d ( 𝜑 → ( ♯ ‘ [ 𝐾 ] { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔𝑋 ( 𝑔 𝑥 ) = 𝑦 ) } ) = ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) )
83 1 2 3 4 5 6 7 8 9 10 sylow3lem2 ( 𝜑𝐻 = 𝑁 )
84 83 fveq2d ( 𝜑 → ( ♯ ‘ 𝐻 ) = ( ♯ ‘ 𝑁 ) )
85 82 84 oveq12d ( 𝜑 → ( ( ♯ ‘ [ 𝐾 ] { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔𝑋 ( 𝑔 𝑥 ) = 𝑦 ) } ) · ( ♯ ‘ 𝐻 ) ) = ( ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) · ( ♯ ‘ 𝑁 ) ) )
86 49 50 85 3eqtr3rd ( 𝜑 → ( ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) · ( ♯ ‘ 𝑁 ) ) = ( ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) · ( ♯ ‘ 𝑁 ) ) )
87 22 31 43 44 86 mulcan2ad ( 𝜑 → ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) = ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) )