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 ⊢ subMat 1 = m ∈ V ⟼ k ∈ ℕ , l ∈ ℕ ⟼ m ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < k i i + 1 if j < l j j + 1

Detailed syntax breakdown

Step Hyp Ref Expression
0 csmat class subMat 1
1 vm setvar m
2 cvv class 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 i + 1
16 12 9 15 cif class if i < k i i + 1
17 8 cv setvar j
18 5 cv setvar l
19 17 18 10 wbr wff j < l
20 17 14 13 co class j + 1
21 19 17 20 cif class if j < l j j + 1
22 16 21 cop class if i < k i i + 1 if j < l j j + 1
23 7 8 4 4 22 cmpo class i ∈ ℕ , j ∈ ℕ ⟼ if i < k i i + 1 if j < l j j + 1
24 6 23 ccom class m ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < k i i + 1 if j < l j j + 1
25 3 5 4 4 24 cmpo class k ∈ ℕ , l ∈ ℕ ⟼ m ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < k i i + 1 if j < l j j + 1
26 1 2 25 cmpt class m ∈ V ⟼ k ∈ ℕ , l ∈ ℕ ⟼ m ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < k i i + 1 if j < l j j + 1
27 0 26 wceq wff subMat 1 = m ∈ V ⟼ k ∈ ℕ , l ∈ ℕ ⟼ m ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < k i i + 1 if j < l j j + 1