Problem (2005CTSTp11b): Let $\omega$ be the circumcircle of acute triangle $ABC$. Two tangents of $\omega$ from $B$ and $C$ intersect at $P$, $AP$ and $BC$ intersect at $D$. Point $E$, $F$ are on $AC$ and $AB$ such that $DE \parallel BA$ and $DF \parallel CA$. (1) Prove that $F,B,C,E$ are concyclic. (2) Denote $A_{1}$ the centre of the circle passing through $F,B,C,E$. $B_{1}$, $C_{1}$ are difined similarly. Prove that $AA_{1}$, $BB_{1}$, $CC_{1}$ are concurrent.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; p = on_tline b o b, on_tline c o c; q = on_tline a o a, on_tline c o c; r = on_tline b o b, on_tline a o a; d1 = on_line a p, on_line b c; e1 = on_line a c, on_pline d1 a b; f1 = on_line a b, on_pline d1 a c; d2 = on_line b q, on_line a c; e2 = on_line b a, on_pline d2 b c; f2 = on_line b c, on_pline d2 b a; d3 = on_line c r, on_line b a; e3 = on_line c b, on_pline d3 c a; f3 = on_line c a, on_pline d3 c b; a1 = circumcenter f1 b c; b1 = circumcenter f2 a c; c1 = circumcenter f3 a b; x = on_line a a1, on_line b b1 ? coll x c c1
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; OA = line O A; OB = line O B; OC = line O C; l1 = perpendicular_line A OA; l2 = perpendicular_line B OB; l3 = perpendicular_line C OC; P = intersection l2 l3; Q = intersection l1 l3; R = intersection l1 l2; AP = line A P; BC = line B C; D1 = intersection AP BC; BQ = line B Q; AC = line A C; D2 = intersection BQ AC; CR = line C R; AB = line A B; D3 = intersection CR AB; l4 = parallel_line D1 AB; E1 = intersection l4 AC; l5 = parallel_line D1 AC; F1 = intersection l5 AB; l6 = parallel_line D2 BC; E2 = intersection l6 AB; l7 = parallel_line D2 AB; F2 = intersection l7 BC; l8 = parallel_line D3 AC; E3 = intersection l8 BC; l9 = parallel_line D3 BC; F3 = intersection l9 AC; A1 = circumcenter F1 B C; B1 = circumcenter F2 C A; C1 = circumcenter F3 A B; AA1 = line A A1; BB1 = line B B1; X = intersection AA1 BB1; Prove: collinear X C C1
Difficulty score: 4.0