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 19677

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 19676	. 2 ⊢ (𝜑 → 𝑃 ∥ Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧))
9		inass 4182	. . . . . . 7 ⊢ (((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∩ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)) = ((𝑌 / ∼ ) ∩ (𝒫 𝑍 ∩ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)))
10		disjdif 4429	. . . . . . . 8 ⊢ (𝒫 𝑍 ∩ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)) = ∅
11	10	ineq2i 4172	. . . . . . 7 ⊢ ((𝑌 / ∼ ) ∩ (𝒫 𝑍 ∩ ((𝑌 / ∼ ) ∖ 𝒫 𝑍))) = ((𝑌 / ∼ ) ∩ ∅)
12		in0 4352	. . . . . . 7 ⊢ ((𝑌 / ∼ ) ∩ ∅) = ∅
13	9, 11, 12	3eqtri 2792	. . . . . 6 ⊢ (((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∩ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)) = ∅
14	13	a1i 11	. . . . 5 ⊢ (𝜑 → (((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∩ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)) = ∅)
15		inundif 4436	. . . . . . 7 ⊢ (((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∪ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)) = (𝑌 / ∼ )
16	15	eqcomi 2774	. . . . . 6 ⊢ (𝑌 / ∼ ) = (((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∪ ((𝑌 / ∼ ) ∖ 𝒫 𝑍))
17	16	a1i 11	. . . . 5 ⊢ (𝜑 → (𝑌 / ∼ ) = (((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∪ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)))
18		pwfi 9266	. . . . . . 7 ⊢ (𝑌 ∈ Fin ↔ 𝒫 𝑌 ∈ Fin)
19	5, 18	sylib 221	. . . . . 6 ⊢ (𝜑 → 𝒫 𝑌 ∈ Fin)
20	7, 1	gaorber 19366	. . . . . . . 8 ⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → ∼ Er 𝑌)
21	2, 20	syl 18	. . . . . . 7 ⊢ (𝜑 → ∼ Er 𝑌)
22	21	qsss 8761	. . . . . 6 ⊢ (𝜑 → (𝑌 / ∼ ) ⊆ 𝒫 𝑌)
23	19, 22	ssfid 9217	. . . . 5 ⊢ (𝜑 → (𝑌 / ∼ ) ∈ Fin)
24	5	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑌 ∈ Fin)
25	22	sselda 3939	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑧 ∈ 𝒫 𝑌)
26	25	elpwid 4567	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑧 ⊆ 𝑌)
27	24, 26	ssfid 9217	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑧 ∈ Fin)
28		hashcl 14380	. . . . . . 7 ⊢ (𝑧 ∈ Fin → (♯‘𝑧) ∈ ℕ₀)
29	27, 28	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → (♯‘𝑧) ∈ ℕ₀)
30	29	nn0cnd 12555	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → (♯‘𝑧) ∈ ℂ)
31	14, 17, 23, 30	fsumsplit 15780	. . . 4 ⊢ (𝜑 → Σ𝑧 ∈ (𝑌 / ∼ )(♯‘𝑧) = (Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)(♯‘𝑧) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧)))
32	21, 5	qshash 15867	. . . 4 ⊢ (𝜑 → (♯‘𝑌) = Σ𝑧 ∈ (𝑌 / ∼ )(♯‘𝑧))
33		inss1 4191	. . . . . . . 8 ⊢ ((𝑌 / ∼ ) ∩ 𝒫 𝑍) ⊆ (𝑌 / ∼ )
34		ssfi 9145	. . . . . . . 8 ⊢ (((𝑌 / ∼ ) ∈ Fin ∧ ((𝑌 / ∼ ) ∩ 𝒫 𝑍) ⊆ (𝑌 / ∼ )) → ((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∈ Fin)
35	23, 33, 34	sylancl 597	. . . . . . 7 ⊢ (𝜑 → ((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∈ Fin)
36		ax-1cn 11146	. . . . . . 7 ⊢ 1 ∈ ℂ
37		fsumconst 15829	. . . . . . 7 ⊢ ((((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∈ Fin ∧ 1 ∈ ℂ) → Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)1 = ((♯‘((𝑌 / ∼ ) ∩ 𝒫 𝑍)) · 1))
38	35, 36, 37	sylancl 597	. . . . . 6 ⊢ (𝜑 → Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)1 = ((♯‘((𝑌 / ∼ ) ∩ 𝒫 𝑍)) · 1))
39		elin 3923	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍) ↔ (𝑧 ∈ (𝑌 / ∼ ) ∧ 𝑧 ∈ 𝒫 𝑍))
40		eqid 2765	. . . . . . . . . . . . 13 ⊢ (𝑌 / ∼ ) = (𝑌 / ∼ )
41		sseq1 3964	. . . . . . . . . . . . . . 15 ⊢ ([𝑤] ∼ = 𝑧 → ([𝑤] ∼ ⊆ 𝑍 ↔ 𝑧 ⊆ 𝑍))
42		velpw 4563	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝒫 𝑍 ↔ 𝑧 ⊆ 𝑍)
43	41, 42	bitr4di 292	. . . . . . . . . . . . . 14 ⊢ ([𝑤] ∼ = 𝑧 → ([𝑤] ∼ ⊆ 𝑍 ↔ 𝑧 ∈ 𝒫 𝑍))
44		breq1 5107	. . . . . . . . . . . . . 14 ⊢ ([𝑤] ∼ = 𝑧 → ([𝑤] ∼ ≈ 1_o ↔ 𝑧 ≈ 1_o))
45	43, 44	imbi12d 347	. . . . . . . . . . . . 13 ⊢ ([𝑤] ∼ = 𝑧 → (([𝑤] ∼ ⊆ 𝑍 → [𝑤] ∼ ≈ 1_o) ↔ (𝑧 ∈ 𝒫 𝑍 → 𝑧 ≈ 1_o)))
46	21	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ∼ Er 𝑌)
47		simpr 489	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑤 ∈ 𝑌)
48	46, 47	erref 8703	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑤 ∼ 𝑤)
49		vex 3461	. . . . . . . . . . . . . . . . 17 ⊢ 𝑤 ∈ V
50	49, 49	elec 8729	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ [𝑤] ∼ ↔ 𝑤 ∼ 𝑤)
51	48, 50	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑤 ∈ [𝑤] ∼ )
52		ssel 3933	. . . . . . . . . . . . . . 15 ⊢ ([𝑤] ∼ ⊆ 𝑍 → (𝑤 ∈ [𝑤] ∼ → 𝑤 ∈ 𝑍))
53	51, 52	syl5com 32	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ([𝑤] ∼ ⊆ 𝑍 → 𝑤 ∈ 𝑍))
54	1, 2, 3, 4, 5, 6, 7	sylow2alem1 19675	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → [𝑤] ∼ = {𝑤})
55	49	ensn1 9006	. . . . . . . . . . . . . . . . 17 ⊢ {𝑤} ≈ 1_o
56	54, 55	eqbrtrdi 5143	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → [𝑤] ∼ ≈ 1_o)
57	56	ex 417	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑤 ∈ 𝑍 → [𝑤] ∼ ≈ 1_o))
58	57	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (𝑤 ∈ 𝑍 → [𝑤] ∼ ≈ 1_o))
59	53, 58	syld 48	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ([𝑤] ∼ ⊆ 𝑍 → [𝑤] ∼ ≈ 1_o))
60	40, 45, 59	ectocld 8768	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → (𝑧 ∈ 𝒫 𝑍 → 𝑧 ≈ 1_o))
61	60	impr 459	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝑌 / ∼ ) ∧ 𝑧 ∈ 𝒫 𝑍)) → 𝑧 ≈ 1_o)
62	39, 61	sylan2b 605	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → 𝑧 ≈ 1_o)
63		en1b 9010	. . . . . . . . . 10 ⊢ (𝑧 ≈ 1_o ↔ 𝑧 = {∪ 𝑧})
64	62, 63	sylib 221	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → 𝑧 = {∪ 𝑧})
65	64	fveq2d 6875	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → (♯‘𝑧) = (♯‘{∪ 𝑧}))
66		vuniex 7726	. . . . . . . . 9 ⊢ ∪ 𝑧 ∈ V
67		hashsng 14393	. . . . . . . . 9 ⊢ (∪ 𝑧 ∈ V → (♯‘{∪ 𝑧}) = 1)
68	66, 67	ax-mp 5	. . . . . . . 8 ⊢ (♯‘{∪ 𝑧}) = 1
69	65, 68	eqtrdi 2816	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → (♯‘𝑧) = 1)
70	69	sumeq2dv 15741	. . . . . 6 ⊢ (𝜑 → Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)(♯‘𝑧) = Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)1)
71	6	ssrab3 4038	. . . . . . . . . . 11 ⊢ 𝑍 ⊆ 𝑌
72		ssfi 9145	. . . . . . . . . . 11 ⊢ ((𝑌 ∈ Fin ∧ 𝑍 ⊆ 𝑌) → 𝑍 ∈ Fin)
73	5, 71, 72	sylancl 597	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ Fin)
74		hashcl 14380	. . . . . . . . . 10 ⊢ (𝑍 ∈ Fin → (♯‘𝑍) ∈ ℕ₀)
75	73, 74	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝑍) ∈ ℕ₀)
76	75	nn0cnd 12555	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝑍) ∈ ℂ)
77	76	mulridd 11214	. . . . . . 7 ⊢ (𝜑 → ((♯‘𝑍) · 1) = (♯‘𝑍))
78	6, 5	rabexd 5300	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ V)
79		eqid 2765	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑍 ↦ {𝑤}) = (𝑤 ∈ 𝑍 ↦ {𝑤})
80	7	relopabiv 5797	. . . . . . . . . . . . . . 15 ⊢ Rel ∼
81		relssdmrn 6259	. . . . . . . . . . . . . . 15 ⊢ (Rel ∼ → ∼ ⊆ (dom ∼ × ran ∼ ))
82	80, 81	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ∼ ⊆ (dom ∼ × ran ∼ )
83		erdm 8693	. . . . . . . . . . . . . . . . 17 ⊢ ( ∼ Er 𝑌 → dom ∼ = 𝑌)
84	21, 83	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom ∼ = 𝑌)
85	84, 5	eqeltrd 2865	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom ∼ ∈ Fin)
86		errn 8705	. . . . . . . . . . . . . . . . 17 ⊢ ( ∼ Er 𝑌 → ran ∼ = 𝑌)
87	21, 86	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran ∼ = 𝑌)
88	87, 5	eqeltrd 2865	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran ∼ ∈ Fin)
89	85, 88	xpexd 7738	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (dom ∼ × ran ∼ ) ∈ V)
90		ssexg 5283	. . . . . . . . . . . . . 14 ⊢ (( ∼ ⊆ (dom ∼ × ran ∼ ) ∧ (dom ∼ × ran ∼ ) ∈ V) → ∼ ∈ V)
91	82, 89, 90	sylancr 598	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∼ ∈ V)
92		simpr 489	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ 𝑍)
93	71, 92	sselid 3937	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ 𝑌)
94		ecelqsw 8754	. . . . . . . . . . . . 13 ⊢ (( ∼ ∈ V ∧ 𝑤 ∈ 𝑌) → [𝑤] ∼ ∈ (𝑌 / ∼ ))
95	91, 93, 94	syl2an2r 697	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → [𝑤] ∼ ∈ (𝑌 / ∼ ))
96	54, 95	eqeltrrd 2866	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {𝑤} ∈ (𝑌 / ∼ ))
97		snelpwi 5415	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ 𝑍 → {𝑤} ∈ 𝒫 𝑍)
98	97	adantl 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {𝑤} ∈ 𝒫 𝑍)
99	96, 98	elind 4155	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {𝑤} ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍))
100		simpr 489	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍))
101	100	elin2d 4160	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → 𝑧 ∈ 𝒫 𝑍)
102	101	elpwid 4567	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → 𝑧 ⊆ 𝑍)
103	64, 102	eqsstrrd 3974	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → {∪ 𝑧} ⊆ 𝑍)
104	66	snss 4746	. . . . . . . . . . 11 ⊢ (∪ 𝑧 ∈ 𝑍 ↔ {∪ 𝑧} ⊆ 𝑍)
105	103, 104	sylibr 237	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → ∪ 𝑧 ∈ 𝑍)
106		sneq 4595	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ∪ 𝑧 → {𝑤} = {∪ 𝑧})
107	106	eqeq2d 2776	. . . . . . . . . . . . 13 ⊢ (𝑤 = ∪ 𝑧 → (𝑧 = {𝑤} ↔ 𝑧 = {∪ 𝑧}))
108	64, 107	syl5ibrcom 250	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → (𝑤 = ∪ 𝑧 → 𝑧 = {𝑤}))
109	108	adantrl 728	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑍 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍))) → (𝑤 = ∪ 𝑧 → 𝑧 = {𝑤}))
110		unieq 4878	. . . . . . . . . . . 12 ⊢ (𝑧 = {𝑤} → ∪ 𝑧 = ∪ {𝑤})
111		unisnv 4887	. . . . . . . . . . . 12 ⊢ ∪ {𝑤} = 𝑤
112	110, 111	eqtr2di 2817	. . . . . . . . . . 11 ⊢ (𝑧 = {𝑤} → 𝑤 = ∪ 𝑧)
113	109, 112	impbid1 228	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑍 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍))) → (𝑤 = ∪ 𝑧 ↔ 𝑧 = {𝑤}))
114	79, 99, 105, 113	f1o2d 7654	. . . . . . . . 9 ⊢ (𝜑 → (𝑤 ∈ 𝑍 ↦ {𝑤}):𝑍–1-1-onto→((𝑌 / ∼ ) ∩ 𝒫 𝑍))
115	78, 114	hasheqf1od 14377	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝑍) = (♯‘((𝑌 / ∼ ) ∩ 𝒫 𝑍)))
116	115	oveq1d 7415	. . . . . . 7 ⊢ (𝜑 → ((♯‘𝑍) · 1) = ((♯‘((𝑌 / ∼ ) ∩ 𝒫 𝑍)) · 1))
117	77, 116	eqtr3d 2802	. . . . . 6 ⊢ (𝜑 → (♯‘𝑍) = ((♯‘((𝑌 / ∼ ) ∩ 𝒫 𝑍)) · 1))
118	38, 70, 117	3eqtr4rd 2811	. . . . 5 ⊢ (𝜑 → (♯‘𝑍) = Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)(♯‘𝑧))
119	118	oveq1d 7415	. . . 4 ⊢ (𝜑 → ((♯‘𝑍) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧)) = (Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)(♯‘𝑧) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧)))
120	31, 32, 119	3eqtr4rd 2811	. . 3 ⊢ (𝜑 → ((♯‘𝑍) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧)) = (♯‘𝑌))
121		hashcl 14380	. . . . . 6 ⊢ (𝑌 ∈ Fin → (♯‘𝑌) ∈ ℕ₀)
122	5, 121	syl 18	. . . . 5 ⊢ (𝜑 → (♯‘𝑌) ∈ ℕ₀)
123	122	nn0cnd 12555	. . . 4 ⊢ (𝜑 → (♯‘𝑌) ∈ ℂ)
124		diffi 9147	. . . . . 6 ⊢ ((𝑌 / ∼ ) ∈ Fin → ((𝑌 / ∼ ) ∖ 𝒫 𝑍) ∈ Fin)
125	23, 124	syl 18	. . . . 5 ⊢ (𝜑 → ((𝑌 / ∼ ) ∖ 𝒫 𝑍) ∈ Fin)
126		eldifi 4087	. . . . . 6 ⊢ (𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍) → 𝑧 ∈ (𝑌 / ∼ ))
127	126, 30	sylan2 604	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)) → (♯‘𝑧) ∈ ℂ)
128	125, 127	fsumcl 15772	. . . 4 ⊢ (𝜑 → Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧) ∈ ℂ)
129	123, 76, 128	subaddd 11575	. . 3 ⊢ (𝜑 → (((♯‘𝑌) − (♯‘𝑍)) = Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧) ↔ ((♯‘𝑍) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧)) = (♯‘𝑌)))
130	120, 129	mpbird 260	. 2 ⊢ (𝜑 → ((♯‘𝑌) − (♯‘𝑍)) = Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧))
131	8, 130	breqtrrd 5132	1 ⊢ (𝜑 → 𝑃 ∥ ((♯‘𝑌) − (♯‘𝑍)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 = wceq 1563 ∈ wcel 2145 ∀wral 3079 ∃wrex 3089 {crab 3417 Vcvv 3457 ∖ cdif 3904 ∪ cun 3905 ∩ cin 3906 ⊆ wss 3907 ∅c0 4288 𝒫 cpw 4558 {csn 4585 {cpr 4587 ∪ cuni 4867 class class class wbr 5104 {copab 5166 ↦ cmpt 5185 × cxp 5649 dom cdm 5651 ran crn 5652 Rel wrel 5656 ‘cfv 6525 (class class class)co 7400 1_oc1o 8434 Er wer 8679 [cec 8680 / cqs 8681 ≈ cen 8928 Fincfn 8931 ℂcc 11086 1c1 11089 + caddc 11091 · cmul 11093 − cmin 11429 ℕ₀cn0 12492 ♯chash 14354 Σcsu 15725 ∥ cdvds 16298 Basecbs 17257 GrpAct cga 19347 pGrp cpgp 19584

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-rep 5231 ax-sep 5250 ax-nul 5260 ax-pow 5326 ax-pr 5394 ax-un 7722 ax-inf2 9598 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165 ax-pre-sup 11166

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-int 4908 df-iun 4953 df-disj 5072 df-br 5105 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6291 df-ord 6352 df-on 6353 df-lim 6354 df-suc 6355 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-isom 6534 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-om 7851 df-1st 7974 df-2nd 7975 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-1o 8441 df-2o 8442 df-oadd 8445 df-omul 8446 df-er 8682 df-ec 8684 df-qs 8688 df-map 8814 df-en 8932 df-dom 8933 df-sdom 8934 df-fin 8935 df-sup 9390 df-inf 9391 df-oi 9460 df-dju 9875 df-card 9913 df-acn 9916 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-div 11860 df-nn 12222 df-2 12291 df-3 12292 df-n0 12493 df-xnn0 12566 df-z 12580 df-uz 12851 df-q 12961 df-rp 13005 df-fz 13524 df-fzo 13671 df-fl 13813 df-mod 13891 df-seq 14026 df-exp 14086 df-fac 14298 df-bc 14327 df-hash 14355 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-clim 15527 df-sum 15726 df-dvds 16299 df-gcd 16541 df-prm 16718 df-pc 16885 df-sets 17212 df-slot 17230 df-ndx 17242 df-base 17258 df-ress 17279 df-plusg 17311 df-0g 17482 df-mgm 18686 df-sgrp 18765 df-mnd 18781 df-submnd 18830 df-grp 18991 df-minusg 18992 df-sbg 18993 df-mulg 19122 df-subg 19177 df-eqg 19179 df-ga 19348 df-od 19586 df-pgp 19588

This theorem is referenced by: sylow2blem3 19680 sylow3lem6 19690

W3C validator