Metamath Proof Explorer

Definition df-ttg

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)

Ref Expression
Assertion df-ttg

Detailed syntax breakdown

Step Hyp Ref Expression
0 cttg ${class}{to𝒢}_{\mathrm{Tarski}}$
1 vw ${setvar}{w}$
2 cvv ${class}\mathrm{V}$
3 vx ${setvar}{x}$
4 cbs ${class}\mathrm{Base}$
5 1 cv ${setvar}{w}$
6 5 4 cfv ${class}{\mathrm{Base}}_{{w}}$
7 vy ${setvar}{y}$
8 vz ${setvar}{z}$
9 vk ${setvar}{k}$
10 cc0 ${class}0$
11 cicc ${class}\left[.\right]$
12 c1 ${class}1$
13 10 12 11 co ${class}\left[0,1\right]$
14 8 cv ${setvar}{z}$
15 csg ${class}{-}_{𝑔}$
16 5 15 cfv ${class}{-}_{{w}}$
17 3 cv ${setvar}{x}$
18 14 17 16 co ${class}\left({z}{-}_{{w}}{x}\right)$
19 9 cv ${setvar}{k}$
20 cvsca ${class}{\cdot }_{𝑠}$
21 5 20 cfv ${class}{\cdot }_{{w}}$
22 7 cv ${setvar}{y}$
23 22 17 16 co ${class}\left({y}{-}_{{w}}{x}\right)$
24 19 23 21 co ${class}\left({k}{\cdot }_{{w}}\left({y}{-}_{{w}}{x}\right)\right)$
25 18 24 wceq ${wff}{z}{-}_{{w}}{x}={k}{\cdot }_{{w}}\left({y}{-}_{{w}}{x}\right)$
26 25 9 13 wrex ${wff}\exists {k}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}{z}{-}_{{w}}{x}={k}{\cdot }_{{w}}\left({y}{-}_{{w}}{x}\right)$
27 26 8 6 crab ${class}\left\{{z}\in {\mathrm{Base}}_{{w}}|\exists {k}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}{z}{-}_{{w}}{x}={k}{\cdot }_{{w}}\left({y}{-}_{{w}}{x}\right)\right\}$
28 3 7 6 6 27 cmpo ${class}\left({x}\in {\mathrm{Base}}_{{w}},{y}\in {\mathrm{Base}}_{{w}}⟼\left\{{z}\in {\mathrm{Base}}_{{w}}|\exists {k}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}{z}{-}_{{w}}{x}={k}{\cdot }_{{w}}\left({y}{-}_{{w}}{x}\right)\right\}\right)$
29 vi ${setvar}{i}$
30 csts ${class}\mathrm{sSet}$
31 citv ${class}\mathrm{Itv}$
32 cnx ${class}\mathrm{ndx}$
33 32 31 cfv ${class}\mathrm{Itv}\left(\mathrm{ndx}\right)$
34 29 cv ${setvar}{i}$
35 33 34 cop ${class}⟨\mathrm{Itv}\left(\mathrm{ndx}\right),{i}⟩$
36 5 35 30 co ${class}\left({w}\mathrm{sSet}⟨\mathrm{Itv}\left(\mathrm{ndx}\right),{i}⟩\right)$
37 clng ${class}{Line}_{𝒢}$
38 32 37 cfv ${class}{Line}_{𝒢}\left(\mathrm{ndx}\right)$
39 17 22 34 co ${class}\left({x}{i}{y}\right)$
40 14 39 wcel ${wff}{z}\in \left({x}{i}{y}\right)$
41 14 22 34 co ${class}\left({z}{i}{y}\right)$
42 17 41 wcel ${wff}{x}\in \left({z}{i}{y}\right)$
43 17 14 34 co ${class}\left({x}{i}{z}\right)$
44 22 43 wcel ${wff}{y}\in \left({x}{i}{z}\right)$
45 40 42 44 w3o ${wff}\left({z}\in \left({x}{i}{y}\right)\vee {x}\in \left({z}{i}{y}\right)\vee {y}\in \left({x}{i}{z}\right)\right)$
46 45 8 6 crab ${class}\left\{{z}\in {\mathrm{Base}}_{{w}}|\left({z}\in \left({x}{i}{y}\right)\vee {x}\in \left({z}{i}{y}\right)\vee {y}\in \left({x}{i}{z}\right)\right)\right\}$
47 3 7 6 6 46 cmpo ${class}\left({x}\in {\mathrm{Base}}_{{w}},{y}\in {\mathrm{Base}}_{{w}}⟼\left\{{z}\in {\mathrm{Base}}_{{w}}|\left({z}\in \left({x}{i}{y}\right)\vee {x}\in \left({z}{i}{y}\right)\vee {y}\in \left({x}{i}{z}\right)\right)\right\}\right)$
48 38 47 cop ${class}⟨{Line}_{𝒢}\left(\mathrm{ndx}\right),\left({x}\in {\mathrm{Base}}_{{w}},{y}\in {\mathrm{Base}}_{{w}}⟼\left\{{z}\in {\mathrm{Base}}_{{w}}|\left({z}\in \left({x}{i}{y}\right)\vee {x}\in \left({z}{i}{y}\right)\vee {y}\in \left({x}{i}{z}\right)\right)\right\}\right)⟩$
49 36 48 30 co ${class}\left(\left({w}\mathrm{sSet}⟨\mathrm{Itv}\left(\mathrm{ndx}\right),{i}⟩\right)\mathrm{sSet}⟨{Line}_{𝒢}\left(\mathrm{ndx}\right),\left({x}\in {\mathrm{Base}}_{{w}},{y}\in {\mathrm{Base}}_{{w}}⟼\left\{{z}\in {\mathrm{Base}}_{{w}}|\left({z}\in \left({x}{i}{y}\right)\vee {x}\in \left({z}{i}{y}\right)\vee {y}\in \left({x}{i}{z}\right)\right)\right\}\right)⟩\right)$
50 29 28 49 csb
51 1 2 50 cmpt
52 0 51 wceq