Metamath Proof Explorer


Theorem ttgelitv

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

Ref Expression
Hypotheses ttgval.n G = to𝒢 Tarski H
ttgitvval.i I = Itv G
ttgitvval.b P = Base H
ttgitvval.m - ˙ = - H
ttgitvval.s · ˙ = H
ttgelitv.x φ X P
ttgelitv.y φ Y P
ttgelitv.h φ H V
ttgelitv.z φ Z P
Assertion ttgelitv φ Z X I Y k 0 1 Z - ˙ X = k · ˙ Y - ˙ X

Proof

Step Hyp Ref Expression
1 ttgval.n G = to𝒢 Tarski H
2 ttgitvval.i I = Itv G
3 ttgitvval.b P = Base H
4 ttgitvval.m - ˙ = - H
5 ttgitvval.s · ˙ = H
6 ttgelitv.x φ X P
7 ttgelitv.y φ Y P
8 ttgelitv.h φ H V
9 ttgelitv.z φ Z P
10 1 2 3 4 5 ttgitvval H V X P Y P X I Y = z P | k 0 1 z - ˙ X = k · ˙ Y - ˙ X
11 8 6 7 10 syl3anc φ X I Y = z P | k 0 1 z - ˙ X = k · ˙ Y - ˙ X
12 11 eleq2d φ Z X I Y Z z P | k 0 1 z - ˙ X = k · ˙ Y - ˙ X
13 oveq1 z = Z z - ˙ X = Z - ˙ X
14 13 eqeq1d z = Z z - ˙ X = k · ˙ Y - ˙ X Z - ˙ X = k · ˙ Y - ˙ X
15 14 rexbidv z = Z k 0 1 z - ˙ X = k · ˙ Y - ˙ X k 0 1 Z - ˙ X = k · ˙ Y - ˙ X
16 15 elrab Z z P | k 0 1 z - ˙ X = k · ˙ Y - ˙ X Z P k 0 1 Z - ˙ X = k · ˙ Y - ˙ X
17 12 16 syl6bb φ Z X I Y Z P k 0 1 Z - ˙ X = k · ˙ Y - ˙ X
18 9 17 mpbirand φ Z X I Y k 0 1 Z - ˙ X = k · ˙ Y - ˙ X