sylow3

Description: Sylow's third theorem. The number of Sylow subgroups is a divisor of | G | / d , where d is the common order of a Sylow subgroup, and is equivalent to 1 mod P . This is part of Metamath 100 proof #72. (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 ℙ$
	sylow3.n	$⊢ N = \|P pSyl G\|$
Assertion	sylow3	$⊢ φ \to (N ∥ (\frac{\|X\|}{P^{P pCnt \|X\|}}) \land N \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		sylow3.n	$⊢ N = \|P pSyl G\|$
6	1	slwn0	$⊢ (G \in Grp \land X \in Fin \land P \in ℙ) \to P pSyl G \neq \emptyset$
7	2 3 4 6	syl3anc	$⊢ φ \to P pSyl G \neq \emptyset$
8		n0	$⊢ P pSyl G \neq \emptyset \leftrightarrow \exists k k \in (P pSyl G)$
9	7 8	sylib	$⊢ φ \to \exists k k \in (P pSyl G)$
10	2	adantr	$⊢ (φ \land k \in (P pSyl G)) \to G \in Grp$
11	3	adantr	$⊢ (φ \land k \in (P pSyl G)) \to X \in Fin$
12	4	adantr	$⊢ (φ \land k \in (P pSyl G)) \to P \in ℙ$
13		eqid	$⊢ +_{G} = +_{G}$
14		eqid	$⊢ -_{G} = -_{G}$
15		oveq2	$⊢ c = z \to a +_{G} c = a +_{G} z$
16	15	oveq1d	$⊢ c = z \to (a +_{G} c) -_{G} a = (a +_{G} z) -_{G} a$
17	16	cbvmptv	$⊢ (c \in b ⟼ (a +_{G} c) -_{G} a) = (z \in b ⟼ (a +_{G} z) -_{G} a)$
18		oveq1	$⊢ a = x \to a +_{G} z = x +_{G} z$
19		id	$⊢ a = x \to a = x$
20	18 19	oveq12d	$⊢ a = x \to (a +_{G} z) -_{G} a = (x +_{G} z) -_{G} x$
21	20	mpteq2dv	$⊢ a = x \to (z \in b ⟼ (a +_{G} z) -_{G} a) = (z \in b ⟼ (x +_{G} z) -_{G} x)$
22	17 21	syl5eq	$⊢ a = x \to (c \in b ⟼ (a +_{G} c) -_{G} a) = (z \in b ⟼ (x +_{G} z) -_{G} x)$
23	22	rneqd	$⊢ a = x \to ran (c \in b ⟼ (a +_{G} c) -_{G} a) = ran (z \in b ⟼ (x +_{G} z) -_{G} x)$
24		mpteq1	$⊢ b = y \to (z \in b ⟼ (x +_{G} z) -_{G} x) = (z \in y ⟼ (x +_{G} z) -_{G} x)$
25	24	rneqd	$⊢ b = y \to ran (z \in b ⟼ (x +_{G} z) -_{G} x) = ran (z \in y ⟼ (x +_{G} z) -_{G} x)$
26	23 25	cbvmpov	$⊢ (a \in X, b \in (P pSyl G) ⟼ ran (c \in b ⟼ (a +_{G} c) -_{G} a)) = (x \in X, y \in (P pSyl G) ⟼ ran (z \in y ⟼ (x +_{G} z) -_{G} x))$
27		simpr	$⊢ (φ \land k \in (P pSyl G)) \to k \in (P pSyl G)$
28		eqid	$⊢ \{u \in X \| u (a \in X, b \in (P pSyl G) ⟼ ran (c \in b ⟼ (a +_{G} c) -_{G} a)) k = k\} = \{u \in X \| u (a \in X, b \in (P pSyl G) ⟼ ran (c \in b ⟼ (a +_{G} c) -_{G} a)) k = k\}$
29		eqid	$⊢ \{x \in X \| \forall y \in X (x +_{G} y \in k \leftrightarrow y +_{G} x \in k)\} = \{x \in X \| \forall y \in X (x +_{G} y \in k \leftrightarrow y +_{G} x \in k)\}$
30	1 10 11 12 13 14 26 27 28 29	sylow3lem4	$⊢ (φ \land k \in (P pSyl G)) \to \|P pSyl G\| ∥ (\frac{\|X\|}{P^{P pCnt \|X\|}})$
31	5 30	eqbrtrid	$⊢ (φ \land k \in (P pSyl G)) \to N ∥ (\frac{\|X\|}{P^{P pCnt \|X\|}})$
32	5	oveq1i	$⊢ N \mod P = \|P pSyl G\| \mod P$
33	23 25	cbvmpov	$⊢ (a \in k, b \in (P pSyl G) ⟼ ran (c \in b ⟼ (a +_{G} c) -_{G} a)) = (x \in k, y \in (P pSyl G) ⟼ ran (z \in y ⟼ (x +_{G} z) -_{G} x))$
34		eqid	$⊢ \{x \in X \| \forall y \in X (x +_{G} y \in s \leftrightarrow y +_{G} x \in s)\} = \{x \in X \| \forall y \in X (x +_{G} y \in s \leftrightarrow y +_{G} x \in s)\}$
35	1 10 11 12 13 14 27 33 34	sylow3lem6	$⊢ (φ \land k \in (P pSyl G)) \to \|P pSyl G\| \mod P = 1$
36	32 35	syl5eq	$⊢ (φ \land k \in (P pSyl G)) \to N \mod P = 1$
37	31 36	jca	$⊢ (φ \land k \in (P pSyl G)) \to (N ∥ (\frac{\|X\|}{P^{P pCnt \|X\|}}) \land N \mod P = 1)$
38	9 37	exlimddv	$⊢ φ \to (N ∥ (\frac{\|X\|}{P^{P pCnt \|X\|}}) \land N \mod P = 1)$

Metamath Proof Explorer

Theorem sylow3

Proof