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 ⊢*𝑝=j∈Top⟼f∈IICnj,g∈IICnj⟼x∈01⟼ifx≤12f⁡2⁢xg⁡2⁢x−1

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpco class*𝑝
1 vj setvarj
2 ctop classTop
3 vf setvarf
4 cii classII
5 ccn classCn
6 1 cv setvarj
7 4 6 5 co classIICnj
8 vg setvarg
9 vx setvarx
10 cc0 class0
11 cicc class.
12 c1 class1
13 10 12 11 co class01
14 9 cv setvarx
15 cle class≤
16 cdiv class÷
17 c2 class2
18 12 17 16 co class12
19 14 18 15 wbr wffx≤12
20 3 cv setvarf
21 cmul class×
22 17 14 21 co class2⁢x
23 22 20 cfv classf⁡2⁢x
24 8 cv setvarg
25 cmin class−
26 22 12 25 co class2⁢x−1
27 26 24 cfv classg⁡2⁢x−1
28 19 23 27 cif classifx≤12f⁡2⁢xg⁡2⁢x−1
29 9 13 28 cmpt classx∈01⟼ifx≤12f⁡2⁢xg⁡2⁢x−1
30 3 8 7 7 29 cmpo classf∈IICnj,g∈IICnj⟼x∈01⟼ifx≤12f⁡2⁢xg⁡2⁢x−1
31 1 2 30 cmpt classj∈Top⟼f∈IICnj,g∈IICnj⟼x∈01⟼ifx≤12f⁡2⁢xg⁡2⁢x−1
32 0 31 wceq wff*𝑝=j∈Top⟼f∈IICnj,g∈IICnj⟼x∈01⟼ifx≤12f⁡2⁢xg⁡2⁢x−1