Metamath Proof Explorer

Theorem rrx2linest

Description: The line passing through the two different points X and Y in a real Euclidean space of dimension 2 in "standard form". (Contributed by AV, 2-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 )
rrx2linest.a 
|- A = ( ( Y ` 1 ) - ( X ` 1 ) )
rrx2linest.b 
|- B = ( ( Y ` 2 ) - ( X ` 2 ) )
rrx2linest.c 
|- C = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) )
Assertion rrx2linest 
|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X L Y ) = { p e. P | ( A x. ( p ` 2 ) ) = ( ( B x. ( p ` 1 ) ) + C ) } )

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 rrx2linest.a 
 |-  A = ( ( Y ` 1 ) - ( X ` 1 ) )
6 rrx2linest.b 
 |-  B = ( ( Y ` 2 ) - ( X ` 2 ) )
7 rrx2linest.c 
 |-  C = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) )
8 simpl1 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> X e. P )
9 simpl2 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> Y e. P )
10 simpr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( X ` 1 ) = ( Y ` 1 ) )
11 simpr 
 |-  ( ( ( X e. P /\ Y e. P ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( X ` 1 ) = ( Y ` 1 ) )
12 11 anim1i 
 |-  ( ( ( ( X e. P /\ Y e. P ) /\ ( X ` 1 ) = ( Y ` 1 ) ) /\ ( X ` 2 ) = ( Y ` 2 ) ) -> ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) = ( Y ` 2 ) ) )
13 1 raleqi 
 |-  ( A. i e. I ( X ` i ) = ( Y ` i ) <-> A. i e. { 1 , 2 } ( X ` i ) = ( Y ` i ) )
14 1ex 
 |-  1 e. _V
15 2ex 
 |-  2 e. _V
16 fveq2 
 |-  ( i = 1 -> ( X ` i ) = ( X ` 1 ) )
17 fveq2 
 |-  ( i = 1 -> ( Y ` i ) = ( Y ` 1 ) )
18 16 17 eqeq12d 
 |-  ( i = 1 -> ( ( X ` i ) = ( Y ` i ) <-> ( X ` 1 ) = ( Y ` 1 ) ) )
19 fveq2 
 |-  ( i = 2 -> ( X ` i ) = ( X ` 2 ) )
20 fveq2 
 |-  ( i = 2 -> ( Y ` i ) = ( Y ` 2 ) )
21 19 20 eqeq12d 
 |-  ( i = 2 -> ( ( X ` i ) = ( Y ` i ) <-> ( X ` 2 ) = ( Y ` 2 ) ) )
22 14 15 18 21 ralpr 
 |-  ( A. i e. { 1 , 2 } ( X ` i ) = ( Y ` i ) <-> ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) = ( Y ` 2 ) ) )
23 13 22 bitri 
 |-  ( A. i e. I ( X ` i ) = ( Y ` i ) <-> ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) = ( Y ` 2 ) ) )
24 12 23 sylibr 
 |-  ( ( ( ( X e. P /\ Y e. P ) /\ ( X ` 1 ) = ( Y ` 1 ) ) /\ ( X ` 2 ) = ( Y ` 2 ) ) -> A. i e. I ( X ` i ) = ( Y ` i ) )
25 elmapfn 
 |-  ( X e. ( RR ^m I ) -> X Fn I )
26 25 3 eleq2s 
 |-  ( X e. P -> X Fn I )
27 elmapfn 
 |-  ( Y e. ( RR ^m I ) -> Y Fn I )
28 27 3 eleq2s 
 |-  ( Y e. P -> Y Fn I )
29 26 28 anim12i 
 |-  ( ( X e. P /\ Y e. P ) -> ( X Fn I /\ Y Fn I ) )
30 29 ad2antrr 
 |-  ( ( ( ( X e. P /\ Y e. P ) /\ ( X ` 1 ) = ( Y ` 1 ) ) /\ ( X ` 2 ) = ( Y ` 2 ) ) -> ( X Fn I /\ Y Fn I ) )
31 eqfnfv 
 |-  ( ( X Fn I /\ Y Fn I ) -> ( X = Y <-> A. i e. I ( X ` i ) = ( Y ` i ) ) )
32 30 31 syl 
 |-  ( ( ( ( X e. P /\ Y e. P ) /\ ( X ` 1 ) = ( Y ` 1 ) ) /\ ( X ` 2 ) = ( Y ` 2 ) ) -> ( X = Y <-> A. i e. I ( X ` i ) = ( Y ` i ) ) )
33 24 32 mpbird 
 |-  ( ( ( ( X e. P /\ Y e. P ) /\ ( X ` 1 ) = ( Y ` 1 ) ) /\ ( X ` 2 ) = ( Y ` 2 ) ) -> X = Y )
34 33 ex 
 |-  ( ( ( X e. P /\ Y e. P ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( ( X ` 2 ) = ( Y ` 2 ) -> X = Y ) )
35 34 necon3d 
 |-  ( ( ( X e. P /\ Y e. P ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( X =/= Y -> ( X ` 2 ) =/= ( Y ` 2 ) ) )
36 35 ex 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( X ` 1 ) = ( Y ` 1 ) -> ( X =/= Y -> ( X ` 2 ) =/= ( Y ` 2 ) ) ) )
37 36 com23 
 |-  ( ( X e. P /\ Y e. P ) -> ( X =/= Y -> ( ( X ` 1 ) = ( Y ` 1 ) -> ( X ` 2 ) =/= ( Y ` 2 ) ) ) )
38 37 3impia 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( X ` 1 ) = ( Y ` 1 ) -> ( X ` 2 ) =/= ( Y ` 2 ) ) )
39 38 imp 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( X ` 2 ) =/= ( Y ` 2 ) )
40 1 2 3 4 rrx2vlinest 
 |-  ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) -> ( X L Y ) = { p e. P | ( p ` 1 ) = ( X ` 1 ) } )
41 8 9 10 39 40 syl112anc 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( X L Y ) = { p e. P | ( p ` 1 ) = ( X ` 1 ) } )
42 ancom 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( X ` 1 ) = ( Y ` 1 ) ) <-> ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) )
43 simplr 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( X e. P /\ Y e. P /\ X =/= Y ) )
44 simpr 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> p e. P )
45 simpll 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( X ` 1 ) = ( Y ` 1 ) )
46 5 oveq1i 
 |-  ( A x. ( p ` 2 ) ) = ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 2 ) )
47 46 a1i 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( A x. ( p ` 2 ) ) = ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 2 ) ) )
48 oveq2 
 |-  ( ( X ` 1 ) = ( Y ` 1 ) -> ( ( Y ` 1 ) - ( X ` 1 ) ) = ( ( Y ` 1 ) - ( Y ` 1 ) ) )
49 48 adantl 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( ( Y ` 1 ) - ( X ` 1 ) ) = ( ( Y ` 1 ) - ( Y ` 1 ) ) )
50 1 3 rrx2pxel 
 |-  ( Y e. P -> ( Y ` 1 ) e. RR )
51 50 recnd 
 |-  ( Y e. P -> ( Y ` 1 ) e. CC )
52 51 3ad2ant2 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( Y ` 1 ) e. CC )
53 52 ad2antrr 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( Y ` 1 ) e. CC )
54 53 subidd 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( ( Y ` 1 ) - ( Y ` 1 ) ) = 0 )
55 49 54 eqtrd 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( ( Y ` 1 ) - ( X ` 1 ) ) = 0 )
56 55 oveq1d 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 2 ) ) = ( 0 x. ( p ` 2 ) ) )
57 1 3 rrx2pyel 
 |-  ( p e. P -> ( p ` 2 ) e. RR )
58 57 recnd 
 |-  ( p e. P -> ( p ` 2 ) e. CC )
59 58 ad2antlr 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( p ` 2 ) e. CC )
60 59 mul02d 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( 0 x. ( p ` 2 ) ) = 0 )
61 47 56 60 3eqtrd 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( A x. ( p ` 2 ) ) = 0 )
62 6 oveq1i 
 |-  ( B x. ( p ` 1 ) ) = ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) )
63 62 a1i 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( B x. ( p ` 1 ) ) = ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) )
64 oveq1 
 |-  ( ( X ` 1 ) = ( Y ` 1 ) -> ( ( X ` 1 ) x. ( Y ` 2 ) ) = ( ( Y ` 1 ) x. ( Y ` 2 ) ) )
65 64 oveq2d 
 |-  ( ( X ` 1 ) = ( Y ` 1 ) -> ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( Y ` 1 ) x. ( Y ` 2 ) ) ) )
66 7 65 eqtrid 
 |-  ( ( X ` 1 ) = ( Y ` 1 ) -> C = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( Y ` 1 ) x. ( Y ` 2 ) ) ) )
67 66 adantl 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> C = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( Y ` 1 ) x. ( Y ` 2 ) ) ) )
68 63 67 oveq12d 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( ( B x. ( p ` 1 ) ) + C ) = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( Y ` 1 ) x. ( Y ` 2 ) ) ) ) )
69 61 68 eqeq12d 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( ( A x. ( p ` 2 ) ) = ( ( B x. ( p ` 1 ) ) + C ) <-> 0 = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( Y ` 1 ) x. ( Y ` 2 ) ) ) ) ) )
70 43 44 45 69 syl21anc 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( ( A x. ( p ` 2 ) ) = ( ( B x. ( p ` 1 ) ) + C ) <-> 0 = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( Y ` 1 ) x. ( Y ` 2 ) ) ) ) ) )
71 1 3 rrx2pyel 
 |-  ( Y e. P -> ( Y ` 2 ) e. RR )
72 71 recnd 
 |-  ( Y e. P -> ( Y ` 2 ) e. CC )
73 72 3ad2ant2 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( Y ` 2 ) e. CC )
74 52 73 mulcomd 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( Y ` 1 ) x. ( Y ` 2 ) ) = ( ( Y ` 2 ) x. ( Y ` 1 ) ) )
75 74 oveq2d 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( Y ` 1 ) x. ( Y ` 2 ) ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( Y ` 2 ) x. ( Y ` 1 ) ) ) )
76 1 3 rrx2pyel 
 |-  ( X e. P -> ( X ` 2 ) e. RR )
77 76 recnd 
 |-  ( X e. P -> ( X ` 2 ) e. CC )
78 77 3ad2ant1 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X ` 2 ) e. CC )
79 78 73 52 subdird 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( Y ` 1 ) ) = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( Y ` 2 ) x. ( Y ` 1 ) ) ) )
80 75 79 eqtr4d 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( Y ` 1 ) x. ( Y ` 2 ) ) ) = ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( Y ` 1 ) ) )
81 80 ad2antlr 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( Y ` 1 ) x. ( Y ` 2 ) ) ) = ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( Y ` 1 ) ) )
82 81 oveq2d 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( Y ` 1 ) x. ( Y ` 2 ) ) ) ) = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( Y ` 1 ) ) ) )
83 82 eqeq2d 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( 0 = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( Y ` 1 ) x. ( Y ` 2 ) ) ) ) <-> 0 = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( Y ` 1 ) ) ) ) )
84 eqcom 
 |-  ( 0 = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( Y ` 1 ) ) ) <-> ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( Y ` 1 ) ) ) = 0 )
85 84 a1i 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( 0 = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( Y ` 1 ) ) ) <-> ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( Y ` 1 ) ) ) = 0 ) )
86 73 ad2antlr 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( Y ` 2 ) e. CC )
87 78 ad2antlr 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( X ` 2 ) e. CC )
88 86 87 subcld 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( ( Y ` 2 ) - ( X ` 2 ) ) e. CC )
89 1 3 rrx2pxel 
 |-  ( p e. P -> ( p ` 1 ) e. RR )
90 89 recnd 
 |-  ( p e. P -> ( p ` 1 ) e. CC )
91 90 adantl 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( p ` 1 ) e. CC )
92 88 91 mulcld 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) e. CC )
93 87 86 subcld 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( ( X ` 2 ) - ( Y ` 2 ) ) e. CC )
94 52 ad2antlr 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( Y ` 1 ) e. CC )
95 93 94 mulcld 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( Y ` 1 ) ) e. CC )
96 addeq0 
 |-  ( ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) e. CC /\ ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( Y ` 1 ) ) e. CC ) -> ( ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( Y ` 1 ) ) ) = 0 <-> ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) = -u ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( Y ` 1 ) ) ) )
97 92 95 96 syl2anc 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( Y ` 1 ) ) ) = 0 <-> ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) = -u ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( Y ` 1 ) ) ) )
98 93 94 mulneg1d 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( -u ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( Y ` 1 ) ) = -u ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( Y ` 1 ) ) )
99 87 86 negsubdi2d 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> -u ( ( X ` 2 ) - ( Y ` 2 ) ) = ( ( Y ` 2 ) - ( X ` 2 ) ) )
100 99 oveq1d 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( -u ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( Y ` 1 ) ) = ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( Y ` 1 ) ) )
101 98 100 eqtr3d 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> -u ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( Y ` 1 ) ) = ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( Y ` 1 ) ) )
102 101 eqeq2d 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) = -u ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( Y ` 1 ) ) <-> ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) = ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( Y ` 1 ) ) ) )
103 necom 
 |-  ( ( X ` 2 ) =/= ( Y ` 2 ) <-> ( Y ` 2 ) =/= ( X ` 2 ) )
104 39 42 103 3imtr3i 
 |-  ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) -> ( Y ` 2 ) =/= ( X ` 2 ) )
105 104 adantr 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( Y ` 2 ) =/= ( X ` 2 ) )
106 86 87 105 subne0d 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( ( Y ` 2 ) - ( X ` 2 ) ) =/= 0 )
107 91 94 88 106 mulcand 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) = ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( Y ` 1 ) ) <-> ( p ` 1 ) = ( Y ` 1 ) ) )
108 102 107 bitrd 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) = -u ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( Y ` 1 ) ) <-> ( p ` 1 ) = ( Y ` 1 ) ) )
109 85 97 108 3bitrd 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( 0 = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( X ` 2 ) - ( Y ` 2 ) ) x. ( Y ` 1 ) ) ) <-> ( p ` 1 ) = ( Y ` 1 ) ) )
110 83 109 bitrd 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( 0 = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( Y ` 1 ) x. ( Y ` 2 ) ) ) ) <-> ( p ` 1 ) = ( Y ` 1 ) ) )
111 simpl 
 |-  ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) -> ( X ` 1 ) = ( Y ` 1 ) )
112 111 eqcomd 
 |-  ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) -> ( Y ` 1 ) = ( X ` 1 ) )
113 112 adantr 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( Y ` 1 ) = ( X ` 1 ) )
114 113 eqeq2d 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( ( p ` 1 ) = ( Y ` 1 ) <-> ( p ` 1 ) = ( X ` 1 ) ) )
115 70 110 114 3bitrrd 
 |-  ( ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> ( ( p ` 1 ) = ( X ` 1 ) <-> ( A x. ( p ` 2 ) ) = ( ( B x. ( p ` 1 ) ) + C ) ) )
116 115 rabbidva 
 |-  ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) -> { p e. P | ( p ` 1 ) = ( X ` 1 ) } = { p e. P | ( A x. ( p ` 2 ) ) = ( ( B x. ( p ` 1 ) ) + C ) } )
117 42 116 sylbi 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> { p e. P | ( p ` 1 ) = ( X ` 1 ) } = { p e. P | ( A x. ( p ` 2 ) ) = ( ( B x. ( p ` 1 ) ) + C ) } )
118 41 117 eqtrd 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( X L Y ) = { p e. P | ( A x. ( p ` 2 ) ) = ( ( B x. ( p ` 1 ) ) + C ) } )
119 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 ) ) ) ) } )
120 119 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ -. ( 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 ) ) ) ) } )
121 df-ne 
 |-  ( ( X ` 1 ) =/= ( Y ` 1 ) <-> -. ( X ` 1 ) = ( Y ` 1 ) )
122 89 ad2antlr 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( p ` 1 ) e. RR )
123 1 3 rrx2pxel 
 |-  ( X e. P -> ( X ` 1 ) e. RR )
124 123 3ad2ant1 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X ` 1 ) e. RR )
125 124 ad2antrr 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( X ` 1 ) e. RR )
126 50 3ad2ant2 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( Y ` 1 ) e. RR )
127 126 ad2antrr 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( Y ` 1 ) e. RR )
128 simpr 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( X ` 1 ) =/= ( Y ` 1 ) )
129 57 ad2antlr 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( p ` 2 ) e. RR )
130 76 3ad2ant1 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X ` 2 ) e. RR )
131 130 ad2antrr 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( X ` 2 ) e. RR )
132 71 3ad2ant2 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( Y ` 2 ) e. RR )
133 132 ad2antrr 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( Y ` 2 ) e. RR )
134 122 125 127 128 129 131 133 affinecomb2 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( 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 ) ) ) ) <-> ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 2 ) ) = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) ) )
135 5 eqcomi 
 |-  ( ( Y ` 1 ) - ( X ` 1 ) ) = A
136 135 oveq1i 
 |-  ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 2 ) ) = ( A x. ( p ` 2 ) )
137 6 eqcomi 
 |-  ( ( Y ` 2 ) - ( X ` 2 ) ) = B
138 137 oveq1i 
 |-  ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) = ( B x. ( p ` 1 ) )
139 7 eqcomi 
 |-  ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) = C
140 138 139 oveq12i 
 |-  ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) = ( ( B x. ( p ` 1 ) ) + C )
141 136 140 eqeq12i 
 |-  ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) x. ( p ` 2 ) ) = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) ) <-> ( A x. ( p ` 2 ) ) = ( ( B x. ( p ` 1 ) ) + C ) )
142 134 141 bitrdi 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ p e. P ) /\ ( X ` 1 ) =/= ( Y ` 1 ) ) -> ( 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 ) ) ) ) <-> ( A x. ( p ` 2 ) ) = ( ( B x. ( p ` 1 ) ) + C ) ) )
143 142 expcom 
 |-  ( ( X ` 1 ) =/= ( Y ` 1 ) -> ( ( ( X e. P /\ Y e. P /\ X =/= 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 ) ) ) ) <-> ( A x. ( p ` 2 ) ) = ( ( B x. ( p ` 1 ) ) + C ) ) ) )
144 121 143 sylbir 
 |-  ( -. ( X ` 1 ) = ( Y ` 1 ) -> ( ( ( X e. P /\ Y e. P /\ X =/= 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 ) ) ) ) <-> ( A x. ( p ` 2 ) ) = ( ( B x. ( p ` 1 ) ) + C ) ) ) )
145 144 expd 
 |-  ( -. ( X ` 1 ) = ( Y ` 1 ) -> ( ( X e. P /\ Y e. P /\ X =/= 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 ) ) ) ) <-> ( A x. ( p ` 2 ) ) = ( ( B x. ( p ` 1 ) ) + C ) ) ) ) )
146 145 impcom 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ -. ( 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 ) ) ) ) <-> ( A x. ( p ` 2 ) ) = ( ( B x. ( p ` 1 ) ) + C ) ) ) )
147 146 imp 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ -. ( 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 ) ) ) ) <-> ( A x. ( p ` 2 ) ) = ( ( B x. ( p ` 1 ) ) + C ) ) )
148 147 rabbidva 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ -. ( 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 | ( A x. ( p ` 2 ) ) = ( ( B x. ( p ` 1 ) ) + C ) } )
149 120 148 eqtrd 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ -. ( X ` 1 ) = ( Y ` 1 ) ) -> ( X L Y ) = { p e. P | ( A x. ( p ` 2 ) ) = ( ( B x. ( p ` 1 ) ) + C ) } )
150 118 149 pm2.61dan 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X L Y ) = { p e. P | ( A x. ( p ` 2 ) ) = ( ( B x. ( p ` 1 ) ) + C ) } )