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=BaseH
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∈XIYβ†”βˆƒk∈01Z-Λ™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=BaseH
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β†’XIY=z∈P|βˆƒk∈01z-Λ™X=kΒ·Λ™Y-Λ™X
11 8 6 7 10 syl3anc βŠ’Ο†β†’XIY=z∈P|βˆƒk∈01z-Λ™X=kΒ·Λ™Y-Λ™X
12 11 eleq2d βŠ’Ο†β†’Z∈XIY↔Z∈z∈P|βˆƒk∈01z-Λ™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∈01z-Λ™X=kΒ·Λ™Y-Λ™Xβ†”βˆƒk∈01Z-Λ™X=kΒ·Λ™Y-Λ™X
16 15 elrab ⊒Z∈z∈P|βˆƒk∈01z-Λ™X=kΒ·Λ™Y-Λ™X↔Z∈Pβˆ§βˆƒk∈01Z-Λ™X=kΒ·Λ™Y-Λ™X
17 12 16 bitrdi βŠ’Ο†β†’Z∈XIY↔Z∈Pβˆ§βˆƒk∈01Z-Λ™X=kΒ·Λ™Y-Λ™X
18 9 17 mpbirand βŠ’Ο†β†’Z∈XIYβ†”βˆƒk∈01Z-Λ™X=kΒ·Λ™Y-Λ™X