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

Detailed syntax breakdown

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