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 \in TopOn (X) \land Y \in X) \to G \in Grp$

Proof

Step	Hyp	Ref	Expression
1		pi1grp.2	$⊢ G = J π_{1} Y$
2		eqid	$⊢ {Base}_{G} = {Base}_{G}$
3		simpl	$⊢ (J \in TopOn (X) \land Y \in X) \to J \in TopOn (X)$
4		simpr	$⊢ (J \in TopOn (X) \land Y \in X) \to Y \in X$
5		eqid	$⊢ [0, 1] \times \{Y\} = [0, 1] \times \{Y\}$
6	1 2 3 4 5	pi1grplem	$⊢ (J \in TopOn (X) \land Y \in X) \to (G \in Grp \land [([0, 1] \times \{Y\})] ≃_{ph} (J) = 0_{G})$
7	6	simpld	$⊢ (J \in TopOn (X) \land Y \in X) \to G \in Grp$