Definition df-smat 29860

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 20383. (Contributed by Thierry Arnoux, 18-Aug-2020.)

Assertion

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

Distinct variable group:   i, j, k, l, m

Detailed syntax breakdown of Definition df-smat

Step	Hyp	Ref	Expression
1		csmat 29859	. 2 class subMat1
2		vm	. . 3 setvar m
3		cvv 3200	. . 3 class _V
4		vk	. . . 4 setvar k
5		vl	. . . 4 setvar l
6		cn 11020	. . . 4 class NN
7	2	cv 1482	. . . . 5 class m
8		vi	. . . . . 6 setvar i
9		vj	. . . . . 6 setvar j
10	8	cv 1482	. . . . . . . . 9 class i
11	4	cv 1482	. . . . . . . . 9 class k
12		clt 10074	. . . . . . . . 9 class <
13	10, 11, 12	wbr 4653	. . . . . . . 8 wff i < k
14		c1 9937	. . . . . . . . 9 class 1
15		caddc 9939	. . . . . . . . 9 class +
16	10, 14, 15	co 6650	. . . . . . . 8 class ( i + 1 )
17	13, 10, 16	cif 4086	. . . . . . 7 class if ( i < k , i , ( i + 1 ) )
18	9	cv 1482	. . . . . . . . 9 class j
19	5	cv 1482	. . . . . . . . 9 class l
20	18, 19, 12	wbr 4653	. . . . . . . 8 wff j < l
21	18, 14, 15	co 6650	. . . . . . . 8 class ( j + 1 )
22	20, 18, 21	cif 4086	. . . . . . 7 class if ( j < l , j , ( j + 1 ) )
23	17, 22	cop 4183	. . . . . 6 class <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >.
24	8, 9, 6, 6, 23	cmpt2 6652	. . . . 5 class ( i e. NN , j e. NN |-> <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. )
25	7, 24	ccom 5118	. . . 4 class ( m o. ( i e. NN , j e. NN |-> <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. ) )
26	4, 5, 6, 6, 25	cmpt2 6652	. . 3 class ( 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	2, 3, 26	cmpt 4729	. 2 class ( 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 ) ) >. ) ) ) )
28	1, 27	wceq 1483	1 wff 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 ) ) >. ) ) ) )

This definition is referenced by:  smatfval  29861