Basis-independent derivation of the fact that the determinant of the composition of two linear maps is the product of the determinant of each A maximal form $\omega$ on $V$ is defined as an alternating type $(0, n)$ tensor (where $\dim V = n$). From there, the determinant is defined as,
$$ \det \phi \equiv \dfrac{\omega\left(\phi(e_1), \dots, \phi(e_n)\right)}{\omega\left(e_1, \dots, e_n \right)}.$$
One can show that this definition of the determinant is independent of the choice of both a maximal form and a basis. I'm interested in knowing whether it's possible to show from this definition that $\det (\phi \circ \psi) = \det \phi \det \psi$ without going to a specific basis. I get to,
$$\det (\phi \circ \psi) = \dfrac{\omega\big(\phi(\psi(e_1)), \dots, \phi(\psi(e_n))\big)}{\omega\left(e_1, \dots, e_n \right)}$$
and have no idea how to proceed. If doing so is possible, any hints on how to proceed would be appreciated.
 A: Here's my attempt at a self-answer (guided by the hint given by @Zack Fox). I had to do it by cases and would appreciate a constructively-valid proof if somebody can provide one.
Case 1: If $\psi$ is an automorphism, then $\{\psi(e_i)\}$ is a basis of V, and since $\det \phi$ is independent of our choice of basis, we have,
$$ \det \phi = \dfrac{\omega \bigg(\phi \big(\psi(e_1) \big), \dots, \phi \big(\psi(e_n) \big) \bigg)}{\omega \big(\psi(e_1), \dots, \psi(e_n) \big)} .$$
Thus,
\begin{align}
\det \phi \det \psi &= \dfrac{\omega \bigg(\phi \big(\psi(e_1) \big), \dots, \phi \big(\psi(e_n) \big) \bigg)}{\omega \big(\psi(e_1), \dots, \psi(e_n) \big)} \cdot \dfrac{\omega \big(\psi(e_1), \dots, \psi(e_n) \big)}{\omega(e_1, \dots, e_n)} \\ 
&= \dfrac{\omega \bigg(\phi \big(\psi(e_1) \big), \dots, \phi \big(\psi(e_n) \big) \bigg)}{\omega(e_1, \dots, e_n)} \equiv \det (\phi \circ \psi).
\end{align}
Case 2: If $\psi$ is not an automorphism, then $\{\psi(e_i)\}$ is linearly dependent and so is $\phi \big( \{\psi(e_i)\} \big)$. Thus, $$ \omega \big(\psi(e_1), \dots, \psi(e_n) \big) = \omega \bigg(\phi \big(\psi(e_1) \big), \dots, \phi \big(\psi(e_n) \big) \bigg) = 0.$$
Putting all of that together,
$$\det (\phi \circ \psi) \equiv \dfrac{\omega \bigg(\phi \big(\psi(e_1) \big), \dots, \phi \big(\psi(e_n) \big) \bigg)}{\omega(e_1, \dots, e_n)} = 0 \\ = \det \phi \cdot \dfrac{\omega \big(\psi(e_1), \dots, \psi(e_n) \big)}{\omega(e_1, \dots, e_n)} = \det \phi \det \psi. $$
A: $
\newcommand\Ext{{\textstyle\bigwedge}}
\newcommand\MVects[1]{\mathop{{\textstyle\bigwedge}^{\!#1}}}
\newcommand\K{\mathbb K}
\newcommand\form[1]{\langle#1\rangle}
$I will admit that I oversold myself a little. Determinants in the exterior algebra are easy, but actually linking this up with alternating multilinear functions does actually take some effort.
I will start by defining the exterior algebra, describing a little bit of its structure, and then showing the analogous result that you want in that context. Then I will show how this transfers to alternating multilinear maps. I should also note here that alternating tensors and the exterior algebra are not the same thing in nonzero characteristic; only when the characteristic is zero (like over $\mathbb R$) can these be made isomorphic.
A good reference for multilinear algebra, particularly involving the exterior algebra, is Werner Greub's Multilinear Algebra. However, I cannot promise that the way I do things below is the same way he does things.
The Exterior Algebra
The exterior algebra $\Ext V$ is the associative algebra generated by $V$ subject only to the relations $v\wedge v = 0$ for all $v \in V$, where it is traditional to write the algebra product as $\wedge$. Note that from this viewpoint $V \subseteq \Ext V$. Concretely, we construct $\Ext V$ by quotienting the tensor algebra by the ideal generated by $\{v\otimes v \;:\; v \in V\}$. What really matters, though, is its universal property which determines it uniquely up to isomorphism:

*

*Identify $V$ as a subset of $\Ext V$, and let $A$ be any associative algebra. Then every linear map $f : V \to A$ such that $f(v)^2 = 0$ extends uniquely to an algebra homomorphism $f' : \Ext V \to A$, i.e. $f'(v) = f(v)$ for all $v \in V$.

Of particular interest to us is the case $A = \Ext V$. If $f : V \to V$ is any linear map, then we can widen the codomain so that $f : V \to \Ext V$. Then the universal propery applies, and $f$ extends to a homomorphism $\Ext V \to \Ext V$; this is called the outermorphism of $f$, and we will use the same symbol $f$ to denote it.
We will also be interested in the exterior powers $\MVects kV$. These are analogous to tensor powers, but for alternating maps instead of just multilinear. They are also characterized by a universal propery:

*

*Let $W$ be another vector space. If $f : V^k \to W$ is an alternating multilinear map, then it extends uniquely to a linear map $f : \MVects kV \to W$ such that
$$
  f(v_1\wedge v_2\wedge\dotsb\wedge v_k) = f(v_1, v_2, \dotsc, v_k).
$$
Note that I've used the same symbol $f$ twice, though $f$ on the LHS and $f$ on the RHS are technically different objects.

As this notation suggests, we can identify $\MVects kV$ as a subspace of $\Ext V$, whereupon we find that $\Ext V$ is a graded algebra
$$
  \Ext V = \MVects0V\oplus\MVects1V\oplus\MVects2V\oplus\dotsb\oplus\MVects nV
$$
where we can identify $\MVects0V$ as the field of scalars and $\MVects1V = V$, and $n$ is the dimension of $V$.
Finally, the following lemma should be easy to establish:

*

*Let $v_1,\dotsc,v_k \in V$. Then $v_1\wedge\dotsb\wedge v_k = 0$ iff these vectors are linearly dependent.

Determinants
This is everything we need. By the previous lemma, $\MVects nV$ is a one dimensional space. Also by this lemma, the outermorphism of any $f : V \to V$ preserves grade. Thus there is a unique scalar $\det f$ such that for every $I \in \MVects nV$
$$
  f(I) = (\det f)I.
$$
In this way, we have defined the determinant $\det f$.
Now let $g : V \to V$ be any other linear function. No more need be said:
$$
  \det(f\circ g)I = (f\circ g)(I) = f(g(I)) = (\det f)g(I) = (\det f)(\det g)I.
$$
Alternating Multilinear Maps
Let $\K$ be our field of scalars. By the universal property of the exterior powers, any alternating multilinear $\phi : V^k \to \K$ can be considered as a map linear $\MVects kV \to \K$; in other words, it is an element of the dual space $\phi \in (\MVects kV)^*$. There is a natural bilinear pairing $\MVects kV^*\times\MVects kV \to \K$ given by
$$
  \form{\alpha_1\wedge\dotsb\wedge\alpha_k,\; v_1\wedge\dotsb\wedge v_k}
= \det\Bigl(\alpha_i(v_j)\Bigr)_{i,j=1}^k.
$$
On the RHS we are taking the determinant of the matrix with entries $\alpha_i(v_j)$. Showing this is natural would take us too far astray, so I will simply use this as a definition. This pairing establishes linear isomorphisms $(\MVects kV)^* \cong \MVects kV^*$, in particular when $k = n$. To be concrete $\phi \in (\MVects kV)^*$ corresponds to a unique $\phi' \in \MVects kV^*$ such that
$$
  \phi(X) = \form{\phi', X}.
$$
We can also put all of these bilinear forms together into a form $\Ext V^*\times\Ext V \to \K$ by linearity and by declaring that $\form{X, Y} = 0$ when $X, Y$ have different grades. This establishes that there is a linear isomorphism $\psi : (\Ext V)^* \cong \Ext V^*$.
Now if $f : V \to V$ is linear, it has a dual $f^* : V^* \to V^*$. The above should make it straighforward to establish that the dual outermorphism $(\Ext V)^* \to (\Ext V)^*$ is exactly the dual of the outermorphism of $f^*$. Using e.g. $f_\wedge$ to denote outermorphisms for the moment, what I mean precisely is
$$
  \psi\circ(f_\wedge)^*\circ\psi^{-1} = (f^*)_\wedge.
$$
Thus, we will write
$$
  \form{X, f(Y)} = \form{f^*(X), Y}
$$
for any $X \in \Ext V^*$ and $Y \in \Ext V$.
It is well known that $\det f^* = \det f$ (this is the fact that the determinant of the transpose of a matrix is the determinant of the original matrix). Let $\phi \in (\MVects nV)^*$ and $\phi' = \psi(\phi) \in \MVects nV^*$, and let $X = v_1\wedge\dotsb\wedge v_n$ for $v_1,\dotsc,v_n \in V$. Then
$$
  \frac{\phi(f(v_1),\dotsc,f(v_n))}{\phi(v_1,\dotsc,v_n)}
= \frac{\form{\phi', f(X)}}{\form{\phi', X}}
= \frac{\form{f^*(\phi'), X}}{\form{\phi', X}}
= (\det f)\frac{\form{\phi', X}}{\form{\phi', X}}
= \det f.
$$
A: Here's a way to see it using old-fashioned matrices. It's essentially as the other proofs given here.
What you've written is the fact that if $C_1, \dots, C_n$ are the columms of a matrix $A$, then if $d(C_1, \dots, C_n)$ is an alternating multilinear function such that $d(e_1, \dots, e_n) = 1$, then $d(C_1, \dots, C_n) = \det A$.
This implies that if $f(C_1, \dots, C_n)$ is an alternating multilinear function, then
$$
f(C_1, \dots, C_n) = f(e_1, \dots, e_n)d(C_1, \dots, C_n).
$$
Now, given a matrix $B$, the function
$$
f(C_1, \dots, C_n) = d(BC_1, \dots, BC_n).
$$
is alternating multilinear. Since $BC_1, \dots, BC_n$ are the columns of $BA$, it follows that \begin{align*}
\det(BA) &= d(BC_1, \dots, BC_n)\\
&=f(C_1, \dots, C_n)\\
&= f(e_1, \dots, e_n)d(C_1, \dots, C_n)\\
&= d(Be_1, \dots, Be_n)\det A\\
&= (\det B)(\det A).
\end{align*}
