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=12
rrx2linest2.e E=msup
rrx2linest2.p P=I
rrx2linest2.l L=LineME
rrx2linest2.a A=X2Y2
rrx2linest2.b B=Y1X1
rrx2linest2.c C=X2Y1X1Y2
Assertion elrrx2linest2 XPYPXYGXLYGPAG1+BG2=C

Proof

Step Hyp Ref Expression
1 rrx2linest2.i I=12
2 rrx2linest2.e E=msup
3 rrx2linest2.p P=I
4 rrx2linest2.l L=LineME
5 rrx2linest2.a A=X2Y2
6 rrx2linest2.b B=Y1X1
7 rrx2linest2.c C=X2Y1X1Y2
8 1 2 3 4 5 6 7 rrx2linest2 XPYPXYXLY=pP|Ap1+Bp2=C
9 8 eleq2d XPYPXYGXLYGpP|Ap1+Bp2=C
10 fveq1 p=Gp1=G1
11 10 oveq2d p=GAp1=AG1
12 fveq1 p=Gp2=G2
13 12 oveq2d p=GBp2=BG2
14 11 13 oveq12d p=GAp1+Bp2=AG1+BG2
15 14 eqeq1d p=GAp1+Bp2=CAG1+BG2=C
16 15 elrab GpP|Ap1+Bp2=CGPAG1+BG2=C
17 9 16 bitrdi XPYPXYGXLYGPAG1+BG2=C