Cauchy-Binet Formula Proof Intuition (Determinants) 
I am having trouble proving the Cauchy-Binet Theorem. I jotted down how far I got in the proof, but I just find myself stuck. Any guidance would be greatly appreciated!

I understand that 
$\begin{align*}\det(AB)
&=\sum_{j_1,j_2, ...,j_k=1}^n b_{j_1,1}b_{j_2,2}...b_{j_k,k}\det(A(J)) \\
&=\sum_{j_1,j_2,...,j_k\in \{1, 2, ..., n\} \text{ and all distinct}} b_{j_1,1}b_{j_2,2}...b_{j_k,k}\det(A(J)) \\
\end{align*}$
The last equations work as for any $J$, we will only consider the $j's$ to be all distinct (otherwise the determinant would be zero) and be integers that are between $1$ and $n$. Now, fix $J'=(j_1', j_2', ..., j_k')$ which organizes these $j's$ from least to greatest. Now, let $\sigma\in S_k$ and have $j'_i=j_{\sigma(i)}$ for $i=1, 2, ...,k$. 

I'm not sure why $\sigma$ is a permutation of $[n]$ here instead of being in $S_k$ like how I defined it above? I thought $\sigma$ was defined here by looking at the index of $j$ and not by $j$ itself (so it isn't associated with n). 

So, then I continue to get $\operatorname{sgn}(\sigma)\det(J')=\det(J)$. Thus, $j_i=j_{\sigma(\underbrace{\sigma^{-1}(i)}_{\in \{ 1, 2, ..., k\}})}=j'_{\sigma^{-1}(i)}$.
Thus, continuing our equation where we left off, we know 
$\begin{align*}
\det(AB)&=\sum_{j_1,j_2,...,j_k\in \{1, 2, ..., n\} \text{ and all distinct}} b_{j_1,1}b_{j_2,2}...b_{j_k,k}\det(A(J)) \\
&=\sum_{j_1,j_2,...,j_k\in \{1, 2, ..., n\} \text{ and all distinct}}  b_{j_1,1}b_{j_2,2}...b_{j_k,k}\operatorname{sgn}(\sigma)\det(A(J'))\\
&=\sum_{j_1,j_2,...,j_k\in \{1, 2, ..., n\} \text{ and all distinct}}\operatorname{sgn}(\sigma^{-1}) b_{j_1,1}b_{j_2,2}...b_{j_k,k}\det(A(J'))\\
&=\sum_{j_1,j_2,...,j_k\in \{1, 2, ..., n\} \text{ and all distinct}}\operatorname{sgn}(\sigma^{-1}) b_{j'_{\sigma^{-1}(1),1}}b_{j'_{\sigma^{-1}(2),2}}...b_{j'_{\sigma^{-1}(k),k}}\det(A(J'))\\
&= \text{and then I get confused here to show} = \sum_{J'}\det(A(J')\det(B(J'))
\end{align*}$
 A: 
Below is the full proof of the Cauchy-Binet Theorem for clarity. I appreciate the time others took to look at this question.

As the determinant is a multilinear function (the notation is $D$ for the function of the determinant here), we know
$\begin{align*}\det(AB)&=\det((AB)_1, (AB)_2, ..., (AB)_k) \text{ where } (AB)_i \text{denotes the } i^{th} \text{column of } AB\\
&=\det(\sum_{i=1}^k\sum_{j_1=1}^na_{i,j_1}b_{j_1,1}\cdot \hat{e}_i,\sum_{i=1}^k\sum_{j_2=1}^na_{i,j_2}b_{j_2,2}\cdot \hat{e}_i , ..., \sum_{i=1}^k\sum_{j_k=1}^na_{i,j_k}b_{j_k,k}\cdot \hat{e}_i ) \\
&=\sum_{i_1,i_2, ..., i_k=1}^k\det(\sum_{j_1=1}^na_{i_1,j_1}b_{j_1,1}\cdot \hat{e}_{i_1},\sum_{j_2=1}^na_{i_2,j_2}b_{j_2,2}\cdot \hat{e}_{i_2} , ..., \sum_{j_k=1}^na_{i_k,j_k}b_{j_k,k}\cdot \hat{e}_{i_k} ) \\
&=\sum_{i_1,i_2, ..., i_k=1}^k\sum_{j_1,j_2, ...,j_k=1}^n\det(a_{i_1,j_1}b_{j_1,1}\cdot \hat{e}_{i_1},a_{i_2,j_2}b_{j_2,2}\cdot \hat{e}_{i_2} , ..., a_{i_k,j_k}b_{j_k,k}\cdot \hat{e}_{i_k} ) \\
&=\sum_{j_1,j_2, ...,j_k=1}^n\sum_{i_1,i_2, ..., i_k=1}^k\det(a_{i_1,j_1}b_{j_1,1}\cdot \hat{e}_{i_1},a_{i_2,j_2}b_{j_2,2}\cdot \hat{e}_{i_2} , ..., a_{i_k,j_k}b_{j_k,k}\cdot \hat{e}_{i_k} ) \\
&=\sum_{j_1,j_2, ...,j_k=1}^n b_{j_1,1}b_{j_2,2}...b_{j_k,k}\sum_{i_1,i_2, ..., i_k=1}^k\det(a_{i_1,j_1}\cdot \hat{e}_{i_1},a_{i_2,j_2}\cdot \hat{e}_{i_2} , ..., a_{i_k,j_k}\cdot \hat{e}_{i_k} ) \\
&=\sum_{j_1,j_2, ...,j_k=1}^n b_{j_1,1}b_{j_2,2}...b_{j_k,k}\sum_{i_1,i_2, ..., i_k=1}^k\det(A(J)_{i_1,1}\cdot\hat e_{i_1},A(J)_{i_2,2}\cdot\hat e_{i_2},\dots,A(J)_{i_k,k}\cdot\hat e_{i_k})\\
&=\sum_{j_1,j_2, ...,j_k=1}^n b_{j_1,1}b_{j_2,2}...b_{j_k,k}\det(A(j_1, j_2, ..., j_k)) \\
&=\sum_{j_1,j_2, ...,j_k=1}^n b_{j_1,1}b_{j_2,2}...b_{j_k,k}\det(A(J)).
\end{align*}$
So, then note the following holds true which is explained below
$\begin{align*}\det(AB)
&=\sum_{j_1,j_2, ...,j_k=1}^n b_{j_1,1}b_{j_2,2}...b_{j_k,k}\det(A(J)) \\
&=\sum_{j_1,j_2,...,j_k\in \{1, 2, ..., n\} \text{ and all distinct}} b_{j_1,1}b_{j_2,2}...b_{j_k,k}\det(A(J)).
\end{align*}$
The last equations work as for any $J$, we will only consider the $j's$ to be all distinct (otherwise the determinant would be zero) and be integers that are between $1$ and $n$. Now, fix $J'=(j_1', j_2', ..., j_k')$ which organizes these $j's$ from least to greatest. Now, consider $\sigma=\begin{pmatrix}
j_1' & j_2' & \cdots & j_k' \\ j_1 & j_2 & \cdots & j_n
\end{pmatrix}\implies \epsilon(j_1, j_2, ..., j_k)\det(A(J'))=\det(A(J)).$
So, 
$\begin{align*}\det(AB)&=\sum_{j_1,j_2,...,j_k\in \{1, 2, ..., n\}} b_{j_1,1}b_{j_2,2}...b_{j_k,k}\epsilon(j_1, j_2, ..., j_k)\det(A(J'))\\
&=\sum_{j_1,j_2,...,j_k\in \{1, 2, ..., n\}} \epsilon(j_1, j_2, ..., j_k) b_{j_1,1}b_{j_2,2}...b_{j_k,k}\det(A(j'_1, j'_2, ..., j'_k))\\
&=\sum_{j_1,j_2,...,j_k\in \{1, 2, ..., n\}} \epsilon(j_1, j_2, ..., j_k) b_{1,j_1}b_{2,j_2}...b_{k,j_k}\det(A(j'_1, j'_2, ..., j'_k))\\
&=\sum_{1\leq j'_1<...<j'_k\leq n}(\sum_{l_1, l_2, ..., l_n=1}^k \epsilon(l_1, l_2, ..., l_k) b_{l_1,j'_1}b_{l_2,j'_2}...b_{l_k,j'_k})\det(A(j'_1, j'_2, ..., j'_k))\\
&=\sum_{1\leq j'_1<...<j'_k\leq n}\det(B(j'_1, j'_2, ..., j'_k))\det(A(j'_1, j'_2, ..., j'_k)). \text{QED}
\end{align*}$
A: It is helpful to define some notation to aid visualizing the various summations :

*

*$[n]$ = the set $\{1, 2, \ldots, n\}$


*$\binom{[n]}{k}$ = set of all subsets of $[n]$ of size $k$


*$P_k$ = set of all bijections ('permutations') $: [k] \rightarrow [k]$


*$Q_k$ = set of all mappings $: [k] \rightarrow [k]$


*$P_{k, n}$ = set of all injections $: [k] \rightarrow [n]$, ($k \leq n$)


*$Q_{k, n}$ = set of all mappings $: [k] \rightarrow [n]$


*$R_{k, n}$ = set of all strictly increasing injections $: [k] \rightarrow [n]$, ($k \leq n$)
Then :

*

*$\left|\binom{[n]}{k}\right|$ = ${}^nC_k = \binom{n}{k} = \frac{n!}{k!(n - k)!} $


*$|P_k|$ = $k!$


*$|Q_k|$ = $k^k$


*$|P_{k, n}|$ = ${}^n\!P_k = \frac{n!}{(n - k)!}$


*$|Q_{k, n}|$ = $n^k$


*$|R_{k, n}|$ = ${}^nC_k = \left|\binom{[n]}{k}\right|$
There is a one-to-one correspondence between the set $R_{k, n}$ and the set $\binom{[n]}{k}$ - for, each strictly increasing injection $: [k] \rightarrow [n]$ defines and is defined by a unique $k$-element subset of $[n]$. The set $P_{k, n}$ includes $R_{k, n}$ as a subset but is $k!$ times larger since for every strictly increasing injection $f \in R_{k, n}$ there are $k!$ reorderings of $f$, thus producing $k!$ distinct injection mappings in $P_{k, n}$.
We can denote a mapping by a list notation, eg $(i_1, \ldots, i_k) \in Q_k$ denotes a mapping taking $r$ to $i_r \in [k]$ for each $r \in \{1, 2, \ldots, k\}$. And $(j_1, \ldots, j_k) \in Q_{k, n}$ denotes a mapping taking $r$ to $j_r \in [n]$ for each $r \in \{1, 2, \ldots, k\}$.
The summation notation $\displaystyle \sum_{i_1, i_2, \ldots, i_k = 1}^{k}$ which denotes the iterated ordered sum $\displaystyle \sum_{i_1 = 1}^{k} \, \sum_{i_2 = 1}^{k} \ldots \sum_{i_k = 1}^{k} $ can also be written as the unordered associative/commutative sum $\displaystyle \sum_{(i_1, i_2, \ldots, i_k) \in Q_k}$, since the order of adding up the summands and the bracketing does not matter. And because the $i_r$ independently take on all the values from $1$ to $k$, the mappings $(i_1, \ldots, i_k)$ are not in general injective, so that they range over $Q_k$ rather than $P_k$.
By contrast the summation $\displaystyle \sum_{j_1, j_2, \ldots, j_k \in \{1, 2, \ldots, n\}\; \text{and all distinct}}$ can be written as the associative/commutative sum $\displaystyle \sum_{(j_1, j_2, \ldots, j_k) \in P_{k, n}}$ with $P_{k, n}$ as the indexing set, since we are now confined to mappings $(j_1, j_2, \ldots, j_k)$ from $[k]$ to $[n]$ which are injective.
Assume we have $A \in F_{k \times n}$ and $B \in F_{n \times k}$, where $F$ is a field of scalars, and $k < n$. (The case $k =n$ of the Cauchy-Binet formula reduces to the product formula for determinants, ie $\det AB = \det A \cdot \det B$, and the case $k > n$ implies $A$, and hence $AB \in F_{k \times k}$, has rank $\leq n < k$, so $AB$ must be singular $\therefore$ LHS of formula is zero, and RHS is also zero as it is an empty sum).
For any $J = (j_1, j_2, \ldots, j_k) \in Q_{k, n}$, we define square matrix $A(J) \in F_{k \times k}$ as having $r^{\text{th}}$ column equal to column $j_r$ of $A$ $(r = 1, 2, \ldots, k)$, and square matrix $B(J) \in F_{k \times k}$ as having $r^{\text{th}}$ row equal to row $j_r$ of $A$ $(r = 1, 2, \ldots, k)$. This means columns of $A(J)$ are picked from $A$, but not necessarily in the order they appear in $A$, and a column may be picked more than once, producing an $A(J)$ with $\det A(J) = 0$, and similarly with $B$.
Thus from
\begin{equation}
\det AB = \sum_{(j_1, j_2, \ldots, j_k) \in Q_{k, n}} (b_{j_1, 1} b_{j_2, 2} \cdots b_{j_k, k}) \cdot \det (A(J))
\tag{1}
\label{eq:detAB-Qkn}
\end{equation}
we obtain
\begin{equation}
\det AB = \sum_{(j_1, j_2, \ldots, j_k) \in P_{k, n}} (b_{j_1, 1} b_{j_2, 2} \cdots b_{j_k, k}) \cdot \det(A(J))
\tag{2}
\label{eq:detAB-Pkn}
\end{equation}
by removing all the non-injective mappings. Now define a mapping $J = (j_1, j_2, \ldots, j_k) \rightarrow \psi(J) = J' = (j'_1, j'_2, \ldots, j'_k)$ from $P_{k, n} \rightarrow R_{k, n}$, where $(j'_1, j'_2, \ldots, j'_k)$ is the ordered version of $(j_1, j_2, \ldots, j_k)$. For each $J \in P_{k, n}$, let $\sigma_J \in P_k$ be the permutation that maps $(j'_1, j'_2, \ldots, j'_k)$ back to $(j_1, j_2, \ldots, j_k)$, ie
\begin{equation}
\sigma_J = 
\left(
\begin{array}{llll}
j'_1 & j'_2 & \cdots & j'_k \\
j_1 & j_2 & \cdots & j_k \\
\end{array}
\right)
\tag{3}
\label{eq:perm-sigma}
\end{equation}
(ie $\sigma_J$ maps the original position of an object in the list to its new position in the permuted list), so that $j_{\sigma_J(r)} = j'_r, \forall r \in \{1, 2, \ldots, k\}$. Note the numbers that are being permuted are numbers in the range $\{1, 2, \ldots, n\}$ but $\sigma_J \in P_k$ acts on their positions which are numbers in the range $\{1, 2, \ldots, k\}$.
If $\sigma_J$ is expressed as a composition of $t$ swap permutations (ie transpositions) then $\operatorname{sgn}(\sigma_J) = (-1)^{t}$ and if the corresponding sequence of $t$ column swaps is applied to the column selections for $A(J')$ then the matrix $A(J)$ is produced. But since each column swap multiplies the determinant by $-1$, we then have
\begin{eqnarray}
\det A(J) & = & (-1)^{t} \det A(J') \tag{4} \label{eq:JtoJ'-perm-t} \\
\mbox{ie.} \hspace{1em} \det A(J) & = & \operatorname{sgn}(\sigma_J) \det A(J') \tag{5} \label{eq:JtoJ'-perm-sigma} \\
\therefore\  \hspace{1em} \det AB & = & \sum_{J = (j_1, j_2, \ldots, j_k) \in P_{k, n}} (b_{j_1, 1} b_{j_2, 2} \cdots b_{j_k, k}) \cdot \operatorname{sgn}(\sigma_J) \cdot \det(A(J')) \tag{6} \label{eq:detAB-sigma}
\end{eqnarray}
Now gather together the terms in the summation (\ref{eq:detAB-sigma}) which have a common $J'$. The set of all possible $J'$ is $R_{k, n}$ and for each $J' \in R_{k, n}$ there will be $k!$ terms $J \in P_{k, n}$ that map to that same $J'$ under $\psi$, ie all the injective maps which when placed in order are the same as $J'$. Thus the above sum (\ref{eq:detAB-sigma}) partitions into the double sum :
\begin{equation}
\det AB = \sum_{J' = (j'_1, j'_2, \ldots, j'_k) \in R_{k, n}} \left( \sum_{\substack{J = (j_1, j_2, \ldots, j_k) \in P_{k, n}, \\ \psi(J) = J' }} (b_{j_1, 1} b_{j_2, 2} \cdots b_{j_k, k}) \cdot \operatorname{sgn}(\sigma_J) \right) \cdot \det(A(J'))
\tag{7} \label{eq:detAB-double-sum}
\end{equation}
Writing $j_r = j_{\sigma_J(\sigma_J^{-1}(r))}$ we have $j_r = j'_{\sigma_J^{-1}(r)}$, and so as the inverse of a permutation has the same signature as the permutation itself, the summand in the inner sum of (\ref{eq:detAB-double-sum}) is :
\begin{equation}
(b_{j'_{\sigma_J^{-1}(1)}, 1} b_{j'_{\sigma_J^{-1}(2)}, 2} \cdots b_{j'_{\sigma_J^{-1}(k)}, k}) \cdot \operatorname{sgn}(\sigma_J^{-1})
\tag{8} \label{eq:detAB-inner-sum-sigma-inverse}
\end{equation}
and this ranges over all $J \in P_{k, n}$ satisfying $\psi(J) = J'$. But such a range of $J$ corresponds with all $k!$ permutations of the in-order $J'$ (which is fixed in the inner sum), and thus $\sigma_J$ over this range of $J$ covers all $k!$ elements of the set $P_k$ of permutations of $[k]$ - hence $\sigma_J^{-1}$ over this range of $J$ covers the latter set of permutations also. Thus with the substitution $\tau = \sigma_J^{-1}$ the inner sum in (\ref{eq:detAB-double-sum}) equals (for a given fixed $J'$) :
\begin{equation}
\sum_{\tau \in P_k} (b_{j'_{\tau(1)}, 1} b_{j'_{\tau(2)}, 2} \cdots b_{j'_{\tau(k)}, k}) \cdot \operatorname{sgn}(\tau)
\tag{9} \label{eq:detAB-inner-sum-tau}
\end{equation}
But from the definition of $B(J')$, $B(J')_{s,r} = b_{j'_{s},r} \forall\:s, r$, and so $B(J')_{\tau(r),r} = b_{j'_{\tau(r)},r}$ for $r \in \{1, 2, \ldots, k\}$, and thus the inner sum (\ref{eq:detAB-inner-sum-tau}) equals :
\begin{equation}
\sum_{\tau \in P_{k}} (B(J')_{\tau(1), 1} B(J')_{\tau(2), 2} \cdots B(J')_{\tau(k), k}) \cdot \operatorname{sgn}(\tau)
\tag{10} \label{eq:detAB-inner-sum-BJ'}
\end{equation}
which is the column-wise Leibniz formula for $\det B(J')$. Thus from (\ref{eq:detAB-double-sum}) :
\begin{eqnarray}
\det AB & = & \sum_{J' \in R_{k,n}} \det B(J') \cdot \det A(J') \tag{11} \label{eq:detAB-Rkn} \\
& = & \sum_{S \in \binom{[n]}{k}} \det A_S \cdot \det B_S \tag{12} \label{eq:detAB-S}
\end{eqnarray}
using the one-to-one correspondence between sets $R_{k, n}$ and $\binom{[n]}{k}$, where $A_S$ denotes the $k \times k$ matrix obtained from $A$ by selecting the column numbers in $A$ from the set $S$, and $B_S$ denotes the $k \times k$ matrix obtained from $B$ by selecting the row numbers in $B$ from the set $S$.
