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 = I
rrx2line.b P = I
rrx2line.l L = Line M E
Assertion rrx2vlinest X P Y P X 1 = Y 1 X 2 Y 2 X L Y = p P | p 1 = X 1

Proof

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