Definition df-om1 18984

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

Step	Hyp	Ref	Expression
1		comi 18979	. 2 class Om 1
2		vj	. . 3 set j
3		vy	. . 3 set y
4		ctop 16913	. . 3 class Top
5	2	cv 1648	. . . 4 class j
6	5	cuni 3975	. . 3 class U. j
7		cnx 13421	. . . . . 6 class ndx
8		cbs 13424	. . . . . 6 class Base
9	7, 8	cfv 5413	. . . . 5 class ( Base ` ndx )
10		cc0 8946	. . . . . . . . 9 class 0
11		vf	. . . . . . . . . 10 set f
12	11	cv 1648	. . . . . . . . 9 class f
13	10, 12	cfv 5413	. . . . . . . 8 class ( f ` 0 )
14	3	cv 1648	. . . . . . . 8 class y
15	13, 14	wceq 1649	. . . . . . 7 wff ( f ` 0 ) = y
16		c1 8947	. . . . . . . . 9 class 1
17	16, 12	cfv 5413	. . . . . . . 8 class ( f ` 1 )
18	17, 14	wceq 1649	. . . . . . 7 wff ( f ` 1 ) = y
19	15, 18	wa 359	. . . . . 6 wff ( ( f ` 0 ) = y /\ ( f ` 1 ) = y )
20		cii 18858	. . . . . . 7 class II
21		ccn 17242	. . . . . . 7 class Cn
22	20, 5, 21	co 6040	. . . . . 6 class ( II Cn j )
23	19, 11, 22	crab 2670	. . . . 5 class { f e. ( II Cn j ) | ( ( f ` 0 ) = y /\ ( f ` 1 ) = y ) }
24	9, 23	cop 3777	. . . 4 class <. ( Base ` ndx ) , { f e. ( II Cn j ) | ( ( f ` 0 ) = y /\ ( f ` 1 ) = y ) } >.
25		cplusg 13484	. . . . . 6 class +g
26	7, 25	cfv 5413	. . . . 5 class ( +g ` ndx )
27		cpco 18978	. . . . . 6 class *p
28	5, 27	cfv 5413	. . . . 5 class ( *p ` j )
29	26, 28	cop 3777	. . . 4 class <. ( +g ` ndx ) , ( *p ` j ) >.
30		cts 13490	. . . . . 6 class TopSet
31	7, 30	cfv 5413	. . . . 5 class (TopSet ` ndx )
32		cxko 17546	. . . . . 6 class ^ k o
33	5, 20, 32	co 6040	. . . . 5 class ( j ^ k o II )
34	31, 33	cop 3777	. . . 4 class <. (TopSet ` ndx ) , ( j ^ k o II ) >.
35	24, 29, 34	ctp 3776	. . 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 ) >. }
36	2, 3, 4, 6, 35	cmpt2 6042	. 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 ) >. } )
37	1, 36	wceq 1649	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 ) >. } )

This definition is referenced by:  om1val  19008