MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-om1 Structured version   Visualization version   GIF version

Definition df-om1 24521
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
StepHypRef Expression
1 comi 24516 . 2 class Ξ©1
2 vj . . 3 setvar 𝑗
3 vy . . 3 setvar 𝑦
4 ctop 22394 . . 3 class Top
52cv 1540 . . . 4 class 𝑗
65cuni 4908 . . 3 class βˆͺ 𝑗
7 cnx 17125 . . . . . 6 class ndx
8 cbs 17143 . . . . . 6 class Base
97, 8cfv 6543 . . . . 5 class (Baseβ€˜ndx)
10 cc0 11109 . . . . . . . . 9 class 0
11 vf . . . . . . . . . 10 setvar 𝑓
1211cv 1540 . . . . . . . . 9 class 𝑓
1310, 12cfv 6543 . . . . . . . 8 class (π‘“β€˜0)
143cv 1540 . . . . . . . 8 class 𝑦
1513, 14wceq 1541 . . . . . . 7 wff (π‘“β€˜0) = 𝑦
16 c1 11110 . . . . . . . . 9 class 1
1716, 12cfv 6543 . . . . . . . 8 class (π‘“β€˜1)
1817, 14wceq 1541 . . . . . . 7 wff (π‘“β€˜1) = 𝑦
1915, 18wa 396 . . . . . 6 wff ((π‘“β€˜0) = 𝑦 ∧ (π‘“β€˜1) = 𝑦)
20 cii 24390 . . . . . . 7 class II
21 ccn 22727 . . . . . . 7 class Cn
2220, 5, 21co 7408 . . . . . 6 class (II Cn 𝑗)
2319, 11, 22crab 3432 . . . . 5 class {𝑓 ∈ (II Cn 𝑗) ∣ ((π‘“β€˜0) = 𝑦 ∧ (π‘“β€˜1) = 𝑦)}
249, 23cop 4634 . . . 4 class ⟨(Baseβ€˜ndx), {𝑓 ∈ (II Cn 𝑗) ∣ ((π‘“β€˜0) = 𝑦 ∧ (π‘“β€˜1) = 𝑦)}⟩
25 cplusg 17196 . . . . . 6 class +g
267, 25cfv 6543 . . . . 5 class (+gβ€˜ndx)
27 cpco 24515 . . . . . 6 class *𝑝
285, 27cfv 6543 . . . . 5 class (*π‘β€˜π‘—)
2926, 28cop 4634 . . . 4 class ⟨(+gβ€˜ndx), (*π‘β€˜π‘—)⟩
30 cts 17202 . . . . . 6 class TopSet
317, 30cfv 6543 . . . . 5 class (TopSetβ€˜ndx)
32 cxko 23064 . . . . . 6 class ↑ko
335, 20, 32co 7408 . . . . 5 class (𝑗 ↑ko II)
3431, 33cop 4634 . . . 4 class ⟨(TopSetβ€˜ndx), (𝑗 ↑ko II)⟩
3524, 29, 34ctp 4632 . . 3 class {⟨(Baseβ€˜ndx), {𝑓 ∈ (II Cn 𝑗) ∣ ((π‘“β€˜0) = 𝑦 ∧ (π‘“β€˜1) = 𝑦)}⟩, ⟨(+gβ€˜ndx), (*π‘β€˜π‘—)⟩, ⟨(TopSetβ€˜ndx), (𝑗 ↑ko II)⟩}
362, 3, 4, 6, 35cmpo 7410 . 2 class (𝑗 ∈ Top, 𝑦 ∈ βˆͺ 𝑗 ↦ {⟨(Baseβ€˜ndx), {𝑓 ∈ (II Cn 𝑗) ∣ ((π‘“β€˜0) = 𝑦 ∧ (π‘“β€˜1) = 𝑦)}⟩, ⟨(+gβ€˜ndx), (*π‘β€˜π‘—)⟩, ⟨(TopSetβ€˜ndx), (𝑗 ↑ko II)⟩})
371, 36wceq 1541 1 wff Ξ©1 = (𝑗 ∈ Top, 𝑦 ∈ βˆͺ 𝑗 ↦ {⟨(Baseβ€˜ndx), {𝑓 ∈ (II Cn 𝑗) ∣ ((π‘“β€˜0) = 𝑦 ∧ (π‘“β€˜1) = 𝑦)}⟩, ⟨(+gβ€˜ndx), (*π‘β€˜π‘—)⟩, ⟨(TopSetβ€˜ndx), (𝑗 ↑ko II)⟩})
Colors of variables: wff setvar class
This definition is referenced by:  om1val  24545
  Copyright terms: Public domain W3C validator