Definition df-om1 19033

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 19028	. 2 class Om 1
2		vj	. . 3 set j
3		vy	. . 3 set y
4		ctop 16960	. . 3 class Top
5	2	cv 1652	. . . 4 class j
6	5	cuni 4017	. . 3 class U. j
7		cnx 13468	. . . . . 6 class ndx
8		cbs 13471	. . . . . 6 class Base
9	7, 8	cfv 5456	. . . . 5 class ( Base ` ndx )
10		cc0 8992	. . . . . . . . 9 class 0
11		vf	. . . . . . . . . 10 set f
12	11	cv 1652	. . . . . . . . 9 class f
13	10, 12	cfv 5456	. . . . . . . 8 class ( f ` 0 )
14	3	cv 1652	. . . . . . . 8 class y
15	13, 14	wceq 1653	. . . . . . 7 wff ( f ` 0 ) = y
16		c1 8993	. . . . . . . . 9 class 1
17	16, 12	cfv 5456	. . . . . . . 8 class ( f ` 1 )
18	17, 14	wceq 1653	. . . . . . 7 wff ( f ` 1 ) = y
19	15, 18	wa 360	. . . . . 6 wff ( ( f ` 0 ) = y /\ ( f ` 1 ) = y )
20		cii 18907	. . . . . . 7 class II
21		ccn 17290	. . . . . . 7 class Cn
22	20, 5, 21	co 6083	. . . . . 6 class ( II Cn j )
23	19, 11, 22	crab 2711	. . . . 5 class { f e. ( II Cn j ) | ( ( f ` 0 ) = y /\ ( f ` 1 ) = y ) }
24	9, 23	cop 3819	. . . 4 class <. ( Base ` ndx ) , { f e. ( II Cn j ) | ( ( f ` 0 ) = y /\ ( f ` 1 ) = y ) } >.
25		cplusg 13531	. . . . . 6 class +g
26	7, 25	cfv 5456	. . . . 5 class ( +g ` ndx )
27		cpco 19027	. . . . . 6 class *p
28	5, 27	cfv 5456	. . . . 5 class ( *p ` j )
29	26, 28	cop 3819	. . . 4 class <. ( +g ` ndx ) , ( *p ` j ) >.
30		cts 13537	. . . . . 6 class TopSet
31	7, 30	cfv 5456	. . . . 5 class (TopSet ` ndx )
32		cxko 17595	. . . . . 6 class ^ k o
33	5, 20, 32	co 6083	. . . . 5 class ( j ^ k o II )
34	31, 33	cop 3819	. . . 4 class <. (TopSet ` ndx ) , ( j ^ k o II ) >.
35	24, 29, 34	ctp 3818	. . 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 6085	. 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 1653	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  19057