sylow2a - Metamath Proof Explorer

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

Theorem sylow2a 18811

Description: A named lemma of Sylow's second and third theorems. If 𝐺 is a finite 𝑃-group that acts on the finite set 𝑌, then the set 𝑍 of all points of 𝑌 fixed by every element of 𝐺 has cardinality equivalent to the cardinality of 𝑌, mod 𝑃. (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
sylow2a	⊢ (𝜑 → 𝑃 ∥ ((♯‘𝑌) − (♯‘𝑍)))

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

Proof of Theorem sylow2a Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sylow2a.x	. . 3 ⊢ 𝑋 = (Base‘𝐺)
2		sylow2a.m	. . 3 ⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑌))
3		sylow2a.p	. . 3 ⊢ (𝜑 → 𝑃 pGrp 𝐺)
4		sylow2a.f	. . 3 ⊢ (𝜑 → 𝑋 ∈ Fin)
5		sylow2a.y	. . 3 ⊢ (𝜑 → 𝑌 ∈ Fin)
6		sylow2a.z	. . 3 ⊢ 𝑍 = {𝑢 ∈ 𝑌 ∣ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑢) = 𝑢}
7		sylow2a.r	. . 3 ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}
8	1, 2, 3, 4, 5, 6, 7	sylow2alem2 18810	. 2 ⊢ (𝜑 → 𝑃 ∥ Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧))
9		inass 4124	. . . . . . 7 ⊢ (((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∩ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)) = ((𝑌 / ∼ ) ∩ (𝒫 𝑍 ∩ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)))
10		disjdif 4368	. . . . . . . 8 ⊢ (𝒫 𝑍 ∩ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)) = ∅
11	10	ineq2i 4114	. . . . . . 7 ⊢ ((𝑌 / ∼ ) ∩ (𝒫 𝑍 ∩ ((𝑌 / ∼ ) ∖ 𝒫 𝑍))) = ((𝑌 / ∼ ) ∩ ∅)
12		in0 4287	. . . . . . 7 ⊢ ((𝑌 / ∼ ) ∩ ∅) = ∅
13	9, 11, 12	3eqtri 2785	. . . . . 6 ⊢ (((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∩ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)) = ∅
14	13	a1i 11	. . . . 5 ⊢ (𝜑 → (((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∩ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)) = ∅)
15		inundif 4375	. . . . . . 7 ⊢ (((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∪ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)) = (𝑌 / ∼ )
16	15	eqcomi 2767	. . . . . 6 ⊢ (𝑌 / ∼ ) = (((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∪ ((𝑌 / ∼ ) ∖ 𝒫 𝑍))
17	16	a1i 11	. . . . 5 ⊢ (𝜑 → (𝑌 / ∼ ) = (((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∪ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)))
18		pwfi 8746	. . . . . . 7 ⊢ (𝑌 ∈ Fin ↔ 𝒫 𝑌 ∈ Fin)
19	5, 18	sylib 221	. . . . . 6 ⊢ (𝜑 → 𝒫 𝑌 ∈ Fin)
20	7, 1	gaorber 18505	. . . . . . . 8 ⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → ∼ Er 𝑌)
21	2, 20	syl 17	. . . . . . 7 ⊢ (𝜑 → ∼ Er 𝑌)
22	21	qsss 8368	. . . . . 6 ⊢ (𝜑 → (𝑌 / ∼ ) ⊆ 𝒫 𝑌)
23	19, 22	ssfid 8778	. . . . 5 ⊢ (𝜑 → (𝑌 / ∼ ) ∈ Fin)
24	5	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑌 ∈ Fin)
25	22	sselda 3892	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑧 ∈ 𝒫 𝑌)
26	25	elpwid 4505	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑧 ⊆ 𝑌)
27	24, 26	ssfid 8778	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑧 ∈ Fin)
28		hashcl 13767	. . . . . . 7 ⊢ (𝑧 ∈ Fin → (♯‘𝑧) ∈ ℕ₀)
29	27, 28	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → (♯‘𝑧) ∈ ℕ₀)
30	29	nn0cnd 11996	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → (♯‘𝑧) ∈ ℂ)
31	14, 17, 23, 30	fsumsplit 15145	. . . 4 ⊢ (𝜑 → Σ𝑧 ∈ (𝑌 / ∼ )(♯‘𝑧) = (Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)(♯‘𝑧) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧)))
32	21, 5	qshash 15230	. . . 4 ⊢ (𝜑 → (♯‘𝑌) = Σ𝑧 ∈ (𝑌 / ∼ )(♯‘𝑧))
33		inss1 4133	. . . . . . . 8 ⊢ ((𝑌 / ∼ ) ∩ 𝒫 𝑍) ⊆ (𝑌 / ∼ )
34		ssfi 8742	. . . . . . . 8 ⊢ (((𝑌 / ∼ ) ∈ Fin ∧ ((𝑌 / ∼ ) ∩ 𝒫 𝑍) ⊆ (𝑌 / ∼ )) → ((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∈ Fin)
35	23, 33, 34	sylancl 589	. . . . . . 7 ⊢ (𝜑 → ((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∈ Fin)
36		ax-1cn 10633	. . . . . . 7 ⊢ 1 ∈ ℂ
37		fsumconst 15193	. . . . . . 7 ⊢ ((((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∈ Fin ∧ 1 ∈ ℂ) → Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)1 = ((♯‘((𝑌 / ∼ ) ∩ 𝒫 𝑍)) · 1))
38	35, 36, 37	sylancl 589	. . . . . 6 ⊢ (𝜑 → Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)1 = ((♯‘((𝑌 / ∼ ) ∩ 𝒫 𝑍)) · 1))
39		elin 3874	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍) ↔ (𝑧 ∈ (𝑌 / ∼ ) ∧ 𝑧 ∈ 𝒫 𝑍))
40		eqid 2758	. . . . . . . . . . . . 13 ⊢ (𝑌 / ∼ ) = (𝑌 / ∼ )
41		sseq1 3917	. . . . . . . . . . . . . . 15 ⊢ ([𝑤] ∼ = 𝑧 → ([𝑤] ∼ ⊆ 𝑍 ↔ 𝑧 ⊆ 𝑍))
42		velpw 4499	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝒫 𝑍 ↔ 𝑧 ⊆ 𝑍)
43	41, 42	bitr4di 292	. . . . . . . . . . . . . 14 ⊢ ([𝑤] ∼ = 𝑧 → ([𝑤] ∼ ⊆ 𝑍 ↔ 𝑧 ∈ 𝒫 𝑍))
44		breq1 5035	. . . . . . . . . . . . . 14 ⊢ ([𝑤] ∼ = 𝑧 → ([𝑤] ∼ ≈ 1_o ↔ 𝑧 ≈ 1_o))
45	43, 44	imbi12d 348	. . . . . . . . . . . . 13 ⊢ ([𝑤] ∼ = 𝑧 → (([𝑤] ∼ ⊆ 𝑍 → [𝑤] ∼ ≈ 1_o) ↔ (𝑧 ∈ 𝒫 𝑍 → 𝑧 ≈ 1_o)))
46	21	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ∼ Er 𝑌)
47		simpr 488	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑤 ∈ 𝑌)
48	46, 47	erref 8319	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑤 ∼ 𝑤)
49		vex 3413	. . . . . . . . . . . . . . . . 17 ⊢ 𝑤 ∈ V
50	49, 49	elec 8343	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ [𝑤] ∼ ↔ 𝑤 ∼ 𝑤)
51	48, 50	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑤 ∈ [𝑤] ∼ )
52		ssel 3885	. . . . . . . . . . . . . . 15 ⊢ ([𝑤] ∼ ⊆ 𝑍 → (𝑤 ∈ [𝑤] ∼ → 𝑤 ∈ 𝑍))
53	51, 52	syl5com 31	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ([𝑤] ∼ ⊆ 𝑍 → 𝑤 ∈ 𝑍))
54	1, 2, 3, 4, 5, 6, 7	sylow2alem1 18809	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → [𝑤] ∼ = {𝑤})
55	49	ensn1 8592	. . . . . . . . . . . . . . . . 17 ⊢ {𝑤} ≈ 1_o
56	54, 55	eqbrtrdi 5071	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → [𝑤] ∼ ≈ 1_o)
57	56	ex 416	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑤 ∈ 𝑍 → [𝑤] ∼ ≈ 1_o))
58	57	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (𝑤 ∈ 𝑍 → [𝑤] ∼ ≈ 1_o))
59	53, 58	syld 47	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ([𝑤] ∼ ⊆ 𝑍 → [𝑤] ∼ ≈ 1_o))
60	40, 45, 59	ectocld 8374	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → (𝑧 ∈ 𝒫 𝑍 → 𝑧 ≈ 1_o))
61	60	impr 458	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝑌 / ∼ ) ∧ 𝑧 ∈ 𝒫 𝑍)) → 𝑧 ≈ 1_o)
62	39, 61	sylan2b 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → 𝑧 ≈ 1_o)
63		en1b 8596	. . . . . . . . . 10 ⊢ (𝑧 ≈ 1_o ↔ 𝑧 = {∪ 𝑧})
64	62, 63	sylib 221	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → 𝑧 = {∪ 𝑧})
65	64	fveq2d 6662	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → (♯‘𝑧) = (♯‘{∪ 𝑧}))
66		vuniex 7463	. . . . . . . . 9 ⊢ ∪ 𝑧 ∈ V
67		hashsng 13780	. . . . . . . . 9 ⊢ (∪ 𝑧 ∈ V → (♯‘{∪ 𝑧}) = 1)
68	66, 67	ax-mp 5	. . . . . . . 8 ⊢ (♯‘{∪ 𝑧}) = 1
69	65, 68	eqtrdi 2809	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → (♯‘𝑧) = 1)
70	69	sumeq2dv 15108	. . . . . 6 ⊢ (𝜑 → Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)(♯‘𝑧) = Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)1)
71	6	ssrab3 3986	. . . . . . . . . . 11 ⊢ 𝑍 ⊆ 𝑌
72		ssfi 8742	. . . . . . . . . . 11 ⊢ ((𝑌 ∈ Fin ∧ 𝑍 ⊆ 𝑌) → 𝑍 ∈ Fin)
73	5, 71, 72	sylancl 589	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ Fin)
74		hashcl 13767	. . . . . . . . . 10 ⊢ (𝑍 ∈ Fin → (♯‘𝑍) ∈ ℕ₀)
75	73, 74	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝑍) ∈ ℕ₀)
76	75	nn0cnd 11996	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝑍) ∈ ℂ)
77	76	mulid1d 10696	. . . . . . 7 ⊢ (𝜑 → ((♯‘𝑍) · 1) = (♯‘𝑍))
78	6, 5	rabexd 5203	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ V)
79		eqid 2758	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑍 ↦ {𝑤}) = (𝑤 ∈ 𝑍 ↦ {𝑤})
80	7	relopabi 5663	. . . . . . . . . . . . . . 15 ⊢ Rel ∼
81		relssdmrn 6098	. . . . . . . . . . . . . . 15 ⊢ (Rel ∼ → ∼ ⊆ (dom ∼ × ran ∼ ))
82	80, 81	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ∼ ⊆ (dom ∼ × ran ∼ )
83		erdm 8309	. . . . . . . . . . . . . . . . 17 ⊢ ( ∼ Er 𝑌 → dom ∼ = 𝑌)
84	21, 83	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom ∼ = 𝑌)
85	84, 5	eqeltrd 2852	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom ∼ ∈ Fin)
86		errn 8321	. . . . . . . . . . . . . . . . 17 ⊢ ( ∼ Er 𝑌 → ran ∼ = 𝑌)
87	21, 86	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran ∼ = 𝑌)
88	87, 5	eqeltrd 2852	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran ∼ ∈ Fin)
89	85, 88	xpexd 7472	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (dom ∼ × ran ∼ ) ∈ V)
90		ssexg 5193	. . . . . . . . . . . . . 14 ⊢ (( ∼ ⊆ (dom ∼ × ran ∼ ) ∧ (dom ∼ × ran ∼ ) ∈ V) → ∼ ∈ V)
91	82, 89, 90	sylancr 590	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∼ ∈ V)
92		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ 𝑍)
93	71, 92	sseldi 3890	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ 𝑌)
94		ecelqsg 8362	. . . . . . . . . . . . 13 ⊢ (( ∼ ∈ V ∧ 𝑤 ∈ 𝑌) → [𝑤] ∼ ∈ (𝑌 / ∼ ))
95	91, 93, 94	syl2an2r 684	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → [𝑤] ∼ ∈ (𝑌 / ∼ ))
96	54, 95	eqeltrrd 2853	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {𝑤} ∈ (𝑌 / ∼ ))
97		snelpwi 5305	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ 𝑍 → {𝑤} ∈ 𝒫 𝑍)
98	97	adantl 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {𝑤} ∈ 𝒫 𝑍)
99	96, 98	elind 4099	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {𝑤} ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍))
100		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍))
101	100	elin2d 4104	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → 𝑧 ∈ 𝒫 𝑍)
102	101	elpwid 4505	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → 𝑧 ⊆ 𝑍)
103	64, 102	eqsstrrd 3931	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → {∪ 𝑧} ⊆ 𝑍)
104	66	snss 4676	. . . . . . . . . . 11 ⊢ (∪ 𝑧 ∈ 𝑍 ↔ {∪ 𝑧} ⊆ 𝑍)
105	103, 104	sylibr 237	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → ∪ 𝑧 ∈ 𝑍)
106		sneq 4532	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ∪ 𝑧 → {𝑤} = {∪ 𝑧})
107	106	eqeq2d 2769	. . . . . . . . . . . . 13 ⊢ (𝑤 = ∪ 𝑧 → (𝑧 = {𝑤} ↔ 𝑧 = {∪ 𝑧}))
108	64, 107	syl5ibrcom 250	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → (𝑤 = ∪ 𝑧 → 𝑧 = {𝑤}))
109	108	adantrl 715	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑍 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍))) → (𝑤 = ∪ 𝑧 → 𝑧 = {𝑤}))
110		unieq 4809	. . . . . . . . . . . 12 ⊢ (𝑧 = {𝑤} → ∪ 𝑧 = ∪ {𝑤})
111	49	unisn 4820	. . . . . . . . . . . 12 ⊢ ∪ {𝑤} = 𝑤
112	110, 111	eqtr2di 2810	. . . . . . . . . . 11 ⊢ (𝑧 = {𝑤} → 𝑤 = ∪ 𝑧)
113	109, 112	impbid1 228	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑍 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍))) → (𝑤 = ∪ 𝑧 ↔ 𝑧 = {𝑤}))
114	79, 99, 105, 113	f1o2d 7395	. . . . . . . . 9 ⊢ (𝜑 → (𝑤 ∈ 𝑍 ↦ {𝑤}):𝑍–1-1-onto→((𝑌 / ∼ ) ∩ 𝒫 𝑍))
115	78, 114	hasheqf1od 13764	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝑍) = (♯‘((𝑌 / ∼ ) ∩ 𝒫 𝑍)))
116	115	oveq1d 7165	. . . . . . 7 ⊢ (𝜑 → ((♯‘𝑍) · 1) = ((♯‘((𝑌 / ∼ ) ∩ 𝒫 𝑍)) · 1))
117	77, 116	eqtr3d 2795	. . . . . 6 ⊢ (𝜑 → (♯‘𝑍) = ((♯‘((𝑌 / ∼ ) ∩ 𝒫 𝑍)) · 1))
118	38, 70, 117	3eqtr4rd 2804	. . . . 5 ⊢ (𝜑 → (♯‘𝑍) = Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)(♯‘𝑧))
119	118	oveq1d 7165	. . . 4 ⊢ (𝜑 → ((♯‘𝑍) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧)) = (Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)(♯‘𝑧) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧)))
120	31, 32, 119	3eqtr4rd 2804	. . 3 ⊢ (𝜑 → ((♯‘𝑍) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧)) = (♯‘𝑌))
121		hashcl 13767	. . . . . 6 ⊢ (𝑌 ∈ Fin → (♯‘𝑌) ∈ ℕ₀)
122	5, 121	syl 17	. . . . 5 ⊢ (𝜑 → (♯‘𝑌) ∈ ℕ₀)
123	122	nn0cnd 11996	. . . 4 ⊢ (𝜑 → (♯‘𝑌) ∈ ℂ)
124		diffi 8786	. . . . . 6 ⊢ ((𝑌 / ∼ ) ∈ Fin → ((𝑌 / ∼ ) ∖ 𝒫 𝑍) ∈ Fin)
125	23, 124	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑌 / ∼ ) ∖ 𝒫 𝑍) ∈ Fin)
126		eldifi 4032	. . . . . 6 ⊢ (𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍) → 𝑧 ∈ (𝑌 / ∼ ))
127	126, 30	sylan2 595	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)) → (♯‘𝑧) ∈ ℂ)
128	125, 127	fsumcl 15138	. . . 4 ⊢ (𝜑 → Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧) ∈ ℂ)
129	123, 76, 128	subaddd 11053	. . 3 ⊢ (𝜑 → (((♯‘𝑌) − (♯‘𝑍)) = Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧) ↔ ((♯‘𝑍) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧)) = (♯‘𝑌)))
130	120, 129	mpbird 260	. 2 ⊢ (𝜑 → ((♯‘𝑌) − (♯‘𝑍)) = Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧))
131	8, 130	breqtrrd 5060	1 ⊢ (𝜑 → 𝑃 ∥ ((♯‘𝑌) − (♯‘𝑍)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 = wceq 1538 ∈ wcel 2111 ∀wral 3070 ∃wrex 3071 {crab 3074 Vcvv 3409 ∖ cdif 3855 ∪ cun 3856 ∩ cin 3857 ⊆ wss 3858 ∅c0 4225 𝒫 cpw 4494 {csn 4522 {cpr 4524 ∪ cuni 4798 class class class wbr 5032 {copab 5094 ↦ cmpt 5112 × cxp 5522 dom cdm 5524 ran crn 5525 Rel wrel 5529 ‘cfv 6335 (class class class)co 7150 1_oc1o 8105 Er wer 8296 [cec 8297 / cqs 8298 ≈ cen 8524 Fincfn 8527 ℂcc 10573 1c1 10576 + caddc 10578 · cmul 10580 − cmin 10908 ℕ₀cn0 11934 ♯chash 13740 Σcsu 15090 ∥ cdvds 15655 Basecbs 16541 GrpAct cga 18486 pGrp cpgp 18721

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-rep 5156 ax-sep 5169 ax-nul 5176 ax-pow 5234 ax-pr 5298 ax-un 7459 ax-inf2 9137 ax-cnex 10631 ax-resscn 10632 ax-1cn 10633 ax-icn 10634 ax-addcl 10635 ax-addrcl 10636 ax-mulcl 10637 ax-mulrcl 10638 ax-mulcom 10639 ax-addass 10640 ax-mulass 10641 ax-distr 10642 ax-i2m1 10643 ax-1ne0 10644 ax-1rid 10645 ax-rnegex 10646 ax-rrecex 10647 ax-cnre 10648 ax-pre-lttri 10649 ax-pre-lttrn 10650 ax-pre-ltadd 10651 ax-pre-mulgt0 10652 ax-pre-sup 10653

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-nel 3056 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3697 df-csb 3806 df-dif 3861 df-un 3863 df-in 3865 df-ss 3875 df-pss 3877 df-nul 4226 df-if 4421 df-pw 4496 df-sn 4523 df-pr 4525 df-tp 4527 df-op 4529 df-uni 4799 df-int 4839 df-iun 4885 df-disj 4998 df-br 5033 df-opab 5095 df-mpt 5113 df-tr 5139 df-id 5430 df-eprel 5435 df-po 5443 df-so 5444 df-fr 5483 df-se 5484 df-we 5485 df-xp 5530 df-rel 5531 df-cnv 5532 df-co 5533 df-dm 5534 df-rn 5535 df-res 5536 df-ima 5537 df-pred 6126 df-ord 6172 df-on 6173 df-lim 6174 df-suc 6175 df-iota 6294 df-fun 6337 df-fn 6338 df-f 6339 df-f1 6340 df-fo 6341 df-f1o 6342 df-fv 6343 df-isom 6344 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7580 df-1st 7693 df-2nd 7694 df-wrecs 7957 df-recs 8018 df-rdg 8056 df-1o 8112 df-2o 8113 df-oadd 8116 df-omul 8117 df-er 8299 df-ec 8301 df-qs 8305 df-map 8418 df-en 8528 df-dom 8529 df-sdom 8530 df-fin 8531 df-sup 8939 df-inf 8940 df-oi 9007 df-dju 9363 df-card 9401 df-acn 9404 df-pnf 10715 df-mnf 10716 df-xr 10717 df-ltxr 10718 df-le 10719 df-sub 10910 df-neg 10911 df-div 11336 df-nn 11675 df-2 11737 df-3 11738 df-n0 11935 df-xnn0 12007 df-z 12021 df-uz 12283 df-q 12389 df-rp 12431 df-fz 12940 df-fzo 13083 df-fl 13211 df-mod 13287 df-seq 13419 df-exp 13480 df-fac 13684 df-bc 13713 df-hash 13741 df-cj 14506 df-re 14507 df-im 14508 df-sqrt 14642 df-abs 14643 df-clim 14893 df-sum 15091 df-dvds 15656 df-gcd 15894 df-prm 16068 df-pc 16229 df-ndx 16544 df-slot 16545 df-base 16547 df-sets 16548 df-ress 16549 df-plusg 16636 df-0g 16773 df-mgm 17918 df-sgrp 17967 df-mnd 17978 df-submnd 18023 df-grp 18172 df-minusg 18173 df-sbg 18174 df-mulg 18292 df-subg 18343 df-eqg 18345 df-ga 18487 df-od 18723 df-pgp 18725

This theorem is referenced by: sylow2blem3 18814 sylow3lem6 18824

W3C validator