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 ⊢ to𝒢 Tarski = w ∈ V ⟼ ⦋ x ∈ Base w , y ∈ Base w ⟼ z ∈ Base w | ∃ k ∈ 0 1 z - w x = k ⋅ w y - w x / i⦌ w sSet Itv ⁡ ndx i sSet Line 𝒢 ⁡ ndx x ∈ Base w , y ∈ Base w ⟼ z ∈ Base w | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cttg class to𝒢 Tarski
1 vw setvar w
2 cvv class V
3 vx setvar x
4 cbs class Base
5 1 cv setvar w
6 5 4 cfv class Base w
7 vy setvar y
8 vz setvar z
9 vk setvar k
10 cc0 class 0
11 cicc class .
12 c1 class 1
13 10 12 11 co class 0 1
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 z - w x
19 9 cv setvar k
20 cvsca class ⋅ 𝑠
21 5 20 cfv class ⋅ w
22 7 cv setvar y
23 22 17 16 co class y - w x
24 19 23 21 co class k ⋅ w y - w x
25 18 24 wceq wff z - w x = k ⋅ w y - w x
26 25 9 13 wrex wff ∃ k ∈ 0 1 z - w x = k ⋅ w y - w x
27 26 8 6 crab class z ∈ Base w | ∃ k ∈ 0 1 z - w x = k ⋅ w y - w x
28 3 7 6 6 27 cmpo class x ∈ Base w , y ∈ Base w ⟼ z ∈ Base w | ∃ k ∈ 0 1 z - w x = k ⋅ w y - w x
29 vi setvar i
30 csts class sSet
31 citv class Itv
32 cnx class ndx
33 32 31 cfv class Itv ⁡ ndx
34 29 cv setvar i
35 33 34 cop class Itv ⁡ ndx i
36 5 35 30 co class w sSet Itv ⁡ ndx i
37 clng class Line 𝒢
38 32 37 cfv class Line 𝒢 ⁡ ndx
39 17 22 34 co class x i y
40 14 39 wcel wff z ∈ x i y
41 14 22 34 co class z i y
42 17 41 wcel wff x ∈ z i y
43 17 14 34 co class x i z
44 22 43 wcel wff y ∈ x i z
45 40 42 44 w3o wff z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
46 45 8 6 crab class z ∈ Base w | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
47 3 7 6 6 46 cmpo class x ∈ Base w , y ∈ Base w ⟼ z ∈ Base w | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
48 38 47 cop class Line 𝒢 ⁡ ndx x ∈ Base w , y ∈ Base w ⟼ z ∈ Base w | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
49 36 48 30 co class w sSet Itv ⁡ ndx i sSet Line 𝒢 ⁡ ndx x ∈ Base w , y ∈ Base w ⟼ z ∈ Base w | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
50 29 28 49 csb class ⦋ x ∈ Base w , y ∈ Base w ⟼ z ∈ Base w | ∃ k ∈ 0 1 z - w x = k ⋅ w y - w x / i⦌ w sSet Itv ⁡ ndx i sSet Line 𝒢 ⁡ ndx x ∈ Base w , y ∈ Base w ⟼ z ∈ Base w | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
51 1 2 50 cmpt class w ∈ V ⟼ ⦋ x ∈ Base w , y ∈ Base w ⟼ z ∈ Base w | ∃ k ∈ 0 1 z - w x = k ⋅ w y - w x / i⦌ w sSet Itv ⁡ ndx i sSet Line 𝒢 ⁡ ndx x ∈ Base w , y ∈ Base w ⟼ z ∈ Base w | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
52 0 51 wceq wff to𝒢 Tarski = w ∈ V ⟼ ⦋ x ∈ Base w , y ∈ Base w ⟼ z ∈ Base w | ∃ k ∈ 0 1 z - w x = k ⋅ w y - w x / i⦌ w sSet Itv ⁡ ndx i sSet Line 𝒢 ⁡ ndx x ∈ Base w , y ∈ Base w ⟼ z ∈ Base w | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z