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 ( ( p1 ) - ( X1 ) ) = ( S x. ( ( p0 ) - ( X0 ) ) ) . (Contributed by AV, 22-Jan-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 )
rrx2linesl.s 
|- S = ( ( ( Y ` 1 ) - ( X ` 1 ) ) / ( ( Y ` 0 ) - ( X ` 0 ) ) )
Assertion rrx2linesl 
|- ( ( X e. P /\ Y e. P /\ ( X ` 0 ) =/= ( Y ` 0 ) ) -> ( X L Y ) = { p e. P | ( p ` 1 ) = ( ( S x. ( ( p ` 0 ) - ( X ` 0 ) ) ) + ( X ` 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 rrx2linesl.s 
 |-  S = ( ( ( Y ` 1 ) - ( X ` 1 ) ) / ( ( Y ` 0 ) - ( X ` 0 ) ) )
6 fveq1 
 |-  ( X = Y -> ( X ` 0 ) = ( Y ` 0 ) )
7 6 necon3i 
 |-  ( ( X ` 0 ) =/= ( Y ` 0 ) -> 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 ` 0 ) = ( ( ( 1 - t ) x. ( X ` 0 ) ) + ( t x. ( Y ` 0 ) ) ) /\ ( p ` 1 ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) ) } )
9 7 8 syl3an3 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 0 ) =/= ( Y ` 0 ) ) -> ( 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 ) ) ) ) } )
10 1 3 rrx2pxel 
 |-  ( p e. P -> ( p ` 0 ) e. RR )
11 10 adantl 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 0 ) =/= ( Y ` 0 ) ) /\ p e. P ) -> ( p ` 0 ) e. RR )
12 1 3 rrx2pxel 
 |-  ( X e. P -> ( X ` 0 ) e. RR )
13 12 3ad2ant1 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 0 ) =/= ( Y ` 0 ) ) -> ( X ` 0 ) e. RR )
14 13 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 0 ) =/= ( Y ` 0 ) ) /\ p e. P ) -> ( X ` 0 ) e. RR )
15 1 3 rrx2pxel 
 |-  ( Y e. P -> ( Y ` 0 ) e. RR )
16 15 3ad2ant2 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 0 ) =/= ( Y ` 0 ) ) -> ( Y ` 0 ) e. RR )
17 16 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 0 ) =/= ( Y ` 0 ) ) /\ p e. P ) -> ( Y ` 0 ) e. RR )
18 simpl3 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 0 ) =/= ( Y ` 0 ) ) /\ p e. P ) -> ( X ` 0 ) =/= ( Y ` 0 ) )
19 1 3 rrx2pyel 
 |-  ( p e. P -> ( p ` 1 ) e. RR )
20 19 adantl 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 0 ) =/= ( Y ` 0 ) ) /\ p e. P ) -> ( p ` 1 ) e. RR )
21 1 3 rrx2pyel 
 |-  ( X e. P -> ( X ` 1 ) e. RR )
22 21 3ad2ant1 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 0 ) =/= ( Y ` 0 ) ) -> ( X ` 1 ) e. RR )
23 22 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 0 ) =/= ( Y ` 0 ) ) /\ p e. P ) -> ( X ` 1 ) e. RR )
24 1 3 rrx2pyel 
 |-  ( Y e. P -> ( Y ` 1 ) e. RR )
25 24 3ad2ant2 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 0 ) =/= ( Y ` 0 ) ) -> ( Y ` 1 ) e. RR )
26 25 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 0 ) =/= ( Y ` 0 ) ) /\ p e. P ) -> ( Y ` 1 ) e. RR )
27 11 14 17 18 20 23 26 5 affinecomb1 
 |-  ( ( ( X e. P /\ Y e. P /\ ( X ` 0 ) =/= ( Y ` 0 ) ) /\ 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 ) ) ) ) <-> ( p ` 1 ) = ( ( S x. ( ( p ` 0 ) - ( X ` 0 ) ) ) + ( X ` 1 ) ) ) )
28 27 rabbidva 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 0 ) =/= ( Y ` 0 ) ) -> { 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 ) ) ) ) } = { p e. P | ( p ` 1 ) = ( ( S x. ( ( p ` 0 ) - ( X ` 0 ) ) ) + ( X ` 1 ) ) } )
29 9 28 eqtrd 
 |-  ( ( X e. P /\ Y e. P /\ ( X ` 0 ) =/= ( Y ` 0 ) ) -> ( X L Y ) = { p e. P | ( p ` 1 ) = ( ( S x. ( ( p ` 0 ) - ( X ` 0 ) ) ) + ( X ` 1 ) ) } )