Problem (2008CTSTp7): Let $ P$ be the the isogonal conjugate of $ Q$ with respect to triangle $ ABC$, and $ P,Q$ are in the interior of triangle $ ABC$. Denote by $ O_{1},O_{2},O_{3}$ the circumcenters of triangle $ PBC,PCA,PAB$, $ O'_{1},O'_{2},O'_{3}$ the circumcenters of triangle $ QBC,QCA,QAB$, $ O$ the circumcenter of triangle $ O_{1}O_{2}O_{3}$, $ O'$ the circumcenter of triangle $ O'_{1}O'_{2}O'_{3}$. Prove that $ OO'$ is parallel to $ PQ$.
AlphaGeometry formalization: a b c = triangle; q = free; p = on_aline p a c b a q, on_aline p b a c b q; o1 = circumcenter p b c; o2 = circumcenter p c a; o3 = circumcenter p a b; o4 = circumcenter q b c; o5 = circumcenter q c a; o6 = circumcenter q a b; o = circumcenter o1 o2 o3; u = circumcenter o4 o5 o6 ? para o u p q
HAGeo formalization: A B C = triangle; P = point; l1 = angle_equal1 A B C A P; l2 = angle_equal1 B C A B P; Q = intersection l1 l2; O1 = circumcenter P B C; O2 = circumcenter P C A; O3 = circumcenter P A B; O4 = circumcenter Q B C; O5 = circumcenter Q C A; O6 = circumcenter Q A B; O = circumcenter O1 O2 O3; U = circumcenter O4 O5 O6; OU = line O U; PQ = line P Q; Prove: parallel OU PQ
Difficulty score: 4.0