Metamath Proof Explorer


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 = n 0 , k DivRing ℙ𝕣𝕠𝕛 k freeLMod 0 n

Detailed syntax breakdown

Step Hyp Ref Expression
0 cprjspn class ℙ𝕣𝕠𝕛 n
1 vn setvar n
2 cn0 class 0
3 vk setvar k
4 cdr class DivRing
5 cprjsp class ℙ𝕣𝕠𝕛
6 3 cv setvar k
7 cfrlm class freeLMod
8 cc0 class 0
9 cfz class
10 1 cv setvar n
11 8 10 9 co class 0 n
12 6 11 7 co class k freeLMod 0 n
13 12 5 cfv class ℙ𝕣𝕠𝕛 k freeLMod 0 n
14 1 3 2 4 13 cmpo class n 0 , k DivRing ℙ𝕣𝕠𝕛 k freeLMod 0 n
15 0 14 wceq wff ℙ𝕣𝕠𝕛 n = n 0 , k DivRing ℙ𝕣𝕠𝕛 k freeLMod 0 n