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 ℙ𝕣𝕠𝕛 = ( 𝑣 ∈ 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 ‘ 𝑣 ) ) 𝑥 = ( 𝑙 ( ·𝑠𝑣 ) 𝑦 ) ) } ) )