Metamath Proof Explorer

Theorem ttgitvval

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 )
Assertion 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 ) ) } )

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 1 3 4 5 2 ttgval 
 |-  ( H e. V -> ( G = ( ( H sSet <. ( Itv ` ndx ) , ( x e. P , y e. P |-> { z e. P | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) >. ) sSet <. ( LineG ` ndx ) , ( x e. P , y e. P |-> { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) >. ) /\ I = ( x e. P , y e. P |-> { z e. P | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) ) )
7 6 simprd 
 |-  ( H e. V -> I = ( x e. P , y e. P |-> { z e. P | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) )
8 7 3ad2ant1 
 |-  ( ( H e. V /\ X e. P /\ Y e. P ) -> I = ( x e. P , y e. P |-> { z e. P | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) )
9 simprl 
 |-  ( ( ( H e. V /\ X e. P /\ Y e. P ) /\ ( x = X /\ y = Y ) ) -> x = X )
10 9 oveq2d 
 |-  ( ( ( H e. V /\ X e. P /\ Y e. P ) /\ ( x = X /\ y = Y ) ) -> ( z .- x ) = ( z .- X ) )
11 simprr 
 |-  ( ( ( H e. V /\ X e. P /\ Y e. P ) /\ ( x = X /\ y = Y ) ) -> y = Y )
12 11 9 oveq12d 
 |-  ( ( ( H e. V /\ X e. P /\ Y e. P ) /\ ( x = X /\ y = Y ) ) -> ( y .- x ) = ( Y .- X ) )
13 12 oveq2d 
 |-  ( ( ( H e. V /\ X e. P /\ Y e. P ) /\ ( x = X /\ y = Y ) ) -> ( k .x. ( y .- x ) ) = ( k .x. ( Y .- X ) ) )
14 10 13 eqeq12d 
 |-  ( ( ( H e. V /\ X e. P /\ Y e. P ) /\ ( x = X /\ y = Y ) ) -> ( ( z .- x ) = ( k .x. ( y .- x ) ) <-> ( z .- X ) = ( k .x. ( Y .- X ) ) ) )
15 14 rexbidv 
 |-  ( ( ( H e. V /\ X e. P /\ Y e. P ) /\ ( x = X /\ y = Y ) ) -> ( E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) <-> E. k e. ( 0 [,] 1 ) ( z .- X ) = ( k .x. ( Y .- X ) ) ) )
16 15 rabbidv 
 |-  ( ( ( H e. V /\ X e. P /\ Y e. P ) /\ ( x = X /\ y = Y ) ) -> { 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 simp2 
 |-  ( ( H e. V /\ X e. P /\ Y e. P ) -> X e. P )
18 simp3 
 |-  ( ( H e. V /\ X e. P /\ Y e. P ) -> Y e. P )
19 3 fvexi 
 |-  P e. _V
20 19 rabex 
 |-  { z e. P | E. k e. ( 0 [,] 1 ) ( z .- X ) = ( k .x. ( Y .- X ) ) } e. _V
21 20 a1i 
 |-  ( ( H e. V /\ X e. P /\ Y e. P ) -> { z e. P | E. k e. ( 0 [,] 1 ) ( z .- X ) = ( k .x. ( Y .- X ) ) } e. _V )
22 8 16 17 18 21 ovmpod 
 |-  ( ( 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 ) ) } )