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	⊢ Ω1 = ( 𝑗 ∈ Top , 𝑦 ∈ ∪ 𝑗 ↦ { ⟨ ( Base ‘ ndx ) , { 𝑓 ∈ ( II Cn 𝑗 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ⟩ , ⟨ ( +g ‘ ndx ) , ( *𝑝 ‘ 𝑗 ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝑗 ↑ko II ) ⟩ } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		comi	⊢ Ω1
1		vj	⊢ 𝑗
2		ctop	⊢ Top
3		vy	⊢ 𝑦
4	1	cv	⊢ 𝑗
5	4	cuni	⊢ ∪ 𝑗
6		cbs	⊢ Base
7		cnx	⊢ ndx
8	7 6	cfv	⊢ ( Base ‘ ndx )
9		vf	⊢ 𝑓
10		cii	⊢ II
11		ccn	⊢ Cn
12	10 4 11	co	⊢ ( II Cn 𝑗 )
13	9	cv	⊢ 𝑓
14		cc0	⊢ 0
15	14 13	cfv	⊢ ( 𝑓 ‘ 0 )
16	3	cv	⊢ 𝑦
17	15 16	wceq	⊢ ( 𝑓 ‘ 0 ) = 𝑦
18		c1	⊢ 1
19	18 13	cfv	⊢ ( 𝑓 ‘ 1 )
20	19 16	wceq	⊢ ( 𝑓 ‘ 1 ) = 𝑦
21	17 20	wa	⊢ ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑦 )
22	21 9 12	crab	⊢ { 𝑓 ∈ ( II Cn 𝑗 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) }
23	8 22	cop	⊢ ⟨ ( Base ‘ ndx ) , { 𝑓 ∈ ( II Cn 𝑗 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ⟩
24		cplusg	⊢ +g
25	7 24	cfv	⊢ ( +g ‘ ndx )
26		cpco	⊢ *𝑝
27	4 26	cfv	⊢ ( *𝑝 ‘ 𝑗 )
28	25 27	cop	⊢ ⟨ ( +g ‘ ndx ) , ( *𝑝 ‘ 𝑗 ) ⟩
29		cts	⊢ TopSet
30	7 29	cfv	⊢ ( TopSet ‘ ndx )
31		cxko	⊢ ↑ko
32	4 10 31	co	⊢ ( 𝑗 ↑ko II )
33	30 32	cop	⊢ ⟨ ( TopSet ‘ ndx ) , ( 𝑗 ↑ko II ) ⟩
34	23 28 33	ctp	⊢ { ⟨ ( Base ‘ ndx ) , { 𝑓 ∈ ( II Cn 𝑗 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ⟩ , ⟨ ( +g ‘ ndx ) , ( *𝑝 ‘ 𝑗 ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝑗 ↑ko II ) ⟩ }
35	1 3 2 5 34	cmpo	⊢ ( 𝑗 ∈ Top , 𝑦 ∈ ∪ 𝑗 ↦ { ⟨ ( Base ‘ ndx ) , { 𝑓 ∈ ( II Cn 𝑗 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ⟩ , ⟨ ( +g ‘ ndx ) , ( *𝑝 ‘ 𝑗 ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝑗 ↑ko II ) ⟩ } )
36	0 35	wceq	⊢ Ω1 = ( 𝑗 ∈ Top , 𝑦 ∈ ∪ 𝑗 ↦ { ⟨ ( Base ‘ ndx ) , { 𝑓 ∈ ( II Cn 𝑗 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ⟩ , ⟨ ( +g ‘ ndx ) , ( *𝑝 ‘ 𝑗 ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝑗 ↑ko II ) ⟩ } )