Problem (ShuZhiMiGeo352): In acute $\triangle ABC$ with circumcenter $O$ and orthocenter $H$, let $\triangle H_AH_BH_C$ be the orthic triangle with centroid $G_H$. Define $H'_A$ as $H_A$'s isotomic conjugate (i.e., $BH'_A=CH_A$), similarly $H'_B,H'_C$, and let $H'$ be the orthocenter of $\triangle H'_AH'_BH'_C$. Prove $H'O \parallel G_HH$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; h = orthocenter a b c; ha = foot a b c; hb = foot b a c; hc = foot c a b; n1 n2 n3 gh = centroid ha hb hc; m_bc = midpoint b c; ha1 = mirror ha m_bc; m_ac = midpoint a c; hb1 = mirror hb m_ac; m_ab = midpoint a b; hc1 = mirror hc m_ab; h1 = orthocenter ha1 hb1 hc1 ? para h1 o gh h
HAGeo formalization: A B C = triangle; O = circumcenter A B C; BC = line B C; AC = line A C; AB = line A B; H = orthocenter A B C; Ha = foot A BC; Hb = foot B AC; Hc = foot C AB; Gh N1 N2 N3 = centroid Ha Hb Hc; Mbc = midpoint B C; Ha1 = reflect_point_wrt_point Ha Mbc; Mac = midpoint A C; Hb1 = reflect_point_wrt_point Hb Mac; Mab = midpoint A B; Hc1 = reflect_point_wrt_point Hc Mab; H1 = orthocenter Ha1 Hb1 Hc1; H1O = line H1 O; GhH = line Gh H; Prove: parallel H1O GhH
Difficulty score: 5.7