Proof of Properties of Dimension

Routine facts about the classes of lengths of independent families, tuples in a smaller set, mutual inclusion and nonempty segments are used without comment (Toolkit for AL2). Let $d=\dim V$, and fix a basis $(b_{1},\dots,b_{d})$ of $V$ (Finite-Dimensional Vector Spaces and Their Dimension (ii)); it spans $V$ and is linearly independent (Finite Basis of a Vector Space (i)).

We first extend an independent family to a basis. Let $u$ be linearly independent. Every linearly independent tuple in $V$ has length at most $d$, by The Steinitz Exchange Lemma (i) applied against the spanning family $(b_{1},\dots,b_{d})$. So among the $p\in\mathbb{N}_{0}$ for which some $p$-tuple $(w_{1},\dots,w_{p})$ makes $(u_{1},\dots,u_{m},w_{1},\dots,w_{p})$ linearly independent there is a largest one, since $p=0$ qualifies and $m+p\leq d$; fix such a $p$ and such a $w$. If this family did not span $V$, some $b_{i}$ would lie outside its span, for otherwise its span, a subspace containing every $b_{i}$, would contain $\operatorname{span}(b_{1},\dots,b_{d})=V$ by The Span of a Finite Family is the Smallest Subspace Containing It (ii) and The Span of a Finite Family is the Smallest Subspace Containing It (iii). Adjoining that $b_{i}$, Elementary Properties of Linear Independence (iii) would then give a linearly independent extension of length $m+p+1$, contradicting the maximality of $p$. So the family spans $V$ and is a basis, which proves (i).

Next, independent families. If $u$ is linearly independent, then $m\leq d$ by The Steinitz Exchange Lemma (i). If $u$ is a basis, then $m=d$ by Finite-Dimensional Vector Spaces and Their Dimension (ii). If $m=d$, the previous paragraph gives a basis of length $m+p$ extending $u$, so $m+p=d$ by Existence and Invariance of the Length of a Basis (ii); hence $p=0$, and the basis is $u$ itself. This proves (ii).

Now spanning families. If $u$ spans $V$, then A Finite Spanning Family Contains a Basis (i) gives a basis of length $r\leq m$, and $r=d$ by Existence and Invariance of the Length of a Basis (ii); so $m\geq d$. If $u$ is a basis, then $m=d$ as before. Suppose finally that $m=d$ but $u$ is linearly dependent. Then Elementary Properties of Linear Independence (iv) gives $j\in[m]$ with

$$u_{j}\in\operatorname{span}(u_{1},\dots,u_{j-1})\subseteq\operatorname{span}(u^{(j)}),$$

where $u^{(j)}$ is the family of the other vectors of $u$, as in Dropping a Redundant Vector Does Not Change the Span, and the inclusion holds by The Span of a Finite Family is the Smallest Subspace Containing It (ii) and The Span of a Finite Family is the Smallest Subspace Containing It (iii). By Dropping a Redundant Vector Does Not Change the Span (i), $u^{(j)}$ would then span $V$, a spanning family of length $d-1$, against the bound $m\geq d$ just shown. So $u$ is linearly independent and spans $V$, hence is a basis. This proves (iii).

For dimension zero: if $d=0$, the basis $(b_{1},\dots,b_{d})$ is the empty family, so $V=\operatorname{span}()=\{0\}$ by The Span of a Finite Family is the Smallest Subspace Containing It (iv). Conversely, if $V=\{0\}$, the empty family spans $V$ (The Span of a Finite Family is the Smallest Subspace Containing It (iv)) and is linearly independent (Elementary Properties of Linear Independence (vi)), so it is a basis and $d=0$ by Finite-Dimensional Vector Spaces and Their Dimension (ii). This proves (iv).

Let now $W$ be a linear subspace of $V$. It is a vector space over $K$ by Linear Subspaces Are Vector Spaces; Intersections (i), and by Linear Subspaces Are Vector Spaces; Intersections (iv) a family in $W$ is linearly independent in $W$ exactly when it is linearly independent in $V$, and its span in $W$ is its span in $V$. Hence linearly independent families in $W$ have length at most $d$, by (ii); take one, $(c_{1},\dots,c_{q})$, of largest length $q\leq d$ (the empty family qualifies). It spans $W$: otherwise some $x\in W$ outside its span would give, by Elementary Properties of Linear Independence (iii), a longer linearly independent family in $W$. So $W$ is finite-dimensional (Finite-Dimensional Vector Spaces and Their Dimension (i)) with $\dim W=q\leq d$ (Finite-Dimensional Vector Spaces and Their Dimension (ii)). If $q=d$, then $(c_{1},\dots,c_{q})$ is a basis of $V$ by (ii), so $V=\operatorname{span}(c_{1},\dots,c_{q})\subseteq W$ by The Span of a Finite Family is the Smallest Subspace Containing It (iii), and $W=V$. Conversely, $W=V$ gives $\dim W=\dim V$. This proves (v).

Finally, Euclidean space. $\mathbb{R}^{n}$ is a real vector space by ℝⁿ Is a Real Vector Space (i), and with $I=[n]$ its addition and scalar multiplication are the pointwise ones (Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iv)). Let $x\in\mathbb{R}^{n}$ and $(\lambda_{1},\dots,\lambda_{n})\in\mathbb{R}^{n}$. Evaluating at $i\in[n]$ with Rules for Pointwise Operations on Real-Valued Maps: a Commutative Ring, Scalar Multiples and Evaluation (vi), using $(e_{k})_{i}=\delta_{ik}$ (Identity Matrix and Standard Basis Vectors (ii)) and extracting the $i$-th term with Iterated Operations over an Interval: Extracting One Term and Reversing the Order (i) (with $n-1$ in place of $n$ and $j=i$), we get

$$\Bigl(\sum_{k=1}^{n}\lambda_{k}e_{k}\Bigr)_{i}=\sum_{k=1}^{n}\lambda_{k}\delta_{ik}=\sum_{k=1}^{n-1}\lambda_{g_{i}(k)}\cdot0+\lambda_{i}\cdot1=\lambda_{i}.$$

Here the remaining terms $\lambda_{g_{i}(k)}\cdot0$ vanish because $g_{i}(k)\neq i$ (Bijections between Intervals: the Gap Map and the Reversal (i)), so that the standard basis vector $e_{g_{i}(k)}$ has entry $\delta_{i\,g_{i}(k)}=0$ at $i$. So $x=\sum_{k=1}^{n}\lambda_{k}e_{k}$ exactly when $\lambda_{k}=x_{k}$ for every $k$ (Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iii)): every $x$ has exactly one tuple of coefficients. By Coordinates with Respect to a Basis (i), $(e_{1},\dots,e_{n})$ is a basis, so $\mathbb{R}^{n}$ is finite-dimensional and $\dim\mathbb{R}^{n}=n$ (Finite-Dimensional Vector Spaces and Their Dimension (i), Finite-Dimensional Vector Spaces and Their Dimension (ii)). This proves (vi).