Problem (2020KoMaLA774): Let $O$ be the circumcenter of triangle $ABC,$ and $D$ be an arbitrary point on the circumcircle of $ABC.$ Let points $X, Y$ and $Z$ be the orthogonal projections of point $D$ onto lines $OA, OB$ and $OC,$ respectively. Prove that the incenter of triangle $XYZ$ is on the Simson-Wallace line of triangle $ABC$ corresponding to point $D.$
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; d = on_circum a b c; x = foot d o a; y = foot d o b; z = foot d o c; i = incenter x y z; p = foot d b c; q = foot d a c ? coll i p q
HAGeo formalization: A B C = triangle; O = circumcenter A B C; (O) = circle_center_point O A; D = on_circle (O); AO = line A O; X = foot D AO; BO = line B O; Y = foot D BO; CO = line C O; Z = foot D CO; I = incenter X Y Z; BC = line B C; AC = line A C; P = foot D BC; Q = foot D AC; Prove: collinear I P Q
Difficulty score: 3.5