Definition df-minmar1 20441

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

Step	Hyp	Ref	Expression
1		cminmar1 20439	. 2 class minMatR1
2		vn	. . 3 setvar n
3		vr	. . 3 setvar r
4		cvv 3200	. . 3 class _V
5		vm	. . . 4 setvar m
6	2	cv 1482	. . . . . 6 class n
7	3	cv 1482	. . . . . 6 class r
8		cmat 20213	. . . . . 6 class Mat
9	6, 7, 8	co 6650	. . . . 5 class ( n Mat r )
10		cbs 15857	. . . . 5 class Base
11	9, 10	cfv 5888	. . . 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
16	14, 12	weq 1874	. . . . . . 7 wff i = k
17	15, 13	weq 1874	. . . . . . . 8 wff j = l
18		cur 18501	. . . . . . . . 9 class 1r
19	7, 18	cfv 5888	. . . . . . . 8 class ( 1r ` r )
20		c0g 16100	. . . . . . . . 9 class 0g
21	7, 20	cfv 5888	. . . . . . . 8 class ( 0g ` r )
22	17, 19, 21	cif 4086	. . . . . . 7 class if ( j = l , ( 1r ` r ) , ( 0g ` r ) )
23	14	cv 1482	. . . . . . . 8 class i
24	15	cv 1482	. . . . . . . 8 class j
25	5	cv 1482	. . . . . . . 8 class m
26	23, 24, 25	co 6650	. . . . . . 7 class ( i m j )
27	16, 22, 26	cif 4086	. . . . . 6 class if ( i = k , if ( j = l , ( 1r ` r ) , ( 0g ` r ) ) , ( i m j ) )
28	14, 15, 6, 6, 27	cmpt2 6652	. . . . 5 class ( i e. n , j e. n |-> if ( i = k , if ( j = l , ( 1r ` r ) , ( 0g ` r ) ) , ( i m j ) ) )
29	12, 13, 6, 6, 28	cmpt2 6652	. . . 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 ) ) ) )
30	5, 11, 29	cmpt 4729	. . 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 ) ) ) ) )
31	2, 3, 4, 4, 30	cmpt2 6652	. 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 ) ) ) ) ) )
32	1, 31	wceq 1483	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 ) ) ) ) ) )

This definition is referenced by:  minmar1fval  20452