Problem (2011G3): Let $ABCD$ be a convex quadrilateral whose sides $AD$ and $BC$ are not parallel. Suppose that the circles with diameters $AB$ and $CD$ meet at points $E$ and $F$ inside the quadrilateral. Let $\omega_E$ be the circle through the feet of the perpendiculars from $E$ to the lines $AB,BC$ and $CD$. Let $\omega_F$ be the circle through the feet of the perpendiculars from $F$ to the lines $CD,DA$ and $AB$. Prove that the midpoint of the segment $EF$ lies on the line through the two intersections of $\omega_E$ and $\omega_F$.
AlphaGeometry formalization: a b c d = quadrangle; m1 = midpoint a b; m2 = midpoint c d; e = on_circle m1 a, on_circle m2 c; f = on_circle m1 a, on_circle m2 c; e1 = foot e a b; e2 = foot e b c; e3 = foot e c d; o_e = circumcenter e1 e2 e3; f1 = foot f c d; f2 = foot f d a; f3 = foot f a b; o_f = circumcenter f1 f2 f3; k1 = on_circle o_e e1, on_circle o_f f1; k2 = on_circle o_e e1, on_circle o_f f1; m = midpoint e f ? coll m k1 k2
HAGeo formalization: A B C D = quadrilateral; M1 = midpoint A B; M2 = midpoint C D; (AB) = circle_center_point M1 A; (CD) = circle_center_point M2 C; E F = intersection (AB) (CD); AB = line A B; P = foot E AB; BC = line B C; Q = foot E BC; CD = line C D; R = foot E CD; S = foot F CD; AD = line A D; T = foot F AD; U = foot F AB; O1 = circumcenter P Q R; (PQR) = circle_center_point O1 P; O2 = circumcenter S T U; (STU) = circle_center_point O2 S; K1 K2 = intersection (PQR) (STU); M = midpoint E F; Prove: collinear M K1 K2
Difficulty score: 4.8