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 21173
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 21171 . 2 class maAdju
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cvv 3495 . . 3 class V
5 vm . . . 4 setvar 𝑚
62cv 1527 . . . . . 6 class 𝑛
73cv 1527 . . . . . 6 class 𝑟
8 cmat 20946 . . . . . 6 class Mat
96, 7, 8co 7145 . . . . 5 class (𝑛 Mat 𝑟)
10 cbs 16473 . . . . 5 class Base
119, 10cfv 6349 . . . 4 class (Base‘(𝑛 Mat 𝑟))
12 vi . . . . 5 setvar 𝑖
13 vj . . . . 5 setvar 𝑗
14 vk . . . . . . 7 setvar 𝑘
15 vl . . . . . . 7 setvar 𝑙
1614, 13weq 1955 . . . . . . . 8 wff 𝑘 = 𝑗
1715, 12weq 1955 . . . . . . . . 9 wff 𝑙 = 𝑖
18 cur 19182 . . . . . . . . . 10 class 1r
197, 18cfv 6349 . . . . . . . . 9 class (1r𝑟)
20 c0g 16703 . . . . . . . . . 10 class 0g
217, 20cfv 6349 . . . . . . . . 9 class (0g𝑟)
2217, 19, 21cif 4465 . . . . . . . 8 class if(𝑙 = 𝑖, (1r𝑟), (0g𝑟))
2314cv 1527 . . . . . . . . 9 class 𝑘
2415cv 1527 . . . . . . . . 9 class 𝑙
255cv 1527 . . . . . . . . 9 class 𝑚
2623, 24, 25co 7145 . . . . . . . 8 class (𝑘𝑚𝑙)
2716, 22, 26cif 4465 . . . . . . 7 class if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑟), (0g𝑟)), (𝑘𝑚𝑙))
2814, 15, 6, 6, 27cmpo 7147 . . . . . 6 class (𝑘𝑛, 𝑙𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑟), (0g𝑟)), (𝑘𝑚𝑙)))
29 cmdat 21123 . . . . . . 7 class maDet
306, 7, 29co 7145 . . . . . 6 class (𝑛 maDet 𝑟)
3128, 30cfv 6349 . . . . 5 class ((𝑛 maDet 𝑟)‘(𝑘𝑛, 𝑙𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑟), (0g𝑟)), (𝑘𝑚𝑙))))
3212, 13, 6, 6, 31cmpo 7147 . . . 4 class (𝑖𝑛, 𝑗𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘𝑛, 𝑙𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑟), (0g𝑟)), (𝑘𝑚𝑙)))))
335, 11, 32cmpt 5138 . . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑖𝑛, 𝑗𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘𝑛, 𝑙𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑟), (0g𝑟)), (𝑘𝑚𝑙))))))
342, 3, 4, 4, 33cmpo 7147 . 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑖𝑛, 𝑗𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘𝑛, 𝑙𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑟), (0g𝑟)), (𝑘𝑚𝑙)))))))
351, 34wceq 1528 1 wff maAdju = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑖𝑛, 𝑗𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘𝑛, 𝑙𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r𝑟), (0g𝑟)), (𝑘𝑚𝑙)))))))
Colors of variables: wff setvar class
This definition is referenced by:  madufval  21176
  Copyright terms: Public domain W3C validator