sylow2alem2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > sylow2alem2		Structured version Visualization version GIF version

Theorem sylow2alem2 17856

Description: Lemma for sylow2a 17857. All the orbits which are not for fixed points have size ∣ 𝐺 ∣ / ∣ 𝐺𝑥 ∣ (where 𝐺𝑥 is the stabilizer subgroup) and thus are powers of 𝑃. And since they are all nontrivial (because any orbit which is a singleton is a fixed point), they all divide 𝑃, and so does the sum of all of them. (Contributed by Mario Carneiro, 17-Jan-2015.)

**Hypotheses**
Ref	Expression
sylow2a.x	⊢ 𝑋 = (Base‘𝐺)
sylow2a.m	⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑌))
sylow2a.p	⊢ (𝜑 → 𝑃 pGrp 𝐺)
sylow2a.f	⊢ (𝜑 → 𝑋 ∈ Fin)
sylow2a.y	⊢ (𝜑 → 𝑌 ∈ Fin)
sylow2a.z	⊢ 𝑍 = {𝑢 ∈ 𝑌 ∣ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑢) = 𝑢}
sylow2a.r	⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}

**Assertion**
Ref	Expression
sylow2alem2	⊢ (𝜑 → 𝑃 ∥ Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(#‘𝑧))

Distinct variable groups: 𝑧,ℎ, ∼ 𝑔,ℎ,𝑢,𝑥,𝑦 𝑔,𝐺,𝑥,𝑦 𝑧,𝑃 ⊕ ,𝑔,ℎ,𝑢,𝑥,𝑦 𝑔,𝑋,ℎ,𝑢,𝑥,𝑦 𝑧,𝑍 𝜑,ℎ,𝑧 𝑧,𝑔,𝑌,ℎ,𝑢,𝑥,𝑦 Allowed substitution hints: 𝜑(𝑥,𝑦,𝑢,𝑔) 𝑃(𝑥,𝑦,𝑢,𝑔,ℎ) ⊕ (𝑧) ∼ (𝑥,𝑦,𝑢,𝑔) 𝐺(𝑧,𝑢,ℎ) 𝑋(𝑧) 𝑍(𝑥,𝑦,𝑢,𝑔,ℎ)

Proof of Theorem sylow2alem2 Dummy variables 𝑘 𝑛 𝑤 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sylow2a.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ Fin)
2		pwfi 8144	. . . . 5 ⊢ (𝑌 ∈ Fin ↔ 𝒫 𝑌 ∈ Fin)
3	1, 2	sylib 207	. . . 4 ⊢ (𝜑 → 𝒫 𝑌 ∈ Fin)
4		sylow2a.m	. . . . . 6 ⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑌))
5		sylow2a.r	. . . . . . 7 ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}
6		sylow2a.x	. . . . . . 7 ⊢ 𝑋 = (Base‘𝐺)
7	5, 6	gaorber 17564	. . . . . 6 ⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → ∼ Er 𝑌)
8	4, 7	syl 17	. . . . 5 ⊢ (𝜑 → ∼ Er 𝑌)
9	8	qsss 7695	. . . 4 ⊢ (𝜑 → (𝑌 / ∼ ) ⊆ 𝒫 𝑌)
10		ssfi 8065	. . . 4 ⊢ ((𝒫 𝑌 ∈ Fin ∧ (𝑌 / ∼ ) ⊆ 𝒫 𝑌) → (𝑌 / ∼ ) ∈ Fin)
11	3, 9, 10	syl2anc 691	. . 3 ⊢ (𝜑 → (𝑌 / ∼ ) ∈ Fin)
12		diffi 8077	. . 3 ⊢ ((𝑌 / ∼ ) ∈ Fin → ((𝑌 / ∼ ) ∖ 𝒫 𝑍) ∈ Fin)
13	11, 12	syl 17	. 2 ⊢ (𝜑 → ((𝑌 / ∼ ) ∖ 𝒫 𝑍) ∈ Fin)
14		sylow2a.p	. . . . 5 ⊢ (𝜑 → 𝑃 pGrp 𝐺)
15		gagrp 17548	. . . . . . 7 ⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → 𝐺 ∈ Grp)
16	4, 15	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ Grp)
17		sylow2a.f	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ Fin)
18	6	pgpfi 17843	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) → (𝑃 pGrp 𝐺 ↔ (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ₀ (#‘𝑋) = (𝑃↑𝑛))))
19	16, 17, 18	syl2anc 691	. . . . 5 ⊢ (𝜑 → (𝑃 pGrp 𝐺 ↔ (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ₀ (#‘𝑋) = (𝑃↑𝑛))))
20	14, 19	mpbid 221	. . . 4 ⊢ (𝜑 → (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ₀ (#‘𝑋) = (𝑃↑𝑛)))
21	20	simpld 474	. . 3 ⊢ (𝜑 → 𝑃 ∈ ℙ)
22		prmz 15227	. . 3 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
23	21, 22	syl 17	. 2 ⊢ (𝜑 → 𝑃 ∈ ℤ)
24		eldifi 3694	. . . . 5 ⊢ (𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍) → 𝑧 ∈ (𝑌 / ∼ ))
25	1	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑌 ∈ Fin)
26	9	sselda 3568	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑧 ∈ 𝒫 𝑌)
27	26	elpwid 4118	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑧 ⊆ 𝑌)
28		ssfi 8065	. . . . . 6 ⊢ ((𝑌 ∈ Fin ∧ 𝑧 ⊆ 𝑌) → 𝑧 ∈ Fin)
29	25, 27, 28	syl2anc 691	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑧 ∈ Fin)
30	24, 29	sylan2 490	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)) → 𝑧 ∈ Fin)
31		hashcl 13009	. . . 4 ⊢ (𝑧 ∈ Fin → (#‘𝑧) ∈ ℕ₀)
32	30, 31	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)) → (#‘𝑧) ∈ ℕ₀)
33	32	nn0zd 11356	. 2 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)) → (#‘𝑧) ∈ ℤ)
34		eldif 3550	. . 3 ⊢ (𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍) ↔ (𝑧 ∈ (𝑌 / ∼ ) ∧ ¬ 𝑧 ∈ 𝒫 𝑍))
35		eqid 2610	. . . . 5 ⊢ (𝑌 / ∼ ) = (𝑌 / ∼ )
36		sseq1 3589	. . . . . . . 8 ⊢ ([𝑤] ∼ = 𝑧 → ([𝑤] ∼ ⊆ 𝑍 ↔ 𝑧 ⊆ 𝑍))
37		selpw 4115	. . . . . . . 8 ⊢ (𝑧 ∈ 𝒫 𝑍 ↔ 𝑧 ⊆ 𝑍)
38	36, 37	syl6bbr 277	. . . . . . 7 ⊢ ([𝑤] ∼ = 𝑧 → ([𝑤] ∼ ⊆ 𝑍 ↔ 𝑧 ∈ 𝒫 𝑍))
39	38	notbid 307	. . . . . 6 ⊢ ([𝑤] ∼ = 𝑧 → (¬ [𝑤] ∼ ⊆ 𝑍 ↔ ¬ 𝑧 ∈ 𝒫 𝑍))
40		fveq2 6103	. . . . . . 7 ⊢ ([𝑤] ∼ = 𝑧 → (#‘[𝑤] ∼ ) = (#‘𝑧))
41	40	breq2d 4595	. . . . . 6 ⊢ ([𝑤] ∼ = 𝑧 → (𝑃 ∥ (#‘[𝑤] ∼ ) ↔ 𝑃 ∥ (#‘𝑧)))
42	39, 41	imbi12d 333	. . . . 5 ⊢ ([𝑤] ∼ = 𝑧 → ((¬ [𝑤] ∼ ⊆ 𝑍 → 𝑃 ∥ (#‘[𝑤] ∼ )) ↔ (¬ 𝑧 ∈ 𝒫 𝑍 → 𝑃 ∥ (#‘𝑧))))
43	21	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑃 ∈ ℙ)
44	8	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ∼ Er 𝑌)
45		simpr 476	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑤 ∈ 𝑌)
46	44, 45	erref 7649	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑤 ∼ 𝑤)
47		vex 3176	. . . . . . . . . . . . . 14 ⊢ 𝑤 ∈ V
48	47, 47	elec 7673	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ [𝑤] ∼ ↔ 𝑤 ∼ 𝑤)
49	46, 48	sylibr 223	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑤 ∈ [𝑤] ∼ )
50		ne0i 3880	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ [𝑤] ∼ → [𝑤] ∼ ≠ ∅)
51	49, 50	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → [𝑤] ∼ ≠ ∅)
52	8	ecss 7675	. . . . . . . . . . . . . 14 ⊢ (𝜑 → [𝑤] ∼ ⊆ 𝑌)
53		ssfi 8065	. . . . . . . . . . . . . 14 ⊢ ((𝑌 ∈ Fin ∧ [𝑤] ∼ ⊆ 𝑌) → [𝑤] ∼ ∈ Fin)
54	1, 52, 53	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (𝜑 → [𝑤] ∼ ∈ Fin)
55	54	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → [𝑤] ∼ ∈ Fin)
56		hashnncl 13018	. . . . . . . . . . . 12 ⊢ ([𝑤] ∼ ∈ Fin → ((#‘[𝑤] ∼ ) ∈ ℕ ↔ [𝑤] ∼ ≠ ∅))
57	55, 56	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ((#‘[𝑤] ∼ ) ∈ ℕ ↔ [𝑤] ∼ ≠ ∅))
58	51, 57	mpbird 246	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (#‘[𝑤] ∼ ) ∈ ℕ)
59		pceq0 15413	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ (#‘[𝑤] ∼ ) ∈ ℕ) → ((𝑃 pCnt (#‘[𝑤] ∼ )) = 0 ↔ ¬ 𝑃 ∥ (#‘[𝑤] ∼ )))
60	43, 58, 59	syl2anc 691	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ((𝑃 pCnt (#‘[𝑤] ∼ )) = 0 ↔ ¬ 𝑃 ∥ (#‘[𝑤] ∼ )))
61		oveq2 6557	. . . . . . . . . 10 ⊢ ((𝑃 pCnt (#‘[𝑤] ∼ )) = 0 → (𝑃↑(𝑃 pCnt (#‘[𝑤] ∼ ))) = (𝑃↑0))
62		hashcl 13009	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ([𝑤] ∼ ∈ Fin → (#‘[𝑤] ∼ ) ∈ ℕ₀)
63	54, 62	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (#‘[𝑤] ∼ ) ∈ ℕ₀)
64	63	nn0zd 11356	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (#‘[𝑤] ∼ ) ∈ ℤ)
65		ssrab2 3650	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤} ⊆ 𝑋
66		ssfi 8065	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑋 ∈ Fin ∧ {𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤} ⊆ 𝑋) → {𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤} ∈ Fin)
67	17, 65, 66	sylancl 693	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → {𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤} ∈ Fin)
68		hashcl 13009	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤} ∈ Fin → (#‘{𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤}) ∈ ℕ₀)
69	67, 68	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (#‘{𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤}) ∈ ℕ₀)
70	69	nn0zd 11356	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (#‘{𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤}) ∈ ℤ)
71		dvdsmul1 14841	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((#‘[𝑤] ∼ ) ∈ ℤ ∧ (#‘{𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤}) ∈ ℤ) → (#‘[𝑤] ∼ ) ∥ ((#‘[𝑤] ∼ ) · (#‘{𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤})))
72	64, 70, 71	syl2anc 691	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (#‘[𝑤] ∼ ) ∥ ((#‘[𝑤] ∼ ) · (#‘{𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤})))
73	72	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (#‘[𝑤] ∼ ) ∥ ((#‘[𝑤] ∼ ) · (#‘{𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤})))
74	4	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ⊕ ∈ (𝐺 GrpAct 𝑌))
75	17	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑋 ∈ Fin)
76		eqid 2610	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤} = {𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤}
77		eqid 2610	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺 ~_QG {𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤}) = (𝐺 ~_QG {𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤})
78	6, 76, 77, 5	orbsta2 17570	. . . . . . . . . . . . . . . . . . 19 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑤 ∈ 𝑌) ∧ 𝑋 ∈ Fin) → (#‘𝑋) = ((#‘[𝑤] ∼ ) · (#‘{𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤})))
79	74, 45, 75, 78	syl21anc 1317	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (#‘𝑋) = ((#‘[𝑤] ∼ ) · (#‘{𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤})))
80	73, 79	breqtrrd 4611	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (#‘[𝑤] ∼ ) ∥ (#‘𝑋))
81	20	simprd 478	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∃𝑛 ∈ ℕ₀ (#‘𝑋) = (𝑃↑𝑛))
82	81	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ∃𝑛 ∈ ℕ₀ (#‘𝑋) = (𝑃↑𝑛))
83		breq2 4587	. . . . . . . . . . . . . . . . . . 19 ⊢ ((#‘𝑋) = (𝑃↑𝑛) → ((#‘[𝑤] ∼ ) ∥ (#‘𝑋) ↔ (#‘[𝑤] ∼ ) ∥ (𝑃↑𝑛)))
84	83	biimpcd 238	. . . . . . . . . . . . . . . . . 18 ⊢ ((#‘[𝑤] ∼ ) ∥ (#‘𝑋) → ((#‘𝑋) = (𝑃↑𝑛) → (#‘[𝑤] ∼ ) ∥ (𝑃↑𝑛)))
85	84	reximdv 2999	. . . . . . . . . . . . . . . . 17 ⊢ ((#‘[𝑤] ∼ ) ∥ (#‘𝑋) → (∃𝑛 ∈ ℕ₀ (#‘𝑋) = (𝑃↑𝑛) → ∃𝑛 ∈ ℕ₀ (#‘[𝑤] ∼ ) ∥ (𝑃↑𝑛)))
86	80, 82, 85	sylc 63	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ∃𝑛 ∈ ℕ₀ (#‘[𝑤] ∼ ) ∥ (𝑃↑𝑛))
87		pcprmpw2 15424	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ ℙ ∧ (#‘[𝑤] ∼ ) ∈ ℕ) → (∃𝑛 ∈ ℕ₀ (#‘[𝑤] ∼ ) ∥ (𝑃↑𝑛) ↔ (#‘[𝑤] ∼ ) = (𝑃↑(𝑃 pCnt (#‘[𝑤] ∼ )))))
88	43, 58, 87	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (∃𝑛 ∈ ℕ₀ (#‘[𝑤] ∼ ) ∥ (𝑃↑𝑛) ↔ (#‘[𝑤] ∼ ) = (𝑃↑(𝑃 pCnt (#‘[𝑤] ∼ )))))
89	86, 88	mpbid 221	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (#‘[𝑤] ∼ ) = (𝑃↑(𝑃 pCnt (#‘[𝑤] ∼ ))))
90	89	eqcomd 2616	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (𝑃↑(𝑃 pCnt (#‘[𝑤] ∼ ))) = (#‘[𝑤] ∼ ))
91	23	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑃 ∈ ℤ)
92	91	zcnd 11359	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑃 ∈ ℂ)
93	92	exp0d 12864	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (𝑃↑0) = 1)
94		hash1 13053	. . . . . . . . . . . . . . 15 ⊢ (#‘1_𝑜) = 1
95	93, 94	syl6eqr 2662	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (𝑃↑0) = (#‘1_𝑜))
96	90, 95	eqeq12d 2625	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ((𝑃↑(𝑃 pCnt (#‘[𝑤] ∼ ))) = (𝑃↑0) ↔ (#‘[𝑤] ∼ ) = (#‘1_𝑜)))
97		df1o2 7459	. . . . . . . . . . . . . . 15 ⊢ 1_𝑜 = {∅}
98		snfi 7923	. . . . . . . . . . . . . . 15 ⊢ {∅} ∈ Fin
99	97, 98	eqeltri 2684	. . . . . . . . . . . . . 14 ⊢ 1_𝑜 ∈ Fin
100		hashen 12997	. . . . . . . . . . . . . 14 ⊢ (([𝑤] ∼ ∈ Fin ∧ 1_𝑜 ∈ Fin) → ((#‘[𝑤] ∼ ) = (#‘1_𝑜) ↔ [𝑤] ∼ ≈ 1_𝑜))
101	55, 99, 100	sylancl 693	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ((#‘[𝑤] ∼ ) = (#‘1_𝑜) ↔ [𝑤] ∼ ≈ 1_𝑜))
102	96, 101	bitrd 267	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ((𝑃↑(𝑃 pCnt (#‘[𝑤] ∼ ))) = (𝑃↑0) ↔ [𝑤] ∼ ≈ 1_𝑜))
103		en1b 7910	. . . . . . . . . . . 12 ⊢ ([𝑤] ∼ ≈ 1_𝑜 ↔ [𝑤] ∼ = {∪ [𝑤] ∼ })
104	102, 103	syl6bb 275	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ((𝑃↑(𝑃 pCnt (#‘[𝑤] ∼ ))) = (𝑃↑0) ↔ [𝑤] ∼ = {∪ [𝑤] ∼ }))
105	45	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤] ∼ })) → 𝑤 ∈ 𝑌)
106	4	ad2antrr 758	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤] ∼ })) → ⊕ ∈ (𝐺 GrpAct 𝑌))
107	6	gaf 17551	. . . . . . . . . . . . . . . . . . . 20 ⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → ⊕ :(𝑋 × 𝑌)⟶𝑌)
108	106, 107	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤] ∼ })) → ⊕ :(𝑋 × 𝑌)⟶𝑌)
109		simprl 790	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤] ∼ })) → ℎ ∈ 𝑋)
110	108, 109, 105	fovrnd 6704	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤] ∼ })) → (ℎ ⊕ 𝑤) ∈ 𝑌)
111		eqid 2610	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ ⊕ 𝑤) = (ℎ ⊕ 𝑤)
112		oveq1 6556	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = ℎ → (𝑘 ⊕ 𝑤) = (ℎ ⊕ 𝑤))
113	112	eqeq1d 2612	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = ℎ → ((𝑘 ⊕ 𝑤) = (ℎ ⊕ 𝑤) ↔ (ℎ ⊕ 𝑤) = (ℎ ⊕ 𝑤)))
114	113	rspcev 3282	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ ∈ 𝑋 ∧ (ℎ ⊕ 𝑤) = (ℎ ⊕ 𝑤)) → ∃𝑘 ∈ 𝑋 (𝑘 ⊕ 𝑤) = (ℎ ⊕ 𝑤))
115	109, 111, 114	sylancl 693	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤] ∼ })) → ∃𝑘 ∈ 𝑋 (𝑘 ⊕ 𝑤) = (ℎ ⊕ 𝑤))
116	5	gaorb 17563	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∼ (ℎ ⊕ 𝑤) ↔ (𝑤 ∈ 𝑌 ∧ (ℎ ⊕ 𝑤) ∈ 𝑌 ∧ ∃𝑘 ∈ 𝑋 (𝑘 ⊕ 𝑤) = (ℎ ⊕ 𝑤)))
117	105, 110, 115, 116	syl3anbrc 1239	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤] ∼ })) → 𝑤 ∼ (ℎ ⊕ 𝑤))
118		ovex 6577	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ ⊕ 𝑤) ∈ V
119	118, 47	elec 7673	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ ⊕ 𝑤) ∈ [𝑤] ∼ ↔ 𝑤 ∼ (ℎ ⊕ 𝑤))
120	117, 119	sylibr 223	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤] ∼ })) → (ℎ ⊕ 𝑤) ∈ [𝑤] ∼ )
121		simprr 792	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤] ∼ })) → [𝑤] ∼ = {∪ [𝑤] ∼ })
122	120, 121	eleqtrd 2690	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤] ∼ })) → (ℎ ⊕ 𝑤) ∈ {∪ [𝑤] ∼ })
123	118	elsn 4140	. . . . . . . . . . . . . . 15 ⊢ ((ℎ ⊕ 𝑤) ∈ {∪ [𝑤] ∼ } ↔ (ℎ ⊕ 𝑤) = ∪ [𝑤] ∼ )
124	122, 123	sylib 207	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤] ∼ })) → (ℎ ⊕ 𝑤) = ∪ [𝑤] ∼ )
125	49	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤] ∼ })) → 𝑤 ∈ [𝑤] ∼ )
126	125, 121	eleqtrd 2690	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤] ∼ })) → 𝑤 ∈ {∪ [𝑤] ∼ })
127	47	elsn 4140	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ {∪ [𝑤] ∼ } ↔ 𝑤 = ∪ [𝑤] ∼ )
128	126, 127	sylib 207	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤] ∼ })) → 𝑤 = ∪ [𝑤] ∼ )
129	124, 128	eqtr4d 2647	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤] ∼ })) → (ℎ ⊕ 𝑤) = 𝑤)
130	129	expr 641	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ ℎ ∈ 𝑋) → ([𝑤] ∼ = {∪ [𝑤] ∼ } → (ℎ ⊕ 𝑤) = 𝑤))
131	130	ralrimdva 2952	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ([𝑤] ∼ = {∪ [𝑤] ∼ } → ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑤) = 𝑤))
132	104, 131	sylbid 229	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ((𝑃↑(𝑃 pCnt (#‘[𝑤] ∼ ))) = (𝑃↑0) → ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑤) = 𝑤))
133	61, 132	syl5 33	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ((𝑃 pCnt (#‘[𝑤] ∼ )) = 0 → ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑤) = 𝑤))
134	60, 133	sylbird 249	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (¬ 𝑃 ∥ (#‘[𝑤] ∼ ) → ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑤) = 𝑤))
135		oveq2 6557	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → (ℎ ⊕ 𝑢) = (ℎ ⊕ 𝑤))
136		id 22	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → 𝑢 = 𝑤)
137	135, 136	eqeq12d 2625	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑤 → ((ℎ ⊕ 𝑢) = 𝑢 ↔ (ℎ ⊕ 𝑤) = 𝑤))
138	137	ralbidv 2969	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑤 → (∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑢) = 𝑢 ↔ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑤) = 𝑤))
139		sylow2a.z	. . . . . . . . . . 11 ⊢ 𝑍 = {𝑢 ∈ 𝑌 ∣ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑢) = 𝑢}
140	138, 139	elrab2 3333	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑍 ↔ (𝑤 ∈ 𝑌 ∧ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑤) = 𝑤))
141	140	baib 942	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑌 → (𝑤 ∈ 𝑍 ↔ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑤) = 𝑤))
142	141	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (𝑤 ∈ 𝑍 ↔ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑤) = 𝑤))
143	134, 142	sylibrd 248	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (¬ 𝑃 ∥ (#‘[𝑤] ∼ ) → 𝑤 ∈ 𝑍))
144	6, 4, 14, 17, 1, 139, 5	sylow2alem1 17855	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → [𝑤] ∼ = {𝑤})
145		simpr 476	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ 𝑍)
146	145	snssd 4281	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {𝑤} ⊆ 𝑍)
147	144, 146	eqsstrd 3602	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → [𝑤] ∼ ⊆ 𝑍)
148	147	ex 449	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ 𝑍 → [𝑤] ∼ ⊆ 𝑍))
149	148	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (𝑤 ∈ 𝑍 → [𝑤] ∼ ⊆ 𝑍))
150	143, 149	syld 46	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (¬ 𝑃 ∥ (#‘[𝑤] ∼ ) → [𝑤] ∼ ⊆ 𝑍))
151	150	con1d 138	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (¬ [𝑤] ∼ ⊆ 𝑍 → 𝑃 ∥ (#‘[𝑤] ∼ )))
152	35, 42, 151	ectocld 7701	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → (¬ 𝑧 ∈ 𝒫 𝑍 → 𝑃 ∥ (#‘𝑧)))
153	152	impr 647	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝑌 / ∼ ) ∧ ¬ 𝑧 ∈ 𝒫 𝑍)) → 𝑃 ∥ (#‘𝑧))
154	34, 153	sylan2b 491	. 2 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)) → 𝑃 ∥ (#‘𝑧))
155	13, 23, 33, 154	fsumdvds 14868	1 ⊢ (𝜑 → 𝑃 ∥ Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(#‘𝑧))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ∀wral 2896 ∃wrex 2897 {crab 2900 ∖ cdif 3537 ⊆ wss 3540 ∅c0 3874 𝒫 cpw 4108 {csn 4125 {cpr 4127 ∪ cuni 4372 class class class wbr 4583 {copab 4642 × cxp 5036 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 1_𝑜c1o 7440 Er wer 7626 [cec 7627 / cqs 7628 ≈ cen 7838 Fincfn 7841 0cc0 9815 1c1 9816 · cmul 9820 ℕcn 10897 ℕ₀cn0 11169 ℤcz 11254 ↑cexp 12722 #chash 12979 Σcsu 14264 ∥ cdvds 14821 ℙcprime 15223 pCnt cpc 15379 Basecbs 15695 Grpcgrp 17245 ~_QG cqg 17413 GrpAct cga 17545 pGrp cpgp 17769

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-inf2 8421 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-fal 1481 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-disj 4554 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-se 4998 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-isom 5813 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-2o 7448 df-oadd 7451 df-omul 7452 df-er 7629 df-ec 7631 df-qs 7635 df-map 7746 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-sup 8231 df-inf 8232 df-oi 8298 df-card 8648 df-acn 8651 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-n0 11170 df-xnn0 11241 df-z 11255 df-uz 11564 df-q 11665 df-rp 11709 df-fz 12198 df-fzo 12335 df-fl 12455 df-mod 12531 df-seq 12664 df-exp 12723 df-fac 12923 df-bc 12952 df-hash 12980 df-cj 13687 df-re 13688 df-im 13689 df-sqrt 13823 df-abs 13824 df-clim 14067 df-sum 14265 df-dvds 14822 df-gcd 15055 df-prm 15224 df-pc 15380 df-ndx 15698 df-slot 15699 df-base 15700 df-sets 15701 df-ress 15702 df-plusg 15781 df-0g 15925 df-mgm 17065 df-sgrp 17107 df-mnd 17118 df-submnd 17159 df-grp 17248 df-minusg 17249 df-sbg 17250 df-mulg 17364 df-subg 17414 df-eqg 17416 df-ga 17546 df-od 17771 df-pgp 17773

This theorem is referenced by: sylow2a 17857

W3C validator