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

Definition df-subma 18841
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 18840 . 2  class subMat
2 vn . . 3  setvar  n
3 vr . . 3  setvar  r
4 cvv 3108 . . 3  class  _V
5 vm . . . 4  setvar  m
62cv 1373 . . . . . 6  class  n
73cv 1373 . . . . . 6  class  r
8 cmat 18671 . . . . . 6  class Mat
96, 7, 8co 6277 . . . . 5  class  ( n Mat  r )
10 cbs 14481 . . . . 5  class  Base
119, 10cfv 5581 . . . 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 1373 . . . . . . . 8  class  k
1716csn 4022 . . . . . . 7  class  { k }
186, 17cdif 3468 . . . . . 6  class  ( n 
\  { k } )
1913cv 1373 . . . . . . . 8  class  l
2019csn 4022 . . . . . . 7  class  { l }
216, 20cdif 3468 . . . . . 6  class  ( n 
\  { l } )
2214cv 1373 . . . . . . 7  class  i
2315cv 1373 . . . . . . 7  class  j
245cv 1373 . . . . . . 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 4500 . . 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 1374 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  18843
  Copyright terms: Public domain W3C validator