This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem slwn0

Description: Every finite group contains a Sylow P -subgroup. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Hypothesis slwn0.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
Assertion slwn0 ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pSyl 𝐺 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 slwn0.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
3 2 0subg ⊢ ( 𝐺 ∈ Grp → { ( 0g ‘ 𝐺 ) } ∈ ( SubGrp ‘ 𝐺 ) )
4 3 3ad2ant1 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) → { ( 0g ‘ 𝐺 ) } ∈ ( SubGrp ‘ 𝐺 ) )
5 simp2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) → 𝑋 ∈ Fin )
6 2 pgp0 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ) → 𝑃 pGrp ( 𝐺 ↾s { ( 0g ‘ 𝐺 ) } ) )
7 6 3adant2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) → 𝑃 pGrp ( 𝐺 ↾s { ( 0g ‘ 𝐺 ) } ) )
8 eqid ⊢ ( 𝐺 ↾s { ( 0g ‘ 𝐺 ) } ) = ( 𝐺 ↾s { ( 0g ‘ 𝐺 ) } )
9 eqid ⊢ ( 𝑥 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ { ( 0g ‘ 𝐺 ) } ⊆ 𝑦 ) } ↦ ( ♯ ‘ 𝑥 ) ) = ( 𝑥 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ { ( 0g ‘ 𝐺 ) } ⊆ 𝑦 ) } ↦ ( ♯ ‘ 𝑥 ) )
10 1 8 9 pgpssslw ⊢ ( ( { ( 0g ‘ 𝐺 ) } ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp ( 𝐺 ↾s { ( 0g ‘ 𝐺 ) } ) ) → ∃ 𝑧 ∈ ( 𝑃 pSyl 𝐺 ) { ( 0g ‘ 𝐺 ) } ⊆ 𝑧 )
11 4 5 7 10 syl3anc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) → ∃ 𝑧 ∈ ( 𝑃 pSyl 𝐺 ) { ( 0g ‘ 𝐺 ) } ⊆ 𝑧 )
12 rexn0 ⊢ ( ∃ 𝑧 ∈ ( 𝑃 pSyl 𝐺 ) { ( 0g ‘ 𝐺 ) } ⊆ 𝑧 → ( 𝑃 pSyl 𝐺 ) ≠ ∅ )
13 11 12 syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pSyl 𝐺 ) ≠ ∅ )