Proof of The Determinant of a Triangular Matrix is the Product of its Diagonal Entries

Each result cited is universally quantified over the data in its own statement. We work in Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices.

Preliminaries. $\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 by Ordered Fields §ordered-field, and sums and products over finite sets are as in Commutative Rings, Fields and Ordered Fields: Standard Notation §rings. The elements of $[n]$ are the $k\in\mathbb{N}$ with $k\le n$, and the rules of Arithmetic and Order of the Natural Numbers apply to them; in particular the order is total, by Arithmetic and Order of the Natural Numbers §partial-order and Arithmetic and Order of the Natural Numbers §trichotomy, which is used below without further mention. $S_{n}$ is a finite nonempty set by Finite Sets: Removing an Element, Injective Self-Maps, Infinite Sets, Sets of Permutations, Pairs and Extended Tuples §permutations, and its elements are exactly the bijections $\sigma:[n]\to[n]$, by Permutations of a Set and the Set of Permutations of [n] §membership; such a $\sigma$ is injective by Injective, Surjective and Bijective Functions between Classes §bijective. $\mathrm{id}_{[n]}\in S_{n}$ by Permutations of [n]: Identity, Composition, Inverses, Translations and Transpositions §identity, and $\operatorname{sgn}(\mathrm{id}_{[n]})=1$ by Rules for the Sign of a Permutation §identity.

(D) For $B\in\mathcal{M}_{n}(\mathbb{R})$ and $\sigma\in S_{n}$, let $t_{B}:S_{n}\to\mathbb{R}$, $t_{B}(\sigma)=\operatorname{sgn}(\sigma)\prod_{k\in[n]}B_{k\sigma(k)}$, be the map 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 §terms with $B$ in place of $A$; by Determinant of a Real Square Matrix §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 §determinant, $\det B=\sum_{\sigma\in S_{n}}t_{B}(\sigma)$.

Step 1: a permutation that moves no element upwards is the identity. Let $\sigma\in S_{n}$ with $\sigma(i)\le i$ for every $i\in[n]$, and let

$$K=\{m\in\mathbb{N}:\forall i\,((i\in[n]\wedge i\le m)\Rightarrow\sigma(i)=i)\}\subseteq\mathbb{N}.$$

$1\in K$: let $i\in[n]$ with $i\le1$. Since $1\le i$ by Arithmetic and Order of the Natural Numbers §least, $i=1$. Then $\sigma(1)\le1$ by hypothesis and $1\le\sigma(1)$ by Arithmetic and Order of the Natural Numbers §least, as $\sigma(1)\in[n]$; so $\sigma(1)=1$.

If $m\in K$, then $m+1\in K$: let $i\in[n]$ with $i\le m+1$. If $i\le m$, then $\sigma(i)=i$ as $m\in K$. Otherwise $m<i\le m+1$, and $i<m+1$ is excluded by Arithmetic and Order of the Natural Numbers §successor; so $i=m+1$. Suppose $\sigma(i)\neq i$. Then $\sigma(i)<i=m+1$ by hypothesis, so $m<\sigma(i)$ is excluded by Arithmetic and Order of the Natural Numbers §successor, and $\sigma(i)\le m$. As $\sigma(i)\in[n]$ and $m\in K$, $\sigma(\sigma(i))=\sigma(i)$, and injectivity of $\sigma$ (Injective, Surjective and Bijective Functions between Classes §injective) gives $\sigma(i)=i$, a contradiction. Hence $\sigma(i)=i$, and $m+1\in K$.

By Arithmetic and Order of the Natural Numbers §induction, $K=\mathbb{N}$. For $i\in[n]$ we have $i\in K$ and $i\le i$, so $\sigma(i)=i$; hence $\sigma=\mathrm{id}_{[n]}$.

Clause lower. Assume $A_{ij}=0$ for all $i,j\in[n]$ with $i<j$. Let $\sigma\in S_{n}$ with $\sigma\neq\mathrm{id}_{[n]}$. By Step 1 there is $i\in[n]$ for which $\sigma(i)\le i$ fails, that is, $i<\sigma(i)$, so $A_{i\sigma(i)}=0$ by the assumption. The map $[n]\to\mathbb{R}$, $k\mapsto A_{k\sigma(k)}$, thus takes the value $0$ at $i$, and its product is $0$ by Products over Finite Sets: a Single Factor, Vanishing in a Field, and Signs and Monotonicity in an Ordered Ring §zero, $\mathbb{R}$ being a field; so $t_{A}(\sigma)=0$. For $\sigma=\mathrm{id}_{[n]}$, $t_{A}(\mathrm{id}_{[n]})=1\cdot\prod_{k\in[n]}A_{kk}=\prod_{k\in[n]}A_{kk}$. By (D) and 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 with $y=\mathrm{id}_{[n]}$,

$$\det A=t_{A}(\mathrm{id}_{[n]})=\prod_{k\in[n]}A_{kk}=\prod_{i=1}^{n}A_{ii}.$$

Clause upper. Assume $A_{ij}=0$ for all $i,j\in[n]$ with $j<i$. By Transpose of a Real Matrix §transpose with $m=n$, the transpose $A^{\top}\in\mathcal{M}_{n}(\mathbb{R})$ has $(A^{\top})_{ij}=A_{ji}$ for $i,j\in[n]$. For $i,j\in[n]$ with $i<j$, the assumption applied to the entry $A_{ji}$ gives $(A^{\top})_{ij}=A_{ji}=0$. So the clause lower applies to $A^{\top}$ and gives $\det(A^{\top})=\prod_{i=1}^{n}(A^{\top})_{ii}=\prod_{i=1}^{n}A_{ii}$. Finally $\det A=\det(A^{\top})$ by Rules for the Determinant: Rows, Scalar Multiples and the Transpose §transpose, so $\det A=\prod_{i=1}^{n}A_{ii}$.