Users' Mathboxes Mathbox for Steven Nguyen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-prjsp Structured version   Visualization version   GIF version

Definition df-prjsp 41344
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, making equivalent rational multiples of real numbers). Compare df-lsatoms 37846. (Contributed by BJ and SN, 29-Apr-2023.)
Assertion
Ref Expression
df-prjsp ℙ𝕣𝕠𝕛 = (𝑣 ∈ LVec ↦ ⦋((Baseβ€˜π‘£) βˆ– {(0gβ€˜π‘£)}) / π‘β¦Œ(𝑏 / {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ βˆƒπ‘™ ∈ (Baseβ€˜(Scalarβ€˜π‘£))π‘₯ = (𝑙( ·𝑠 β€˜π‘£)𝑦))}))
Distinct variable group:   𝑣,𝑏,π‘₯,𝑦,𝑙

Detailed syntax breakdown of Definition df-prjsp
StepHypRef Expression
1 cprjsp 41343 . 2 class ℙ𝕣𝕠𝕛
2 vv . . 3 setvar 𝑣
3 clvec 20713 . . 3 class LVec
4 vb . . . 4 setvar 𝑏
52cv 1541 . . . . . 6 class 𝑣
6 cbs 17144 . . . . . 6 class Base
75, 6cfv 6544 . . . . 5 class (Baseβ€˜π‘£)
8 c0g 17385 . . . . . . 7 class 0g
95, 8cfv 6544 . . . . . 6 class (0gβ€˜π‘£)
109csn 4629 . . . . 5 class {(0gβ€˜π‘£)}
117, 10cdif 3946 . . . 4 class ((Baseβ€˜π‘£) βˆ– {(0gβ€˜π‘£)})
124cv 1541 . . . . 5 class 𝑏
13 vx . . . . . . . . 9 setvar π‘₯
1413, 4wel 2108 . . . . . . . 8 wff π‘₯ ∈ 𝑏
15 vy . . . . . . . . 9 setvar 𝑦
1615, 4wel 2108 . . . . . . . 8 wff 𝑦 ∈ 𝑏
1714, 16wa 397 . . . . . . 7 wff (π‘₯ ∈ 𝑏 ∧ 𝑦 ∈ 𝑏)
1813cv 1541 . . . . . . . . 9 class π‘₯
19 vl . . . . . . . . . . 11 setvar 𝑙
2019cv 1541 . . . . . . . . . 10 class 𝑙
2115cv 1541 . . . . . . . . . 10 class 𝑦
22 cvsca 17201 . . . . . . . . . . 11 class ·𝑠
235, 22cfv 6544 . . . . . . . . . 10 class ( ·𝑠 β€˜π‘£)
2420, 21, 23co 7409 . . . . . . . . 9 class (𝑙( ·𝑠 β€˜π‘£)𝑦)
2518, 24wceq 1542 . . . . . . . 8 wff π‘₯ = (𝑙( ·𝑠 β€˜π‘£)𝑦)
26 csca 17200 . . . . . . . . . 10 class Scalar
275, 26cfv 6544 . . . . . . . . 9 class (Scalarβ€˜π‘£)
2827, 6cfv 6544 . . . . . . . 8 class (Baseβ€˜(Scalarβ€˜π‘£))
2925, 19, 28wrex 3071 . . . . . . 7 wff βˆƒπ‘™ ∈ (Baseβ€˜(Scalarβ€˜π‘£))π‘₯ = (𝑙( ·𝑠 β€˜π‘£)𝑦)
3017, 29wa 397 . . . . . 6 wff ((π‘₯ ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ βˆƒπ‘™ ∈ (Baseβ€˜(Scalarβ€˜π‘£))π‘₯ = (𝑙( ·𝑠 β€˜π‘£)𝑦))
3130, 13, 15copab 5211 . . . . 5 class {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ βˆƒπ‘™ ∈ (Baseβ€˜(Scalarβ€˜π‘£))π‘₯ = (𝑙( ·𝑠 β€˜π‘£)𝑦))}
3212, 31cqs 8702 . . . 4 class (𝑏 / {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ βˆƒπ‘™ ∈ (Baseβ€˜(Scalarβ€˜π‘£))π‘₯ = (𝑙( ·𝑠 β€˜π‘£)𝑦))})
334, 11, 32csb 3894 . . 3 class ⦋((Baseβ€˜π‘£) βˆ– {(0gβ€˜π‘£)}) / π‘β¦Œ(𝑏 / {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ βˆƒπ‘™ ∈ (Baseβ€˜(Scalarβ€˜π‘£))π‘₯ = (𝑙( ·𝑠 β€˜π‘£)𝑦))})
342, 3, 33cmpt 5232 . 2 class (𝑣 ∈ LVec ↦ ⦋((Baseβ€˜π‘£) βˆ– {(0gβ€˜π‘£)}) / π‘β¦Œ(𝑏 / {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ βˆƒπ‘™ ∈ (Baseβ€˜(Scalarβ€˜π‘£))π‘₯ = (𝑙( ·𝑠 β€˜π‘£)𝑦))}))
351, 34wceq 1542 1 wff ℙ𝕣𝕠𝕛 = (𝑣 ∈ LVec ↦ ⦋((Baseβ€˜π‘£) βˆ– {(0gβ€˜π‘£)}) / π‘β¦Œ(𝑏 / {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ βˆƒπ‘™ ∈ (Baseβ€˜(Scalarβ€˜π‘£))π‘₯ = (𝑙( ·𝑠 β€˜π‘£)𝑦))}))
Colors of variables: wff setvar class
This definition is referenced by:  prjspval  41345
  Copyright terms: Public domain W3C validator