Definition df-prjspn 42625

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 25420. This space is considered n-dimensional because the vector space (𝑘 freeLMod (0...𝑛)) is (n+1)-dimensional and the ℙ𝕣𝕠𝕛 function returns equivalence classes with respect to a linear (1-dimensional) relation. (Contributed by BJ and Steven Nguyen, 29-Apr-2023.)

Assertion

Ref	Expression
df-prjspn	⊢ ℙ𝕣𝕠𝕛n = (𝑛 ∈ ℕ0, 𝑘 ∈ DivRing ↦ (ℙ𝕣𝕠𝕛‘(𝑘 freeLMod (0...𝑛))))

Distinct variable group:   𝑘,𝑛

Detailed syntax breakdown of Definition df-prjspn

Step	Hyp	Ref	Expression
1		cprjspn 42624	. 2 class ℙ𝕣𝕠𝕛n
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12526	. . 3 class ℕ0
5		cdr 20729	. . 3 class DivRing
6	3	cv 1539	. . . . 5 class 𝑘
7		cc0 11155	. . . . . 6 class 0
8	2	cv 1539	. . . . . 6 class 𝑛
9		cfz 13547	. . . . . 6 class ...
10	7, 8, 9	co 7431	. . . . 5 class (0...𝑛)
11		cfrlm 21766	. . . . 5 class freeLMod
12	6, 10, 11	co 7431	. . . 4 class (𝑘 freeLMod (0...𝑛))
13		cprjsp 42611	. . . 4 class ℙ𝕣𝕠𝕛
14	12, 13	cfv 6561	. . 3 class (ℙ𝕣𝕠𝕛‘(𝑘 freeLMod (0...𝑛)))
15	2, 3, 4, 5, 14	cmpo 7433	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ DivRing ↦ (ℙ𝕣𝕠𝕛‘(𝑘 freeLMod (0...𝑛))))
16	1, 15	wceq 1540	1 wff ℙ𝕣𝕠𝕛n = (𝑛 ∈ ℕ0, 𝑘 ∈ DivRing ↦ (ℙ𝕣𝕠𝕛‘(𝑘 freeLMod (0...𝑛))))

This definition is referenced by:  prjspnval  42626