MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-subma Structured version   Visualization version   GIF version

Definition df-subma 22079
Description: Define the submatrices of a square matrix. A submatrix is obtained by deleting a row and a column of the original matrix. Since the indices of a matrix need not to be sequential integers, it does not matter that there may be gaps in the numbering of the indices for the submatrix. The determinants of such submatrices are called the "minors" of the original matrix. (Contributed by AV, 27-Dec-2018.)
Assertion
Ref Expression
df-subma subMat = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘𝑛, 𝑙𝑛 ↦ (𝑖 ∈ (𝑛 ∖ {𝑘}), 𝑗 ∈ (𝑛 ∖ {𝑙}) ↦ (𝑖𝑚𝑗)))))
Distinct variable group:   𝑛,𝑟,𝑚,𝑖,𝑗,𝑘,𝑙

Detailed syntax breakdown of Definition df-subma
StepHypRef Expression
1 csubma 22078 . 2 class subMat
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cvv 3475 . . 3 class V
5 vm . . . 4 setvar 𝑚
62cv 1541 . . . . . 6 class 𝑛
73cv 1541 . . . . . 6 class 𝑟
8 cmat 21907 . . . . . 6 class Mat
96, 7, 8co 7409 . . . . 5 class (𝑛 Mat 𝑟)
10 cbs 17144 . . . . 5 class Base
119, 10cfv 6544 . . . 4 class (Base‘(𝑛 Mat 𝑟))
12 vk . . . . 5 setvar 𝑘
13 vl . . . . 5 setvar 𝑙
14 vi . . . . . 6 setvar 𝑖
15 vj . . . . . 6 setvar 𝑗
1612cv 1541 . . . . . . . 8 class 𝑘
1716csn 4629 . . . . . . 7 class {𝑘}
186, 17cdif 3946 . . . . . 6 class (𝑛 ∖ {𝑘})
1913cv 1541 . . . . . . . 8 class 𝑙
2019csn 4629 . . . . . . 7 class {𝑙}
216, 20cdif 3946 . . . . . 6 class (𝑛 ∖ {𝑙})
2214cv 1541 . . . . . . 7 class 𝑖
2315cv 1541 . . . . . . 7 class 𝑗
245cv 1541 . . . . . . 7 class 𝑚
2522, 23, 24co 7409 . . . . . 6 class (𝑖𝑚𝑗)
2614, 15, 18, 21, 25cmpo 7411 . . . . 5 class (𝑖 ∈ (𝑛 ∖ {𝑘}), 𝑗 ∈ (𝑛 ∖ {𝑙}) ↦ (𝑖𝑚𝑗))
2712, 13, 6, 6, 26cmpo 7411 . . . 4 class (𝑘𝑛, 𝑙𝑛 ↦ (𝑖 ∈ (𝑛 ∖ {𝑘}), 𝑗 ∈ (𝑛 ∖ {𝑙}) ↦ (𝑖𝑚𝑗)))
285, 11, 27cmpt 5232 . . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘𝑛, 𝑙𝑛 ↦ (𝑖 ∈ (𝑛 ∖ {𝑘}), 𝑗 ∈ (𝑛 ∖ {𝑙}) ↦ (𝑖𝑚𝑗))))
292, 3, 4, 4, 28cmpo 7411 . 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘𝑛, 𝑙𝑛 ↦ (𝑖 ∈ (𝑛 ∖ {𝑘}), 𝑗 ∈ (𝑛 ∖ {𝑙}) ↦ (𝑖𝑚𝑗)))))
301, 29wceq 1542 1 wff subMat = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘𝑛, 𝑙𝑛 ↦ (𝑖 ∈ (𝑛 ∖ {𝑘}), 𝑗 ∈ (𝑛 ∖ {𝑙}) ↦ (𝑖𝑚𝑗)))))
Colors of variables: wff setvar class
This definition is referenced by:  submafval  22081
  Copyright terms: Public domain W3C validator