Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-madu Unicode version

Definition df-madu 27589
Description: Define the adjunct (matrix of cofactors) of a square matrix. This definition gives the standard cofactors, however the internal minors are not the standard minors. (Contributed by Stefan O'Rear, 7-Sep-2015.)
Assertion
Ref Expression
df-madu  |- maAdju  =  ( n  e.  _V , 
r  e.  _V  |->  ( m  e.  ( Base `  ( n Mat  r ) )  |->  ( i  e.  n ,  j  e.  n  |->  ( if ( i  =  j ,  ( 1r `  r
) ,  ( ( inv g `  r
) `  ( 1r `  r ) ) ) ( .r `  r
) ( ( ( n  \  { i } ) maDet  r ) `
 ( k  e.  ( n  \  {
i } ) ,  l  e.  ( n 
\  { i } )  |->  ( if ( k  =  j ,  i ,  k ) m l ) ) ) ) ) ) )
Distinct variable group:    n, r, m, i, j, k, l

Detailed syntax breakdown of Definition df-madu
StepHypRef Expression
1 cmadu 27587 . 2  class maAdju
2 vn . . 3  set  n
3 vr . . 3  set  r
4 cvv 2801 . . 3  class  _V
5 vm . . . 4  set  m
62cv 1631 . . . . . 6  class  n
73cv 1631 . . . . . 6  class  r
8 cmat 27543 . . . . . 6  class Mat
96, 7, 8co 5874 . . . . 5  class  ( n Mat  r )
10 cbs 13164 . . . . 5  class  Base
119, 10cfv 5271 . . . 4  class  ( Base `  ( n Mat  r ) )
12 vi . . . . 5  set  i
13 vj . . . . 5  set  j
1412, 13weq 1633 . . . . . . 7  wff  i  =  j
15 cur 15355 . . . . . . . 8  class  1r
167, 15cfv 5271 . . . . . . 7  class  ( 1r
`  r )
17 cminusg 14379 . . . . . . . . 9  class  inv g
187, 17cfv 5271 . . . . . . . 8  class  ( inv g `  r )
1916, 18cfv 5271 . . . . . . 7  class  ( ( inv g `  r
) `  ( 1r `  r ) )
2014, 16, 19cif 3578 . . . . . 6  class  if ( i  =  j ,  ( 1r `  r
) ,  ( ( inv g `  r
) `  ( 1r `  r ) ) )
21 vk . . . . . . . 8  set  k
22 vl . . . . . . . 8  set  l
2312cv 1631 . . . . . . . . . 10  class  i
2423csn 3653 . . . . . . . . 9  class  { i }
256, 24cdif 3162 . . . . . . . 8  class  ( n 
\  { i } )
2621, 13weq 1633 . . . . . . . . . 10  wff  k  =  j
2721cv 1631 . . . . . . . . . 10  class  k
2826, 23, 27cif 3578 . . . . . . . . 9  class  if ( k  =  j ,  i ,  k )
2922cv 1631 . . . . . . . . 9  class  l
305cv 1631 . . . . . . . . 9  class  m
3128, 29, 30co 5874 . . . . . . . 8  class  ( if ( k  =  j ,  i ,  k ) m l )
3221, 22, 25, 25, 31cmpt2 5876 . . . . . . 7  class  ( k  e.  ( n  \  { i } ) ,  l  e.  ( n  \  { i } )  |->  ( if ( k  =  j ,  i ,  k ) m l ) )
33 cmdat 27586 . . . . . . . 8  class maDet
3425, 7, 33co 5874 . . . . . . 7  class  ( ( n  \  { i } ) maDet  r )
3532, 34cfv 5271 . . . . . 6  class  ( ( ( n  \  {
i } ) maDet  r
) `  ( k  e.  ( n  \  {
i } ) ,  l  e.  ( n 
\  { i } )  |->  ( if ( k  =  j ,  i ,  k ) m l ) ) )
36 cmulr 13225 . . . . . . 7  class  .r
377, 36cfv 5271 . . . . . 6  class  ( .r
`  r )
3820, 35, 37co 5874 . . . . 5  class  ( if ( i  =  j ,  ( 1r `  r ) ,  ( ( inv g `  r ) `  ( 1r `  r ) ) ) ( .r `  r ) ( ( ( n  \  {
i } ) maDet  r
) `  ( k  e.  ( n  \  {
i } ) ,  l  e.  ( n 
\  { i } )  |->  ( if ( k  =  j ,  i ,  k ) m l ) ) ) )
3912, 13, 6, 6, 38cmpt2 5876 . . . 4  class  ( i  e.  n ,  j  e.  n  |->  ( if ( i  =  j ,  ( 1r `  r ) ,  ( ( inv g `  r ) `  ( 1r `  r ) ) ) ( .r `  r ) ( ( ( n  \  {
i } ) maDet  r
) `  ( k  e.  ( n  \  {
i } ) ,  l  e.  ( n 
\  { i } )  |->  ( if ( k  =  j ,  i ,  k ) m l ) ) ) ) )
405, 11, 39cmpt 4093 . . 3  class  ( m  e.  ( Base `  (
n Mat  r ) ) 
|->  ( i  e.  n ,  j  e.  n  |->  ( if ( i  =  j ,  ( 1r `  r ) ,  ( ( inv g `  r ) `
 ( 1r `  r ) ) ) ( .r `  r
) ( ( ( n  \  { i } ) maDet  r ) `
 ( k  e.  ( n  \  {
i } ) ,  l  e.  ( n 
\  { i } )  |->  ( if ( k  =  j ,  i ,  k ) m l ) ) ) ) ) )
412, 3, 4, 4, 40cmpt2 5876 . 2  class  ( n  e.  _V ,  r  e.  _V  |->  ( m  e.  ( Base `  (
n Mat  r ) ) 
|->  ( i  e.  n ,  j  e.  n  |->  ( if ( i  =  j ,  ( 1r `  r ) ,  ( ( inv g `  r ) `
 ( 1r `  r ) ) ) ( .r `  r
) ( ( ( n  \  { i } ) maDet  r ) `
 ( k  e.  ( n  \  {
i } ) ,  l  e.  ( n 
\  { i } )  |->  ( if ( k  =  j ,  i ,  k ) m l ) ) ) ) ) ) )
421, 41wceq 1632 1  wff maAdju  =  ( n  e.  _V , 
r  e.  _V  |->  ( m  e.  ( Base `  ( n Mat  r ) )  |->  ( i  e.  n ,  j  e.  n  |->  ( if ( i  =  j ,  ( 1r `  r
) ,  ( ( inv g `  r
) `  ( 1r `  r ) ) ) ( .r `  r
) ( ( ( n  \  { i } ) maDet  r ) `
 ( k  e.  ( n  \  {
i } ) ,  l  e.  ( n 
\  { i } )  |->  ( if ( k  =  j ,  i ,  k ) m l ) ) ) ) ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator