Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-madu Structured version   Visualization version   GIF 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
df-madu maAdju = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑖𝑛, 𝑗𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘𝑛, 𝑙𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑟), (0g𝑟)), (𝑘𝑚𝑙)))))))
Distinct variable group:   𝑛,𝑟,𝑚,𝑖,𝑗,𝑘,𝑙

Detailed syntax breakdown of Definition df-madu
StepHypRef Expression
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cvv 3231 . . 3 class V
5 vm . . . 4 setvar 𝑚
62cv 1522 . . . . . 6 class 𝑛
73cv 1522 . . . . . 6 class 𝑟
8 cmat 20261 . . . . . 6 class Mat
96, 7, 8co 6690 . . . . 5 class (𝑛 Mat 𝑟)
10 cbs 15904 . . . . 5 class Base
119, 10cfv 5926 . . . 4 class (Base‘(𝑛 Mat 𝑟))
12 vi . . . . 5 setvar 𝑖
13 vj . . . . 5 setvar 𝑗
14 vk . . . . . . 7 setvar 𝑘
15 vl . . . . . . 7 setvar 𝑙
1614, 13weq 1931 . . . . . . . 8 wff 𝑘 = 𝑗
1715, 12weq 1931 . . . . . . . . 9 wff 𝑙 = 𝑖
18 cur 18547 . . . . . . . . . 10 class 1r
197, 18cfv 5926 . . . . . . . . 9 class (1r𝑟)
20 c0g 16147 . . . . . . . . . 10 class 0g
217, 20cfv 5926 . . . . . . . . 9 class (0g𝑟)
2217, 19, 21cif 4119 . . . . . . . 8 class if(𝑙 = 𝑖, (1r𝑟), (0g𝑟))
2314cv 1522 . . . . . . . . 9 class 𝑘
2415cv 1522 . . . . . . . . 9 class 𝑙
255cv 1522 . . . . . . . . 9 class 𝑚
2623, 24, 25co 6690 . . . . . . . 8 class (𝑘𝑚𝑙)
2716, 22, 26cif 4119 . . . . . . 7 class if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑟), (0g𝑟)), (𝑘𝑚𝑙))
2814, 15, 6, 6, 27cmpt2 6692 . . . . . 6 class (𝑘𝑛, 𝑙𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑟), (0g𝑟)), (𝑘𝑚𝑙)))
29 cmdat 20438 . . . . . . 7 class maDet
306, 7, 29co 6690 . . . . . 6 class (𝑛 maDet 𝑟)
3128, 30cfv 5926 . . . . 5 class ((𝑛 maDet 𝑟)‘(𝑘𝑛, 𝑙𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑟), (0g𝑟)), (𝑘𝑚𝑙))))
3212, 13, 6, 6, 31cmpt2 6692 . . . 4 class (𝑖𝑛, 𝑗𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘𝑛, 𝑙𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑟), (0g𝑟)), (𝑘𝑚𝑙)))))
335, 11, 32cmpt 4762 . . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑖𝑛, 𝑗𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘𝑛, 𝑙𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑟), (0g𝑟)), (𝑘𝑚𝑙))))))
342, 3, 4, 4, 33cmpt2 6692 . 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑖𝑛, 𝑗𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘𝑛, 𝑙𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑟), (0g𝑟)), (𝑘𝑚𝑙)))))))
351, 34wceq 1523 1 wff maAdju = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑖𝑛, 𝑗𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘𝑛, 𝑙𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑟), (0g𝑟)), (𝑘𝑚𝑙)))))))
 Colors of variables: wff setvar class This definition is referenced by:  madufval  20491
 Copyright terms: Public domain W3C validator