Definition df-prjsp 42612

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 38977. (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 42611	. 2 class ℙ𝕣𝕠𝕛
2		vv	. . 3 setvar 𝑣
3		clvec 21101	. . 3 class LVec
4		vb	. . . 4 setvar 𝑏
5	2	cv 1539	. . . . . 6 class 𝑣
6		cbs 17247	. . . . . 6 class Base
7	5, 6	cfv 6561	. . . . 5 class (Base‘𝑣)
8		c0g 17484	. . . . . . 7 class 0g
9	5, 8	cfv 6561	. . . . . 6 class (0g‘𝑣)
10	9	csn 4626	. . . . 5 class {(0g‘𝑣)}
11	7, 10	cdif 3948	. . . 4 class ((Base‘𝑣) ∖ {(0g‘𝑣)})
12	4	cv 1539	. . . . 5 class 𝑏
13		vx	. . . . . . . . 9 setvar 𝑥
14	13, 4	wel 2109	. . . . . . . 8 wff 𝑥 ∈ 𝑏
15		vy	. . . . . . . . 9 setvar 𝑦
16	15, 4	wel 2109	. . . . . . . 8 wff 𝑦 ∈ 𝑏
17	14, 16	wa 395	. . . . . . 7 wff (𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏)
18	13	cv 1539	. . . . . . . . 9 class 𝑥
19		vl	. . . . . . . . . . 11 setvar 𝑙
20	19	cv 1539	. . . . . . . . . 10 class 𝑙
21	15	cv 1539	. . . . . . . . . 10 class 𝑦
22		cvsca 17301	. . . . . . . . . . 11 class ·𝑠
23	5, 22	cfv 6561	. . . . . . . . . 10 class ( ·𝑠 ‘𝑣)
24	20, 21, 23	co 7431	. . . . . . . . 9 class (𝑙( ·𝑠 ‘𝑣)𝑦)
25	18, 24	wceq 1540	. . . . . . . 8 wff 𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦)
26		csca 17300	. . . . . . . . . 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 3070	. . . . . . 7 wff ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦)
30	17, 29	wa 395	. . . . . 6 wff ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))
31	30, 13, 15	copab 5205	. . . . 5 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))}
32	12, 31	cqs 8744	. . . 4 class (𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))})
33	4, 11, 32	csb 3899	. . 3 class ⦋((Base‘𝑣) ∖ {(0g‘𝑣)}) / 𝑏⦌(𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))})
34	2, 3, 33	cmpt 5225	. 2 class (𝑣 ∈ LVec ↦ ⦋((Base‘𝑣) ∖ {(0g‘𝑣)}) / 𝑏⦌(𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))}))
35	1, 34	wceq 1540	1 wff ℙ𝕣𝕠𝕛 = (𝑣 ∈ LVec ↦ ⦋((Base‘𝑣) ∖ {(0g‘𝑣)}) / 𝑏⦌(𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))}))

This definition is referenced by:  prjspval  42613