This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-minmar1

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 - note that the matrix is transposed compared with the submatrix defined in df-subma , but this does not matter because the determinants are the same, see mdettpos ). Such matrices are used in the definition of an adjunct of a square matrix, see df-madu . (Contributed by AV, 27-Dec-2018)

Ref Expression
Assertion 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 ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cminmar1 
 |-  minMatR1
1 vn 
 |-  n
2 cvv 
 |-  _V
3 vr 
 |-  r
4 vm 
 |-  m
5 cbs 
 |-  Base
6 1 cv 
 |-  n
7 cmat 
 |-  Mat
8 3 cv 
 |-  r
9 6 8 7 co 
 |-  ( n Mat r )
10 9 5 cfv 
 |-  ( Base ` ( n Mat r ) )
11 vk 
 |-  k
12 vl 
 |-  l
13 vi 
 |-  i
14 vj 
 |-  j
15 13 cv 
 |-  i
16 11 cv 
 |-  k
17 15 16 wceq 
 |-  i = k
18 14 cv 
 |-  j
19 12 cv 
 |-  l
20 18 19 wceq 
 |-  j = l
21 cur 
 |-  1r
22 8 21 cfv 
 |-  ( 1r ` r )
23 c0g 
 |-  0g
24 8 23 cfv 
 |-  ( 0g ` r )
25 20 22 24 cif 
 |-  if ( j = l , ( 1r ` r ) , ( 0g ` r ) )
26 4 cv 
 |-  m
27 15 18 26 co 
 |-  ( i m j )
28 17 25 27 cif 
 |-  if ( i = k , if ( j = l , ( 1r ` r ) , ( 0g ` r ) ) , ( i m j ) )
29 13 14 6 6 28 cmpo 
 |-  ( i e. n , j e. n |-> if ( i = k , if ( j = l , ( 1r ` r ) , ( 0g ` r ) ) , ( i m j ) ) )
30 11 12 6 6 29 cmpo 
 |-  ( 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 ) ) ) )
31 4 10 30 cmpt 
 |-  ( 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 ) ) ) ) )
32 1 3 2 2 31 cmpo 
 |-  ( 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 ) ) ) ) ) )
33 0 32 wceq 
 |-  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 ) ) ) ) ) )