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 19533

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 19532	. 2 ⊢ (𝜑 → 𝑃 ∥ Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧))
9		inass 4177	. . . . . . 7 ⊢ (((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∩ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)) = ((𝑌 / ∼ ) ∩ (𝒫 𝑍 ∩ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)))
10		disjdif 4421	. . . . . . . 8 ⊢ (𝒫 𝑍 ∩ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)) = ∅
11	10	ineq2i 4166	. . . . . . 7 ⊢ ((𝑌 / ∼ ) ∩ (𝒫 𝑍 ∩ ((𝑌 / ∼ ) ∖ 𝒫 𝑍))) = ((𝑌 / ∼ ) ∩ ∅)
12		in0 4344	. . . . . . 7 ⊢ ((𝑌 / ∼ ) ∩ ∅) = ∅
13	9, 11, 12	3eqtri 2760	. . . . . 6 ⊢ (((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∩ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)) = ∅
14	13	a1i 11	. . . . 5 ⊢ (𝜑 → (((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∩ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)) = ∅)
15		inundif 4428	. . . . . . 7 ⊢ (((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∪ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)) = (𝑌 / ∼ )
16	15	eqcomi 2742	. . . . . 6 ⊢ (𝑌 / ∼ ) = (((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∪ ((𝑌 / ∼ ) ∖ 𝒫 𝑍))
17	16	a1i 11	. . . . 5 ⊢ (𝜑 → (𝑌 / ∼ ) = (((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∪ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)))
18		pwfi 9210	. . . . . . 7 ⊢ (𝑌 ∈ Fin ↔ 𝒫 𝑌 ∈ Fin)
19	5, 18	sylib 218	. . . . . 6 ⊢ (𝜑 → 𝒫 𝑌 ∈ Fin)
20	7, 1	gaorber 19222	. . . . . . . 8 ⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → ∼ Er 𝑌)
21	2, 20	syl 17	. . . . . . 7 ⊢ (𝜑 → ∼ Er 𝑌)
22	21	qsss 8706	. . . . . 6 ⊢ (𝜑 → (𝑌 / ∼ ) ⊆ 𝒫 𝑌)
23	19, 22	ssfid 9160	. . . . 5 ⊢ (𝜑 → (𝑌 / ∼ ) ∈ Fin)
24	5	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑌 ∈ Fin)
25	22	sselda 3930	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑧 ∈ 𝒫 𝑌)
26	25	elpwid 4558	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑧 ⊆ 𝑌)
27	24, 26	ssfid 9160	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑧 ∈ Fin)
28		hashcl 14265	. . . . . . 7 ⊢ (𝑧 ∈ Fin → (♯‘𝑧) ∈ ℕ₀)
29	27, 28	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → (♯‘𝑧) ∈ ℕ₀)
30	29	nn0cnd 12451	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → (♯‘𝑧) ∈ ℂ)
31	14, 17, 23, 30	fsumsplit 15650	. . . 4 ⊢ (𝜑 → Σ𝑧 ∈ (𝑌 / ∼ )(♯‘𝑧) = (Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)(♯‘𝑧) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧)))
32	21, 5	qshash 15736	. . . 4 ⊢ (𝜑 → (♯‘𝑌) = Σ𝑧 ∈ (𝑌 / ∼ )(♯‘𝑧))
33		inss1 4186	. . . . . . . 8 ⊢ ((𝑌 / ∼ ) ∩ 𝒫 𝑍) ⊆ (𝑌 / ∼ )
34		ssfi 9089	. . . . . . . 8 ⊢ (((𝑌 / ∼ ) ∈ Fin ∧ ((𝑌 / ∼ ) ∩ 𝒫 𝑍) ⊆ (𝑌 / ∼ )) → ((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∈ Fin)
35	23, 33, 34	sylancl 586	. . . . . . 7 ⊢ (𝜑 → ((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∈ Fin)
36		ax-1cn 11071	. . . . . . 7 ⊢ 1 ∈ ℂ
37		fsumconst 15699	. . . . . . 7 ⊢ ((((𝑌 / ∼ ) ∩ 𝒫 𝑍) ∈ Fin ∧ 1 ∈ ℂ) → Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)1 = ((♯‘((𝑌 / ∼ ) ∩ 𝒫 𝑍)) · 1))
38	35, 36, 37	sylancl 586	. . . . . 6 ⊢ (𝜑 → Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)1 = ((♯‘((𝑌 / ∼ ) ∩ 𝒫 𝑍)) · 1))
39		elin 3914	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍) ↔ (𝑧 ∈ (𝑌 / ∼ ) ∧ 𝑧 ∈ 𝒫 𝑍))
40		eqid 2733	. . . . . . . . . . . . 13 ⊢ (𝑌 / ∼ ) = (𝑌 / ∼ )
41		sseq1 3956	. . . . . . . . . . . . . . 15 ⊢ ([𝑤] ∼ = 𝑧 → ([𝑤] ∼ ⊆ 𝑍 ↔ 𝑧 ⊆ 𝑍))
42		velpw 4554	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝒫 𝑍 ↔ 𝑧 ⊆ 𝑍)
43	41, 42	bitr4di 289	. . . . . . . . . . . . . 14 ⊢ ([𝑤] ∼ = 𝑧 → ([𝑤] ∼ ⊆ 𝑍 ↔ 𝑧 ∈ 𝒫 𝑍))
44		breq1 5096	. . . . . . . . . . . . . 14 ⊢ ([𝑤] ∼ = 𝑧 → ([𝑤] ∼ ≈ 1_o ↔ 𝑧 ≈ 1_o))
45	43, 44	imbi12d 344	. . . . . . . . . . . . 13 ⊢ ([𝑤] ∼ = 𝑧 → (([𝑤] ∼ ⊆ 𝑍 → [𝑤] ∼ ≈ 1_o) ↔ (𝑧 ∈ 𝒫 𝑍 → 𝑧 ≈ 1_o)))
46	21	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ∼ Er 𝑌)
47		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑤 ∈ 𝑌)
48	46, 47	erref 8648	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑤 ∼ 𝑤)
49		vex 3441	. . . . . . . . . . . . . . . . 17 ⊢ 𝑤 ∈ V
50	49, 49	elec 8674	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ [𝑤] ∼ ↔ 𝑤 ∼ 𝑤)
51	48, 50	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑤 ∈ [𝑤] ∼ )
52		ssel 3924	. . . . . . . . . . . . . . 15 ⊢ ([𝑤] ∼ ⊆ 𝑍 → (𝑤 ∈ [𝑤] ∼ → 𝑤 ∈ 𝑍))
53	51, 52	syl5com 31	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ([𝑤] ∼ ⊆ 𝑍 → 𝑤 ∈ 𝑍))
54	1, 2, 3, 4, 5, 6, 7	sylow2alem1 19531	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → [𝑤] ∼ = {𝑤})
55	49	ensn1 8950	. . . . . . . . . . . . . . . . 17 ⊢ {𝑤} ≈ 1_o
56	54, 55	eqbrtrdi 5132	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → [𝑤] ∼ ≈ 1_o)
57	56	ex 412	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑤 ∈ 𝑍 → [𝑤] ∼ ≈ 1_o))
58	57	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (𝑤 ∈ 𝑍 → [𝑤] ∼ ≈ 1_o))
59	53, 58	syld 47	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ([𝑤] ∼ ⊆ 𝑍 → [𝑤] ∼ ≈ 1_o))
60	40, 45, 59	ectocld 8712	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → (𝑧 ∈ 𝒫 𝑍 → 𝑧 ≈ 1_o))
61	60	impr 454	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝑌 / ∼ ) ∧ 𝑧 ∈ 𝒫 𝑍)) → 𝑧 ≈ 1_o)
62	39, 61	sylan2b 594	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → 𝑧 ≈ 1_o)
63		en1b 8954	. . . . . . . . . 10 ⊢ (𝑧 ≈ 1_o ↔ 𝑧 = {∪ 𝑧})
64	62, 63	sylib 218	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → 𝑧 = {∪ 𝑧})
65	64	fveq2d 6832	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → (♯‘𝑧) = (♯‘{∪ 𝑧}))
66		vuniex 7678	. . . . . . . . 9 ⊢ ∪ 𝑧 ∈ V
67		hashsng 14278	. . . . . . . . 9 ⊢ (∪ 𝑧 ∈ V → (♯‘{∪ 𝑧}) = 1)
68	66, 67	ax-mp 5	. . . . . . . 8 ⊢ (♯‘{∪ 𝑧}) = 1
69	65, 68	eqtrdi 2784	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → (♯‘𝑧) = 1)
70	69	sumeq2dv 15611	. . . . . 6 ⊢ (𝜑 → Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)(♯‘𝑧) = Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)1)
71	6	ssrab3 4031	. . . . . . . . . . 11 ⊢ 𝑍 ⊆ 𝑌
72		ssfi 9089	. . . . . . . . . . 11 ⊢ ((𝑌 ∈ Fin ∧ 𝑍 ⊆ 𝑌) → 𝑍 ∈ Fin)
73	5, 71, 72	sylancl 586	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ Fin)
74		hashcl 14265	. . . . . . . . . 10 ⊢ (𝑍 ∈ Fin → (♯‘𝑍) ∈ ℕ₀)
75	73, 74	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝑍) ∈ ℕ₀)
76	75	nn0cnd 12451	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝑍) ∈ ℂ)
77	76	mulridd 11136	. . . . . . 7 ⊢ (𝜑 → ((♯‘𝑍) · 1) = (♯‘𝑍))
78	6, 5	rabexd 5280	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ V)
79		eqid 2733	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑍 ↦ {𝑤}) = (𝑤 ∈ 𝑍 ↦ {𝑤})
80	7	relopabiv 5764	. . . . . . . . . . . . . . 15 ⊢ Rel ∼
81		relssdmrn 6221	. . . . . . . . . . . . . . 15 ⊢ (Rel ∼ → ∼ ⊆ (dom ∼ × ran ∼ ))
82	80, 81	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ∼ ⊆ (dom ∼ × ran ∼ )
83		erdm 8638	. . . . . . . . . . . . . . . . 17 ⊢ ( ∼ Er 𝑌 → dom ∼ = 𝑌)
84	21, 83	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom ∼ = 𝑌)
85	84, 5	eqeltrd 2833	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom ∼ ∈ Fin)
86		errn 8650	. . . . . . . . . . . . . . . . 17 ⊢ ( ∼ Er 𝑌 → ran ∼ = 𝑌)
87	21, 86	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran ∼ = 𝑌)
88	87, 5	eqeltrd 2833	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran ∼ ∈ Fin)
89	85, 88	xpexd 7690	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (dom ∼ × ran ∼ ) ∈ V)
90		ssexg 5263	. . . . . . . . . . . . . 14 ⊢ (( ∼ ⊆ (dom ∼ × ran ∼ ) ∧ (dom ∼ × ran ∼ ) ∈ V) → ∼ ∈ V)
91	82, 89, 90	sylancr 587	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∼ ∈ V)
92		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ 𝑍)
93	71, 92	sselid 3928	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ 𝑌)
94		ecelqsw 8699	. . . . . . . . . . . . 13 ⊢ (( ∼ ∈ V ∧ 𝑤 ∈ 𝑌) → [𝑤] ∼ ∈ (𝑌 / ∼ ))
95	91, 93, 94	syl2an2r 685	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → [𝑤] ∼ ∈ (𝑌 / ∼ ))
96	54, 95	eqeltrrd 2834	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {𝑤} ∈ (𝑌 / ∼ ))
97		snelpwi 5387	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ 𝑍 → {𝑤} ∈ 𝒫 𝑍)
98	97	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {𝑤} ∈ 𝒫 𝑍)
99	96, 98	elind 4149	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {𝑤} ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍))
100		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍))
101	100	elin2d 4154	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → 𝑧 ∈ 𝒫 𝑍)
102	101	elpwid 4558	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → 𝑧 ⊆ 𝑍)
103	64, 102	eqsstrrd 3966	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → {∪ 𝑧} ⊆ 𝑍)
104	66	snss 4736	. . . . . . . . . . 11 ⊢ (∪ 𝑧 ∈ 𝑍 ↔ {∪ 𝑧} ⊆ 𝑍)
105	103, 104	sylibr 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → ∪ 𝑧 ∈ 𝑍)
106		sneq 4585	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ∪ 𝑧 → {𝑤} = {∪ 𝑧})
107	106	eqeq2d 2744	. . . . . . . . . . . . 13 ⊢ (𝑤 = ∪ 𝑧 → (𝑧 = {𝑤} ↔ 𝑧 = {∪ 𝑧}))
108	64, 107	syl5ibrcom 247	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)) → (𝑤 = ∪ 𝑧 → 𝑧 = {𝑤}))
109	108	adantrl 716	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑍 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍))) → (𝑤 = ∪ 𝑧 → 𝑧 = {𝑤}))
110		unieq 4869	. . . . . . . . . . . 12 ⊢ (𝑧 = {𝑤} → ∪ 𝑧 = ∪ {𝑤})
111		unisnv 4878	. . . . . . . . . . . 12 ⊢ ∪ {𝑤} = 𝑤
112	110, 111	eqtr2di 2785	. . . . . . . . . . 11 ⊢ (𝑧 = {𝑤} → 𝑤 = ∪ 𝑧)
113	109, 112	impbid1 225	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑍 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍))) → (𝑤 = ∪ 𝑧 ↔ 𝑧 = {𝑤}))
114	79, 99, 105, 113	f1o2d 7606	. . . . . . . . 9 ⊢ (𝜑 → (𝑤 ∈ 𝑍 ↦ {𝑤}):𝑍–1-1-onto→((𝑌 / ∼ ) ∩ 𝒫 𝑍))
115	78, 114	hasheqf1od 14262	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝑍) = (♯‘((𝑌 / ∼ ) ∩ 𝒫 𝑍)))
116	115	oveq1d 7367	. . . . . . 7 ⊢ (𝜑 → ((♯‘𝑍) · 1) = ((♯‘((𝑌 / ∼ ) ∩ 𝒫 𝑍)) · 1))
117	77, 116	eqtr3d 2770	. . . . . 6 ⊢ (𝜑 → (♯‘𝑍) = ((♯‘((𝑌 / ∼ ) ∩ 𝒫 𝑍)) · 1))
118	38, 70, 117	3eqtr4rd 2779	. . . . 5 ⊢ (𝜑 → (♯‘𝑍) = Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)(♯‘𝑧))
119	118	oveq1d 7367	. . . 4 ⊢ (𝜑 → ((♯‘𝑍) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧)) = (Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫 𝑍)(♯‘𝑧) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧)))
120	31, 32, 119	3eqtr4rd 2779	. . 3 ⊢ (𝜑 → ((♯‘𝑍) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧)) = (♯‘𝑌))
121		hashcl 14265	. . . . . 6 ⊢ (𝑌 ∈ Fin → (♯‘𝑌) ∈ ℕ₀)
122	5, 121	syl 17	. . . . 5 ⊢ (𝜑 → (♯‘𝑌) ∈ ℕ₀)
123	122	nn0cnd 12451	. . . 4 ⊢ (𝜑 → (♯‘𝑌) ∈ ℂ)
124		diffi 9091	. . . . . 6 ⊢ ((𝑌 / ∼ ) ∈ Fin → ((𝑌 / ∼ ) ∖ 𝒫 𝑍) ∈ Fin)
125	23, 124	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑌 / ∼ ) ∖ 𝒫 𝑍) ∈ Fin)
126		eldifi 4080	. . . . . 6 ⊢ (𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍) → 𝑧 ∈ (𝑌 / ∼ ))
127	126, 30	sylan2 593	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)) → (♯‘𝑧) ∈ ℂ)
128	125, 127	fsumcl 15642	. . . 4 ⊢ (𝜑 → Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧) ∈ ℂ)
129	123, 76, 128	subaddd 11497	. . 3 ⊢ (𝜑 → (((♯‘𝑌) − (♯‘𝑍)) = Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧) ↔ ((♯‘𝑍) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧)) = (♯‘𝑌)))
130	120, 129	mpbird 257	. 2 ⊢ (𝜑 → ((♯‘𝑌) − (♯‘𝑍)) = Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧))
131	8, 130	breqtrrd 5121	1 ⊢ (𝜑 → 𝑃 ∥ ((♯‘𝑌) − (♯‘𝑍)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2113 ∀wral 3048 ∃wrex 3057 {crab 3396 Vcvv 3437 ∖ cdif 3895 ∪ cun 3896 ∩ cin 3897 ⊆ wss 3898 ∅c0 4282 𝒫 cpw 4549 {csn 4575 {cpr 4577 ∪ cuni 4858 class class class wbr 5093 {copab 5155 ↦ cmpt 5174 × cxp 5617 dom cdm 5619 ran crn 5620 Rel wrel 5624 ‘cfv 6486 (class class class)co 7352 1_oc1o 8384 Er wer 8625 [cec 8626 / cqs 8627 ≈ cen 8872 Fincfn 8875 ℂcc 11011 1c1 11014 + caddc 11016 · cmul 11018 − cmin 11351 ℕ₀cn0 12388 ♯chash 14239 Σcsu 15595 ∥ cdvds 16165 Basecbs 17122 GrpAct cga 19203 pGrp cpgp 19440

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5219 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-inf2 9538 ax-cnex 11069 ax-resscn 11070 ax-1cn 11071 ax-icn 11072 ax-addcl 11073 ax-addrcl 11074 ax-mulcl 11075 ax-mulrcl 11076 ax-mulcom 11077 ax-addass 11078 ax-mulass 11079 ax-distr 11080 ax-i2m1 11081 ax-1ne0 11082 ax-1rid 11083 ax-rnegex 11084 ax-rrecex 11085 ax-cnre 11086 ax-pre-lttri 11087 ax-pre-lttrn 11088 ax-pre-ltadd 11089 ax-pre-mulgt0 11090 ax-pre-sup 11091

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-op 4582 df-uni 4859 df-int 4898 df-iun 4943 df-disj 5061 df-br 5094 df-opab 5156 df-mpt 5175 df-tr 5201 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-isom 6495 df-riota 7309 df-ov 7355 df-oprab 7356 df-mpo 7357 df-om 7803 df-1st 7927 df-2nd 7928 df-frecs 8217 df-wrecs 8248 df-recs 8297 df-rdg 8335 df-1o 8391 df-2o 8392 df-oadd 8395 df-omul 8396 df-er 8628 df-ec 8630 df-qs 8634 df-map 8758 df-en 8876 df-dom 8877 df-sdom 8878 df-fin 8879 df-sup 9333 df-inf 9334 df-oi 9403 df-dju 9801 df-card 9839 df-acn 9842 df-pnf 11155 df-mnf 11156 df-xr 11157 df-ltxr 11158 df-le 11159 df-sub 11353 df-neg 11354 df-div 11782 df-nn 12133 df-2 12195 df-3 12196 df-n0 12389 df-xnn0 12462 df-z 12476 df-uz 12739 df-q 12849 df-rp 12893 df-fz 13410 df-fzo 13557 df-fl 13698 df-mod 13776 df-seq 13911 df-exp 13971 df-fac 14183 df-bc 14212 df-hash 14240 df-cj 15008 df-re 15009 df-im 15010 df-sqrt 15144 df-abs 15145 df-clim 15397 df-sum 15596 df-dvds 16166 df-gcd 16408 df-prm 16585 df-pc 16751 df-sets 17077 df-slot 17095 df-ndx 17107 df-base 17123 df-ress 17144 df-plusg 17176 df-0g 17347 df-mgm 18550 df-sgrp 18629 df-mnd 18645 df-submnd 18694 df-grp 18851 df-minusg 18852 df-sbg 18853 df-mulg 18983 df-subg 19038 df-eqg 19040 df-ga 19204 df-od 19442 df-pgp 19444

This theorem is referenced by: sylow2blem3 19536 sylow3lem6 19546

W3C validator