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 pi1 Y ) |
|
| Assertion | pi1grp | |- ( ( J e. ( TopOn ` X ) /\ Y e. X ) -> G e. Grp ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pi1grp.2 | |- G = ( J pi1 Y ) |
|
| 2 | eqid | |- ( Base ` G ) = ( Base ` G ) |
|
| 3 | simpl | |- ( ( J e. ( TopOn ` X ) /\ Y e. X ) -> J e. ( TopOn ` X ) ) |
|
| 4 | simpr | |- ( ( J e. ( TopOn ` X ) /\ Y e. X ) -> Y e. X ) |
|
| 5 | eqid | |- ( ( 0 [,] 1 ) X. { Y } ) = ( ( 0 [,] 1 ) X. { Y } ) |
|
| 6 | 1 2 3 4 5 | pi1grplem | |- ( ( J e. ( TopOn ` X ) /\ Y e. X ) -> ( G e. Grp /\ [ ( ( 0 [,] 1 ) X. { Y } ) ] ( ~=ph ` J ) = ( 0g ` G ) ) ) |
| 7 | 6 | simpld | |- ( ( J e. ( TopOn ` X ) /\ Y e. X ) -> G e. Grp ) |