This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( 𝑃 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 𝑁 ) ) ) )