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 30958
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 21114. (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 30957 . 2 class subMat1
2 vm . . 3 setvar 𝑚
3 cvv 3492 . . 3 class V
4 vk . . . 4 setvar 𝑘
5 vl . . . 4 setvar 𝑙
6 cn 11626 . . . 4 class
72cv 1527 . . . . 5 class 𝑚
8 vi . . . . . 6 setvar 𝑖
9 vj . . . . . 6 setvar 𝑗
108cv 1527 . . . . . . . . 9 class 𝑖
114cv 1527 . . . . . . . . 9 class 𝑘
12 clt 10663 . . . . . . . . 9 class <
1310, 11, 12wbr 5057 . . . . . . . 8 wff 𝑖 < 𝑘
14 c1 10526 . . . . . . . . 9 class 1
15 caddc 10528 . . . . . . . . 9 class +
1610, 14, 15co 7145 . . . . . . . 8 class (𝑖 + 1)
1713, 10, 16cif 4463 . . . . . . 7 class if(𝑖 < 𝑘, 𝑖, (𝑖 + 1))
189cv 1527 . . . . . . . . 9 class 𝑗
195cv 1527 . . . . . . . . 9 class 𝑙
2018, 19, 12wbr 5057 . . . . . . . 8 wff 𝑗 < 𝑙
2118, 14, 15co 7145 . . . . . . . 8 class (𝑗 + 1)
2220, 18, 21cif 4463 . . . . . . 7 class if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))
2317, 22cop 4563 . . . . . 6 class ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩
248, 9, 6, 6, 23cmpo 7147 . . . . 5 class (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩)
257, 24ccom 5552 . . . 4 class (𝑚 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩))
264, 5, 6, 6, 25cmpo 7147 . . 3 class (𝑘 ∈ ℕ, 𝑙 ∈ ℕ ↦ (𝑚 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩)))
272, 3, 26cmpt 5137 . 2 class (𝑚 ∈ V ↦ (𝑘 ∈ ℕ, 𝑙 ∈ ℕ ↦ (𝑚 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩))))
281, 27wceq 1528 1 wff subMat1 = (𝑚 ∈ V ↦ (𝑘 ∈ ℕ, 𝑙 ∈ ℕ ↦ (𝑚 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩))))
Colors of variables: wff setvar class
This definition is referenced by:  smatfval  30959
  Copyright terms: Public domain W3C validator