Definition df-prjsp 43375

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. This definition does not quite give all the properties needed, since the scalars of a left vector space can be "less dense" than the vectors (for example, making equivalent rational multiples of real numbers). Compare df-lsatoms 39791. (Contributed by BJ and SN, 29-Apr-2023.)

Assertion

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

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

Detailed syntax breakdown of Definition df-prjsp

Step	Hyp	Ref	Expression
1		cprjsp 43374	. 2 class ℙ𝕣𝕠𝕛
2		vv	. . 3 setvar 𝑣
3		clvec 21260	. . 3 class LVec
4		vb	. . . 4 setvar 𝑏
5	2	cv 1569	. . . . . 6 class 𝑣
6		cbs 17294	. . . . . 6 class Base
7	5, 6	cfv 6543	. . . . 5 class (Base‘𝑣)
8		c0g 17517	. . . . . . 7 class 0g
9	5, 8	cfv 6543	. . . . . 6 class (0g‘𝑣)
10	9	csn 4594	. . . . 5 class {(0g‘𝑣)}
11	7, 10	cdif 3905	. . . 4 class ((Base‘𝑣) ∖ {(0g‘𝑣)})
12	4	cv 1569	. . . . 5 class 𝑏
13		vx	. . . . . . . . 9 setvar 𝑥
14	13, 4	wel 2147	. . . . . . . 8 wff 𝑥 ∈ 𝑏
15		vy	. . . . . . . . 9 setvar 𝑦
16	15, 4	wel 2147	. . . . . . . 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 17339	. . . . . . . . . . 11 class ·𝑠
23	5, 22	cfv 6543	. . . . . . . . . 10 class ( ·𝑠 ‘𝑣)
24	20, 21, 23	co 7423	. . . . . . . . 9 class (𝑙( ·𝑠 ‘𝑣)𝑦)
25	18, 24	wceq 1570	. . . . . . . 8 wff 𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦)
26		csca 17338	. . . . . . . . . 10 class Scalar
27	5, 26	cfv 6543	. . . . . . . . 9 class (Scalar‘𝑣)
28	27, 6	cfv 6543	. . . . . . . 8 class (Base‘(Scalar‘𝑣))
29	25, 19, 28	wrex 3092	. . . . . . 7 wff ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦)
30	17, 29	wa 401	. . . . . 6 wff ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))
31	30, 13, 15	copab 5178	. . . . 5 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))}
32	12, 31	cqs 8702	. . . 4 class (𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))})
33	4, 11, 32	csb 3856	. . 3 class ⦋((Base‘𝑣) ∖ {(0g‘𝑣)}) / 𝑏⦌(𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))})
34	2, 3, 33	cmpt 5197	. 2 class (𝑣 ∈ LVec ↦ ⦋((Base‘𝑣) ∖ {(0g‘𝑣)}) / 𝑏⦌(𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))}))
35	1, 34	wceq 1570	1 wff ℙ𝕣𝕠𝕛 = (𝑣 ∈ LVec ↦ ⦋((Base‘𝑣) ∖ {(0g‘𝑣)}) / 𝑏⦌(𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))}))

This definition is used by:  prjspval  43376