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 𝐺 = ( 𝐽 π1 𝑌 )
Assertion pi1grp ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑌𝑋 ) → 𝐺 ∈ Grp )

Proof

Step Hyp Ref Expression
1 pi1grp.2 𝐺 = ( 𝐽 π1 𝑌 )
2 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
3 simpl ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑌𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4 simpr ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑌𝑋 ) → 𝑌𝑋 )
5 eqid ( ( 0 [,] 1 ) × { 𝑌 } ) = ( ( 0 [,] 1 ) × { 𝑌 } )
6 1 2 3 4 5 pi1grplem ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑌𝑋 ) → ( 𝐺 ∈ Grp ∧ [ ( ( 0 [,] 1 ) × { 𝑌 } ) ] ( ≃ph𝐽 ) = ( 0g𝐺 ) ) )
7 6 simpld ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑌𝑋 ) → 𝐺 ∈ Grp )