MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-madu Structured version   Unicode version

Definition df-madu 18575
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.)
Assertion
Ref Expression
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 ) ) ) ) ) ) )
Distinct variable group:    n, r, m, i, j, k, l

Detailed syntax breakdown of Definition df-madu
StepHypRef Expression
1 cmadu 18573 . 2  class maAdju
2 vn . . 3  setvar  n
3 vr . . 3  setvar  r
4 cvv 3078 . . 3  class  _V
5 vm . . . 4  setvar  m
62cv 1369 . . . . . 6  class  n
73cv 1369 . . . . . 6  class  r
8 cmat 18408 . . . . . 6  class Mat
96, 7, 8co 6203 . . . . 5  class  ( n Mat  r )
10 cbs 14295 . . . . 5  class  Base
119, 10cfv 5529 . . . 4  class  ( Base `  ( n Mat  r ) )
12 vi . . . . 5  setvar  i
13 vj . . . . 5  setvar  j
14 vk . . . . . . 7  setvar  k
15 vl . . . . . . 7  setvar  l
1614, 13weq 1696 . . . . . . . 8  wff  k  =  j
1715, 12weq 1696 . . . . . . . . 9  wff  l  =  i
18 cur 16728 . . . . . . . . . 10  class  1r
197, 18cfv 5529 . . . . . . . . 9  class  ( 1r
`  r )
20 c0g 14500 . . . . . . . . . 10  class  0g
217, 20cfv 5529 . . . . . . . . 9  class  ( 0g
`  r )
2217, 19, 21cif 3902 . . . . . . . 8  class  if ( l  =  i ,  ( 1r `  r
) ,  ( 0g
`  r ) )
2314cv 1369 . . . . . . . . 9  class  k
2415cv 1369 . . . . . . . . 9  class  l
255cv 1369 . . . . . . . . 9  class  m
2623, 24, 25co 6203 . . . . . . . 8  class  ( k m l )
2716, 22, 26cif 3902 . . . . . . 7  class  if ( k  =  j ,  if ( l  =  i ,  ( 1r
`  r ) ,  ( 0g `  r
) ) ,  ( k m l ) )
2814, 15, 6, 6, 27cmpt2 6205 . . . . . 6  class  ( k  e.  n ,  l  e.  n  |->  if ( k  =  j ,  if ( l  =  i ,  ( 1r
`  r ) ,  ( 0g `  r
) ) ,  ( k m l ) ) )
29 cmdat 18525 . . . . . . 7  class maDet
306, 7, 29co 6203 . . . . . 6  class  ( n maDet 
r )
3128, 30cfv 5529 . . . . 5  class  ( ( n maDet  r ) `  ( k  e.  n ,  l  e.  n  |->  if ( k  =  j ,  if ( l  =  i ,  ( 1r `  r
) ,  ( 0g
`  r ) ) ,  ( k m l ) ) ) )
3212, 13, 6, 6, 31cmpt2 6205 . . . 4  class  ( 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 ) ) ) ) )
335, 11, 32cmpt 4461 . . 3  class  ( 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 ) ) ) ) ) )
342, 3, 4, 4, 33cmpt2 6205 . 2  class  ( 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 ) ) ) ) ) ) )
351, 34wceq 1370 1  wff 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 ) ) ) ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  madufval  18578
  Copyright terms: Public domain W3C validator