I am reading "Linear Algebra" written by Takeshi Saito.
I like the following proof of the dimension theorem.
Are there any other books whose proof of this theorem looks like Saito's proof?
Saito's proof of the dimension theorem is like the following:
Let $V$ be a $K$ vector space. If both $x_1, \cdots, x_m$ and $y_1, \cdots, y_n$ are bases of $V$, then $m = n$.
Saito's proof:
Let $V$ be a $K$ vector space.
Let $x_1, \cdots, x_m$ be a basis of $V$.
Let $y_1, \cdots, y_n$ be a basis of $V$.
Let $V_0 := \{0\}$ and $V_i := K x_1 + \cdots K x_i$ for $i \in \{1, \dots, m\}$.
Let $W_0 := \{0\}$ and $W_j := K y_1 + \cdots + K y_j$ for $j \in \{1, \dots, n\}$.
Consider the following sequence:
$V_{i-1} = V_{i-1} + W_0 \subset V_{i-1} + W_1 \subset \cdots \subset V_{i-1} + W_n = V$.
$x_i \notin V_{i-1} = V_{i-1} + W_0$ and $x_i \in V = V_{i-1} + W_n$.
So, we can define $f : \{1, \cdots, m\} \to \{1, \cdots, n\}$ as follows:
$f : i \mapsto \min\{j | x_i \in V_{i-1} + W_j\}$
Consider the following sequence:
$W_{j-1} = V_0 + W_{j-1} \subset V_1 + W_{j-1} \subset \cdots \subset V_m + W_{j-1} = V$.
$y_j \notin W_{j-1} = V_0 + W_{j-1}$ and $y_j \in V = V_m + W_{j-1}$.
So, we can define $g : \{1, \cdots, n\} \to \{1, \cdots, m\}$ as follows:
$g : j \mapsto \min\{i | y_j \in V_i + W_{j-1}\}$
Let $f(i) = j$.
Then, $x_i \in V_{i-1} + W_j$ and $x_i \notin V_{i-1} + W_{j-1}$.
$x_i \in V_{i-1} + W_j$, so $V_{i-1} + W_j = V_i + W_j$.
$x_i \notin V_{i-1} + W_{j-1}$, so $V_{i-1} + W_{j-1} \subsetneqq V_i + W_{j-1}$.
$x_i \in V_{i-1} + W_j$, so we can write $x_i = a y_j + z$ for some $a \in K$ and some $z \in V_{i-1} + W_{j-1}$.
$x_i \notin V_{i-1} + W_{j-1}$, so $a \neq 0$.
$y_j = \frac{1}{a} (x_i - z) \in V_i + W_{j-1}$.
$\therefore V_i + W_{j-1} = V_i + W_j$.
$\therefore V_{i-1} + W_{j-1} \subsetneqq V_i + W_{j-1} = V_i + W_j = V_{i-1} + W_j$.
$\therefore y_j \notin V_{i-1} + W_{j-1}$.
$\therefore g(j) = i$.
So, $f(i) = j \Rightarrow g(j) = i$.
Similarly, $g(j) = i \Rightarrow f(i) = j$.
$\therefore f : \{1, \cdots, m\} \rightarrow \{1, \cdots, n\}$ is bijective.
$\therefore m = n$.