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 ) ) ) ) ) )