I want to prove a statement that a subspace $L^m$ of X is of codimension at most m if and only if there exists linear functionals $\lambda_1,\cdots,\lambda_m$ : $X\rightarrow\mathbb{R}$ in the dual space $X^*$ such that $$L^m=\{x\in X:\lambda_i(x)=0\,,\forall i\in[m]\}=\ker A,$$where $A:X\rightarrow\mathbb{R}^m,x\mapsto[\lambda_1(x),\cdots,\lambda_m(x)]^T$
I have an idea to prove "if" part :
$\operatorname{codim}(L^m)=\dim(X)-\dim(L^m)=\dim(X)-\dim(\ker A)$
=$\dim(X)-(\dim(X)-\operatorname{rank}(A))=\operatorname{rank}(A)\leq m$
since A is of size $m\times\dim(X)$
However, now I have no idea regarding the "only if" part
Can anyone help me with the remaining part of this statement? Besides, if my proof of the "if" part has any faults, please also feel free to correct me
Thanks!
Assume the codimension of $L^m$ in $X$ is equal $k\le m.$ Let $B_0$ denote the Hamel basis in $L^m.$ By assumptions there are elements $v_1,v_2,\ldots, v_k$ such that the set $B=B_0\cup\{v_1,v_2,\ldots ,v_k\}$ constitutes the Hamel basis in $X.$ Every element $x\in X$ has a unique representation $$x=\sum_{b\in B} x_b b=\sum_{b\in B_0}x_b b+\sum_{j=1}^k x_{v_j}v_j,$$ where only finitely many coefficients $x_b$ are nonzero. Let $\lambda_j(x)=x_{v_j}.$ Then $L_j$ is a linear functional on $X$ and $$L^{m}=\{x\in X\,:\, \lambda_j(x)=0,\ j=1,2,\ldots, k\}$$ If $k=m$ we are done. If not let $\lambda_j=\lambda_k$ for $k<j\le m.$ In this way we get $$L^{m}=\{x\in X\,:\, \lambda_j(x)=0,\ j=1,2,\ldots, m\}$$ If $X$ is a Banach space and we require continuity of the functionals, then the assumption that $L^m$ is closed is necessary. In that case the quotient space $X/L^m$ is a Banach space with norm given by $$[x]=\inf\{\|y-x\|\in L^m\,:\, y\in L^m\}$$ By assumption the quotient space has dimension $k\le m.$ Choose a basis in $X/L^m.$ The elements of the basis are of the form $[v_1],[v_2],\ldots [v_k],$ for some $v_j\in X.$ Every element $[x]$ is uniquely represented as $$[x]=\sum_{j=1}^m \mu_j([x])[v_j]$$ As $X/L^m$ is finite dimensional the functionals $[x]\mapsto \mu_j([x])$ are bounded. Define the functionals $\lambda_j$ on $X$ by $$\lambda_j(x)=\mu_j([x]),\qquad j=1,2,\ldots, m$$ The functionals $\lambda_j$ are bounded as $$|\lambda(x)|=|\mu_j([x])|\le \|\mu_j\|\,\|[x]\|\le \|\mu_j\|\,\|x\|$$ Moreover $$L^m=\{x\in X\,:\, \lambda_j(x)=0,\ j=1,2,\ldots, k\}$$ In case $k<m$ we may repeat the same trick as in the first part.