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

Definition df-pco 23536
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 23531 . 2 class *𝑝
2 vj . . 3 setvar 𝑗
3 ctop 21429 . . 3 class Top
4 vf . . . 4 setvar 𝑓
5 vg . . . 4 setvar 𝑔
6 cii 23410 . . . . 5 class II
72cv 1527 . . . . 5 class 𝑗
8 ccn 21760 . . . . 5 class Cn
96, 7, 8co 7145 . . . 4 class (II Cn 𝑗)
10 vx . . . . 5 setvar 𝑥
11 cc0 10525 . . . . . 6 class 0
12 c1 10526 . . . . . 6 class 1
13 cicc 12729 . . . . . 6 class [,]
1411, 12, 13co 7145 . . . . 5 class (0[,]1)
1510cv 1527 . . . . . . 7 class 𝑥
16 c2 11680 . . . . . . . 8 class 2
17 cdiv 11285 . . . . . . . 8 class /
1812, 16, 17co 7145 . . . . . . 7 class (1 / 2)
19 cle 10664 . . . . . . 7 class
2015, 18, 19wbr 5057 . . . . . 6 wff 𝑥 ≤ (1 / 2)
21 cmul 10530 . . . . . . . 8 class ·
2216, 15, 21co 7145 . . . . . . 7 class (2 · 𝑥)
234cv 1527 . . . . . . 7 class 𝑓
2422, 23cfv 6348 . . . . . 6 class (𝑓‘(2 · 𝑥))
25 cmin 10858 . . . . . . . 8 class
2622, 12, 25co 7145 . . . . . . 7 class ((2 · 𝑥) − 1)
275cv 1527 . . . . . . 7 class 𝑔
2826, 27cfv 6348 . . . . . 6 class (𝑔‘((2 · 𝑥) − 1))
2920, 24, 28cif 4463 . . . . 5 class if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))
3010, 14, 29cmpt 5137 . . . 4 class (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))
314, 5, 9, 9, 30cmpo 7147 . . 3 class (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))))
322, 3, 31cmpt 5137 . 2 class (𝑗 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))))
331, 32wceq 1528 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  23541
  Copyright terms: Public domain W3C validator