Metamath Proof Explorer

Definition df-madu

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)

Ref Expression
Assertion df-madu maAdju = ( 𝑛 ∈ V , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ ( ( 𝑛 maDet 𝑟 ) ‘ ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmadu ⊢ maAdju
1 vn ⊢ 𝑛
2 cvv ⊢ V
3 vr ⊢ 𝑟
4 vm ⊢ 𝑚
5 cbs ⊢ Base
6 1 cv ⊢ 𝑛
7 cmat ⊢ Mat
8 3 cv ⊢ 𝑟
9 6 8 7 co ⊢ ( 𝑛 Mat 𝑟 )
10 9 5 cfv ⊢ ( Base ‘ ( 𝑛 Mat 𝑟 ) )
11 vi ⊢ 𝑖
12 vj ⊢ 𝑗
13 cmdat ⊢ maDet
14 6 8 13 co ⊢ ( 𝑛 maDet 𝑟 )
15 vk ⊢ 𝑘
16 vl ⊢ 𝑙
17 15 cv ⊢ 𝑘
18 12 cv ⊢ 𝑗
19 17 18 wceq ⊢ 𝑘 = 𝑗
20 16 cv ⊢ 𝑙
21 11 cv ⊢ 𝑖
22 20 21 wceq ⊢ 𝑙 = 𝑖
23 cur ⊢ 1r
24 8 23 cfv ⊢ ( 1r ‘ 𝑟 )
25 c0g ⊢ 0g
26 8 25 cfv ⊢ ( 0g ‘ 𝑟 )
27 22 24 26 cif ⊢ if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) )
28 4 cv ⊢ 𝑚
29 17 20 28 co ⊢ ( 𝑘 𝑚 𝑙 )
30 19 27 29 cif ⊢ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) )
31 15 16 6 6 30 cmpo ⊢ ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) ) )
32 31 14 cfv ⊢ ( ( 𝑛 maDet 𝑟 ) ‘ ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) )
33 11 12 6 6 32 cmpo ⊢ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ ( ( 𝑛 maDet 𝑟 ) ‘ ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) )
34 4 10 33 cmpt ⊢ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ ( ( 𝑛 maDet 𝑟 ) ‘ ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) )
35 1 3 2 2 34 cmpo ⊢ ( 𝑛 ∈ V , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ ( ( 𝑛 maDet 𝑟 ) ‘ ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) ) )
36 0 35 wceq ⊢ maAdju = ( 𝑛 ∈ V , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ ( ( 𝑛 maDet 𝑟 ) ‘ ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) ) )