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 = n ∈ V , r ∈ V ⟼ m ∈ Base n Mat r ⟼ i ∈ n , j ∈ n ⟼ n maDet r ⁡ k ∈ n , l ∈ n ⟼ if k = j if l = i 1 r 0 r k m l

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmadu class maAdju
1 vn setvar n
2 cvv class V
3 vr setvar r
4 vm setvar m
5 cbs class Base
6 1 cv setvar n
7 cmat class Mat
8 3 cv setvar r
9 6 8 7 co class n Mat r
10 9 5 cfv class Base n Mat r
11 vi setvar i
12 vj setvar j
13 cmdat class maDet
14 6 8 13 co class n maDet r
15 vk setvar k
16 vl setvar l
17 15 cv setvar k
18 12 cv setvar j
19 17 18 wceq wff k = j
20 16 cv setvar l
21 11 cv setvar i
22 20 21 wceq wff l = i
23 cur class 1 r
24 8 23 cfv class 1 r
25 c0g class 0 𝑔
26 8 25 cfv class 0 r
27 22 24 26 cif class if l = i 1 r 0 r
28 4 cv setvar m
29 17 20 28 co class k m l
30 19 27 29 cif class if k = j if l = i 1 r 0 r k m l
31 15 16 6 6 30 cmpo class k ∈ n , l ∈ n ⟼ if k = j if l = i 1 r 0 r k m l
32 31 14 cfv class n maDet r ⁡ k ∈ n , l ∈ n ⟼ if k = j if l = i 1 r 0 r k m l
33 11 12 6 6 32 cmpo class i ∈ n , j ∈ n ⟼ n maDet r ⁡ k ∈ n , l ∈ n ⟼ if k = j if l = i 1 r 0 r k m l
34 4 10 33 cmpt class m ∈ Base n Mat r ⟼ i ∈ n , j ∈ n ⟼ n maDet r ⁡ k ∈ n , l ∈ n ⟼ if k = j if l = i 1 r 0 r k m l
35 1 3 2 2 34 cmpo class n ∈ V , r ∈ V ⟼ m ∈ Base n Mat r ⟼ i ∈ n , j ∈ n ⟼ n maDet r ⁡ k ∈ n , l ∈ n ⟼ if k = j if l = i 1 r 0 r k m l
36 0 35 wceq wff maAdju = n ∈ V , r ∈ V ⟼ m ∈ Base n Mat r ⟼ i ∈ n , j ∈ n ⟼ n maDet r ⁡ k ∈ n , l ∈ n ⟼ if k = j if l = i 1 r 0 r k m l