Definition df-ttg 28882

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 = (𝑤 ∈ V ↦ ⦋(𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝑤)𝑥) = (𝑘( ·𝑠 ‘𝑤)(𝑦(-g‘𝑤)𝑥))}) / 𝑖⦌((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))

Distinct variable group:   𝑖,𝑘,𝑤,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-ttg

Step	Hyp	Ref	Expression
1		cttg 28881	. 2 class toTG
2		vw	. . 3 setvar 𝑤
3		cvv 3480	. . 3 class V
4		vi	. . . 4 setvar 𝑖
5		vx	. . . . 5 setvar 𝑥
6		vy	. . . . 5 setvar 𝑦
7	2	cv 1539	. . . . . 6 class 𝑤
8		cbs 17247	. . . . . 6 class Base
9	7, 8	cfv 6561	. . . . 5 class (Base‘𝑤)
10		vz	. . . . . . . . . 10 setvar 𝑧
11	10	cv 1539	. . . . . . . . 9 class 𝑧
12	5	cv 1539	. . . . . . . . 9 class 𝑥
13		csg 18953	. . . . . . . . . 10 class -g
14	7, 13	cfv 6561	. . . . . . . . 9 class (-g‘𝑤)
15	11, 12, 14	co 7431	. . . . . . . 8 class (𝑧(-g‘𝑤)𝑥)
16		vk	. . . . . . . . . 10 setvar 𝑘
17	16	cv 1539	. . . . . . . . 9 class 𝑘
18	6	cv 1539	. . . . . . . . . 10 class 𝑦
19	18, 12, 14	co 7431	. . . . . . . . 9 class (𝑦(-g‘𝑤)𝑥)
20		cvsca 17301	. . . . . . . . . 10 class ·𝑠
21	7, 20	cfv 6561	. . . . . . . . 9 class ( ·𝑠 ‘𝑤)
22	17, 19, 21	co 7431	. . . . . . . 8 class (𝑘( ·𝑠 ‘𝑤)(𝑦(-g‘𝑤)𝑥))
23	15, 22	wceq 1540	. . . . . . 7 wff (𝑧(-g‘𝑤)𝑥) = (𝑘( ·𝑠 ‘𝑤)(𝑦(-g‘𝑤)𝑥))
24		cc0 11155	. . . . . . . 8 class 0
25		c1 11156	. . . . . . . 8 class 1
26		cicc 13390	. . . . . . . 8 class [,]
27	24, 25, 26	co 7431	. . . . . . 7 class (0[,]1)
28	23, 16, 27	wrex 3070	. . . . . 6 wff ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝑤)𝑥) = (𝑘( ·𝑠 ‘𝑤)(𝑦(-g‘𝑤)𝑥))
29	28, 10, 9	crab 3436	. . . . 5 class {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝑤)𝑥) = (𝑘( ·𝑠 ‘𝑤)(𝑦(-g‘𝑤)𝑥))}
30	5, 6, 9, 9, 29	cmpo 7433	. . . 4 class (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝑤)𝑥) = (𝑘( ·𝑠 ‘𝑤)(𝑦(-g‘𝑤)𝑥))})
31		cnx 17230	. . . . . . . 8 class ndx
32		citv 28441	. . . . . . . 8 class Itv
33	31, 32	cfv 6561	. . . . . . 7 class (Itv‘ndx)
34	4	cv 1539	. . . . . . 7 class 𝑖
35	33, 34	cop 4632	. . . . . 6 class ⟨(Itv‘ndx), 𝑖⟩
36		csts 17200	. . . . . 6 class sSet
37	7, 35, 36	co 7431	. . . . 5 class (𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩)
38		clng 28442	. . . . . . 7 class LineG
39	31, 38	cfv 6561	. . . . . 6 class (LineG‘ndx)
40	12, 18, 34	co 7431	. . . . . . . . . 10 class (𝑥𝑖𝑦)
41	11, 40	wcel 2108	. . . . . . . . 9 wff 𝑧 ∈ (𝑥𝑖𝑦)
42	11, 18, 34	co 7431	. . . . . . . . . 10 class (𝑧𝑖𝑦)
43	12, 42	wcel 2108	. . . . . . . . 9 wff 𝑥 ∈ (𝑧𝑖𝑦)
44	12, 11, 34	co 7431	. . . . . . . . . 10 class (𝑥𝑖𝑧)
45	18, 44	wcel 2108	. . . . . . . . 9 wff 𝑦 ∈ (𝑥𝑖𝑧)
46	41, 43, 45	w3o 1086	. . . . . . . 8 wff (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))
47	46, 10, 9	crab 3436	. . . . . . 7 class {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}
48	5, 6, 9, 9, 47	cmpo 7433	. . . . . 6 class (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})
49	39, 48	cop 4632	. . . . 5 class ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩
50	37, 49, 36	co 7431	. . . 4 class ((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩)
51	4, 30, 50	csb 3899	. . 3 class ⦋(𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝑤)𝑥) = (𝑘( ·𝑠 ‘𝑤)(𝑦(-g‘𝑤)𝑥))}) / 𝑖⦌((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩)
52	2, 3, 51	cmpt 5225	. 2 class (𝑤 ∈ V ↦ ⦋(𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝑤)𝑥) = (𝑘( ·𝑠 ‘𝑤)(𝑦(-g‘𝑤)𝑥))}) / 𝑖⦌((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
53	1, 52	wceq 1540	1 wff toTG = (𝑤 ∈ V ↦ ⦋(𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝑤)𝑥) = (𝑘( ·𝑠 ‘𝑤)(𝑦(-g‘𝑤)𝑥))}) / 𝑖⦌((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))

This definition is referenced by:  ttgval  28883  ttgvalOLD  28884