Definition df-om1 23604

Description: Define the loop space of a topological space, with a magma structure on it given by concatenation of loops. This structure is not a group, but the operation is compatible with homotopy, which allows the homotopy groups to be defined based on this operation. (Contributed by Mario Carneiro, 10-Jul-2015.)

Assertion

Ref	Expression
df-om1	⊢ Ω1 = (𝑗 ∈ Top, 𝑦 ∈ ∪ 𝑗 ↦ {⟨(Base‘ndx), {𝑓 ∈ (II Cn 𝑗) ∣ ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)}⟩, ⟨(+g‘ndx), (*𝑝‘𝑗)⟩, ⟨(TopSet‘ndx), (𝑗 ↑ko II)⟩})

Distinct variable group:   𝑓,𝑗,𝑦

Detailed syntax breakdown of Definition df-om1

Step	Hyp	Ref	Expression
1		comi 23599	. 2 class Ω1
2		vj	. . 3 setvar 𝑗
3		vy	. . 3 setvar 𝑦
4		ctop 21495	. . 3 class Top
5	2	cv 1532	. . . 4 class 𝑗
6	5	cuni 4831	. . 3 class ∪ 𝑗
7		cnx 16474	. . . . . 6 class ndx
8		cbs 16477	. . . . . 6 class Base
9	7, 8	cfv 6349	. . . . 5 class (Base‘ndx)
10		cc0 10531	. . . . . . . . 9 class 0
11		vf	. . . . . . . . . 10 setvar 𝑓
12	11	cv 1532	. . . . . . . . 9 class 𝑓
13	10, 12	cfv 6349	. . . . . . . 8 class (𝑓‘0)
14	3	cv 1532	. . . . . . . 8 class 𝑦
15	13, 14	wceq 1533	. . . . . . 7 wff (𝑓‘0) = 𝑦
16		c1 10532	. . . . . . . . 9 class 1
17	16, 12	cfv 6349	. . . . . . . 8 class (𝑓‘1)
18	17, 14	wceq 1533	. . . . . . 7 wff (𝑓‘1) = 𝑦
19	15, 18	wa 398	. . . . . 6 wff ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)
20		cii 23477	. . . . . . 7 class II
21		ccn 21826	. . . . . . 7 class Cn
22	20, 5, 21	co 7150	. . . . . 6 class (II Cn 𝑗)
23	19, 11, 22	crab 3142	. . . . 5 class {𝑓 ∈ (II Cn 𝑗) ∣ ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)}
24	9, 23	cop 4566	. . . 4 class ⟨(Base‘ndx), {𝑓 ∈ (II Cn 𝑗) ∣ ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)}⟩
25		cplusg 16559	. . . . . 6 class +g
26	7, 25	cfv 6349	. . . . 5 class (+g‘ndx)
27		cpco 23598	. . . . . 6 class *𝑝
28	5, 27	cfv 6349	. . . . 5 class (*𝑝‘𝑗)
29	26, 28	cop 4566	. . . 4 class ⟨(+g‘ndx), (*𝑝‘𝑗)⟩
30		cts 16565	. . . . . 6 class TopSet
31	7, 30	cfv 6349	. . . . 5 class (TopSet‘ndx)
32		cxko 22163	. . . . . 6 class ↑ko
33	5, 20, 32	co 7150	. . . . 5 class (𝑗 ↑ko II)
34	31, 33	cop 4566	. . . 4 class ⟨(TopSet‘ndx), (𝑗 ↑ko II)⟩
35	24, 29, 34	ctp 4564	. . 3 class {⟨(Base‘ndx), {𝑓 ∈ (II Cn 𝑗) ∣ ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)}⟩, ⟨(+g‘ndx), (*𝑝‘𝑗)⟩, ⟨(TopSet‘ndx), (𝑗 ↑ko II)⟩}
36	2, 3, 4, 6, 35	cmpo 7152	. 2 class (𝑗 ∈ Top, 𝑦 ∈ ∪ 𝑗 ↦ {⟨(Base‘ndx), {𝑓 ∈ (II Cn 𝑗) ∣ ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)}⟩, ⟨(+g‘ndx), (*𝑝‘𝑗)⟩, ⟨(TopSet‘ndx), (𝑗 ↑ko II)⟩})
37	1, 36	wceq 1533	1 wff Ω1 = (𝑗 ∈ Top, 𝑦 ∈ ∪ 𝑗 ↦ {⟨(Base‘ndx), {𝑓 ∈ (II Cn 𝑗) ∣ ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)}⟩, ⟨(+g‘ndx), (*𝑝‘𝑗)⟩, ⟨(TopSet‘ndx), (𝑗 ↑ko II)⟩})

This definition is referenced by:  om1val  23628