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 \in V ⟼ ⦋ (x \in {Base}_{w}, y \in {Base}_{w} ⟼ \{z \in {Base}_{w} \| \exists k \in [0, 1] z -_{w} x = k \cdot_{w} (y -_{w} x)\}) / i ⦌ ((w sSet ⟨Itv (ndx), i⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in {Base}_{w}, y \in {Base}_{w} ⟼ \{z \in {Base}_{w} \| (z \in (x i y) \lor x \in (z i y) \lor y \in (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 \cdot_{𝑠}$
21	5 20	cfv	$class \cdot_{w}$
22	7	cv	$setvar y$
23	22 17 16	co	$class (y -_{w} x)$
24	19 23 21	co	$class (k \cdot_{w} (y -_{w} x))$
25	18 24	wceq	$wff z -_{w} x = k \cdot_{w} (y -_{w} x)$
26	25 9 13	wrex	$wff \exists k \in [0, 1] z -_{w} x = k \cdot_{w} (y -_{w} x)$
27	26 8 6	crab	$class \{z \in {Base}_{w} \| \exists k \in [0, 1] z -_{w} x = k \cdot_{w} (y -_{w} x)\}$
28	3 7 6 6 27	cmpo	$class (x \in {Base}_{w}, y \in {Base}_{w} ⟼ \{z \in {Base}_{w} \| \exists k \in [0, 1] z -_{w} x = k \cdot_{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 \in (x i y)$
41	14 22 34	co	$class (z i y)$
42	17 41	wcel	$wff x \in (z i y)$
43	17 14 34	co	$class (x i z)$
44	22 43	wcel	$wff y \in (x i z)$
45	40 42 44	w3o	$wff (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))$
46	45 8 6	crab	$class \{z \in {Base}_{w} \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\}$
47	3 7 6 6 46	cmpo	$class (x \in {Base}_{w}, y \in {Base}_{w} ⟼ \{z \in {Base}_{w} \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})$
48	38 47	cop	$class ⟨{Line}_{𝒢} (ndx), (x \in {Base}_{w}, y \in {Base}_{w} ⟼ \{z \in {Base}_{w} \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})⟩$
49	36 48 30	co	$class ((w sSet ⟨Itv (ndx), i⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in {Base}_{w}, y \in {Base}_{w} ⟼ \{z \in {Base}_{w} \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})⟩)$
50	29 28 49	csb	$class ⦋ (x \in {Base}_{w}, y \in {Base}_{w} ⟼ \{z \in {Base}_{w} \| \exists k \in [0, 1] z -_{w} x = k \cdot_{w} (y -_{w} x)\}) / i ⦌ ((w sSet ⟨Itv (ndx), i⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in {Base}_{w}, y \in {Base}_{w} ⟼ \{z \in {Base}_{w} \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})⟩)$
51	1 2 50	cmpt	$class (w \in V ⟼ ⦋ (x \in {Base}_{w}, y \in {Base}_{w} ⟼ \{z \in {Base}_{w} \| \exists k \in [0, 1] z -_{w} x = k \cdot_{w} (y -_{w} x)\}) / i ⦌ ((w sSet ⟨Itv (ndx), i⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in {Base}_{w}, y \in {Base}_{w} ⟼ \{z \in {Base}_{w} \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})⟩))$
52	0 51	wceq	$wff {to𝒢}_{Tarski} = (w \in V ⟼ ⦋ (x \in {Base}_{w}, y \in {Base}_{w} ⟼ \{z \in {Base}_{w} \| \exists k \in [0, 1] z -_{w} x = k \cdot_{w} (y -_{w} x)\}) / i ⦌ ((w sSet ⟨Itv (ndx), i⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in {Base}_{w}, y \in {Base}_{w} ⟼ \{z \in {Base}_{w} \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})⟩))$

Metamath Proof Explorer

Definition df-ttg

Detailed syntax breakdown