[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.[/step]

[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: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]