Problem (2013ARMOg10p7): The incircle of triangle $ ABC $ has centre $I$ and touches the sides $ BC $, $ CA $, $ AB $ at points $ A_1 $, $ B_1 $, $ C_1 $, respectively. Let $ I_a $, $ I_b $, $ I_c $ be excentres of triangle $ ABC $, touching the sides $ BC $, $ CA $, $ AB $ respectively. The segments $ I_aB_1 $ and $ I_bA_1 $ intersect at $ C_2 $. Similarly, segments $ I_bC_1 $ and $ I_cB_1 $ intersect at $ A_2 $, and the segments $ I_cA_1 $ and $ I_aC_1 $ at $ B_2 $. Prove that $ I $ is the center of the circumcircle of the triangle $ A_2B_2C_2 $.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; a1 = foot i b c; b1 = foot i a c; c1 = foot i a b; ia = excenter a b c; ib = excenter b c a; ic = excenter c a b; c2 = on_line ia b1, on_line ib a1; a2 = on_line ib c1, on_line ic b1; b2 = on_line ic a1, on_line ia c1 ? cong i a2 i b2
HAGeo formalization: A B C = triangle; I = incenter A B C; BC = line B C; A1 = foot I BC; AC = line A C; B1 = foot I AC; AB = line A B; C1 = foot I AB; Ia = excenter A B C; Ib = excenter B C A; Ic = excenter C A B; B1Ia = line B1 Ia; A1Ib = line A1 Ib; C2 = intersection B1Ia A1Ib; C1Ib = line C1 Ib; B1Ic = line B1 Ic; A2 = intersection C1Ib B1Ic; A1Ic = line A1 Ic; C1Ia = line C1 Ia; B2 = intersection A1Ic C1Ia; Prove: cong I A2 I B2
Difficulty score: 3.7