Description: Define the fundamental group, whose operation is given by concatenation of homotopy classes of loops. Definition of Hatcher p. 26. (Contributed by Mario Carneiro, 11-Feb-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-pi1 | |- pi1 = ( j e. Top , y e. U. j |-> ( ( j Om1 y ) /s ( ~=ph ` j ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cpi1 | |- pi1 |
|
| 1 | vj | |- j |
|
| 2 | ctop | |- Top |
|
| 3 | vy | |- y |
|
| 4 | 1 | cv | |- j |
| 5 | 4 | cuni | |- U. j |
| 6 | comi | |- Om1 |
|
| 7 | 3 | cv | |- y |
| 8 | 4 7 6 | co | |- ( j Om1 y ) |
| 9 | cqus | |- /s |
|
| 10 | cphtpc | |- ~=ph |
|
| 11 | 4 10 | cfv | |- ( ~=ph ` j ) |
| 12 | 8 11 9 | co | |- ( ( j Om1 y ) /s ( ~=ph ` j ) ) |
| 13 | 1 3 2 5 12 | cmpo | |- ( j e. Top , y e. U. j |-> ( ( j Om1 y ) /s ( ~=ph ` j ) ) ) |
| 14 | 0 13 | wceq | |- pi1 = ( j e. Top , y e. U. j |-> ( ( j Om1 y ) /s ( ~=ph ` j ) ) ) |