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

Definition df-pco 18503
 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 18498 . 2
2 vj . . 3
3 ctop 16631 . . 3
4 vf . . . 4
5 vg . . . 4
6 cii 18379 . . . . 5
72cv 1622 . . . . 5
8 ccn 16954 . . . . 5
96, 7, 8co 5858 . . . 4
10 vx . . . . 5
11 cc0 8737 . . . . . 6
12 c1 8738 . . . . . 6
13 cicc 10659 . . . . . 6
1411, 12, 13co 5858 . . . . 5
1510cv 1622 . . . . . . 7
16 c2 9795 . . . . . . . 8
17 cdiv 9423 . . . . . . . 8
1812, 16, 17co 5858 . . . . . . 7
19 cle 8868 . . . . . . 7
2015, 18, 19wbr 4023 . . . . . 6
21 cmul 8742 . . . . . . . 8
2216, 15, 21co 5858 . . . . . . 7
234cv 1622 . . . . . . 7
2422, 23cfv 5255 . . . . . 6
25 cmin 9037 . . . . . . . 8
2622, 12, 25co 5858 . . . . . . 7
275cv 1622 . . . . . . 7
2826, 27cfv 5255 . . . . . 6
2920, 24, 28cif 3565 . . . . 5
3010, 14, 29cmpt 4077 . . . 4
314, 5, 9, 9, 30cmpt2 5860 . . 3
322, 3, 31cmpt 4077 . 2
331, 32wceq 1623 1
 Colors of variables: wff set class This definition is referenced by:  pcofval  18508
 Copyright terms: Public domain W3C validator