Problem (2017CHNSouthEastMOg10p2): Let $ABC$ be an acute-angled triangle. In $ABC$, $AB \neq AB$, $K$ is the midpoint of the the median $AD$, $DE \perp AB$ at $E$, $DF \perp AC$ at $F$. The lines $KE$, $KF$ intersect the line $BC$ at $M$, $N$, respectively. The circumcenters of $\triangle DEM$, $\triangle DFN$ are $O_1, O_2$, respectively. Prove that $O_1 O_2 \parallel BC$.
AlphaGeometry formalization: a b c = triangle; d = midpoint b c; k = midpoint a d; e = foot d a b; f = foot d a c; m = on_line b c, on_line k e; n = on_line b c, on_line k f; o1 = circumcenter d e m; o2 = circumcenter d f n ? para o1 o2 b c
HAGeo formalization: A B C = acute_triangle; D = midpoint B C; K = midpoint A D; AB = line A B; E = foot D AB; AC = line A C; F = foot D AC; EK = line E K; BC = line B C; M = intersection EK BC; FK = line F K; N = intersection FK BC; O1 = circumcenter D E M; O2 = circumcenter D F N; O1O2 = line O1 O2; Prove: parallel O1O2 BC
Difficulty score: 2.8