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
|- PrjSp = ( v e. LVec |-> [_ ( ( Base ` v ) \ { ( 0g ` v ) } ) / b ]_ ( b /. { <. x , y >. | ( ( x e. b /\ y e. b ) /\ E. l e. ( Base ` ( Scalar ` v ) ) x = ( l ( .s ` v ) y ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cprjsp
 |-  PrjSp
1 vv
 |-  v
2 clvec
 |-  LVec
3 cbs
 |-  Base
4 1 cv
 |-  v
5 4 3 cfv
 |-  ( Base ` v )
6 c0g
 |-  0g
7 4 6 cfv
 |-  ( 0g ` v )
8 7 csn
 |-  { ( 0g ` v ) }
9 5 8 cdif
 |-  ( ( Base ` v ) \ { ( 0g ` v ) } )
10 vb
 |-  b
11 10 cv
 |-  b
12 vx
 |-  x
13 vy
 |-  y
14 12 cv
 |-  x
15 14 11 wcel
 |-  x e. b
16 13 cv
 |-  y
17 16 11 wcel
 |-  y e. b
18 15 17 wa
 |-  ( x e. b /\ y e. b )
19 vl
 |-  l
20 csca
 |-  Scalar
21 4 20 cfv
 |-  ( Scalar ` v )
22 21 3 cfv
 |-  ( Base ` ( Scalar ` v ) )
23 19 cv
 |-  l
24 cvsca
 |-  .s
25 4 24 cfv
 |-  ( .s ` v )
26 23 16 25 co
 |-  ( l ( .s ` v ) y )
27 14 26 wceq
 |-  x = ( l ( .s ` v ) y )
28 27 19 22 wrex
 |-  E. l e. ( Base ` ( Scalar ` v ) ) x = ( l ( .s ` v ) y )
29 18 28 wa
 |-  ( ( x e. b /\ y e. b ) /\ E. l e. ( Base ` ( Scalar ` v ) ) x = ( l ( .s ` v ) y ) )
30 29 12 13 copab
 |-  { <. x , y >. | ( ( x e. b /\ y e. b ) /\ E. l e. ( Base ` ( Scalar ` v ) ) x = ( l ( .s ` v ) y ) ) }
31 11 30 cqs
 |-  ( b /. { <. x , y >. | ( ( x e. b /\ y e. b ) /\ E. l e. ( Base ` ( Scalar ` v ) ) x = ( l ( .s ` v ) y ) ) } )
32 10 9 31 csb
 |-  [_ ( ( Base ` v ) \ { ( 0g ` v ) } ) / b ]_ ( b /. { <. x , y >. | ( ( x e. b /\ y e. b ) /\ E. l e. ( Base ` ( Scalar ` v ) ) x = ( l ( .s ` v ) y ) ) } )
33 1 2 32 cmpt
 |-  ( v e. LVec |-> [_ ( ( Base ` v ) \ { ( 0g ` v ) } ) / b ]_ ( b /. { <. x , y >. | ( ( x e. b /\ y e. b ) /\ E. l e. ( Base ` ( Scalar ` v ) ) x = ( l ( .s ` v ) y ) ) } ) )
34 0 33 wceq
 |-  PrjSp = ( v e. LVec |-> [_ ( ( Base ` v ) \ { ( 0g ` v ) } ) / b ]_ ( b /. { <. x , y >. | ( ( x e. b /\ y e. b ) /\ E. l e. ( Base ` ( Scalar ` v ) ) x = ( l ( .s ` v ) y ) ) } ) )