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	⊢ *𝑝 = ( 𝑗 ∈ Top ↦ ( 𝑓 ∈ ( II Cn 𝑗 ) , 𝑔 ∈ ( II Cn 𝑗 ) ↦ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑓 ‘ ( 2 · 𝑥 ) ) , ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpco	⊢ *𝑝
1		vj	⊢ 𝑗
2		ctop	⊢ Top
3		vf	⊢ 𝑓
4		cii	⊢ II
5		ccn	⊢ Cn
6	1	cv	⊢ 𝑗
7	4 6 5	co	⊢ ( II Cn 𝑗 )
8		vg	⊢ 𝑔
9		vx	⊢ 𝑥
10		cc0	⊢ 0
11		cicc	⊢ [,]
12		c1	⊢ 1
13	10 12 11	co	⊢ ( 0 [,] 1 )
14	9	cv	⊢ 𝑥
15		cle	⊢ ≤
16		cdiv	⊢ /
17		c2	⊢ 2
18	12 17 16	co	⊢ ( 1 / 2 )
19	14 18 15	wbr	⊢ 𝑥 ≤ ( 1 / 2 )
20	3	cv	⊢ 𝑓
21		cmul	⊢ ·
22	17 14 21	co	⊢ ( 2 · 𝑥 )
23	22 20	cfv	⊢ ( 𝑓 ‘ ( 2 · 𝑥 ) )
24	8	cv	⊢ 𝑔
25		cmin	⊢ −
26	22 12 25	co	⊢ ( ( 2 · 𝑥 ) − 1 )
27	26 24	cfv	⊢ ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) )
28	19 23 27	cif	⊢ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑓 ‘ ( 2 · 𝑥 ) ) , ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) )
29	9 13 28	cmpt	⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑓 ‘ ( 2 · 𝑥 ) ) , ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) )
30	3 8 7 7 29	cmpo	⊢ ( 𝑓 ∈ ( II Cn 𝑗 ) , 𝑔 ∈ ( II Cn 𝑗 ) ↦ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑓 ‘ ( 2 · 𝑥 ) ) , ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) )
31	1 2 30	cmpt	⊢ ( 𝑗 ∈ Top ↦ ( 𝑓 ∈ ( II Cn 𝑗 ) , 𝑔 ∈ ( II Cn 𝑗 ) ↦ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑓 ‘ ( 2 · 𝑥 ) ) , ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ) )
32	0 31	wceq	⊢ *𝑝 = ( 𝑗 ∈ Top ↦ ( 𝑓 ∈ ( II Cn 𝑗 ) , 𝑔 ∈ ( II Cn 𝑗 ) ↦ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑓 ‘ ( 2 · 𝑥 ) ) , ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ) )