I'll post a solution to the second part (the inequality) for now: Observe that 2[ACB1] = R * b * (1 - cosB), where R is the circumradius. Hence it suffices to show that p >= a * cosA + b * cosB + c * cosC, where p is the semi-perimeter. Now it's not difficult to convert this into proving: 2p / R >= sin2A + sin2B + sin2C = 4sinA * sinB * sinC. Use sine law to reduce it to: 2p * R² >= abc, then the result follows immediately from 4R = abc / S, S = rp, and R >= 2r, where S and r are the area and inradius of ABC, respectively.

Note that $ABC$ is the orthic triangle of $A_{0}B_{0}C_{0}$, so it lies on the nine-point circle, and since $A_{1}B_{1}C_{1}$ is a homothety of $A_{0}B_{0}C_{0}$ about the incenter $I$, we further have that the ratio must be one half (as the nine-point circle has half the radius of the circumcircle). It is then clear that $[IA_{1}BC_{1}] = \frac{1}{2}\cdot [A_{0}IC_{0}]$. Adding these analogous equations yields the first equality. For the second part, it suffices to show that $2[ABC] \le [BA_{1}CB_{1}AC_{1}]$. Indeed, if we let $P, Q, R$ be points on the circumcircle with $AP \perp BC$, etc., then $[BA_{1}CB_{1}AC_{1}] \ge [ARBPCQ] = 2 [ABC]$. If for example angle A is obtuse, then we already have $[ABA_{1}C] \ge 2[ABC]$.

This is actually length bashable. Use the $\frac{1}{2} ab\sin C$ formula to find the areas of triangles ABC1 and the linik, and then just bash bash bash untnil you get something like $\sum_{cyc} 2abc^2-a^2c^2-b^2c^2+c^4 \ge (a+b+c)(a+b-c)(a+c-b)(b+c-a)$, which is easily provable by Schur's then AM-GM. (hahaha Muirhead fails...)