Problem (2006CTSTp5): Let $\omega$ be the circumcircle of $\triangle{ABC}$. $P$ is an interior point of $\triangle{ABC}$. $A_{1}, B_{1}, C_{1}$ are the intersections of $AP, BP, CP$ respectively and $A_{2}, B_{2}, C_{2}$ are the symmetrical points of $A_{1}, B_{1}, C_{1}$ with respect to the midpoints of side $BC, CA, AB$. Show that the circumcircle of $\triangle{A_{2}B_{2}C_{2}}$ passes through the orthocentre of $\triangle{ABC}$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; p = free; a1 = on_line a p, on_circle o a; b1 = on_line b p, on_circle o a; c1 = on_line c p, on_circle o a; ma = midpoint b c; mb = midpoint c a; mc = midpoint a b; a2 = mirror a1 ma; b2 = mirror b1 mb; c2 = mirror c1 mc; h = orthocenter a b c ? cyclic h a2 b2 c2
HAGeo formalization: A B C = triangle; O = circumcenter A B C; (ABC) = circle_center_point O A; P = point; AP = line A P; A1 = intersection AP (ABC); BP = line B P; B1 = intersection BP (ABC); CP = line C P; C1 = intersection CP (ABC); L = midpoint B C; M = midpoint C A; N = midpoint A B; A2 = reflect A1 L; B2 = reflect B1 M; C2 = reflect C1 N; H = orthocenter A B C; Prove: concyclic H A2 B2 C2
Difficulty score: 3.6