Metamath Proof Explorer

Definition df-om1

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)

Ref Expression
Assertion df-om1 
|- Om1 = ( 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 ^ko II ) >. } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 comi 
 |-  Om1
1 vj 
 |-  j
2 ctop 
 |-  Top
3 vy 
 |-  y
4 1 cv 
 |-  j
5 4 cuni 
 |-  U. j
6 cbs 
 |-  Base
7 cnx 
 |-  ndx
8 7 6 cfv 
 |-  ( Base ` ndx )
9 vf 
 |-  f
10 cii 
 |-  II
11 ccn 
 |-  Cn
12 10 4 11 co 
 |-  ( II Cn j )
13 9 cv 
 |-  f
14 cc0 
 |-  0
15 14 13 cfv 
 |-  ( f ` 0 )
16 3 cv 
 |-  y
17 15 16 wceq 
 |-  ( f ` 0 ) = y
18 c1 
 |-  1
19 18 13 cfv 
 |-  ( f ` 1 )
20 19 16 wceq 
 |-  ( f ` 1 ) = y
21 17 20 wa 
 |-  ( ( f ` 0 ) = y /\ ( f ` 1 ) = y )
22 21 9 12 crab 
 |-  { f e. ( II Cn j ) | ( ( f ` 0 ) = y /\ ( f ` 1 ) = y ) }
23 8 22 cop 
 |-  <. ( Base ` ndx ) , { f e. ( II Cn j ) | ( ( f ` 0 ) = y /\ ( f ` 1 ) = y ) } >.
24 cplusg 
 |-  +g
25 7 24 cfv 
 |-  ( +g ` ndx )
26 cpco 
 |-  *p
27 4 26 cfv 
 |-  ( *p ` j )
28 25 27 cop 
 |-  <. ( +g ` ndx ) , ( *p ` j ) >.
29 cts 
 |-  TopSet
30 7 29 cfv 
 |-  ( TopSet ` ndx )
31 cxko 
 |-  ^ko
32 4 10 31 co 
 |-  ( j ^ko II )
33 30 32 cop 
 |-  <. ( TopSet ` ndx ) , ( j ^ko II ) >.
34 23 28 33 ctp 
 |-  { <. ( Base ` ndx ) , { f e. ( II Cn j ) | ( ( f ` 0 ) = y /\ ( f ` 1 ) = y ) } >. , <. ( +g ` ndx ) , ( *p ` j ) >. , <. ( TopSet ` ndx ) , ( j ^ko II ) >. }
35 1 3 2 5 34 cmpo 
 |-  ( 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 ^ko II ) >. } )
36 0 35 wceq 
 |-  Om1 = ( 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 ^ko II ) >. } )