# 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
`|- maAdju = ( n e. _V , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( i e. n , j e. n |-> ( ( n maDet r ) ` ( k e. n , l e. n |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) ) ) ) )`

### Detailed syntax breakdown

Step Hyp Ref Expression
` |-  maAdju`
1 vn
` |-  n`
2 cvv
` |-  _V`
3 vr
` |-  r`
4 vm
` |-  m`
5 cbs
` |-  Base`
6 1 cv
` |-  n`
7 cmat
` |-  Mat`
8 3 cv
` |-  r`
9 6 8 7 co
` |-  ( n Mat r )`
10 9 5 cfv
` |-  ( Base ` ( n Mat r ) )`
11 vi
` |-  i`
12 vj
` |-  j`
13 cmdat
` |-  maDet`
14 6 8 13 co
` |-  ( n maDet r )`
15 vk
` |-  k`
16 vl
` |-  l`
17 15 cv
` |-  k`
18 12 cv
` |-  j`
19 17 18 wceq
` |-  k = j`
20 16 cv
` |-  l`
21 11 cv
` |-  i`
22 20 21 wceq
` |-  l = i`
23 cur
` |-  1r`
24 8 23 cfv
` |-  ( 1r ` r )`
25 c0g
` |-  0g`
26 8 25 cfv
` |-  ( 0g ` r )`
27 22 24 26 cif
` |-  if ( l = i , ( 1r ` r ) , ( 0g ` r ) )`
28 4 cv
` |-  m`
29 17 20 28 co
` |-  ( k m l )`
30 19 27 29 cif
` |-  if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) )`
31 15 16 6 6 30 cmpo
` |-  ( k e. n , l e. n |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) )`
32 31 14 cfv
` |-  ( ( n maDet r ) ` ( k e. n , l e. n |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) )`
33 11 12 6 6 32 cmpo
` |-  ( i e. n , j e. n |-> ( ( n maDet r ) ` ( k e. n , l e. n |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) ) )`
34 4 10 33 cmpt
` |-  ( m e. ( Base ` ( n Mat r ) ) |-> ( i e. n , j e. n |-> ( ( n maDet r ) ` ( k e. n , l e. n |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) ) ) )`
35 1 3 2 2 34 cmpo
` |-  ( n e. _V , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( i e. n , j e. n |-> ( ( n maDet r ) ` ( k e. n , l e. n |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) ) ) ) )`
36 0 35 wceq
` |-  maAdju = ( n e. _V , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( i e. n , j e. n |-> ( ( n maDet r ) ` ( k e. n , l e. n |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) ) ) ) )`