Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-subma | Structured version Visualization version Unicode version |
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.) |
Ref | Expression |
---|---|
df-subma | subMat Mat |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csubma 20382 | . 2 subMat | |
2 | vn | . . 3 | |
3 | vr | . . 3 | |
4 | cvv 3200 | . . 3 | |
5 | vm | . . . 4 | |
6 | 2 | cv 1482 | . . . . . 6 |
7 | 3 | cv 1482 | . . . . . 6 |
8 | cmat 20213 | . . . . . 6 Mat | |
9 | 6, 7, 8 | co 6650 | . . . . 5 Mat |
10 | cbs 15857 | . . . . 5 | |
11 | 9, 10 | cfv 5888 | . . . 4 Mat |
12 | vk | . . . . 5 | |
13 | vl | . . . . 5 | |
14 | vi | . . . . . 6 | |
15 | vj | . . . . . 6 | |
16 | 12 | cv 1482 | . . . . . . . 8 |
17 | 16 | csn 4177 | . . . . . . 7 |
18 | 6, 17 | cdif 3571 | . . . . . 6 |
19 | 13 | cv 1482 | . . . . . . . 8 |
20 | 19 | csn 4177 | . . . . . . 7 |
21 | 6, 20 | cdif 3571 | . . . . . 6 |
22 | 14 | cv 1482 | . . . . . . 7 |
23 | 15 | cv 1482 | . . . . . . 7 |
24 | 5 | cv 1482 | . . . . . . 7 |
25 | 22, 23, 24 | co 6650 | . . . . . 6 |
26 | 14, 15, 18, 21, 25 | cmpt2 6652 | . . . . 5 |
27 | 12, 13, 6, 6, 26 | cmpt2 6652 | . . . 4 |
28 | 5, 11, 27 | cmpt 4729 | . . 3 Mat |
29 | 2, 3, 4, 4, 28 | cmpt2 6652 | . 2 Mat |
30 | 1, 29 | wceq 1483 | 1 subMat Mat |
Colors of variables: wff setvar class |
This definition is referenced by: submafval 20385 |
Copyright terms: Public domain | W3C validator |