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 ∈ II Cn j , g ∈ II Cn j ⟼ x ∈ 0 1 ⟼ if x ≤ 1 2 f ⁡ 2 ⁢ x g ⁡ 2 ⁢ x − 1

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpco class * 𝑝
1 vj setvar j
2 ctop class Top
3 vf setvar f
4 cii class II
5 ccn class Cn
6 1 cv setvar j
7 4 6 5 co class II Cn j
8 vg setvar g
9 vx setvar x
10 cc0 class 0
11 cicc class .
12 c1 class 1
13 10 12 11 co class 0 1
14 9 cv setvar x
15 cle class ≤
16 cdiv class ÷
17 c2 class 2
18 12 17 16 co class 1 2
19 14 18 15 wbr wff x ≤ 1 2
20 3 cv setvar f
21 cmul class ×
22 17 14 21 co class 2 ⁢ x
23 22 20 cfv class f ⁡ 2 ⁢ x
24 8 cv setvar g
25 cmin class −
26 22 12 25 co class 2 ⁢ x − 1
27 26 24 cfv class g ⁡ 2 ⁢ x − 1
28 19 23 27 cif class if x ≤ 1 2 f ⁡ 2 ⁢ x g ⁡ 2 ⁢ x − 1
29 9 13 28 cmpt class x ∈ 0 1 ⟼ if x ≤ 1 2 f ⁡ 2 ⁢ x g ⁡ 2 ⁢ x − 1
30 3 8 7 7 29 cmpo class f ∈ II Cn j , g ∈ II Cn j ⟼ x ∈ 0 1 ⟼ if x ≤ 1 2 f ⁡ 2 ⁢ x g ⁡ 2 ⁢ x − 1
31 1 2 30 cmpt class j ∈ Top ⟼ f ∈ II Cn j , g ∈ II Cn j ⟼ x ∈ 0 1 ⟼ if x ≤ 1 2 f ⁡ 2 ⁢ x g ⁡ 2 ⁢ x − 1
32 0 31 wceq wff * 𝑝 = j ∈ Top ⟼ f ∈ II Cn j , g ∈ II Cn j ⟼ x ∈ 0 1 ⟼ if x ≤ 1 2 f ⁡ 2 ⁢ x g ⁡ 2 ⁢ x − 1