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

Definition df-minmar1 18904
Description: Define the matrices whose determinants are the minors of a square matrix. In contrast to the standard definition of minors, a row is replaced by 0's and one 1 instead of deleting the column and row (e.g. definition in [Lang] p. 515). By this, the determinant of such a matrix is equal to the minor determined in the standard way (as determinant of a submatrix, see df-subma 18846- note that the matrix is transposed compared with the submatrix defined in df-subma 18846, but this does not matter because the determinants are the same, see mdettpos 18880). Such matrices are used in the definition of an adjunct of a square matrix, see df-madu 18903. (Contributed by AV, 27-Dec-2018.)
Assertion
Ref Expression
df-minmar1  |- minMatR1  =  ( n  e.  _V , 
r  e.  _V  |->  ( m  e.  ( Base `  ( n Mat  r ) )  |->  ( k  e.  n ,  l  e.  n  |->  ( i  e.  n ,  j  e.  n  |->  if ( i  =  k ,  if ( j  =  l ,  ( 1r `  r ) ,  ( 0g `  r ) ) ,  ( i m j ) ) ) ) ) )
Distinct variable group:    n, r, m, i, j, k, l

Detailed syntax breakdown of Definition df-minmar1
StepHypRef Expression
1 cminmar1 18902 . 2  class minMatR1
2 vn . . 3  setvar  n
3 vr . . 3  setvar  r
4 cvv 3113 . . 3  class  _V
5 vm . . . 4  setvar  m
62cv 1378 . . . . . 6  class  n
73cv 1378 . . . . . 6  class  r
8 cmat 18676 . . . . . 6  class Mat
96, 7, 8co 6282 . . . . 5  class  ( n Mat  r )
10 cbs 14486 . . . . 5  class  Base
119, 10cfv 5586 . . . 4  class  ( Base `  ( n Mat  r ) )
12 vk . . . . 5  setvar  k
13 vl . . . . 5  setvar  l
14 vi . . . . . 6  setvar  i
15 vj . . . . . 6  setvar  j
1614, 12weq 1705 . . . . . . 7  wff  i  =  k
1715, 13weq 1705 . . . . . . . 8  wff  j  =  l
18 cur 16943 . . . . . . . . 9  class  1r
197, 18cfv 5586 . . . . . . . 8  class  ( 1r
`  r )
20 c0g 14691 . . . . . . . . 9  class  0g
217, 20cfv 5586 . . . . . . . 8  class  ( 0g
`  r )
2217, 19, 21cif 3939 . . . . . . 7  class  if ( j  =  l ,  ( 1r `  r
) ,  ( 0g
`  r ) )
2314cv 1378 . . . . . . . 8  class  i
2415cv 1378 . . . . . . . 8  class  j
255cv 1378 . . . . . . . 8  class  m
2623, 24, 25co 6282 . . . . . . 7  class  ( i m j )
2716, 22, 26cif 3939 . . . . . 6  class  if ( i  =  k ,  if ( j  =  l ,  ( 1r
`  r ) ,  ( 0g `  r
) ) ,  ( i m j ) )
2814, 15, 6, 6, 27cmpt2 6284 . . . . 5  class  ( i  e.  n ,  j  e.  n  |->  if ( i  =  k ,  if ( j  =  l ,  ( 1r
`  r ) ,  ( 0g `  r
) ) ,  ( i m j ) ) )
2912, 13, 6, 6, 28cmpt2 6284 . . . 4  class  ( k  e.  n ,  l  e.  n  |->  ( i  e.  n ,  j  e.  n  |->  if ( i  =  k ,  if ( j  =  l ,  ( 1r
`  r ) ,  ( 0g `  r
) ) ,  ( i m j ) ) ) )
305, 11, 29cmpt 4505 . . 3  class  ( m  e.  ( Base `  (
n Mat  r ) ) 
|->  ( k  e.  n ,  l  e.  n  |->  ( i  e.  n ,  j  e.  n  |->  if ( i  =  k ,  if ( j  =  l ,  ( 1r `  r
) ,  ( 0g
`  r ) ) ,  ( i m j ) ) ) ) )
312, 3, 4, 4, 30cmpt2 6284 . 2  class  ( n  e.  _V ,  r  e.  _V  |->  ( m  e.  ( Base `  (
n Mat  r ) ) 
|->  ( k  e.  n ,  l  e.  n  |->  ( i  e.  n ,  j  e.  n  |->  if ( i  =  k ,  if ( j  =  l ,  ( 1r `  r
) ,  ( 0g
`  r ) ) ,  ( i m j ) ) ) ) ) )
321, 31wceq 1379 1  wff minMatR1  =  ( n  e.  _V , 
r  e.  _V  |->  ( m  e.  ( Base `  ( n Mat  r ) )  |->  ( k  e.  n ,  l  e.  n  |->  ( i  e.  n ,  j  e.  n  |->  if ( i  =  k ,  if ( j  =  l ,  ( 1r `  r ) ,  ( 0g `  r ) ) ,  ( i m j ) ) ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  minmar1fval  18915
  Copyright terms: Public domain W3C validator