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 = ( toTG ` H )
	ttgitvval.i	|- I = ( Itv ` G )
	ttgitvval.b	|- P = ( Base ` H )
	ttgitvval.m	|- .- = ( -g ` H )
	ttgitvval.s	|- .x. = ( .s ` H )
	ttgelitv.x	|- ( ph -> X e. P )
	ttgelitv.y	|- ( ph -> Y e. P )
	ttgelitv.h	|- ( ph -> H e. V )
	ttgelitv.z	|- ( ph -> Z e. P )
Assertion	ttgelitv	|- ( ph -> ( Z e. ( X I Y ) <-> E. k e. ( 0 [,] 1 ) ( Z .- X ) = ( k .x. ( Y .- X ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ttgval.n	|- G = ( toTG ` H )
2		ttgitvval.i	|- I = ( Itv ` G )
3		ttgitvval.b	|- P = ( Base ` H )
4		ttgitvval.m	|- .- = ( -g ` H )
5		ttgitvval.s	|- .x. = ( .s ` H )
6		ttgelitv.x	|- ( ph -> X e. P )
7		ttgelitv.y	|- ( ph -> Y e. P )
8		ttgelitv.h	|- ( ph -> H e. V )
9		ttgelitv.z	|- ( ph -> Z e. P )
10	1 2 3 4 5	ttgitvval	|- ( ( H e. V /\ X e. P /\ Y e. P ) -> ( X I Y ) = { z e. P | E. k e. ( 0 [,] 1 ) ( z .- X ) = ( k .x. ( Y .- X ) ) } )
11	8 6 7 10	syl3anc	|- ( ph -> ( X I Y ) = { z e. P | E. k e. ( 0 [,] 1 ) ( z .- X ) = ( k .x. ( Y .- X ) ) } )
12	11	eleq2d	|- ( ph -> ( Z e. ( X I Y ) <-> Z e. { z e. P | E. k e. ( 0 [,] 1 ) ( z .- X ) = ( k .x. ( Y .- X ) ) } ) )
13		oveq1	|- ( z = Z -> ( z .- X ) = ( Z .- X ) )
14	13	eqeq1d	|- ( z = Z -> ( ( z .- X ) = ( k .x. ( Y .- X ) ) <-> ( Z .- X ) = ( k .x. ( Y .- X ) ) ) )
15	14	rexbidv	|- ( z = Z -> ( E. k e. ( 0 [,] 1 ) ( z .- X ) = ( k .x. ( Y .- X ) ) <-> E. k e. ( 0 [,] 1 ) ( Z .- X ) = ( k .x. ( Y .- X ) ) ) )
16	15	elrab	|- ( Z e. { z e. P | E. k e. ( 0 [,] 1 ) ( z .- X ) = ( k .x. ( Y .- X ) ) } <-> ( Z e. P /\ E. k e. ( 0 [,] 1 ) ( Z .- X ) = ( k .x. ( Y .- X ) ) ) )
17	12 16	bitrdi	|- ( ph -> ( Z e. ( X I Y ) <-> ( Z e. P /\ E. k e. ( 0 [,] 1 ) ( Z .- X ) = ( k .x. ( Y .- X ) ) ) ) )
18	9 17	mpbirand	|- ( ph -> ( Z e. ( X I Y ) <-> E. k e. ( 0 [,] 1 ) ( Z .- X ) = ( k .x. ( Y .- X ) ) ) )