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

 Description: Define the adjugate or adjunct (matrix of cofactors) of a square matrix. This definition gives the standard cofactors, however the internal minors are not the standard minors, see definition in [Lang] p. 518. (Contributed by Stefan O'Rear, 7-Sep-2015.) (Revised by SO, 10-Jul-2018.)
Assertion
Ref Expression
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-madu
StepHypRef Expression
2 vn . . 3
3 vr . . 3
4 cvv 3078 . . 3
5 vm . . . 4
62cv 1369 . . . . . 6
73cv 1369 . . . . . 6
8 cmat 18408 . . . . . 6 Mat
96, 7, 8co 6203 . . . . 5 Mat
10 cbs 14295 . . . . 5
119, 10cfv 5529 . . . 4 Mat
12 vi . . . . 5
13 vj . . . . 5
14 vk . . . . . . 7
15 vl . . . . . . 7
1614, 13weq 1696 . . . . . . . 8
1715, 12weq 1696 . . . . . . . . 9
18 cur 16728 . . . . . . . . . 10
197, 18cfv 5529 . . . . . . . . 9
20 c0g 14500 . . . . . . . . . 10
217, 20cfv 5529 . . . . . . . . 9
2217, 19, 21cif 3902 . . . . . . . 8
2314cv 1369 . . . . . . . . 9
2415cv 1369 . . . . . . . . 9
255cv 1369 . . . . . . . . 9
2623, 24, 25co 6203 . . . . . . . 8
2716, 22, 26cif 3902 . . . . . . 7
2814, 15, 6, 6, 27cmpt2 6205 . . . . . 6
29 cmdat 18525 . . . . . . 7 maDet
306, 7, 29co 6203 . . . . . 6 maDet
3128, 30cfv 5529 . . . . 5 maDet
3212, 13, 6, 6, 31cmpt2 6205 . . . 4 maDet
335, 11, 32cmpt 4461 . . 3 Mat maDet
342, 3, 4, 4, 33cmpt2 6205 . 2 Mat maDet