Metamath Proof Explorer


Theorem elrrx2linest2

Description: The line passing through the two different points X and Y in a real Euclidean space of dimension 2 in another "standard form" (usually with ( p1 ) = x and ( p2 ) = y ). (Contributed by AV, 23-Feb-2023)

Ref Expression
Hypotheses rrx2linest2.i I = 1 2
rrx2linest2.e E = I
rrx2linest2.p P = I
rrx2linest2.l L = Line M E
rrx2linest2.a A = X 2 Y 2
rrx2linest2.b B = Y 1 X 1
rrx2linest2.c C = X 2 Y 1 X 1 Y 2
Assertion elrrx2linest2 X P Y P X Y G X L Y G P A G 1 + B G 2 = C

Proof

Step Hyp Ref Expression
1 rrx2linest2.i I = 1 2
2 rrx2linest2.e E = I
3 rrx2linest2.p P = I
4 rrx2linest2.l L = Line M E
5 rrx2linest2.a A = X 2 Y 2
6 rrx2linest2.b B = Y 1 X 1
7 rrx2linest2.c C = X 2 Y 1 X 1 Y 2
8 1 2 3 4 5 6 7 rrx2linest2 X P Y P X Y X L Y = p P | A p 1 + B p 2 = C
9 8 eleq2d X P Y P X Y G X L Y G p P | A p 1 + B p 2 = C
10 fveq1 p = G p 1 = G 1
11 10 oveq2d p = G A p 1 = A G 1
12 fveq1 p = G p 2 = G 2
13 12 oveq2d p = G B p 2 = B G 2
14 11 13 oveq12d p = G A p 1 + B p 2 = A G 1 + B G 2
15 14 eqeq1d p = G A p 1 + B p 2 = C A G 1 + B G 2 = C
16 15 elrab G p P | A p 1 + B p 2 = C G P A G 1 + B G 2 = C
17 9 16 bitrdi X P Y P X Y G X L Y G P A G 1 + B G 2 = C