The Wallace--Simson Line Theorem in Isabelle/HOL

We formalize the Wallace--Simson line theorem in Isabelle/HOL. Let \(ABC\) be a nondegenerate triangle and let \(M\) be a point on its circumcircle. Dropping the perpendiculars from \(M\) to the three side lines \(BC\), \(CA\), \(AB\) gives feet \(P\), \(Q\), \(R\); the theorem asserts that \(P\), \(Q\), \(R\) are collinear. The line through them is the Simson line, also called the Wallace line after William Wallace, whose published work on geometrical porisms is the standard early source for this result. We also prove the converse: if the three feet are collinear, then \(M\) lies on the circumcircle of \(ABC\). The development uses complex coordinates.