Problem (XinXingV35p1): In $\triangle ABC$, the perpendicular bisector of $BC$ meets $AC,AB$ at $D,E$ respectively. Let $l_a$ be the Euler line of $\triangle ADE$ (similarly define $l_b,l_c$). If $T$ is the circumcenter of the triangle formed by $l_a,l_b,l_c$, prove $T$ lies on $\triangle ABC$'s Euler line.
AlphaGeometry formalization: a b c = triangle; da = on_bline b c, on_line a c; ea = on_bline b c, on_line a b; oa = circumcenter a da ea; ha = orthocenter a da ea; db = on_bline a c, on_line b c; eb = on_bline a c, on_line a b; ob = circumcenter b db eb; hb = orthocenter b db eb; dc = on_bline a b, on_line b c; ec = on_bline a b, on_line a c; oc = circumcenter c dc ec; hc = orthocenter c dc ec; v1 = on_line oa ha, on_line ob hb; v2 = on_line ob hb, on_line oc hc; v3 = on_line oc hc, on_line oa ha; t = circumcenter v1 v2 v3; o = circumcenter a b c; h = orthocenter a b c ? coll t o h
HAGeo formalization: A B C = triangle; l1 = perpendicular_bisector B C; AC = line A C; Da = intersection l1 AC; AB = line A B; Ea = intersection l1 AB; Oa = circumcenter A Da Ea; Ha = orthocenter A Da Ea; l2 = perpendicular_bisector A C; BC = line B C; Db = intersection l2 BC; Eb = intersection l2 AB; Ob = circumcenter B Db Eb; Hb = orthocenter B Db Eb; l3 = perpendicular_bisector A B; Dc = intersection l3 BC; Ec = intersection l3 AC; Oc = circumcenter C Dc Ec; Hc = orthocenter C Dc Ec; OaHa = line Oa Ha; ObHb = line Ob Hb; V1 = intersection OaHa ObHb; OcHc = line Oc Hc; V2 = intersection ObHb OcHc; V3 = intersection OcHc OaHa; T = circumcenter V1 V2 V3; O = circumcenter A B C; H = orthocenter A B C; Prove: collinear T O H
Difficulty score: 6.8