sylow3lem6

Description: Lemma for sylow3 , second part. Using the lemma sylow2a , show that the number of sylow subgroups is equivalent mod P to the number of fixed points under the group action. But K is the unique element of the set of Sylow subgroups that is fixed under the group action, so there is exactly one fixed point and so ( ( #( P pSyl G ) ) mod P ) = 1 . (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 ℙ$
	sylow3lem5.a	$⊢ \underset{˙}{+} = +_{G}$
	sylow3lem5.d	$⊢ \underset{˙}{-} = -_{G}$
	sylow3lem5.k	$⊢ φ \to K \in (P pSyl G)$
	sylow3lem5.m	$⊢ \underset{˙}{\oplus} = (x \in K, y \in (P pSyl G) ⟼ ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x))$
	sylow3lem6.n	$⊢ N = \{x \in X \| \forall y \in X (x \underset{˙}{+} y \in s \leftrightarrow y \underset{˙}{+} x \in s)\}$
Assertion	sylow3lem6	$⊢ φ \to \|P pSyl G\| \mod P = 1$

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		sylow3lem5.a	$⊢ \underset{˙}{+} = +_{G}$
6		sylow3lem5.d	$⊢ \underset{˙}{-} = -_{G}$
7		sylow3lem5.k	$⊢ φ \to K \in (P pSyl G)$
8		sylow3lem5.m	$⊢ \underset{˙}{\oplus} = (x \in K, y \in (P pSyl G) ⟼ ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x))$
9		sylow3lem6.n	$⊢ N = \{x \in X \| \forall y \in X (x \underset{˙}{+} y \in s \leftrightarrow y \underset{˙}{+} x \in s)\}$
10		eqid	$⊢ {Base}_{(G ↾_{𝑠} K)} = {Base}_{(G ↾_{𝑠} K)}$
11	1 2 3 4 5 6 7 8	sylow3lem5	$⊢ φ \to \underset{˙}{\oplus} \in ((G ↾_{𝑠} K) GrpAct (P pSyl G))$
12		eqid	$⊢ G ↾_{𝑠} K = G ↾_{𝑠} K$
13	12	slwpgp	$⊢ K \in (P pSyl G) \to P pGrp (G ↾_{𝑠} K)$
14	7 13	syl	$⊢ φ \to P pGrp (G ↾_{𝑠} K)$
15		slwsubg	$⊢ K \in (P pSyl G) \to K \in SubGrp (G)$
16	7 15	syl	$⊢ φ \to K \in SubGrp (G)$
17	12	subgbas	$⊢ K \in SubGrp (G) \to K = {Base}_{(G ↾_{𝑠} K)}$
18	16 17	syl	$⊢ φ \to K = {Base}_{(G ↾_{𝑠} K)}$
19	1	subgss	$⊢ K \in SubGrp (G) \to K \subseteq X$
20	16 19	syl	$⊢ φ \to K \subseteq X$
21	3 20	ssfid	$⊢ φ \to K \in Fin$
22	18 21	eqeltrrd	$⊢ φ \to {Base}_{(G ↾_{𝑠} K)} \in Fin$
23		pwfi	$⊢ X \in Fin \leftrightarrow 𝒫 X \in Fin$
24	3 23	sylib	$⊢ φ \to 𝒫 X \in Fin$
25		slwsubg	$⊢ x \in (P pSyl G) \to x \in SubGrp (G)$
26	1	subgss	$⊢ x \in SubGrp (G) \to x \subseteq X$
27	25 26	syl	$⊢ x \in (P pSyl G) \to x \subseteq X$
28	25 27	elpwd	$⊢ x \in (P pSyl G) \to x \in 𝒫 X$
29	28	ssriv	$⊢ P pSyl G \subseteq 𝒫 X$
30		ssfi	$⊢ (𝒫 X \in Fin \land P pSyl G \subseteq 𝒫 X) \to P pSyl G \in Fin$
31	24 29 30	sylancl	$⊢ φ \to P pSyl G \in Fin$
32		eqid	$⊢ \{s \in (P pSyl G) \| \forall g \in {Base}_{(G ↾_{𝑠} K)} g \underset{˙}{\oplus} s = s\} = \{s \in (P pSyl G) \| \forall g \in {Base}_{(G ↾_{𝑠} K)} g \underset{˙}{\oplus} s = s\}$
33		eqid	$⊢ \{⟨z, w⟩ \| (\{z, w\} \subseteq P pSyl G \land \exists h \in {Base}_{(G ↾_{𝑠} K)} h \underset{˙}{\oplus} z = w)\} = \{⟨z, w⟩ \| (\{z, w\} \subseteq P pSyl G \land \exists h \in {Base}_{(G ↾_{𝑠} K)} h \underset{˙}{\oplus} z = w)\}$
34	10 11 14 22 31 32 33	sylow2a	$⊢ φ \to P ∥ (\|P pSyl G\| - \|\{s \in (P pSyl G) \| \forall g \in {Base}_{(G ↾_{𝑠} K)} g \underset{˙}{\oplus} s = s\}\|)$
35		eqcom	$⊢ ran (z \in s ⟼ (g \underset{˙}{+} z) \underset{˙}{-} g) = s \leftrightarrow s = ran (z \in s ⟼ (g \underset{˙}{+} z) \underset{˙}{-} g)$
36	20	adantr	$⊢ (φ \land s \in (P pSyl G)) \to K \subseteq X$
37	36	sselda	$⊢ ((φ \land s \in (P pSyl G)) \land g \in K) \to g \in X$
38	37	biantrurd	$⊢ ((φ \land s \in (P pSyl G)) \land g \in K) \to (s = ran (z \in s ⟼ (g \underset{˙}{+} z) \underset{˙}{-} g) \leftrightarrow (g \in X \land s = ran (z \in s ⟼ (g \underset{˙}{+} z) \underset{˙}{-} g)))$
39	35 38	syl5bb	$⊢ ((φ \land s \in (P pSyl G)) \land g \in K) \to (ran (z \in s ⟼ (g \underset{˙}{+} z) \underset{˙}{-} g) = s \leftrightarrow (g \in X \land s = ran (z \in s ⟼ (g \underset{˙}{+} z) \underset{˙}{-} g)))$
40		simpr	$⊢ ((φ \land s \in (P pSyl G)) \land g \in K) \to g \in K$
41		simplr	$⊢ ((φ \land s \in (P pSyl G)) \land g \in K) \to s \in (P pSyl G)$
42		simpr	$⊢ (x = g \land y = s) \to y = s$
43		simpl	$⊢ (x = g \land y = s) \to x = g$
44	43	oveq1d	$⊢ (x = g \land y = s) \to x \underset{˙}{+} z = g \underset{˙}{+} z$
45	44 43	oveq12d	$⊢ (x = g \land y = s) \to (x \underset{˙}{+} z) \underset{˙}{-} x = (g \underset{˙}{+} z) \underset{˙}{-} g$
46	42 45	mpteq12dv	$⊢ (x = g \land y = s) \to (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) = (z \in s ⟼ (g \underset{˙}{+} z) \underset{˙}{-} g)$
47	46	rneqd	$⊢ (x = g \land y = s) \to ran (z \in y ⟼ (x \underset{˙}{+} z) \underset{˙}{-} x) = ran (z \in s ⟼ (g \underset{˙}{+} z) \underset{˙}{-} g)$
48		vex	$⊢ s \in V$
49	48	mptex	$⊢ (z \in s ⟼ (g \underset{˙}{+} z) \underset{˙}{-} g) \in V$
50	49	rnex	$⊢ ran (z \in s ⟼ (g \underset{˙}{+} z) \underset{˙}{-} g) \in V$
51	47 8 50	ovmpoa	$⊢ (g \in K \land s \in (P pSyl G)) \to g \underset{˙}{\oplus} s = ran (z \in s ⟼ (g \underset{˙}{+} z) \underset{˙}{-} g)$
52	40 41 51	syl2anc	$⊢ ((φ \land s \in (P pSyl G)) \land g \in K) \to g \underset{˙}{\oplus} s = ran (z \in s ⟼ (g \underset{˙}{+} z) \underset{˙}{-} g)$
53	52	eqeq1d	$⊢ ((φ \land s \in (P pSyl G)) \land g \in K) \to (g \underset{˙}{\oplus} s = s \leftrightarrow ran (z \in s ⟼ (g \underset{˙}{+} z) \underset{˙}{-} g) = s)$
54		slwsubg	$⊢ s \in (P pSyl G) \to s \in SubGrp (G)$
55	54	ad2antlr	$⊢ ((φ \land s \in (P pSyl G)) \land g \in K) \to s \in SubGrp (G)$
56		eqid	$⊢ (z \in s ⟼ (g \underset{˙}{+} z) \underset{˙}{-} g) = (z \in s ⟼ (g \underset{˙}{+} z) \underset{˙}{-} g)$
57	1 5 6 56 9	conjnmzb	$⊢ s \in SubGrp (G) \to (g \in N \leftrightarrow (g \in X \land s = ran (z \in s ⟼ (g \underset{˙}{+} z) \underset{˙}{-} g)))$
58	55 57	syl	$⊢ ((φ \land s \in (P pSyl G)) \land g \in K) \to (g \in N \leftrightarrow (g \in X \land s = ran (z \in s ⟼ (g \underset{˙}{+} z) \underset{˙}{-} g)))$
59	39 53 58	3bitr4d	$⊢ ((φ \land s \in (P pSyl G)) \land g \in K) \to (g \underset{˙}{\oplus} s = s \leftrightarrow g \in N)$
60	59	ralbidva	$⊢ (φ \land s \in (P pSyl G)) \to (\forall g \in K g \underset{˙}{\oplus} s = s \leftrightarrow \forall g \in K g \in N)$
61		dfss3	$⊢ K \subseteq N \leftrightarrow \forall g \in K g \in N$
62	60 61	bitr4di	$⊢ (φ \land s \in (P pSyl G)) \to (\forall g \in K g \underset{˙}{\oplus} s = s \leftrightarrow K \subseteq N)$
63	18	adantr	$⊢ (φ \land s \in (P pSyl G)) \to K = {Base}_{(G ↾_{𝑠} K)}$
64	63	raleqdv	$⊢ (φ \land s \in (P pSyl G)) \to (\forall g \in K g \underset{˙}{\oplus} s = s \leftrightarrow \forall g \in {Base}_{(G ↾_{𝑠} K)} g \underset{˙}{\oplus} s = s)$
65		eqid	$⊢ {Base}_{(G ↾_{𝑠} N)} = {Base}_{(G ↾_{𝑠} N)}$
66	2	ad2antrr	$⊢ ((φ \land s \in (P pSyl G)) \land K \subseteq N) \to G \in Grp$
67	9 1 5	nmzsubg	$⊢ G \in Grp \to N \in SubGrp (G)$
68	66 67	syl	$⊢ ((φ \land s \in (P pSyl G)) \land K \subseteq N) \to N \in SubGrp (G)$
69		eqid	$⊢ G ↾_{𝑠} N = G ↾_{𝑠} N$
70	69	subgbas	$⊢ N \in SubGrp (G) \to N = {Base}_{(G ↾_{𝑠} N)}$
71	68 70	syl	$⊢ ((φ \land s \in (P pSyl G)) \land K \subseteq N) \to N = {Base}_{(G ↾_{𝑠} N)}$
72	3	ad2antrr	$⊢ ((φ \land s \in (P pSyl G)) \land K \subseteq N) \to X \in Fin$
73	1	subgss	$⊢ N \in SubGrp (G) \to N \subseteq X$
74	68 73	syl	$⊢ ((φ \land s \in (P pSyl G)) \land K \subseteq N) \to N \subseteq X$
75	72 74	ssfid	$⊢ ((φ \land s \in (P pSyl G)) \land K \subseteq N) \to N \in Fin$
76	71 75	eqeltrrd	$⊢ ((φ \land s \in (P pSyl G)) \land K \subseteq N) \to {Base}_{(G ↾_{𝑠} N)} \in Fin$
77	7	ad2antrr	$⊢ ((φ \land s \in (P pSyl G)) \land K \subseteq N) \to K \in (P pSyl G)$
78		simpr	$⊢ ((φ \land s \in (P pSyl G)) \land K \subseteq N) \to K \subseteq N$
79	69	subgslw	$⊢ (N \in SubGrp (G) \land K \in (P pSyl G) \land K \subseteq N) \to K \in (P pSyl (G ↾_{𝑠} N))$
80	68 77 78 79	syl3anc	$⊢ ((φ \land s \in (P pSyl G)) \land K \subseteq N) \to K \in (P pSyl (G ↾_{𝑠} N))$
81		simplr	$⊢ ((φ \land s \in (P pSyl G)) \land K \subseteq N) \to s \in (P pSyl G)$
82	54	ad2antlr	$⊢ ((φ \land s \in (P pSyl G)) \land K \subseteq N) \to s \in SubGrp (G)$
83	9 1 5	ssnmz	$⊢ s \in SubGrp (G) \to s \subseteq N$
84	82 83	syl	$⊢ ((φ \land s \in (P pSyl G)) \land K \subseteq N) \to s \subseteq N$
85	69	subgslw	$⊢ (N \in SubGrp (G) \land s \in (P pSyl G) \land s \subseteq N) \to s \in (P pSyl (G ↾_{𝑠} N))$
86	68 81 84 85	syl3anc	$⊢ ((φ \land s \in (P pSyl G)) \land K \subseteq N) \to s \in (P pSyl (G ↾_{𝑠} N))$
87	1	fvexi	$⊢ X \in V$
88	9 87	rabex2	$⊢ N \in V$
89	69 5	ressplusg	$⊢ N \in V \to \underset{˙}{+} = +_{(G ↾_{𝑠} N)}$
90	88 89	ax-mp	$⊢ \underset{˙}{+} = +_{(G ↾_{𝑠} N)}$
91		eqid	$⊢ -_{(G ↾_{𝑠} N)} = -_{(G ↾_{𝑠} N)}$
92	65 76 80 86 90 91	sylow2	$⊢ ((φ \land s \in (P pSyl G)) \land K \subseteq N) \to \exists g \in {Base}_{(G ↾_{𝑠} N)} K = ran (z \in s ⟼ (g \underset{˙}{+} z) -_{(G ↾_{𝑠} N)} g)$
93	9 1 5 69	nmznsg	$⊢ s \in SubGrp (G) \to s \in NrmSGrp (G ↾_{𝑠} N)$
94	82 93	syl	$⊢ ((φ \land s \in (P pSyl G)) \land K \subseteq N) \to s \in NrmSGrp (G ↾_{𝑠} N)$
95		eqid	$⊢ (z \in s ⟼ (g \underset{˙}{+} z) -_{(G ↾_{𝑠} N)} g) = (z \in s ⟼ (g \underset{˙}{+} z) -_{(G ↾_{𝑠} N)} g)$
96	65 90 91 95	conjnsg	$⊢ (s \in NrmSGrp (G ↾_{𝑠} N) \land g \in {Base}_{(G ↾_{𝑠} N)}) \to s = ran (z \in s ⟼ (g \underset{˙}{+} z) -_{(G ↾_{𝑠} N)} g)$
97	94 96	sylan	$⊢ (((φ \land s \in (P pSyl G)) \land K \subseteq N) \land g \in {Base}_{(G ↾_{𝑠} N)}) \to s = ran (z \in s ⟼ (g \underset{˙}{+} z) -_{(G ↾_{𝑠} N)} g)$
98		eqeq2	$⊢ K = ran (z \in s ⟼ (g \underset{˙}{+} z) -_{(G ↾_{𝑠} N)} g) \to (s = K \leftrightarrow s = ran (z \in s ⟼ (g \underset{˙}{+} z) -_{(G ↾_{𝑠} N)} g))$
99	97 98	syl5ibrcom	$⊢ (((φ \land s \in (P pSyl G)) \land K \subseteq N) \land g \in {Base}_{(G ↾_{𝑠} N)}) \to (K = ran (z \in s ⟼ (g \underset{˙}{+} z) -_{(G ↾_{𝑠} N)} g) \to s = K)$
100	99	rexlimdva	$⊢ ((φ \land s \in (P pSyl G)) \land K \subseteq N) \to (\exists g \in {Base}_{(G ↾_{𝑠} N)} K = ran (z \in s ⟼ (g \underset{˙}{+} z) -_{(G ↾_{𝑠} N)} g) \to s = K)$
101	92 100	mpd	$⊢ ((φ \land s \in (P pSyl G)) \land K \subseteq N) \to s = K$
102		simpr	$⊢ ((φ \land s \in (P pSyl G)) \land s = K) \to s = K$
103	16	ad2antrr	$⊢ ((φ \land s \in (P pSyl G)) \land s = K) \to K \in SubGrp (G)$
104	102 103	eqeltrd	$⊢ ((φ \land s \in (P pSyl G)) \land s = K) \to s \in SubGrp (G)$
105	104 83	syl	$⊢ ((φ \land s \in (P pSyl G)) \land s = K) \to s \subseteq N$
106	102 105	eqsstrrd	$⊢ ((φ \land s \in (P pSyl G)) \land s = K) \to K \subseteq N$
107	101 106	impbida	$⊢ (φ \land s \in (P pSyl G)) \to (K \subseteq N \leftrightarrow s = K)$
108	62 64 107	3bitr3d	$⊢ (φ \land s \in (P pSyl G)) \to (\forall g \in {Base}_{(G ↾_{𝑠} K)} g \underset{˙}{\oplus} s = s \leftrightarrow s = K)$
109	108	rabbidva	$⊢ φ \to \{s \in (P pSyl G) \| \forall g \in {Base}_{(G ↾_{𝑠} K)} g \underset{˙}{\oplus} s = s\} = \{s \in (P pSyl G) \| s = K\}$
110		rabsn	$⊢ K \in (P pSyl G) \to \{s \in (P pSyl G) \| s = K\} = \{K\}$
111	7 110	syl	$⊢ φ \to \{s \in (P pSyl G) \| s = K\} = \{K\}$
112	109 111	eqtrd	$⊢ φ \to \{s \in (P pSyl G) \| \forall g \in {Base}_{(G ↾_{𝑠} K)} g \underset{˙}{\oplus} s = s\} = \{K\}$
113	112	fveq2d	$⊢ φ \to \|\{s \in (P pSyl G) \| \forall g \in {Base}_{(G ↾_{𝑠} K)} g \underset{˙}{\oplus} s = s\}\| = \|\{K\}\|$
114		hashsng	$⊢ K \in (P pSyl G) \to \|\{K\}\| = 1$
115	7 114	syl	$⊢ φ \to \|\{K\}\| = 1$
116	113 115	eqtrd	$⊢ φ \to \|\{s \in (P pSyl G) \| \forall g \in {Base}_{(G ↾_{𝑠} K)} g \underset{˙}{\oplus} s = s\}\| = 1$
117	116	oveq2d	$⊢ φ \to \|P pSyl G\| - \|\{s \in (P pSyl G) \| \forall g \in {Base}_{(G ↾_{𝑠} K)} g \underset{˙}{\oplus} s = s\}\| = \|P pSyl G\| - 1$
118	34 117	breqtrd	$⊢ φ \to P ∥ (\|P pSyl G\| - 1)$
119		prmnn	$⊢ P \in ℙ \to P \in ℕ$
120	4 119	syl	$⊢ φ \to P \in ℕ$
121		hashcl	$⊢ P pSyl G \in Fin \to \|P pSyl G\| \in ℕ_{0}$
122	31 121	syl	$⊢ φ \to \|P pSyl G\| \in ℕ_{0}$
123	122	nn0zd	$⊢ φ \to \|P pSyl G\| \in ℤ$
124		1zzd	$⊢ φ \to 1 \in ℤ$
125		moddvds	$⊢ (P \in ℕ \land \|P pSyl G\| \in ℤ \land 1 \in ℤ) \to (\|P pSyl G\| \mod P = 1 \mod P \leftrightarrow P ∥ (\|P pSyl G\| - 1))$
126	120 123 124 125	syl3anc	$⊢ φ \to (\|P pSyl G\| \mod P = 1 \mod P \leftrightarrow P ∥ (\|P pSyl G\| - 1))$
127	118 126	mpbird	$⊢ φ \to \|P pSyl G\| \mod P = 1 \mod P$
128		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
129		eluz2b2	$⊢ P \in ℤ_{\geq 2} \leftrightarrow (P \in ℕ \land 1 < P)$
130		nnre	$⊢ P \in ℕ \to P \in ℝ$
131		1mod	$⊢ (P \in ℝ \land 1 < P) \to 1 \mod P = 1$
132	130 131	sylan	$⊢ (P \in ℕ \land 1 < P) \to 1 \mod P = 1$
133	129 132	sylbi	$⊢ P \in ℤ_{\geq 2} \to 1 \mod P = 1$
134	4 128 133	3syl	$⊢ φ \to 1 \mod P = 1$
135	127 134	eqtrd	$⊢ φ \to \|P pSyl G\| \mod P = 1$

Metamath Proof Explorer

Theorem sylow3lem6

Proof