sylow3lem3 - Metamath Proof Explorer

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

Theorem sylow3lem3 19559

Description: Lemma for sylow3 19563, first part. The number of Sylow subgroups is the same as the index (number of cosets) of the normalizer of the Sylow subgroup 𝐾. (Contributed by Mario Carneiro, 19-Jan-2015.)

**Hypotheses**
Ref	Expression
sylow3.x	⊢ 𝑋 = (Base‘𝐺)
sylow3.g	⊢ (𝜑 → 𝐺 ∈ Grp)
sylow3.xf	⊢ (𝜑 → 𝑋 ∈ Fin)
sylow3.p	⊢ (𝜑 → 𝑃 ∈ ℙ)
sylow3lem1.a	⊢ + = (+_g‘𝐺)
sylow3lem1.d	⊢ − = (-_g‘𝐺)
sylow3lem1.m	⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)))
sylow3lem2.k	⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺))
sylow3lem2.h	⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾}
sylow3lem2.n	⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝐾 ↔ (𝑦 + 𝑥) ∈ 𝐾)}

**Assertion**
Ref	Expression
sylow3lem3	⊢ (𝜑 → (♯‘(𝑃 pSyl 𝐺)) = (♯‘(𝑋 / (𝐺 ~_QG 𝑁))))

Distinct variable groups: 𝑥,𝑢,𝑦,𝑧, − 𝑢, ⊕ ,𝑥,𝑦,𝑧 𝑥,𝐻,𝑦 𝑢,𝐾,𝑥,𝑦,𝑧 𝑢,𝑁,𝑧 𝑢,𝑋,𝑥,𝑦,𝑧 𝑢,𝐺,𝑥,𝑦,𝑧 𝜑,𝑢,𝑥,𝑦,𝑧 𝑢, + ,𝑥,𝑦,𝑧 𝑢,𝑃,𝑥,𝑦,𝑧 Allowed substitution hints: 𝐻(𝑧,𝑢) 𝑁(𝑥,𝑦)

Proof of Theorem sylow3lem3 Dummy variables 𝑔 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sylow3.xf	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ Fin)
2		pwfi 9268	. . . . . 6 ⊢ (𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin)
3	1, 2	sylib 218	. . . . 5 ⊢ (𝜑 → 𝒫 𝑋 ∈ Fin)
4		slwsubg 19540	. . . . . . 7 ⊢ (𝑥 ∈ (𝑃 pSyl 𝐺) → 𝑥 ∈ (SubGrp‘𝐺))
5		sylow3.x	. . . . . . . . 9 ⊢ 𝑋 = (Base‘𝐺)
6	5	subgss 19059	. . . . . . . 8 ⊢ (𝑥 ∈ (SubGrp‘𝐺) → 𝑥 ⊆ 𝑋)
7	4, 6	syl 17	. . . . . . 7 ⊢ (𝑥 ∈ (𝑃 pSyl 𝐺) → 𝑥 ⊆ 𝑋)
8	4, 7	elpwd 4569	. . . . . 6 ⊢ (𝑥 ∈ (𝑃 pSyl 𝐺) → 𝑥 ∈ 𝒫 𝑋)
9	8	ssriv 3950	. . . . 5 ⊢ (𝑃 pSyl 𝐺) ⊆ 𝒫 𝑋
10		ssfi 9137	. . . . 5 ⊢ ((𝒫 𝑋 ∈ Fin ∧ (𝑃 pSyl 𝐺) ⊆ 𝒫 𝑋) → (𝑃 pSyl 𝐺) ∈ Fin)
11	3, 9, 10	sylancl 586	. . . 4 ⊢ (𝜑 → (𝑃 pSyl 𝐺) ∈ Fin)
12		hashcl 14321	. . . 4 ⊢ ((𝑃 pSyl 𝐺) ∈ Fin → (♯‘(𝑃 pSyl 𝐺)) ∈ ℕ₀)
13	11, 12	syl 17	. . 3 ⊢ (𝜑 → (♯‘(𝑃 pSyl 𝐺)) ∈ ℕ₀)
14	13	nn0cnd 12505	. 2 ⊢ (𝜑 → (♯‘(𝑃 pSyl 𝐺)) ∈ ℂ)
15		sylow3.g	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ Grp)
16		sylow3lem2.n	. . . . . . . 8 ⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝐾 ↔ (𝑦 + 𝑥) ∈ 𝐾)}
17		sylow3lem1.a	. . . . . . . 8 ⊢ + = (+_g‘𝐺)
18	16, 5, 17	nmzsubg 19097	. . . . . . 7 ⊢ (𝐺 ∈ Grp → 𝑁 ∈ (SubGrp‘𝐺))
19		eqid 2729	. . . . . . . 8 ⊢ (𝐺 ~_QG 𝑁) = (𝐺 ~_QG 𝑁)
20	5, 19	eqger 19110	. . . . . . 7 ⊢ (𝑁 ∈ (SubGrp‘𝐺) → (𝐺 ~_QG 𝑁) Er 𝑋)
21	15, 18, 20	3syl 18	. . . . . 6 ⊢ (𝜑 → (𝐺 ~_QG 𝑁) Er 𝑋)
22	21	qsss 8749	. . . . 5 ⊢ (𝜑 → (𝑋 / (𝐺 ~_QG 𝑁)) ⊆ 𝒫 𝑋)
23	3, 22	ssfid 9212	. . . 4 ⊢ (𝜑 → (𝑋 / (𝐺 ~_QG 𝑁)) ∈ Fin)
24		hashcl 14321	. . . 4 ⊢ ((𝑋 / (𝐺 ~_QG 𝑁)) ∈ Fin → (♯‘(𝑋 / (𝐺 ~_QG 𝑁))) ∈ ℕ₀)
25	23, 24	syl 17	. . 3 ⊢ (𝜑 → (♯‘(𝑋 / (𝐺 ~_QG 𝑁))) ∈ ℕ₀)
26	25	nn0cnd 12505	. 2 ⊢ (𝜑 → (♯‘(𝑋 / (𝐺 ~_QG 𝑁))) ∈ ℂ)
27	15, 18	syl 17	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ (SubGrp‘𝐺))
28		eqid 2729	. . . . . 6 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
29	28	subg0cl 19066	. . . . 5 ⊢ (𝑁 ∈ (SubGrp‘𝐺) → (0_g‘𝐺) ∈ 𝑁)
30		ne0i 4304	. . . . 5 ⊢ ((0_g‘𝐺) ∈ 𝑁 → 𝑁 ≠ ∅)
31	27, 29, 30	3syl 18	. . . 4 ⊢ (𝜑 → 𝑁 ≠ ∅)
32	5	subgss 19059	. . . . . . 7 ⊢ (𝑁 ∈ (SubGrp‘𝐺) → 𝑁 ⊆ 𝑋)
33	15, 18, 32	3syl 18	. . . . . 6 ⊢ (𝜑 → 𝑁 ⊆ 𝑋)
34	1, 33	ssfid 9212	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ Fin)
35		hashnncl 14331	. . . . 5 ⊢ (𝑁 ∈ Fin → ((♯‘𝑁) ∈ ℕ ↔ 𝑁 ≠ ∅))
36	34, 35	syl 17	. . . 4 ⊢ (𝜑 → ((♯‘𝑁) ∈ ℕ ↔ 𝑁 ≠ ∅))
37	31, 36	mpbird 257	. . 3 ⊢ (𝜑 → (♯‘𝑁) ∈ ℕ)
38	37	nncnd 12202	. 2 ⊢ (𝜑 → (♯‘𝑁) ∈ ℂ)
39	37	nnne0d 12236	. 2 ⊢ (𝜑 → (♯‘𝑁) ≠ 0)
40		sylow3.p	. . . . 5 ⊢ (𝜑 → 𝑃 ∈ ℙ)
41		sylow3lem1.d	. . . . 5 ⊢ − = (-_g‘𝐺)
42		sylow3lem1.m	. . . . 5 ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)))
43	5, 15, 1, 40, 17, 41, 42	sylow3lem1 19557	. . . 4 ⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct (𝑃 pSyl 𝐺)))
44		sylow3lem2.k	. . . 4 ⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺))
45		sylow3lem2.h	. . . . 5 ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾}
46		eqid 2729	. . . . 5 ⊢ (𝐺 ~_QG 𝐻) = (𝐺 ~_QG 𝐻)
47		eqid 2729	. . . . 5 ⊢ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}
48	5, 45, 46, 47	orbsta2 19246	. . . 4 ⊢ ((( ⊕ ∈ (𝐺 GrpAct (𝑃 pSyl 𝐺)) ∧ 𝐾 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑋 ∈ Fin) → (♯‘𝑋) = ((♯‘[𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}) · (♯‘𝐻)))
49	43, 44, 1, 48	syl21anc 837	. . 3 ⊢ (𝜑 → (♯‘𝑋) = ((♯‘[𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}) · (♯‘𝐻)))
50	5, 19, 27, 1	lagsubg2 19126	. . 3 ⊢ (𝜑 → (♯‘𝑋) = ((♯‘(𝑋 / (𝐺 ~_QG 𝑁))) · (♯‘𝑁)))
51	47, 5	gaorber 19240	. . . . . . . 8 ⊢ ( ⊕ ∈ (𝐺 GrpAct (𝑃 pSyl 𝐺)) → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} Er (𝑃 pSyl 𝐺))
52	43, 51	syl 17	. . . . . . 7 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} Er (𝑃 pSyl 𝐺))
53	52	ecss 8722	. . . . . 6 ⊢ (𝜑 → [𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} ⊆ (𝑃 pSyl 𝐺))
54	44	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → 𝐾 ∈ (𝑃 pSyl 𝐺))
55		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → ℎ ∈ (𝑃 pSyl 𝐺))
56	1	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → 𝑋 ∈ Fin)
57	5, 56, 55, 54, 17, 41	sylow2 19556	. . . . . . . . 9 ⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → ∃𝑢 ∈ 𝑋 ℎ = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
58		eqcom 2736	. . . . . . . . . . 11 ⊢ ((𝑢 ⊕ 𝐾) = ℎ ↔ ℎ = (𝑢 ⊕ 𝐾))
59		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → 𝑢 ∈ 𝑋)
60	54	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → 𝐾 ∈ (𝑃 pSyl 𝐺))
61		mptexg 7195	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (𝑃 pSyl 𝐺) → (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V)
62		rnexg 7878	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V → ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V)
63	60, 61, 62	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V)
64		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → 𝑦 = 𝐾)
65		simpl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → 𝑥 = 𝑢)
66	65	oveq1d 7402	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → (𝑥 + 𝑧) = (𝑢 + 𝑧))
67	66, 65	oveq12d 7405	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → ((𝑥 + 𝑧) − 𝑥) = ((𝑢 + 𝑧) − 𝑢))
68	64, 67	mpteq12dv 5194	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
69	68	rneqd 5902	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
70	69, 42	ovmpoga 7543	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∈ 𝑋 ∧ 𝐾 ∈ (𝑃 pSyl 𝐺) ∧ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
71	59, 60, 63, 70	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
72	71	eqeq2d 2740	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → (ℎ = (𝑢 ⊕ 𝐾) ↔ ℎ = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))))
73	58, 72	bitrid 283	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → ((𝑢 ⊕ 𝐾) = ℎ ↔ ℎ = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))))
74	73	rexbidva 3155	. . . . . . . . 9 ⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → (∃𝑢 ∈ 𝑋 (𝑢 ⊕ 𝐾) = ℎ ↔ ∃𝑢 ∈ 𝑋 ℎ = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))))
75	57, 74	mpbird 257	. . . . . . . 8 ⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → ∃𝑢 ∈ 𝑋 (𝑢 ⊕ 𝐾) = ℎ)
76	47	gaorb 19239	. . . . . . . 8 ⊢ (𝐾{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}ℎ ↔ (𝐾 ∈ (𝑃 pSyl 𝐺) ∧ ℎ ∈ (𝑃 pSyl 𝐺) ∧ ∃𝑢 ∈ 𝑋 (𝑢 ⊕ 𝐾) = ℎ))
77	54, 55, 75, 76	syl3anbrc 1344	. . . . . . 7 ⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → 𝐾{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}ℎ)
78		elecg 8715	. . . . . . . 8 ⊢ ((ℎ ∈ (𝑃 pSyl 𝐺) ∧ 𝐾 ∈ (𝑃 pSyl 𝐺)) → (ℎ ∈ [𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} ↔ 𝐾{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}ℎ))
79	55, 54, 78	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → (ℎ ∈ [𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} ↔ 𝐾{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}ℎ))
80	77, 79	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → ℎ ∈ [𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)})
81	53, 80	eqelssd 3968	. . . . 5 ⊢ (𝜑 → [𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} = (𝑃 pSyl 𝐺))
82	81	fveq2d 6862	. . . 4 ⊢ (𝜑 → (♯‘[𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}) = (♯‘(𝑃 pSyl 𝐺)))
83	5, 15, 1, 40, 17, 41, 42, 44, 45, 16	sylow3lem2 19558	. . . . 5 ⊢ (𝜑 → 𝐻 = 𝑁)
84	83	fveq2d 6862	. . . 4 ⊢ (𝜑 → (♯‘𝐻) = (♯‘𝑁))
85	82, 84	oveq12d 7405	. . 3 ⊢ (𝜑 → ((♯‘[𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}) · (♯‘𝐻)) = ((♯‘(𝑃 pSyl 𝐺)) · (♯‘𝑁)))
86	49, 50, 85	3eqtr3rd 2773	. 2 ⊢ (𝜑 → ((♯‘(𝑃 pSyl 𝐺)) · (♯‘𝑁)) = ((♯‘(𝑋 / (𝐺 ~_QG 𝑁))) · (♯‘𝑁)))
87	14, 26, 38, 39, 86	mulcan2ad 11814	1 ⊢ (𝜑 → (♯‘(𝑃 pSyl 𝐺)) = (♯‘(𝑋 / (𝐺 ~_QG 𝑁))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 {crab 3405 Vcvv 3447 ⊆ wss 3914 ∅c0 4296 𝒫 cpw 4563 {cpr 4591 class class class wbr 5107 {copab 5169 ↦ cmpt 5188 ran crn 5639 ‘cfv 6511 (class class class)co 7387 ∈ cmpo 7389 Er wer 8668 [cec 8669 / cqs 8670 Fincfn 8918 · cmul 11073 ℕcn 12186 ℕ₀cn0 12442 ♯chash 14295 ℙcprime 16641 Basecbs 17179 +_gcplusg 17220 0_gc0g 17402 Grpcgrp 18865 -_gcsg 18867 SubGrpcsubg 19052 ~_QG cqg 19054 GrpAct cga 19221 pSyl cslw 19457

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-inf2 9594 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145 ax-pre-sup 11146

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-disj 5075 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-se 5592 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-isom 6520 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-om 7843 df-1st 7968 df-2nd 7969 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-2o 8435 df-oadd 8438 df-omul 8439 df-er 8671 df-ec 8673 df-qs 8677 df-map 8801 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-sup 9393 df-inf 9394 df-oi 9463 df-dju 9854 df-card 9892 df-acn 9895 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-div 11836 df-nn 12187 df-2 12249 df-3 12250 df-n0 12443 df-xnn0 12516 df-z 12530 df-uz 12794 df-q 12908 df-rp 12952 df-fz 13469 df-fzo 13616 df-fl 13754 df-mod 13832 df-seq 13967 df-exp 14027 df-fac 14239 df-bc 14268 df-hash 14296 df-cj 15065 df-re 15066 df-im 15067 df-sqrt 15201 df-abs 15202 df-clim 15454 df-sum 15653 df-dvds 16223 df-gcd 16465 df-prm 16642 df-pc 16808 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-0g 17404 df-mgm 18567 df-sgrp 18646 df-mnd 18662 df-submnd 18711 df-grp 18868 df-minusg 18869 df-sbg 18870 df-mulg 19000 df-subg 19055 df-eqg 19057 df-ghm 19145 df-ga 19222 df-od 19458 df-pgp 19460 df-slw 19461

This theorem is referenced by: sylow3lem4 19560

W3C validator