I stumbled onto the following identity, and I would like to know: Is it known by some name and are there some references I might cite (or is it actually too trivial to be mentioned anywhere)? Are there any slick proofs that come to mind (for example something like Will Jagy's in this somehow related question)? (I may need to explain this to some folks who are not familiar with the exterior algebra.)
Let $V$ be a $n$-dimensional inner product space and let $A$ be the $k\times n$ matrix whose rows are the $n$-dimensional vectors $a_1,\dots,a_k\subset V$ and let $B$ be the $n\times k$ matrix whose columns are the $n$-dimensional vectors $b_1,\dots,b_k\subset V$.
Furthermore suppose for simplicity that $a_1,\dots,a_k$ are orthonormal in $V$ and that $a_1,\dots,a_k,\tilde{a}_{k+1},\dots,\tilde{a}_n$ form an orthonormal basis for $V$.
Proposition: $\det(AB)=\det(M)$ where $M$ is the $n\times n$ matrix whose first $k$ columns are $b_1,\dots,b_k$ and whose last $n-k$ columns are $\tilde{a}_{k+1},\dots,\tilde{a}_n$.
Proof: Recall that the inner product on $V$ induces an inner product on $\Lambda^kV$ so that $\det(AB)=\langle a_1\wedge\cdots\wedge a_k,b_1\wedge\cdots\wedge b_k\rangle$. Then, by the definition of the Hodge star, $\det(AB)\omega=b_1\wedge\cdots\wedge b_k\wedge \star(a_1\wedge\cdots\wedge a_k)$, where $\omega\subset\Lambda^nV$ is the unit $n$-vector (n.b. $\omega=a_1\wedge\cdots\wedge\tilde{a}_n$, it is not simply a unit $n$-dimensional vector). But then $\star(a_1\wedge\cdots\wedge a_k)=\tilde{a}_{k+1}\wedge\cdots\wedge\tilde{a}_n$, so that $\det(AB)\omega=b_1\wedge\cdots\wedge b_k\wedge \tilde{a}_{k+1}\wedge\cdots\wedge\tilde{a}_n$, which yields the proposition as desired.
