Problem (2020G7): Let $P$ be a point on the circumcircle of acute triangle $ABC$. Let $D,E,F$ be the reflections of $P$ in the $A$-midline, $B$-midline, and $C$-midline. Let $\omega$ be the circumcircle of the triangle formed by the perpendicular bisectors of $AD, BE, CF$. Show that the circumcircles of $\triangle ADP, \triangle BEP, \triangle CFP,$ and $\omega$ share a common point.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; p = on_circle o a; m_ab = midpoint a b; m_ac = midpoint a c; m_bc = midpoint b c; d = reflect p m_ab m_ac; e = reflect p m_ab m_bc; f = reflect p m_ac m_bc; v1 = on_bline a d, on_bline b e; v2 = on_bline b e, on_bline c f; v3 = on_bline c f, on_bline a d; o1 = circumcenter a d p; o2 = circumcenter b e p; o3 = circumcenter c f p; k = on_circle o1 p, on_circle o2 b ? cyclic k v1 v2 v3
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; (ABC) = circle_center_point O A; P = on_circle (ABC); M1 = midpoint B C; M2 = midpoint C A; M3 = midpoint A B; M2M3 = line M2 M3; M1M3 = line M1 M3; M1M2 = line M1 M2; D = reflect_point_wrt_line P M2M3; E = reflect_point_wrt_line P M1M3; F = reflect_point_wrt_line P M1M2; m1 = perpendicular_bisector A D; m2 = perpendicular_bisector B E; m3 = perpendicular_bisector C F; V1 = intersection m2 m3; V2 = intersection m1 m3; V3 = intersection m1 m2; O1 = circumcenter A D P; O2 = circumcenter B E P; O3 = circumcenter C F P; (ADP) = circle_center_point O1 P; (BEP) = circle_center_point O2 P; X = intersection (ADP) (BEP); Prove: concyclic X V1 V2 V3
Difficulty score: 5.1