# Metamath Proof Explorer

Description: An entry of the adjunct (cofactor) matrix. (Contributed by SO, 11-Jul-2018)

Ref Expression
Hypotheses madufval.a ${⊢}{A}={N}\mathrm{Mat}{R}$
madufval.d ${⊢}{D}={N}\mathrm{maDet}{R}$
madufval.j ${⊢}{J}={N}\mathrm{maAdju}{R}$
madufval.b ${⊢}{B}={\mathrm{Base}}_{{A}}$

### Proof

Step Hyp Ref Expression
1 madufval.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 madufval.d ${⊢}{D}={N}\mathrm{maDet}{R}$
3 madufval.j ${⊢}{J}={N}\mathrm{maAdju}{R}$
4 madufval.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
7 1 2 3 4 5 6 maduval
9 simp1r ${⊢}\left(\left({i}={I}\wedge {j}={H}\right)\wedge {k}\in {N}\wedge {l}\in {N}\right)\to {j}={H}$
10 9 eqeq2d ${⊢}\left(\left({i}={I}\wedge {j}={H}\right)\wedge {k}\in {N}\wedge {l}\in {N}\right)\to \left({k}={j}↔{k}={H}\right)$
11 simp1l ${⊢}\left(\left({i}={I}\wedge {j}={H}\right)\wedge {k}\in {N}\wedge {l}\in {N}\right)\to {i}={I}$
12 11 eqeq2d ${⊢}\left(\left({i}={I}\wedge {j}={H}\right)\wedge {k}\in {N}\wedge {l}\in {N}\right)\to \left({l}={i}↔{l}={I}\right)$
18 simp2 ${⊢}\left({M}\in {B}\wedge {I}\in {N}\wedge {H}\in {N}\right)\to {I}\in {N}$
19 simp3 ${⊢}\left({M}\in {B}\wedge {I}\in {N}\wedge {H}\in {N}\right)\to {H}\in {N}$