Problem (2024PlanetCupp10): Let $\triangle DEF$ and $\triangle D'E'F'$ be the orthic triangles of $\triangle ABC$ and $\triangle DEF$ respectively. With $N$ as the nine-point center and $M$ as $BC$'s midpoint, suppose $E'F'$ and $D'N$ meet $BC$ at $J,K$. Let $O$ be $\triangle AJK$'s circumcenter. Line $AM$ meets $\odot O$ and $EF$ at $T,P$. If $TK\cap AJ=Q$, prove $PQ\perp OM$.
AlphaGeometry formalization: a b c = triangle; d = foot a b c; e = foot b a c; f = foot c a b; d1 = foot d e f; e1 = foot e d f; f1 = foot f d e; n1 = circumcenter d e f; m = midpoint b c; j = on_line e1 f1, on_line b c; k = on_line d1 n1, on_line b c; o = circumcenter a j k; t = on_line a m, on_circle o a; p = on_line a m, on_line e f; q = on_line t k, on_line a j ? perp p q o m
HAGeo formalization: A B C = triangle; BC = line B C; D = foot A BC; AC = line A C; E = foot B AC; AB = line A B; F = foot C AB; EF = line E F; DF = line D F; DE = line D E; D1 = foot D EF; E1 = foot E DF; F1 = foot F DE; N1 = circumcenter D E F; M = midpoint B C; E1F1 = line E1 F1; BC = line B C; J = intersection E1F1 BC; D1N1 = line D1 N1; K = intersection D1N1 BC; O = circumcenter A J K; AM = line A M; (O) = circle_center_point O A; T = intersection AM (O); EF = line E F; P = intersection AM EF; TK = line T K; AJ = line A J; Q = intersection TK AJ; PQ = line P Q; OM = line O M; Prove: perpendicular PQ OM
Difficulty score: 5.9