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. Note that the meaning of "projective space" is more general than the section comment might suggest. In particular, the projective space obtained from RR as a QQ -vector space is infinite-dimensional and is not of the form covered by df-prjspn . 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 ) ) } ) )