(CONTEXT) I am a high school student who self-studies proof-based linear algebra through the use of Linear Algebra by Serge Lang. In order to consolidate my knowledge of significant results of linear algebra, and to enhance my capacity to produce correct mathematical proofs, I have attempted to prove nearly every result in the aforementioned book before I looked at the proof presented by the author; and as a part of that endeavour, I wrote a proof of the theorem below.
(REQUEST) Not fully confident in the validity of my proof, I am desirous to ask someone who is proficient in proof-based mathematics to examine my proof — which is available below — and tell me if it is correct. Additionally, the (PLL) tags mark the sections of the proof that concerns me the most; therefore, please focus on the marked sections of the proof if you do not have enough time to scrutinize the entire proof. Finally, should you so desire, please feel free to critique the stylistic aspect of my proof. In advance, thank you very much.
(THEOREM 6.2) Let $V$ be a nontrivial finite-dimensional complex vector space with a positive definite Hermitian product. Let $U$ be a unitary linear operator on $V$. Then $V$ has an orthogonal basis that consists entirely of eigenvectors of $U$.
(PROOF) Suppose that we have $\dim V=1$ . By an adequate reformulation of $\mathrm{theorem\space 2.3}\space,$ we see that $U$ has an eigenvector and a correspondent eigenvalue; and hence, we may let $v\in V$ be an eigenvector of $U$ with eigenvalue $\lambda$ . Then as $v\in V$ and $v$ is non-zero (by definition of eigenvector, since $v$ is an eigenvector of $U$, we see that $v$ is non-zero), it follows that $\{v\}$ is a linearly independent set in $V$. As $\{v\}$ is a linearly independent set in $V$, and as $V$ is a 1-dimensional vector space, by $\mathrm{theorem\space I.3.4}\space,$ it follows that $\{v\}$ is a basis of $V$. Since $\{v\}$ is vacuously orthogonal, since $v$ is an eigenvector of $U$, and since $\{v\}$ is a basis of $V$, it follows that $\{v\}$ is an orthogonal basis of $V$ that consists entirely of an eigenvector of $V$. And hence, the assertion holds for $\dim V = 1$ .
Suppose that, for some natural number $k\space,$ if $V$ is $k$-dimensional, then the assertion holds.
And now suppose that we have $\dim V = k+1\space.$ By an adequate reformulation of $\mathrm{theorem\space 2.3}\space,$ we know that $U$ has an eigenvector and a correspondent eigenvalue; and hence, we may again let $v_1\in V$ be an eigenvector of $U$ with eigenvalue $\lambda_1\space;$ and let $W=\mathrm{span}(\{v_1\})$ . As $v_1$ is an eigenvector of $U$, by definition of eigenvector, $v_1$ is non-zero, and therefore, $\{v_1\}$ is a linearly independent set. As $\{v_1\}$ generates $W$, and as $\{v_1\}$ is a linearly independent set, it follows that $\{v_1\}$ is a basis of $W$. Since $\{v_1\}$ is vacuously orthogonal, since $v_1$ is an eigenvector of $U$, and since $\{v_1\}$ is a basis of $W$, it follows that $\{v_1\}$ is an orthogonal basis of $W$ that consists entirely of an eigenvector of $U$.
Let $w\in W$. Then as $w\in W$ and $\{v_1\}$ is a basis of $W$, it follows that there exists some $x_1\in\mathbb{C}$ such that we have $w=x_1v_1\space;$ in that case, we have $$\begin{aligned} Uw&=U(x_1v_1) \\ &=x_1Uv_1 \\ &=x_1\lambda_1v_1 \\ &=(\lambda_1x_1)v_1\space, \end{aligned}$$ and as $Uw=(\lambda_1x_1)v_1$ and $\{v_1\}$ is a basis of $W$, it follows that we have $Uw\in W$, and therefore, $W$ is stable under $U$.
As $W$ is stable under $U$, and as $U$ is complex unitary, by $\mathrm{lemma\space6.1}\space,$ it follows that $W^\perp$ is also stable under $U$, and therefore, we can clearly see that $U$ can be viewed as a unitary linear operator on $W^\perp$ (PLL). Additionally, by $\mathrm{theorem\space V.2.6}\space,$ we have $$\begin{aligned} k+1 &= \dim V \\ k+1 &= \dim W + \dim W^\perp\\ k+1 &= N(\{v_1\})+\dim W^\perp \\ k+1 &= 1 + \dim W^\perp \\ k &= \dim W^\perp\space, \end{aligned}$$ and therefore, $W^\perp$ is $k$-dimensional. Since $U$ can be viewed as a unitary linear operator on $W^\perp$ (PLL), and since $W^\perp$ is $k$-dimensional, by the inductive hypothesis, it follows that $W^\perp$ has an orthogonal basis that consists entirely of eigenvectors of $U\space;$ and hence, we may let $v_2 \dots v_{k+1}\in W^\perp$ such that $\{v_2 \dots v_{k+1}\}$ is an orthogonal basis of $W^\perp$ that consists entirely of eigenvectors of $U$.
Because $\{v_1\}$ is an orthogonal basis of $W$ that consists entirely of an eigenvector of $U$, because $\{v_2 \dots v_{k+1}\}$ is an orthogonal basis of $W^\perp$ that also consists entirely of eigenvectors of $U$, and because $W$ and $W^\perp$ are obviously mutually perpendicular, by $\mathrm{lemma\space P.5.4}\space,$ it follows that $\{v_1 \dots v_{k+1}\}$ is an orthogonal basis of $W\oplus W^\perp$ that consists entirely of eigenvectors of $U$. And as $W\oplus W^\perp = V$ (cf. $\mathrm{theorem\space V.2.7}$), it follows that $\{v_1 \dots v_{k+1}\}$ is an orthogonal basis of $V$ that consists entirely of eigenvectors of $U$. And thus, the assertion holds for $\dim V = k+1$ .
To conclude, by the principle of mathematical induction, the assertion holds whenever $\dim V \in \mathbb{N}$; but because $V$ is finite-dimensional and nontrivial, we know that we have $\dim V \in \mathbb{N}$ in any case, and therefore, the assertion always holds.
Q.E.D.