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

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $n\in\mathbb{N}$ and $A\in\mathcal{M}_{n}(\mathbb{R})$, with $[n]$ as in Intervals of Natural Numbers §segment, real matrices and their entries, points of $\mathbb{R}^{n}$ and their components as in Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §membership, the set $S_{n}$ of permutations of $[n]$, which is finite by Finite Sets: Removing an Element, Injective Self-Maps, Infinite Sets, Sets of Permutations, Pairs and Extended Tuples §permutations, the sign $\operatorname{sgn}:S_{n}\to\mathbb{R}$, sums and products and powers as in Commutative Rings, Fields and Ordered Fields: Standard Notation §rings, and the difference $n-1$ as in Commutative Rings, Fields and Ordered Fields: Standard Notation §numerals.

¶ For $\sigma\in S_{n}$, the map $[n]\to\mathbb{R}$, $i\mapsto A_{i\sigma(i)}$, exists, and its product $\prod_{i\in[n]}A_{i\sigma(i)}$ is an element of $\mathbb{R}$. There is exactly one map $t_{A}:S_{n}\to\mathbb{R}$ with $t_{A}(\sigma)=\operatorname{sgn}(\sigma)\prod_{i\in[n]}A_{i\sigma(i)}$ for every $\sigma\in S_{n}$.

¶ There is exactly one map $D_{n}:\mathcal{M}_{n}(\mathbb{R})\to\mathbb{R}$ with $D_{n}(B)=\sum_{\sigma\in S_{n}}t_{B}(\sigma)$ for every $B\in\mathcal{M}_{n}(\mathbb{R})$, where $t_{B}$ is the map of clause terms with $B$ in place of $A$.

¶ For every map $f:[n]\to[n]$ there is exactly one $A^{f}\in\mathcal{M}_{n}(\mathbb{R})$ with $(A^{f})_{ij}=A_{f(i)j}$ for all $i,j\in[n]$.

¶ For every $i\in[n]$ and $u\in\mathbb{R}^{n}$ there is exactly one $A[i\leftarrow u]\in\mathcal{M}_{n}(\mathbb{R})$ with $(A[i\leftarrow u])_{ij}=u_{j}$ for all $j\in[n]$ and $(A[i\leftarrow u])_{kj}=A_{kj}$ for all $j,k\in[n]$ with $k\neq i$.

¶ Let $2\le n$ for the order of $\mathbb{N}_{0}$, so that $n-1\in\mathbb{N}$ by The Index Map Skipping One Element of [n] §difference, and, for $i\in[n]$, let $s_{i}:[n-1]\to[n]$ be the deletion index map. For all $i,j\in[n]$ there exists a matrix $A^{(i,j)}\in\mathcal{M}_{n-1}(\mathbb{R})$, that is a map $A^{(i,j)}:[n-1]\times[n-1]\to\mathbb{R}$ as in Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §matrices, with entries $(A^{(i,j)})_{kl}=A_{s_{i}(k)s_{j}(l)}$ for all $k,l\in[n-1]$, and it is unique: every $C\in\mathcal{M}_{n-1}(\mathbb{R})$ with $C_{kl}=A_{s_{i}(k)s_{j}(l)}$ for all $k,l\in[n-1]$ is $A^{(i,j)}$.

¶ Let $2\le n$, so that $n-1\in\mathbb{N}$ by The Index Map Skipping One Element of [n] §difference, let $D_{n-1}$ be the map of clause determinant with $n-1$ in place of $n$, and, for $i,j\in[n]$, let $A^{(j,i)}\in\mathcal{M}_{n-1}(\mathbb{R})$ be the matrix of clause deletion with $j$ and $i$ in place of $i$ and $j$. There exists a matrix $B\in\mathcal{M}_{n}(\mathbb{R})$ with entries $B_{ij}=(-1)^{j+i}D_{n-1}(A^{(j,i)})$ for all $i,j\in[n]$, and it is unique: every $B'\in\mathcal{M}_{n}(\mathbb{R})$ with $B'_{ij}=(-1)^{j+i}D_{n-1}(A^{(j,i)})$ for all $i,j\in[n]$ is $B$.