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 = ( 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 ) ) ) )