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

Definition df-subma 20600
 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 20599 . 2 class subMat
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cvv 3349 . . 3 class V
5 vm . . . 4 setvar 𝑚
62cv 1629 . . . . . 6 class 𝑛
73cv 1629 . . . . . 6 class 𝑟
8 cmat 20429 . . . . . 6 class Mat
96, 7, 8co 6792 . . . . 5 class (𝑛 Mat 𝑟)
10 cbs 16063 . . . . 5 class Base
119, 10cfv 6031 . . . 4 class (Base‘(𝑛 Mat 𝑟))
12 vk . . . . 5 setvar 𝑘
13 vl . . . . 5 setvar 𝑙
14 vi . . . . . 6 setvar 𝑖
15 vj . . . . . 6 setvar 𝑗
1612cv 1629 . . . . . . . 8 class 𝑘
1716csn 4314 . . . . . . 7 class {𝑘}
186, 17cdif 3718 . . . . . 6 class (𝑛 ∖ {𝑘})
1913cv 1629 . . . . . . . 8 class 𝑙
2019csn 4314 . . . . . . 7 class {𝑙}
216, 20cdif 3718 . . . . . 6 class (𝑛 ∖ {𝑙})
2214cv 1629 . . . . . . 7 class 𝑖
2315cv 1629 . . . . . . 7 class 𝑗
245cv 1629 . . . . . . 7 class 𝑚
2522, 23, 24co 6792 . . . . . 6 class (𝑖𝑚𝑗)
2614, 15, 18, 21, 25cmpt2 6794 . . . . 5 class (𝑖 ∈ (𝑛 ∖ {𝑘}), 𝑗 ∈ (𝑛 ∖ {𝑙}) ↦ (𝑖𝑚𝑗))
2712, 13, 6, 6, 26cmpt2 6794 . . . 4 class (𝑘𝑛, 𝑙𝑛 ↦ (𝑖 ∈ (𝑛 ∖ {𝑘}), 𝑗 ∈ (𝑛 ∖ {𝑙}) ↦ (𝑖𝑚𝑗)))
285, 11, 27cmpt 4861 . . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘𝑛, 𝑙𝑛 ↦ (𝑖 ∈ (𝑛 ∖ {𝑘}), 𝑗 ∈ (𝑛 ∖ {𝑙}) ↦ (𝑖𝑚𝑗))))
292, 3, 4, 4, 28cmpt2 6794 . 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘𝑛, 𝑙𝑛 ↦ (𝑖 ∈ (𝑛 ∖ {𝑘}), 𝑗 ∈ (𝑛 ∖ {𝑙}) ↦ (𝑖𝑚𝑗)))))
301, 29wceq 1630 1 wff subMat = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘𝑛, 𝑙𝑛 ↦ (𝑖 ∈ (𝑛 ∖ {𝑘}), 𝑗 ∈ (𝑛 ∖ {𝑙}) ↦ (𝑖𝑚𝑗)))))
 Colors of variables: wff setvar class This definition is referenced by:  submafval  20602
 Copyright terms: Public domain W3C validator