proving lines are perpendicular

This may not be the kind of proof you are looking for, but if you can't come up with some nice theorems to use, sometimes brute force computation can yield a proof.

I'm using homogeneous coordinates. Without loss of generality, the circle is the unit circle, with $B=[1:0:1]$ at the right. Using the tangent half angle formula, there have to exist parameters $c$ and $d$ such that $C=[c^2-1:2c:c^2+1]$ and $D=[d^2-1:2d:d^2+1]$ as any point on the unit circle except for $B$ itself can be expressed like this. We also need the matrix $M:=\operatorname{diag}(1,1,0)$ which turns a line into the point at infinity orthogonal to that. We can use this to construct your perpendiculars. Joining points to form lines, as well as intersecting lines to obtain points, can be expressed using the cross product.

So (with a bit of help from a computer algebra system I'd suggest) one can perform the following computation, canceling common factors wherever they occur:

\begin{align*} I &= [0:0:1] \\ B &= [1:0:1] \\ C &= [c^2-1:2c:c^2+1] \\ D &= [d^2-1:2d:d^2+1] \\ BC &= B\times C = [c:1:-c] \\ CD &= C\times D = [1-cd:-c-d:cd+1] \\ BD &= B\times D = [d:1:-d] \\ DE &= (M\cdot BC)\times D = [d^2+1:-cd^2-c:2cd-d^2+1] \\ CF &= (M\cdot BD)\times C = [c^2+1:-c^2d-d:-c^2+2cd+1] \\ BG &= (M\cdot CD)\times B = [-c-d:cd-1:c+d] \\ E &= DE\times BC = [c^2d^2+c^2-2cd+d^2-1:2c^2d+2c:c^2d^2+c^2+d^2+1] \\ F &= CF\times BD = [c^2d^2+c^2-2cd+d^2-1:2cd^2+2d:c^2d^2+c^2+d^2+1] \\ G &= BG\times CD = [c^2d^2+c^2+2cd+d^2-1:2c+2d:c^2d^2+c^2+d^2+1] \\ L &= DE\times CF \\&= [3c^2d^2+c^2+d^2-1:2c^2d+2cd^2+2c+2d:c^2d^2+c^2+d^2+1] \\ H &= CF\times(G\times E) \\&= [c^4d^3+c^4d+4c^3d^2-4c^2d^3+2c^3-2c^2d-d^3-2c+d\\&\quad:2c^3d^3+4c^3d+2c^2d^2-2cd^3+4c^2-2d^2\\&\quad:c^4d^3+c^4d+2c^3d^2+2c^3+2cd^2-d^3+2c-d] \\ J &= DE\times(G\times F) \\&= [c^3d^4-4c^3d^2+4c^2d^3+cd^4-c^3-2cd^2+2d^3+c-2d\\&\quad:2c^3d^3-2c^3d+2c^2d^2+4cd^3-2c^2+4d^2\\&\quad:c^3d^4+2c^2d^3+cd^4-c^3+2c^2d+2d^3-c+2d] \\ K &= I_3\cdot L + L_3\cdot I \\&= [3c^2d^2+c^2+d^2-1:2c^2d+2cd^2+2c+2d:2c^2d^2+2c^2+2d^2+2] \\ BK &= B\times K \\&= [2c^2d+2cd^2+2c+2d:-c^2d^2+c^2+d^2+3:-2c^2d-2cd^2-2c-2d] \\ HJ &= H\times J \\&= [c^2d^2-c^2-d^2-3:2c^2d+2cd^2+2c+2d:-c^2d^2+c^2-6cd+d^2-3] \\ 0 &= BK^T\cdot M\cdot HJ = \langle BK,M\cdot HJ\rangle = \langle M\cdot BK,HJ\rangle \end{align*}

Let's repeat this in words. $I$ is the origin, $B$ the point $(1,0)$. $C,D$ are two generic points on the circle, excluding $B$ itself. $BC,BD,CD$ are lines joining these points. For $DE$ you take the line $BC$, compute the point at infinity orthogonal to that, then join it with $D$. $E$ is the intersection of that with $BC$. $H$ and $J$ are points of intersection between two lines again, as indicated. $L$ is computed as the intersection of two of the altitudes, $\langle L,BG\rangle=0$ verifies that the third altitude passes through that as well. $K$ is a midpoint, which you can compute by summing homogeneous coordinate vectors after ensuring that the homogenization term (i.e. the last coordinate) is the same. We do this by cross-multiplying with the last coordinate of the respective other term. In the end, you verify orthogonality by computing some bilinear form and checking that it evaluates to zero, or in more geometric terms by ensuring that the orthogonal point at infinity of one line is incident with the other line. q.e.d.


This is NOT a solution. I just want to share my finding which is too long to be included in a comment.

enter image description here

As pointed out, K is the center of the nine-point circle. Its properties, together with LK = KI, generate several pairs of parallel lines (marked in blue) but they don’t seem to help.

The standard way to prove $BK \bot HJ$ is to prove $\angle BMH = 90^0$; where M is the intersection of BK and HJ. This is done if we can prove BEBJ is cyclic by showing $\angle MJE = \angle MBE$. Or alternately, if we can show the purple lines are parallel; where EN is drawn to be perpendicular to BK extended.


I am gonna continue on Mick's writings and image. I hope you know using trigonometry on geometry.

We should prove $\angle MJE = \angle MBE$ , so $\angle HJL = \angle KBE$. $$ $$

We know that $\angle HJL+\angle JHL=B=\angle KBE+\angle KBF$ $$ $$

So it's enough to show that $$\dfrac {\sin(HJL)}{\sin(JHL)}=\dfrac {\sin(KBE)}{\sin(KBF)}$$

$$ $$ (Left as an exercise: if $x+y=z+t\lt180$ and $\dfrac {\sin(x)}{\sin(y)}=\dfrac {\sin(z)}{\sin(t)}$, then $x=z$ and $y=t$)

$$ $$

Let $P$ and $Q$ be the projections of $K$ onto $BC$ and $BD$, respectively. Then,

$KP=KB*\sin(KBE)$ and $KQ=KB*\sin(KBF)$, so

$$\dfrac {\sin(KBE)}{\sin(KBF)}=\dfrac {KP}{KQ}$$

and also (Let $R$ be the radius of circumcircle of $BCD$)$$KP=\dfrac {LE+IT}{2}=\dfrac {2R\cos(B)\cos(C)+R\cos(D)}{2}=\dfrac {R\cos(B-C)}{2}$$, $$KQ=\dfrac {LF+IS}{2}=\dfrac {2R\cos(B)\cos(D)+R\cos(C)}{2}=\dfrac {R\cos(B-D)}{2}$$ $$\Rightarrow \dfrac {\sin(KBE)}{\sin(KBF)}=\dfrac {KP}{KQ}=\dfrac {\cos(B-C)}{\cos(B-D)}\tag {1}$$ $$ $$

By the triangle $HJL$, $$\dfrac {\sin(HJL)}{\sin(JHL)}=\dfrac {HL}{JL}=\dfrac {HL}{EL}*\dfrac {EL}{JL}$$

Because $\angle HEL=90-D$ and $\angle EHL=90+D-B$ $\quad$(easy to see) $$\dfrac {HL}{EL}=\dfrac {\cos(D)}{\cos(B-D)}$$

Because $GL$ is bisecting $\angle EGJ$

and because $\angle GEJ=90-D$ and $\angle GJE=90+B-C$ $\quad$(easy to see) $$\dfrac {EL}{JL}=\dfrac {EG}{GJ}=\dfrac {\cos(B-C)}{\cos(D)}$$ $$\Rightarrow \dfrac {\sin(HJL)}{\sin(JHL)}=\dfrac {HL}{EL}*\dfrac {EL}{JL}=\dfrac {\cos(B-C)}{\cos(B-D)}\tag {2}$$ $$ $$ By (1) and (2), $$\dfrac {\sin(HJL)}{\sin(JHL)}=\dfrac {\cos(B-C)}{\cos(B-D)}=\dfrac {\sin(KBE)}{\sin(KBF)}$$ $$ $$ $$\Rightarrow \angle HJL = \angle KBE $$ $$\Rightarrow \angle MJE = \angle MBE $$