Problem (2019KoMaLA736): Let $P$ be a point in the plane of triangle $ABC$. Denote the reflections of $A,B,C$ over $P$ by $A',B'$ and $C'$, respectively. Let $A'',B'',C''$ be the reflection of $A',B',C'$ over $BC,CA$ and $AB$, respectively. Let the line $A''B''$ intersects $AC$ at $A_b$ and let $A''C''$ intersects $AB$ at $A_c$. Denote by $\omega_A$ the circle through the points $A,A_b,A_c$. The circles $\omega_B,\omega_C$ are defined similarly. Prove that $\omega_A ,\omega_B ,\omega_C$ are coaxial, i.e., they share a common radical axis.
AlphaGeometry formalization: a b c = triangle; p = free; a1 = mirror a p; b1 = mirror b p; c1 = mirror c p; a2 = reflect a1 b c; b2 = reflect b1 c a; c2 = reflect c1 a b; ab = on_line a2 b2, on_line a c; ac = on_line a2 c2, on_line a b; o1 = circumcenter a ab ac; bc = on_line b2 c2, on_line b a; ba = on_line b2 a2, on_line b c; o2 = circumcenter b bc ba; ca = on_line c2 a2, on_line c b; cb = on_line c2 b2, on_line c a; o3 = circumcenter c ca cb; z = on_circle o1 a, on_circle o2 b ? cyclic z ca cb c
HAGeo formalization: A B C = triangle; P = point; A1 = reflect A P; B1 = reflect B P; C1 = reflect C P; BC = line B C; A2 = reflect_point_wrt_line A1 BC; AC = line A C; B2 = reflect_point_wrt_line B1 AC; AB = line A B; C2 = reflect_point_wrt_line C1 AB; A2B2 = line A2 B2; Ab = intersection A2B2 AC; A2C2 = line A2 C2; Ac = intersection A2C2 AB; B2C2 = line B2 C2; Bc = intersection B2C2 AB; Ba = intersection A2B2 BC; Ca = intersection A2C2 BC; Cb = intersection B2C2 AC; O1 = circumcenter A Ab Ac; (O1) = circle_center_point O1 A; O2 = circumcenter B Bc Ba; (O2) = circle_center_point O2 B; Oc = circumcenter C Ca Cb; Z = intersection (O1) (O2); Prove: concyclic Z Ca Cb C
Difficulty score: 4.3