The Leibniz formula for determinants allows us to express an $n \times n$ matrix determinant as a sum over permutations in $S_n$:
$$\det A = \sum_{\sigma \in S_n} \operatorname{sgn}(\sigma) \cdot \prod_{k=1}^n a_{\sigma(k), k}$$
A surprising amount of properties about determinants can be proven from this formula alone, using algebraic manipulation and basic facts about permutations. (Particularly, it's simple (and fun) to use it to show what happens to the determinant of a matrix when you apply elementary row operations; try it!)
Is there an existing proof of the fact that $\det AB = \det A \cdot \det B$ for $n \times n$ matrices $A$ and $B$, relying only on algebraic manipulation of the above formula? The resulting sums get rather ugly:
\begin{align*} \det A \cdot \det B &= \sum_{\sigma \in S_n, \tau \in S_n} \operatorname{sgn}(\sigma \circ \tau) \prod_{k=1}^n a_{\sigma(k), k} \cdot b_{\tau(k), k} \\ &\stackrel{\color{red}?}{\color{red}=} \sum_{\sigma \in S_n} \operatorname{sgn}(\sigma) \prod_{k=1}^n \left( \sum_{x=1}^n a_{\sigma(k), x} \cdot b_{x, k} \right) \\&= \det AB \end{align*}
How would I go about trying to prove that these expressions are equivalent?