Problem (2021GOWACAp5): Let $ABC$ be an acute triangle with altitude $\overline{AD}$, circumcenter $O$, and symmedian point $K$. Let $D_1$, $D_2$ be points on segment $\overline{BC}$ such that $BD = CD_1$ and $\angle BAD_2 = \angle CAD_1$. The line through $K$ perpendicular to $\overline{AO}$ meets $\overline{AD_2}$ at $P$, and the lines through $K$ perpendicular to $\overline{BO}$, $\overline{CO}$ meet $\overline{BC}$ at $X$, $Y$. Prove that the incenter $I$ of $\triangle PXY$ lies on $\overline{AD}$.
AlphaGeometry formalization: a b c = triangle; d = foot a b c; o = circumcenter a b c; m m1 m2 g = centroid a b c; k = on_aline k a c b a g, on_aline k b a c b g; d1 = mirror d m; d2 = on_line b c, on_aline d2 a b c a d1; p = on_tline k a o, on_line a d2; x = on_line b c, on_tline k b o; y = on_line b c, on_tline k c o; i = incenter p x y ? coll i a d
HAGeo formalization: A B C = acute_triangle; BC = line B C; D = foot A BC; O = circumcenter A B C; G M1 M2 M3 = centroid A B C; l1 = angle_equal1 A C B A G; l2 = angle_equal1 B A C B G; K = intersection l1 l2; D1 = reflect D M1; l3 = angle_equal1 A B C A D1; D2 = intersection l3 BC; AO = line A O; l4 = perpendicular_line K AO; AD2 = line A D2; P = intersection l4 AD2; BO = line B O; l5 = perpendicular_line K BO; X = intersection l5 BC; CO = line C O; l6 = perpendicular_line K CO; Y = intersection l6 BC; I = incenter P X Y; Prove: collinear A D I
Difficulty score: 5.0