Definition df-om1 22806

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	|- 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 ) >. } )

Distinct variable group:   f, j, y

Detailed syntax breakdown of Definition df-om1

Step	Hyp	Ref	Expression
1		comi 22801	. 2 class Om1
2		vj	. . 3 setvar j
3		vy	. . 3 setvar y
4		ctop 20698	. . 3 class Top
5	2	cv 1482	. . . 4 class j
6	5	cuni 4436	. . 3 class U. j
7		cnx 15854	. . . . . 6 class ndx
8		cbs 15857	. . . . . 6 class Base
9	7, 8	cfv 5888	. . . . 5 class ( Base ` ndx )
10		cc0 9936	. . . . . . . . 9 class 0
11		vf	. . . . . . . . . 10 setvar f
12	11	cv 1482	. . . . . . . . 9 class f
13	10, 12	cfv 5888	. . . . . . . 8 class ( f ` 0 )
14	3	cv 1482	. . . . . . . 8 class y
15	13, 14	wceq 1483	. . . . . . 7 wff ( f ` 0 ) = y
16		c1 9937	. . . . . . . . 9 class 1
17	16, 12	cfv 5888	. . . . . . . 8 class ( f ` 1 )
18	17, 14	wceq 1483	. . . . . . 7 wff ( f ` 1 ) = y
19	15, 18	wa 384	. . . . . 6 wff ( ( f ` 0 ) = y /\ ( f ` 1 ) = y )
20		cii 22678	. . . . . . 7 class II
21		ccn 21028	. . . . . . 7 class Cn
22	20, 5, 21	co 6650	. . . . . 6 class ( II Cn j )
23	19, 11, 22	crab 2916	. . . . 5 class { f e. ( II Cn j ) | ( ( f ` 0 ) = y /\ ( f ` 1 ) = y ) }
24	9, 23	cop 4183	. . . 4 class <. ( Base ` ndx ) , { f e. ( II Cn j ) | ( ( f ` 0 ) = y /\ ( f ` 1 ) = y ) } >.
25		cplusg 15941	. . . . . 6 class +g
26	7, 25	cfv 5888	. . . . 5 class ( +g ` ndx )
27		cpco 22800	. . . . . 6 class *p
28	5, 27	cfv 5888	. . . . 5 class ( *p ` j )
29	26, 28	cop 4183	. . . 4 class <. ( +g ` ndx ) , ( *p ` j ) >.
30		cts 15947	. . . . . 6 class TopSet
31	7, 30	cfv 5888	. . . . 5 class (TopSet ` ndx )
32		cxko 21364	. . . . . 6 class ^ko
33	5, 20, 32	co 6650	. . . . 5 class ( j ^ko II )
34	31, 33	cop 4183	. . . 4 class <. (TopSet ` ndx ) , ( j ^ko II ) >.
35	24, 29, 34	ctp 4181	. . 3 class { <. ( Base ` ndx ) , { f e. ( II Cn j ) | ( ( f ` 0 ) = y /\ ( f ` 1 ) = y ) } >. , <. ( +g ` ndx ) , ( *p ` j ) >. , <. (TopSet ` ndx ) , ( j ^ko II ) >. }
36	2, 3, 4, 6, 35	cmpt2 6652	. 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 ^ko II ) >. } )
37	1, 36	wceq 1483	1 wff 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 ) >. } )

This definition is referenced by:  om1val  22830