df-pin - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-pin		Structured version Visualization version Unicode version

Definition df-pin 22809

Description: Define the n-th homotopy group, which is formed by taking the

-th loop space and forming the quotient under the relation of path homotopy equivalence in the base space of the

-th loop space, which is the

-th loop space. For

, since this is not well-defined we replace this relation with the path-connectedness relation, so that the

-th homotopy group is the set of path components of

. (Since the

-th loop space does not have a group operation, neither does the

-th homotopy group, but the rest are genuine groups.) (Contributed by Mario Carneiro, 11-Feb-2015.)

**Assertion**
Ref	Expression
df-pin	_s $/\$

**Detailed syntax breakdown of Definition df-pin**
Step	Hyp	Ref	Expression
1		cpin 22804	. 2
2		vj	. . 3
3		vp	. . 3
4		ctop 20698	. . 3
5	2	cv 1482	. . . 4
6	5	cuni 4436	. . 3
7		vn	. . . 4
8		cn0 11292	. . . 4
9	7	cv 1482	. . . . . . 7
10	3	cv 1482	. . . . . . . 8
11		comn 22802	. . . . . . . 8
12	5, 10, 11	co 6650	. . . . . . 7
13	9, 12	cfv 5888	. . . . . 6
14		c1st 7166	. . . . . 6
15	13, 14	cfv 5888	. . . . 5
16		cc0 9936	. . . . . . 7
17	9, 16	wceq 1483	. . . . . 6
18		vf	. . . . . . . . . . . 12
19	18	cv 1482	. . . . . . . . . . 11
20	16, 19	cfv 5888	. . . . . . . . . 10
21		vx	. . . . . . . . . . 11
22	21	cv 1482	. . . . . . . . . 10
23	20, 22	wceq 1483	. . . . . . . . 9
24		c1 9937	. . . . . . . . . . 11
25	24, 19	cfv 5888	. . . . . . . . . 10
26		vy	. . . . . . . . . . 11
27	26	cv 1482	. . . . . . . . . 10
28	25, 27	wceq 1483	. . . . . . . . 9
29	23, 28	wa 384	. . . . . . . 8 $/\$
30		cii 22678	. . . . . . . . 9
31		ccn 21028	. . . . . . . . 9
32	30, 5, 31	co 6650	. . . . . . . 8
33	29, 18, 32	wrex 2913	. . . . . . 7 $/\$
34	33, 21, 26	copab 4712	. . . . . 6 $/\$
35		cmin 10266	. . . . . . . . . . 11
36	9, 24, 35	co 6650	. . . . . . . . . 10
37	36, 12	cfv 5888	. . . . . . . . 9
38	37, 14	cfv 5888	. . . . . . . 8
39		ctopn 16082	. . . . . . . 8
40	38, 39	cfv 5888	. . . . . . 7
41		cphtpc 22768	. . . . . . 7
42	40, 41	cfv 5888	. . . . . 6
43	17, 34, 42	cif 4086	. . . . 5 $/\$
44		cqus 16165	. . . . 5 _s
45	15, 43, 44	co 6650	. . . 4 _s $/\$
46	7, 8, 45	cmpt 4729	. . 3 _s $/\$
47	2, 3, 4, 6, 46	cmpt2 6652	. 2 _s $/\$
48	1, 47	wceq 1483	1 _s $/\$

Colors of variables: wff setvar class

This definition is referenced by: (None)