df-pco - Metamath Proof Explorer

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

Definition df-pco 22805

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**
Step	Hyp	Ref	Expression
1		cpco 22800	. 2
2		vj	. . 3
3		ctop 20698	. . 3
4		vf	. . . 4
5		vg	. . . 4
6		cii 22678	. . . . 5
7	2	cv 1482	. . . . 5
8		ccn 21028	. . . . 5
9	6, 7, 8	co 6650	. . . 4
10		vx	. . . . 5
11		cc0 9936	. . . . . 6
12		c1 9937	. . . . . 6
13		cicc 12178	. . . . . 6
14	11, 12, 13	co 6650	. . . . 5
15	10	cv 1482	. . . . . . 7
16		c2 11070	. . . . . . . 8
17		cdiv 10684	. . . . . . . 8
18	12, 16, 17	co 6650	. . . . . . 7
19		cle 10075	. . . . . . 7
20	15, 18, 19	wbr 4653	. . . . . 6
21		cmul 9941	. . . . . . . 8
22	16, 15, 21	co 6650	. . . . . . 7
23	4	cv 1482	. . . . . . 7
24	22, 23	cfv 5888	. . . . . 6
25		cmin 10266	. . . . . . . 8
26	22, 12, 25	co 6650	. . . . . . 7
27	5	cv 1482	. . . . . . 7
28	26, 27	cfv 5888	. . . . . 6
29	20, 24, 28	cif 4086	. . . . 5
30	10, 14, 29	cmpt 4729	. . . 4
31	4, 5, 9, 9, 30	cmpt2 6652	. . 3
32	2, 3, 31	cmpt 4729	. 2
33	1, 32	wceq 1483	1

Colors of variables: wff setvar class

This definition is referenced by: pcofval 22810

W3C validator