Proof of Adjugate Formula for the Matrix Inverse

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

Setup. We work in Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices. Entries of scalar multiples of matrices are given by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §operations, two matrices in $\mathcal{M}_{n}(\mathbb{R})$ are equal when all their entries agree by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §equality, and $\delta_{ik}=(I_{n})_{ik}$ denotes the entries of the identity matrix. Write $d=\det A$, so $d\neq0$, let $c=1/d$, so that $c\,d=1$, and let $N=c\operatorname{adj}(A)\in\mathcal{M}_{n}(\mathbb{R})$, the scalar multiple of the adjugate; thus $N=(1/\det A)\operatorname{adj}(A)$.

The matrix $c(dI_{n})$. For $i,k\in[n]$, by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §operations applied twice, $(c(dI_{n}))_{ik}=c\,(d\,\delta_{ik})=\delta_{ik}$. Hence $c(dI_{n})=I_{n}$.

Clause formula. By Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes §scalar (with $m=n=p$, $s=c$), by Cofactor Expansion of the Determinant along a Row or a Column, and the Adjugate Identity §adjugate-identity, and by the previous paragraph,

$$AN=A\bigl(c\operatorname{adj}(A)\bigr)=c\bigl(A\operatorname{adj}(A)\bigr)=c\,(dI_{n})=I_{n},\qquad NA=\bigl(c\operatorname{adj}(A)\bigr)A=c\bigl(\operatorname{adj}(A)A\bigr)=c\,(dI_{n})=I_{n}.$$

So $N$ is an inverse of $A$ by Inverse Matrix and Invertible Real Square Matrix §inverse, and $A$ is invertible by Inverse Matrix and Invertible Real Square Matrix §invertible. By that clause $A$ has exactly one inverse, denoted $A^{-1}$, so $A^{-1}=N=(1/\det A)\operatorname{adj}(A)$.

Clause entries. Let $i,j\in[n]$. By clause formula, Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §operations and Minor, Cofactor, and Adjugate of a Real Square Matrix §adjugate, which gives $\operatorname{adj}(A)_{ij}=C_{ji}(A)$,

$$(A^{-1})_{ij}=(c\operatorname{adj}(A))_{ij}=c\,C_{ji}(A)=C_{ji}(A)/\det A.$$