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	⊢ ( 𝜑 → 𝑃 ∥ Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) )