Problem (2004CTSTp22): Points $D,E,F$ are on the sides $BC, CA$ and $AB$, respectively which satisfy $EF || BC$, $D_1$ is a point on $BC,$ Make $D_1E_1 || D_E, D_1F_1 || DF$ which intersect $AC$ and $AB$ at $E_1$ and $F_1$, respectively. Make $\bigtriangleup PBC \sim \bigtriangleup DEF$ such that $P$ and $A$ are on the same side of $BC.$ Prove that $E, E_1F_1, PD_1$ are concurrent.
AlphaGeometry formalization: a b c = triangle; e = on_line c a; f = on_line a b, on_pline e b c; d = on_line b c; d1 = on_line b c; e1 = on_line a c, on_pline d1 d e; f1 = on_line a b, on_pline d1 d f; p = on_aline p b c d e f, on_aline p c b d f e; x = on_line e1 f1, on_line e f ? coll p d1 x
HAGeo formalization: A B C = triangle; BC = line B C; D = foot A BC; AC = line A C; E = on_line AC; l1 = parallel_line E BC; AB = line A B; F = intersection AB l1; D1 = on_line BC; DE = line D E; l2 = parallel_line D1 DE; E1 = intersection AC l2; DF = line D F; l3 = parallel_line D1 DF; F1 = intersection AB l3; l4 = angle_equal1 B C D E F; l5 = angle_equal1 C B D F E; P = intersection l4 l5; EF = line E F; E1F1 = line E1 F1; X = intersection E1F1 EF; Prove: collinear P D1 X
Difficulty score: 4.0