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 = { 1 , 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 ` 1 ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) /\ ( p ` 2 ) = ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) ) } )

Proof

Step Hyp Ref Expression
1 rrx2line.i 
 |-  I = { 1 , 2 }
2 rrx2line.e 
 |-  E = ( RR^ ` I )
3 rrx2line.b 
 |-  P = ( RR ^m I )
4 rrx2line.l 
 |-  L = ( LineM ` E )
5 prfi 
 |-  { 1 , 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 1 a1i 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ t e. RR ) -> I = { 1 , 2 } )
10 9 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. { 1 , 2 } ( p ` i ) = ( ( ( 1 - t ) x. ( X ` i ) ) + ( t x. ( Y ` i ) ) ) ) )
11 1ex 
 |-  1 e. _V
12 2ex 
 |-  2 e. _V
13 fveq2 
 |-  ( i = 1 -> ( p ` i ) = ( p ` 1 ) )
14 fveq2 
 |-  ( i = 1 -> ( X ` i ) = ( X ` 1 ) )
15 14 oveq2d 
 |-  ( i = 1 -> ( ( 1 - t ) x. ( X ` i ) ) = ( ( 1 - t ) x. ( X ` 1 ) ) )
16 fveq2 
 |-  ( i = 1 -> ( Y ` i ) = ( Y ` 1 ) )
17 16 oveq2d 
 |-  ( i = 1 -> ( t x. ( Y ` i ) ) = ( t x. ( Y ` 1 ) ) )
18 15 17 oveq12d 
 |-  ( i = 1 -> ( ( ( 1 - t ) x. ( X ` i ) ) + ( t x. ( Y ` i ) ) ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) )
19 13 18 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 ) ) ) ) )
20 fveq2 
 |-  ( i = 2 -> ( p ` i ) = ( p ` 2 ) )
21 fveq2 
 |-  ( i = 2 -> ( X ` i ) = ( X ` 2 ) )
22 21 oveq2d 
 |-  ( i = 2 -> ( ( 1 - t ) x. ( X ` i ) ) = ( ( 1 - t ) x. ( X ` 2 ) ) )
23 fveq2 
 |-  ( i = 2 -> ( Y ` i ) = ( Y ` 2 ) )
24 23 oveq2d 
 |-  ( i = 2 -> ( t x. ( Y ` i ) ) = ( t x. ( Y ` 2 ) ) )
25 22 24 oveq12d 
 |-  ( i = 2 -> ( ( ( 1 - t ) x. ( X ` i ) ) + ( t x. ( Y ` i ) ) ) = ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) )
26 20 25 eqeq12d 
 |-  ( i = 2 -> ( ( p ` i ) = ( ( ( 1 - t ) x. ( X ` i ) ) + ( t x. ( Y ` i ) ) ) <-> ( p ` 2 ) = ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) ) )
27 11 12 19 26 ralpr 
 |-  ( A. i e. { 1 , 2 } ( p ` i ) = ( ( ( 1 - t ) x. ( X ` i ) ) + ( t x. ( Y ` i ) ) ) <-> ( ( p ` 1 ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) /\ ( p ` 2 ) = ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) ) )
28 10 27 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 ` 1 ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) /\ ( p ` 2 ) = ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) ) ) )
29 28 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 ` 1 ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) /\ ( p ` 2 ) = ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) ) ) )
30 29 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 ` 1 ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) /\ ( p ` 2 ) = ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) ) } )
31 8 30 eqtrd 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X L Y ) = { p e. P | E. t e. RR ( ( p ` 1 ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) /\ ( p ` 2 ) = ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) ) } )