Angle bisector ⇔ equidistant from sides

Dependencies: SAS congruence. At this layer we prove only the forward direction: the converse (equidistant from the two sides ⟹ on the angle bisector) is deferred until after HL (hypotenuse-leg) congruence.

Statement

Angle bisector: let $\angle AOB$ be a nonzero, non-straight angle. If a ray $OM$ lies inside $\angle AOB$ and satisfies

then $OM$ is called the angle bisector of $\angle AOB$ — the "half-angle" real number provided by axiom III (Protractor axiom) corresponds to exactly one such ray, which exists and is unique.

Distance from a point to a line: let $\ell$ be a line and $P$ a point not on $\ell$. By axiom III, the foot of the perpendicular from $P$ to $\ell$ is unique; call it $E$. Then distance $\operatorname{dist}(P,\ell) := |PE|$.

The complete biconditional —

let $P$ be a point inside $\angle AOB$ distinct from $O$, and drop perpendiculars from $P$ to $OA$ and $OB$ with feet $E$ and $F$ respectively. Then

This section proves only the forward direction ($\Rightarrow$): $P$ on the angle bisector $\Rightarrow |PE|=|PF|$. The converse ($\Leftarrow$) must wait until after HL; the reasons are in On the converse.