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 ⊢subMat1=m∈V⟼k∈ℕ,l∈ℕ⟼m∘i∈ℕ,j∈ℕ⟼ifi<kii+1ifj<ljj+1

Detailed syntax breakdown

Step Hyp Ref Expression
0 csmat classsubMat1
1 vm setvarm
2 cvv classV
3 vk setvark
4 cn classℕ
5 vl setvarl
6 1 cv setvarm
7 vi setvari
8 vj setvarj
9 7 cv setvari
10 clt class<
11 3 cv setvark
12 9 11 10 wbr wffi<k
13 caddc class+
14 c1 class1
15 9 14 13 co classi+1
16 12 9 15 cif classifi<kii+1
17 8 cv setvarj
18 5 cv setvarl
19 17 18 10 wbr wffj<l
20 17 14 13 co classj+1
21 19 17 20 cif classifj<ljj+1
22 16 21 cop classifi<kii+1ifj<ljj+1
23 7 8 4 4 22 cmpo classi∈ℕ,j∈ℕ⟼ifi<kii+1ifj<ljj+1
24 6 23 ccom classm∘i∈ℕ,j∈ℕ⟼ifi<kii+1ifj<ljj+1
25 3 5 4 4 24 cmpo classk∈ℕ,l∈ℕ⟼m∘i∈ℕ,j∈ℕ⟼ifi<kii+1ifj<ljj+1
26 1 2 25 cmpt classm∈V⟼k∈ℕ,l∈ℕ⟼m∘i∈ℕ,j∈ℕ⟼ifi<kii+1ifj<ljj+1
27 0 26 wceq wffsubMat1=m∈V⟼k∈ℕ,l∈ℕ⟼m∘i∈ℕ,j∈ℕ⟼ifi<kii+1ifj<ljj+1