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

Definition df-om1 18504
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  |-  Om 1  =  ( j  e. 
Top ,  y  e.  U. j  |->  { <. ( Base `  ndx ) ,  { f  e.  ( II  Cn  j )  |  ( ( f `
 0 )  =  y  /\  ( f `
 1 )  =  y ) } >. , 
<. ( +g  `  ndx ) ,  ( *p `  j ) >. ,  <. (TopSet `  ndx ) ,  ( j  ^ k o  II ) >. } )
Distinct variable group:    f, j, y

Detailed syntax breakdown of Definition df-om1
StepHypRef Expression
1 comi 18499 . 2  class  Om 1
2 vj . . 3  set  j
3 vy . . 3  set  y
4 ctop 16631 . . 3  class  Top
52cv 1622 . . . 4  class  j
65cuni 3827 . . 3  class  U. j
7 cnx 13145 . . . . . 6  class  ndx
8 cbs 13148 . . . . . 6  class  Base
97, 8cfv 5255 . . . . 5  class  ( Base `  ndx )
10 cc0 8737 . . . . . . . . 9  class  0
11 vf . . . . . . . . . 10  set  f
1211cv 1622 . . . . . . . . 9  class  f
1310, 12cfv 5255 . . . . . . . 8  class  ( f `
 0 )
143cv 1622 . . . . . . . 8  class  y
1513, 14wceq 1623 . . . . . . 7  wff  ( f `
 0 )  =  y
16 c1 8738 . . . . . . . . 9  class  1
1716, 12cfv 5255 . . . . . . . 8  class  ( f `
 1 )
1817, 14wceq 1623 . . . . . . 7  wff  ( f `
 1 )  =  y
1915, 18wa 358 . . . . . 6  wff  ( ( f `  0 )  =  y  /\  (
f `  1 )  =  y )
20 cii 18379 . . . . . . 7  class  II
21 ccn 16954 . . . . . . 7  class  Cn
2220, 5, 21co 5858 . . . . . 6  class  ( II 
Cn  j )
2319, 11, 22crab 2547 . . . . 5  class  { f  e.  ( II  Cn  j )  |  ( ( f `  0
)  =  y  /\  ( f `  1
)  =  y ) }
249, 23cop 3643 . . . 4  class  <. ( Base `  ndx ) ,  { f  e.  ( II  Cn  j )  |  ( ( f `
 0 )  =  y  /\  ( f `
 1 )  =  y ) } >.
25 cplusg 13208 . . . . . 6  class  +g
267, 25cfv 5255 . . . . 5  class  ( +g  ` 
ndx )
27 cpco 18498 . . . . . 6  class  *p
285, 27cfv 5255 . . . . 5  class  ( *p
`  j )
2926, 28cop 3643 . . . 4  class  <. ( +g  `  ndx ) ,  ( *p `  j
) >.
30 cts 13214 . . . . . 6  class TopSet
317, 30cfv 5255 . . . . 5  class  (TopSet `  ndx )
32 cxko 17256 . . . . . 6  class  ^ k o
335, 20, 32co 5858 . . . . 5  class  ( j  ^ k o  II )
3431, 33cop 3643 . . . 4  class  <. (TopSet ` 
ndx ) ,  ( j  ^ k o  II ) >.
3524, 29, 34ctp 3642 . . 3  class  { <. (
Base `  ndx ) ,  { f  e.  ( II  Cn  j )  |  ( ( f `
 0 )  =  y  /\  ( f `
 1 )  =  y ) } >. , 
<. ( +g  `  ndx ) ,  ( *p `  j ) >. ,  <. (TopSet `  ndx ) ,  ( j  ^ k o  II ) >. }
362, 3, 4, 6, 35cmpt2 5860 . 2  class  ( j  e.  Top ,  y  e.  U. j  |->  {
<. ( Base `  ndx ) ,  { f  e.  ( II  Cn  j
)  |  ( ( f `  0 )  =  y  /\  (
f `  1 )  =  y ) }
>. ,  <. ( +g  ` 
ndx ) ,  ( *p `  j )
>. ,  <. (TopSet `  ndx ) ,  ( j  ^ k o  II ) >. } )
371, 36wceq 1623 1  wff  Om 1  =  ( j  e. 
Top ,  y  e.  U. j  |->  { <. ( Base `  ndx ) ,  { f  e.  ( II  Cn  j )  |  ( ( f `
 0 )  =  y  /\  ( f `
 1 )  =  y ) } >. , 
<. ( +g  `  ndx ) ,  ( *p `  j ) >. ,  <. (TopSet `  ndx ) ,  ( j  ^ k o  II ) >. } )
Colors of variables: wff set class
This definition is referenced by:  om1val  18528
  Copyright terms: Public domain W3C validator