Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-smat Structured version   Visualization version   GIF version

Definition df-smat 29684
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 20323. (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
StepHypRef Expression
1 csmat 29683 . 2 class subMat1
2 vm . . 3 setvar 𝑚
3 cvv 3190 . . 3 class V
4 vk . . . 4 setvar 𝑘
5 vl . . . 4 setvar 𝑙
6 cn 10980 . . . 4 class
72cv 1479 . . . . 5 class 𝑚
8 vi . . . . . 6 setvar 𝑖
9 vj . . . . . 6 setvar 𝑗
108cv 1479 . . . . . . . . 9 class 𝑖
114cv 1479 . . . . . . . . 9 class 𝑘
12 clt 10034 . . . . . . . . 9 class <
1310, 11, 12wbr 4623 . . . . . . . 8 wff 𝑖 < 𝑘
14 c1 9897 . . . . . . . . 9 class 1
15 caddc 9899 . . . . . . . . 9 class +
1610, 14, 15co 6615 . . . . . . . 8 class (𝑖 + 1)
1713, 10, 16cif 4064 . . . . . . 7 class if(𝑖 < 𝑘, 𝑖, (𝑖 + 1))
189cv 1479 . . . . . . . . 9 class 𝑗
195cv 1479 . . . . . . . . 9 class 𝑙
2018, 19, 12wbr 4623 . . . . . . . 8 wff 𝑗 < 𝑙
2118, 14, 15co 6615 . . . . . . . 8 class (𝑗 + 1)
2220, 18, 21cif 4064 . . . . . . 7 class if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))
2317, 22cop 4161 . . . . . 6 class ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩
248, 9, 6, 6, 23cmpt2 6617 . . . . 5 class (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩)
257, 24ccom 5088 . . . 4 class (𝑚 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩))
264, 5, 6, 6, 25cmpt2 6617 . . 3 class (𝑘 ∈ ℕ, 𝑙 ∈ ℕ ↦ (𝑚 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩)))
272, 3, 26cmpt 4683 . 2 class (𝑚 ∈ V ↦ (𝑘 ∈ ℕ, 𝑙 ∈ ℕ ↦ (𝑚 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩))))
281, 27wceq 1480 1 wff subMat1 = (𝑚 ∈ V ↦ (𝑘 ∈ ℕ, 𝑙 ∈ ℕ ↦ (𝑚 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩))))
Colors of variables: wff setvar class
This definition is referenced by:  smatfval  29685
  Copyright terms: Public domain W3C validator