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 19527

Description: Lemma for sylow3 19531, 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 9226	. . . . . 6 ⊢ (𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin)
3	1, 2	sylib 218	. . . . 5 ⊢ (𝜑 → 𝒫 𝑋 ∈ Fin)
4		slwsubg 19508	. . . . . . 7 ⊢ (𝑥 ∈ (𝑃 pSyl 𝐺) → 𝑥 ∈ (SubGrp‘𝐺))
5		sylow3.x	. . . . . . . . 9 ⊢ 𝑋 = (Base‘𝐺)
6	5	subgss 19025	. . . . . . . 8 ⊢ (𝑥 ∈ (SubGrp‘𝐺) → 𝑥 ⊆ 𝑋)
7	4, 6	syl 17	. . . . . . 7 ⊢ (𝑥 ∈ (𝑃 pSyl 𝐺) → 𝑥 ⊆ 𝑋)
8	4, 7	elpwd 4559	. . . . . 6 ⊢ (𝑥 ∈ (𝑃 pSyl 𝐺) → 𝑥 ∈ 𝒫 𝑋)
9	8	ssriv 3941	. . . . 5 ⊢ (𝑃 pSyl 𝐺) ⊆ 𝒫 𝑋
10		ssfi 9097	. . . . 5 ⊢ ((𝒫 𝑋 ∈ Fin ∧ (𝑃 pSyl 𝐺) ⊆ 𝒫 𝑋) → (𝑃 pSyl 𝐺) ∈ Fin)
11	3, 9, 10	sylancl 586	. . . 4 ⊢ (𝜑 → (𝑃 pSyl 𝐺) ∈ Fin)
12		hashcl 14282	. . . 4 ⊢ ((𝑃 pSyl 𝐺) ∈ Fin → (♯‘(𝑃 pSyl 𝐺)) ∈ ℕ₀)
13	11, 12	syl 17	. . 3 ⊢ (𝜑 → (♯‘(𝑃 pSyl 𝐺)) ∈ ℕ₀)
14	13	nn0cnd 12466	. 2 ⊢ (𝜑 → (♯‘(𝑃 pSyl 𝐺)) ∈ ℂ)
15		sylow3.g	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ Grp)
16		sylow3lem2.n	. . . . . . . 8 ⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝐾 ↔ (𝑦 + 𝑥) ∈ 𝐾)}
17		sylow3lem1.a	. . . . . . . 8 ⊢ + = (+_g‘𝐺)
18	16, 5, 17	nmzsubg 19063	. . . . . . 7 ⊢ (𝐺 ∈ Grp → 𝑁 ∈ (SubGrp‘𝐺))
19		eqid 2729	. . . . . . . 8 ⊢ (𝐺 ~_QG 𝑁) = (𝐺 ~_QG 𝑁)
20	5, 19	eqger 19076	. . . . . . 7 ⊢ (𝑁 ∈ (SubGrp‘𝐺) → (𝐺 ~_QG 𝑁) Er 𝑋)
21	15, 18, 20	3syl 18	. . . . . 6 ⊢ (𝜑 → (𝐺 ~_QG 𝑁) Er 𝑋)
22	21	qsss 8710	. . . . 5 ⊢ (𝜑 → (𝑋 / (𝐺 ~_QG 𝑁)) ⊆ 𝒫 𝑋)
23	3, 22	ssfid 9170	. . . 4 ⊢ (𝜑 → (𝑋 / (𝐺 ~_QG 𝑁)) ∈ Fin)
24		hashcl 14282	. . . 4 ⊢ ((𝑋 / (𝐺 ~_QG 𝑁)) ∈ Fin → (♯‘(𝑋 / (𝐺 ~_QG 𝑁))) ∈ ℕ₀)
25	23, 24	syl 17	. . 3 ⊢ (𝜑 → (♯‘(𝑋 / (𝐺 ~_QG 𝑁))) ∈ ℕ₀)
26	25	nn0cnd 12466	. 2 ⊢ (𝜑 → (♯‘(𝑋 / (𝐺 ~_QG 𝑁))) ∈ ℂ)
27	15, 18	syl 17	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ (SubGrp‘𝐺))
28		eqid 2729	. . . . . 6 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
29	28	subg0cl 19032	. . . . 5 ⊢ (𝑁 ∈ (SubGrp‘𝐺) → (0_g‘𝐺) ∈ 𝑁)
30		ne0i 4294	. . . . 5 ⊢ ((0_g‘𝐺) ∈ 𝑁 → 𝑁 ≠ ∅)
31	27, 29, 30	3syl 18	. . . 4 ⊢ (𝜑 → 𝑁 ≠ ∅)
32	5	subgss 19025	. . . . . . 7 ⊢ (𝑁 ∈ (SubGrp‘𝐺) → 𝑁 ⊆ 𝑋)
33	15, 18, 32	3syl 18	. . . . . 6 ⊢ (𝜑 → 𝑁 ⊆ 𝑋)
34	1, 33	ssfid 9170	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ Fin)
35		hashnncl 14292	. . . . 5 ⊢ (𝑁 ∈ Fin → ((♯‘𝑁) ∈ ℕ ↔ 𝑁 ≠ ∅))
36	34, 35	syl 17	. . . 4 ⊢ (𝜑 → ((♯‘𝑁) ∈ ℕ ↔ 𝑁 ≠ ∅))
37	31, 36	mpbird 257	. . 3 ⊢ (𝜑 → (♯‘𝑁) ∈ ℕ)
38	37	nncnd 12163	. 2 ⊢ (𝜑 → (♯‘𝑁) ∈ ℂ)
39	37	nnne0d 12197	. 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 19525	. . . 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 19212	. . . 4 ⊢ ((( ⊕ ∈ (𝐺 GrpAct (𝑃 pSyl 𝐺)) ∧ 𝐾 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑋 ∈ Fin) → (♯‘𝑋) = ((♯‘[𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}) · (♯‘𝐻)))
49	43, 44, 1, 48	syl21anc 837	. . 3 ⊢ (𝜑 → (♯‘𝑋) = ((♯‘[𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}) · (♯‘𝐻)))
50	5, 19, 27, 1	lagsubg2 19092	. . 3 ⊢ (𝜑 → (♯‘𝑋) = ((♯‘(𝑋 / (𝐺 ~_QG 𝑁))) · (♯‘𝑁)))
51	47, 5	gaorber 19206	. . . . . . . 8 ⊢ ( ⊕ ∈ (𝐺 GrpAct (𝑃 pSyl 𝐺)) → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} Er (𝑃 pSyl 𝐺))
52	43, 51	syl 17	. . . . . . 7 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} Er (𝑃 pSyl 𝐺))
53	52	ecss 8683	. . . . . 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 19524	. . . . . . . . 9 ⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → ∃𝑢 ∈ 𝑋 ℎ = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
58		eqcom 2736	. . . . . . . . . . 11 ⊢ ((𝑢 ⊕ 𝐾) = ℎ ↔ ℎ = (𝑢 ⊕ 𝐾))
59		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → 𝑢 ∈ 𝑋)
60	54	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → 𝐾 ∈ (𝑃 pSyl 𝐺))
61		mptexg 7161	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (𝑃 pSyl 𝐺) → (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V)
62		rnexg 7842	. . . . . . . . . . . . . 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 7368	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → (𝑥 + 𝑧) = (𝑢 + 𝑧))
67	66, 65	oveq12d 7371	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → ((𝑥 + 𝑧) − 𝑥) = ((𝑢 + 𝑧) − 𝑢))
68	64, 67	mpteq12dv 5182	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
69	68	rneqd 5884	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
70	69, 42	ovmpoga 7507	. . . . . . . . . . . . 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 3151	. . . . . . . . 9 ⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → (∃𝑢 ∈ 𝑋 (𝑢 ⊕ 𝐾) = ℎ ↔ ∃𝑢 ∈ 𝑋 ℎ = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))))
75	57, 74	mpbird 257	. . . . . . . 8 ⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → ∃𝑢 ∈ 𝑋 (𝑢 ⊕ 𝐾) = ℎ)
76	47	gaorb 19205	. . . . . . . 8 ⊢ (𝐾{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}ℎ ↔ (𝐾 ∈ (𝑃 pSyl 𝐺) ∧ ℎ ∈ (𝑃 pSyl 𝐺) ∧ ∃𝑢 ∈ 𝑋 (𝑢 ⊕ 𝐾) = ℎ))
77	54, 55, 75, 76	syl3anbrc 1344	. . . . . . 7 ⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → 𝐾{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}ℎ)
78		elecg 8676	. . . . . . . 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 3959	. . . . 5 ⊢ (𝜑 → [𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} = (𝑃 pSyl 𝐺))
82	81	fveq2d 6830	. . . 4 ⊢ (𝜑 → (♯‘[𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}) = (♯‘(𝑃 pSyl 𝐺)))
83	5, 15, 1, 40, 17, 41, 42, 44, 45, 16	sylow3lem2 19526	. . . . 5 ⊢ (𝜑 → 𝐻 = 𝑁)
84	83	fveq2d 6830	. . . 4 ⊢ (𝜑 → (♯‘𝐻) = (♯‘𝑁))
85	82, 84	oveq12d 7371	. . 3 ⊢ (𝜑 → ((♯‘[𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}) · (♯‘𝐻)) = ((♯‘(𝑃 pSyl 𝐺)) · (♯‘𝑁)))
86	49, 50, 85	3eqtr3rd 2773	. 2 ⊢ (𝜑 → ((♯‘(𝑃 pSyl 𝐺)) · (♯‘𝑁)) = ((♯‘(𝑋 / (𝐺 ~_QG 𝑁))) · (♯‘𝑁)))
87	14, 26, 38, 39, 86	mulcan2ad 11775	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 3396 Vcvv 3438 ⊆ wss 3905 ∅c0 4286 𝒫 cpw 4553 {cpr 4581 class class class wbr 5095 {copab 5157 ↦ cmpt 5176 ran crn 5624 ‘cfv 6486 (class class class)co 7353 ∈ cmpo 7355 Er wer 8629 [cec 8630 / cqs 8631 Fincfn 8879 · cmul 11033 ℕcn 12147 ℕ₀cn0 12403 ♯chash 14256 ℙcprime 16601 Basecbs 17139 +_gcplusg 17180 0_gc0g 17362 Grpcgrp 18831 -_gcsg 18833 SubGrpcsubg 19018 ~_QG cqg 19020 GrpAct cga 19187 pSyl cslw 19425

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 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-inf2 9556 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-pre-sup 11106

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 3345 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4862 df-int 4900 df-iun 4946 df-disj 5063 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-se 5577 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 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 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-oadd 8399 df-omul 8400 df-er 8632 df-ec 8634 df-qs 8638 df-map 8762 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-sup 9351 df-inf 9352 df-oi 9421 df-dju 9816 df-card 9854 df-acn 9857 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-div 11797 df-nn 12148 df-2 12210 df-3 12211 df-n0 12404 df-xnn0 12477 df-z 12491 df-uz 12755 df-q 12869 df-rp 12913 df-fz 13430 df-fzo 13577 df-fl 13715 df-mod 13793 df-seq 13928 df-exp 13988 df-fac 14200 df-bc 14229 df-hash 14257 df-cj 15025 df-re 15026 df-im 15027 df-sqrt 15161 df-abs 15162 df-clim 15414 df-sum 15613 df-dvds 16183 df-gcd 16425 df-prm 16602 df-pc 16768 df-sets 17094 df-slot 17112 df-ndx 17124 df-base 17140 df-ress 17161 df-plusg 17193 df-0g 17364 df-mgm 18533 df-sgrp 18612 df-mnd 18628 df-submnd 18677 df-grp 18834 df-minusg 18835 df-sbg 18836 df-mulg 18966 df-subg 19021 df-eqg 19023 df-ghm 19111 df-ga 19188 df-od 19426 df-pgp 19428 df-slw 19429

This theorem is referenced by: sylow3lem4 19528

W3C validator