---
tag: PNN3764365
kind: proof
name: Proof of the dimension formula for a direct product
msc: [15A03]
proves: 06HN47VPTH
uses: [0EX2HPXPJ6, 0KCQ9Y3QKA, 0CRMGPAH83, 088RYKAWK9, 03GSZ8RTZJ, 0ZHWKQMVX5]
sources:
  - url: https://publish.obsidian.md/ilithmath/Books/Badescu,+Lectures+on+Geometry/1.+Linear+Algebra/2.+Vector+Spaces/1.+Subspaces,+Generators,+Independence/Dimension+of+Direct+Product+of+Vector+Spaces
---

## Proof

We build a basis of $V \times W$ from bases of $V$ and $W$.

1. Let $n = \dim V$ and $m = \dim W$. Let $(v_1, \dots, v_n)$ be a [[basis|0KCQ9Y3QKA]] of $V$ and $(w_1, \dots, w_m)$ a basis of $W$.
2. In the [[product|0EX2HPXPJ6]] $V \times W$, consider the family $\mathcal{F}$ of the $n + m$ vectors $(v_1, 0), \dots, (v_n, 0), (0, w_1), \dots, (0, w_m)$.
3. The family $\mathcal{F}$ [[spans|088RYKAWK9]] $V \times W$. Let $(v, w) \in V \times W$. Since the bases span, $v = \sum_{i=1}^n a_i v_i$ and $w = \sum_{j=1}^m c_j w_j$ for some scalars $a_i, c_j \in F$.
4. By the componentwise operations of the product, $\sum_i a_i (v_i, 0) + \sum_j c_j (0, w_j) = \left(\sum_i a_i v_i, \sum_j c_j w_j\right) = (v, w)$.
5. The family $\mathcal{F}$ is [[linearly independent|0CRMGPAH83]]. Suppose $\sum_i a_i (v_i, 0) + \sum_j c_j (0, w_j) = (0, 0)$ with $a_i, c_j \in F$.
6. By the computation of step 4, this says $\sum_i a_i v_i = 0$ in $V$ and $\sum_j c_j w_j = 0$ in $W$.
7. The family $(v_i)$ is linearly independent, so all $a_i = 0$. The family $(w_j)$ is linearly independent, so all $c_j = 0$.
8. By steps 3 to 7, $\mathcal{F}$ is a basis of $V \times W$. It is finite, so $V \times W$ is [[finite-dimensional|0ZHWKQMVX5]].
9. A basis of $V \times W$ has $n + m$ vectors, so $\dim(V \times W) = n + m = \dim V + \dim W$ by the definition of [[dimension|03GSZ8RTZJ]].

## Idea

A pair $(v, w)$ splits as $(v, 0) + (0, w)$. So a basis of $V$ placed in the first slot, together with a basis of $W$ placed in the second slot, gives a basis of the product. The two bases do not interact, so their sizes add.