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	$$⊢{\Omega }_1=\left(j\in \mathrm{Top},y\in \bigcup j⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{f\in \left(\mathrm{II}\mathrm{Cn}j\right)|\left(f\left(0\right)=y\wedge f\left(1\right)=y\right)\right\}⟩,⟨{+}_{\mathrm{ndx}},{*}_{𝑝}\left(j\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),j{^}_{\mathrm{ko}}\mathrm{II}⟩\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		comi	$$class{\Omega }_1$$
1		vj	$$setvarj$$
2		ctop	$$class\mathrm{Top}$$
3		vy	$$setvary$$
4	1	cv	$$setvarj$$
5	4	cuni	$$class\bigcup j$$
6		cbs	$$class\mathrm{Base}$$
7		cnx	$$class\mathrm{ndx}$$
8	7 6	cfv	$$class{\mathrm{Base}}_{\mathrm{ndx}}$$
9		vf	$$setvarf$$
10		cii	$$class\mathrm{II}$$
11		ccn	$$class\mathrm{Cn}$$
12	10 4 11	co	$$class\left(\mathrm{II}\mathrm{Cn}j\right)$$
13	9	cv	$$setvarf$$
14		cc0	$$class0$$
15	14 13	cfv	$$classf\left(0\right)$$
16	3	cv	$$setvary$$
17	15 16	wceq	$$wfff\left(0\right)=y$$
18		c1	$$class1$$
19	18 13	cfv	$$classf\left(1\right)$$
20	19 16	wceq	$$wfff\left(1\right)=y$$
21	17 20	wa	$$wff\left(f\left(0\right)=y\wedge f\left(1\right)=y\right)$$
22	21 9 12	crab	$$class\left\{f\in \left(\mathrm{II}\mathrm{Cn}j\right)|\left(f\left(0\right)=y\wedge f\left(1\right)=y\right)\right\}$$
23	8 22	cop	$$class⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{f\in \left(\mathrm{II}\mathrm{Cn}j\right)|\left(f\left(0\right)=y\wedge f\left(1\right)=y\right)\right\}⟩$$
24		cplusg	$$class{+}_{𝑔}$$
25	7 24	cfv	$$class{+}_{\mathrm{ndx}}$$
26		cpco	$$class{*}_{𝑝}$$
27	4 26	cfv	$$class{*}_{𝑝}\left(j\right)$$
28	25 27	cop	$$class⟨{+}_{\mathrm{ndx}},{*}_{𝑝}\left(j\right)⟩$$
29		cts	$$class\mathrm{TopSet}$$
30	7 29	cfv	$$class\mathrm{TopSet}\left(\mathrm{ndx}\right)$$
31		cxko	$$class{^}_{\mathrm{ko}}$$
32	4 10 31	co	$$class\left(j{^}_{\mathrm{ko}}\mathrm{II}\right)$$
33	30 32	cop	$$class⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),j{^}_{\mathrm{ko}}\mathrm{II}⟩$$
34	23 28 33	ctp	$$class\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{f\in \left(\mathrm{II}\mathrm{Cn}j\right)|\left(f\left(0\right)=y\wedge f\left(1\right)=y\right)\right\}⟩,⟨{+}_{\mathrm{ndx}},{*}_{𝑝}\left(j\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),j{^}_{\mathrm{ko}}\mathrm{II}⟩\right\}$$
35	1 3 2 5 34	cmpo	$$class\left(j\in \mathrm{Top},y\in \bigcup j⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{f\in \left(\mathrm{II}\mathrm{Cn}j\right)|\left(f\left(0\right)=y\wedge f\left(1\right)=y\right)\right\}⟩,⟨{+}_{\mathrm{ndx}},{*}_{𝑝}\left(j\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),j{^}_{\mathrm{ko}}\mathrm{II}⟩\right\}\right)$$
36	0 35	wceq	$$wff{\Omega }_1=\left(j\in \mathrm{Top},y\in \bigcup j⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{f\in \left(\mathrm{II}\mathrm{Cn}j\right)|\left(f\left(0\right)=y\wedge f\left(1\right)=y\right)\right\}⟩,⟨{+}_{\mathrm{ndx}},{*}_{𝑝}\left(j\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),j{^}_{\mathrm{ko}}\mathrm{II}⟩\right\}\right)$$