Metamath Proof Explorer

Theorem rrx2line

Description: The line passing through the two different points X and Y in a real Euclidean space of dimension 2. (Contributed by AV, 22-Jan-2023) (Proof shortened by AV, 13-Feb-2023)

Ref Expression
Hypotheses rrx2line.i 
|- I = ( 0 ..^ 2 )
rrx2line.e 
|- E = ( RR^ ` I )
rrx2line.b 
|- P = ( RR ^m I )
rrx2line.l 
|- L = ( LineM ` E )
Assertion rrx2line 
|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X L Y ) = { p e. P | E. t e. RR ( ( p ` 0 ) = ( ( ( 1 - t ) x. ( X ` 0 ) ) + ( t x. ( Y ` 0 ) ) ) /\ ( p ` 1 ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) ) } )

Proof

Step Hyp Ref Expression
1 rrx2line.i 
 |-  I = ( 0 ..^ 2 )
2 rrx2line.e 
 |-  E = ( RR^ ` I )
3 rrx2line.b 
 |-  P = ( RR ^m I )
4 rrx2line.l 
 |-  L = ( LineM ` E )
5 fzofi 
 |-  ( 0 ..^ 2 ) e. Fin
6 1 5 eqeltri 
 |-  I e. Fin
7 2 3 4 rrxlinec 
 |-  ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) -> ( X L Y ) = { p e. P | E. t e. RR A. i e. I ( p ` i ) = ( ( ( 1 - t ) x. ( X ` i ) ) + ( t x. ( Y ` i ) ) ) } )
8 6 7 mpan 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X L Y ) = { p e. P | E. t e. RR A. i e. I ( p ` i ) = ( ( ( 1 - t ) x. ( X ` i ) ) + ( t x. ( Y ` i ) ) ) } )
9 fzo0to2pr 
 |-  ( 0 ..^ 2 ) = { 0 , 1 }
10 1 9 eqtri 
 |-  I = { 0 , 1 }
11 10 a1i 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ t e. RR ) -> I = { 0 , 1 } )
12 11 raleqdv 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ t e. RR ) -> ( A. i e. I ( p ` i ) = ( ( ( 1 - t ) x. ( X ` i ) ) + ( t x. ( Y ` i ) ) ) <-> A. i e. { 0 , 1 } ( p ` i ) = ( ( ( 1 - t ) x. ( X ` i ) ) + ( t x. ( Y ` i ) ) ) ) )
13 c0ex 
 |-  0 e. _V
14 1ex 
 |-  1 e. _V
15 fveq2 
 |-  ( i = 0 -> ( p ` i ) = ( p ` 0 ) )
16 fveq2 
 |-  ( i = 0 -> ( X ` i ) = ( X ` 0 ) )
17 16 oveq2d 
 |-  ( i = 0 -> ( ( 1 - t ) x. ( X ` i ) ) = ( ( 1 - t ) x. ( X ` 0 ) ) )
18 fveq2 
 |-  ( i = 0 -> ( Y ` i ) = ( Y ` 0 ) )
19 18 oveq2d 
 |-  ( i = 0 -> ( t x. ( Y ` i ) ) = ( t x. ( Y ` 0 ) ) )
20 17 19 oveq12d 
 |-  ( i = 0 -> ( ( ( 1 - t ) x. ( X ` i ) ) + ( t x. ( Y ` i ) ) ) = ( ( ( 1 - t ) x. ( X ` 0 ) ) + ( t x. ( Y ` 0 ) ) ) )
21 15 20 eqeq12d 
 |-  ( i = 0 -> ( ( p ` i ) = ( ( ( 1 - t ) x. ( X ` i ) ) + ( t x. ( Y ` i ) ) ) <-> ( p ` 0 ) = ( ( ( 1 - t ) x. ( X ` 0 ) ) + ( t x. ( Y ` 0 ) ) ) ) )
22 fveq2 
 |-  ( i = 1 -> ( p ` i ) = ( p ` 1 ) )
23 fveq2 
 |-  ( i = 1 -> ( X ` i ) = ( X ` 1 ) )
24 23 oveq2d 
 |-  ( i = 1 -> ( ( 1 - t ) x. ( X ` i ) ) = ( ( 1 - t ) x. ( X ` 1 ) ) )
25 fveq2 
 |-  ( i = 1 -> ( Y ` i ) = ( Y ` 1 ) )
26 25 oveq2d 
 |-  ( i = 1 -> ( t x. ( Y ` i ) ) = ( t x. ( Y ` 1 ) ) )
27 24 26 oveq12d 
 |-  ( i = 1 -> ( ( ( 1 - t ) x. ( X ` i ) ) + ( t x. ( Y ` i ) ) ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) )
28 22 27 eqeq12d 
 |-  ( i = 1 -> ( ( p ` i ) = ( ( ( 1 - t ) x. ( X ` i ) ) + ( t x. ( Y ` i ) ) ) <-> ( p ` 1 ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) ) )
29 13 14 21 28 ralpr 
 |-  ( A. i e. { 0 , 1 } ( p ` i ) = ( ( ( 1 - t ) x. ( X ` i ) ) + ( t x. ( Y ` i ) ) ) <-> ( ( p ` 0 ) = ( ( ( 1 - t ) x. ( X ` 0 ) ) + ( t x. ( Y ` 0 ) ) ) /\ ( p ` 1 ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) ) )
30 12 29 bitrdi 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ t e. RR ) -> ( A. i e. I ( p ` i ) = ( ( ( 1 - t ) x. ( X ` i ) ) + ( t x. ( Y ` i ) ) ) <-> ( ( p ` 0 ) = ( ( ( 1 - t ) x. ( X ` 0 ) ) + ( t x. ( Y ` 0 ) ) ) /\ ( p ` 1 ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) ) ) )
31 30 rexbidva 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( E. t e. RR A. i e. I ( p ` i ) = ( ( ( 1 - t ) x. ( X ` i ) ) + ( t x. ( Y ` i ) ) ) <-> E. t e. RR ( ( p ` 0 ) = ( ( ( 1 - t ) x. ( X ` 0 ) ) + ( t x. ( Y ` 0 ) ) ) /\ ( p ` 1 ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) ) ) )
32 31 rabbidva 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> { p e. P | E. t e. RR A. i e. I ( p ` i ) = ( ( ( 1 - t ) x. ( X ` i ) ) + ( t x. ( Y ` i ) ) ) } = { p e. P | E. t e. RR ( ( p ` 0 ) = ( ( ( 1 - t ) x. ( X ` 0 ) ) + ( t x. ( Y ` 0 ) ) ) /\ ( p ` 1 ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) ) } )
33 8 32 eqtrd 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X L Y ) = { p e. P | E. t e. RR ( ( p ` 0 ) = ( ( ( 1 - t ) x. ( X ` 0 ) ) + ( t x. ( Y ` 0 ) ) ) /\ ( p ` 1 ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) ) } )