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

Metamath Proof Explorer

Theorem slwpss

Description: A proper superset of a Sylow subgroup is not a P -group. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Hypothesis slwispgp.1 ⊢ 𝑆 = ( 𝐺 ↾s 𝐾 )
Assertion slwpss ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → ¬ 𝑃 pGrp 𝑆 )

Proof

Step Hyp Ref Expression
1 slwispgp.1 ⊢ 𝑆 = ( 𝐺 ↾s 𝐾 )
2 simp3 ⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → 𝐻 ⊊ 𝐾 )
3 2 pssned ⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → 𝐻 ≠ 𝐾 )
4 2 pssssd ⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → 𝐻 ⊆ 𝐾 )
5 4 biantrurd ⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → ( 𝑃 pGrp 𝑆 ↔ ( 𝐻 ⊆ 𝐾 ∧ 𝑃 pGrp 𝑆 ) ) )
6 1 slwispgp ⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝐻 ⊆ 𝐾 ∧ 𝑃 pGrp 𝑆 ) ↔ 𝐻 = 𝐾 ) )
7 6 3adant3 ⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → ( ( 𝐻 ⊆ 𝐾 ∧ 𝑃 pGrp 𝑆 ) ↔ 𝐻 = 𝐾 ) )
8 5 7 bitrd ⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → ( 𝑃 pGrp 𝑆 ↔ 𝐻 = 𝐾 ) )
9 8 necon3bbid ⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → ( ¬ 𝑃 pGrp 𝑆 ↔ 𝐻 ≠ 𝐾 ) )
10 3 9 mpbird ⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → ¬ 𝑃 pGrp 𝑆 )