# Metamath Proof Explorer

Description: The coefficients of an adjunct (matrix of cofactors) expressed as determinants of the minor matrices (alternative definition) of the original matrix. (Contributed by AV, 31-Dec-2018)

Ref Expression
Hypotheses maducoevalmin1.a ${⊢}{A}={N}\mathrm{Mat}{R}$
maducoevalmin1.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
maducoevalmin1.d ${⊢}{D}={N}\mathrm{maDet}{R}$
maducoevalmin1.j ${⊢}{J}={N}\mathrm{maAdju}{R}$
Assertion maducoevalmin1 ${⊢}\left({M}\in {B}\wedge {I}\in {N}\wedge {H}\in {N}\right)\to {I}{J}\left({M}\right){H}={D}\left({H}\left({N}\mathrm{minMatR1}{R}\right)\left({M}\right){I}\right)$

### Proof

Step Hyp Ref Expression
1 maducoevalmin1.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 maducoevalmin1.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 maducoevalmin1.d ${⊢}{D}={N}\mathrm{maDet}{R}$
4 maducoevalmin1.j ${⊢}{J}={N}\mathrm{maAdju}{R}$
5 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
6 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
7 1 3 4 2 5 6 maducoeval ${⊢}\left({M}\in {B}\wedge {I}\in {N}\wedge {H}\in {N}\right)\to {I}{J}\left({M}\right){H}={D}\left(\left({i}\in {N},{j}\in {N}⟼if\left({i}={H},if\left({j}={I},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right)\right)$
8 eqid ${⊢}{N}\mathrm{minMatR1}{R}={N}\mathrm{minMatR1}{R}$
9 1 2 8 5 6 minmar1val ${⊢}\left({M}\in {B}\wedge {H}\in {N}\wedge {I}\in {N}\right)\to {H}\left({N}\mathrm{minMatR1}{R}\right)\left({M}\right){I}=\left({i}\in {N},{j}\in {N}⟼if\left({i}={H},if\left({j}={I},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right)$
10 9 3com23 ${⊢}\left({M}\in {B}\wedge {I}\in {N}\wedge {H}\in {N}\right)\to {H}\left({N}\mathrm{minMatR1}{R}\right)\left({M}\right){I}=\left({i}\in {N},{j}\in {N}⟼if\left({i}={H},if\left({j}={I},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right)$
11 10 eqcomd ${⊢}\left({M}\in {B}\wedge {I}\in {N}\wedge {H}\in {N}\right)\to \left({i}\in {N},{j}\in {N}⟼if\left({i}={H},if\left({j}={I},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right)={H}\left({N}\mathrm{minMatR1}{R}\right)\left({M}\right){I}$
12 11 fveq2d ${⊢}\left({M}\in {B}\wedge {I}\in {N}\wedge {H}\in {N}\right)\to {D}\left(\left({i}\in {N},{j}\in {N}⟼if\left({i}={H},if\left({j}={I},{1}_{{R}},{0}_{{R}}\right),{i}{M}{j}\right)\right)\right)={D}\left({H}\left({N}\mathrm{minMatR1}{R}\right)\left({M}\right){I}\right)$
13 7 12 eqtrd ${⊢}\left({M}\in {B}\wedge {I}\in {N}\wedge {H}\in {N}\right)\to {I}{J}\left({M}\right){H}={D}\left({H}\left({N}\mathrm{minMatR1}{R}\right)\left({M}\right){I}\right)$