Definition df-pco

Description: Define the concatenation of two paths in a topological space J . 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)

	Ref	Expression
Assertion	df-pco	|- *p = ( j e. Top |-> ( f e. ( II Cn j ) , g e. ( II Cn j ) |-> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( f ` ( 2 x. x ) ) , ( g ` ( ( 2 x. x ) - 1 ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpco	|- *p
1		vj	|- j
2		ctop	|- Top
3		vf	|- f
4		cii	|- II
5		ccn	|- Cn
6	1	cv	|- j
7	4 6 5	co	|- ( II Cn j )
8		vg	|- g
9		vx	|- x
10		cc0	|- 0
11		cicc	|- [,]
12		c1	|- 1
13	10 12 11	co	|- ( 0 [,] 1 )
14	9	cv	|- x
15		cle	|- <_
16		cdiv	|- /
17		c2	|- 2
18	12 17 16	co	|- ( 1 / 2 )
19	14 18 15	wbr	|- x <_ ( 1 / 2 )
20	3	cv	|- f
21		cmul	|- x.
22	17 14 21	co	|- ( 2 x. x )
23	22 20	cfv	|- ( f ` ( 2 x. x ) )
24	8	cv	|- g
25		cmin	|- -
26	22 12 25	co	|- ( ( 2 x. x ) - 1 )
27	26 24	cfv	|- ( g ` ( ( 2 x. x ) - 1 ) )
28	19 23 27	cif	|- if ( x <_ ( 1 / 2 ) , ( f ` ( 2 x. x ) ) , ( g ` ( ( 2 x. x ) - 1 ) ) )
29	9 13 28	cmpt	|- ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( f ` ( 2 x. x ) ) , ( g ` ( ( 2 x. x ) - 1 ) ) ) )
30	3 8 7 7 29	cmpo	|- ( f e. ( II Cn j ) , g e. ( II Cn j ) |-> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( f ` ( 2 x. x ) ) , ( g ` ( ( 2 x. x ) - 1 ) ) ) ) )
31	1 2 30	cmpt	|- ( j e. Top |-> ( f e. ( II Cn j ) , g e. ( II Cn j ) |-> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( f ` ( 2 x. x ) ) , ( g ` ( ( 2 x. x ) - 1 ) ) ) ) ) )
32	0 31	wceq	|- *p = ( j e. Top |-> ( f e. ( II Cn j ) , g e. ( II Cn j ) |-> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( f ` ( 2 x. x ) ) , ( g ` ( ( 2 x. x ) - 1 ) ) ) ) ) )