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 𝑆 )