Theorem 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	⊢ 𝑋 = ( Base ‘ 𝐺 )
	sylow1.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	sylow1.f	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	sylow1.p	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	sylow1.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	sylow1.d	⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝑋 ) )
	sylow1lem.a	⊢ + = ( +g ‘ 𝐺 )
	sylow1lem.s	⊢ 𝑆 = { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) }
	sylow1lem.m	⊢ ⊕ = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑆 ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) )
	sylow1lem3.1	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑆 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) }
	sylow1lem4.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
	sylow1lem4.h	⊢ 𝐻 = { 𝑢 ∈ 𝑋 ∣ ( 𝑢 ⊕ 𝐵 ) = 𝐵 }
Assertion	sylow1lem4	⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ≤ ( 𝑃 ↑ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		sylow1.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		sylow1.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
3		sylow1.f	⊢ ( 𝜑 → 𝑋 ∈ Fin )
4		sylow1.p	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5		sylow1.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6		sylow1.d	⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝑋 ) )
7		sylow1lem.a	⊢ + = ( +g ‘ 𝐺 )
8		sylow1lem.s	⊢ 𝑆 = { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) }
9		sylow1lem.m	⊢ ⊕ = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑆 ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) )
10		sylow1lem3.1	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑆 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) }
11		sylow1lem4.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
12		sylow1lem4.h	⊢ 𝐻 = { 𝑢 ∈ 𝑋 ∣ ( 𝑢 ⊕ 𝐵 ) = 𝐵 }
13		fveqeq2	⊢ ( 𝑠 = 𝐵 → ( ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) ↔ ( ♯ ‘ 𝐵 ) = ( 𝑃 ↑ 𝑁 ) ) )
14	13 8	elrab2	⊢ ( 𝐵 ∈ 𝑆 ↔ ( 𝐵 ∈ 𝒫 𝑋 ∧ ( ♯ ‘ 𝐵 ) = ( 𝑃 ↑ 𝑁 ) ) )
15	11 14	sylib	⊢ ( 𝜑 → ( 𝐵 ∈ 𝒫 𝑋 ∧ ( ♯ ‘ 𝐵 ) = ( 𝑃 ↑ 𝑁 ) ) )
16	15	simprd	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( 𝑃 ↑ 𝑁 ) )
17		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
18	4 17	syl	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
19	18 5	nnexpcld	⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∈ ℕ )
20	16 19	eqeltrd	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ )
21	20	nnne0d	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ≠ 0 )
22		hasheq0	⊢ ( 𝐵 ∈ 𝑆 → ( ( ♯ ‘ 𝐵 ) = 0 ↔ 𝐵 = ∅ ) )
23	22	necon3bid	⊢ ( 𝐵 ∈ 𝑆 → ( ( ♯ ‘ 𝐵 ) ≠ 0 ↔ 𝐵 ≠ ∅ ) )
24	11 23	syl	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) ≠ 0 ↔ 𝐵 ≠ ∅ ) )
25	21 24	mpbid	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
26		n0	⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑎 𝑎 ∈ 𝐵 )
27	25 26	sylib	⊢ ( 𝜑 → ∃ 𝑎 𝑎 ∈ 𝐵 )
28	11	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝐵 ∈ 𝑆 )
29		simplr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐻 ) → 𝑎 ∈ 𝐵 )
30		oveq2	⊢ ( 𝑧 = 𝑎 → ( 𝑏 + 𝑧 ) = ( 𝑏 + 𝑎 ) )
31		eqid	⊢ ( 𝑧 ∈ 𝐵 ↦ ( 𝑏 + 𝑧 ) ) = ( 𝑧 ∈ 𝐵 ↦ ( 𝑏 + 𝑧 ) )
32		ovex	⊢ ( 𝑏 + 𝑎 ) ∈ V
33	30 31 32	fvmpt	⊢ ( 𝑎 ∈ 𝐵 → ( ( 𝑧 ∈ 𝐵 ↦ ( 𝑏 + 𝑧 ) ) ‘ 𝑎 ) = ( 𝑏 + 𝑎 ) )
34	29 33	syl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐻 ) → ( ( 𝑧 ∈ 𝐵 ↦ ( 𝑏 + 𝑧 ) ) ‘ 𝑎 ) = ( 𝑏 + 𝑎 ) )
35		ovex	⊢ ( 𝑏 + 𝑧 ) ∈ V
36	35 31	fnmpti	⊢ ( 𝑧 ∈ 𝐵 ↦ ( 𝑏 + 𝑧 ) ) Fn 𝐵
37		fnfvelrn	⊢ ( ( ( 𝑧 ∈ 𝐵 ↦ ( 𝑏 + 𝑧 ) ) Fn 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝑧 ∈ 𝐵 ↦ ( 𝑏 + 𝑧 ) ) ‘ 𝑎 ) ∈ ran ( 𝑧 ∈ 𝐵 ↦ ( 𝑏 + 𝑧 ) ) )
38	36 29 37	sylancr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐻 ) → ( ( 𝑧 ∈ 𝐵 ↦ ( 𝑏 + 𝑧 ) ) ‘ 𝑎 ) ∈ ran ( 𝑧 ∈ 𝐵 ↦ ( 𝑏 + 𝑧 ) ) )
39	34 38	eqeltrrd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐻 ) → ( 𝑏 + 𝑎 ) ∈ ran ( 𝑧 ∈ 𝐵 ↦ ( 𝑏 + 𝑧 ) ) )
40	12	ssrab3	⊢ 𝐻 ⊆ 𝑋
41		simpr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐻 ) → 𝑏 ∈ 𝐻 )
42	40 41	sselid	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐻 ) → 𝑏 ∈ 𝑋 )
43	11	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐻 ) → 𝐵 ∈ 𝑆 )
44		mptexg	⊢ ( 𝐵 ∈ 𝑆 → ( 𝑧 ∈ 𝐵 ↦ ( 𝑏 + 𝑧 ) ) ∈ V )
45		rnexg	⊢ ( ( 𝑧 ∈ 𝐵 ↦ ( 𝑏 + 𝑧 ) ) ∈ V → ran ( 𝑧 ∈ 𝐵 ↦ ( 𝑏 + 𝑧 ) ) ∈ V )
46	43 44 45	3syl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐻 ) → ran ( 𝑧 ∈ 𝐵 ↦ ( 𝑏 + 𝑧 ) ) ∈ V )
47		simpr	⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = 𝐵 ) → 𝑦 = 𝐵 )
48		simpl	⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = 𝐵 ) → 𝑥 = 𝑏 )
49	48	oveq1d	⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = 𝐵 ) → ( 𝑥 + 𝑧 ) = ( 𝑏 + 𝑧 ) )
50	47 49	mpteq12dv	⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = 𝐵 ) → ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) = ( 𝑧 ∈ 𝐵 ↦ ( 𝑏 + 𝑧 ) ) )
51	50	rneqd	⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = 𝐵 ) → ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) = ran ( 𝑧 ∈ 𝐵 ↦ ( 𝑏 + 𝑧 ) ) )
52	51 9	ovmpoga	⊢ ( ( 𝑏 ∈ 𝑋 ∧ 𝐵 ∈ 𝑆 ∧ ran ( 𝑧 ∈ 𝐵 ↦ ( 𝑏 + 𝑧 ) ) ∈ V ) → ( 𝑏 ⊕ 𝐵 ) = ran ( 𝑧 ∈ 𝐵 ↦ ( 𝑏 + 𝑧 ) ) )
53	42 43 46 52	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐻 ) → ( 𝑏 ⊕ 𝐵 ) = ran ( 𝑧 ∈ 𝐵 ↦ ( 𝑏 + 𝑧 ) ) )
54	39 53	eleqtrrd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐻 ) → ( 𝑏 + 𝑎 ) ∈ ( 𝑏 ⊕ 𝐵 ) )
55		oveq1	⊢ ( 𝑢 = 𝑏 → ( 𝑢 ⊕ 𝐵 ) = ( 𝑏 ⊕ 𝐵 ) )
56	55	eqeq1d	⊢ ( 𝑢 = 𝑏 → ( ( 𝑢 ⊕ 𝐵 ) = 𝐵 ↔ ( 𝑏 ⊕ 𝐵 ) = 𝐵 ) )
57	56 12	elrab2	⊢ ( 𝑏 ∈ 𝐻 ↔ ( 𝑏 ∈ 𝑋 ∧ ( 𝑏 ⊕ 𝐵 ) = 𝐵 ) )
58	57	simprbi	⊢ ( 𝑏 ∈ 𝐻 → ( 𝑏 ⊕ 𝐵 ) = 𝐵 )
59	58	adantl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐻 ) → ( 𝑏 ⊕ 𝐵 ) = 𝐵 )
60	54 59	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐻 ) → ( 𝑏 + 𝑎 ) ∈ 𝐵 )
61	60	ex	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑏 ∈ 𝐻 → ( 𝑏 + 𝑎 ) ∈ 𝐵 ) )
62	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐻 ∧ 𝑐 ∈ 𝐻 ) ) → 𝐺 ∈ Grp )
63		simprl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐻 ∧ 𝑐 ∈ 𝐻 ) ) → 𝑏 ∈ 𝐻 )
64	40 63	sselid	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐻 ∧ 𝑐 ∈ 𝐻 ) ) → 𝑏 ∈ 𝑋 )
65		simprr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐻 ∧ 𝑐 ∈ 𝐻 ) ) → 𝑐 ∈ 𝐻 )
66	40 65	sselid	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐻 ∧ 𝑐 ∈ 𝐻 ) ) → 𝑐 ∈ 𝑋 )
67	15	simpld	⊢ ( 𝜑 → 𝐵 ∈ 𝒫 𝑋 )
68	67	elpwid	⊢ ( 𝜑 → 𝐵 ⊆ 𝑋 )
69	68	sselda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑎 ∈ 𝑋 )
70	69	adantr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐻 ∧ 𝑐 ∈ 𝐻 ) ) → 𝑎 ∈ 𝑋 )
71	1 7	grprcan	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ) ) → ( ( 𝑏 + 𝑎 ) = ( 𝑐 + 𝑎 ) ↔ 𝑏 = 𝑐 ) )
72	62 64 66 70 71	syl13anc	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐻 ∧ 𝑐 ∈ 𝐻 ) ) → ( ( 𝑏 + 𝑎 ) = ( 𝑐 + 𝑎 ) ↔ 𝑏 = 𝑐 ) )
73	72	ex	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝑏 ∈ 𝐻 ∧ 𝑐 ∈ 𝐻 ) → ( ( 𝑏 + 𝑎 ) = ( 𝑐 + 𝑎 ) ↔ 𝑏 = 𝑐 ) ) )
74	61 73	dom2d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝐵 ∈ 𝑆 → 𝐻 ≼ 𝐵 ) )
75	28 74	mpd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝐻 ≼ 𝐵 )
76	27 75	exlimddv	⊢ ( 𝜑 → 𝐻 ≼ 𝐵 )
77		ssfi	⊢ ( ( 𝑋 ∈ Fin ∧ 𝐻 ⊆ 𝑋 ) → 𝐻 ∈ Fin )
78	3 40 77	sylancl	⊢ ( 𝜑 → 𝐻 ∈ Fin )
79	3 68	ssfid	⊢ ( 𝜑 → 𝐵 ∈ Fin )
80		hashdom	⊢ ( ( 𝐻 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐻 ) ≤ ( ♯ ‘ 𝐵 ) ↔ 𝐻 ≼ 𝐵 ) )
81	78 79 80	syl2anc	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) ≤ ( ♯ ‘ 𝐵 ) ↔ 𝐻 ≼ 𝐵 ) )
82	76 81	mpbird	⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ≤ ( ♯ ‘ 𝐵 ) )
83	82 16	breqtrd	⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ≤ ( 𝑃 ↑ 𝑁 ) )