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

Definition df-madu 21794
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
df-madu maAdju = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑖𝑛, 𝑗𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘𝑛, 𝑙𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑟), (0g𝑟)), (𝑘𝑚𝑙)))))))
Distinct variable group:   𝑛,𝑟,𝑚,𝑖,𝑗,𝑘,𝑙

Detailed syntax breakdown of Definition df-madu
StepHypRef Expression
1 cmadu 21792 . 2 class maAdju
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cvv 3431 . . 3 class V
5 vm . . . 4 setvar 𝑚
62cv 1541 . . . . . 6 class 𝑛
73cv 1541 . . . . . 6 class 𝑟
8 cmat 21565 . . . . . 6 class Mat
96, 7, 8co 7272 . . . . 5 class (𝑛 Mat 𝑟)
10 cbs 16923 . . . . 5 class Base
119, 10cfv 6432 . . . 4 class (Base‘(𝑛 Mat 𝑟))
12 vi . . . . 5 setvar 𝑖
13 vj . . . . 5 setvar 𝑗
14 vk . . . . . . 7 setvar 𝑘
15 vl . . . . . . 7 setvar 𝑙
1614, 13weq 1970 . . . . . . . 8 wff 𝑘 = 𝑗
1715, 12weq 1970 . . . . . . . . 9 wff 𝑙 = 𝑖
18 cur 19748 . . . . . . . . . 10 class 1r
197, 18cfv 6432 . . . . . . . . 9 class (1r𝑟)
20 c0g 17161 . . . . . . . . . 10 class 0g
217, 20cfv 6432 . . . . . . . . 9 class (0g𝑟)
2217, 19, 21cif 4465 . . . . . . . 8 class if(𝑙 = 𝑖, (1r𝑟), (0g𝑟))
2314cv 1541 . . . . . . . . 9 class 𝑘
2415cv 1541 . . . . . . . . 9 class 𝑙
255cv 1541 . . . . . . . . 9 class 𝑚
2623, 24, 25co 7272 . . . . . . . 8 class (𝑘𝑚𝑙)
2716, 22, 26cif 4465 . . . . . . 7 class if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑟), (0g𝑟)), (𝑘𝑚𝑙))
2814, 15, 6, 6, 27cmpo 7274 . . . . . 6 class (𝑘𝑛, 𝑙𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑟), (0g𝑟)), (𝑘𝑚𝑙)))
29 cmdat 21744 . . . . . . 7 class maDet
306, 7, 29co 7272 . . . . . 6 class (𝑛 maDet 𝑟)
3128, 30cfv 6432 . . . . 5 class ((𝑛 maDet 𝑟)‘(𝑘𝑛, 𝑙𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑟), (0g𝑟)), (𝑘𝑚𝑙))))
3212, 13, 6, 6, 31cmpo 7274 . . . 4 class (𝑖𝑛, 𝑗𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘𝑛, 𝑙𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑟), (0g𝑟)), (𝑘𝑚𝑙)))))
335, 11, 32cmpt 5162 . . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑖𝑛, 𝑗𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘𝑛, 𝑙𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑟), (0g𝑟)), (𝑘𝑚𝑙))))))
342, 3, 4, 4, 33cmpo 7274 . 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑖𝑛, 𝑗𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘𝑛, 𝑙𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑟), (0g𝑟)), (𝑘𝑚𝑙)))))))
351, 34wceq 1542 1 wff maAdju = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑖𝑛, 𝑗𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘𝑛, 𝑙𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑟), (0g𝑟)), (𝑘𝑚𝑙)))))))
Colors of variables: wff setvar class
This definition is referenced by:  madufval  21797
  Copyright terms: Public domain W3C validator