Metamath Proof Explorer

Theorem pi1grp

Description: The fundamental group is a group. Proposition 1.3 of Hatcher p. 26. (Contributed by Jeff Madsen, 19-Jun-2010) (Proof shortened by Mario Carneiro, 8-Jun-2014) (Revised by Mario Carneiro, 10-Aug-2015)

Ref Expression
Hypothesis pi1grp.2 ⊢ G = J π 1 Y
Assertion pi1grp ⊢ J ∈ TopOn ⁡ X ∧ Y ∈ X → G ∈ Grp

Proof

Step Hyp Ref Expression
1 pi1grp.2 ⊢ G = J π 1 Y
2 eqid ⊢ Base G = Base G
3 simpl ⊢ J ∈ TopOn ⁡ X ∧ Y ∈ X → J ∈ TopOn ⁡ X
4 simpr ⊢ J ∈ TopOn ⁡ X ∧ Y ∈ X → Y ∈ X
5 eqid ⊢ 0 1 × Y = 0 1 × Y
6 1 2 3 4 5 pi1grplem ⊢ J ∈ TopOn ⁡ X ∧ Y ∈ X → G ∈ Grp ∧ 0 1 × Y ≃ ph ⁡ J = 0 G
7 6 simpld ⊢ J ∈ TopOn ⁡ X ∧ Y ∈ X → G ∈ Grp