Hilbert projection theorem For every vector $x$ in a Hilbert space $H$ and every closed vector subspace $C$, there exists a unique vector $m\in C$ such that $x−m$ is orthogonal to $C$.
All proofs of this theorem that I know of use the axiom of countable choice.
Can Hilbert projection theorem be proved without AC or its weak form?
There is a question with a similar title, but its answer does not answer this question.