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 bitrdi ⊢ φ → 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