Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-pco Structured version   Unicode version

Definition df-pco 21371
 Description: Define the concatenation of two paths in a topological space . For simplicity of definition, we define it on all paths, not just those whose endpoints line up. Definition of [Hatcher] p. 26. Hatcher denotes path concatenation with a square dot; other authors, such as Munkres, use a star. (Contributed by Jeff Madsen, 15-Jun-2010.)
Assertion
Ref Expression
df-pco
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-pco
StepHypRef Expression
1 cpco 21366 . 2
2 vj . . 3
3 ctop 19261 . . 3
4 vf . . . 4
5 vg . . . 4
6 cii 21245 . . . . 5
72cv 1380 . . . . 5
8 ccn 19591 . . . . 5
96, 7, 8co 6277 . . . 4
10 vx . . . . 5
11 cc0 9490 . . . . . 6
12 c1 9491 . . . . . 6
13 cicc 11536 . . . . . 6
1411, 12, 13co 6277 . . . . 5
1510cv 1380 . . . . . . 7
16 c2 10586 . . . . . . . 8
17 cdiv 10207 . . . . . . . 8
1812, 16, 17co 6277 . . . . . . 7
19 cle 9627 . . . . . . 7
2015, 18, 19wbr 4433 . . . . . 6
21 cmul 9495 . . . . . . . 8
2216, 15, 21co 6277 . . . . . . 7
234cv 1380 . . . . . . 7
2422, 23cfv 5574 . . . . . 6
25 cmin 9805 . . . . . . . 8
2622, 12, 25co 6277 . . . . . . 7
275cv 1380 . . . . . . 7
2826, 27cfv 5574 . . . . . 6
2920, 24, 28cif 3922 . . . . 5
3010, 14, 29cmpt 4491 . . . 4
314, 5, 9, 9, 30cmpt2 6279 . . 3
322, 3, 31cmpt 4491 . 2
331, 32wceq 1381 1
 Colors of variables: wff setvar class This definition is referenced by:  pcofval  21376
 Copyright terms: Public domain W3C validator