# Metamath Proof Explorer

## Theorem ttgval

Description: Define a function to augment a subcomplex Hilbert space with betweenness and a line definition. (Contributed by Thierry Arnoux, 25-Mar-2019)

Ref Expression
Hypotheses ttgval.n ${⊢}{G}={to𝒢}_{\mathrm{Tarski}}\left({H}\right)$
ttgval.b ${⊢}{B}={\mathrm{Base}}_{{H}}$
ttgval.m
ttgval.s
ttgval.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
Assertion ttgval

### Proof

Step Hyp Ref Expression
1 ttgval.n ${⊢}{G}={to𝒢}_{\mathrm{Tarski}}\left({H}\right)$
2 ttgval.b ${⊢}{B}={\mathrm{Base}}_{{H}}$
3 ttgval.m
4 ttgval.s
5 ttgval.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
6 1 a1i ${⊢}{H}\in {V}\to {G}={to𝒢}_{\mathrm{Tarski}}\left({H}\right)$
7 elex ${⊢}{H}\in {V}\to {H}\in \mathrm{V}$
8 fveq2 ${⊢}{w}={H}\to {\mathrm{Base}}_{{w}}={\mathrm{Base}}_{{H}}$
9 8 2 eqtr4di ${⊢}{w}={H}\to {\mathrm{Base}}_{{w}}={B}$
10 fveq2 ${⊢}{w}={H}\to {-}_{{w}}={-}_{{H}}$
11 10 3 eqtr4di
12 11 oveqd
13 fveq2 ${⊢}{w}={H}\to {\cdot }_{{w}}={\cdot }_{{H}}$
14 13 4 eqtr4di
15 eqidd ${⊢}{w}={H}\to {k}={k}$
16 11 oveqd
17 14 15 16 oveq123d
18 12 17 eqeq12d
19 18 rexbidv
20 9 19 rabeqbidv
21 9 9 20 mpoeq123dv
22 21 csbeq1d
23 oveq1 ${⊢}{w}={H}\to {w}\mathrm{sSet}⟨\mathrm{Itv}\left(\mathrm{ndx}\right),{i}⟩={H}\mathrm{sSet}⟨\mathrm{Itv}\left(\mathrm{ndx}\right),{i}⟩$
24 9 rabeqdv ${⊢}{w}={H}\to \left\{{z}\in {\mathrm{Base}}_{{w}}|\left({z}\in \left({x}{i}{y}\right)\vee {x}\in \left({z}{i}{y}\right)\vee {y}\in \left({x}{i}{z}\right)\right)\right\}=\left\{{z}\in {B}|\left({z}\in \left({x}{i}{y}\right)\vee {x}\in \left({z}{i}{y}\right)\vee {y}\in \left({x}{i}{z}\right)\right)\right\}$
25 9 9 24 mpoeq123dv ${⊢}{w}={H}\to \left({x}\in {\mathrm{Base}}_{{w}},{y}\in {\mathrm{Base}}_{{w}}⟼\left\{{z}\in {\mathrm{Base}}_{{w}}|\left({z}\in \left({x}{i}{y}\right)\vee {x}\in \left({z}{i}{y}\right)\vee {y}\in \left({x}{i}{z}\right)\right)\right\}\right)=\left({x}\in {B},{y}\in {B}⟼\left\{{z}\in {B}|\left({z}\in \left({x}{i}{y}\right)\vee {x}\in \left({z}{i}{y}\right)\vee {y}\in \left({x}{i}{z}\right)\right)\right\}\right)$
26 25 opeq2d ${⊢}{w}={H}\to ⟨{Line}_{𝒢}\left(\mathrm{ndx}\right),\left({x}\in {\mathrm{Base}}_{{w}},{y}\in {\mathrm{Base}}_{{w}}⟼\left\{{z}\in {\mathrm{Base}}_{{w}}|\left({z}\in \left({x}{i}{y}\right)\vee {x}\in \left({z}{i}{y}\right)\vee {y}\in \left({x}{i}{z}\right)\right)\right\}\right)⟩=⟨{Line}_{𝒢}\left(\mathrm{ndx}\right),\left({x}\in {B},{y}\in {B}⟼\left\{{z}\in {B}|\left({z}\in \left({x}{i}{y}\right)\vee {x}\in \left({z}{i}{y}\right)\vee {y}\in \left({x}{i}{z}\right)\right)\right\}\right)⟩$
27 23 26 oveq12d ${⊢}{w}={H}\to \left({w}\mathrm{sSet}⟨\mathrm{Itv}\left(\mathrm{ndx}\right),{i}⟩\right)\mathrm{sSet}⟨{Line}_{𝒢}\left(\mathrm{ndx}\right),\left({x}\in {\mathrm{Base}}_{{w}},{y}\in {\mathrm{Base}}_{{w}}⟼\left\{{z}\in {\mathrm{Base}}_{{w}}|\left({z}\in \left({x}{i}{y}\right)\vee {x}\in \left({z}{i}{y}\right)\vee {y}\in \left({x}{i}{z}\right)\right)\right\}\right)⟩=\left({H}\mathrm{sSet}⟨\mathrm{Itv}\left(\mathrm{ndx}\right),{i}⟩\right)\mathrm{sSet}⟨{Line}_{𝒢}\left(\mathrm{ndx}\right),\left({x}\in {B},{y}\in {B}⟼\left\{{z}\in {B}|\left({z}\in \left({x}{i}{y}\right)\vee {x}\in \left({z}{i}{y}\right)\vee {y}\in \left({x}{i}{z}\right)\right)\right\}\right)⟩$
28 27 csbeq2dv
29 22 28 eqtrd
30 df-ttg
31 ovex ${⊢}\left({H}\mathrm{sSet}⟨\mathrm{Itv}\left(\mathrm{ndx}\right),{i}⟩\right)\mathrm{sSet}⟨{Line}_{𝒢}\left(\mathrm{ndx}\right),\left({x}\in {B},{y}\in {B}⟼\left\{{z}\in {B}|\left({z}\in \left({x}{i}{y}\right)\vee {x}\in \left({z}{i}{y}\right)\vee {y}\in \left({x}{i}{z}\right)\right)\right\}\right)⟩\in \mathrm{V}$
32 31 csbex
33 29 30 32 fvmpt
34 7 33 syl
35 2 fvexi ${⊢}{B}\in \mathrm{V}$
36 35 35 mpoex
37 36 a1i
38 simpr
39 oveq2
40 oveq2
41 40 oveq2d
42 39 41 eqeq12d
43 42 rexbidv
44 43 rabbidv
45 oveq1
46 45 oveq2d
47 46 eqeq2d
48 47 rexbidv
49 48 rabbidv
50 oveq1
51 50 eqeq1d
52 51 rexbidv
53 52 cbvrabv
54 49 53 eqtrdi
55 44 54 cbvmpov
56 38 55 eqtr4di
57 simpr
58 57 55 eqtrdi
59 58 opeq2d
60 59 oveq2d
61 58 oveqd
62 61 eleq2d
63 58 oveqd
64 63 eleq2d
65 58 oveqd
66 65 eleq2d
67 62 64 66 3orbi123d
68 67 rabbidv
69 68 mpoeq3dv
70 69 opeq2d
71 60 70 oveq12d
72 56 71 syldan
73 37 72 csbied
74 6 34 73 3eqtrd
75 74 fveq2d
76 itvid ${⊢}\mathrm{Itv}=\mathrm{Slot}\mathrm{Itv}\left(\mathrm{ndx}\right)$
77 1nn0 ${⊢}1\in {ℕ}_{0}$
78 6nn ${⊢}6\in ℕ$
79 77 78 decnncl ${⊢}16\in ℕ$
80 79 nnrei ${⊢}16\in ℝ$
81 6nn0 ${⊢}6\in {ℕ}_{0}$
82 7nn ${⊢}7\in ℕ$
83 6lt7 ${⊢}6<7$
84 77 81 82 83 declt ${⊢}16<17$
85 80 84 ltneii ${⊢}16\ne 17$
86 itvndx ${⊢}\mathrm{Itv}\left(\mathrm{ndx}\right)=16$
87 lngndx ${⊢}{Line}_{𝒢}\left(\mathrm{ndx}\right)=17$
88 86 87 neeq12i ${⊢}\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {Line}_{𝒢}\left(\mathrm{ndx}\right)↔16\ne 17$
89 85 88 mpbir ${⊢}\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {Line}_{𝒢}\left(\mathrm{ndx}\right)$
90 76 89 setsnid
91 75 90 eqtr4di
92 5 a1i ${⊢}{H}\in {V}\to {I}=\mathrm{Itv}\left({G}\right)$
93 76 setsid
94 36 93 mpan2
95 91 92 94 3eqtr4d
96 95 oveqd
97 96 eleq2d
98 95 oveqd
99 98 eleq2d
100 95 oveqd
101 100 eleq2d
102 97 99 101 3orbi123d
103 102 rabbidv
104 103 mpoeq3dv
105 104 opeq2d
106 105 oveq2d
107 74 106 eqtr4d
108 107 95 jca