Definition df-prjspn 43737

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 25713. This space is considered n-dimensional because the vector space (𝑘 freeLMod (0...𝑛)) is (n+1)-dimensional and the ℙroj 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	⊢ ℙrojn = (𝑛 ∈ ℕ0, 𝑘 ∈ DivRing ↦ (ℙroj‘(𝑘 freeLMod (0...𝑛))))

Distinct variable group:   𝑘,𝑛

Detailed syntax breakdown of Definition df-prjspn

Step	Hyp	Ref	Expression
1		cprjspn 43736	. 2 class ℙrojn
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12610	. . 3 class ℕ0
5		cdr 20986	. . 3 class DivRing
6	3	cv 1568	. . . . 5 class 𝑘
7		cc0 11204	. . . . . 6 class 0
8	2	cv 1568	. . . . . 6 class 𝑛
9		cfz 13643	. . . . . 6 class ...
10	7, 8, 9	co 7421	. . . . 5 class (0...𝑛)
11		cfrlm 22058	. . . . 5 class freeLMod
12	6, 10, 11	co 7421	. . . 4 class (𝑘 freeLMod (0...𝑛))
13		cprjsp 43723	. . . 4 class ℙroj
14	12, 13	cfv 6539	. . 3 class (ℙroj‘(𝑘 freeLMod (0...𝑛)))
15	2, 3, 4, 5, 14	cmpo 7423	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ DivRing ↦ (ℙroj‘(𝑘 freeLMod (0...𝑛))))
16	1, 15	wceq 1569	1 wff ℙrojn = (𝑛 ∈ ℕ0, 𝑘 ∈ DivRing ↦ (ℙroj‘(𝑘 freeLMod (0...𝑛))))

This definition is used by:  prjspnval  43738