I would like to ask for some help about proofs of two corollaries of bounded linear functionals extension theorem. I am new to functional analysis, so hopefully it is OK if I give too many details to be commented on.
Theorem: Given a normed space $X$ over a field $\mathbb{K}$ (here it is the field reals or complexes) and a bounded linear functional $f:V\rightarrow \mathbb{K}$, where $V$ is a subspace of $X$. Then there is a bounded linear functional $F:X\rightarrow \mathbb{K}$ that is an extension of $f$ and has the same norm, which is $$\left\lVert F\right\rVert:=\sup\{|F(x)|:x\in X,\left\lVert x\right\rVert\leq1\}=\sup\{|f(x)|:x\in V,\left\lVert x\right\rVert\leq1\}=:\left\lVert f \right\rVert.$$
It is a consequence of Hahn-Banach theorem. Now, these are exercises I have tried:
Corollary 1: Let $X$ be a Banach space over a field $\mathbb{K}$ (reals or complexes) and $x,y\in X$ two different vectors. Then there is a continuous linear functional $F:X\rightarrow \mathbb{K}$ with $F(x)\neq F(y)$.
Proof: (i) Define $V:={\rm span}\{x-y\}$, hence it is a normed subspace of $X$ (with the same norm $\left\lVert.\right\rVert_X$).
(ii) Define $f:V\rightarrow \mathbb{K}$ with $f(k(x-y))=k\left\lVert x-y \right\rVert_X$. This is a well-defined linear functional. It is bounded: If $\left\lVert k(x-y)\right\rVert_X\leq 1$, then $|f(k(x-y))|=|k\left\lVert x-y \right\rVert_X|=|k|\left\lVert x-y \right\rVert_X=\left\lVert k(x-y)\right\rVert_X\leq 1.$
(iii) By the theorem, we have a bounded (hence continuous) linear functional $F:X\rightarrow \mathbb{K}$ which extends $f$. This means $F(x-y)=f(x-y)=\left\lVert x-y\right\rVert_X$. This would be zero by linearity if $F(x)=F(y)$, implying a contradiction $x=y$. Thus we are done.
Corollary 2: Let $X$ be a Banach space over a field $\mathbb{K}$ (reals or complexes) and $x\in X$. Then there is a continuous linear functional $F:X\rightarrow \mathbb{K}$ with $F(x)=\left\lVert x\right\rVert_X$ and $\left\lVert F\right\rVert=1$
Proof: Similar to the proof of Corollary 1 with $V:={\rm span\{x\}}$ instead. Clearly $1$ is an upper bound that is attained by $\frac{x}{\left\lVert x\right\rVert_X}\in V$ (hence a supremum) and checked by the norm equality in the theorem. Thus we are done.
One more: I do not get where we use the completeness of Banach space.
Suggestion for correction of any detail is really appreciated, maybe even if there is something unnecessary. Thank you very much.