sylow1lem4

Description: Lemma for sylow1 . The stabilizer subgroup of any element of S is at most P ^ N in size. (Contributed by Mario Carneiro, 15-Jan-2015)

	Ref	Expression
Hypotheses	sylow1.x	$⊢ X = {Base}_{G}$
	sylow1.g	$⊢ φ \to G \in Grp$
	sylow1.f	$⊢ φ \to X \in Fin$
	sylow1.p	$⊢ φ \to P \in ℙ$
	sylow1.n	$⊢ φ \to N \in ℕ_{0}$
	sylow1.d	$⊢ φ \to P^{N} ∥ \|X\|$
	sylow1lem.a	$⊢ \underset{˙}{+} = +_{G}$
	sylow1lem.s	$⊢ S = \{s \in 𝒫 X \| \|s\| = P^{N}\}$
	sylow1lem.m	$⊢ \underset{˙}{\oplus} = (x \in X, y \in S ⟼ ran (z \in y ⟼ x \underset{˙}{+} z))$
	sylow1lem3.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| (\{x, y\} \subseteq S \land \exists g \in X g \underset{˙}{\oplus} x = y)\}$
	sylow1lem4.b	$⊢ φ \to B \in S$
	sylow1lem4.h	$⊢ H = \{u \in X \| u \underset{˙}{\oplus} B = B\}$
Assertion	sylow1lem4	$⊢ φ \to \|H\| \leq P^{N}$

Proof

Step	Hyp	Ref	Expression
1		sylow1.x	$⊢ X = {Base}_{G}$
2		sylow1.g	$⊢ φ \to G \in Grp$
3		sylow1.f	$⊢ φ \to X \in Fin$
4		sylow1.p	$⊢ φ \to P \in ℙ$
5		sylow1.n	$⊢ φ \to N \in ℕ_{0}$
6		sylow1.d	$⊢ φ \to P^{N} ∥ \|X\|$
7		sylow1lem.a	$⊢ \underset{˙}{+} = +_{G}$
8		sylow1lem.s	$⊢ S = \{s \in 𝒫 X \| \|s\| = P^{N}\}$
9		sylow1lem.m	$⊢ \underset{˙}{\oplus} = (x \in X, y \in S ⟼ ran (z \in y ⟼ x \underset{˙}{+} z))$
10		sylow1lem3.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| (\{x, y\} \subseteq S \land \exists g \in X g \underset{˙}{\oplus} x = y)\}$
11		sylow1lem4.b	$⊢ φ \to B \in S$
12		sylow1lem4.h	$⊢ H = \{u \in X \| u \underset{˙}{\oplus} B = B\}$
13		fveqeq2	$⊢ s = B \to (\|s\| = P^{N} \leftrightarrow \|B\| = P^{N})$
14	13 8	elrab2	$⊢ B \in S \leftrightarrow (B \in 𝒫 X \land \|B\| = P^{N})$
15	11 14	sylib	$⊢ φ \to (B \in 𝒫 X \land \|B\| = P^{N})$
16	15	simprd	$⊢ φ \to \|B\| = P^{N}$
17		prmnn	$⊢ P \in ℙ \to P \in ℕ$
18	4 17	syl	$⊢ φ \to P \in ℕ$
19	18 5	nnexpcld	$⊢ φ \to P^{N} \in ℕ$
20	16 19	eqeltrd	$⊢ φ \to \|B\| \in ℕ$
21	20	nnne0d	$⊢ φ \to \|B\| \neq 0$
22		hasheq0	$⊢ B \in S \to (\|B\| = 0 \leftrightarrow B = \emptyset)$
23	22	necon3bid	$⊢ B \in S \to (\|B\| \neq 0 \leftrightarrow B \neq \emptyset)$
24	11 23	syl	$⊢ φ \to (\|B\| \neq 0 \leftrightarrow B \neq \emptyset)$
25	21 24	mpbid	$⊢ φ \to B \neq \emptyset$
26		n0	$⊢ B \neq \emptyset \leftrightarrow \exists a a \in B$
27	25 26	sylib	$⊢ φ \to \exists a a \in B$
28	11	adantr	$⊢ (φ \land a \in B) \to B \in S$
29		simplr	$⊢ ((φ \land a \in B) \land b \in H) \to a \in B$
30		oveq2	$⊢ z = a \to b \underset{˙}{+} z = b \underset{˙}{+} a$
31		eqid	$⊢ (z \in B ⟼ b \underset{˙}{+} z) = (z \in B ⟼ b \underset{˙}{+} z)$
32		ovex	$⊢ b \underset{˙}{+} a \in V$
33	30 31 32	fvmpt	$⊢ a \in B \to (z \in B ⟼ b \underset{˙}{+} z) (a) = b \underset{˙}{+} a$
34	29 33	syl	$⊢ ((φ \land a \in B) \land b \in H) \to (z \in B ⟼ b \underset{˙}{+} z) (a) = b \underset{˙}{+} a$
35		ovex	$⊢ b \underset{˙}{+} z \in V$
36	35 31	fnmpti	$⊢ (z \in B ⟼ b \underset{˙}{+} z) Fn B$
37		fnfvelrn	$⊢ ((z \in B ⟼ b \underset{˙}{+} z) Fn B \land a \in B) \to (z \in B ⟼ b \underset{˙}{+} z) (a) \in ran (z \in B ⟼ b \underset{˙}{+} z)$
38	36 29 37	sylancr	$⊢ ((φ \land a \in B) \land b \in H) \to (z \in B ⟼ b \underset{˙}{+} z) (a) \in ran (z \in B ⟼ b \underset{˙}{+} z)$
39	34 38	eqeltrrd	$⊢ ((φ \land a \in B) \land b \in H) \to b \underset{˙}{+} a \in ran (z \in B ⟼ b \underset{˙}{+} z)$
40	12	ssrab3	$⊢ H \subseteq X$
41		simpr	$⊢ ((φ \land a \in B) \land b \in H) \to b \in H$
42	40 41	sseldi	$⊢ ((φ \land a \in B) \land b \in H) \to b \in X$
43	11	ad2antrr	$⊢ ((φ \land a \in B) \land b \in H) \to B \in S$
44		mptexg	$⊢ B \in S \to (z \in B ⟼ b \underset{˙}{+} z) \in V$
45		rnexg	$⊢ (z \in B ⟼ b \underset{˙}{+} z) \in V \to ran (z \in B ⟼ b \underset{˙}{+} z) \in V$
46	43 44 45	3syl	$⊢ ((φ \land a \in B) \land b \in H) \to ran (z \in B ⟼ b \underset{˙}{+} z) \in V$
47		simpr	$⊢ (x = b \land y = B) \to y = B$
48		simpl	$⊢ (x = b \land y = B) \to x = b$
49	48	oveq1d	$⊢ (x = b \land y = B) \to x \underset{˙}{+} z = b \underset{˙}{+} z$
50	47 49	mpteq12dv	$⊢ (x = b \land y = B) \to (z \in y ⟼ x \underset{˙}{+} z) = (z \in B ⟼ b \underset{˙}{+} z)$
51	50	rneqd	$⊢ (x = b \land y = B) \to ran (z \in y ⟼ x \underset{˙}{+} z) = ran (z \in B ⟼ b \underset{˙}{+} z)$
52	51 9	ovmpoga	$⊢ (b \in X \land B \in S \land ran (z \in B ⟼ b \underset{˙}{+} z) \in V) \to b \underset{˙}{\oplus} B = ran (z \in B ⟼ b \underset{˙}{+} z)$
53	42 43 46 52	syl3anc	$⊢ ((φ \land a \in B) \land b \in H) \to b \underset{˙}{\oplus} B = ran (z \in B ⟼ b \underset{˙}{+} z)$
54	39 53	eleqtrrd	$⊢ ((φ \land a \in B) \land b \in H) \to b \underset{˙}{+} a \in (b \underset{˙}{\oplus} B)$
55		oveq1	$⊢ u = b \to u \underset{˙}{\oplus} B = b \underset{˙}{\oplus} B$
56	55	eqeq1d	$⊢ u = b \to (u \underset{˙}{\oplus} B = B \leftrightarrow b \underset{˙}{\oplus} B = B)$
57	56 12	elrab2	$⊢ b \in H \leftrightarrow (b \in X \land b \underset{˙}{\oplus} B = B)$
58	57	simprbi	$⊢ b \in H \to b \underset{˙}{\oplus} B = B$
59	58	adantl	$⊢ ((φ \land a \in B) \land b \in H) \to b \underset{˙}{\oplus} B = B$
60	54 59	eleqtrd	$⊢ ((φ \land a \in B) \land b \in H) \to b \underset{˙}{+} a \in B$
61	60	ex	$⊢ (φ \land a \in B) \to (b \in H \to b \underset{˙}{+} a \in B)$
62	2	ad2antrr	$⊢ ((φ \land a \in B) \land (b \in H \land c \in H)) \to G \in Grp$
63		simprl	$⊢ ((φ \land a \in B) \land (b \in H \land c \in H)) \to b \in H$
64	40 63	sseldi	$⊢ ((φ \land a \in B) \land (b \in H \land c \in H)) \to b \in X$
65		simprr	$⊢ ((φ \land a \in B) \land (b \in H \land c \in H)) \to c \in H$
66	40 65	sseldi	$⊢ ((φ \land a \in B) \land (b \in H \land c \in H)) \to c \in X$
67	15	simpld	$⊢ φ \to B \in 𝒫 X$
68	67	elpwid	$⊢ φ \to B \subseteq X$
69	68	sselda	$⊢ (φ \land a \in B) \to a \in X$
70	69	adantr	$⊢ ((φ \land a \in B) \land (b \in H \land c \in H)) \to a \in X$
71	1 7	grprcan	$⊢ (G \in Grp \land (b \in X \land c \in X \land a \in X)) \to (b \underset{˙}{+} a = c \underset{˙}{+} a \leftrightarrow b = c)$
72	62 64 66 70 71	syl13anc	$⊢ ((φ \land a \in B) \land (b \in H \land c \in H)) \to (b \underset{˙}{+} a = c \underset{˙}{+} a \leftrightarrow b = c)$
73	72	ex	$⊢ (φ \land a \in B) \to ((b \in H \land c \in H) \to (b \underset{˙}{+} a = c \underset{˙}{+} a \leftrightarrow b = c))$
74	61 73	dom2d	$⊢ (φ \land a \in B) \to (B \in S \to H ≼ B)$
75	28 74	mpd	$⊢ (φ \land a \in B) \to H ≼ B$
76	27 75	exlimddv	$⊢ φ \to H ≼ B$
77		ssfi	$⊢ (X \in Fin \land H \subseteq X) \to H \in Fin$
78	3 40 77	sylancl	$⊢ φ \to H \in Fin$
79	3 68	ssfid	$⊢ φ \to B \in Fin$
80		hashdom	$⊢ (H \in Fin \land B \in Fin) \to (\|H\| \leq \|B\| \leftrightarrow H ≼ B)$
81	78 79 80	syl2anc	$⊢ φ \to (\|H\| \leq \|B\| \leftrightarrow H ≼ B)$
82	76 81	mpbird	$⊢ φ \to \|H\| \leq \|B\|$
83	82 16	breqtrd	$⊢ φ \to \|H\| \leq P^{N}$

Metamath Proof Explorer

Theorem sylow1lem4

Proof