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	⊢ ℙ𝕣𝕠𝕛n = ( 𝑛 ∈ ℕ0 , 𝑘 ∈ DivRing ↦ ( ℙ𝕣𝕠𝕛 ‘ ( 𝑘 freeLMod ( 0 ... 𝑛 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprjspn	⊢ ℙ𝕣𝕠𝕛n
1		vn	⊢ 𝑛
2		cn0	⊢ ℕ0
3		vk	⊢ 𝑘
4		cdr	⊢ DivRing
5		cprjsp	⊢ ℙ𝕣𝕠𝕛
6	3	cv	⊢ 𝑘
7		cfrlm	⊢ freeLMod
8		cc0	⊢ 0
9		cfz	⊢ ...
10	1	cv	⊢ 𝑛
11	8 10 9	co	⊢ ( 0 ... 𝑛 )
12	6 11 7	co	⊢ ( 𝑘 freeLMod ( 0 ... 𝑛 ) )
13	12 5	cfv	⊢ ( ℙ𝕣𝕠𝕛 ‘ ( 𝑘 freeLMod ( 0 ... 𝑛 ) ) )
14	1 3 2 4 13	cmpo	⊢ ( 𝑛 ∈ ℕ0 , 𝑘 ∈ DivRing ↦ ( ℙ𝕣𝕠𝕛 ‘ ( 𝑘 freeLMod ( 0 ... 𝑛 ) ) ) )
15	0 14	wceq	⊢ ℙ𝕣𝕠𝕛n = ( 𝑛 ∈ ℕ0 , 𝑘 ∈ DivRing ↦ ( ℙ𝕣𝕠𝕛 ‘ ( 𝑘 freeLMod ( 0 ... 𝑛 ) ) ) )