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

Definition df-subma 19369
Description: Define the submatrices of a square matrix. A submatrix is obtained by deleting a row and a column of the original matrix. Since the indices of a matrix need not to be sequential integers, it does not matter that there may be gaps in the numbering of the indices for the submatrix. The determinants of such submatrices are called the "minors" of the original matrix. (Contributed by AV, 27-Dec-2018.)
Assertion
Ref Expression
df-subma  |- subMat  =  ( n  e.  _V , 
r  e.  _V  |->  ( m  e.  ( Base `  ( n Mat  r ) )  |->  ( k  e.  n ,  l  e.  n  |->  ( i  e.  ( n  \  {
k } ) ,  j  e.  ( n 
\  { l } )  |->  ( i m j ) ) ) ) )
Distinct variable group:    n, r, m, i, j, k, l

Detailed syntax breakdown of Definition df-subma
StepHypRef Expression
1 csubma 19368 . 2  class subMat
2 vn . . 3  setvar  n
3 vr . . 3  setvar  r
4 cvv 3058 . . 3  class  _V
5 vm . . . 4  setvar  m
62cv 1404 . . . . . 6  class  n
73cv 1404 . . . . . 6  class  r
8 cmat 19199 . . . . . 6  class Mat
96, 7, 8co 6277 . . . . 5  class  ( n Mat  r )
10 cbs 14839 . . . . 5  class  Base
119, 10cfv 5568 . . . 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
1612cv 1404 . . . . . . . 8  class  k
1716csn 3971 . . . . . . 7  class  { k }
186, 17cdif 3410 . . . . . 6  class  ( n 
\  { k } )
1913cv 1404 . . . . . . . 8  class  l
2019csn 3971 . . . . . . 7  class  { l }
216, 20cdif 3410 . . . . . 6  class  ( n 
\  { l } )
2214cv 1404 . . . . . . 7  class  i
2315cv 1404 . . . . . . 7  class  j
245cv 1404 . . . . . . 7  class  m
2522, 23, 24co 6277 . . . . . 6  class  ( i m j )
2614, 15, 18, 21, 25cmpt2 6279 . . . . 5  class  ( i  e.  ( n  \  { k } ) ,  j  e.  ( n  \  { l } )  |->  ( i m j ) )
2712, 13, 6, 6, 26cmpt2 6279 . . . 4  class  ( k  e.  n ,  l  e.  n  |->  ( i  e.  ( n  \  { k } ) ,  j  e.  ( n  \  { l } )  |->  ( i m j ) ) )
285, 11, 27cmpt 4452 . . 3  class  ( m  e.  ( Base `  (
n Mat  r ) ) 
|->  ( k  e.  n ,  l  e.  n  |->  ( i  e.  ( n  \  { k } ) ,  j  e.  ( n  \  { l } ) 
|->  ( i m j ) ) ) )
292, 3, 4, 4, 28cmpt2 6279 . 2  class  ( n  e.  _V ,  r  e.  _V  |->  ( m  e.  ( Base `  (
n Mat  r ) ) 
|->  ( k  e.  n ,  l  e.  n  |->  ( i  e.  ( n  \  { k } ) ,  j  e.  ( n  \  { l } ) 
|->  ( i m j ) ) ) ) )
301, 29wceq 1405 1  wff subMat  =  ( n  e.  _V , 
r  e.  _V  |->  ( m  e.  ( Base `  ( n Mat  r ) )  |->  ( k  e.  n ,  l  e.  n  |->  ( i  e.  ( n  \  {
k } ) ,  j  e.  ( n 
\  { l } )  |->  ( i m j ) ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  submafval  19371
  Copyright terms: Public domain W3C validator