Description: A Sylow P -subgroup is a subgroup. (Contributed by Mario Carneiro, 16-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | slwsubg | ⊢ ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isslw | ⊢ ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ↔ ( 𝑃 ∈ ℙ ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) ) | |
2 | 1 | simp2bi | ⊢ ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) |