Metamath Proof Explorer


Definition df-prjsp

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, equivocating rational multiples of real numbers). Compare df-lsatoms . (Contributed by BJ and SN, 29-Apr-2023)

Ref Expression
Assertion df-prjsp ℙ𝕣𝕠𝕛=vLVecBasev0v/bb/xy|xbyblBaseScalarvx=lvy

Detailed syntax breakdown

Step Hyp Ref Expression
0 cprjsp classℙ𝕣𝕠𝕛
1 vv setvarv
2 clvec classLVec
3 cbs classBase
4 1 cv setvarv
5 4 3 cfv classBasev
6 c0g class0𝑔
7 4 6 cfv class0v
8 7 csn class0v
9 5 8 cdif classBasev0v
10 vb setvarb
11 10 cv setvarb
12 vx setvarx
13 vy setvary
14 12 cv setvarx
15 14 11 wcel wffxb
16 13 cv setvary
17 16 11 wcel wffyb
18 15 17 wa wffxbyb
19 vl setvarl
20 csca classScalar
21 4 20 cfv classScalarv
22 21 3 cfv classBaseScalarv
23 19 cv setvarl
24 cvsca class𝑠
25 4 24 cfv classv
26 23 16 25 co classlvy
27 14 26 wceq wffx=lvy
28 27 19 22 wrex wfflBaseScalarvx=lvy
29 18 28 wa wffxbyblBaseScalarvx=lvy
30 29 12 13 copab classxy|xbyblBaseScalarvx=lvy
31 11 30 cqs classb/xy|xbyblBaseScalarvx=lvy
32 10 9 31 csb classBasev0v/bb/xy|xbyblBaseScalarvx=lvy
33 1 2 32 cmpt classvLVecBasev0v/bb/xy|xbyblBaseScalarvx=lvy
34 0 33 wceq wffℙ𝕣𝕠𝕛=vLVecBasev0v/bb/xy|xbyblBaseScalarvx=lvy