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 25735
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 25734 . 2 class toTG
2 vw . . 3 setvar 𝑤
3 cvv 3195 . . 3 class V
4 vi . . . 4 setvar 𝑖
5 vx . . . . 5 setvar 𝑥
6 vy . . . . 5 setvar 𝑦
72cv 1480 . . . . . 6 class 𝑤
8 cbs 15838 . . . . . 6 class Base
97, 8cfv 5876 . . . . 5 class (Base‘𝑤)
10 vz . . . . . . . . . 10 setvar 𝑧
1110cv 1480 . . . . . . . . 9 class 𝑧
125cv 1480 . . . . . . . . 9 class 𝑥
13 csg 17405 . . . . . . . . . 10 class -g
147, 13cfv 5876 . . . . . . . . 9 class (-g𝑤)
1511, 12, 14co 6635 . . . . . . . 8 class (𝑧(-g𝑤)𝑥)
16 vk . . . . . . . . . 10 setvar 𝑘
1716cv 1480 . . . . . . . . 9 class 𝑘
186cv 1480 . . . . . . . . . 10 class 𝑦
1918, 12, 14co 6635 . . . . . . . . 9 class (𝑦(-g𝑤)𝑥)
20 cvsca 15926 . . . . . . . . . 10 class ·𝑠
217, 20cfv 5876 . . . . . . . . 9 class ( ·𝑠𝑤)
2217, 19, 21co 6635 . . . . . . . 8 class (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))
2315, 22wceq 1481 . . . . . . 7 wff (𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))
24 cc0 9921 . . . . . . . 8 class 0
25 c1 9922 . . . . . . . 8 class 1
26 cicc 12163 . . . . . . . 8 class [,]
2724, 25, 26co 6635 . . . . . . 7 class (0[,]1)
2823, 16, 27wrex 2910 . . . . . 6 wff 𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))
2928, 10, 9crab 2913 . . . . 5 class {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))}
305, 6, 9, 9, 29cmpt2 6637 . . . 4 class (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))})
31 cnx 15835 . . . . . . . 8 class ndx
32 citv 25316 . . . . . . . 8 class Itv
3331, 32cfv 5876 . . . . . . 7 class (Itv‘ndx)
344cv 1480 . . . . . . 7 class 𝑖
3533, 34cop 4174 . . . . . 6 class ⟨(Itv‘ndx), 𝑖
36 csts 15836 . . . . . 6 class sSet
377, 35, 36co 6635 . . . . 5 class (𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩)
38 clng 25317 . . . . . . 7 class LineG
3931, 38cfv 5876 . . . . . 6 class (LineG‘ndx)
4012, 18, 34co 6635 . . . . . . . . . 10 class (𝑥𝑖𝑦)
4111, 40wcel 1988 . . . . . . . . 9 wff 𝑧 ∈ (𝑥𝑖𝑦)
4211, 18, 34co 6635 . . . . . . . . . 10 class (𝑧𝑖𝑦)
4312, 42wcel 1988 . . . . . . . . 9 wff 𝑥 ∈ (𝑧𝑖𝑦)
4412, 11, 34co 6635 . . . . . . . . . 10 class (𝑥𝑖𝑧)
4518, 44wcel 1988 . . . . . . . . 9 wff 𝑦 ∈ (𝑥𝑖𝑧)
4641, 43, 45w3o 1035 . . . . . . . 8 wff (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))
4746, 10, 9crab 2913 . . . . . . 7 class {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}
485, 6, 9, 9, 47cmpt2 6637 . . . . . 6 class (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})
4939, 48cop 4174 . . . . 5 class ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩
5037, 49, 36co 6635 . . . 4 class ((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩)
514, 30, 50csb 3526 . . 3 class (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))}) / 𝑖((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩)
522, 3, 51cmpt 4720 . 2 class (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))}) / 𝑖((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
531, 52wceq 1481 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  25736
  Copyright terms: Public domain W3C validator