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 = ( 0 ..^ 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 ` 0 ) = ( Y ` 0 ) /\ ( X ` 1 ) =/= ( Y ` 1 ) ) ) -> ( X L Y ) = { p e. P | ( p ` 0 ) = ( X ` 0 ) } )

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