Problem (2023ELMOSLp2): Let \(ABC\) be an acute scalene triangle with orthocenter \(H\). Line \(BH\) intersects \(\overline{AC}\) at \(E\) and line \(CH\) intersects \(\overline{AB}\) at \(F\). Let \(X\) be the foot of the perpendicular from \(H\) to the line through \(A\) parallel to \(\overline{EF}\). Point \(B_1\) lies on line \(XF\) such that \(\overline{BB_1}\) is parallel to \(\overline{AC}\), and point \(C_1\) lies on line \(XE\) such that \(\overline{CC_1}\) is parallel to \(\overline{AB}\). Prove that points \(B\), \(C\), \(B_1\), \(C_1\) are concyclic.
AlphaGeometry formalization: a b c = triangle; h = orthocenter a b c; e = on_line a c, on_line b h; f = on_line a b, on_line c h; x = on_pline a e f, on_tline h e f; b1 = on_line x f, on_pline b a c; c1 = on_line x e, on_pline c a b ? cyclic b c b1 c1
HAGeo formalization: A B C = acute_triangle; H = orthocenter A B C; BH = line B H; AC = line A C; E = intersection BH AC; CH = line C H; AB = line A B; F = intersection CH AB; EF = line E F; la = parallel_line A EF; X = foot H la; l1 = parallel_line B AC; FX = line F X; B1 = intersection FX l1; l2 = parallel_line C AB; EX = line E X; C1 = intersection EX l2; Prove: concyclic B C B1 C1
Difficulty score: 2.5