# Metamath Proof Explorer

## 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 ${⊢}{\mathrm{subMat}}_{1}=\left({m}\in \mathrm{V}⟼\left({k}\in ℕ,{l}\in ℕ⟼{m}\circ \left({i}\in ℕ,{j}\in ℕ⟼⟨if\left({i}<{k},{i},{i}+1\right),if\left({j}<{l},{j},{j}+1\right)⟩\right)\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 csmat ${class}{\mathrm{subMat}}_{1}$
1 vm ${setvar}{m}$
2 cvv ${class}\mathrm{V}$
3 vk ${setvar}{k}$
4 cn ${class}ℕ$
5 vl ${setvar}{l}$
6 1 cv ${setvar}{m}$
7 vi ${setvar}{i}$
8 vj ${setvar}{j}$
9 7 cv ${setvar}{i}$
10 clt ${class}<$
11 3 cv ${setvar}{k}$
12 9 11 10 wbr ${wff}{i}<{k}$
13 caddc ${class}+$
14 c1 ${class}1$
15 9 14 13 co ${class}\left({i}+1\right)$
16 12 9 15 cif ${class}if\left({i}<{k},{i},{i}+1\right)$
17 8 cv ${setvar}{j}$
18 5 cv ${setvar}{l}$
19 17 18 10 wbr ${wff}{j}<{l}$
20 17 14 13 co ${class}\left({j}+1\right)$
21 19 17 20 cif ${class}if\left({j}<{l},{j},{j}+1\right)$
22 16 21 cop ${class}⟨if\left({i}<{k},{i},{i}+1\right),if\left({j}<{l},{j},{j}+1\right)⟩$
23 7 8 4 4 22 cmpo ${class}\left({i}\in ℕ,{j}\in ℕ⟼⟨if\left({i}<{k},{i},{i}+1\right),if\left({j}<{l},{j},{j}+1\right)⟩\right)$
24 6 23 ccom ${class}\left({m}\circ \left({i}\in ℕ,{j}\in ℕ⟼⟨if\left({i}<{k},{i},{i}+1\right),if\left({j}<{l},{j},{j}+1\right)⟩\right)\right)$
25 3 5 4 4 24 cmpo ${class}\left({k}\in ℕ,{l}\in ℕ⟼{m}\circ \left({i}\in ℕ,{j}\in ℕ⟼⟨if\left({i}<{k},{i},{i}+1\right),if\left({j}<{l},{j},{j}+1\right)⟩\right)\right)$
26 1 2 25 cmpt ${class}\left({m}\in \mathrm{V}⟼\left({k}\in ℕ,{l}\in ℕ⟼{m}\circ \left({i}\in ℕ,{j}\in ℕ⟼⟨if\left({i}<{k},{i},{i}+1\right),if\left({j}<{l},{j},{j}+1\right)⟩\right)\right)\right)$
27 0 26 wceq ${wff}{\mathrm{subMat}}_{1}=\left({m}\in \mathrm{V}⟼\left({k}\in ℕ,{l}\in ℕ⟼{m}\circ \left({i}\in ℕ,{j}\in ℕ⟼⟨if\left({i}<{k},{i},{i}+1\right),if\left({j}<{l},{j},{j}+1\right)⟩\right)\right)\right)$