Definition df-prjspn

Description: Define the n-dimensional projective space function. A projective space of dimension 1 is a projective line, and a projective space of dimension 2 is a projective plane. Compare df-ehl . This space is considered n-dimensional because the vector space ( k freeLMod ( 0 ... n ) ) is (n+1)-dimensional and the PrjSp function returns equivalence classes with respect to a linear (1-dimensional) relation. (Contributed by BJ and Steven Nguyen, 29-Apr-2023)

	Ref	Expression
Assertion	df-prjspn	$$⊢{\mathrm{\mathbb{P}𝕣𝕠𝕛}}_n=\left(n\in {\mathbb{N}}_0,k\in \mathrm{DivRing}⟼\mathrm{\mathbb{P}𝕣𝕠𝕛}\left(k\mathrm{freeLMod}\left(0\dots n\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprjspn	$$class{\mathrm{\mathbb{P}𝕣𝕠𝕛}}_n$$
1		vn	$$setvarn$$
2		cn0	$$class{\mathbb{N}}_0$$
3		vk	$$setvark$$
4		cdr	$$class\mathrm{DivRing}$$
5		cprjsp	$$class\mathrm{\mathbb{P}𝕣𝕠𝕛}$$
6	3	cv	$$setvark$$
7		cfrlm	$$class\mathrm{freeLMod}$$
8		cc0	$$class0$$
9		cfz	$$class\dots$$
10	1	cv	$$setvarn$$
11	8 10 9	co	$$class\left(0\dots n\right)$$
12	6 11 7	co	$$class\left(k\mathrm{freeLMod}\left(0\dots n\right)\right)$$
13	12 5	cfv	$$class\mathrm{\mathbb{P}𝕣𝕠𝕛}\left(k\mathrm{freeLMod}\left(0\dots n\right)\right)$$
14	1 3 2 4 13	cmpo	$$class\left(n\in {\mathbb{N}}_0,k\in \mathrm{DivRing}⟼\mathrm{\mathbb{P}𝕣𝕠𝕛}\left(k\mathrm{freeLMod}\left(0\dots n\right)\right)\right)$$
15	0 14	wceq	$$wff{\mathrm{\mathbb{P}𝕣𝕠𝕛}}_n=\left(n\in {\mathbb{N}}_0,k\in \mathrm{DivRing}⟼\mathrm{\mathbb{P}𝕣𝕠𝕛}\left(k\mathrm{freeLMod}\left(0\dots n\right)\right)\right)$$