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 28122
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 28121 . 2 class toTG
2 vw . . 3 setvar 𝑀
3 cvv 3474 . . 3 class V
4 vi . . . 4 setvar 𝑖
5 vx . . . . 5 setvar π‘₯
6 vy . . . . 5 setvar 𝑦
72cv 1540 . . . . . 6 class 𝑀
8 cbs 17143 . . . . . 6 class Base
97, 8cfv 6543 . . . . 5 class (Baseβ€˜π‘€)
10 vz . . . . . . . . . 10 setvar 𝑧
1110cv 1540 . . . . . . . . 9 class 𝑧
125cv 1540 . . . . . . . . 9 class π‘₯
13 csg 18820 . . . . . . . . . 10 class -g
147, 13cfv 6543 . . . . . . . . 9 class (-gβ€˜π‘€)
1511, 12, 14co 7408 . . . . . . . 8 class (𝑧(-gβ€˜π‘€)π‘₯)
16 vk . . . . . . . . . 10 setvar π‘˜
1716cv 1540 . . . . . . . . 9 class π‘˜
186cv 1540 . . . . . . . . . 10 class 𝑦
1918, 12, 14co 7408 . . . . . . . . 9 class (𝑦(-gβ€˜π‘€)π‘₯)
20 cvsca 17200 . . . . . . . . . 10 class ·𝑠
217, 20cfv 6543 . . . . . . . . 9 class ( ·𝑠 β€˜π‘€)
2217, 19, 21co 7408 . . . . . . . 8 class (π‘˜( ·𝑠 β€˜π‘€)(𝑦(-gβ€˜π‘€)π‘₯))
2315, 22wceq 1541 . . . . . . 7 wff (𝑧(-gβ€˜π‘€)π‘₯) = (π‘˜( ·𝑠 β€˜π‘€)(𝑦(-gβ€˜π‘€)π‘₯))
24 cc0 11109 . . . . . . . 8 class 0
25 c1 11110 . . . . . . . 8 class 1
26 cicc 13326 . . . . . . . 8 class [,]
2724, 25, 26co 7408 . . . . . . 7 class (0[,]1)
2823, 16, 27wrex 3070 . . . . . 6 wff βˆƒπ‘˜ ∈ (0[,]1)(𝑧(-gβ€˜π‘€)π‘₯) = (π‘˜( ·𝑠 β€˜π‘€)(𝑦(-gβ€˜π‘€)π‘₯))
2928, 10, 9crab 3432 . . . . 5 class {𝑧 ∈ (Baseβ€˜π‘€) ∣ βˆƒπ‘˜ ∈ (0[,]1)(𝑧(-gβ€˜π‘€)π‘₯) = (π‘˜( ·𝑠 β€˜π‘€)(𝑦(-gβ€˜π‘€)π‘₯))}
305, 6, 9, 9, 29cmpo 7410 . . . 4 class (π‘₯ ∈ (Baseβ€˜π‘€), 𝑦 ∈ (Baseβ€˜π‘€) ↦ {𝑧 ∈ (Baseβ€˜π‘€) ∣ βˆƒπ‘˜ ∈ (0[,]1)(𝑧(-gβ€˜π‘€)π‘₯) = (π‘˜( ·𝑠 β€˜π‘€)(𝑦(-gβ€˜π‘€)π‘₯))})
31 cnx 17125 . . . . . . . 8 class ndx
32 citv 27681 . . . . . . . 8 class Itv
3331, 32cfv 6543 . . . . . . 7 class (Itvβ€˜ndx)
344cv 1540 . . . . . . 7 class 𝑖
3533, 34cop 4634 . . . . . 6 class ⟨(Itvβ€˜ndx), π‘–βŸ©
36 csts 17095 . . . . . 6 class sSet
377, 35, 36co 7408 . . . . 5 class (𝑀 sSet ⟨(Itvβ€˜ndx), π‘–βŸ©)
38 clng 27682 . . . . . . 7 class LineG
3931, 38cfv 6543 . . . . . 6 class (LineGβ€˜ndx)
4012, 18, 34co 7408 . . . . . . . . . 10 class (π‘₯𝑖𝑦)
4111, 40wcel 2106 . . . . . . . . 9 wff 𝑧 ∈ (π‘₯𝑖𝑦)
4211, 18, 34co 7408 . . . . . . . . . 10 class (𝑧𝑖𝑦)
4312, 42wcel 2106 . . . . . . . . 9 wff π‘₯ ∈ (𝑧𝑖𝑦)
4412, 11, 34co 7408 . . . . . . . . . 10 class (π‘₯𝑖𝑧)
4518, 44wcel 2106 . . . . . . . . 9 wff 𝑦 ∈ (π‘₯𝑖𝑧)
4641, 43, 45w3o 1086 . . . . . . . 8 wff (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))
4746, 10, 9crab 3432 . . . . . . 7 class {𝑧 ∈ (Baseβ€˜π‘€) ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))}
485, 6, 9, 9, 47cmpo 7410 . . . . . 6 class (π‘₯ ∈ (Baseβ€˜π‘€), 𝑦 ∈ (Baseβ€˜π‘€) ↦ {𝑧 ∈ (Baseβ€˜π‘€) ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})
4939, 48cop 4634 . . . . 5 class ⟨(LineGβ€˜ndx), (π‘₯ ∈ (Baseβ€˜π‘€), 𝑦 ∈ (Baseβ€˜π‘€) ↦ {𝑧 ∈ (Baseβ€˜π‘€) ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})⟩
5037, 49, 36co 7408 . . . 4 class ((𝑀 sSet ⟨(Itvβ€˜ndx), π‘–βŸ©) sSet ⟨(LineGβ€˜ndx), (π‘₯ ∈ (Baseβ€˜π‘€), 𝑦 ∈ (Baseβ€˜π‘€) ↦ {𝑧 ∈ (Baseβ€˜π‘€) ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})⟩)
514, 30, 50csb 3893 . . 3 class ⦋(π‘₯ ∈ (Baseβ€˜π‘€), 𝑦 ∈ (Baseβ€˜π‘€) ↦ {𝑧 ∈ (Baseβ€˜π‘€) ∣ βˆƒπ‘˜ ∈ (0[,]1)(𝑧(-gβ€˜π‘€)π‘₯) = (π‘˜( ·𝑠 β€˜π‘€)(𝑦(-gβ€˜π‘€)π‘₯))}) / π‘–β¦Œ((𝑀 sSet ⟨(Itvβ€˜ndx), π‘–βŸ©) sSet ⟨(LineGβ€˜ndx), (π‘₯ ∈ (Baseβ€˜π‘€), 𝑦 ∈ (Baseβ€˜π‘€) ↦ {𝑧 ∈ (Baseβ€˜π‘€) ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})⟩)
522, 3, 51cmpt 5231 . 2 class (𝑀 ∈ V ↦ ⦋(π‘₯ ∈ (Baseβ€˜π‘€), 𝑦 ∈ (Baseβ€˜π‘€) ↦ {𝑧 ∈ (Baseβ€˜π‘€) ∣ βˆƒπ‘˜ ∈ (0[,]1)(𝑧(-gβ€˜π‘€)π‘₯) = (π‘˜( ·𝑠 β€˜π‘€)(𝑦(-gβ€˜π‘€)π‘₯))}) / π‘–β¦Œ((𝑀 sSet ⟨(Itvβ€˜ndx), π‘–βŸ©) sSet ⟨(LineGβ€˜ndx), (π‘₯ ∈ (Baseβ€˜π‘€), 𝑦 ∈ (Baseβ€˜π‘€) ↦ {𝑧 ∈ (Baseβ€˜π‘€) ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})⟩))
531, 52wceq 1541 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  28123  ttgvalOLD  28124
  Copyright terms: Public domain W3C validator