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 
|- 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 ) ) } ) >. ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cttg 
 |-  toTG
1 vw 
 |-  w
2 cvv 
 |-  _V
3 vx 
 |-  x
4 cbs 
 |-  Base
5 1 cv 
 |-  w
6 5 4 cfv 
 |-  ( Base ` w )
7 vy 
 |-  y
8 vz 
 |-  z
9 vk 
 |-  k
10 cc0 
 |-  0
11 cicc 
 |-  [,]
12 c1 
 |-  1
13 10 12 11 co 
 |-  ( 0 [,] 1 )
14 8 cv 
 |-  z
15 csg 
 |-  -g
16 5 15 cfv 
 |-  ( -g ` w )
17 3 cv 
 |-  x
18 14 17 16 co 
 |-  ( z ( -g ` w ) x )
19 9 cv 
 |-  k
20 cvsca 
 |-  .s
21 5 20 cfv 
 |-  ( .s ` w )
22 7 cv 
 |-  y
23 22 17 16 co 
 |-  ( y ( -g ` w ) x )
24 19 23 21 co 
 |-  ( k ( .s ` w ) ( y ( -g ` w ) x ) )
25 18 24 wceq 
 |-  ( z ( -g ` w ) x ) = ( k ( .s ` w ) ( y ( -g ` w ) x ) )
26 25 9 13 wrex 
 |-  E. k e. ( 0 [,] 1 ) ( z ( -g ` w ) x ) = ( k ( .s ` w ) ( y ( -g ` w ) x ) )
27 26 8 6 crab 
 |-  { z e. ( Base ` w ) | E. k e. ( 0 [,] 1 ) ( z ( -g ` w ) x ) = ( k ( .s ` w ) ( y ( -g ` w ) x ) ) }
28 3 7 6 6 27 cmpo 
 |-  ( 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 ) ) } )
29 vi 
 |-  i
30 csts 
 |-  sSet
31 citv 
 |-  Itv
32 cnx 
 |-  ndx
33 32 31 cfv 
 |-  ( Itv ` ndx )
34 29 cv 
 |-  i
35 33 34 cop 
 |-  <. ( Itv ` ndx ) , i >.
36 5 35 30 co 
 |-  ( w sSet <. ( Itv ` ndx ) , i >. )
37 clng 
 |-  LineG
38 32 37 cfv 
 |-  ( LineG ` ndx )
39 17 22 34 co 
 |-  ( x i y )
40 14 39 wcel 
 |-  z e. ( x i y )
41 14 22 34 co 
 |-  ( z i y )
42 17 41 wcel 
 |-  x e. ( z i y )
43 17 14 34 co 
 |-  ( x i z )
44 22 43 wcel 
 |-  y e. ( x i z )
45 40 42 44 w3o 
 |-  ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) )
46 45 8 6 crab 
 |-  { z e. ( Base ` w ) | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) }
47 3 7 6 6 46 cmpo 
 |-  ( 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 ) ) } )
48 38 47 cop 
 |-  <. ( 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 ) ) } ) >.
49 36 48 30 co 
 |-  ( ( 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 ) ) } ) >. )
50 29 28 49 csb 
 |-  [_ ( 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 ) ) } ) >. )
51 1 2 50 cmpt 
 |-  ( 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 ) ) } ) >. ) )
52 0 51 wceq 
 |-  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 ) ) } ) >. ) )