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 = 1 2
rrx2line.e E = I
rrx2line.b P = I
rrx2line.l L = Line M E
rrx2linest.a A = Y 1 X 1
rrx2linest.b B = Y 2 X 2
rrx2linest.c C = X 2 Y 1 X 1 Y 2
Assertion rrx2linest X P Y P X Y X L Y = p P | A p 2 = B p 1 + C

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