Definition df-smat

Description: Define a function generating submatrices of an integer-indexed matrix. The function maps an index in ( ( 1 ... M ) X. ( 1 ... N ) ) into a new index in ( ( 1 ... ( M - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) . A submatrix is obtained by deleting a row and a column of the original matrix. Because this function re-indexes the matrix, the resulting submatrix still has the same index set for rows and columns, and its determinent is defined, unlike the current df-subma . (Contributed by Thierry Arnoux, 18-Aug-2020)

	Ref	Expression
Assertion	df-smat	|- subMat1 = ( m e. _V |-> ( k e. NN , l e. NN |-> ( m o. ( i e. NN , j e. NN |-> <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csmat	|- subMat1
1		vm	|- m
2		cvv	|- _V
3		vk	|- k
4		cn	|- NN
5		vl	|- l
6	1	cv	|- m
7		vi	|- i
8		vj	|- j
9	7	cv	|- i
10		clt	|- <
11	3	cv	|- k
12	9 11 10	wbr	|- i < k
13		caddc	|- +
14		c1	|- 1
15	9 14 13	co	|- ( i + 1 )
16	12 9 15	cif	|- if ( i < k , i , ( i + 1 ) )
17	8	cv	|- j
18	5	cv	|- l
19	17 18 10	wbr	|- j < l
20	17 14 13	co	|- ( j + 1 )
21	19 17 20	cif	|- if ( j < l , j , ( j + 1 ) )
22	16 21	cop	|- <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >.
23	7 8 4 4 22	cmpo	|- ( i e. NN , j e. NN |-> <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. )
24	6 23	ccom	|- ( m o. ( i e. NN , j e. NN |-> <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. ) )
25	3 5 4 4 24	cmpo	|- ( k e. NN , l e. NN |-> ( m o. ( i e. NN , j e. NN |-> <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. ) ) )
26	1 2 25	cmpt	|- ( m e. _V |-> ( k e. NN , l e. NN |-> ( m o. ( i e. NN , j e. NN |-> <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. ) ) ) )
27	0 26	wceq	|- subMat1 = ( m e. _V |-> ( k e. NN , l e. NN |-> ( m o. ( i e. NN , j e. NN |-> <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. ) ) ) )