Definition df-prjsp 43035

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 39422. (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 43034	. 2 class ℙ𝕣𝕠𝕛
2		vv	. . 3 setvar 𝑣
3		clvec 21097	. . 3 class LVec
4		vb	. . . 4 setvar 𝑏
5	2	cv 1541	. . . . . 6 class 𝑣
6		cbs 17179	. . . . . 6 class Base
7	5, 6	cfv 6498	. . . . 5 class (Base‘𝑣)
8		c0g 17402	. . . . . . 7 class 0g
9	5, 8	cfv 6498	. . . . . 6 class (0g‘𝑣)
10	9	csn 4567	. . . . 5 class {(0g‘𝑣)}
11	7, 10	cdif 3886	. . . 4 class ((Base‘𝑣) ∖ {(0g‘𝑣)})
12	4	cv 1541	. . . . 5 class 𝑏
13		vx	. . . . . . . . 9 setvar 𝑥
14	13, 4	wel 2115	. . . . . . . 8 wff 𝑥 ∈ 𝑏
15		vy	. . . . . . . . 9 setvar 𝑦
16	15, 4	wel 2115	. . . . . . . 8 wff 𝑦 ∈ 𝑏
17	14, 16	wa 395	. . . . . . 7 wff (𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏)
18	13	cv 1541	. . . . . . . . 9 class 𝑥
19		vl	. . . . . . . . . . 11 setvar 𝑙
20	19	cv 1541	. . . . . . . . . 10 class 𝑙
21	15	cv 1541	. . . . . . . . . 10 class 𝑦
22		cvsca 17224	. . . . . . . . . . 11 class ·𝑠
23	5, 22	cfv 6498	. . . . . . . . . 10 class ( ·𝑠 ‘𝑣)
24	20, 21, 23	co 7367	. . . . . . . . 9 class (𝑙( ·𝑠 ‘𝑣)𝑦)
25	18, 24	wceq 1542	. . . . . . . 8 wff 𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦)
26		csca 17223	. . . . . . . . . 10 class Scalar
27	5, 26	cfv 6498	. . . . . . . . 9 class (Scalar‘𝑣)
28	27, 6	cfv 6498	. . . . . . . 8 class (Base‘(Scalar‘𝑣))
29	25, 19, 28	wrex 3061	. . . . . . 7 wff ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦)
30	17, 29	wa 395	. . . . . 6 wff ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))
31	30, 13, 15	copab 5147	. . . . 5 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))}
32	12, 31	cqs 8642	. . . 4 class (𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))})
33	4, 11, 32	csb 3837	. . 3 class ⦋((Base‘𝑣) ∖ {(0g‘𝑣)}) / 𝑏⦌(𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))})
34	2, 3, 33	cmpt 5166	. 2 class (𝑣 ∈ LVec ↦ ⦋((Base‘𝑣) ∖ {(0g‘𝑣)}) / 𝑏⦌(𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))}))
35	1, 34	wceq 1542	1 wff ℙ𝕣𝕠𝕛 = (𝑣 ∈ LVec ↦ ⦋((Base‘𝑣) ∖ {(0g‘𝑣)}) / 𝑏⦌(𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))}))

This definition is referenced by:  prjspval  43036