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

Definition df-minmar1 19427
 Description: Define the matrices whose determinants are the minors of a square matrix. In contrast to the standard definition of minors, a row is replaced by 0's and one 1 instead of deleting the column and row (e.g. definition in [Lang] p. 515). By this, the determinant of such a matrix is equal to the minor determined in the standard way (as determinant of a submatrix, see df-subma 19369- note that the matrix is transposed compared with the submatrix defined in df-subma 19369, but this does not matter because the determinants are the same, see mdettpos 19403). Such matrices are used in the definition of an adjunct of a square matrix, see df-madu 19426. (Contributed by AV, 27-Dec-2018.)
Assertion
Ref Expression
df-minmar1 minMatR1 Mat
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-minmar1
StepHypRef Expression
1 cminmar1 19425 . 2 minMatR1
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
1614, 12weq 1757 . . . . . . 7
1715, 13weq 1757 . . . . . . . 8
18 cur 17471 . . . . . . . . 9
197, 18cfv 5568 . . . . . . . 8
20 c0g 15052 . . . . . . . . 9
217, 20cfv 5568 . . . . . . . 8
2217, 19, 21cif 3884 . . . . . . 7
2314cv 1404 . . . . . . . 8
2415cv 1404 . . . . . . . 8
255cv 1404 . . . . . . . 8
2623, 24, 25co 6277 . . . . . . 7
2716, 22, 26cif 3884 . . . . . 6
2814, 15, 6, 6, 27cmpt2 6279 . . . . 5
2912, 13, 6, 6, 28cmpt2 6279 . . . 4
305, 11, 29cmpt 4452 . . 3 Mat
312, 3, 4, 4, 30cmpt2 6279 . 2 Mat
321, 31wceq 1405 1 minMatR1 Mat
 Colors of variables: wff setvar class This definition is referenced by:  minmar1fval  19438
 Copyright terms: Public domain W3C validator