I am trying to prove that given any line $l$ and a point $A$ not on it, there exists a unique line $k$ that crosses $A$ and is perpendicular to $l$.
Proof: By the Expansion Postulate, I know there exists at least two distinct points on $l$, call them $B$ and $C$. By the line postulate, construct line $\overleftrightarrow{AB}$. By the protractor postulate, construct ray starting at $A$ and ending at point $D$ so that $\overrightarrow{AD}$ is coplanar to plane $ABC$ (plane postulate), so that $\measuredangle BAD = 180-2\measuredangle ABC$, and finally, so that $\overrightarrow{AD}\cap\overleftrightarrow{BC}\neq \emptyset$. Let $$\overrightarrow{AD}\cap\overleftrightarrow{BC}=E$$ by the line intersection postulate.
It is clear that $\triangle ABE$ is isosceles (isosceles triangle theorem). Now, by the protractor postulate, choose point $F$ in the interior of $\angle BAE$ so that $$\measuredangle BAF = \measuredangle FAE =\frac{1}{2} \measuredangle BAE$$ ... Therefore, $\overleftrightarrow{AF}$ is a perpendicular to $\overleftrightarrow{CB}=l$. $\blacksquare$
The rest of the proof, including uniqueness is not too bad. But overall, this felt incredibly long winded and inefficient. The high-school book I am using says that they are using the postulates from Euclid but after research it seems as though they are much more closely using Hilbert's Axioms.
My question is this, is this route of proof valid? What is a better proof? I am likely missing something quite simple. I am aware of this and this post but these do not assume Playfair's postulate which I have no issue accepting (even though I guess I haven't used it here.) Any guidance or critiques are much appreciated.
EDIT
Second proof: By the expansion postulate, let $l=\overleftrightarrow{BC}$. By protractor postulate, choose point $D$ on the same side of $l$ as $A$, so that $\measuredangle DBC=90^\circ$. By line postulate, construct $\overleftrightarrow{DB}$. Notice $l \perp \overleftrightarrow{DB}$. If $A\in \overleftrightarrow{DB}$ then $\overleftrightarrow{DB}$ is the perpendicular we are looking for. Otherwise, by playfair we have a unique line $k$ going through $A$ so that $k \parallel \overleftrightarrow{DB}$. Notice $k\cap l \neq \emptyset$ for if that were true we would have that $l \parallel k \parallel \overleftrightarrow{DB}$ but $l$ and $\overleftrightarrow{DB}$ share point $B$. So let $k \cap l = E$. From here, using the consecutive interior angle theorem, it is easy to see that $\angle BEA$ is right so that line $k$ is the perpendicular we need. $\blacksquare$