Proof of The Determinant is Multiplicative

Each result cited is universally quantified over the data in its own statement.

Conventions. We work in Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices; $\mathbb{R}$ is an ordered field by The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness §reals, hence a field and a commutative ring by Ordered Fields §ordered-field and Fields §field, and sums and products over finite sets are as in Commutative Rings, Fields and Ordered Fields: Standard Notation §rings. For finite sets $D$ and $E$ we use: (P1) for maps $f,g:D\to\mathbb{R}$, $\prod_{x\in D}f(x)g(x)=\bigl(\prod_{x\in D}f(x)\bigr)\bigl(\prod_{x\in D}g(x)\bigr)$, by Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §termwise for the multiplication of $\mathbb{R}$; (P2) for a map $h:D\times E\to\mathbb{R}$, $\sum_{x\in D}\sum_{y\in E}h(x,y)=\sum_{y\in E}\sum_{x\in D}h(x,y)$, by Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §product; (P3) for $f:D\to\mathbb{R}$ and $c\in\mathbb{R}$, $c\sum_{x\in D}f(x)=\sum_{x\in D}c\,f(x)$, by Sums over Finite Sets in a Commutative Ring and in an Ordered Field: Distributivity, Products of Sums, Vanishing Terms, Sums over Pairs, Expanding Products of Sums, Counting, Comparison, Monotonicity and the Triangle Inequality §distributive; (P4) if $G\subseteq D$, $f:D\to\mathbb{R}$ and $f(x)=0$ for every $x\in D\setminus G$, then $\sum_{x\in D}f(x)=\sum_{x\in G}f(x)$, by Sums over Finite Sets in a Commutative Ring and in an Ordered Field: Distributivity, Products of Sums, Vanishing Terms, Sums over Pairs, Expanding Products of Sums, Counting, Comparison, Monotonicity and the Triangle Inequality §vanishing. Entries of $AB$ are given by Product of Real Matrices §product. For every $M\in\mathcal{M}_{n}(\mathbb{R})$, $\det M=\sum_{\sigma\in S_{n}}t_{M}(\sigma)$ with $t_{M}(\sigma)=\operatorname{sgn}(\sigma)\prod_{i\in[n]}M_{i\sigma(i)}$, by Determinant of a Real Square Matrix §determinant, The Determinant Map and the Matrices Formed from a Square Matrix by Reindexing Rows, Replacing a Row and Deleting a Row and a Column Exist and Are Unique §determinant and The Determinant Map and the Matrices Formed from a Square Matrix by Reindexing Rows, Replacing a Row and Deleting a Row and a Column Exist and Are Unique §terms. For a map $f:[n]\to[n]$, $B^{f}\in\mathcal{M}_{n}(\mathbb{R})$ is the matrix of The Determinant Map and the Matrices Formed from a Square Matrix by Reindexing Rows, Replacing a Row and Deleting a Row and a Column Exist and Are Unique §row-reindexing with $B$ in place of $A$, so $(B^{f})_{ij}=B_{f(i)j}$ for all $i,j\in[n]$.

Index sets and maps. Let $F=[n]^{[n]}$, a set by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set §set whose elements are exactly the maps $[n]\to[n]$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set §members, and finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §maps. By Permutations of a Set and the Set of Permutations of [n] §permutations and Permutations of a Set and the Set of Permutations of [n] §membership, $S_{n}\subseteq F$ and the elements of $S_{n}$ are exactly the bijections $[n]\to[n]$; $S_{n}$ is finite by Finite Sets: Removing an Element, Injective Self-Maps, Infinite Sets, Sets of Permutations, Pairs and Extended Tuples §permutations. Let $a:F\to\mathbb{R}$, $b:S_{n}\times F\to\mathbb{R}$, $w:S_{n}\times F\to\mathbb{R}$ and $d:F\to\mathbb{R}$ be the maps with

$$a(\varphi)=\prod_{i\in[n]}A_{i\varphi(i)},\quad b(\sigma,\varphi)=\prod_{x\in[n]}B_{\varphi(x)\sigma(x)},\quad w(\sigma,\varphi)=a(\varphi)\operatorname{sgn}(\sigma)b(\sigma,\varphi),\quad d(\varphi)=\sum_{\sigma\in S_{n}}\operatorname{sgn}(\sigma)b(\sigma,\varphi).$$

Step 1: expanding a product of sums. Fix $\sigma\in S_{n}$, and let $u_{\sigma}:[n]\times[n]\to\mathbb{R}$ be the map with $u_{\sigma}(x,y)=A_{xy}B_{y\sigma(x)}$. For $x\in[n]$, $\sum_{y\in[n]}u_{\sigma}(x,y)=(AB)_{x\sigma(x)}$. By Expanding a Product of Sums over a Fixed Finite Index Set §expansion with $[n]$ as both index sets and $u_{\sigma}$ as $u$, and then (P1) for each $\varphi\in F$ with the maps $x\mapsto A_{x\varphi(x)}$ and $x\mapsto B_{\varphi(x)\sigma(x)}$ on $[n]$,

$$\prod_{x\in[n]}(AB)_{x\sigma(x)}=\prod_{x\in[n]}\sum_{y\in[n]}A_{xy}B_{y\sigma(x)}=\sum_{\varphi\in F}\prod_{x\in[n]}A_{x\varphi(x)}B_{\varphi(x)\sigma(x)}=\sum_{\varphi\in F}a(\varphi)b(\sigma,\varphi).\tag{1}$$

Step 2: exchanging the sums. By the conventions, (1), (P3) with $c=\operatorname{sgn}(\sigma)$, then (P2) for $w$ on $S_{n}\times F$, then (P3) with $c=a(\varphi)$,

$$\det(AB)=\sum_{\sigma\in S_{n}}\operatorname{sgn}(\sigma)\prod_{x\in[n]}(AB)_{x\sigma(x)}=\sum_{\sigma\in S_{n}}\sum_{\varphi\in F}w(\sigma,\varphi)=\sum_{\varphi\in F}\sum_{\sigma\in S_{n}}w(\sigma,\varphi)=\sum_{\varphi\in F}a(\varphi)d(\varphi).\tag{2}$$

For $\varphi\in F$, $\sigma\in S_{n}$ and $x\in[n]$, $B_{\varphi(x)\sigma(x)}=(B^{\varphi})_{x\sigma(x)}$, so $\operatorname{sgn}(\sigma)b(\sigma,\varphi)=t_{B^{\varphi}}(\sigma)$ and

$$d(\varphi)=\sum_{\sigma\in S_{n}}t_{B^{\varphi}}(\sigma)=\det(B^{\varphi}).\tag{3}$$

Step 3: maps that are not injective. Let $\varphi\in F\setminus S_{n}$. Then $\varphi$ is a map $[n]\to[n]$ that is not a bijection. If $\varphi$ were injective, it would be a bijection by Finite Sets: Removing an Element, Injective Self-Maps, Infinite Sets, Sets of Permutations, Pairs and Extended Tuples §injective-self-map, $[n]$ being finite; so $\varphi$ is not injective, that is, there are $p,q\in[n]$ with $p\neq q$ and $\varphi(p)=\varphi(q)$. Then $(B^{\varphi})_{pj}=B_{\varphi(p)j}=B_{\varphi(q)j}=(B^{\varphi})_{qj}$ for every $j\in[n]$, so $\det(B^{\varphi})=0$ by Rules for the Determinant: Rows, Scalar Multiples and the Transpose §equal-rows with $B^{\varphi}$ in place of $A$, and $a(\varphi)d(\varphi)=0$ by (3). By (P4) with $G=S_{n}\subseteq F$, (2) becomes

$$\det(AB)=\sum_{\pi\in S_{n}}a(\pi)d(\pi).$$

Step 4: permutations. For $\pi\in S_{n}$, $d(\pi)=\det(B^{\pi})=\operatorname{sgn}(\pi)\det B$ by (3) and Rules for the Determinant: Rows, Scalar Multiples and the Transpose §row-reindexing with $B$ in place of $A$, and $\operatorname{sgn}(\pi)a(\pi)=t_{A}(\pi)$; so $a(\pi)d(\pi)=\det B\cdot t_{A}(\pi)$. Hence, by (P3),

$$\det(AB)=\sum_{\pi\in S_{n}}\det B\cdot t_{A}(\pi)=\det B\sum_{\pi\in S_{n}}t_{A}(\pi)=\det A\cdot\det B,$$

which is clause multiplicative.