Proof of The Determinant is Multiplicative

Let $S_{n}$ be the set of permutations of $[n]$ and let $[n]^{n}$ be the set of $n$-tuples in $[n]$, that is, of maps $f:[n]\to[n]$; both are nonempty and finite, by claims 3 and 4 of Finiteness of Cartesian Products, Tuple Sets, and Permutation Sets, and $S_{n}$ is a subset of $[n]^{n}$. For $f\in[n]^{n}$ let $B_{f}$ be the real $n\times n$ matrix with $(B_{f})_{ij}=B_{f(i)\,j}$ for all $i,j\in[n]$, and put

Expanding the product of the rows. Fix $\sigma\in S_{n}$. By Product of Real Matrices,

so Generalized Distributivity: Expanding a Product of Finite Sums, applied with $m=n$ to the family whose entry at $(i,k)$ is $A_{ik}B_{k\sigma(i)}$, gives

By claim 2 of Properties of Finite Products each inner product factors as

Multiplying by $\mathrm{sgn}(\sigma)$ and using claim 4 of Properties of a Sum over a Finite Index Set,

Interchanging the two sums. Summing the last identity over $\sigma\in S_{n}$ and interchanging the two sums by claim 5 of Peeling, Splitting, and Interchange for Sums over a Finite Index Set, applied to the map on the product of $S_{n}$ and $[n]^{n}$ whose value at $(\sigma,f)$ is the summand above, and then taking the constant factor $\alpha_{f}$ out of the inner sum by claim 4 of Properties of a Sum over a Finite Index Set,

the last equality by the form of the determinant recorded in Row Properties of the Determinant.

Discarding the non-injective terms. Let $f\in[n]^{n}$ and suppose $f$ is not bijective. By claim 1 of An Injective Self-Map of a Finite Set is a Bijection it is then not injective, so there are $p,q\in[n]$ with $p\ne q$ and $f(p)=f(q)$. Consequently $(B_{f})_{pj}=B_{f(p)j}=B_{f(q)j}=(B_{f})_{qj}$ for every $j\in[n]$, and claim 4 of Row Properties of the Determinant gives $\det B_{f}=0$, so the term at $f$ vanishes by Zero Products and Elementary Identities in a Field. The remaining $f$ are exactly the elements of $S_{n}$, a nonempty subset of $[n]^{n}$, so claim 4 of Peeling, Splitting, and Interchange for Sums over a Finite Index Set gives

Conclusion. For $f\in S_{n}$ the matrix $B_{f}$ is the row permutation of $B$ by $f$, so claim 3 of Row Properties of the Determinant gives $\det B_{f}=\mathrm{sgn}(f)\det B$. Taking the constant factor $\det B$ out of the sum by claim 4 of Properties of a Sum over a Finite Index Set,