Definition df-pco 24503

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

Step	Hyp	Ref	Expression
1		cpco 24498	. 2 class *𝑝
2		vj	. . 3 setvar 𝑗
3		ctop 22377	. . 3 class Top
4		vf	. . . 4 setvar 𝑓
5		vg	. . . 4 setvar 𝑔
6		cii 24373	. . . . 5 class II
7	2	cv 1541	. . . . 5 class 𝑗
8		ccn 22710	. . . . 5 class Cn
9	6, 7, 8	co 7404	. . . 4 class (II Cn 𝑗)
10		vx	. . . . 5 setvar 𝑥
11		cc0 11106	. . . . . 6 class 0
12		c1 11107	. . . . . 6 class 1
13		cicc 13323	. . . . . 6 class [,]
14	11, 12, 13	co 7404	. . . . 5 class (0[,]1)
15	10	cv 1541	. . . . . . 7 class 𝑥
16		c2 12263	. . . . . . . 8 class 2
17		cdiv 11867	. . . . . . . 8 class /
18	12, 16, 17	co 7404	. . . . . . 7 class (1 / 2)
19		cle 11245	. . . . . . 7 class ≤
20	15, 18, 19	wbr 5147	. . . . . 6 wff 𝑥 ≤ (1 / 2)
21		cmul 11111	. . . . . . . 8 class ·
22	16, 15, 21	co 7404	. . . . . . 7 class (2 · 𝑥)
23	4	cv 1541	. . . . . . 7 class 𝑓
24	22, 23	cfv 6540	. . . . . 6 class (𝑓‘(2 · 𝑥))
25		cmin 11440	. . . . . . . 8 class −
26	22, 12, 25	co 7404	. . . . . . 7 class ((2 · 𝑥) − 1)
27	5	cv 1541	. . . . . . 7 class 𝑔
28	26, 27	cfv 6540	. . . . . 6 class (𝑔‘((2 · 𝑥) − 1))
29	20, 24, 28	cif 4527	. . . . 5 class if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))
30	10, 14, 29	cmpt 5230	. . . 4 class (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))
31	4, 5, 9, 9, 30	cmpo 7406	. . 3 class (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))))
32	2, 3, 31	cmpt 5230	. 2 class (𝑗 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))))
33	1, 32	wceq 1542	1 wff *𝑝 = (𝑗 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))))

This definition is referenced by:  pcofval  24508