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 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
0 cmadu 
 |-  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 ) ) ) ) ) ) )