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 27233
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 27232 . 2 class toTG
2 vw . . 3 setvar 𝑤
3 cvv 3431 . . 3 class V
4 vi . . . 4 setvar 𝑖
5 vx . . . . 5 setvar 𝑥
6 vy . . . . 5 setvar 𝑦
72cv 1538 . . . . . 6 class 𝑤
8 cbs 16910 . . . . . 6 class Base
97, 8cfv 6435 . . . . 5 class (Base‘𝑤)
10 vz . . . . . . . . . 10 setvar 𝑧
1110cv 1538 . . . . . . . . 9 class 𝑧
125cv 1538 . . . . . . . . 9 class 𝑥
13 csg 18577 . . . . . . . . . 10 class -g
147, 13cfv 6435 . . . . . . . . 9 class (-g𝑤)
1511, 12, 14co 7277 . . . . . . . 8 class (𝑧(-g𝑤)𝑥)
16 vk . . . . . . . . . 10 setvar 𝑘
1716cv 1538 . . . . . . . . 9 class 𝑘
186cv 1538 . . . . . . . . . 10 class 𝑦
1918, 12, 14co 7277 . . . . . . . . 9 class (𝑦(-g𝑤)𝑥)
20 cvsca 16964 . . . . . . . . . 10 class ·𝑠
217, 20cfv 6435 . . . . . . . . 9 class ( ·𝑠𝑤)
2217, 19, 21co 7277 . . . . . . . 8 class (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))
2315, 22wceq 1539 . . . . . . 7 wff (𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))
24 cc0 10869 . . . . . . . 8 class 0
25 c1 10870 . . . . . . . 8 class 1
26 cicc 13080 . . . . . . . 8 class [,]
2724, 25, 26co 7277 . . . . . . 7 class (0[,]1)
2823, 16, 27wrex 3065 . . . . . 6 wff 𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))
2928, 10, 9crab 3068 . . . . 5 class {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))}
305, 6, 9, 9, 29cmpo 7279 . . . 4 class (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))})
31 cnx 16892 . . . . . . . 8 class ndx
32 citv 26792 . . . . . . . 8 class Itv
3331, 32cfv 6435 . . . . . . 7 class (Itv‘ndx)
344cv 1538 . . . . . . 7 class 𝑖
3533, 34cop 4569 . . . . . 6 class ⟨(Itv‘ndx), 𝑖
36 csts 16862 . . . . . 6 class sSet
377, 35, 36co 7277 . . . . 5 class (𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩)
38 clng 26793 . . . . . . 7 class LineG
3931, 38cfv 6435 . . . . . 6 class (LineG‘ndx)
4012, 18, 34co 7277 . . . . . . . . . 10 class (𝑥𝑖𝑦)
4111, 40wcel 2106 . . . . . . . . 9 wff 𝑧 ∈ (𝑥𝑖𝑦)
4211, 18, 34co 7277 . . . . . . . . . 10 class (𝑧𝑖𝑦)
4312, 42wcel 2106 . . . . . . . . 9 wff 𝑥 ∈ (𝑧𝑖𝑦)
4412, 11, 34co 7277 . . . . . . . . . 10 class (𝑥𝑖𝑧)
4518, 44wcel 2106 . . . . . . . . 9 wff 𝑦 ∈ (𝑥𝑖𝑧)
4641, 43, 45w3o 1085 . . . . . . . 8 wff (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))
4746, 10, 9crab 3068 . . . . . . 7 class {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}
485, 6, 9, 9, 47cmpo 7279 . . . . . 6 class (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})
4939, 48cop 4569 . . . . 5 class ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩
5037, 49, 36co 7277 . . . 4 class ((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩)
514, 30, 50csb 3833 . . 3 class (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))}) / 𝑖((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩)
522, 3, 51cmpt 5159 . 2 class (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))}) / 𝑖((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
531, 52wceq 1539 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  27234  ttgvalOLD  27235
  Copyright terms: Public domain W3C validator