Problem (2018G5): Let $ABC$ be a triangle with circumcircle $\Omega$ and incentre $I$. A line $\ell$ intersects the lines $AI$, $BI$, and $CI$ at points $D$, $E$, and $F$, respectively, distinct from the points $A$, $B$, $C$, and $I$. The perpendicular bisectors $x$, $y$, and $z$ of the segments $AD$, $BE$, and $CF$, respectively determine a triangle $\Theta$. Show that the circumcircle of the triangle $\Theta$ is tangent to $\Omega$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; i = incenter a b c; p1 p2 = segment; d = on_line p1 p2, on_line a i; e = on_line p1 p2, on_line b i; f = on_line p1 p2, on_line c i; p = on_bline a d, on_bline b e; q = on_bline b e, on_bline c f; r = on_bline c f, on_bline a d; o1 = circumcenter p q r; t = on_circle o1 p, on_circle o a ? coll t o1 o
HAGeo formalization: A B C = triangle; O = circumcenter A B C; (ABC) = circle_center_point O A; I = incenter A B C; l = line; AI = line A I; D = intersection l AI; BI = line B I; E = intersection l BI; CI = line C I; F = intersection l CI; l1 = perpendicular_bisector A D; l2 = perpendicular_bisector B E; l3 = perpendicular_bisector C F; P = intersection l2 l3; Q = intersection l1 l3; R = intersection l1 l2; O1 = circumcenter P Q R; (PQR) = circle_center_point O1 P; T = intersection (ABC) (PQR); Prove: collinear T O1 O
Difficulty score: 4.3