Metamath Proof Explorer

Theorem rrx2linesl

Description: The line passing through the two different points X and Y in a real Euclidean space of dimension 2, expressed by the slope S between the two points ("point-slope form"), sometimes also written as ( ( p2 ) - ( X2 ) ) = ( S x. ( ( p1 ) - ( X1 ) ) ) . (Contributed by AV, 22-Jan-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 )
rrx2linesl.s 
|- S = ( ( ( Y ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 1 ) - ( X ` 1 ) ) )
Assertion rrx2linesl 
|- ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( X L Y ) = { p e. P | ( p ` 2 ) = ( ( S x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( X ` 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 rrx2linesl.s 
 |-  S = ( ( ( Y ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 1 ) - ( X ` 1 ) ) )
6 fveq1 
 |-  ( X = Y -> ( X ` 1 ) = ( Y ` 1 ) )
7 6 necon3i 
 |-  ( ( X ` 1 ) =/= ( Y ` 1 ) -> X =/= Y )
8 1 2 3 4 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 ) ) ) ) } )
9 7 8 syl3an3 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( 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 ) ) ) ) } )
10 reex 
 |-  RR e. _V
11 prex 
 |-  { 1 , 2 } e. _V
12 1 11 eqeltri 
 |-  I e. _V
13 10 12 elmap 
 |-  ( p e. ( RR ^m I ) <-> p : I --> RR )
14 id 
 |-  ( p : I --> RR -> p : I --> RR )
15 1ex 
 |-  1 e. _V
16 15 prid1 
 |-  1 e. { 1 , 2 }
17 16 1 eleqtrri 
 |-  1 e. I
18 17 a1i 
 |-  ( p : I --> RR -> 1 e. I )
19 14 18 ffvelrnd 
 |-  ( p : I --> RR -> ( p ` 1 ) e. RR )
20 13 19 sylbi 
 |-  ( p e. ( RR ^m I ) -> ( p ` 1 ) e. RR )
21 20 3 eleq2s 
 |-  ( p e. P -> ( p ` 1 ) e. RR )
22 21 adantl 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) /\ p e. P ) -> ( p ` 1 ) e. RR )
23 10 12 elmap 
 |-  ( X e. ( RR ^m I ) <-> X : I --> RR )
24 id 
 |-  ( X : I --> RR -> X : I --> RR )
25 17 a1i 
 |-  ( X : I --> RR -> 1 e. I )
26 24 25 ffvelrnd 
 |-  ( X : I --> RR -> ( X ` 1 ) e. RR )
27 23 26 sylbi 
 |-  ( X e. ( RR ^m I ) -> ( X ` 1 ) e. RR )
28 27 3 eleq2s 
 |-  ( X e. P -> ( X ` 1 ) e. RR )
29 28 3ad2ant1 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( X ` 1 ) e. RR )
30 29 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) /\ p e. P ) -> ( X ` 1 ) e. RR )
31 10 12 elmap 
 |-  ( Y e. ( RR ^m I ) <-> Y : I --> RR )
32 id 
 |-  ( Y : I --> RR -> Y : I --> RR )
33 17 a1i 
 |-  ( Y : I --> RR -> 1 e. I )
34 32 33 ffvelrnd 
 |-  ( Y : I --> RR -> ( Y ` 1 ) e. RR )
35 31 34 sylbi 
 |-  ( Y e. ( RR ^m I ) -> ( Y ` 1 ) e. RR )
36 35 3 eleq2s 
 |-  ( Y e. P -> ( Y ` 1 ) e. RR )
37 36 3ad2ant2 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( Y ` 1 ) e. RR )
38 37 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) /\ p e. P ) -> ( Y ` 1 ) e. RR )
39 simpl3 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) /\ p e. P ) -> ( X ` 1 ) =/= ( Y ` 1 ) )
40 2ex 
 |-  2 e. _V
41 40 prid2 
 |-  2 e. { 1 , 2 }
42 41 1 eleqtrri 
 |-  2 e. I
43 42 a1i 
 |-  ( p : I --> RR -> 2 e. I )
44 14 43 ffvelrnd 
 |-  ( p : I --> RR -> ( p ` 2 ) e. RR )
45 13 44 sylbi 
 |-  ( p e. ( RR ^m I ) -> ( p ` 2 ) e. RR )
46 45 3 eleq2s 
 |-  ( p e. P -> ( p ` 2 ) e. RR )
47 46 adantl 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) /\ p e. P ) -> ( p ` 2 ) e. RR )
48 42 a1i 
 |-  ( X : I --> RR -> 2 e. I )
49 24 48 ffvelrnd 
 |-  ( X : I --> RR -> ( X ` 2 ) e. RR )
50 23 49 sylbi 
 |-  ( X e. ( RR ^m I ) -> ( X ` 2 ) e. RR )
51 50 3 eleq2s 
 |-  ( X e. P -> ( X ` 2 ) e. RR )
52 51 3ad2ant1 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( X ` 2 ) e. RR )
53 52 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) /\ p e. P ) -> ( X ` 2 ) e. RR )
54 3 eleq2i 
 |-  ( Y e. P <-> Y e. ( RR ^m I ) )
55 54 31 bitri 
 |-  ( Y e. P <-> Y : I --> RR )
56 42 a1i 
 |-  ( Y : I --> RR -> 2 e. I )
57 32 56 ffvelrnd 
 |-  ( Y : I --> RR -> ( Y ` 2 ) e. RR )
58 55 57 sylbi 
 |-  ( Y e. P -> ( Y ` 2 ) e. RR )
59 58 3ad2ant2 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( Y ` 2 ) e. RR )
60 59 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) /\ p e. P ) -> ( Y ` 2 ) e. RR )
61 22 30 38 39 47 53 60 5 affinecomb1 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) /\ 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 ) ) ) ) <-> ( p ` 2 ) = ( ( S x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( X ` 2 ) ) ) )
62 61 rabbidva 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> { 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 ) ) ) ) } = { p e. P | ( p ` 2 ) = ( ( S x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( X ` 2 ) ) } )
63 9 62 eqtrd 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( X L Y ) = { p e. P | ( p ` 2 ) = ( ( S x. ( ( p ` 1 ) - ( X ` 1 ) ) ) + ( X ` 2 ) ) } )