A Linear Subspace is a Vector Space and Inherits an Inner Product

Let $K$ be a \reftext{def:field-c54-2026b}{field}, let $V$ be a \reftext{def:vector-space-2026a}{vector space over $K$} with \reftext{lem:vector-space-basic-identities-2026a}{zero vector} $0_{V}$, and let $W$ be a \reftext{def:linear-subspace-2026a}{linear subspace} of $V$. Then the following hold.

\textbf{1. (Vector space)} The set $W$, equipped with the restrictions to $W$ of the addition and the scalar multiplication of $V$, is a vector space over $K$. Its zero vector is $0_{V}$, and for $w\in W$ the additive inverse of $w$ in $W$ is its additive inverse $-w$ in $V$.

\textbf{2. (Finite sums agree)} Let $n$ be a \reftext{def:natural-numbers-2026a}{natural number} and let $w\in W^{n}$ be an \reftext{def:finite-tuple-power-2026a}{$n$-tuple} in $W$. Then the \reftext{def:finite-sum-vector-space-2026a}{finite sum} of $w$ formed in the vector space $W$ of claim 1 is equal to the finite sum of $w$ formed in $V$, the latter being the finite sum of $w$ regarded as an $n$-tuple in $V$.

\textbf{3. (Inner product)} Suppose $K$ is the field of \reftext{def:complex-numbers-2026a}{complex numbers} and $V$ together with $\langle\cdot,\cdot\rangle$ is a \reftext{def:complex-inner-product-space-2026a}{complex inner product space}. Then the map assigning to each pair $w,w'$ of elements of $W$ the complex number $\langle w,w'\rangle$ is an inner product on the vector space $W$ of claim 1. The \reftext{def:inner-product-norm-2026a}{norm induced} on $W$ by this inner product assigns to each $w\in W$ the same real number $\lVert w\rVert$ as the norm induced on $V$; and the \reftext{def:metric-space-2026a}{metric} on $W$ obtained from it as in claim 3 of \ref{lem:inner-product-norm-is-norm-2026a} is the restriction to $W$ of the corresponding metric on $V$.