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 19558

Description: Lemma for sylow3 19562, 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 9219	. . . . . 6 ⊢ (𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin)
3	1, 2	sylib 218	. . . . 5 ⊢ (𝜑 → 𝒫 𝑋 ∈ Fin)
4		slwsubg 19539	. . . . . . 7 ⊢ (𝑥 ∈ (𝑃 pSyl 𝐺) → 𝑥 ∈ (SubGrp‘𝐺))
5		sylow3.x	. . . . . . . . 9 ⊢ 𝑋 = (Base‘𝐺)
6	5	subgss 19057	. . . . . . . 8 ⊢ (𝑥 ∈ (SubGrp‘𝐺) → 𝑥 ⊆ 𝑋)
7	4, 6	syl 17	. . . . . . 7 ⊢ (𝑥 ∈ (𝑃 pSyl 𝐺) → 𝑥 ⊆ 𝑋)
8	4, 7	elpwd 4560	. . . . . 6 ⊢ (𝑥 ∈ (𝑃 pSyl 𝐺) → 𝑥 ∈ 𝒫 𝑋)
9	8	ssriv 3937	. . . . 5 ⊢ (𝑃 pSyl 𝐺) ⊆ 𝒫 𝑋
10		ssfi 9097	. . . . 5 ⊢ ((𝒫 𝑋 ∈ Fin ∧ (𝑃 pSyl 𝐺) ⊆ 𝒫 𝑋) → (𝑃 pSyl 𝐺) ∈ Fin)
11	3, 9, 10	sylancl 586	. . . 4 ⊢ (𝜑 → (𝑃 pSyl 𝐺) ∈ Fin)
12		hashcl 14279	. . . 4 ⊢ ((𝑃 pSyl 𝐺) ∈ Fin → (♯‘(𝑃 pSyl 𝐺)) ∈ ℕ₀)
13	11, 12	syl 17	. . 3 ⊢ (𝜑 → (♯‘(𝑃 pSyl 𝐺)) ∈ ℕ₀)
14	13	nn0cnd 12464	. 2 ⊢ (𝜑 → (♯‘(𝑃 pSyl 𝐺)) ∈ ℂ)
15		sylow3.g	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ Grp)
16		sylow3lem2.n	. . . . . . . 8 ⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝐾 ↔ (𝑦 + 𝑥) ∈ 𝐾)}
17		sylow3lem1.a	. . . . . . . 8 ⊢ + = (+_g‘𝐺)
18	16, 5, 17	nmzsubg 19094	. . . . . . 7 ⊢ (𝐺 ∈ Grp → 𝑁 ∈ (SubGrp‘𝐺))
19		eqid 2736	. . . . . . . 8 ⊢ (𝐺 ~_QG 𝑁) = (𝐺 ~_QG 𝑁)
20	5, 19	eqger 19107	. . . . . . 7 ⊢ (𝑁 ∈ (SubGrp‘𝐺) → (𝐺 ~_QG 𝑁) Er 𝑋)
21	15, 18, 20	3syl 18	. . . . . 6 ⊢ (𝜑 → (𝐺 ~_QG 𝑁) Er 𝑋)
22	21	qsss 8713	. . . . 5 ⊢ (𝜑 → (𝑋 / (𝐺 ~_QG 𝑁)) ⊆ 𝒫 𝑋)
23	3, 22	ssfid 9169	. . . 4 ⊢ (𝜑 → (𝑋 / (𝐺 ~_QG 𝑁)) ∈ Fin)
24		hashcl 14279	. . . 4 ⊢ ((𝑋 / (𝐺 ~_QG 𝑁)) ∈ Fin → (♯‘(𝑋 / (𝐺 ~_QG 𝑁))) ∈ ℕ₀)
25	23, 24	syl 17	. . 3 ⊢ (𝜑 → (♯‘(𝑋 / (𝐺 ~_QG 𝑁))) ∈ ℕ₀)
26	25	nn0cnd 12464	. 2 ⊢ (𝜑 → (♯‘(𝑋 / (𝐺 ~_QG 𝑁))) ∈ ℂ)
27	15, 18	syl 17	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ (SubGrp‘𝐺))
28		eqid 2736	. . . . . 6 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
29	28	subg0cl 19064	. . . . 5 ⊢ (𝑁 ∈ (SubGrp‘𝐺) → (0_g‘𝐺) ∈ 𝑁)
30		ne0i 4293	. . . . 5 ⊢ ((0_g‘𝐺) ∈ 𝑁 → 𝑁 ≠ ∅)
31	27, 29, 30	3syl 18	. . . 4 ⊢ (𝜑 → 𝑁 ≠ ∅)
32	5	subgss 19057	. . . . . . 7 ⊢ (𝑁 ∈ (SubGrp‘𝐺) → 𝑁 ⊆ 𝑋)
33	15, 18, 32	3syl 18	. . . . . 6 ⊢ (𝜑 → 𝑁 ⊆ 𝑋)
34	1, 33	ssfid 9169	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ Fin)
35		hashnncl 14289	. . . . 5 ⊢ (𝑁 ∈ Fin → ((♯‘𝑁) ∈ ℕ ↔ 𝑁 ≠ ∅))
36	34, 35	syl 17	. . . 4 ⊢ (𝜑 → ((♯‘𝑁) ∈ ℕ ↔ 𝑁 ≠ ∅))
37	31, 36	mpbird 257	. . 3 ⊢ (𝜑 → (♯‘𝑁) ∈ ℕ)
38	37	nncnd 12161	. 2 ⊢ (𝜑 → (♯‘𝑁) ∈ ℂ)
39	37	nnne0d 12195	. 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 19556	. . . 4 ⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct (𝑃 pSyl 𝐺)))
44		sylow3lem2.k	. . . 4 ⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺))
45		sylow3lem2.h	. . . . 5 ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾}
46		eqid 2736	. . . . 5 ⊢ (𝐺 ~_QG 𝐻) = (𝐺 ~_QG 𝐻)
47		eqid 2736	. . . . 5 ⊢ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}
48	5, 45, 46, 47	orbsta2 19243	. . . 4 ⊢ ((( ⊕ ∈ (𝐺 GrpAct (𝑃 pSyl 𝐺)) ∧ 𝐾 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑋 ∈ Fin) → (♯‘𝑋) = ((♯‘[𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}) · (♯‘𝐻)))
49	43, 44, 1, 48	syl21anc 837	. . 3 ⊢ (𝜑 → (♯‘𝑋) = ((♯‘[𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}) · (♯‘𝐻)))
50	5, 19, 27, 1	lagsubg2 19123	. . 3 ⊢ (𝜑 → (♯‘𝑋) = ((♯‘(𝑋 / (𝐺 ~_QG 𝑁))) · (♯‘𝑁)))
51	47, 5	gaorber 19237	. . . . . . . 8 ⊢ ( ⊕ ∈ (𝐺 GrpAct (𝑃 pSyl 𝐺)) → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} Er (𝑃 pSyl 𝐺))
52	43, 51	syl 17	. . . . . . 7 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} Er (𝑃 pSyl 𝐺))
53	52	ecss 8686	. . . . . 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 19555	. . . . . . . . 9 ⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → ∃𝑢 ∈ 𝑋 ℎ = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
58		eqcom 2743	. . . . . . . . . . 11 ⊢ ((𝑢 ⊕ 𝐾) = ℎ ↔ ℎ = (𝑢 ⊕ 𝐾))
59		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → 𝑢 ∈ 𝑋)
60	54	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → 𝐾 ∈ (𝑃 pSyl 𝐺))
61		mptexg 7167	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (𝑃 pSyl 𝐺) → (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V)
62		rnexg 7844	. . . . . . . . . . . . . 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 7373	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → (𝑥 + 𝑧) = (𝑢 + 𝑧))
67	66, 65	oveq12d 7376	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → ((𝑥 + 𝑧) − 𝑥) = ((𝑢 + 𝑧) − 𝑢))
68	64, 67	mpteq12dv 5185	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
69	68	rneqd 5887	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
70	69, 42	ovmpoga 7512	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∈ 𝑋 ∧ 𝐾 ∈ (𝑃 pSyl 𝐺) ∧ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
71	59, 60, 63, 70	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
72	71	eqeq2d 2747	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → (ℎ = (𝑢 ⊕ 𝐾) ↔ ℎ = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))))
73	58, 72	bitrid 283	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → ((𝑢 ⊕ 𝐾) = ℎ ↔ ℎ = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))))
74	73	rexbidva 3158	. . . . . . . . 9 ⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → (∃𝑢 ∈ 𝑋 (𝑢 ⊕ 𝐾) = ℎ ↔ ∃𝑢 ∈ 𝑋 ℎ = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))))
75	57, 74	mpbird 257	. . . . . . . 8 ⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → ∃𝑢 ∈ 𝑋 (𝑢 ⊕ 𝐾) = ℎ)
76	47	gaorb 19236	. . . . . . . 8 ⊢ (𝐾{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}ℎ ↔ (𝐾 ∈ (𝑃 pSyl 𝐺) ∧ ℎ ∈ (𝑃 pSyl 𝐺) ∧ ∃𝑢 ∈ 𝑋 (𝑢 ⊕ 𝐾) = ℎ))
77	54, 55, 75, 76	syl3anbrc 1344	. . . . . . 7 ⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → 𝐾{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}ℎ)
78		elecg 8679	. . . . . . . 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 3955	. . . . 5 ⊢ (𝜑 → [𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} = (𝑃 pSyl 𝐺))
82	81	fveq2d 6838	. . . 4 ⊢ (𝜑 → (♯‘[𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}) = (♯‘(𝑃 pSyl 𝐺)))
83	5, 15, 1, 40, 17, 41, 42, 44, 45, 16	sylow3lem2 19557	. . . . 5 ⊢ (𝜑 → 𝐻 = 𝑁)
84	83	fveq2d 6838	. . . 4 ⊢ (𝜑 → (♯‘𝐻) = (♯‘𝑁))
85	82, 84	oveq12d 7376	. . 3 ⊢ (𝜑 → ((♯‘[𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}) · (♯‘𝐻)) = ((♯‘(𝑃 pSyl 𝐺)) · (♯‘𝑁)))
86	49, 50, 85	3eqtr3rd 2780	. 2 ⊢ (𝜑 → ((♯‘(𝑃 pSyl 𝐺)) · (♯‘𝑁)) = ((♯‘(𝑋 / (𝐺 ~_QG 𝑁))) · (♯‘𝑁)))
87	14, 26, 38, 39, 86	mulcan2ad 11773	1 ⊢ (𝜑 → (♯‘(𝑃 pSyl 𝐺)) = (♯‘(𝑋 / (𝐺 ~_QG 𝑁))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∈ wcel 2113 ≠ wne 2932 ∀wral 3051 ∃wrex 3060 {crab 3399 Vcvv 3440 ⊆ wss 3901 ∅c0 4285 𝒫 cpw 4554 {cpr 4582 class class class wbr 5098 {copab 5160 ↦ cmpt 5179 ran crn 5625 ‘cfv 6492 (class class class)co 7358 ∈ cmpo 7360 Er wer 8632 [cec 8633 / cqs 8634 Fincfn 8883 · cmul 11031 ℕcn 12145 ℕ₀cn0 12401 ♯chash 14253 ℙcprime 16598 Basecbs 17136 +_gcplusg 17177 0_gc0g 17359 Grpcgrp 18863 -_gcsg 18865 SubGrpcsubg 19050 ~_QG cqg 19052 GrpAct cga 19218 pSyl cslw 19456

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 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-inf2 9550 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103 ax-pre-sup 11104

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 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-int 4903 df-iun 4948 df-disj 5066 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-se 5578 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-2o 8398 df-oadd 8401 df-omul 8402 df-er 8635 df-ec 8637 df-qs 8641 df-map 8765 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-sup 9345 df-inf 9346 df-oi 9415 df-dju 9813 df-card 9851 df-acn 9854 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-div 11795 df-nn 12146 df-2 12208 df-3 12209 df-n0 12402 df-xnn0 12475 df-z 12489 df-uz 12752 df-q 12862 df-rp 12906 df-fz 13424 df-fzo 13571 df-fl 13712 df-mod 13790 df-seq 13925 df-exp 13985 df-fac 14197 df-bc 14226 df-hash 14254 df-cj 15022 df-re 15023 df-im 15024 df-sqrt 15158 df-abs 15159 df-clim 15411 df-sum 15610 df-dvds 16180 df-gcd 16422 df-prm 16599 df-pc 16765 df-sets 17091 df-slot 17109 df-ndx 17121 df-base 17137 df-ress 17158 df-plusg 17190 df-0g 17361 df-mgm 18565 df-sgrp 18644 df-mnd 18660 df-submnd 18709 df-grp 18866 df-minusg 18867 df-sbg 18868 df-mulg 18998 df-subg 19053 df-eqg 19055 df-ghm 19142 df-ga 19219 df-od 19457 df-pgp 19459 df-slw 19460

This theorem is referenced by: sylow3lem4 19559

W3C validator