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 mullidd 
 |-  ( 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 ) } )