Problem (2009ARMOg9p2): Let be given a triangle $ ABC$ and its internal angle bisector $ BD$ $ (D\in BC)$. The line $ BD$ intersects the circumcircle $ \Omega$ of triangle $ ABC$ at $ B$ and $ E$. Circle $ \omega$ with diameter $ DE$ cuts $ \Omega$ again at $ F$. Prove that $ BF$ is the symmedian line of triangle $ ABC$.
AlphaGeometry formalization: a b c = triangle; d = on_line a c, angle_bisector a b c; o = circumcenter a b c; e = on_line b d, on_circle o a; f = on_circle o a, on_dia d e; m = midpoint a c; f1 = reflect f b d ? coll b f1 m
HAGeo formalization: A B C = triangle; l1 = angle_bisector A B C; AC = line A C; D = intersection l1 AC; O = circumcenter A B C; (O) = circle_center_point O A; BD = line B D; E = intersection BD (O); (DE) = circle_diameter D E; F = intersection (DE) (O); F1 = reflect_point_wrt_line F BD; M = midpoint A C; Prove: collinear M B F1
Difficulty score: 2.1