[proofplan]
Choose a basis of the intersection $U \cap W$ and extend it separately to a basis of $U$ and to a basis of $W$. The combined list consisting of the intersection basis, the extra basis vectors for $U$, and the extra basis vectors for $W$ will be shown to be a basis of $U+W$. Spanning follows by decomposing an arbitrary element of $U+W$ as $u+w$; [linear independence](/page/Linear%20Independence) follows by moving the $U$-part of a relation to the $W$-part and observing that the common vector lies in $U \cap W$. Counting the vectors in this basis gives the dimension formula.
[/proofplan]
[step:Choose a basis of the intersection and extend it to bases of both subspaces]
Since $U$ and $W$ are subspaces of the [finite-dimensional vector space](/page/Finite-Dimensional%20Vector%20Space) $V$, [citetheorem:9922] implies that $U$, $W$, and $U \cap W$ are finite-dimensional over $k$.
Let $r=\dim_k(U \cap W)$. Choose an ordered basis
\begin{align*}
\mathcal{A}=(a_1,\ldots,a_r)
\end{align*}
of $U \cap W$, with the convention that $\mathcal{A}$ is the empty list when $r=0$.
Extend $\mathcal{A}$ to an ordered basis of $U$:
\begin{align*}
\mathcal{B}_U=(a_1,\ldots,a_r,u_1,\ldots,u_s),
\end{align*}
where $s \ge 0$ is an integer. Extend $\mathcal{A}$ to an ordered basis of $W$:
\begin{align*}
\mathcal{B}_W=(a_1,\ldots,a_r,w_1,\ldots,w_t),
\end{align*}
where $t \ge 0$ is an integer. Thus
\begin{align*}
\dim_k U=r+s
\end{align*}
and
\begin{align*}
\dim_k W=r+t.
\end{align*}
[/step]
[step:Show the combined list spans $U+W$]
Define the ordered list
\begin{align*}
\mathcal{C}=(a_1,\ldots,a_r,u_1,\ldots,u_s,w_1,\ldots,w_t)
\end{align*}
of vectors in $V$. We prove that $\mathcal{C}$ spans $U+W$.
Let $x \in U+W$. By the definition of the sum of subspaces, there exist vectors $u \in U$ and $w \in W$ such that
\begin{align*}
x=u+w.
\end{align*}
Since $\mathcal{B}_U$ is a basis of $U$, there exist scalars $\alpha_1,\ldots,\alpha_r,\beta_1,\ldots,\beta_s \in k$ such that
\begin{align*}
u=\sum_{i=1}^{r}\alpha_i a_i+\sum_{j=1}^{s}\beta_j u_j.
\end{align*}
Since $\mathcal{B}_W$ is a basis of $W$, there exist scalars $\gamma_1,\ldots,\gamma_r,\delta_1,\ldots,\delta_t \in k$ such that
\begin{align*}
w=\sum_{i=1}^{r}\gamma_i a_i+\sum_{\ell=1}^{t}\delta_\ell w_\ell.
\end{align*}
Adding these two expansions gives
\begin{align*}
x=\sum_{i=1}^{r}(\alpha_i+\gamma_i)a_i+\sum_{j=1}^{s}\beta_j u_j+\sum_{\ell=1}^{t}\delta_\ell w_\ell.
\end{align*}
Hence $x$ lies in the span of $\mathcal{C}$. Therefore $\mathcal{C}$ spans $U+W$.
[/step]
[step:Prove the combined list is linearly independent]
Suppose that scalars $\lambda_1,\ldots,\lambda_r,\mu_1,\ldots,\mu_s,\nu_1,\ldots,\nu_t \in k$ satisfy
\begin{align*}
\sum_{i=1}^{r}\lambda_i a_i+\sum_{j=1}^{s}\mu_j u_j+\sum_{\ell=1}^{t}\nu_\ell w_\ell=0.
\end{align*}
Move the $W$-basis terms to the other side:
\begin{align*}
\sum_{i=1}^{r}\lambda_i a_i+\sum_{j=1}^{s}\mu_j u_j=-\sum_{\ell=1}^{t}\nu_\ell w_\ell.
\end{align*}
The left-hand side belongs to $U$, because $a_i \in U \cap W \subset U$ and $u_j \in U$. The right-hand side belongs to $W$, because $w_\ell \in W$. Hence the common vector belongs to $U \cap W$.
Since $\mathcal{A}=(a_1,\ldots,a_r)$ spans $U \cap W$, there exist scalars $\rho_1,\ldots,\rho_r \in k$ such that
\begin{align*}
\sum_{i=1}^{r}\lambda_i a_i+\sum_{j=1}^{s}\mu_j u_j=\sum_{i=1}^{r}\rho_i a_i.
\end{align*}
Rearranging gives a linear relation among the basis vectors in $\mathcal{B}_U$:
\begin{align*}
\sum_{i=1}^{r}(\lambda_i-\rho_i)a_i+\sum_{j=1}^{s}\mu_j u_j=0.
\end{align*}
Because $\mathcal{B}_U$ is linearly independent, $\mu_j=0$ for every $1 \le j \le s$ and $\lambda_i=\rho_i$ for every $1 \le i \le r$.
Substituting $\mu_1=\cdots=\mu_s=0$ into the original relation gives
\begin{align*}
\sum_{i=1}^{r}\lambda_i a_i+\sum_{\ell=1}^{t}\nu_\ell w_\ell=0.
\end{align*}
This is a linear relation among the basis vectors in $\mathcal{B}_W$, so linear independence of $\mathcal{B}_W$ implies $\lambda_i=0$ for every $1 \le i \le r$ and $\nu_\ell=0$ for every $1 \le \ell \le t$. All coefficients in the original relation are zero, so $\mathcal{C}$ is linearly independent.
[guided]
We need to prove that no nonzero linear relation can occur among the vectors
\begin{align*}
a_1,\ldots,a_r,u_1,\ldots,u_s,w_1,\ldots,w_t.
\end{align*}
Assume that scalars $\lambda_1,\ldots,\lambda_r,\mu_1,\ldots,\mu_s,\nu_1,\ldots,\nu_t \in k$ satisfy
\begin{align*}
\sum_{i=1}^{r}\lambda_i a_i+\sum_{j=1}^{s}\mu_j u_j+\sum_{\ell=1}^{t}\nu_\ell w_\ell=0.
\end{align*}
The key move is to separate the vectors coming from the basis of $U$ from the extra vectors coming from the basis of $W$. Rearranging gives
\begin{align*}
\sum_{i=1}^{r}\lambda_i a_i+\sum_{j=1}^{s}\mu_j u_j=-\sum_{\ell=1}^{t}\nu_\ell w_\ell.
\end{align*}
The left-hand side is an element of $U$, because each $a_i$ lies in $U \cap W \subset U$ and each $u_j$ lies in $U$. The right-hand side is an element of $W$, because each $w_\ell$ lies in $W$. Therefore the vector represented by both sides lies in $U \cap W$.
Because $\mathcal{A}=(a_1,\ldots,a_r)$ is a basis of $U \cap W$, that common vector has an expansion using only the $a_i$. Thus there are scalars $\rho_1,\ldots,\rho_r \in k$ such that
\begin{align*}
\sum_{i=1}^{r}\lambda_i a_i+\sum_{j=1}^{s}\mu_j u_j=\sum_{i=1}^{r}\rho_i a_i.
\end{align*}
Moving the right-hand side to the left gives
\begin{align*}
\sum_{i=1}^{r}(\lambda_i-\rho_i)a_i+\sum_{j=1}^{s}\mu_j u_j=0.
\end{align*}
This is now a relation among the vectors of the basis
\begin{align*}
\mathcal{B}_U=(a_1,\ldots,a_r,u_1,\ldots,u_s).
\end{align*}
Since a basis is linearly independent, every coefficient in this relation is zero. Hence $\mu_j=0$ for every $1 \le j \le s$, and $\lambda_i=\rho_i$ for every $1 \le i \le r$.
Return to the original relation and use $\mu_1=\cdots=\mu_s=0$. We obtain
\begin{align*}
\sum_{i=1}^{r}\lambda_i a_i+\sum_{\ell=1}^{t}\nu_\ell w_\ell=0.
\end{align*}
This relation involves only vectors from the basis
\begin{align*}
\mathcal{B}_W=(a_1,\ldots,a_r,w_1,\ldots,w_t).
\end{align*}
Since $\mathcal{B}_W$ is linearly independent, all its coefficients in the displayed relation vanish. Therefore $\lambda_i=0$ for every $1 \le i \le r$ and $\nu_\ell=0$ for every $1 \le \ell \le t$. Together with $\mu_j=0$ for every $1 \le j \le s$, this proves that the original relation was the zero relation. Hence $\mathcal{C}$ is linearly independent.
[/guided]
[/step]
[step:Count the basis vectors to obtain the dimension formula]
The preceding two steps show that
\begin{align*}
\mathcal{C}=(a_1,\ldots,a_r,u_1,\ldots,u_s,w_1,\ldots,w_t)
\end{align*}
is a basis of $U+W$. Therefore
\begin{align*}
\dim_k(U+W)=r+s+t.
\end{align*}
Using $\dim_k U=r+s$, $\dim_k W=r+t$, and $\dim_k(U \cap W)=r$, we compute
\begin{align*}
\dim_k U+\dim_k W-\dim_k(U \cap W)=(r+s)+(r+t)-r.
\end{align*}
Hence
\begin{align*}
\dim_k U+\dim_k W-\dim_k(U \cap W)=r+s+t.
\end{align*}
Combining the two equalities gives
\begin{align*}
\dim_k(U+W)=\dim_k U+\dim_k W-\dim_k(U \cap W).
\end{align*}
This proves the dimension formula.
[/step]
