Metamath Proof Explorer

Theorem ttgitvval

Description: Betweenness for a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019)

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

Proof

Step Hyp Ref Expression
1 ttgval.n ${⊢}{G}={to𝒢}_{\mathrm{Tarski}}\left({H}\right)$
2 ttgitvval.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
3 ttgitvval.b ${⊢}{P}={\mathrm{Base}}_{{H}}$
4 ttgitvval.m
5 ttgitvval.s
6 1 3 4 5 2 ttgval
7 6 simprd
9 simprl ${⊢}\left(\left({H}\in {V}\wedge {X}\in {P}\wedge {Y}\in {P}\right)\wedge \left({x}={X}\wedge {y}={Y}\right)\right)\to {x}={X}$
10 9 oveq2d
11 simprr ${⊢}\left(\left({H}\in {V}\wedge {X}\in {P}\wedge {Y}\in {P}\right)\wedge \left({x}={X}\wedge {y}={Y}\right)\right)\to {y}={Y}$
12 11 9 oveq12d
13 12 oveq2d
14 10 13 eqeq12d
15 14 rexbidv
16 15 rabbidv
17 simp2 ${⊢}\left({H}\in {V}\wedge {X}\in {P}\wedge {Y}\in {P}\right)\to {X}\in {P}$
18 simp3 ${⊢}\left({H}\in {V}\wedge {X}\in {P}\wedge {Y}\in {P}\right)\to {Y}\in {P}$
19 3 fvexi ${⊢}{P}\in \mathrm{V}$
20 19 rabex
21 20 a1i
22 8 16 17 18 21 ovmpod