sylow1

Description: Sylow's first theorem. If P ^ N is a prime power that divides the cardinality of G , then G has a supgroup with size P ^ N . This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 16-Jan-2015)

	Ref	Expression
Hypotheses	sylow1.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	sylow1.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	sylow1.f	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	sylow1.p	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	sylow1.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
	sylow1.d	⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝑋 ) )
Assertion	sylow1	⊢ ( 𝜑 → ∃ 𝑔 ∈ ( SubGrp ‘ 𝐺 ) ( ♯ ‘ 𝑔 ) = ( 𝑃 ↑ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		sylow1.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		sylow1.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
3		sylow1.f	⊢ ( 𝜑 → 𝑋 ∈ Fin )
4		sylow1.p	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5		sylow1.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
6		sylow1.d	⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝑋 ) )
7		eqid	⊢ ( +_g ‘ 𝐺 ) = ( +_g ‘ 𝐺 )
8		eqid	⊢ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } = { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) }
9		oveq2	⊢ ( 𝑠 = 𝑧 → ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) = ( 𝑢 ( +_g ‘ 𝐺 ) 𝑧 ) )
10	9	cbvmptv	⊢ ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) = ( 𝑧 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑧 ) )
11		oveq1	⊢ ( 𝑢 = 𝑥 → ( 𝑢 ( +_g ‘ 𝐺 ) 𝑧 ) = ( 𝑥 ( +_g ‘ 𝐺 ) 𝑧 ) )
12	11	mpteq2dv	⊢ ( 𝑢 = 𝑥 → ( 𝑧 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑧 ) ) = ( 𝑧 ∈ 𝑣 ↦ ( 𝑥 ( +_g ‘ 𝐺 ) 𝑧 ) ) )
13	10 12	eqtrid	⊢ ( 𝑢 = 𝑥 → ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) = ( 𝑧 ∈ 𝑣 ↦ ( 𝑥 ( +_g ‘ 𝐺 ) 𝑧 ) ) )
14	13	rneqd	⊢ ( 𝑢 = 𝑥 → ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) = ran ( 𝑧 ∈ 𝑣 ↦ ( 𝑥 ( +_g ‘ 𝐺 ) 𝑧 ) ) )
15		mpteq1	⊢ ( 𝑣 = 𝑦 → ( 𝑧 ∈ 𝑣 ↦ ( 𝑥 ( +_g ‘ 𝐺 ) 𝑧 ) ) = ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 ( +_g ‘ 𝐺 ) 𝑧 ) ) )
16	15	rneqd	⊢ ( 𝑣 = 𝑦 → ran ( 𝑧 ∈ 𝑣 ↦ ( 𝑥 ( +_g ‘ 𝐺 ) 𝑧 ) ) = ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 ( +_g ‘ 𝐺 ) 𝑧 ) ) )
17	14 16	cbvmpov	⊢ ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 ( +_g ‘ 𝐺 ) 𝑧 ) ) )
18		preq12	⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → { 𝑎 , 𝑏 } = { 𝑥 , 𝑦 } )
19	18	sseq1d	⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↔ { 𝑥 , 𝑦 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ) )
20		oveq2	⊢ ( 𝑎 = 𝑥 → ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) ) 𝑥 ) )
21		id	⊢ ( 𝑏 = 𝑦 → 𝑏 = 𝑦 )
22	20 21	eqeqan12d	⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ↔ ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) ) 𝑥 ) = 𝑦 ) )
23	22	rexbidv	⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ↔ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) ) 𝑥 ) = 𝑦 ) )
24	19 23	anbi12d	⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) ↔ ( { 𝑥 , 𝑦 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) ) 𝑥 ) = 𝑦 ) ) )
25	24	cbvopabv	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) ) 𝑥 ) = 𝑦 ) }
26	1 2 3 4 5 6 7 8 17 25	sylow1lem3	⊢ ( 𝜑 → ∃ ℎ ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ( 𝑃 pCnt ( ♯ ‘ [ ℎ ] { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) )
27	2	adantr	⊢ ( ( 𝜑 ∧ ( ℎ ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ℎ ] { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → 𝐺 ∈ Grp )
28	3	adantr	⊢ ( ( 𝜑 ∧ ( ℎ ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ℎ ] { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → 𝑋 ∈ Fin )
29	4	adantr	⊢ ( ( 𝜑 ∧ ( ℎ ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ℎ ] { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → 𝑃 ∈ ℙ )
30	5	adantr	⊢ ( ( 𝜑 ∧ ( ℎ ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ℎ ] { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → 𝑁 ∈ ℕ₀ )
31	6	adantr	⊢ ( ( 𝜑 ∧ ( ℎ ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ℎ ] { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝑋 ) )
32		simprl	⊢ ( ( 𝜑 ∧ ( ℎ ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ℎ ] { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → ℎ ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } )
33		eqid	⊢ { 𝑡 ∈ 𝑋 ∣ ( 𝑡 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) ) ℎ ) = ℎ } = { 𝑡 ∈ 𝑋 ∣ ( 𝑡 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) ) ℎ ) = ℎ }
34		simprr	⊢ ( ( 𝜑 ∧ ( ℎ ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ℎ ] { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → ( 𝑃 pCnt ( ♯ ‘ [ ℎ ] { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) )
35	1 27 28 29 30 31 7 8 17 25 32 33 34	sylow1lem5	⊢ ( ( 𝜑 ∧ ( ℎ ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ℎ ] { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ( 𝑢 ∈ 𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) } ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 ( +_g ‘ 𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → ∃ 𝑔 ∈ ( SubGrp ‘ 𝐺 ) ( ♯ ‘ 𝑔 ) = ( 𝑃 ↑ 𝑁 ) )
36	26 35	rexlimddv	⊢ ( 𝜑 → ∃ 𝑔 ∈ ( SubGrp ‘ 𝐺 ) ( ♯ ‘ 𝑔 ) = ( 𝑃 ↑ 𝑁 ) )

Metamath Proof Explorer

Theorem sylow1

Proof