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

Definition df-ttg 26587
Description: Define a function converting a subcomplex 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 26586 . 2 class toTG
2 vw . . 3 setvar 𝑤
3 cvv 3492 . . 3 class V
4 vi . . . 4 setvar 𝑖
5 vx . . . . 5 setvar 𝑥
6 vy . . . . 5 setvar 𝑦
72cv 1527 . . . . . 6 class 𝑤
8 cbs 16471 . . . . . 6 class Base
97, 8cfv 6348 . . . . 5 class (Base‘𝑤)
10 vz . . . . . . . . . 10 setvar 𝑧
1110cv 1527 . . . . . . . . 9 class 𝑧
125cv 1527 . . . . . . . . 9 class 𝑥
13 csg 18043 . . . . . . . . . 10 class -g
147, 13cfv 6348 . . . . . . . . 9 class (-g𝑤)
1511, 12, 14co 7145 . . . . . . . 8 class (𝑧(-g𝑤)𝑥)
16 vk . . . . . . . . . 10 setvar 𝑘
1716cv 1527 . . . . . . . . 9 class 𝑘
186cv 1527 . . . . . . . . . 10 class 𝑦
1918, 12, 14co 7145 . . . . . . . . 9 class (𝑦(-g𝑤)𝑥)
20 cvsca 16557 . . . . . . . . . 10 class ·𝑠
217, 20cfv 6348 . . . . . . . . 9 class ( ·𝑠𝑤)
2217, 19, 21co 7145 . . . . . . . 8 class (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))
2315, 22wceq 1528 . . . . . . 7 wff (𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))
24 cc0 10525 . . . . . . . 8 class 0
25 c1 10526 . . . . . . . 8 class 1
26 cicc 12729 . . . . . . . 8 class [,]
2724, 25, 26co 7145 . . . . . . 7 class (0[,]1)
2823, 16, 27wrex 3136 . . . . . 6 wff 𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))
2928, 10, 9crab 3139 . . . . 5 class {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))}
305, 6, 9, 9, 29cmpo 7147 . . . 4 class (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))})
31 cnx 16468 . . . . . . . 8 class ndx
32 citv 26149 . . . . . . . 8 class Itv
3331, 32cfv 6348 . . . . . . 7 class (Itv‘ndx)
344cv 1527 . . . . . . 7 class 𝑖
3533, 34cop 4563 . . . . . 6 class ⟨(Itv‘ndx), 𝑖
36 csts 16469 . . . . . 6 class sSet
377, 35, 36co 7145 . . . . 5 class (𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩)
38 clng 26150 . . . . . . 7 class LineG
3931, 38cfv 6348 . . . . . 6 class (LineG‘ndx)
4012, 18, 34co 7145 . . . . . . . . . 10 class (𝑥𝑖𝑦)
4111, 40wcel 2105 . . . . . . . . 9 wff 𝑧 ∈ (𝑥𝑖𝑦)
4211, 18, 34co 7145 . . . . . . . . . 10 class (𝑧𝑖𝑦)
4312, 42wcel 2105 . . . . . . . . 9 wff 𝑥 ∈ (𝑧𝑖𝑦)
4412, 11, 34co 7145 . . . . . . . . . 10 class (𝑥𝑖𝑧)
4518, 44wcel 2105 . . . . . . . . 9 wff 𝑦 ∈ (𝑥𝑖𝑧)
4641, 43, 45w3o 1078 . . . . . . . 8 wff (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))
4746, 10, 9crab 3139 . . . . . . 7 class {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}
485, 6, 9, 9, 47cmpo 7147 . . . . . 6 class (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})
4939, 48cop 4563 . . . . 5 class ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩
5037, 49, 36co 7145 . . . 4 class ((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩)
514, 30, 50csb 3880 . . 3 class (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))}) / 𝑖((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩)
522, 3, 51cmpt 5137 . 2 class (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))}) / 𝑖((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
531, 52wceq 1528 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  26588
  Copyright terms: Public domain W3C validator