Metamath Proof Explorer


Theorem rrx2vlinest

Description: The vertical 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 )
Assertion 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 ) } )

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 fveq1
 |-  ( X = Y -> ( X ` 2 ) = ( Y ` 2 ) )
6 5 necon3i
 |-  ( ( X ` 2 ) =/= ( Y ` 2 ) -> X =/= Y )
7 6 adantl
 |-  ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> 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 ` 2 ) =/= ( Y ` 2 ) ) ) -> ( 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 oveq2
 |-  ( ( Y ` 1 ) = ( X ` 1 ) -> ( t x. ( Y ` 1 ) ) = ( t x. ( X ` 1 ) ) )
11 10 oveq2d
 |-  ( ( Y ` 1 ) = ( X ` 1 ) -> ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( X ` 1 ) ) ) )
12 11 eqcoms
 |-  ( ( X ` 1 ) = ( Y ` 1 ) -> ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( X ` 1 ) ) ) )
13 12 adantr
 |-  ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( X ` 1 ) ) ) )
14 13 3ad2ant3
 |-  ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) -> ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( X ` 1 ) ) ) )
15 14 adantr
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( X ` 1 ) ) ) )
16 15 adantr
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) /\ t e. RR ) -> ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( X ` 1 ) ) ) )
17 1 3 rrx2pxel
 |-  ( X e. P -> ( X ` 1 ) e. RR )
18 17 recnd
 |-  ( X e. P -> ( X ` 1 ) e. CC )
19 18 3ad2ant1
 |-  ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) -> ( X ` 1 ) e. CC )
20 19 adantr
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> ( X ` 1 ) e. CC )
21 20 adantr
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) /\ t e. RR ) -> ( X ` 1 ) e. CC )
22 recn
 |-  ( t e. RR -> t e. CC )
23 22 adantl
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) /\ t e. RR ) -> t e. CC )
24 21 23 affineid
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) /\ t e. RR ) -> ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( X ` 1 ) ) ) = ( X ` 1 ) )
25 16 24 eqtrd
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) /\ t e. RR ) -> ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) = ( X ` 1 ) )
26 25 eqeq2d
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) /\ t e. RR ) -> ( ( p ` 1 ) = ( ( ( 1 - t ) x. ( X ` 1 ) ) + ( t x. ( Y ` 1 ) ) ) <-> ( p ` 1 ) = ( X ` 1 ) ) )
27 26 anbi1d
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) /\ 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 ` 1 ) = ( X ` 1 ) /\ ( p ` 2 ) = ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) ) ) )
28 27 rexbidva
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ 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 ) ) ) ) <-> E. t e. RR ( ( p ` 1 ) = ( X ` 1 ) /\ ( p ` 2 ) = ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) ) ) )
29 simpl
 |-  ( ( ( p ` 1 ) = ( X ` 1 ) /\ ( p ` 2 ) = ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) ) -> ( p ` 1 ) = ( X ` 1 ) )
30 29 a1i
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) /\ t e. RR ) -> ( ( ( p ` 1 ) = ( X ` 1 ) /\ ( p ` 2 ) = ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) ) -> ( p ` 1 ) = ( X ` 1 ) ) )
31 30 rexlimdva
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> ( E. t e. RR ( ( p ` 1 ) = ( X ` 1 ) /\ ( p ` 2 ) = ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) ) -> ( p ` 1 ) = ( X ` 1 ) ) )
32 1 3 rrx2pyel
 |-  ( p e. P -> ( p ` 2 ) e. RR )
33 32 adantl
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> ( p ` 2 ) e. RR )
34 1 3 rrx2pyel
 |-  ( X e. P -> ( X ` 2 ) e. RR )
35 34 3ad2ant1
 |-  ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) -> ( X ` 2 ) e. RR )
36 35 adantr
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> ( X ` 2 ) e. RR )
37 33 36 resubcld
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> ( ( p ` 2 ) - ( X ` 2 ) ) e. RR )
38 1 3 rrx2pyel
 |-  ( Y e. P -> ( Y ` 2 ) e. RR )
39 38 3ad2ant2
 |-  ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) -> ( Y ` 2 ) e. RR )
40 39 35 resubcld
 |-  ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) -> ( ( Y ` 2 ) - ( X ` 2 ) ) e. RR )
41 40 adantr
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> ( ( Y ` 2 ) - ( X ` 2 ) ) e. RR )
42 38 recnd
 |-  ( Y e. P -> ( Y ` 2 ) e. CC )
43 42 3ad2ant2
 |-  ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) -> ( Y ` 2 ) e. CC )
44 34 recnd
 |-  ( X e. P -> ( X ` 2 ) e. CC )
45 44 3ad2ant1
 |-  ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) -> ( X ` 2 ) e. CC )
46 simpr
 |-  ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> ( X ` 2 ) =/= ( Y ` 2 ) )
47 46 necomd
 |-  ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) -> ( Y ` 2 ) =/= ( X ` 2 ) )
48 47 3ad2ant3
 |-  ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) -> ( Y ` 2 ) =/= ( X ` 2 ) )
49 43 45 48 subne0d
 |-  ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) -> ( ( Y ` 2 ) - ( X ` 2 ) ) =/= 0 )
50 49 adantr
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> ( ( Y ` 2 ) - ( X ` 2 ) ) =/= 0 )
51 37 41 50 redivcld
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) e. RR )
52 51 adantr
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) /\ ( p ` 1 ) = ( X ` 1 ) ) -> ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) e. RR )
53 oveq2
 |-  ( t = ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) -> ( 1 - t ) = ( 1 - ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) ) )
54 53 oveq1d
 |-  ( t = ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) -> ( ( 1 - t ) x. ( X ` 2 ) ) = ( ( 1 - ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) ) x. ( X ` 2 ) ) )
55 oveq1
 |-  ( t = ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) -> ( t x. ( Y ` 2 ) ) = ( ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) x. ( Y ` 2 ) ) )
56 54 55 oveq12d
 |-  ( t = ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) -> ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) = ( ( ( 1 - ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) ) x. ( X ` 2 ) ) + ( ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) x. ( Y ` 2 ) ) ) )
57 56 eqeq2d
 |-  ( t = ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) -> ( ( p ` 2 ) = ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) <-> ( p ` 2 ) = ( ( ( 1 - ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) ) x. ( X ` 2 ) ) + ( ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) x. ( Y ` 2 ) ) ) ) )
58 57 anbi2d
 |-  ( t = ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) -> ( ( ( p ` 1 ) = ( X ` 1 ) /\ ( p ` 2 ) = ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) ) <-> ( ( p ` 1 ) = ( X ` 1 ) /\ ( p ` 2 ) = ( ( ( 1 - ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) ) x. ( X ` 2 ) ) + ( ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) x. ( Y ` 2 ) ) ) ) ) )
59 58 adantl
 |-  ( ( ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) /\ ( p ` 1 ) = ( X ` 1 ) ) /\ t = ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) ) -> ( ( ( p ` 1 ) = ( X ` 1 ) /\ ( p ` 2 ) = ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) ) <-> ( ( p ` 1 ) = ( X ` 1 ) /\ ( p ` 2 ) = ( ( ( 1 - ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) ) x. ( X ` 2 ) ) + ( ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) x. ( Y ` 2 ) ) ) ) ) )
60 simpr
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) /\ ( p ` 1 ) = ( X ` 1 ) ) -> ( p ` 1 ) = ( X ` 1 ) )
61 44 mulid2d
 |-  ( X e. P -> ( 1 x. ( X ` 2 ) ) = ( X ` 2 ) )
62 61 3ad2ant1
 |-  ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) -> ( 1 x. ( X ` 2 ) ) = ( X ` 2 ) )
63 62 adantr
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> ( 1 x. ( X ` 2 ) ) = ( X ` 2 ) )
64 37 recnd
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> ( ( p ` 2 ) - ( X ` 2 ) ) e. CC )
65 42 adantl
 |-  ( ( X e. P /\ Y e. P ) -> ( Y ` 2 ) e. CC )
66 44 adantr
 |-  ( ( X e. P /\ Y e. P ) -> ( X ` 2 ) e. CC )
67 65 66 subcld
 |-  ( ( X e. P /\ Y e. P ) -> ( ( Y ` 2 ) - ( X ` 2 ) ) e. CC )
68 67 3adant3
 |-  ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) -> ( ( Y ` 2 ) - ( X ` 2 ) ) e. CC )
69 68 adantr
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> ( ( Y ` 2 ) - ( X ` 2 ) ) e. CC )
70 64 69 50 divcan1d
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> ( ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) x. ( ( Y ` 2 ) - ( X ` 2 ) ) ) = ( ( p ` 2 ) - ( X ` 2 ) ) )
71 63 70 oveq12d
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> ( ( 1 x. ( X ` 2 ) ) + ( ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) x. ( ( Y ` 2 ) - ( X ` 2 ) ) ) ) = ( ( X ` 2 ) + ( ( p ` 2 ) - ( X ` 2 ) ) ) )
72 45 adantr
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> ( X ` 2 ) e. CC )
73 32 recnd
 |-  ( p e. P -> ( p ` 2 ) e. CC )
74 73 adantl
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> ( p ` 2 ) e. CC )
75 72 74 pncan3d
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> ( ( X ` 2 ) + ( ( p ` 2 ) - ( X ` 2 ) ) ) = ( p ` 2 ) )
76 71 75 eqtr2d
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> ( p ` 2 ) = ( ( 1 x. ( X ` 2 ) ) + ( ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) x. ( ( Y ` 2 ) - ( X ` 2 ) ) ) ) )
77 76 adantr
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) /\ ( p ` 1 ) = ( X ` 1 ) ) -> ( p ` 2 ) = ( ( 1 x. ( X ` 2 ) ) + ( ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) x. ( ( Y ` 2 ) - ( X ` 2 ) ) ) ) )
78 1cnd
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> 1 e. CC )
79 51 recnd
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) e. CC )
80 43 adantr
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> ( Y ` 2 ) e. CC )
81 78 79 72 80 submuladdmuld
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> ( ( ( 1 - ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) ) x. ( X ` 2 ) ) + ( ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) x. ( Y ` 2 ) ) ) = ( ( 1 x. ( X ` 2 ) ) + ( ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) x. ( ( Y ` 2 ) - ( X ` 2 ) ) ) ) )
82 81 adantr
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) /\ ( p ` 1 ) = ( X ` 1 ) ) -> ( ( ( 1 - ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) ) x. ( X ` 2 ) ) + ( ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) x. ( Y ` 2 ) ) ) = ( ( 1 x. ( X ` 2 ) ) + ( ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) x. ( ( Y ` 2 ) - ( X ` 2 ) ) ) ) )
83 77 82 eqtr4d
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) /\ ( p ` 1 ) = ( X ` 1 ) ) -> ( p ` 2 ) = ( ( ( 1 - ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) ) x. ( X ` 2 ) ) + ( ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) x. ( Y ` 2 ) ) ) )
84 60 83 jca
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) /\ ( p ` 1 ) = ( X ` 1 ) ) -> ( ( p ` 1 ) = ( X ` 1 ) /\ ( p ` 2 ) = ( ( ( 1 - ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) ) x. ( X ` 2 ) ) + ( ( ( ( p ` 2 ) - ( X ` 2 ) ) / ( ( Y ` 2 ) - ( X ` 2 ) ) ) x. ( Y ` 2 ) ) ) ) )
85 52 59 84 rspcedvd
 |-  ( ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) /\ ( p ` 1 ) = ( X ` 1 ) ) -> E. t e. RR ( ( p ` 1 ) = ( X ` 1 ) /\ ( p ` 2 ) = ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) ) )
86 85 ex
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> ( ( p ` 1 ) = ( X ` 1 ) -> E. t e. RR ( ( p ` 1 ) = ( X ` 1 ) /\ ( p ` 2 ) = ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) ) ) )
87 31 86 impbid
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ p e. P ) -> ( E. t e. RR ( ( p ` 1 ) = ( X ` 1 ) /\ ( p ` 2 ) = ( ( ( 1 - t ) x. ( X ` 2 ) ) + ( t x. ( Y ` 2 ) ) ) ) <-> ( p ` 1 ) = ( X ` 1 ) ) )
88 28 87 bitrd
 |-  ( ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) /\ 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 ` 1 ) = ( X ` 1 ) ) )
89 88 rabbidva
 |-  ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) -> { 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 ` 1 ) = ( X ` 1 ) } )
90 9 89 eqtrd
 |-  ( ( X e. P /\ Y e. P /\ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) =/= ( Y ` 2 ) ) ) -> ( X L Y ) = { p e. P | ( p ` 1 ) = ( X ` 1 ) } )