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