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

Metamath Proof Explorer

Theorem sylow2alem2

Description: Lemma for sylow2a . All the orbits which are not for fixed points have size | G | / | G x | (where G x is the stabilizer subgroup) and thus are powers of P . And since they are all nontrivial (because any orbit which is a singleton is a fixed point), they all divide P , and so does the sum of all of them. (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 sylow2alem2 ( 𝜑 → 𝑃 ∥ Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) )

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 pwfi ⊢ ( 𝑌 ∈ Fin ↔ 𝒫 𝑌 ∈ Fin )
9 5 8 sylib ⊢ ( 𝜑 → 𝒫 𝑌 ∈ Fin )
10 7 1 gaorber ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → ∼ Er 𝑌 )
11 2 10 syl ⊢ ( 𝜑 → ∼ Er 𝑌 )
12 11 qsss ⊢ ( 𝜑 → ( 𝑌 / ∼ ) ⊆ 𝒫 𝑌 )
13 9 12 ssfid ⊢ ( 𝜑 → ( 𝑌 / ∼ ) ∈ Fin )
14 diffi ⊢ ( ( 𝑌 / ∼ ) ∈ Fin → ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ∈ Fin )
15 13 14 syl ⊢ ( 𝜑 → ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ∈ Fin )
16 gagrp ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → 𝐺 ∈ Grp )
17 2 16 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
18 1 pgpfi ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) → ( 𝑃 pGrp 𝐺 ↔ ( 𝑃 ∈ ℙ ∧ ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) ) ) )
19 17 4 18 syl2anc ⊢ ( 𝜑 → ( 𝑃 pGrp 𝐺 ↔ ( 𝑃 ∈ ℙ ∧ ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) ) ) )
20 3 19 mpbid ⊢ ( 𝜑 → ( 𝑃 ∈ ℙ ∧ ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) ) )
21 20 simpld ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
22 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
23 21 22 syl ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
24 eldifi ⊢ ( 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) → 𝑧 ∈ ( 𝑌 / ∼ ) )
25 5 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 / ∼ ) ) → 𝑌 ∈ Fin )
26 12 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 / ∼ ) ) → 𝑧 ∈ 𝒫 𝑌 )
27 26 elpwid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 / ∼ ) ) → 𝑧 ⊆ 𝑌 )
28 25 27 ssfid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 / ∼ ) ) → 𝑧 ∈ Fin )
29 24 28 sylan2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ) → 𝑧 ∈ Fin )
30 hashcl ⊢ ( 𝑧 ∈ Fin → ( ♯ ‘ 𝑧 ) ∈ ℕ0 )
31 29 30 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ) → ( ♯ ‘ 𝑧 ) ∈ ℕ0 )
32 31 nn0zd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ) → ( ♯ ‘ 𝑧 ) ∈ ℤ )
33 eldif ⊢ ( 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ↔ ( 𝑧 ∈ ( 𝑌 / ∼ ) ∧ ¬ 𝑧 ∈ 𝒫 𝑍 ) )
34 eqid ⊢ ( 𝑌 / ∼ ) = ( 𝑌 / ∼ )
35 sseq1 ⊢ ( [ 𝑤 ] ∼ = 𝑧 → ( [ 𝑤 ] ∼ ⊆ 𝑍 ↔ 𝑧 ⊆ 𝑍 ) )
36 velpw ⊢ ( 𝑧 ∈ 𝒫 𝑍 ↔ 𝑧 ⊆ 𝑍 )
37 35 36 bitr4di ⊢ ( [ 𝑤 ] ∼ = 𝑧 → ( [ 𝑤 ] ∼ ⊆ 𝑍 ↔ 𝑧 ∈ 𝒫 𝑍 ) )
38 37 notbid ⊢ ( [ 𝑤 ] ∼ = 𝑧 → ( ¬ [ 𝑤 ] ∼ ⊆ 𝑍 ↔ ¬ 𝑧 ∈ 𝒫 𝑍 ) )
39 fveq2 ⊢ ( [ 𝑤 ] ∼ = 𝑧 → ( ♯ ‘ [ 𝑤 ] ∼ ) = ( ♯ ‘ 𝑧 ) )
40 39 breq2d ⊢ ( [ 𝑤 ] ∼ = 𝑧 → ( 𝑃 ∥ ( ♯ ‘ [ 𝑤 ] ∼ ) ↔ 𝑃 ∥ ( ♯ ‘ 𝑧 ) ) )
41 38 40 imbi12d ⊢ ( [ 𝑤 ] ∼ = 𝑧 → ( ( ¬ [ 𝑤 ] ∼ ⊆ 𝑍 → 𝑃 ∥ ( ♯ ‘ [ 𝑤 ] ∼ ) ) ↔ ( ¬ 𝑧 ∈ 𝒫 𝑍 → 𝑃 ∥ ( ♯ ‘ 𝑧 ) ) ) )
42 21 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → 𝑃 ∈ ℙ )
43 11 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ∼ Er 𝑌 )
44 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → 𝑤 ∈ 𝑌 )
45 43 44 erref ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → 𝑤 ∼ 𝑤 )
46 vex ⊢ 𝑤 ∈ V
47 46 46 elec ⊢ ( 𝑤 ∈ [ 𝑤 ] ∼ ↔ 𝑤 ∼ 𝑤 )
48 45 47 sylibr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → 𝑤 ∈ [ 𝑤 ] ∼ )
49 48 ne0d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → [ 𝑤 ] ∼ ≠ ∅ )
50 11 ecss ⊢ ( 𝜑 → [ 𝑤 ] ∼ ⊆ 𝑌 )
51 5 50 ssfid ⊢ ( 𝜑 → [ 𝑤 ] ∼ ∈ Fin )
52 51 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → [ 𝑤 ] ∼ ∈ Fin )
53 hashnncl ⊢ ( [ 𝑤 ] ∼ ∈ Fin → ( ( ♯ ‘ [ 𝑤 ] ∼ ) ∈ ℕ ↔ [ 𝑤 ] ∼ ≠ ∅ ) )
54 52 53 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( ( ♯ ‘ [ 𝑤 ] ∼ ) ∈ ℕ ↔ [ 𝑤 ] ∼ ≠ ∅ ) )
55 49 54 mpbird ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( ♯ ‘ [ 𝑤 ] ∼ ) ∈ ℕ )
56 pceq0 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ♯ ‘ [ 𝑤 ] ∼ ) ∈ ℕ ) → ( ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) = 0 ↔ ¬ 𝑃 ∥ ( ♯ ‘ [ 𝑤 ] ∼ ) ) )
57 42 55 56 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) = 0 ↔ ¬ 𝑃 ∥ ( ♯ ‘ [ 𝑤 ] ∼ ) ) )
58 oveq2 ⊢ ( ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) = 0 → ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) ) = ( 𝑃 ↑ 0 ) )
59 hashcl ⊢ ( [ 𝑤 ] ∼ ∈ Fin → ( ♯ ‘ [ 𝑤 ] ∼ ) ∈ ℕ0 )
60 51 59 syl ⊢ ( 𝜑 → ( ♯ ‘ [ 𝑤 ] ∼ ) ∈ ℕ0 )
61 60 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ [ 𝑤 ] ∼ ) ∈ ℤ )
62 ssrab2 ⊢ { 𝑣 ∈ 𝑋 ∣ ( 𝑣 ⊕ 𝑤 ) = 𝑤 } ⊆ 𝑋
63 ssfi ⊢ ( ( 𝑋 ∈ Fin ∧ { 𝑣 ∈ 𝑋 ∣ ( 𝑣 ⊕ 𝑤 ) = 𝑤 } ⊆ 𝑋 ) → { 𝑣 ∈ 𝑋 ∣ ( 𝑣 ⊕ 𝑤 ) = 𝑤 } ∈ Fin )
64 4 62 63 sylancl ⊢ ( 𝜑 → { 𝑣 ∈ 𝑋 ∣ ( 𝑣 ⊕ 𝑤 ) = 𝑤 } ∈ Fin )
65 hashcl ⊢ ( { 𝑣 ∈ 𝑋 ∣ ( 𝑣 ⊕ 𝑤 ) = 𝑤 } ∈ Fin → ( ♯ ‘ { 𝑣 ∈ 𝑋 ∣ ( 𝑣 ⊕ 𝑤 ) = 𝑤 } ) ∈ ℕ0 )
66 64 65 syl ⊢ ( 𝜑 → ( ♯ ‘ { 𝑣 ∈ 𝑋 ∣ ( 𝑣 ⊕ 𝑤 ) = 𝑤 } ) ∈ ℕ0 )
67 66 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ { 𝑣 ∈ 𝑋 ∣ ( 𝑣 ⊕ 𝑤 ) = 𝑤 } ) ∈ ℤ )
68 dvdsmul1 ⊢ ( ( ( ♯ ‘ [ 𝑤 ] ∼ ) ∈ ℤ ∧ ( ♯ ‘ { 𝑣 ∈ 𝑋 ∣ ( 𝑣 ⊕ 𝑤 ) = 𝑤 } ) ∈ ℤ ) → ( ♯ ‘ [ 𝑤 ] ∼ ) ∥ ( ( ♯ ‘ [ 𝑤 ] ∼ ) · ( ♯ ‘ { 𝑣 ∈ 𝑋 ∣ ( 𝑣 ⊕ 𝑤 ) = 𝑤 } ) ) )
69 61 67 68 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ [ 𝑤 ] ∼ ) ∥ ( ( ♯ ‘ [ 𝑤 ] ∼ ) · ( ♯ ‘ { 𝑣 ∈ 𝑋 ∣ ( 𝑣 ⊕ 𝑤 ) = 𝑤 } ) ) )
70 69 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( ♯ ‘ [ 𝑤 ] ∼ ) ∥ ( ( ♯ ‘ [ 𝑤 ] ∼ ) · ( ♯ ‘ { 𝑣 ∈ 𝑋 ∣ ( 𝑣 ⊕ 𝑤 ) = 𝑤 } ) ) )
71 2 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) )
72 4 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → 𝑋 ∈ Fin )
73 eqid ⊢ { 𝑣 ∈ 𝑋 ∣ ( 𝑣 ⊕ 𝑤 ) = 𝑤 } = { 𝑣 ∈ 𝑋 ∣ ( 𝑣 ⊕ 𝑤 ) = 𝑤 }
74 eqid ⊢ ( 𝐺 ~QG { 𝑣 ∈ 𝑋 ∣ ( 𝑣 ⊕ 𝑤 ) = 𝑤 } ) = ( 𝐺 ~QG { 𝑣 ∈ 𝑋 ∣ ( 𝑣 ⊕ 𝑤 ) = 𝑤 } )
75 1 73 74 7 orbsta2 ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑤 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ 𝑋 ) = ( ( ♯ ‘ [ 𝑤 ] ∼ ) · ( ♯ ‘ { 𝑣 ∈ 𝑋 ∣ ( 𝑣 ⊕ 𝑤 ) = 𝑤 } ) ) )
76 71 44 72 75 syl21anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( ♯ ‘ 𝑋 ) = ( ( ♯ ‘ [ 𝑤 ] ∼ ) · ( ♯ ‘ { 𝑣 ∈ 𝑋 ∣ ( 𝑣 ⊕ 𝑤 ) = 𝑤 } ) ) )
77 70 76 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( ♯ ‘ [ 𝑤 ] ∼ ) ∥ ( ♯ ‘ 𝑋 ) )
78 20 simprd ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) )
79 78 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) )
80 breq2 ⊢ ( ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) → ( ( ♯ ‘ [ 𝑤 ] ∼ ) ∥ ( ♯ ‘ 𝑋 ) ↔ ( ♯ ‘ [ 𝑤 ] ∼ ) ∥ ( 𝑃 ↑ 𝑛 ) ) )
81 80 biimpcd ⊢ ( ( ♯ ‘ [ 𝑤 ] ∼ ) ∥ ( ♯ ‘ 𝑋 ) → ( ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) → ( ♯ ‘ [ 𝑤 ] ∼ ) ∥ ( 𝑃 ↑ 𝑛 ) ) )
82 81 reximdv ⊢ ( ( ♯ ‘ [ 𝑤 ] ∼ ) ∥ ( ♯ ‘ 𝑋 ) → ( ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) → ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ [ 𝑤 ] ∼ ) ∥ ( 𝑃 ↑ 𝑛 ) ) )
83 77 79 82 sylc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ [ 𝑤 ] ∼ ) ∥ ( 𝑃 ↑ 𝑛 ) )
84 pcprmpw2 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ♯ ‘ [ 𝑤 ] ∼ ) ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ [ 𝑤 ] ∼ ) ∥ ( 𝑃 ↑ 𝑛 ) ↔ ( ♯ ‘ [ 𝑤 ] ∼ ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) ) ) )
85 42 55 84 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ [ 𝑤 ] ∼ ) ∥ ( 𝑃 ↑ 𝑛 ) ↔ ( ♯ ‘ [ 𝑤 ] ∼ ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) ) ) )
86 83 85 mpbid ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( ♯ ‘ [ 𝑤 ] ∼ ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) ) )
87 86 eqcomd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) ) = ( ♯ ‘ [ 𝑤 ] ∼ ) )
88 23 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → 𝑃 ∈ ℤ )
89 88 zcnd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → 𝑃 ∈ ℂ )
90 89 exp0d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( 𝑃 ↑ 0 ) = 1 )
91 hash1 ⊢ ( ♯ ‘ 1o ) = 1
92 90 91 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( 𝑃 ↑ 0 ) = ( ♯ ‘ 1o ) )
93 87 92 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) ) = ( 𝑃 ↑ 0 ) ↔ ( ♯ ‘ [ 𝑤 ] ∼ ) = ( ♯ ‘ 1o ) ) )
94 df1o2 ⊢ 1o = { ∅ }
95 snfi ⊢ { ∅ } ∈ Fin
96 94 95 eqeltri ⊢ 1o ∈ Fin
97 hashen ⊢ ( ( [ 𝑤 ] ∼ ∈ Fin ∧ 1o ∈ Fin ) → ( ( ♯ ‘ [ 𝑤 ] ∼ ) = ( ♯ ‘ 1o ) ↔ [ 𝑤 ] ∼ ≈ 1o ) )
98 52 96 97 sylancl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( ( ♯ ‘ [ 𝑤 ] ∼ ) = ( ♯ ‘ 1o ) ↔ [ 𝑤 ] ∼ ≈ 1o ) )
99 93 98 bitrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) ) = ( 𝑃 ↑ 0 ) ↔ [ 𝑤 ] ∼ ≈ 1o ) )
100 en1b ⊢ ( [ 𝑤 ] ∼ ≈ 1o ↔ [ 𝑤 ] ∼ = { ∪ [ 𝑤 ] ∼ } )
101 99 100 bitrdi ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) ) = ( 𝑃 ↑ 0 ) ↔ [ 𝑤 ] ∼ = { ∪ [ 𝑤 ] ∼ } ) )
102 44 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) ∧ ( ℎ ∈ 𝑋 ∧ [ 𝑤 ] ∼ = { ∪ [ 𝑤 ] ∼ } ) ) → 𝑤 ∈ 𝑌 )
103 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) ∧ ( ℎ ∈ 𝑋 ∧ [ 𝑤 ] ∼ = { ∪ [ 𝑤 ] ∼ } ) ) → ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) )
104 1 gaf ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → ⊕ : ( 𝑋 × 𝑌 ) ⟶ 𝑌 )
105 103 104 syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) ∧ ( ℎ ∈ 𝑋 ∧ [ 𝑤 ] ∼ = { ∪ [ 𝑤 ] ∼ } ) ) → ⊕ : ( 𝑋 × 𝑌 ) ⟶ 𝑌 )
106 simprl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) ∧ ( ℎ ∈ 𝑋 ∧ [ 𝑤 ] ∼ = { ∪ [ 𝑤 ] ∼ } ) ) → ℎ ∈ 𝑋 )
107 105 106 102 fovcdmd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) ∧ ( ℎ ∈ 𝑋 ∧ [ 𝑤 ] ∼ = { ∪ [ 𝑤 ] ∼ } ) ) → ( ℎ ⊕ 𝑤 ) ∈ 𝑌 )
108 eqid ⊢ ( ℎ ⊕ 𝑤 ) = ( ℎ ⊕ 𝑤 )
109 oveq1 ⊢ ( 𝑘 = ℎ → ( 𝑘 ⊕ 𝑤 ) = ( ℎ ⊕ 𝑤 ) )
110 109 eqeq1d ⊢ ( 𝑘 = ℎ → ( ( 𝑘 ⊕ 𝑤 ) = ( ℎ ⊕ 𝑤 ) ↔ ( ℎ ⊕ 𝑤 ) = ( ℎ ⊕ 𝑤 ) ) )
111 110 rspcev ⊢ ( ( ℎ ∈ 𝑋 ∧ ( ℎ ⊕ 𝑤 ) = ( ℎ ⊕ 𝑤 ) ) → ∃ 𝑘 ∈ 𝑋 ( 𝑘 ⊕ 𝑤 ) = ( ℎ ⊕ 𝑤 ) )
112 106 108 111 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) ∧ ( ℎ ∈ 𝑋 ∧ [ 𝑤 ] ∼ = { ∪ [ 𝑤 ] ∼ } ) ) → ∃ 𝑘 ∈ 𝑋 ( 𝑘 ⊕ 𝑤 ) = ( ℎ ⊕ 𝑤 ) )
113 7 gaorb ⊢ ( 𝑤 ∼ ( ℎ ⊕ 𝑤 ) ↔ ( 𝑤 ∈ 𝑌 ∧ ( ℎ ⊕ 𝑤 ) ∈ 𝑌 ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ⊕ 𝑤 ) = ( ℎ ⊕ 𝑤 ) ) )
114 102 107 112 113 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) ∧ ( ℎ ∈ 𝑋 ∧ [ 𝑤 ] ∼ = { ∪ [ 𝑤 ] ∼ } ) ) → 𝑤 ∼ ( ℎ ⊕ 𝑤 ) )
115 ovex ⊢ ( ℎ ⊕ 𝑤 ) ∈ V
116 115 46 elec ⊢ ( ( ℎ ⊕ 𝑤 ) ∈ [ 𝑤 ] ∼ ↔ 𝑤 ∼ ( ℎ ⊕ 𝑤 ) )
117 114 116 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) ∧ ( ℎ ∈ 𝑋 ∧ [ 𝑤 ] ∼ = { ∪ [ 𝑤 ] ∼ } ) ) → ( ℎ ⊕ 𝑤 ) ∈ [ 𝑤 ] ∼ )
118 simprr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) ∧ ( ℎ ∈ 𝑋 ∧ [ 𝑤 ] ∼ = { ∪ [ 𝑤 ] ∼ } ) ) → [ 𝑤 ] ∼ = { ∪ [ 𝑤 ] ∼ } )
119 117 118 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) ∧ ( ℎ ∈ 𝑋 ∧ [ 𝑤 ] ∼ = { ∪ [ 𝑤 ] ∼ } ) ) → ( ℎ ⊕ 𝑤 ) ∈ { ∪ [ 𝑤 ] ∼ } )
120 115 elsn ⊢ ( ( ℎ ⊕ 𝑤 ) ∈ { ∪ [ 𝑤 ] ∼ } ↔ ( ℎ ⊕ 𝑤 ) = ∪ [ 𝑤 ] ∼ )
121 119 120 sylib ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) ∧ ( ℎ ∈ 𝑋 ∧ [ 𝑤 ] ∼ = { ∪ [ 𝑤 ] ∼ } ) ) → ( ℎ ⊕ 𝑤 ) = ∪ [ 𝑤 ] ∼ )
122 48 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) ∧ ( ℎ ∈ 𝑋 ∧ [ 𝑤 ] ∼ = { ∪ [ 𝑤 ] ∼ } ) ) → 𝑤 ∈ [ 𝑤 ] ∼ )
123 122 118 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) ∧ ( ℎ ∈ 𝑋 ∧ [ 𝑤 ] ∼ = { ∪ [ 𝑤 ] ∼ } ) ) → 𝑤 ∈ { ∪ [ 𝑤 ] ∼ } )
124 46 elsn ⊢ ( 𝑤 ∈ { ∪ [ 𝑤 ] ∼ } ↔ 𝑤 = ∪ [ 𝑤 ] ∼ )
125 123 124 sylib ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) ∧ ( ℎ ∈ 𝑋 ∧ [ 𝑤 ] ∼ = { ∪ [ 𝑤 ] ∼ } ) ) → 𝑤 = ∪ [ 𝑤 ] ∼ )
126 121 125 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) ∧ ( ℎ ∈ 𝑋 ∧ [ 𝑤 ] ∼ = { ∪ [ 𝑤 ] ∼ } ) ) → ( ℎ ⊕ 𝑤 ) = 𝑤 )
127 126 expr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) ∧ ℎ ∈ 𝑋 ) → ( [ 𝑤 ] ∼ = { ∪ [ 𝑤 ] ∼ } → ( ℎ ⊕ 𝑤 ) = 𝑤 ) )
128 127 ralrimdva ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( [ 𝑤 ] ∼ = { ∪ [ 𝑤 ] ∼ } → ∀ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑤 ) = 𝑤 ) )
129 101 128 sylbid ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) ) = ( 𝑃 ↑ 0 ) → ∀ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑤 ) = 𝑤 ) )
130 58 129 syl5 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( ( 𝑃 pCnt ( ♯ ‘ [ 𝑤 ] ∼ ) ) = 0 → ∀ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑤 ) = 𝑤 ) )
131 57 130 sylbird ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( ¬ 𝑃 ∥ ( ♯ ‘ [ 𝑤 ] ∼ ) → ∀ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑤 ) = 𝑤 ) )
132 oveq2 ⊢ ( 𝑢 = 𝑤 → ( ℎ ⊕ 𝑢 ) = ( ℎ ⊕ 𝑤 ) )
133 id ⊢ ( 𝑢 = 𝑤 → 𝑢 = 𝑤 )
134 132 133 eqeq12d ⊢ ( 𝑢 = 𝑤 → ( ( ℎ ⊕ 𝑢 ) = 𝑢 ↔ ( ℎ ⊕ 𝑤 ) = 𝑤 ) )
135 134 ralbidv ⊢ ( 𝑢 = 𝑤 → ( ∀ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑢 ↔ ∀ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑤 ) = 𝑤 ) )
136 135 6 elrab2 ⊢ ( 𝑤 ∈ 𝑍 ↔ ( 𝑤 ∈ 𝑌 ∧ ∀ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑤 ) = 𝑤 ) )
137 136 baib ⊢ ( 𝑤 ∈ 𝑌 → ( 𝑤 ∈ 𝑍 ↔ ∀ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑤 ) = 𝑤 ) )
138 137 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( 𝑤 ∈ 𝑍 ↔ ∀ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑤 ) = 𝑤 ) )
139 131 138 sylibrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( ¬ 𝑃 ∥ ( ♯ ‘ [ 𝑤 ] ∼ ) → 𝑤 ∈ 𝑍 ) )
140 1 2 3 4 5 6 7 sylow2alem1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → [ 𝑤 ] ∼ = { 𝑤 } )
141 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → 𝑤 ∈ 𝑍 )
142 141 snssd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → { 𝑤 } ⊆ 𝑍 )
143 140 142 eqsstrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → [ 𝑤 ] ∼ ⊆ 𝑍 )
144 143 ex ⊢ ( 𝜑 → ( 𝑤 ∈ 𝑍 → [ 𝑤 ] ∼ ⊆ 𝑍 ) )
145 144 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( 𝑤 ∈ 𝑍 → [ 𝑤 ] ∼ ⊆ 𝑍 ) )
146 139 145 syld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( ¬ 𝑃 ∥ ( ♯ ‘ [ 𝑤 ] ∼ ) → [ 𝑤 ] ∼ ⊆ 𝑍 ) )
147 146 con1d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( ¬ [ 𝑤 ] ∼ ⊆ 𝑍 → 𝑃 ∥ ( ♯ ‘ [ 𝑤 ] ∼ ) ) )
148 34 41 147 ectocld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 / ∼ ) ) → ( ¬ 𝑧 ∈ 𝒫 𝑍 → 𝑃 ∥ ( ♯ ‘ 𝑧 ) ) )
149 148 impr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝑌 / ∼ ) ∧ ¬ 𝑧 ∈ 𝒫 𝑍 ) ) → 𝑃 ∥ ( ♯ ‘ 𝑧 ) )
150 33 149 sylan2b ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ) → 𝑃 ∥ ( ♯ ‘ 𝑧 ) )
151 15 23 32 150 fsumdvds ⊢ ( 𝜑 → 𝑃 ∥ Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) )