fislw

Description: The sylow subgroups of a finite group are exactly the groups which have cardinality equal to the maximum power of P dividing the group. (Contributed by Mario Carneiro, 16-Jan-2015)

		Ref	Expression
	Hypothesis	fislw.1	$⊢ X = {Base}_{G}$
	Assertion	fislw	$⊢ (G \in Grp \land X \in Fin \land P \in ℙ) \to (H \in (P pSyl G) \leftrightarrow (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|}))$

Proof

Step	Hyp	Ref	Expression
1		fislw.1	$⊢ X = {Base}_{G}$
2		simpr	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land H \in (P pSyl G)) \to H \in (P pSyl G)$
3		slwsubg	$⊢ H \in (P pSyl G) \to H \in SubGrp (G)$
4	2 3	syl	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land H \in (P pSyl G)) \to H \in SubGrp (G)$
5		simpl2	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land H \in (P pSyl G)) \to X \in Fin$
6	1 5 2	slwhash	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land H \in (P pSyl G)) \to \|H\| = P^{P pCnt \|X\|}$
7	4 6	jca	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land H \in (P pSyl G)) \to (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})$
8		simpl3	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \to P \in ℙ$
9		simprl	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \to H \in SubGrp (G)$
10		simpl2	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \to X \in Fin$
11	10	adantr	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to X \in Fin$
12		simprl	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to k \in SubGrp (G)$
13	1	subgss	$⊢ k \in SubGrp (G) \to k \subseteq X$
14	12 13	syl	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to k \subseteq X$
15	11 14	ssfid	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to k \in Fin$
16		simprrl	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to H \subseteq k$
17		ssdomg	$⊢ k \in Fin \to (H \subseteq k \to H ≼ k)$
18	15 16 17	sylc	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to H ≼ k$
19		simprrr	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to P pGrp (G ↾_{𝑠} k)$
20		eqid	$⊢ G ↾_{𝑠} k = G ↾_{𝑠} k$
21	20	subggrp	$⊢ k \in SubGrp (G) \to G ↾_{𝑠} k \in Grp$
22	12 21	syl	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to G ↾_{𝑠} k \in Grp$
23	20	subgbas	$⊢ k \in SubGrp (G) \to k = {Base}_{(G ↾_{𝑠} k)}$
24	12 23	syl	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to k = {Base}_{(G ↾_{𝑠} k)}$
25	24 15	eqeltrrd	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to {Base}_{(G ↾_{𝑠} k)} \in Fin$
26		eqid	$⊢ {Base}_{(G ↾_{𝑠} k)} = {Base}_{(G ↾_{𝑠} k)}$
27	26	pgpfi	$⊢ (G ↾_{𝑠} k \in Grp \land {Base}_{(G ↾_{𝑠} k)} \in Fin) \to (P pGrp (G ↾_{𝑠} k) \leftrightarrow (P \in ℙ \land \exists n \in ℕ_{0} \|{Base}_{(G ↾_{𝑠} k)}\| = P^{n}))$
28	22 25 27	syl2anc	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to (P pGrp (G ↾_{𝑠} k) \leftrightarrow (P \in ℙ \land \exists n \in ℕ_{0} \|{Base}_{(G ↾_{𝑠} k)}\| = P^{n}))$
29	19 28	mpbid	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to (P \in ℙ \land \exists n \in ℕ_{0} \|{Base}_{(G ↾_{𝑠} k)}\| = P^{n})$
30	29	simpld	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to P \in ℙ$
31		prmnn	$⊢ P \in ℙ \to P \in ℕ$
32	30 31	syl	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to P \in ℕ$
33	32	nnred	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to P \in ℝ$
34	32	nnge1d	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to 1 \leq P$
35		eqid	$⊢ 0_{G} = 0_{G}$
36	35	subg0cl	$⊢ k \in SubGrp (G) \to 0_{G} \in k$
37	12 36	syl	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to 0_{G} \in k$
38	37	ne0d	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to k \neq \emptyset$
39		hashnncl	$⊢ k \in Fin \to (\|k\| \in ℕ \leftrightarrow k \neq \emptyset)$
40	15 39	syl	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to (\|k\| \in ℕ \leftrightarrow k \neq \emptyset)$
41	38 40	mpbird	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to \|k\| \in ℕ$
42	30 41	pccld	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to P pCnt \|k\| \in ℕ_{0}$
43	42	nn0zd	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to P pCnt \|k\| \in ℤ$
44		simpl1	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \to G \in Grp$
45	1	grpbn0	$⊢ G \in Grp \to X \neq \emptyset$
46	44 45	syl	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \to X \neq \emptyset$
47		hashnncl	$⊢ X \in Fin \to (\|X\| \in ℕ \leftrightarrow X \neq \emptyset)$
48	10 47	syl	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \to (\|X\| \in ℕ \leftrightarrow X \neq \emptyset)$
49	46 48	mpbird	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \to \|X\| \in ℕ$
50	8 49	pccld	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \to P pCnt \|X\| \in ℕ_{0}$
51	50	adantr	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to P pCnt \|X\| \in ℕ_{0}$
52	51	nn0zd	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to P pCnt \|X\| \in ℤ$
53		oveq1	$⊢ p = P \to p pCnt \|k\| = P pCnt \|k\|$
54		oveq1	$⊢ p = P \to p pCnt \|X\| = P pCnt \|X\|$
55	53 54	breq12d	$⊢ p = P \to (p pCnt \|k\| \leq p pCnt \|X\| \leftrightarrow P pCnt \|k\| \leq P pCnt \|X\|)$
56	1	lagsubg	$⊢ (k \in SubGrp (G) \land X \in Fin) \to \|k\| ∥ \|X\|$
57	12 11 56	syl2anc	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to \|k\| ∥ \|X\|$
58	41	nnzd	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to \|k\| \in ℤ$
59	49	adantr	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to \|X\| \in ℕ$
60	59	nnzd	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to \|X\| \in ℤ$
61		pc2dvds	$⊢ (\|k\| \in ℤ \land \|X\| \in ℤ) \to (\|k\| ∥ \|X\| \leftrightarrow \forall p \in ℙ p pCnt \|k\| \leq p pCnt \|X\|)$
62	58 60 61	syl2anc	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to (\|k\| ∥ \|X\| \leftrightarrow \forall p \in ℙ p pCnt \|k\| \leq p pCnt \|X\|)$
63	57 62	mpbid	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to \forall p \in ℙ p pCnt \|k\| \leq p pCnt \|X\|$
64	55 63 30	rspcdva	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to P pCnt \|k\| \leq P pCnt \|X\|$
65		eluz2	$⊢ P pCnt \|X\| \in ℤ_{\geq (P pCnt \|k\|)} \leftrightarrow (P pCnt \|k\| \in ℤ \land P pCnt \|X\| \in ℤ \land P pCnt \|k\| \leq P pCnt \|X\|)$
66	43 52 64 65	syl3anbrc	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to P pCnt \|X\| \in ℤ_{\geq (P pCnt \|k\|)}$
67	33 34 66	leexp2ad	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to P^{P pCnt \|k\|} \leq P^{P pCnt \|X\|}$
68	29	simprd	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to \exists n \in ℕ_{0} \|{Base}_{(G ↾_{𝑠} k)}\| = P^{n}$
69	24	fveqeq2d	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to (\|k\| = P^{n} \leftrightarrow \|{Base}_{(G ↾_{𝑠} k)}\| = P^{n})$
70	69	rexbidv	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to (\exists n \in ℕ_{0} \|k\| = P^{n} \leftrightarrow \exists n \in ℕ_{0} \|{Base}_{(G ↾_{𝑠} k)}\| = P^{n})$
71	68 70	mpbird	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to \exists n \in ℕ_{0} \|k\| = P^{n}$
72		pcprmpw	$⊢ (P \in ℙ \land \|k\| \in ℕ) \to (\exists n \in ℕ_{0} \|k\| = P^{n} \leftrightarrow \|k\| = P^{P pCnt \|k\|})$
73	30 41 72	syl2anc	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to (\exists n \in ℕ_{0} \|k\| = P^{n} \leftrightarrow \|k\| = P^{P pCnt \|k\|})$
74	71 73	mpbid	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to \|k\| = P^{P pCnt \|k\|}$
75		simplrr	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to \|H\| = P^{P pCnt \|X\|}$
76	67 74 75	3brtr4d	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to \|k\| \leq \|H\|$
77	1	subgss	$⊢ H \in SubGrp (G) \to H \subseteq X$
78	77	ad2antrl	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \to H \subseteq X$
79	10 78	ssfid	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \to H \in Fin$
80	79	adantr	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to H \in Fin$
81		hashdom	$⊢ (k \in Fin \land H \in Fin) \to (\|k\| \leq \|H\| \leftrightarrow k ≼ H)$
82	15 80 81	syl2anc	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to (\|k\| \leq \|H\| \leftrightarrow k ≼ H)$
83	76 82	mpbid	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to k ≼ H$
84		sbth	$⊢ (H ≼ k \land k ≼ H) \to H \approx k$
85	18 83 84	syl2anc	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to H \approx k$
86		fisseneq	$⊢ (k \in Fin \land H \subseteq k \land H \approx k) \to H = k$
87	15 16 85 86	syl3anc	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land (k \in SubGrp (G) \land (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))) \to H = k$
88	87	expr	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land k \in SubGrp (G)) \to ((H \subseteq k \land P pGrp (G ↾_{𝑠} k)) \to H = k)$
89		eqid	$⊢ G ↾_{𝑠} H = G ↾_{𝑠} H$
90	89	subgbas	$⊢ H \in SubGrp (G) \to H = {Base}_{(G ↾_{𝑠} H)}$
91	90	ad2antrl	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \to H = {Base}_{(G ↾_{𝑠} H)}$
92	91	fveq2d	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \to \|H\| = \|{Base}_{(G ↾_{𝑠} H)}\|$
93		simprr	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \to \|H\| = P^{P pCnt \|X\|}$
94	92 93	eqtr3d	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \to \|{Base}_{(G ↾_{𝑠} H)}\| = P^{P pCnt \|X\|}$
95		oveq2	$⊢ n = P pCnt \|X\| \to P^{n} = P^{P pCnt \|X\|}$
96	95	rspceeqv	$⊢ (P pCnt \|X\| \in ℕ_{0} \land \|{Base}_{(G ↾_{𝑠} H)}\| = P^{P pCnt \|X\|}) \to \exists n \in ℕ_{0} \|{Base}_{(G ↾_{𝑠} H)}\| = P^{n}$
97	50 94 96	syl2anc	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \to \exists n \in ℕ_{0} \|{Base}_{(G ↾_{𝑠} H)}\| = P^{n}$
98	89	subggrp	$⊢ H \in SubGrp (G) \to G ↾_{𝑠} H \in Grp$
99	98	ad2antrl	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \to G ↾_{𝑠} H \in Grp$
100	91 79	eqeltrrd	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \to {Base}_{(G ↾_{𝑠} H)} \in Fin$
101		eqid	$⊢ {Base}_{(G ↾_{𝑠} H)} = {Base}_{(G ↾_{𝑠} H)}$
102	101	pgpfi	$⊢ (G ↾_{𝑠} H \in Grp \land {Base}_{(G ↾_{𝑠} H)} \in Fin) \to (P pGrp (G ↾_{𝑠} H) \leftrightarrow (P \in ℙ \land \exists n \in ℕ_{0} \|{Base}_{(G ↾_{𝑠} H)}\| = P^{n}))$
103	99 100 102	syl2anc	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \to (P pGrp (G ↾_{𝑠} H) \leftrightarrow (P \in ℙ \land \exists n \in ℕ_{0} \|{Base}_{(G ↾_{𝑠} H)}\| = P^{n}))$
104	8 97 103	mpbir2and	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \to P pGrp (G ↾_{𝑠} H)$
105	104	adantr	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land k \in SubGrp (G)) \to P pGrp (G ↾_{𝑠} H)$
106		oveq2	$⊢ H = k \to G ↾_{𝑠} H = G ↾_{𝑠} k$
107	106	breq2d	$⊢ H = k \to (P pGrp (G ↾_{𝑠} H) \leftrightarrow P pGrp (G ↾_{𝑠} k))$
108		eqimss	$⊢ H = k \to H \subseteq k$
109	108	biantrurd	$⊢ H = k \to (P pGrp (G ↾_{𝑠} k) \leftrightarrow (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))$
110	107 109	bitrd	$⊢ H = k \to (P pGrp (G ↾_{𝑠} H) \leftrightarrow (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))$
111	105 110	syl5ibcom	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land k \in SubGrp (G)) \to (H = k \to (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))$
112	88 111	impbid	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \land k \in SubGrp (G)) \to ((H \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow H = k)$
113	112	ralrimiva	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \to \forall k \in SubGrp (G) ((H \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow H = k)$
114		isslw	$⊢ H \in (P pSyl G) \leftrightarrow (P \in ℙ \land H \in SubGrp (G) \land \forall k \in SubGrp (G) ((H \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow H = k))$
115	8 9 113 114	syl3anbrc	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|})) \to H \in (P pSyl G)$
116	7 115	impbida	$⊢ (G \in Grp \land X \in Fin \land P \in ℙ) \to (H \in (P pSyl G) \leftrightarrow (H \in SubGrp (G) \land \|H\| = P^{P pCnt \|X\|}))$

Metamath Proof Explorer

Theorem fislw

Proof