Metamath Proof Explorer

Description: Define the adjugate or adjunct (matrix of cofactors) of a square matrix. This definition gives the standard cofactors, however the internal minors are not the standard minors, see definition in Lang p. 518. (Contributed by Stefan O'Rear, 7-Sep-2015) (Revised by SO, 10-Jul-2018)

Ref Expression
Assertion df-madu ${⊢}\mathrm{maAdju}=\left({n}\in \mathrm{V},{r}\in \mathrm{V}⟼\left({m}\in {\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}⟼\left({i}\in {n},{j}\in {n}⟼\left({n}\mathrm{maDet}{r}\right)\left(\left({k}\in {n},{l}\in {n}⟼if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)\right)\right)\right)\right)\right)$

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmadu ${class}\mathrm{maAdju}$
1 vn ${setvar}{n}$
2 cvv ${class}\mathrm{V}$
3 vr ${setvar}{r}$
4 vm ${setvar}{m}$
5 cbs ${class}\mathrm{Base}$
6 1 cv ${setvar}{n}$
7 cmat ${class}\mathrm{Mat}$
8 3 cv ${setvar}{r}$
9 6 8 7 co ${class}\left({n}\mathrm{Mat}{r}\right)$
10 9 5 cfv ${class}{\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}$
11 vi ${setvar}{i}$
12 vj ${setvar}{j}$
13 cmdat ${class}\mathrm{maDet}$
14 6 8 13 co ${class}\left({n}\mathrm{maDet}{r}\right)$
15 vk ${setvar}{k}$
16 vl ${setvar}{l}$
17 15 cv ${setvar}{k}$
18 12 cv ${setvar}{j}$
19 17 18 wceq ${wff}{k}={j}$
20 16 cv ${setvar}{l}$
21 11 cv ${setvar}{i}$
22 20 21 wceq ${wff}{l}={i}$
23 cur ${class}{1}_{r}$
24 8 23 cfv ${class}{1}_{{r}}$
25 c0g ${class}{0}_{𝑔}$
26 8 25 cfv ${class}{0}_{{r}}$
27 22 24 26 cif ${class}if\left({l}={i},{1}_{{r}},{0}_{{r}}\right)$
28 4 cv ${setvar}{m}$
29 17 20 28 co ${class}\left({k}{m}{l}\right)$
30 19 27 29 cif ${class}if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)$
31 15 16 6 6 30 cmpo ${class}\left({k}\in {n},{l}\in {n}⟼if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)\right)$
32 31 14 cfv ${class}\left({n}\mathrm{maDet}{r}\right)\left(\left({k}\in {n},{l}\in {n}⟼if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)\right)\right)$
33 11 12 6 6 32 cmpo ${class}\left({i}\in {n},{j}\in {n}⟼\left({n}\mathrm{maDet}{r}\right)\left(\left({k}\in {n},{l}\in {n}⟼if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)\right)\right)\right)$
34 4 10 33 cmpt ${class}\left({m}\in {\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}⟼\left({i}\in {n},{j}\in {n}⟼\left({n}\mathrm{maDet}{r}\right)\left(\left({k}\in {n},{l}\in {n}⟼if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)\right)\right)\right)\right)$
35 1 3 2 2 34 cmpo ${class}\left({n}\in \mathrm{V},{r}\in \mathrm{V}⟼\left({m}\in {\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}⟼\left({i}\in {n},{j}\in {n}⟼\left({n}\mathrm{maDet}{r}\right)\left(\left({k}\in {n},{l}\in {n}⟼if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)\right)\right)\right)\right)\right)$
36 0 35 wceq ${wff}\mathrm{maAdju}=\left({n}\in \mathrm{V},{r}\in \mathrm{V}⟼\left({m}\in {\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}⟼\left({i}\in {n},{j}\in {n}⟼\left({n}\mathrm{maDet}{r}\right)\left(\left({k}\in {n},{l}\in {n}⟼if\left({k}={j},if\left({l}={i},{1}_{{r}},{0}_{{r}}\right),{k}{m}{l}\right)\right)\right)\right)\right)\right)$