Definition df-prjsp 43834

Description: Define the projective space function. In the bijection between 3D lines through the origin and points in the projective plane (see section comment), this is equivalent to making any two 3D points (excluding the origin) equivalent iff one is a multiple of another. Note that the meaning of "projective space" is more general than the section comment might suggest. In particular, the projective space obtained from ℝ as a ℚ-vector space is infinite-dimensional and is not of the form covered by df-prjspn 43847. Compare df-lsatoms 40236. (Contributed by BJ and SN, 29-Apr-2023.)

Assertion

Ref	Expression
df-prjsp	⊢ ℙroj = (𝑣 ∈ LVec ↦ ⦋((Base‘𝑣) ∖ {(0g‘𝑣)}) / 𝑏⦌(𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))}))

Distinct variable group:   𝑣,𝑏,𝑥,𝑦,𝑙

Detailed syntax breakdown of Definition df-prjsp

Step	Hyp	Ref	Expression
1		cprjsp 43833	. 2 class ℙroj
2		vv	. . 3 setvar 𝑣
3		clvec 21410	. . 3 class LVec
4		vb	. . . 4 setvar 𝑏
5	2	cv 1569	. . . . . 6 class 𝑣
6		cbs 17419	. . . . . 6 class Base
7	5, 6	cfv 6561	. . . . 5 class (Base‘𝑣)
8		c0g 17642	. . . . . . 7 class 0g
9	5, 8	cfv 6561	. . . . . 6 class (0g‘𝑣)
10	9	csn 4588	. . . . 5 class {(0g‘𝑣)}
11	7, 10	cdif 4048	. . . 4 class ((Base‘𝑣) ∖ {(0g‘𝑣)})
12	4	cv 1569	. . . . 5 class 𝑏
13		vx	. . . . . . . . 9 setvar 𝑥
14	13, 4	wel 2148	. . . . . . . 8 wff 𝑥 ∈ 𝑏
15		vy	. . . . . . . . 9 setvar 𝑦
16	15, 4	wel 2148	. . . . . . . 8 wff 𝑦 ∈ 𝑏
17	14, 16	wa 401	. . . . . . 7 wff (𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏)
18	13	cv 1569	. . . . . . . . 9 class 𝑥
19		vl	. . . . . . . . . . 11 setvar 𝑙
20	19	cv 1569	. . . . . . . . . 10 class 𝑙
21	15	cv 1569	. . . . . . . . . 10 class 𝑦
22		cvsca 17464	. . . . . . . . . . 11 class ·𝑠
23	5, 22	cfv 6561	. . . . . . . . . 10 class ( ·𝑠 ‘𝑣)
24	20, 21, 23	co 7446	. . . . . . . . 9 class (𝑙( ·𝑠 ‘𝑣)𝑦)
25	18, 24	wceq 1570	. . . . . . . 8 wff 𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦)
26		csca 17463	. . . . . . . . . 10 class Scalar
27	5, 26	cfv 6561	. . . . . . . . 9 class (Scalar‘𝑣)
28	27, 6	cfv 6561	. . . . . . . 8 class (Base‘(Scalar‘𝑣))
29	25, 19, 28	wrex 3090	. . . . . . 7 wff ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦)
30	17, 29	wa 401	. . . . . 6 wff ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))
31	30, 13, 15	copab 5171	. . . . 5 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))}
32	12, 31	cqs 8747	. . . 4 class (𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))})
33	4, 11, 32	csb 3851	. . 3 class ⦋((Base‘𝑣) ∖ {(0g‘𝑣)}) / 𝑏⦌(𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))})
34	2, 3, 33	cmpt 5190	. 2 class (𝑣 ∈ LVec ↦ ⦋((Base‘𝑣) ∖ {(0g‘𝑣)}) / 𝑏⦌(𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))}))
35	1, 34	wceq 1570	1 wff ℙroj = (𝑣 ∈ LVec ↦ ⦋((Base‘𝑣) ∖ {(0g‘𝑣)}) / 𝑏⦌(𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))}))

This definition is used by:  prjspval  43835