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

Definition df-subma 19369
 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 Mat
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-subma
StepHypRef Expression
1 csubma 19368 . 2 subMat
2 vn . . 3
3 vr . . 3
4 cvv 3058 . . 3
5 vm . . . 4
62cv 1404 . . . . . 6
73cv 1404 . . . . . 6
8 cmat 19199 . . . . . 6 Mat
96, 7, 8co 6277 . . . . 5 Mat
10 cbs 14839 . . . . 5
119, 10cfv 5568 . . . 4 Mat
12 vk . . . . 5
13 vl . . . . 5
14 vi . . . . . 6
15 vj . . . . . 6
1612cv 1404 . . . . . . . 8
1716csn 3971 . . . . . . 7
186, 17cdif 3410 . . . . . 6
1913cv 1404 . . . . . . . 8
2019csn 3971 . . . . . . 7
216, 20cdif 3410 . . . . . 6
2214cv 1404 . . . . . . 7
2315cv 1404 . . . . . . 7
245cv 1404 . . . . . . 7
2522, 23, 24co 6277 . . . . . 6
2614, 15, 18, 21, 25cmpt2 6279 . . . . 5
2712, 13, 6, 6, 26cmpt2 6279 . . . 4
285, 11, 27cmpt 4452 . . 3 Mat
292, 3, 4, 4, 28cmpt2 6279 . 2 Mat
301, 29wceq 1405 1 subMat Mat
 Colors of variables: wff setvar class This definition is referenced by:  submafval  19371
 Copyright terms: Public domain W3C validator