Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ttg Structured version   Visualization version   GIF version

Definition df-ttg 25554
 Description: Define a function converting a complex Hilbert space to a Tarski Geometry. It does so by equipping the structure with a betweenness operation. Note that because the scalar product is applied over the interval (0[,]1), only spaces whose scalar field is a superset of that interval can be considered. (Contributed by Thierry Arnoux, 24-Mar-2019.)
Assertion
Ref Expression
df-ttg toTG = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))}) / 𝑖((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
Distinct variable group:   𝑖,𝑘,𝑤,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-ttg
StepHypRef Expression
1 cttg 25553 . 2 class toTG
2 vw . . 3 setvar 𝑤
3 cvv 3173 . . 3 class V
4 vi . . . 4 setvar 𝑖
5 vx . . . . 5 setvar 𝑥
6 vy . . . . 5 setvar 𝑦
72cv 1474 . . . . . 6 class 𝑤
8 cbs 15695 . . . . . 6 class Base
97, 8cfv 5804 . . . . 5 class (Base‘𝑤)
10 vz . . . . . . . . . 10 setvar 𝑧
1110cv 1474 . . . . . . . . 9 class 𝑧
125cv 1474 . . . . . . . . 9 class 𝑥
13 csg 17247 . . . . . . . . . 10 class -g
147, 13cfv 5804 . . . . . . . . 9 class (-g𝑤)
1511, 12, 14co 6549 . . . . . . . 8 class (𝑧(-g𝑤)𝑥)
16 vk . . . . . . . . . 10 setvar 𝑘
1716cv 1474 . . . . . . . . 9 class 𝑘
186cv 1474 . . . . . . . . . 10 class 𝑦
1918, 12, 14co 6549 . . . . . . . . 9 class (𝑦(-g𝑤)𝑥)
20 cvsca 15772 . . . . . . . . . 10 class ·𝑠
217, 20cfv 5804 . . . . . . . . 9 class ( ·𝑠𝑤)
2217, 19, 21co 6549 . . . . . . . 8 class (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))
2315, 22wceq 1475 . . . . . . 7 wff (𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))
24 cc0 9815 . . . . . . . 8 class 0
25 c1 9816 . . . . . . . 8 class 1
26 cicc 12049 . . . . . . . 8 class [,]
2724, 25, 26co 6549 . . . . . . 7 class (0[,]1)
2823, 16, 27wrex 2897 . . . . . 6 wff 𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))
2928, 10, 9crab 2900 . . . . 5 class {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))}
305, 6, 9, 9, 29cmpt2 6551 . . . 4 class (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))})
31 cnx 15692 . . . . . . . 8 class ndx
32 citv 25135 . . . . . . . 8 class Itv
3331, 32cfv 5804 . . . . . . 7 class (Itv‘ndx)
344cv 1474 . . . . . . 7 class 𝑖
3533, 34cop 4131 . . . . . 6 class ⟨(Itv‘ndx), 𝑖
36 csts 15693 . . . . . 6 class sSet
377, 35, 36co 6549 . . . . 5 class (𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩)
38 clng 25136 . . . . . . 7 class LineG
3931, 38cfv 5804 . . . . . 6 class (LineG‘ndx)
4012, 18, 34co 6549 . . . . . . . . . 10 class (𝑥𝑖𝑦)
4111, 40wcel 1977 . . . . . . . . 9 wff 𝑧 ∈ (𝑥𝑖𝑦)
4211, 18, 34co 6549 . . . . . . . . . 10 class (𝑧𝑖𝑦)
4312, 42wcel 1977 . . . . . . . . 9 wff 𝑥 ∈ (𝑧𝑖𝑦)
4412, 11, 34co 6549 . . . . . . . . . 10 class (𝑥𝑖𝑧)
4518, 44wcel 1977 . . . . . . . . 9 wff 𝑦 ∈ (𝑥𝑖𝑧)
4641, 43, 45w3o 1030 . . . . . . . 8 wff (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))
4746, 10, 9crab 2900 . . . . . . 7 class {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}
485, 6, 9, 9, 47cmpt2 6551 . . . . . 6 class (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})
4939, 48cop 4131 . . . . 5 class ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩
5037, 49, 36co 6549 . . . 4 class ((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩)
514, 30, 50csb 3499 . . 3 class (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))}) / 𝑖((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩)
522, 3, 51cmpt 4643 . 2 class (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))}) / 𝑖((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
531, 52wceq 1475 1 wff toTG = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))}) / 𝑖((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
 Colors of variables: wff setvar class This definition is referenced by:  ttgval  25555
 Copyright terms: Public domain W3C validator