Let $E$ be a $\mathbb{K}$-vector space. I have seen that every subspace $F \subset E$ has an (algebraic) complement $F'$ ($F+F'=E$ and $F \cap F'=\{0\}$).
One proof (using that every vector space admits a basis) is found here, and another using directly Zorn's lemma in here.
What I would like to know is if it is possible to prove that statement without using the axiom of choice.
One idea that came to me was this: in the finite case, the complement of a subspace $F \subset E$ is isomorphic to the quotient space $E/F$. Is this true in the general case? If there were a way to embed $E/F$ in $E$ in such a way that it is the complement of $F$, we could prove the statement.
On the other hand, a way to prove that this is not possible to achieve could be to deduce that every vector space admits a basis (without using AC) from the fact that every subspace admits a complement. But I can't see how this could be done.
Thanks in advance for any help
No, it is not a theorem of ZF (provided ZF is consistent). For information of this kind you may consult Rubin & Rubin, Equivalents of the Axiom of Choice, I and II.
One case with no complement constructible in ZF is this one: $\mathbb Q \subset \mathbb R$, vector spaces over $\mathbb Q$. There is a model for ZF due to Solovay (and Shelah?) where every subset of $\mathbb R$ has the property of Baire. But a group homomorphism $f : \mathbb R \to \mathbb R$ such that $f^{-1}(U)$ has the property of Baire for every open set $U$ must be continuous. But any additive projection of $\mathbb R$ onto the subspace $\mathbb Q$ is discontinuous.