Metamath Proof Explorer

Theorem rrx2linest2

Description: The line passing through the two different points X and Y in a real Euclidean space of dimension 2 in another "standard form" (usually with ( p1 ) = x and ( p2 ) = y ). (Contributed by AV, 23-Feb-2023)

Ref Expression
Hypotheses rrx2linest2.i 
|- I = { 1 , 2 }
rrx2linest2.e 
|- E = ( RR^ ` I )
rrx2linest2.p 
|- P = ( RR ^m I )
rrx2linest2.l 
|- L = ( LineM ` E )
rrx2linest2.a 
|- A = ( ( X ` 2 ) - ( Y ` 2 ) )
rrx2linest2.b 
|- B = ( ( Y ` 1 ) - ( X ` 1 ) )
rrx2linest2.c 
|- C = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) )
Assertion rrx2linest2 
|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X L Y ) = { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C } )

Proof

Step Hyp Ref Expression
1 rrx2linest2.i 
 |-  I = { 1 , 2 }
2 rrx2linest2.e 
 |-  E = ( RR^ ` I )
3 rrx2linest2.p 
 |-  P = ( RR ^m I )
4 rrx2linest2.l 
 |-  L = ( LineM ` E )
5 rrx2linest2.a 
 |-  A = ( ( X ` 2 ) - ( Y ` 2 ) )
6 rrx2linest2.b 
 |-  B = ( ( Y ` 1 ) - ( X ` 1 ) )
7 rrx2linest2.c 
 |-  C = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) )
8 eqid 
 |-  ( ( Y ` 2 ) - ( X ` 2 ) ) = ( ( Y ` 2 ) - ( X ` 2 ) )
9 1 2 3 4 6 8 7 rrx2linest 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X L Y ) = { p e. P | ( B x. ( p ` 2 ) ) = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + C ) } )
10 eqcom 
 |-  ( ( B x. ( p ` 2 ) ) = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + C ) <-> ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + C ) = ( B x. ( p ` 2 ) ) )
11 1 3 rrx2pyel 
 |-  ( Y e. P -> ( Y ` 2 ) e. RR )
12 11 3ad2ant2 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( Y ` 2 ) e. RR )
13 1 3 rrx2pyel 
 |-  ( X e. P -> ( X ` 2 ) e. RR )
14 13 3ad2ant1 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X ` 2 ) e. RR )
15 12 14 resubcld 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( Y ` 2 ) - ( X ` 2 ) ) e. RR )
16 15 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( ( Y ` 2 ) - ( X ` 2 ) ) e. RR )
17 1 3 rrx2pxel 
 |-  ( p e. P -> ( p ` 1 ) e. RR )
18 17 adantl 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( p ` 1 ) e. RR )
19 16 18 remulcld 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) e. RR )
20 19 recnd 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) e. CC )
21 1 3 rrx2pxel 
 |-  ( Y e. P -> ( Y ` 1 ) e. RR )
22 21 3ad2ant2 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( Y ` 1 ) e. RR )
23 14 22 remulcld 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( X ` 2 ) x. ( Y ` 1 ) ) e. RR )
24 1 3 rrx2pxel 
 |-  ( X e. P -> ( X ` 1 ) e. RR )
25 24 3ad2ant1 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X ` 1 ) e. RR )
26 25 12 remulcld 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( X ` 1 ) x. ( Y ` 2 ) ) e. RR )
27 23 26 resubcld 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) e. RR )
28 7 27 eqeltrid 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> C e. RR )
29 28 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> C e. RR )
30 29 recnd 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> C e. CC )
31 22 25 resubcld 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( Y ` 1 ) - ( X ` 1 ) ) e. RR )
32 6 31 eqeltrid 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> B e. RR )
33 32 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> B e. RR )
34 1 3 rrx2pyel 
 |-  ( p e. P -> ( p ` 2 ) e. RR )
35 34 adantl 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( p ` 2 ) e. RR )
36 33 35 remulcld 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( B x. ( p ` 2 ) ) e. RR )
37 36 recnd 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( B x. ( p ` 2 ) ) e. CC )
38 20 30 37 addrsub 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + C ) = ( B x. ( p ` 2 ) ) <-> C = ( ( B x. ( p ` 2 ) ) - ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) ) ) )
39 eqcom 
 |-  ( C = ( ( B x. ( p ` 2 ) ) - ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) ) <-> ( ( B x. ( p ` 2 ) ) - ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) ) = C )
40 14 12 resubcld 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( X ` 2 ) - ( Y ` 2 ) ) e. RR )
41 5 40 eqeltrid 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> A e. RR )
42 41 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> A e. RR )
43 42 18 remulcld 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( A x. ( p ` 1 ) ) e. RR )
44 43 recnd 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( A x. ( p ` 1 ) ) e. CC )
45 44 37 addcomd 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = ( ( B x. ( p ` 2 ) ) + ( A x. ( p ` 1 ) ) ) )
46 12 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( Y ` 2 ) e. RR )
47 46 recnd 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( Y ` 2 ) e. CC )
48 14 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( X ` 2 ) e. RR )
49 48 recnd 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( X ` 2 ) e. CC )
50 47 49 negsubdi2d 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> -u ( ( Y ` 2 ) - ( X ` 2 ) ) = ( ( X ` 2 ) - ( Y ` 2 ) ) )
51 5 50 eqtr4id 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> A = -u ( ( Y ` 2 ) - ( X ` 2 ) ) )
52 51 oveq1d 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( A x. ( p ` 1 ) ) = ( -u ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) )
53 16 recnd 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( ( Y ` 2 ) - ( X ` 2 ) ) e. CC )
54 18 recnd 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( p ` 1 ) e. CC )
55 53 54 mulneg1d 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( -u ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) = -u ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) )
56 52 55 eqtrd 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( A x. ( p ` 1 ) ) = -u ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) )
57 56 oveq2d 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( ( B x. ( p ` 2 ) ) + ( A x. ( p ` 1 ) ) ) = ( ( B x. ( p ` 2 ) ) + -u ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) ) )
58 37 20 negsubd 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( ( B x. ( p ` 2 ) ) + -u ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) ) = ( ( B x. ( p ` 2 ) ) - ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) ) )
59 45 57 58 3eqtrd 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = ( ( B x. ( p ` 2 ) ) - ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) ) )
60 59 eqeq1d 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( ( B x. ( p ` 2 ) ) - ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) ) = C ) )
61 39 60 bitr4id 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( C = ( ( B x. ( p ` 2 ) ) - ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) ) <-> ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C ) )
62 38 61 bitrd 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + C ) = ( B x. ( p ` 2 ) ) <-> ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C ) )
63 10 62 syl5bb 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) -> ( ( B x. ( p ` 2 ) ) = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + C ) <-> ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C ) )
64 63 rabbidva 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> { p e. P | ( B x. ( p ` 2 ) ) = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + C ) } = { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C } )
65 9 64 eqtrd 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X L Y ) = { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C } )