Problem (2008ARMOg10p6): In a scalene triangle $ ABC$ the altitudes $ AA_{1}$ and $ CC_{1}$ intersect at $ H, O$ is the circumcenter, and $ B_{0}$ the midpoint of side $ AC$. The line $ BO$ intersects side $ AC$ at $ P$, while the lines $ BH$ and $ A_{1}C_{1}$ meet at $ Q$. Prove that the lines $ HB_{0}$ and $ PQ$ are parallel.
AlphaGeometry formalization: a b c = triangle; a1 = foot a b c; c1 = foot c a b; h = orthocenter a b c; o = circumcenter a b c; b0 = midpoint a c; p = on_line b o, on_line a c; q = on_line b h, on_line a1 c1 ? para h b0 p q
HAGeo formalization: A B C = triangle; BC = line B C; A1 = foot A BC; AB = line A B; C1 = foot C AB; H = orthocenter A B C; O = circumcenter A B C; B0 = midpoint A C; BO = line B O; AC = line A C; P = intersection BO AC; BH = line B H; A1C1 = line A1 C1; Q = intersection BH A1C1; B0H = line B0 H; PQ = line P Q; Prove: parallel B0H PQ
Difficulty score: 2.2