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 19536

Description: Lemma for sylow3 19540, 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 9198	. . . . . 6 ⊢ (𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin)
3	1, 2	sylib 218	. . . . 5 ⊢ (𝜑 → 𝒫 𝑋 ∈ Fin)
4		slwsubg 19517	. . . . . . 7 ⊢ (𝑥 ∈ (𝑃 pSyl 𝐺) → 𝑥 ∈ (SubGrp‘𝐺))
5		sylow3.x	. . . . . . . . 9 ⊢ 𝑋 = (Base‘𝐺)
6	5	subgss 19035	. . . . . . . 8 ⊢ (𝑥 ∈ (SubGrp‘𝐺) → 𝑥 ⊆ 𝑋)
7	4, 6	syl 17	. . . . . . 7 ⊢ (𝑥 ∈ (𝑃 pSyl 𝐺) → 𝑥 ⊆ 𝑋)
8	4, 7	elpwd 4551	. . . . . 6 ⊢ (𝑥 ∈ (𝑃 pSyl 𝐺) → 𝑥 ∈ 𝒫 𝑋)
9	8	ssriv 3933	. . . . 5 ⊢ (𝑃 pSyl 𝐺) ⊆ 𝒫 𝑋
10		ssfi 9077	. . . . 5 ⊢ ((𝒫 𝑋 ∈ Fin ∧ (𝑃 pSyl 𝐺) ⊆ 𝒫 𝑋) → (𝑃 pSyl 𝐺) ∈ Fin)
11	3, 9, 10	sylancl 586	. . . 4 ⊢ (𝜑 → (𝑃 pSyl 𝐺) ∈ Fin)
12		hashcl 14258	. . . 4 ⊢ ((𝑃 pSyl 𝐺) ∈ Fin → (♯‘(𝑃 pSyl 𝐺)) ∈ ℕ₀)
13	11, 12	syl 17	. . 3 ⊢ (𝜑 → (♯‘(𝑃 pSyl 𝐺)) ∈ ℕ₀)
14	13	nn0cnd 12439	. 2 ⊢ (𝜑 → (♯‘(𝑃 pSyl 𝐺)) ∈ ℂ)
15		sylow3.g	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ Grp)
16		sylow3lem2.n	. . . . . . . 8 ⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝐾 ↔ (𝑦 + 𝑥) ∈ 𝐾)}
17		sylow3lem1.a	. . . . . . . 8 ⊢ + = (+_g‘𝐺)
18	16, 5, 17	nmzsubg 19072	. . . . . . 7 ⊢ (𝐺 ∈ Grp → 𝑁 ∈ (SubGrp‘𝐺))
19		eqid 2731	. . . . . . . 8 ⊢ (𝐺 ~_QG 𝑁) = (𝐺 ~_QG 𝑁)
20	5, 19	eqger 19085	. . . . . . 7 ⊢ (𝑁 ∈ (SubGrp‘𝐺) → (𝐺 ~_QG 𝑁) Er 𝑋)
21	15, 18, 20	3syl 18	. . . . . 6 ⊢ (𝜑 → (𝐺 ~_QG 𝑁) Er 𝑋)
22	21	qsss 8695	. . . . 5 ⊢ (𝜑 → (𝑋 / (𝐺 ~_QG 𝑁)) ⊆ 𝒫 𝑋)
23	3, 22	ssfid 9148	. . . 4 ⊢ (𝜑 → (𝑋 / (𝐺 ~_QG 𝑁)) ∈ Fin)
24		hashcl 14258	. . . 4 ⊢ ((𝑋 / (𝐺 ~_QG 𝑁)) ∈ Fin → (♯‘(𝑋 / (𝐺 ~_QG 𝑁))) ∈ ℕ₀)
25	23, 24	syl 17	. . 3 ⊢ (𝜑 → (♯‘(𝑋 / (𝐺 ~_QG 𝑁))) ∈ ℕ₀)
26	25	nn0cnd 12439	. 2 ⊢ (𝜑 → (♯‘(𝑋 / (𝐺 ~_QG 𝑁))) ∈ ℂ)
27	15, 18	syl 17	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ (SubGrp‘𝐺))
28		eqid 2731	. . . . . 6 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
29	28	subg0cl 19042	. . . . 5 ⊢ (𝑁 ∈ (SubGrp‘𝐺) → (0_g‘𝐺) ∈ 𝑁)
30		ne0i 4286	. . . . 5 ⊢ ((0_g‘𝐺) ∈ 𝑁 → 𝑁 ≠ ∅)
31	27, 29, 30	3syl 18	. . . 4 ⊢ (𝜑 → 𝑁 ≠ ∅)
32	5	subgss 19035	. . . . . . 7 ⊢ (𝑁 ∈ (SubGrp‘𝐺) → 𝑁 ⊆ 𝑋)
33	15, 18, 32	3syl 18	. . . . . 6 ⊢ (𝜑 → 𝑁 ⊆ 𝑋)
34	1, 33	ssfid 9148	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ Fin)
35		hashnncl 14268	. . . . 5 ⊢ (𝑁 ∈ Fin → ((♯‘𝑁) ∈ ℕ ↔ 𝑁 ≠ ∅))
36	34, 35	syl 17	. . . 4 ⊢ (𝜑 → ((♯‘𝑁) ∈ ℕ ↔ 𝑁 ≠ ∅))
37	31, 36	mpbird 257	. . 3 ⊢ (𝜑 → (♯‘𝑁) ∈ ℕ)
38	37	nncnd 12136	. 2 ⊢ (𝜑 → (♯‘𝑁) ∈ ℂ)
39	37	nnne0d 12170	. 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 19534	. . . 4 ⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct (𝑃 pSyl 𝐺)))
44		sylow3lem2.k	. . . 4 ⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺))
45		sylow3lem2.h	. . . . 5 ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾}
46		eqid 2731	. . . . 5 ⊢ (𝐺 ~_QG 𝐻) = (𝐺 ~_QG 𝐻)
47		eqid 2731	. . . . 5 ⊢ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}
48	5, 45, 46, 47	orbsta2 19221	. . . 4 ⊢ ((( ⊕ ∈ (𝐺 GrpAct (𝑃 pSyl 𝐺)) ∧ 𝐾 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑋 ∈ Fin) → (♯‘𝑋) = ((♯‘[𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}) · (♯‘𝐻)))
49	43, 44, 1, 48	syl21anc 837	. . 3 ⊢ (𝜑 → (♯‘𝑋) = ((♯‘[𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}) · (♯‘𝐻)))
50	5, 19, 27, 1	lagsubg2 19101	. . 3 ⊢ (𝜑 → (♯‘𝑋) = ((♯‘(𝑋 / (𝐺 ~_QG 𝑁))) · (♯‘𝑁)))
51	47, 5	gaorber 19215	. . . . . . . 8 ⊢ ( ⊕ ∈ (𝐺 GrpAct (𝑃 pSyl 𝐺)) → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} Er (𝑃 pSyl 𝐺))
52	43, 51	syl 17	. . . . . . 7 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} Er (𝑃 pSyl 𝐺))
53	52	ecss 8668	. . . . . 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 19533	. . . . . . . . 9 ⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → ∃𝑢 ∈ 𝑋 ℎ = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
58		eqcom 2738	. . . . . . . . . . 11 ⊢ ((𝑢 ⊕ 𝐾) = ℎ ↔ ℎ = (𝑢 ⊕ 𝐾))
59		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → 𝑢 ∈ 𝑋)
60	54	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → 𝐾 ∈ (𝑃 pSyl 𝐺))
61		mptexg 7150	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (𝑃 pSyl 𝐺) → (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V)
62		rnexg 7827	. . . . . . . . . . . . . 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 7356	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → (𝑥 + 𝑧) = (𝑢 + 𝑧))
67	66, 65	oveq12d 7359	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → ((𝑥 + 𝑧) − 𝑥) = ((𝑢 + 𝑧) − 𝑢))
68	64, 67	mpteq12dv 5173	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
69	68	rneqd 5873	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
70	69, 42	ovmpoga 7495	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∈ 𝑋 ∧ 𝐾 ∈ (𝑃 pSyl 𝐺) ∧ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
71	59, 60, 63, 70	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))
72	71	eqeq2d 2742	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → (ℎ = (𝑢 ⊕ 𝐾) ↔ ℎ = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))))
73	58, 72	bitrid 283	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → ((𝑢 ⊕ 𝐾) = ℎ ↔ ℎ = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))))
74	73	rexbidva 3154	. . . . . . . . 9 ⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → (∃𝑢 ∈ 𝑋 (𝑢 ⊕ 𝐾) = ℎ ↔ ∃𝑢 ∈ 𝑋 ℎ = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))))
75	57, 74	mpbird 257	. . . . . . . 8 ⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → ∃𝑢 ∈ 𝑋 (𝑢 ⊕ 𝐾) = ℎ)
76	47	gaorb 19214	. . . . . . . 8 ⊢ (𝐾{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}ℎ ↔ (𝐾 ∈ (𝑃 pSyl 𝐺) ∧ ℎ ∈ (𝑃 pSyl 𝐺) ∧ ∃𝑢 ∈ 𝑋 (𝑢 ⊕ 𝐾) = ℎ))
77	54, 55, 75, 76	syl3anbrc 1344	. . . . . . 7 ⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → 𝐾{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}ℎ)
78		elecg 8661	. . . . . . . 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 3951	. . . . 5 ⊢ (𝜑 → [𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} = (𝑃 pSyl 𝐺))
82	81	fveq2d 6821	. . . 4 ⊢ (𝜑 → (♯‘[𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}) = (♯‘(𝑃 pSyl 𝐺)))
83	5, 15, 1, 40, 17, 41, 42, 44, 45, 16	sylow3lem2 19535	. . . . 5 ⊢ (𝜑 → 𝐻 = 𝑁)
84	83	fveq2d 6821	. . . 4 ⊢ (𝜑 → (♯‘𝐻) = (♯‘𝑁))
85	82, 84	oveq12d 7359	. . 3 ⊢ (𝜑 → ((♯‘[𝐾]{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}) · (♯‘𝐻)) = ((♯‘(𝑃 pSyl 𝐺)) · (♯‘𝑁)))
86	49, 50, 85	3eqtr3rd 2775	. 2 ⊢ (𝜑 → ((♯‘(𝑃 pSyl 𝐺)) · (♯‘𝑁)) = ((♯‘(𝑋 / (𝐺 ~_QG 𝑁))) · (♯‘𝑁)))
87	14, 26, 38, 39, 86	mulcan2ad 11748	1 ⊢ (𝜑 → (♯‘(𝑃 pSyl 𝐺)) = (♯‘(𝑋 / (𝐺 ~_QG 𝑁))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∈ wcel 2111 ≠ wne 2928 ∀wral 3047 ∃wrex 3056 {crab 3395 Vcvv 3436 ⊆ wss 3897 ∅c0 4278 𝒫 cpw 4545 {cpr 4573 class class class wbr 5086 {copab 5148 ↦ cmpt 5167 ran crn 5612 ‘cfv 6476 (class class class)co 7341 ∈ cmpo 7343 Er wer 8614 [cec 8615 / cqs 8616 Fincfn 8864 · cmul 11006 ℕcn 12120 ℕ₀cn0 12376 ♯chash 14232 ℙcprime 16577 Basecbs 17115 +_gcplusg 17156 0_gc0g 17338 Grpcgrp 18841 -_gcsg 18843 SubGrpcsubg 19028 ~_QG cqg 19030 GrpAct cga 19196 pSyl cslw 19434

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 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5212 ax-sep 5229 ax-nul 5239 ax-pow 5298 ax-pr 5365 ax-un 7663 ax-inf2 9526 ax-cnex 11057 ax-resscn 11058 ax-1cn 11059 ax-icn 11060 ax-addcl 11061 ax-addrcl 11062 ax-mulcl 11063 ax-mulrcl 11064 ax-mulcom 11065 ax-addass 11066 ax-mulass 11067 ax-distr 11068 ax-i2m1 11069 ax-1ne0 11070 ax-1rid 11071 ax-rnegex 11072 ax-rrecex 11073 ax-cnre 11074 ax-pre-lttri 11075 ax-pre-lttrn 11076 ax-pre-ltadd 11077 ax-pre-mulgt0 11078 ax-pre-sup 11079

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 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4279 df-if 4471 df-pw 4547 df-sn 4572 df-pr 4574 df-op 4578 df-uni 4855 df-int 4893 df-iun 4938 df-disj 5054 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5506 df-eprel 5511 df-po 5519 df-so 5520 df-fr 5564 df-se 5565 df-we 5566 df-xp 5617 df-rel 5618 df-cnv 5619 df-co 5620 df-dm 5621 df-rn 5622 df-res 5623 df-ima 5624 df-pred 6243 df-ord 6304 df-on 6305 df-lim 6306 df-suc 6307 df-iota 6432 df-fun 6478 df-fn 6479 df-f 6480 df-f1 6481 df-fo 6482 df-f1o 6483 df-fv 6484 df-isom 6485 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-om 7792 df-1st 7916 df-2nd 7917 df-frecs 8206 df-wrecs 8237 df-recs 8286 df-rdg 8324 df-1o 8380 df-2o 8381 df-oadd 8384 df-omul 8385 df-er 8617 df-ec 8619 df-qs 8623 df-map 8747 df-en 8865 df-dom 8866 df-sdom 8867 df-fin 8868 df-sup 9321 df-inf 9322 df-oi 9391 df-dju 9789 df-card 9827 df-acn 9830 df-pnf 11143 df-mnf 11144 df-xr 11145 df-ltxr 11146 df-le 11147 df-sub 11341 df-neg 11342 df-div 11770 df-nn 12121 df-2 12183 df-3 12184 df-n0 12377 df-xnn0 12450 df-z 12464 df-uz 12728 df-q 12842 df-rp 12886 df-fz 13403 df-fzo 13550 df-fl 13691 df-mod 13769 df-seq 13904 df-exp 13964 df-fac 14176 df-bc 14205 df-hash 14233 df-cj 15001 df-re 15002 df-im 15003 df-sqrt 15137 df-abs 15138 df-clim 15390 df-sum 15589 df-dvds 16159 df-gcd 16401 df-prm 16578 df-pc 16744 df-sets 17070 df-slot 17088 df-ndx 17100 df-base 17116 df-ress 17137 df-plusg 17169 df-0g 17340 df-mgm 18543 df-sgrp 18622 df-mnd 18638 df-submnd 18687 df-grp 18844 df-minusg 18845 df-sbg 18846 df-mulg 18976 df-subg 19031 df-eqg 19033 df-ghm 19120 df-ga 19197 df-od 19435 df-pgp 19437 df-slw 19438

This theorem is referenced by: sylow3lem4 19537

W3C validator