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 | |- PrjSpn = ( n e. NN0 , k e. DivRing |-> ( PrjSp ` ( k freeLMod ( 0 ... n ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cprjspn | |- PrjSpn |
|
| 1 | vn | |- n |
|
| 2 | cn0 | |- NN0 |
|
| 3 | vk | |- k |
|
| 4 | cdr | |- DivRing |
|
| 5 | cprjsp | |- PrjSp |
|
| 6 | 3 | cv | |- k |
| 7 | cfrlm | |- freeLMod |
|
| 8 | cc0 | |- 0 |
|
| 9 | cfz | |- ... |
|
| 10 | 1 | cv | |- n |
| 11 | 8 10 9 | co | |- ( 0 ... n ) |
| 12 | 6 11 7 | co | |- ( k freeLMod ( 0 ... n ) ) |
| 13 | 12 5 | cfv | |- ( PrjSp ` ( k freeLMod ( 0 ... n ) ) ) |
| 14 | 1 3 2 4 13 | cmpo | |- ( n e. NN0 , k e. DivRing |-> ( PrjSp ` ( k freeLMod ( 0 ... n ) ) ) ) |
| 15 | 0 14 | wceq | |- PrjSpn = ( n e. NN0 , k e. DivRing |-> ( PrjSp ` ( k freeLMod ( 0 ... n ) ) ) ) |