slwhash

Description: A sylow subgroup has cardinality equal to the maximum power of P dividing the group. (Contributed by Mario Carneiro, 18-Jan-2015)

	Ref	Expression
Hypotheses	fislw.1	$⊢ X = {Base}_{G}$
	slwhash.3	$⊢ φ \to X \in Fin$
	slwhash.4	$⊢ φ \to H \in (P pSyl G)$
Assertion	slwhash	$⊢ φ \to \|H\| = P^{P pCnt \|X\|}$

Proof

Step	Hyp	Ref	Expression
1		fislw.1	$⊢ X = {Base}_{G}$
2		slwhash.3	$⊢ φ \to X \in Fin$
3		slwhash.4	$⊢ φ \to H \in (P pSyl G)$
4		slwsubg	$⊢ H \in (P pSyl G) \to H \in SubGrp (G)$
5	3 4	syl	$⊢ φ \to H \in SubGrp (G)$
6		subgrcl	$⊢ H \in SubGrp (G) \to G \in Grp$
7	5 6	syl	$⊢ φ \to G \in Grp$
8		slwprm	$⊢ H \in (P pSyl G) \to P \in ℙ$
9	3 8	syl	$⊢ φ \to P \in ℙ$
10	1	grpbn0	$⊢ G \in Grp \to X \neq \emptyset$
11	7 10	syl	$⊢ φ \to X \neq \emptyset$
12		hashnncl	$⊢ X \in Fin \to (\|X\| \in ℕ \leftrightarrow X \neq \emptyset)$
13	2 12	syl	$⊢ φ \to (\|X\| \in ℕ \leftrightarrow X \neq \emptyset)$
14	11 13	mpbird	$⊢ φ \to \|X\| \in ℕ$
15	9 14	pccld	$⊢ φ \to P pCnt \|X\| \in ℕ_{0}$
16		pcdvds	$⊢ (P \in ℙ \land \|X\| \in ℕ) \to P^{P pCnt \|X\|} ∥ \|X\|$
17	9 14 16	syl2anc	$⊢ φ \to P^{P pCnt \|X\|} ∥ \|X\|$
18	1 7 2 9 15 17	sylow1	$⊢ φ \to \exists k \in SubGrp (G) \|k\| = P^{P pCnt \|X\|}$
19	2	adantr	$⊢ (φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \to X \in Fin$
20	5	adantr	$⊢ (φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \to H \in SubGrp (G)$
21		simprl	$⊢ (φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \to k \in SubGrp (G)$
22		eqid	$⊢ +_{G} = +_{G}$
23		eqid	$⊢ G ↾_{𝑠} H = G ↾_{𝑠} H$
24	23	slwpgp	$⊢ H \in (P pSyl G) \to P pGrp (G ↾_{𝑠} H)$
25	3 24	syl	$⊢ φ \to P pGrp (G ↾_{𝑠} H)$
26	25	adantr	$⊢ (φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \to P pGrp (G ↾_{𝑠} H)$
27		simprr	$⊢ (φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \to \|k\| = P^{P pCnt \|X\|}$
28		eqid	$⊢ -_{G} = -_{G}$
29	1 19 20 21 22 26 27 28	sylow2b	$⊢ (φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \to \exists g \in X H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g)$
30		simprr	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g)$
31	3	ad2antrr	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to H \in (P pSyl G)$
32	31 8	syl	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to P \in ℙ$
33	15	ad2antrr	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to P pCnt \|X\| \in ℕ_{0}$
34	21	adantr	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to k \in SubGrp (G)$
35		simprl	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to g \in X$
36		eqid	$⊢ (x \in k ⟼ (g +_{G} x) -_{G} g) = (x \in k ⟼ (g +_{G} x) -_{G} g)$
37	1 22 28 36	conjsubg	$⊢ (k \in SubGrp (G) \land g \in X) \to ran (x \in k ⟼ (g +_{G} x) -_{G} g) \in SubGrp (G)$
38	34 35 37	syl2anc	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to ran (x \in k ⟼ (g +_{G} x) -_{G} g) \in SubGrp (G)$
39		eqid	$⊢ G ↾_{𝑠} ran (x \in k ⟼ (g +_{G} x) -_{G} g) = G ↾_{𝑠} ran (x \in k ⟼ (g +_{G} x) -_{G} g)$
40	39	subgbas	$⊢ ran (x \in k ⟼ (g +_{G} x) -_{G} g) \in SubGrp (G) \to ran (x \in k ⟼ (g +_{G} x) -_{G} g) = {Base}_{(G ↾_{𝑠} ran (x \in k ⟼ (g +_{G} x) -_{G} g))}$
41	38 40	syl	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to ran (x \in k ⟼ (g +_{G} x) -_{G} g) = {Base}_{(G ↾_{𝑠} ran (x \in k ⟼ (g +_{G} x) -_{G} g))}$
42	41	fveq2d	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to \|ran (x \in k ⟼ (g +_{G} x) -_{G} g)\| = \|{Base}_{(G ↾_{𝑠} ran (x \in k ⟼ (g +_{G} x) -_{G} g))}\|$
43	1 22 28 36	conjsubgen	$⊢ (k \in SubGrp (G) \land g \in X) \to k \approx ran (x \in k ⟼ (g +_{G} x) -_{G} g)$
44	34 35 43	syl2anc	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to k \approx ran (x \in k ⟼ (g +_{G} x) -_{G} g)$
45	2	ad2antrr	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to X \in Fin$
46	1	subgss	$⊢ k \in SubGrp (G) \to k \subseteq X$
47	34 46	syl	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to k \subseteq X$
48	45 47	ssfid	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to k \in Fin$
49	1	subgss	$⊢ ran (x \in k ⟼ (g +_{G} x) -_{G} g) \in SubGrp (G) \to ran (x \in k ⟼ (g +_{G} x) -_{G} g) \subseteq X$
50	38 49	syl	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to ran (x \in k ⟼ (g +_{G} x) -_{G} g) \subseteq X$
51	45 50	ssfid	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to ran (x \in k ⟼ (g +_{G} x) -_{G} g) \in Fin$
52		hashen	$⊢ (k \in Fin \land ran (x \in k ⟼ (g +_{G} x) -_{G} g) \in Fin) \to (\|k\| = \|ran (x \in k ⟼ (g +_{G} x) -_{G} g)\| \leftrightarrow k \approx ran (x \in k ⟼ (g +_{G} x) -_{G} g))$
53	48 51 52	syl2anc	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to (\|k\| = \|ran (x \in k ⟼ (g +_{G} x) -_{G} g)\| \leftrightarrow k \approx ran (x \in k ⟼ (g +_{G} x) -_{G} g))$
54	44 53	mpbird	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to \|k\| = \|ran (x \in k ⟼ (g +_{G} x) -_{G} g)\|$
55		simplrr	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to \|k\| = P^{P pCnt \|X\|}$
56	54 55	eqtr3d	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to \|ran (x \in k ⟼ (g +_{G} x) -_{G} g)\| = P^{P pCnt \|X\|}$
57	42 56	eqtr3d	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to \|{Base}_{(G ↾_{𝑠} ran (x \in k ⟼ (g +_{G} x) -_{G} g))}\| = P^{P pCnt \|X\|}$
58		oveq2	$⊢ n = P pCnt \|X\| \to P^{n} = P^{P pCnt \|X\|}$
59	58	rspceeqv	$⊢ (P pCnt \|X\| \in ℕ_{0} \land \|{Base}_{(G ↾_{𝑠} ran (x \in k ⟼ (g +_{G} x) -_{G} g))}\| = P^{P pCnt \|X\|}) \to \exists n \in ℕ_{0} \|{Base}_{(G ↾_{𝑠} ran (x \in k ⟼ (g +_{G} x) -_{G} g))}\| = P^{n}$
60	33 57 59	syl2anc	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to \exists n \in ℕ_{0} \|{Base}_{(G ↾_{𝑠} ran (x \in k ⟼ (g +_{G} x) -_{G} g))}\| = P^{n}$
61	39	subggrp	$⊢ ran (x \in k ⟼ (g +_{G} x) -_{G} g) \in SubGrp (G) \to G ↾_{𝑠} ran (x \in k ⟼ (g +_{G} x) -_{G} g) \in Grp$
62	38 61	syl	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to G ↾_{𝑠} ran (x \in k ⟼ (g +_{G} x) -_{G} g) \in Grp$
63	41 51	eqeltrrd	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to {Base}_{(G ↾_{𝑠} ran (x \in k ⟼ (g +_{G} x) -_{G} g))} \in Fin$
64		eqid	$⊢ {Base}_{(G ↾_{𝑠} ran (x \in k ⟼ (g +_{G} x) -_{G} g))} = {Base}_{(G ↾_{𝑠} ran (x \in k ⟼ (g +_{G} x) -_{G} g))}$
65	64	pgpfi	$⊢ (G ↾_{𝑠} ran (x \in k ⟼ (g +_{G} x) -_{G} g) \in Grp \land {Base}_{(G ↾_{𝑠} ran (x \in k ⟼ (g +_{G} x) -_{G} g))} \in Fin) \to (P pGrp (G ↾_{𝑠} ran (x \in k ⟼ (g +_{G} x) -_{G} g)) \leftrightarrow (P \in ℙ \land \exists n \in ℕ_{0} \|{Base}_{(G ↾_{𝑠} ran (x \in k ⟼ (g +_{G} x) -_{G} g))}\| = P^{n}))$
66	62 63 65	syl2anc	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to (P pGrp (G ↾_{𝑠} ran (x \in k ⟼ (g +_{G} x) -_{G} g)) \leftrightarrow (P \in ℙ \land \exists n \in ℕ_{0} \|{Base}_{(G ↾_{𝑠} ran (x \in k ⟼ (g +_{G} x) -_{G} g))}\| = P^{n}))$
67	32 60 66	mpbir2and	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to P pGrp (G ↾_{𝑠} ran (x \in k ⟼ (g +_{G} x) -_{G} g))$
68	39	slwispgp	$⊢ (H \in (P pSyl G) \land ran (x \in k ⟼ (g +_{G} x) -_{G} g) \in SubGrp (G)) \to ((H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g) \land P pGrp (G ↾_{𝑠} ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \leftrightarrow H = ran (x \in k ⟼ (g +_{G} x) -_{G} g))$
69	31 38 68	syl2anc	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to ((H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g) \land P pGrp (G ↾_{𝑠} ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \leftrightarrow H = ran (x \in k ⟼ (g +_{G} x) -_{G} g))$
70	30 67 69	mpbi2and	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to H = ran (x \in k ⟼ (g +_{G} x) -_{G} g)$
71	70	fveq2d	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to \|H\| = \|ran (x \in k ⟼ (g +_{G} x) -_{G} g)\|$
72	71 56	eqtrd	$⊢ ((φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \land (g \in X \land H \subseteq ran (x \in k ⟼ (g +_{G} x) -_{G} g))) \to \|H\| = P^{P pCnt \|X\|}$
73	29 72	rexlimddv	$⊢ (φ \land (k \in SubGrp (G) \land \|k\| = P^{P pCnt \|X\|})) \to \|H\| = P^{P pCnt \|X\|}$
74	18 73	rexlimddv	$⊢ φ \to \|H\| = P^{P pCnt \|X\|}$

Metamath Proof Explorer

Theorem slwhash

Proof