Metamath Proof Explorer


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 ) ) ) ) ) )