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 39512
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.)
Assertion
Ref Expression
df-prjsp ℙ𝕣𝕠𝕛 = (𝑣 ∈ LVec ↦ ((Base‘𝑣) ∖ {(0g𝑣)}) / 𝑏(𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝑏𝑦𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠𝑣)𝑦))}))
Distinct variable group:   𝑣,𝑏,𝑥,𝑦,𝑙

Detailed syntax breakdown of Definition df-prjsp
StepHypRef Expression
1 cprjsp 39511 . 2 class ℙ𝕣𝕠𝕛
2 vv . . 3 setvar 𝑣
3 clvec 19874 . . 3 class LVec
4 vb . . . 4 setvar 𝑏
52cv 1537 . . . . . 6 class 𝑣
6 cbs 16483 . . . . . 6 class Base
75, 6cfv 6343 . . . . 5 class (Base‘𝑣)
8 c0g 16713 . . . . . . 7 class 0g
95, 8cfv 6343 . . . . . 6 class (0g𝑣)
109csn 4550 . . . . 5 class {(0g𝑣)}
117, 10cdif 3916 . . . 4 class ((Base‘𝑣) ∖ {(0g𝑣)})
124cv 1537 . . . . 5 class 𝑏
13 vx . . . . . . . . 9 setvar 𝑥
1413, 4wel 2116 . . . . . . . 8 wff 𝑥𝑏
15 vy . . . . . . . . 9 setvar 𝑦
1615, 4wel 2116 . . . . . . . 8 wff 𝑦𝑏
1714, 16wa 399 . . . . . . 7 wff (𝑥𝑏𝑦𝑏)
1813cv 1537 . . . . . . . . 9 class 𝑥
19 vl . . . . . . . . . . 11 setvar 𝑙
2019cv 1537 . . . . . . . . . 10 class 𝑙
2115cv 1537 . . . . . . . . . 10 class 𝑦
22 cvsca 16569 . . . . . . . . . . 11 class ·𝑠
235, 22cfv 6343 . . . . . . . . . 10 class ( ·𝑠𝑣)
2420, 21, 23co 7149 . . . . . . . . 9 class (𝑙( ·𝑠𝑣)𝑦)
2518, 24wceq 1538 . . . . . . . 8 wff 𝑥 = (𝑙( ·𝑠𝑣)𝑦)
26 csca 16568 . . . . . . . . . 10 class Scalar
275, 26cfv 6343 . . . . . . . . 9 class (Scalar‘𝑣)
2827, 6cfv 6343 . . . . . . . 8 class (Base‘(Scalar‘𝑣))
2925, 19, 28wrex 3134 . . . . . . 7 wff 𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠𝑣)𝑦)
3017, 29wa 399 . . . . . 6 wff ((𝑥𝑏𝑦𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠𝑣)𝑦))
3130, 13, 15copab 5114 . . . . 5 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝑏𝑦𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠𝑣)𝑦))}
3212, 31cqs 8284 . . . 4 class (𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝑏𝑦𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠𝑣)𝑦))})
334, 11, 32csb 3866 . . 3 class ((Base‘𝑣) ∖ {(0g𝑣)}) / 𝑏(𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝑏𝑦𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠𝑣)𝑦))})
342, 3, 33cmpt 5132 . 2 class (𝑣 ∈ LVec ↦ ((Base‘𝑣) ∖ {(0g𝑣)}) / 𝑏(𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝑏𝑦𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠𝑣)𝑦))}))
351, 34wceq 1538 1 wff ℙ𝕣𝕠𝕛 = (𝑣 ∈ LVec ↦ ((Base‘𝑣) ∖ {(0g𝑣)}) / 𝑏(𝑏 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝑏𝑦𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠𝑣)𝑦))}))
Colors of variables: wff setvar class
This definition is referenced by:  prjspval  39513
  Copyright terms: Public domain W3C validator