pgpssslw

Description: Every P -subgroup is contained in a Sylow P -subgroup. (Contributed by Mario Carneiro, 16-Jan-2015)

	Ref	Expression
Hypotheses	pgpssslw.1	$⊢ X = {Base}_{G}$
	pgpssslw.2	$⊢ S = G ↾_{𝑠} H$
	pgpssslw.3	$⊢ F = (x \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\} ⟼ \|x\|)$
Assertion	pgpssslw	$⊢ (H \in SubGrp (G) \land X \in Fin \land P pGrp S) \to \exists k \in (P pSyl G) H \subseteq k$

Proof

Step	Hyp	Ref	Expression
1		pgpssslw.1	$⊢ X = {Base}_{G}$
2		pgpssslw.2	$⊢ S = G ↾_{𝑠} H$
3		pgpssslw.3	$⊢ F = (x \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\} ⟼ \|x\|)$
4		simp2	$⊢ (H \in SubGrp (G) \land X \in Fin \land P pGrp S) \to X \in Fin$
5		elrabi	$⊢ x \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\} \to x \in SubGrp (G)$
6	1	subgss	$⊢ x \in SubGrp (G) \to x \subseteq X$
7	5 6	syl	$⊢ x \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\} \to x \subseteq X$
8		ssfi	$⊢ (X \in Fin \land x \subseteq X) \to x \in Fin$
9	4 7 8	syl2an	$⊢ ((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land x \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\}) \to x \in Fin$
10		hashcl	$⊢ x \in Fin \to \|x\| \in ℕ_{0}$
11	9 10	syl	$⊢ ((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land x \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\}) \to \|x\| \in ℕ_{0}$
12	11	nn0zd	$⊢ ((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land x \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\}) \to \|x\| \in ℤ$
13	12 3	fmptd	$⊢ (H \in SubGrp (G) \land X \in Fin \land P pGrp S) \to F : \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\} ⟶ ℤ$
14	13	frnd	$⊢ (H \in SubGrp (G) \land X \in Fin \land P pGrp S) \to ran F \subseteq ℤ$
15		fvex	$⊢ \|x\| \in V$
16	15 3	fnmpti	$⊢ F Fn \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\}$
17		eqimss2	$⊢ y = H \to H \subseteq y$
18	17	biantrud	$⊢ y = H \to (P pGrp (G ↾_{𝑠} y) \leftrightarrow (P pGrp (G ↾_{𝑠} y) \land H \subseteq y))$
19		oveq2	$⊢ y = H \to G ↾_{𝑠} y = G ↾_{𝑠} H$
20	19 2	syl6eqr	$⊢ y = H \to G ↾_{𝑠} y = S$
21	20	breq2d	$⊢ y = H \to (P pGrp (G ↾_{𝑠} y) \leftrightarrow P pGrp S)$
22	18 21	bitr3d	$⊢ y = H \to ((P pGrp (G ↾_{𝑠} y) \land H \subseteq y) \leftrightarrow P pGrp S)$
23		simp1	$⊢ (H \in SubGrp (G) \land X \in Fin \land P pGrp S) \to H \in SubGrp (G)$
24		simp3	$⊢ (H \in SubGrp (G) \land X \in Fin \land P pGrp S) \to P pGrp S$
25	22 23 24	elrabd	$⊢ (H \in SubGrp (G) \land X \in Fin \land P pGrp S) \to H \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\}$
26		fnfvelrn	$⊢ (F Fn \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\} \land H \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\}) \to F (H) \in ran F$
27	16 25 26	sylancr	$⊢ (H \in SubGrp (G) \land X \in Fin \land P pGrp S) \to F (H) \in ran F$
28	27	ne0d	$⊢ (H \in SubGrp (G) \land X \in Fin \land P pGrp S) \to ran F \neq \emptyset$
29		hashcl	$⊢ X \in Fin \to \|X\| \in ℕ_{0}$
30	4 29	syl	$⊢ (H \in SubGrp (G) \land X \in Fin \land P pGrp S) \to \|X\| \in ℕ_{0}$
31	30	nn0red	$⊢ (H \in SubGrp (G) \land X \in Fin \land P pGrp S) \to \|X\| \in ℝ$
32		fveq2	$⊢ x = m \to \|x\| = \|m\|$
33		fvex	$⊢ \|m\| \in V$
34	32 3 33	fvmpt	$⊢ m \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\} \to F (m) = \|m\|$
35	34	adantl	$⊢ ((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land m \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\}) \to F (m) = \|m\|$
36		oveq2	$⊢ y = m \to G ↾_{𝑠} y = G ↾_{𝑠} m$
37	36	breq2d	$⊢ y = m \to (P pGrp (G ↾_{𝑠} y) \leftrightarrow P pGrp (G ↾_{𝑠} m))$
38		sseq2	$⊢ y = m \to (H \subseteq y \leftrightarrow H \subseteq m)$
39	37 38	anbi12d	$⊢ y = m \to ((P pGrp (G ↾_{𝑠} y) \land H \subseteq y) \leftrightarrow (P pGrp (G ↾_{𝑠} m) \land H \subseteq m))$
40	39	elrab	$⊢ m \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\} \leftrightarrow (m \in SubGrp (G) \land (P pGrp (G ↾_{𝑠} m) \land H \subseteq m))$
41	4	adantr	$⊢ ((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (m \in SubGrp (G) \land (P pGrp (G ↾_{𝑠} m) \land H \subseteq m))) \to X \in Fin$
42	1	subgss	$⊢ m \in SubGrp (G) \to m \subseteq X$
43	42	ad2antrl	$⊢ ((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (m \in SubGrp (G) \land (P pGrp (G ↾_{𝑠} m) \land H \subseteq m))) \to m \subseteq X$
44		ssdomg	$⊢ X \in Fin \to (m \subseteq X \to m ≼ X)$
45	41 43 44	sylc	$⊢ ((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (m \in SubGrp (G) \land (P pGrp (G ↾_{𝑠} m) \land H \subseteq m))) \to m ≼ X$
46	41 43	ssfid	$⊢ ((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (m \in SubGrp (G) \land (P pGrp (G ↾_{𝑠} m) \land H \subseteq m))) \to m \in Fin$
47		hashdom	$⊢ (m \in Fin \land X \in Fin) \to (\|m\| \leq \|X\| \leftrightarrow m ≼ X)$
48	46 41 47	syl2anc	$⊢ ((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (m \in SubGrp (G) \land (P pGrp (G ↾_{𝑠} m) \land H \subseteq m))) \to (\|m\| \leq \|X\| \leftrightarrow m ≼ X)$
49	45 48	mpbird	$⊢ ((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (m \in SubGrp (G) \land (P pGrp (G ↾_{𝑠} m) \land H \subseteq m))) \to \|m\| \leq \|X\|$
50	40 49	sylan2b	$⊢ ((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land m \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\}) \to \|m\| \leq \|X\|$
51	35 50	eqbrtrd	$⊢ ((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land m \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\}) \to F (m) \leq \|X\|$
52	51	ralrimiva	$⊢ (H \in SubGrp (G) \land X \in Fin \land P pGrp S) \to \forall m \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\} F (m) \leq \|X\|$
53		breq1	$⊢ w = F (m) \to (w \leq \|X\| \leftrightarrow F (m) \leq \|X\|)$
54	53	ralrn	$⊢ F Fn \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\} \to (\forall w \in ran F w \leq \|X\| \leftrightarrow \forall m \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\} F (m) \leq \|X\|)$
55	16 54	ax-mp	$⊢ \forall w \in ran F w \leq \|X\| \leftrightarrow \forall m \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\} F (m) \leq \|X\|$
56	52 55	sylibr	$⊢ (H \in SubGrp (G) \land X \in Fin \land P pGrp S) \to \forall w \in ran F w \leq \|X\|$
57		brralrspcev	$⊢ (\|X\| \in ℝ \land \forall w \in ran F w \leq \|X\|) \to \exists z \in ℝ \forall w \in ran F w \leq z$
58	31 56 57	syl2anc	$⊢ (H \in SubGrp (G) \land X \in Fin \land P pGrp S) \to \exists z \in ℝ \forall w \in ran F w \leq z$
59		suprzcl	$⊢ (ran F \subseteq ℤ \land ran F \neq \emptyset \land \exists z \in ℝ \forall w \in ran F w \leq z) \to sup (ran F ℝ <) \in ran F$
60	14 28 58 59	syl3anc	$⊢ (H \in SubGrp (G) \land X \in Fin \land P pGrp S) \to sup (ran F ℝ <) \in ran F$
61		fvelrnb	$⊢ F Fn \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\} \to (sup (ran F ℝ <) \in ran F \leftrightarrow \exists k \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\} F (k) = sup (ran F ℝ <))$
62	16 61	ax-mp	$⊢ sup (ran F ℝ <) \in ran F \leftrightarrow \exists k \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\} F (k) = sup (ran F ℝ <)$
63	60 62	sylib	$⊢ (H \in SubGrp (G) \land X \in Fin \land P pGrp S) \to \exists k \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\} F (k) = sup (ran F ℝ <)$
64		oveq2	$⊢ y = k \to G ↾_{𝑠} y = G ↾_{𝑠} k$
65	64	breq2d	$⊢ y = k \to (P pGrp (G ↾_{𝑠} y) \leftrightarrow P pGrp (G ↾_{𝑠} k))$
66		sseq2	$⊢ y = k \to (H \subseteq y \leftrightarrow H \subseteq k)$
67	65 66	anbi12d	$⊢ y = k \to ((P pGrp (G ↾_{𝑠} y) \land H \subseteq y) \leftrightarrow (P pGrp (G ↾_{𝑠} k) \land H \subseteq k))$
68	67	rexrab	$⊢ \exists k \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\} F (k) = sup (ran F ℝ <) \leftrightarrow \exists k \in SubGrp (G) ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <))$
69	63 68	sylib	$⊢ (H \in SubGrp (G) \land X \in Fin \land P pGrp S) \to \exists k \in SubGrp (G) ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <))$
70		simpl3	$⊢ ((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \to P pGrp S$
71		pgpprm	$⊢ P pGrp S \to P \in ℙ$
72	70 71	syl	$⊢ ((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \to P \in ℙ$
73		simprl	$⊢ ((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \to k \in SubGrp (G)$
74		zssre	$⊢ ℤ \subseteq ℝ$
75	14 74	sstrdi	$⊢ (H \in SubGrp (G) \land X \in Fin \land P pGrp S) \to ran F \subseteq ℝ$
76	75	ad2antrr	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to ran F \subseteq ℝ$
77	28	ad2antrr	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to ran F \neq \emptyset$
78	58	ad2antrr	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to \exists z \in ℝ \forall w \in ran F w \leq z$
79		simprl	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to m \in SubGrp (G)$
80		simprrr	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to P pGrp (G ↾_{𝑠} m)$
81		simprrl	$⊢ ((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \to (P pGrp (G ↾_{𝑠} k) \land H \subseteq k)$
82	81	adantr	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to (P pGrp (G ↾_{𝑠} k) \land H \subseteq k)$
83	82	simprd	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to H \subseteq k$
84		simprrl	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to k \subseteq m$
85	83 84	sstrd	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to H \subseteq m$
86	80 85	jca	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to (P pGrp (G ↾_{𝑠} m) \land H \subseteq m)$
87	39 79 86	elrabd	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to m \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\}$
88	87 34	syl	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to F (m) = \|m\|$
89		fnfvelrn	$⊢ (F Fn \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\} \land m \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\}) \to F (m) \in ran F$
90	16 87 89	sylancr	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to F (m) \in ran F$
91	88 90	eqeltrrd	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to \|m\| \in ran F$
92	76 77 78 91	suprubd	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to \|m\| \leq sup (ran F ℝ <)$
93		simprrr	$⊢ ((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \to F (k) = sup (ran F ℝ <)$
94	93	adantr	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to F (k) = sup (ran F ℝ <)$
95	73	adantr	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to k \in SubGrp (G)$
96	67 95 82	elrabd	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to k \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\}$
97		fveq2	$⊢ x = k \to \|x\| = \|k\|$
98		fvex	$⊢ \|k\| \in V$
99	97 3 98	fvmpt	$⊢ k \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land H \subseteq y)\} \to F (k) = \|k\|$
100	96 99	syl	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to F (k) = \|k\|$
101	94 100	eqtr3d	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to sup (ran F ℝ <) = \|k\|$
102	92 101	breqtrd	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to \|m\| \leq \|k\|$
103		simpll2	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to X \in Fin$
104	42	ad2antrl	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to m \subseteq X$
105	103 104	ssfid	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to m \in Fin$
106	105 84	ssfid	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to k \in Fin$
107		hashcl	$⊢ m \in Fin \to \|m\| \in ℕ_{0}$
108		hashcl	$⊢ k \in Fin \to \|k\| \in ℕ_{0}$
109		nn0re	$⊢ \|m\| \in ℕ_{0} \to \|m\| \in ℝ$
110		nn0re	$⊢ \|k\| \in ℕ_{0} \to \|k\| \in ℝ$
111		lenlt	$⊢ (\|m\| \in ℝ \land \|k\| \in ℝ) \to (\|m\| \leq \|k\| \leftrightarrow \neg \|k\| < \|m\|)$
112	109 110 111	syl2an	$⊢ (\|m\| \in ℕ_{0} \land \|k\| \in ℕ_{0}) \to (\|m\| \leq \|k\| \leftrightarrow \neg \|k\| < \|m\|)$
113	107 108 112	syl2an	$⊢ (m \in Fin \land k \in Fin) \to (\|m\| \leq \|k\| \leftrightarrow \neg \|k\| < \|m\|)$
114	105 106 113	syl2anc	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to (\|m\| \leq \|k\| \leftrightarrow \neg \|k\| < \|m\|)$
115	102 114	mpbid	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to \neg \|k\| < \|m\|$
116		php3	$⊢ (m \in Fin \land k \subset m) \to k ≺ m$
117	116	ex	$⊢ m \in Fin \to (k \subset m \to k ≺ m)$
118	105 117	syl	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to (k \subset m \to k ≺ m)$
119		hashsdom	$⊢ (k \in Fin \land m \in Fin) \to (\|k\| < \|m\| \leftrightarrow k ≺ m)$
120	106 105 119	syl2anc	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to (\|k\| < \|m\| \leftrightarrow k ≺ m)$
121	118 120	sylibrd	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to (k \subset m \to \|k\| < \|m\|)$
122	115 121	mtod	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to \neg k \subset m$
123		sspss	$⊢ k \subseteq m \leftrightarrow (k \subset m \lor k = m)$
124	84 123	sylib	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to (k \subset m \lor k = m)$
125	124	ord	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to (\neg k \subset m \to k = m)$
126	122 125	mpd	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land (m \in SubGrp (G) \land (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))) \to k = m$
127	126	expr	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land m \in SubGrp (G)) \to ((k \subseteq m \land P pGrp (G ↾_{𝑠} m)) \to k = m)$
128	81	simpld	$⊢ ((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \to P pGrp (G ↾_{𝑠} k)$
129	128	adantr	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land m \in SubGrp (G)) \to P pGrp (G ↾_{𝑠} k)$
130		oveq2	$⊢ k = m \to G ↾_{𝑠} k = G ↾_{𝑠} m$
131	130	breq2d	$⊢ k = m \to (P pGrp (G ↾_{𝑠} k) \leftrightarrow P pGrp (G ↾_{𝑠} m))$
132		eqimss	$⊢ k = m \to k \subseteq m$
133	132	biantrurd	$⊢ k = m \to (P pGrp (G ↾_{𝑠} m) \leftrightarrow (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))$
134	131 133	bitrd	$⊢ k = m \to (P pGrp (G ↾_{𝑠} k) \leftrightarrow (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))$
135	129 134	syl5ibcom	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land m \in SubGrp (G)) \to (k = m \to (k \subseteq m \land P pGrp (G ↾_{𝑠} m)))$
136	127 135	impbid	$⊢ (((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \land m \in SubGrp (G)) \to ((k \subseteq m \land P pGrp (G ↾_{𝑠} m)) \leftrightarrow k = m)$
137	136	ralrimiva	$⊢ ((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \to \forall m \in SubGrp (G) ((k \subseteq m \land P pGrp (G ↾_{𝑠} m)) \leftrightarrow k = m)$
138		isslw	$⊢ k \in (P pSyl G) \leftrightarrow (P \in ℙ \land k \in SubGrp (G) \land \forall m \in SubGrp (G) ((k \subseteq m \land P pGrp (G ↾_{𝑠} m)) \leftrightarrow k = m))$
139	72 73 137 138	syl3anbrc	$⊢ ((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \to k \in (P pSyl G)$
140	81	simprd	$⊢ ((H \in SubGrp (G) \land X \in Fin \land P pGrp S) \land (k \in SubGrp (G) \land ((P pGrp (G ↾_{𝑠} k) \land H \subseteq k) \land F (k) = sup (ran F ℝ <)))) \to H \subseteq k$
141	69 139 140	reximssdv	$⊢ (H \in SubGrp (G) \land X \in Fin \land P pGrp S) \to \exists k \in (P pSyl G) H \subseteq k$

Metamath Proof Explorer

Theorem pgpssslw

Proof