Definition df-ttg 25754

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 = ( w e. _V |-> [_ ( x e. ( Base ` w ) , y e. ( Base ` w ) |-> { z e. ( Base ` w ) | E. k e. ( 0 [,] 1 ) ( z ( -g ` w ) x ) = ( k ( .s ` w ) ( y ( -g ` w ) x ) ) } ) / i ]_ ( ( w sSet <. (Itv ` ndx ) , i >. ) sSet <. (LineG ` ndx ) , ( x e. ( Base ` w ) , y e. ( Base ` w ) |-> { z e. ( Base ` w ) | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) >. ) )

Distinct variable group:   i, k, w, x, y, z

Detailed syntax breakdown of Definition df-ttg

Step	Hyp	Ref	Expression
1		cttg 25753	. 2 class toTG
2		vw	. . 3 setvar w
3		cvv 3200	. . 3 class _V
4		vi	. . . 4 setvar i
5		vx	. . . . 5 setvar x
6		vy	. . . . 5 setvar y
7	2	cv 1482	. . . . . 6 class w
8		cbs 15857	. . . . . 6 class Base
9	7, 8	cfv 5888	. . . . 5 class ( Base ` w )
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1482	. . . . . . . . 9 class z
12	5	cv 1482	. . . . . . . . 9 class x
13		csg 17424	. . . . . . . . . 10 class -g
14	7, 13	cfv 5888	. . . . . . . . 9 class ( -g ` w )
15	11, 12, 14	co 6650	. . . . . . . 8 class ( z ( -g ` w ) x )
16		vk	. . . . . . . . . 10 setvar k
17	16	cv 1482	. . . . . . . . 9 class k
18	6	cv 1482	. . . . . . . . . 10 class y
19	18, 12, 14	co 6650	. . . . . . . . 9 class ( y ( -g ` w ) x )
20		cvsca 15945	. . . . . . . . . 10 class .s
21	7, 20	cfv 5888	. . . . . . . . 9 class ( .s ` w )
22	17, 19, 21	co 6650	. . . . . . . 8 class ( k ( .s ` w ) ( y ( -g ` w ) x ) )
23	15, 22	wceq 1483	. . . . . . 7 wff ( z ( -g ` w ) x ) = ( k ( .s ` w ) ( y ( -g ` w ) x ) )
24		cc0 9936	. . . . . . . 8 class 0
25		c1 9937	. . . . . . . 8 class 1
26		cicc 12178	. . . . . . . 8 class [,]
27	24, 25, 26	co 6650	. . . . . . 7 class ( 0 [,] 1 )
28	23, 16, 27	wrex 2913	. . . . . 6 wff E. k e. ( 0 [,] 1 ) ( z ( -g ` w ) x ) = ( k ( .s ` w ) ( y ( -g ` w ) x ) )
29	28, 10, 9	crab 2916	. . . . 5 class { z e. ( Base ` w ) | E. k e. ( 0 [,] 1 ) ( z ( -g ` w ) x ) = ( k ( .s ` w ) ( y ( -g ` w ) x ) ) }
30	5, 6, 9, 9, 29	cmpt2 6652	. . . 4 class ( x e. ( Base ` w ) , y e. ( Base ` w ) |-> { z e. ( Base ` w ) | E. k e. ( 0 [,] 1 ) ( z ( -g ` w ) x ) = ( k ( .s ` w ) ( y ( -g ` w ) x ) ) } )
31		cnx 15854	. . . . . . . 8 class ndx
32		citv 25335	. . . . . . . 8 class Itv
33	31, 32	cfv 5888	. . . . . . 7 class (Itv ` ndx )
34	4	cv 1482	. . . . . . 7 class i
35	33, 34	cop 4183	. . . . . 6 class <. (Itv ` ndx ) , i >.
36		csts 15855	. . . . . 6 class sSet
37	7, 35, 36	co 6650	. . . . 5 class ( w sSet <. (Itv ` ndx ) , i >. )
38		clng 25336	. . . . . . 7 class LineG
39	31, 38	cfv 5888	. . . . . 6 class (LineG ` ndx )
40	12, 18, 34	co 6650	. . . . . . . . . 10 class ( x i y )
41	11, 40	wcel 1990	. . . . . . . . 9 wff z e. ( x i y )
42	11, 18, 34	co 6650	. . . . . . . . . 10 class ( z i y )
43	12, 42	wcel 1990	. . . . . . . . 9 wff x e. ( z i y )
44	12, 11, 34	co 6650	. . . . . . . . . 10 class ( x i z )
45	18, 44	wcel 1990	. . . . . . . . 9 wff y e. ( x i z )
46	41, 43, 45	w3o 1036	. . . . . . . 8 wff ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) )
47	46, 10, 9	crab 2916	. . . . . . 7 class { z e. ( Base ` w ) | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) }
48	5, 6, 9, 9, 47	cmpt2 6652	. . . . . 6 class ( x e. ( Base ` w ) , y e. ( Base ` w ) |-> { z e. ( Base ` w ) | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } )
49	39, 48	cop 4183	. . . . 5 class <. (LineG ` ndx ) , ( x e. ( Base ` w ) , y e. ( Base ` w ) |-> { z e. ( Base ` w ) | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) >.
50	37, 49, 36	co 6650	. . . 4 class ( ( w sSet <. (Itv ` ndx ) , i >. ) sSet <. (LineG ` ndx ) , ( x e. ( Base ` w ) , y e. ( Base ` w ) |-> { z e. ( Base ` w ) | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) >. )
51	4, 30, 50	csb 3533	. . 3 class [_ ( x e. ( Base ` w ) , y e. ( Base ` w ) |-> { z e. ( Base ` w ) | E. k e. ( 0 [,] 1 ) ( z ( -g ` w ) x ) = ( k ( .s ` w ) ( y ( -g ` w ) x ) ) } ) / i ]_ ( ( w sSet <. (Itv ` ndx ) , i >. ) sSet <. (LineG ` ndx ) , ( x e. ( Base ` w ) , y e. ( Base ` w ) |-> { z e. ( Base ` w ) | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) >. )
52	2, 3, 51	cmpt 4729	. 2 class ( w e. _V |-> [_ ( x e. ( Base ` w ) , y e. ( Base ` w ) |-> { z e. ( Base ` w ) | E. k e. ( 0 [,] 1 ) ( z ( -g ` w ) x ) = ( k ( .s ` w ) ( y ( -g ` w ) x ) ) } ) / i ]_ ( ( w sSet <. (Itv ` ndx ) , i >. ) sSet <. (LineG ` ndx ) , ( x e. ( Base ` w ) , y e. ( Base ` w ) |-> { z e. ( Base ` w ) | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) >. ) )
53	1, 52	wceq 1483	1 wff toTG = ( w e. _V |-> [_ ( x e. ( Base ` w ) , y e. ( Base ` w ) |-> { z e. ( Base ` w ) | E. k e. ( 0 [,] 1 ) ( z ( -g ` w ) x ) = ( k ( .s ` w ) ( y ( -g ` w ) x ) ) } ) / i ]_ ( ( w sSet <. (Itv ` ndx ) , i >. ) sSet <. (LineG ` ndx ) , ( x e. ( Base ` w ) , y e. ( Base ` w ) |-> { z e. ( Base ` w ) | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) >. ) )

This definition is referenced by:  ttgval  25755