sylow3lem3

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

	Ref	Expression
Hypotheses	sylow3.x	$⊢ X = {Base}_{G}$
	sylow3.g	$⊢ φ \to G \in Grp$
	sylow3.xf	$⊢ φ \to X \in Fin$
	sylow3.p	$⊢ φ \to P \in ℙ$
	sylow3lem1.a	$⊢ \underset{˙}{+} = +_{G}$
	sylow3lem1.d	$⊢ \underset{˙}{-} = -_{G}$
	sylow3lem1.m	$⊢ \underset{˙}{\oplus} = (x \in X, y \in (P pSyl G) ⟼ ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x))$
	sylow3lem2.k	$⊢ φ \to K \in (P pSyl G)$
	sylow3lem2.h	$⊢ H = \{u \in X \| u \underset{˙}{\oplus} K = K\}$
	sylow3lem2.n	$⊢ N = \{x \in X \| \forall y \in X (x \underset{˙}{+} y \in K \leftrightarrow y \underset{˙}{+} x \in K)\}$
Assertion	sylow3lem3	$⊢ φ \to \|P pSyl G\| = \|X / (G ~_{QG} N)\|$

Proof

Step	Hyp	Ref	Expression
1		sylow3.x	$⊢ X = {Base}_{G}$
2		sylow3.g	$⊢ φ \to G \in Grp$
3		sylow3.xf	$⊢ φ \to X \in Fin$
4		sylow3.p	$⊢ φ \to P \in ℙ$
5		sylow3lem1.a	$⊢ \underset{˙}{+} = +_{G}$
6		sylow3lem1.d	$⊢ \underset{˙}{-} = -_{G}$
7		sylow3lem1.m	$⊢ \underset{˙}{\oplus} = (x \in X, y \in (P pSyl G) ⟼ ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x))$
8		sylow3lem2.k	$⊢ φ \to K \in (P pSyl G)$
9		sylow3lem2.h	$⊢ H = \{u \in X \| u \underset{˙}{\oplus} K = K\}$
10		sylow3lem2.n	$⊢ N = \{x \in X \| \forall y \in X (x \underset{˙}{+} y \in K \leftrightarrow y \underset{˙}{+} x \in K)\}$
11		pwfi	$⊢ X \in Fin \leftrightarrow 𝒫 X \in Fin$
12	3 11	sylib	$⊢ φ \to 𝒫 X \in Fin$
13		slwsubg	$⊢ x \in (P pSyl G) \to x \in SubGrp (G)$
14	1	subgss	$⊢ x \in SubGrp (G) \to x \subseteq X$
15	13 14	syl	$⊢ x \in (P pSyl G) \to x \subseteq X$
16	13 15	elpwd	$⊢ x \in (P pSyl G) \to x \in 𝒫 X$
17	16	ssriv	$⊢ P pSyl G \subseteq 𝒫 X$
18		ssfi	$⊢ (𝒫 X \in Fin \land P pSyl G \subseteq 𝒫 X) \to P pSyl G \in Fin$
19	12 17 18	sylancl	$⊢ φ \to P pSyl G \in Fin$
20		hashcl	$⊢ P pSyl G \in Fin \to \|P pSyl G\| \in ℕ_{0}$
21	19 20	syl	$⊢ φ \to \|P pSyl G\| \in ℕ_{0}$
22	21	nn0cnd	$⊢ φ \to \|P pSyl G\| \in ℂ$
23	10 1 5	nmzsubg	$⊢ G \in Grp \to N \in SubGrp (G)$
24		eqid	$⊢ G ~_{QG} N = G ~_{QG} N$
25	1 24	eqger	$⊢ N \in SubGrp (G) \to (G ~_{QG} N) Er X$
26	2 23 25	3syl	$⊢ φ \to (G ~_{QG} N) Er X$
27	26	qsss	$⊢ φ \to X / (G ~_{QG} N) \subseteq 𝒫 X$
28	12 27	ssfid	$⊢ φ \to X / (G ~_{QG} N) \in Fin$
29		hashcl	$⊢ X / (G ~_{QG} N) \in Fin \to \|X / (G ~_{QG} N)\| \in ℕ_{0}$
30	28 29	syl	$⊢ φ \to \|X / (G ~_{QG} N)\| \in ℕ_{0}$
31	30	nn0cnd	$⊢ φ \to \|X / (G ~_{QG} N)\| \in ℂ$
32	2 23	syl	$⊢ φ \to N \in SubGrp (G)$
33		eqid	$⊢ 0_{G} = 0_{G}$
34	33	subg0cl	$⊢ N \in SubGrp (G) \to 0_{G} \in N$
35		ne0i	$⊢ 0_{G} \in N \to N \neq \emptyset$
36	32 34 35	3syl	$⊢ φ \to N \neq \emptyset$
37	1	subgss	$⊢ N \in SubGrp (G) \to N \subseteq X$
38	2 23 37	3syl	$⊢ φ \to N \subseteq X$
39	3 38	ssfid	$⊢ φ \to N \in Fin$
40		hashnncl	$⊢ N \in Fin \to (\|N\| \in ℕ \leftrightarrow N \neq \emptyset)$
41	39 40	syl	$⊢ φ \to (\|N\| \in ℕ \leftrightarrow N \neq \emptyset)$
42	36 41	mpbird	$⊢ φ \to \|N\| \in ℕ$
43	42	nncnd	$⊢ φ \to \|N\| \in ℂ$
44	42	nnne0d	$⊢ φ \to \|N\| \neq 0$
45	1 2 3 4 5 6 7	sylow3lem1	$⊢ φ \to \underset{˙}{\oplus} \in (G GrpAct (P pSyl G))$
46		eqid	$⊢ G ~_{QG} H = G ~_{QG} H$
47		eqid	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq P pSyl G \land \exists g \in X g \underset{˙}{\oplus} x = y)\} = \{⟨x, y⟩ \| (\{x, y\} \subseteq P pSyl G \land \exists g \in X g \underset{˙}{\oplus} x = y)\}$
48	1 9 46 47	orbsta2	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct (P pSyl G)) \land K \in (P pSyl G)) \land X \in Fin) \to \|X\| = \|[K] \{⟨x, y⟩ \| (\{x, y\} \subseteq P pSyl G \land \exists g \in X g \underset{˙}{\oplus} x = y)\}\| \|H\|$
49	45 8 3 48	syl21anc	$⊢ φ \to \|X\| = \|[K] \{⟨x, y⟩ \| (\{x, y\} \subseteq P pSyl G \land \exists g \in X g \underset{˙}{\oplus} x = y)\}\| \|H\|$
50	1 24 32 3	lagsubg2	$⊢ φ \to \|X\| = \|X / (G ~_{QG} N)\| \|N\|$
51	47 1	gaorber	$⊢ \underset{˙}{\oplus} \in (G GrpAct (P pSyl G)) \to \{⟨x, y⟩ \| (\{x, y\} \subseteq P pSyl G \land \exists g \in X g \underset{˙}{\oplus} x = y)\} Er (P pSyl G)$
52	45 51	syl	$⊢ φ \to \{⟨x, y⟩ \| (\{x, y\} \subseteq P pSyl G \land \exists g \in X g \underset{˙}{\oplus} x = y)\} Er (P pSyl G)$
53	52	ecss	$⊢ φ \to [K] \{⟨x, y⟩ \| (\{x, y\} \subseteq P pSyl G \land \exists g \in X g \underset{˙}{\oplus} x = y)\} \subseteq P pSyl G$
54	8	adantr	$⊢ (φ \land h \in (P pSyl G)) \to K \in (P pSyl G)$
55		simpr	$⊢ (φ \land h \in (P pSyl G)) \to h \in (P pSyl G)$
56	3	adantr	$⊢ (φ \land h \in (P pSyl G)) \to X \in Fin$
57	1 56 55 54 5 6	sylow2	$⊢ (φ \land h \in (P pSyl G)) \to \exists u \in X h = ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u)$
58		eqcom	$⊢ u \underset{˙}{\oplus} K = h \leftrightarrow h = u \underset{˙}{\oplus} K$
59		simpr	$⊢ ((φ \land h \in (P pSyl G)) \land u \in X) \to u \in X$
60	54	adantr	$⊢ ((φ \land h \in (P pSyl G)) \land u \in X) \to K \in (P pSyl G)$
61		mptexg	$⊢ K \in (P pSyl G) \to (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u) \in V$
62		rnexg	$⊢ (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u) \in V \to ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u) \in V$
63	60 61 62	3syl	$⊢ ((φ \land h \in (P pSyl G)) \land u \in X) \to ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u) \in V$
64		simpr	$⊢ (x = u \land y = K) \to y = K$
65		simpl	$⊢ (x = u \land y = K) \to x = u$
66	65	oveq1d	$⊢ (x = u \land y = K) \to x \underset{˙}{+} z = u \underset{˙}{+} z$
67	66 65	oveq12d	$⊢ (x = u \land y = K) \to (x \underset{˙}{+} z) \underset{˙}{-} x = (u \underset{˙}{+} z) \underset{˙}{-} u$
68	64 67	mpteq12dv	$⊢ (x = u \land y = K) \to (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) = (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u)$
69	68	rneqd	$⊢ (x = u \land y = K) \to ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) = ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u)$
70	69 7	ovmpoga	$⊢ (u \in X \land K \in (P pSyl G) \land ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u) \in V) \to u \underset{˙}{\oplus} K = ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u)$
71	59 60 63 70	syl3anc	$⊢ ((φ \land h \in (P pSyl G)) \land u \in X) \to u \underset{˙}{\oplus} K = ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u)$
72	71	eqeq2d	$⊢ ((φ \land h \in (P pSyl G)) \land u \in X) \to (h = u \underset{˙}{\oplus} K \leftrightarrow h = ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u))$
73	58 72	bitrid	$⊢ ((φ \land h \in (P pSyl G)) \land u \in X) \to (u \underset{˙}{\oplus} K = h \leftrightarrow h = ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u))$
74	73	rexbidva	$⊢ (φ \land h \in (P pSyl G)) \to (\exists u \in X u \underset{˙}{\oplus} K = h \leftrightarrow \exists u \in X h = ran (z \in K ⟼ (u \underset{˙}{+} z) \underset{˙}{-} u))$
75	57 74	mpbird	$⊢ (φ \land h \in (P pSyl G)) \to \exists u \in X u \underset{˙}{\oplus} K = h$
76	47	gaorb	$⊢ K \{⟨x, y⟩ \| (\{x, y\} \subseteq P pSyl G \land \exists g \in X g \underset{˙}{\oplus} x = y)\} h \leftrightarrow (K \in (P pSyl G) \land h \in (P pSyl G) \land \exists u \in X u \underset{˙}{\oplus} K = h)$
77	54 55 75 76	syl3anbrc	$⊢ (φ \land h \in (P pSyl G)) \to K \{⟨x, y⟩ \| (\{x, y\} \subseteq P pSyl G \land \exists g \in X g \underset{˙}{\oplus} x = y)\} h$
78		elecg	$⊢ (h \in (P pSyl G) \land K \in (P pSyl G)) \to (h \in [K] \{⟨x, y⟩ \| (\{x, y\} \subseteq P pSyl G \land \exists g \in X g \underset{˙}{\oplus} x = y)\} \leftrightarrow K \{⟨x, y⟩ \| (\{x, y\} \subseteq P pSyl G \land \exists g \in X g \underset{˙}{\oplus} x = y)\} h)$
79	55 54 78	syl2anc	$⊢ (φ \land h \in (P pSyl G)) \to (h \in [K] \{⟨x, y⟩ \| (\{x, y\} \subseteq P pSyl G \land \exists g \in X g \underset{˙}{\oplus} x = y)\} \leftrightarrow K \{⟨x, y⟩ \| (\{x, y\} \subseteq P pSyl G \land \exists g \in X g \underset{˙}{\oplus} x = y)\} h)$
80	77 79	mpbird	$⊢ (φ \land h \in (P pSyl G)) \to h \in [K] \{⟨x, y⟩ \| (\{x, y\} \subseteq P pSyl G \land \exists g \in X g \underset{˙}{\oplus} x = y)\}$
81	53 80	eqelssd	$⊢ φ \to [K] \{⟨x, y⟩ \| (\{x, y\} \subseteq P pSyl G \land \exists g \in X g \underset{˙}{\oplus} x = y)\} = P pSyl G$
82	81	fveq2d	$⊢ φ \to \|[K] \{⟨x, y⟩ \| (\{x, y\} \subseteq P pSyl G \land \exists g \in X g \underset{˙}{\oplus} x = y)\}\| = \|P pSyl G\|$
83	1 2 3 4 5 6 7 8 9 10	sylow3lem2	$⊢ φ \to H = N$
84	83	fveq2d	$⊢ φ \to \|H\| = \|N\|$
85	82 84	oveq12d	$⊢ φ \to \|[K] \{⟨x, y⟩ \| (\{x, y\} \subseteq P pSyl G \land \exists g \in X g \underset{˙}{\oplus} x = y)\}\| \|H\| = \|P pSyl G\| \|N\|$
86	49 50 85	3eqtr3rd	$⊢ φ \to \|P pSyl G\| \|N\| = \|X / (G ~_{QG} N)\| \|N\|$
87	22 31 43 44 86	mulcan2ad	$⊢ φ \to \|P pSyl G\| = \|X / (G ~_{QG} N)\|$

Metamath Proof Explorer

Theorem sylow3lem3

Proof