Definition df-prjsp 43723

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 43736. Compare df-lsatoms 40126. (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 43722	. 2 class ℙroj
2		vv	. . 3 setvar 𝑣
3		clvec 21382	. . 3 class LVec
4		vb	. . . 4 setvar 𝑏
5	2	cv 1568	. . . . . 6 class 𝑣
6		cbs 17392	. . . . . 6 class Base
7	5, 6	cfv 6538	. . . . 5 class (Base‘𝑣)
8		c0g 17615	. . . . . . 7 class 0g
9	5, 8	cfv 6538	. . . . . 6 class (0g‘𝑣)
10	9	csn 4584	. . . . 5 class {(0g‘𝑣)}
11	7, 10	cdif 4045	. . . 4 class ((Base‘𝑣) ∖ {(0g‘𝑣)})
12	4	cv 1568	. . . . 5 class 𝑏
13		vx	. . . . . . . . 9 setvar 𝑥
14	13, 4	wel 2145	. . . . . . . 8 wff 𝑥 ∈ 𝑏
15		vy	. . . . . . . . 9 setvar 𝑦
16	15, 4	wel 2145	. . . . . . . 8 wff 𝑦 ∈ 𝑏
17	14, 16	wa 401	. . . . . . 7 wff (𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏)
18	13	cv 1568	. . . . . . . . 9 class 𝑥
19		vl	. . . . . . . . . . 11 setvar 𝑙
20	19	cv 1568	. . . . . . . . . 10 class 𝑙
21	15	cv 1568	. . . . . . . . . 10 class 𝑦
22		cvsca 17437	. . . . . . . . . . 11 class ·𝑠
23	5, 22	cfv 6538	. . . . . . . . . 10 class ( ·𝑠 ‘𝑣)
24	20, 21, 23	co 7420	. . . . . . . . 9 class (𝑙( ·𝑠 ‘𝑣)𝑦)
25	18, 24	wceq 1569	. . . . . . . 8 wff 𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦)
26		csca 17436	. . . . . . . . . 10 class Scalar
27	5, 26	cfv 6538	. . . . . . . . 9 class (Scalar‘𝑣)
28	27, 6	cfv 6538	. . . . . . . 8 class (Base‘(Scalar‘𝑣))
29	25, 19, 28	wrex 3086	. . . . . . 7 wff ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦)
30	17, 29	wa 401	. . . . . 6 wff ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))
31	30, 13, 15	copab 5166	. . . . 5 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))}
32	12, 31	cqs 8719	. . . 4 class (𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))})
33	4, 11, 32	csb 3846	. . 3 class ⦋((Base‘𝑣) ∖ {(0g‘𝑣)}) / 𝑏⦌(𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))})
34	2, 3, 33	cmpt 5185	. 2 class (𝑣 ∈ LVec ↦ ⦋((Base‘𝑣) ∖ {(0g‘𝑣)}) / 𝑏⦌(𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))}))
35	1, 34	wceq 1569	1 wff ℙroj = (𝑣 ∈ LVec ↦ ⦋((Base‘𝑣) ∖ {(0g‘𝑣)}) / 𝑏⦌(𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))}))

This definition is used by:  prjspval  43724