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 22713
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 22708 . 2 class *𝑝
2 vj . . 3 setvar 𝑗
3 ctop 20617 . . 3 class Top
4 vf . . . 4 setvar 𝑓
5 vg . . . 4 setvar 𝑔
6 cii 22586 . . . . 5 class II
72cv 1479 . . . . 5 class 𝑗
8 ccn 20938 . . . . 5 class Cn
96, 7, 8co 6604 . . . 4 class (II Cn 𝑗)
10 vx . . . . 5 setvar 𝑥
11 cc0 9880 . . . . . 6 class 0
12 c1 9881 . . . . . 6 class 1
13 cicc 12120 . . . . . 6 class [,]
1411, 12, 13co 6604 . . . . 5 class (0[,]1)
1510cv 1479 . . . . . . 7 class 𝑥
16 c2 11014 . . . . . . . 8 class 2
17 cdiv 10628 . . . . . . . 8 class /
1812, 16, 17co 6604 . . . . . . 7 class (1 / 2)
19 cle 10019 . . . . . . 7 class
2015, 18, 19wbr 4613 . . . . . 6 wff 𝑥 ≤ (1 / 2)
21 cmul 9885 . . . . . . . 8 class ·
2216, 15, 21co 6604 . . . . . . 7 class (2 · 𝑥)
234cv 1479 . . . . . . 7 class 𝑓
2422, 23cfv 5847 . . . . . 6 class (𝑓‘(2 · 𝑥))
25 cmin 10210 . . . . . . . 8 class
2622, 12, 25co 6604 . . . . . . 7 class ((2 · 𝑥) − 1)
275cv 1479 . . . . . . 7 class 𝑔
2826, 27cfv 5847 . . . . . 6 class (𝑔‘((2 · 𝑥) − 1))
2920, 24, 28cif 4058 . . . . 5 class if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))
3010, 14, 29cmpt 4673 . . . 4 class (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))
314, 5, 9, 9, 30cmpt2 6606 . . 3 class (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))))
322, 3, 31cmpt 4673 . 2 class (𝑗 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))))
331, 32wceq 1480 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  22718
  Copyright terms: Public domain W3C validator