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

Definition df-pco 19061
 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 19056 . 2
2 vj . . 3
3 ctop 16989 . . 3
4 vf . . . 4
5 vg . . . 4
6 cii 18936 . . . . 5
72cv 1652 . . . . 5
8 ccn 17319 . . . . 5
96, 7, 8co 6110 . . . 4
10 vx . . . . 5
11 cc0 9021 . . . . . 6
12 c1 9022 . . . . . 6
13 cicc 10950 . . . . . 6
1411, 12, 13co 6110 . . . . 5
1510cv 1652 . . . . . . 7
16 c2 10080 . . . . . . . 8
17 cdiv 9708 . . . . . . . 8
1812, 16, 17co 6110 . . . . . . 7
19 cle 9152 . . . . . . 7
2015, 18, 19wbr 4237 . . . . . 6
21 cmul 9026 . . . . . . . 8
2216, 15, 21co 6110 . . . . . . 7
234cv 1652 . . . . . . 7
2422, 23cfv 5483 . . . . . 6
25 cmin 9322 . . . . . . . 8
2622, 12, 25co 6110 . . . . . . 7
275cv 1652 . . . . . . 7
2826, 27cfv 5483 . . . . . 6
2920, 24, 28cif 3763 . . . . 5
3010, 14, 29cmpt 4291 . . . 4
314, 5, 9, 9, 30cmpt2 6112 . . 3
322, 3, 31cmpt 4291 . 2
331, 32wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  pcofval  19066
 Copyright terms: Public domain W3C validator