Definition df-madu 20440

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 = ( n e. _V , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( i e. n , j e. n |-> ( ( n maDet r ) ` ( k e. n , l e. n |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) ) ) ) )

Distinct variable group:   n, r, m, i, j, k, l

Detailed syntax breakdown of Definition df-madu

Step	Hyp	Ref	Expression
1		cmadu 20438	. 2 class maAdju
2		vn	. . 3 setvar n
3		vr	. . 3 setvar r
4		cvv 3200	. . 3 class _V
5		vm	. . . 4 setvar m
6	2	cv 1482	. . . . . 6 class n
7	3	cv 1482	. . . . . 6 class r
8		cmat 20213	. . . . . 6 class Mat
9	6, 7, 8	co 6650	. . . . 5 class ( n Mat r )
10		cbs 15857	. . . . 5 class Base
11	9, 10	cfv 5888	. . . 4 class ( Base ` ( n Mat r ) )
12		vi	. . . . 5 setvar i
13		vj	. . . . 5 setvar j
14		vk	. . . . . . 7 setvar k
15		vl	. . . . . . 7 setvar l
16	14, 13	weq 1874	. . . . . . . 8 wff k = j
17	15, 12	weq 1874	. . . . . . . . 9 wff l = i
18		cur 18501	. . . . . . . . . 10 class 1r
19	7, 18	cfv 5888	. . . . . . . . 9 class ( 1r ` r )
20		c0g 16100	. . . . . . . . . 10 class 0g
21	7, 20	cfv 5888	. . . . . . . . 9 class ( 0g ` r )
22	17, 19, 21	cif 4086	. . . . . . . 8 class if ( l = i , ( 1r ` r ) , ( 0g ` r ) )
23	14	cv 1482	. . . . . . . . 9 class k
24	15	cv 1482	. . . . . . . . 9 class l
25	5	cv 1482	. . . . . . . . 9 class m
26	23, 24, 25	co 6650	. . . . . . . 8 class ( k m l )
27	16, 22, 26	cif 4086	. . . . . . 7 class if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) )
28	14, 15, 6, 6, 27	cmpt2 6652	. . . . . 6 class ( k e. n , l e. n |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) )
29		cmdat 20390	. . . . . . 7 class maDet
30	6, 7, 29	co 6650	. . . . . 6 class ( n maDet r )
31	28, 30	cfv 5888	. . . . 5 class ( ( n maDet r ) ` ( k e. n , l e. n |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) )
32	12, 13, 6, 6, 31	cmpt2 6652	. . . 4 class ( i e. n , j e. n |-> ( ( n maDet r ) ` ( k e. n , l e. n |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) ) )
33	5, 11, 32	cmpt 4729	. . 3 class ( m e. ( Base ` ( n Mat r ) ) |-> ( i e. n , j e. n |-> ( ( n maDet r ) ` ( k e. n , l e. n |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) ) ) )
34	2, 3, 4, 4, 33	cmpt2 6652	. 2 class ( n e. _V , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( i e. n , j e. n |-> ( ( n maDet r ) ` ( k e. n , l e. n |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) ) ) ) )
35	1, 34	wceq 1483	1 wff maAdju = ( n e. _V , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( i e. n , j e. n |-> ( ( n maDet r ) ` ( k e. n , l e. n |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) ) ) ) )

This definition is referenced by:  madufval  20443