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 = ( 0 ..^ 2 )
rrx2line.e 
|- E = ( RR^ ` I )
rrx2line.b 
|- P = ( RR ^m I )
rrx2line.l 
|- L = ( LineM ` E )
rrx2linest.a 
|- A = ( ( Y ` 0 ) - ( X ` 0 ) )
rrx2linest.b 
|- B = ( ( Y ` 1 ) - ( X ` 1 ) )
rrx2linest.c 
|- C = ( ( ( X ` 1 ) x. ( Y ` 0 ) ) - ( ( X ` 0 ) x. ( Y ` 1 ) ) )
Assertion rrx2linest 
|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X L Y ) = { p e. P | ( A x. ( p ` 1 ) ) = ( ( B x. ( p ` 0 ) ) + C ) } )

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