Metamath Proof Explorer

Definition df-madu

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 ⊢maAdju=n∈V,r∈V⟼m∈BasenMatr⟼i∈n,j∈n⟼nmaDetr⁡k∈n,l∈n⟼ifk=jifl=i1r0rkml

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmadu classmaAdju
1 vn setvarn
2 cvv classV
3 vr setvarr
4 vm setvarm
5 cbs classBase
6 1 cv setvarn
7 cmat classMat
8 3 cv setvarr
9 6 8 7 co classnMatr
10 9 5 cfv classBasenMatr
11 vi setvari
12 vj setvarj
13 cmdat classmaDet
14 6 8 13 co classnmaDetr
15 vk setvark
16 vl setvarl
17 15 cv setvark
18 12 cv setvarj
19 17 18 wceq wffk=j
20 16 cv setvarl
21 11 cv setvari
22 20 21 wceq wffl=i
23 cur class1r
24 8 23 cfv class1r
25 c0g class0𝑔
26 8 25 cfv class0r
27 22 24 26 cif classifl=i1r0r
28 4 cv setvarm
29 17 20 28 co classkml
30 19 27 29 cif classifk=jifl=i1r0rkml
31 15 16 6 6 30 cmpo classk∈n,l∈n⟼ifk=jifl=i1r0rkml
32 31 14 cfv classnmaDetr⁡k∈n,l∈n⟼ifk=jifl=i1r0rkml
33 11 12 6 6 32 cmpo classi∈n,j∈n⟼nmaDetr⁡k∈n,l∈n⟼ifk=jifl=i1r0rkml
34 4 10 33 cmpt classm∈BasenMatr⟼i∈n,j∈n⟼nmaDetr⁡k∈n,l∈n⟼ifk=jifl=i1r0rkml
35 1 3 2 2 34 cmpo classn∈V,r∈V⟼m∈BasenMatr⟼i∈n,j∈n⟼nmaDetr⁡k∈n,l∈n⟼ifk=jifl=i1r0rkml
36 0 35 wceq wffmaAdju=n∈V,r∈V⟼m∈BasenMatr⟼i∈n,j∈n⟼nmaDetr⁡k∈n,l∈n⟼ifk=jifl=i1r0rkml