Definition df-pco 24074

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 24069	. 2 class *𝑝
2		vj	. . 3 setvar 𝑗
3		ctop 21950	. . 3 class Top
4		vf	. . . 4 setvar 𝑓
5		vg	. . . 4 setvar 𝑔
6		cii 23944	. . . . 5 class II
7	2	cv 1538	. . . . 5 class 𝑗
8		ccn 22283	. . . . 5 class Cn
9	6, 7, 8	co 7255	. . . 4 class (II Cn 𝑗)
10		vx	. . . . 5 setvar 𝑥
11		cc0 10802	. . . . . 6 class 0
12		c1 10803	. . . . . 6 class 1
13		cicc 13011	. . . . . 6 class [,]
14	11, 12, 13	co 7255	. . . . 5 class (0[,]1)
15	10	cv 1538	. . . . . . 7 class 𝑥
16		c2 11958	. . . . . . . 8 class 2
17		cdiv 11562	. . . . . . . 8 class /
18	12, 16, 17	co 7255	. . . . . . 7 class (1 / 2)
19		cle 10941	. . . . . . 7 class ≤
20	15, 18, 19	wbr 5070	. . . . . 6 wff 𝑥 ≤ (1 / 2)
21		cmul 10807	. . . . . . . 8 class ·
22	16, 15, 21	co 7255	. . . . . . 7 class (2 · 𝑥)
23	4	cv 1538	. . . . . . 7 class 𝑓
24	22, 23	cfv 6418	. . . . . 6 class (𝑓‘(2 · 𝑥))
25		cmin 11135	. . . . . . . 8 class −
26	22, 12, 25	co 7255	. . . . . . 7 class ((2 · 𝑥) − 1)
27	5	cv 1538	. . . . . . 7 class 𝑔
28	26, 27	cfv 6418	. . . . . 6 class (𝑔‘((2 · 𝑥) − 1))
29	20, 24, 28	cif 4456	. . . . 5 class if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))
30	10, 14, 29	cmpt 5153	. . . 4 class (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))
31	4, 5, 9, 9, 30	cmpo 7257	. . 3 class (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))))
32	2, 3, 31	cmpt 5153	. 2 class (𝑗 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))))
33	1, 32	wceq 1539	1 wff *𝑝 = (𝑗 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))))

This definition is referenced by:  pcofval  24079