[proofplan] We define an auxiliary form $d(b_1, \dots, b_n) = \det(Ab_1 \mid \cdots \mid Ab_n)$, verify it is alternating multilinear, and apply the [Determinant as Universal Volume Form](/theorems/393) to conclude $d = (\det A) \cdot \det$. Evaluating at the columns of $B$ yields $\det(AB) = (\det A)(\det B)$. [/proofplan] [step:Define the auxiliary alternating multilinear form] For vectors $b_1, \dots, b_n \in \mathbb{F}^n$, define \begin{align*} d: (\mathbb{F}^n)^n &\to \mathbb{F} \\ (b_1, \dots, b_n) &\mapsto \det(Ab_1 \mid \cdots \mid Ab_n), \end{align*} where $(Ab_1 \mid \cdots \mid Ab_n)$ denotes the $n \times n$ matrix whose $j$th column is $Ab_j$. [/step] [step:Verify $d$ is alternating and multilinear] [claim:Auxiliary Form Properties] The function $d$ is multilinear and alternating. [/claim] [proof] **Multilinearity:** Fix all arguments except the $j$th. The map $b_j \mapsto Ab_j$ is linear (matrix-vector multiplication), so the $j$th column of the matrix $(Ab_1 \mid \cdots \mid Ab_n)$ depends linearly on $b_j$. Since $\det$ is multilinear in its columns, $d$ is linear in $b_j$. **Alternating:** If $b_k = b_\ell$ for some $k \neq \ell$, then $Ab_k = Ab_\ell$, so the matrix $(Ab_1 \mid \cdots \mid Ab_n)$ has two equal columns. Since $\det$ is alternating, $d(b_1, \dots, b_n) = 0$. [/proof] [/step] [step:Apply the universal volume form property to express $d$ in terms of $\det$] Since $d$ is an alternating multilinear form on $(\mathbb{F}^n)^n$, the [Determinant as Universal Volume Form](/theorems/393) gives \begin{align*} d(b_1, \dots, b_n) = d(e_1, \dots, e_n) \cdot \det B, \end{align*} where $B = (b_1 \mid \cdots \mid b_n)$ is the matrix with columns $b_j$, and $\{e_1, \dots, e_n\}$ is the standard basis of $\mathbb{F}^n$. Now evaluate the normalisation constant: \begin{align*} d(e_1, \dots, e_n) = \det(Ae_1 \mid \cdots \mid Ae_n) = \det A, \end{align*} since the columns of $A$ are $Ae_1, \dots, Ae_n$. [guided] The [Determinant as Universal Volume Form](/theorems/393) states that any alternating multilinear form $d$ on $(\mathbb{F}^n)^n$ satisfies $d(b_1, \dots, b_n) = d(e_1, \dots, e_n) \cdot \det B$ where $B$ is the matrix with columns $b_j$. We verified $d$ is alternating multilinear in the previous step, so this applies. The scalar $d(e_1, \dots, e_n)$ is computed by plugging in the standard basis: $d(e_1, \dots, e_n) = \det(Ae_1 \mid \cdots \mid Ae_n)$. But $Ae_j$ is the $j$th column of $A$, so $(Ae_1 \mid \cdots \mid Ae_n) = A$ and $d(e_1, \dots, e_n) = \det A$. Combining: $d(b_1, \dots, b_n) = (\det A) \cdot \det B$. [/guided] [/step] [step:Conclude $\det(AB) = (\det A)(\det B)$] Setting $b_j$ to be the $j$th column of $B$, so that $B = (b_1 \mid \cdots \mid b_n)$ and $(Ab_1 \mid \cdots \mid Ab_n) = AB$: \begin{align*} \det(AB) = d(b_1, \dots, b_n) = (\det A)(\det B). \end{align*} [/step]