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 24168
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 24163 . 2 class *𝑝
2 vj . . 3 setvar 𝑗
3 ctop 22042 . . 3 class Top
4 vf . . . 4 setvar 𝑓
5 vg . . . 4 setvar 𝑔
6 cii 24038 . . . . 5 class II
72cv 1538 . . . . 5 class 𝑗
8 ccn 22375 . . . . 5 class Cn
96, 7, 8co 7275 . . . 4 class (II Cn 𝑗)
10 vx . . . . 5 setvar 𝑥
11 cc0 10871 . . . . . 6 class 0
12 c1 10872 . . . . . 6 class 1
13 cicc 13082 . . . . . 6 class [,]
1411, 12, 13co 7275 . . . . 5 class (0[,]1)
1510cv 1538 . . . . . . 7 class 𝑥
16 c2 12028 . . . . . . . 8 class 2
17 cdiv 11632 . . . . . . . 8 class /
1812, 16, 17co 7275 . . . . . . 7 class (1 / 2)
19 cle 11010 . . . . . . 7 class
2015, 18, 19wbr 5074 . . . . . 6 wff 𝑥 ≤ (1 / 2)
21 cmul 10876 . . . . . . . 8 class ·
2216, 15, 21co 7275 . . . . . . 7 class (2 · 𝑥)
234cv 1538 . . . . . . 7 class 𝑓
2422, 23cfv 6433 . . . . . 6 class (𝑓‘(2 · 𝑥))
25 cmin 11205 . . . . . . . 8 class
2622, 12, 25co 7275 . . . . . . 7 class ((2 · 𝑥) − 1)
275cv 1538 . . . . . . 7 class 𝑔
2826, 27cfv 6433 . . . . . 6 class (𝑔‘((2 · 𝑥) − 1))
2920, 24, 28cif 4459 . . . . 5 class if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))
3010, 14, 29cmpt 5157 . . . 4 class (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))
314, 5, 9, 9, 30cmpo 7277 . . 3 class (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))))
322, 3, 31cmpt 5157 . 2 class (𝑗 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))))
331, 32wceq 1539 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  24173
  Copyright terms: Public domain W3C validator