Definition df-smat 31764

Description: Define a function generating submatrices of an integer-indexed matrix. The function maps an index in ((1...𝑀) × (1...𝑁)) into a new index in ((1...(𝑀 − 1)) × (1...(𝑁 − 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 21746. (Contributed by Thierry Arnoux, 18-Aug-2020.)

Assertion

Ref	Expression
df-smat	⊢ subMat1 = (𝑚 ∈ V ↦ (𝑘 ∈ ℕ, 𝑙 ∈ ℕ ↦ (𝑚 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩))))

Distinct variable group:   𝑖,𝑗,𝑘,𝑙,𝑚

Detailed syntax breakdown of Definition df-smat

Step	Hyp	Ref	Expression
1		csmat 31763	. 2 class subMat1
2		vm	. . 3 setvar 𝑚
3		cvv 3436	. . 3 class V
4		vk	. . . 4 setvar 𝑘
5		vl	. . . 4 setvar 𝑙
6		cn 11993	. . . 4 class ℕ
7	2	cv 1537	. . . . 5 class 𝑚
8		vi	. . . . . 6 setvar 𝑖
9		vj	. . . . . 6 setvar 𝑗
10	8	cv 1537	. . . . . . . . 9 class 𝑖
11	4	cv 1537	. . . . . . . . 9 class 𝑘
12		clt 11029	. . . . . . . . 9 class <
13	10, 11, 12	wbr 5078	. . . . . . . 8 wff 𝑖 < 𝑘
14		c1 10892	. . . . . . . . 9 class 1
15		caddc 10894	. . . . . . . . 9 class +
16	10, 14, 15	co 7287	. . . . . . . 8 class (𝑖 + 1)
17	13, 10, 16	cif 4463	. . . . . . 7 class if(𝑖 < 𝑘, 𝑖, (𝑖 + 1))
18	9	cv 1537	. . . . . . . . 9 class 𝑗
19	5	cv 1537	. . . . . . . . 9 class 𝑙
20	18, 19, 12	wbr 5078	. . . . . . . 8 wff 𝑗 < 𝑙
21	18, 14, 15	co 7287	. . . . . . . 8 class (𝑗 + 1)
22	20, 18, 21	cif 4463	. . . . . . 7 class if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))
23	17, 22	cop 4571	. . . . . 6 class ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩
24	8, 9, 6, 6, 23	cmpo 7289	. . . . 5 class (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩)
25	7, 24	ccom 5597	. . . 4 class (𝑚 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩))
26	4, 5, 6, 6, 25	cmpo 7289	. . 3 class (𝑘 ∈ ℕ, 𝑙 ∈ ℕ ↦ (𝑚 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩)))
27	2, 3, 26	cmpt 5161	. 2 class (𝑚 ∈ V ↦ (𝑘 ∈ ℕ, 𝑙 ∈ ℕ ↦ (𝑚 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩))))
28	1, 27	wceq 1538	1 wff subMat1 = (𝑚 ∈ V ↦ (𝑘 ∈ ℕ, 𝑙 ∈ ℕ ↦ (𝑚 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩))))

This definition is referenced by:  smatfval  31765