Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-pco Structured version   Visualization version   GIF version

Definition df-pco 22613
 Description: Define the concatenation of two paths in a topological space 𝐽. 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.)
Assertion
Ref Expression
df-pco *𝑝 = (𝑗 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))))
Distinct variable group:   𝑓,𝑔,𝑗,𝑥

Detailed syntax breakdown of Definition df-pco
StepHypRef Expression
1 cpco 22608 . 2 class *𝑝
2 vj . . 3 setvar 𝑗
3 ctop 20517 . . 3 class Top
4 vf . . . 4 setvar 𝑓
5 vg . . . 4 setvar 𝑔
6 cii 22486 . . . . 5 class II
72cv 1474 . . . . 5 class 𝑗
8 ccn 20838 . . . . 5 class Cn
96, 7, 8co 6549 . . . 4 class (II Cn 𝑗)
10 vx . . . . 5 setvar 𝑥
11 cc0 9815 . . . . . 6 class 0
12 c1 9816 . . . . . 6 class 1
13 cicc 12049 . . . . . 6 class [,]
1411, 12, 13co 6549 . . . . 5 class (0[,]1)
1510cv 1474 . . . . . . 7 class 𝑥
16 c2 10947 . . . . . . . 8 class 2
17 cdiv 10563 . . . . . . . 8 class /
1812, 16, 17co 6549 . . . . . . 7 class (1 / 2)
19 cle 9954 . . . . . . 7 class
2015, 18, 19wbr 4583 . . . . . 6 wff 𝑥 ≤ (1 / 2)
21 cmul 9820 . . . . . . . 8 class ·
2216, 15, 21co 6549 . . . . . . 7 class (2 · 𝑥)
234cv 1474 . . . . . . 7 class 𝑓
2422, 23cfv 5804 . . . . . 6 class (𝑓‘(2 · 𝑥))
25 cmin 10145 . . . . . . . 8 class
2622, 12, 25co 6549 . . . . . . 7 class ((2 · 𝑥) − 1)
275cv 1474 . . . . . . 7 class 𝑔
2826, 27cfv 5804 . . . . . 6 class (𝑔‘((2 · 𝑥) − 1))
2920, 24, 28cif 4036 . . . . 5 class if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))
3010, 14, 29cmpt 4643 . . . 4 class (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))
314, 5, 9, 9, 30cmpt2 6551 . . 3 class (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))))
322, 3, 31cmpt 4643 . 2 class (𝑗 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))))
331, 32wceq 1475 1 wff *𝑝 = (𝑗 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))))
 Colors of variables: wff setvar class This definition is referenced by:  pcofval  22618
 Copyright terms: Public domain W3C validator