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). (Contributed by BJ and Steven Nguyen, 29-Apr-2023)

	Ref	Expression
Assertion	df-prjsp	⊢ ℙ𝕣𝕠𝕛 = ( 𝑣 ∈ LVec ↦ ⦋ ( ( Base ‘ 𝑣 ) ∖ { ( 0g ‘ 𝑣 ) } ) / 𝑏 ⦌ ( 𝑏 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprjsp	⊢ ℙ𝕣𝕠𝕛
1		vv	⊢ 𝑣
2		clvec	⊢ LVec
3		cbs	⊢ Base
4	1	cv	⊢ 𝑣
5	4 3	cfv	⊢ ( Base ‘ 𝑣 )
6		c0g	⊢ 0g
7	4 6	cfv	⊢ ( 0g ‘ 𝑣 )
8	7	csn	⊢ { ( 0g ‘ 𝑣 ) }
9	5 8	cdif	⊢ ( ( Base ‘ 𝑣 ) ∖ { ( 0g ‘ 𝑣 ) } )
10		vb	⊢ 𝑏
11	10	cv	⊢ 𝑏
12		vx	⊢ 𝑥
13		vy	⊢ 𝑦
14	12	cv	⊢ 𝑥
15	14 11	wcel	⊢ 𝑥 ∈ 𝑏
16	13	cv	⊢ 𝑦
17	16 11	wcel	⊢ 𝑦 ∈ 𝑏
18	15 17	wa	⊢ ( 𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏 )
19		vl	⊢ 𝑙
20		csca	⊢ Scalar
21	4 20	cfv	⊢ ( Scalar ‘ 𝑣 )
22	21 3	cfv	⊢ ( Base ‘ ( Scalar ‘ 𝑣 ) )
23	19	cv	⊢ 𝑙
24		cvsca	⊢ ·𝑠
25	4 24	cfv	⊢ ( ·𝑠 ‘ 𝑣 )
26	23 16 25	co	⊢ ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 )
27	14 26	wceq	⊢ 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 )
28	27 19 22	wrex	⊢ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 )
29	18 28	wa	⊢ ( ( 𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) )
30	29 12 13	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) ) }
31	11 30	cqs	⊢ ( 𝑏 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) ) } )
32	10 9 31	csb	⊢ ⦋ ( ( Base ‘ 𝑣 ) ∖ { ( 0g ‘ 𝑣 ) } ) / 𝑏 ⦌ ( 𝑏 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) ) } )
33	1 2 32	cmpt	⊢ ( 𝑣 ∈ LVec ↦ ⦋ ( ( Base ‘ 𝑣 ) ∖ { ( 0g ‘ 𝑣 ) } ) / 𝑏 ⦌ ( 𝑏 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) ) } ) )
34	0 33	wceq	⊢ ℙ𝕣𝕠𝕛 = ( 𝑣 ∈ LVec ↦ ⦋ ( ( Base ‘ 𝑣 ) ∖ { ( 0g ‘ 𝑣 ) } ) / 𝑏 ⦌ ( 𝑏 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) ) } ) )