Proof of Standard Basis Vectors of ℝ^q: Coordinates, Orthonormality and Unit Length

Each result cited is universally quantified over the data in its own statement.

Clause coordinates. By The Dot Product on $\mathbb{R}^n$ §dot-product, $e_{k}\cdot w=\sum_{i=1}^{q}(e_{k})_{i}w_{i}$, the sum over $[q]$ of the pointwise product $f\in\mathbb{R}^{[q]}$, $f(i)=(e_{k})_{i}w_{i}$. By Identity Matrix and Standard Basis Vectors §basis, $(e_{k})_{i}=\delta_{ik}$ for $i\in[q]$, and by Identity Matrix and Standard Basis Vectors §identity, $\delta_{ik}=1$ if $i=k$ and $\delta_{ik}=0$ if $i\neq k$. Hence $f(i)=0\cdot w_{i}=0$ for every $i\in[q]$ with $i\neq k$, and $f(k)=1\cdot w_{k}=w_{k}$. The set $[q]=\{1,\dots,q\}$ is finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §naturals, and $k\in[q]$. So Sums over Finite Sets in a Commutative Ring and in an Ordered Field: Distributivity, Products of Sums, Vanishing Terms, Sums over Pairs, Expanding Products of Sums, Counting, Comparison, Monotonicity and the Triangle Inequality §vanishing, with $\mathbb{R}$ for its $R$, $[q]$ for its $A$ and $k$ for its $y$, gives $e_{k}\cdot w=f(k)=w_{k}$.

Clause orthonormal. Clause coordinates with $w=e_{l}$ gives $e_{k}\cdot e_{l}=(e_{l})_{k}$, and $(e_{l})_{k}=\delta_{kl}$ by Identity Matrix and Standard Basis Vectors §basis. By Identity Matrix and Standard Basis Vectors §identity, $\delta_{kl}=1$ if $k=l$ and $\delta_{kl}=0$ if $k\neq l$.

Clause unit. By clause orthonormal with $l=k$, $e_{k}\cdot e_{k}=1$. Thus $1$ is a nonnegative real number whose square is $e_{k}\cdot e_{k}=1$. By Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square §square, the norm $\lVert e_{k}\rVert$ of The Euclidean Norm on $\mathbb{R}^n$ §norm is the only nonnegative real number whose square is $e_{k}\cdot e_{k}$. Hence $\lVert e_{k}\rVert=1$.