madjusmdet

Description: Express the cofactor of the matrix, i.e. the entries of its adjunct matrix, using determinant of submatrices. (Contributed by Thierry Arnoux, 23-Aug-2020)

	Ref	Expression
Hypotheses	madjusmdet.b	\|- B = ( Base ` A )
	madjusmdet.a	\|- A = ( ( 1 ... N ) Mat R )
	madjusmdet.d	\|- D = ( ( 1 ... N ) maDet R )
	madjusmdet.k	\|- K = ( ( 1 ... N ) maAdju R )
	madjusmdet.t	\|- .x. = ( .r ` R )
	madjusmdet.z	\|- Z = ( ZRHom ` R )
	madjusmdet.e	\|- E = ( ( 1 ... ( N - 1 ) ) maDet R )
	madjusmdet.n	\|- ( ph -> N e. NN )
	madjusmdet.r	\|- ( ph -> R e. CRing )
	madjusmdet.i	\|- ( ph -> I e. ( 1 ... N ) )
	madjusmdet.j	\|- ( ph -> J e. ( 1 ... N ) )
	madjusmdet.m	\|- ( ph -> M e. B )
Assertion	madjusmdet	\|- ( ph -> ( J ( K ` M ) I ) = ( ( Z ` ( -u 1 ^ ( I + J ) ) ) .x. ( E ` ( I ( subMat1 ` M ) J ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		madjusmdet.b	\|- B = ( Base ` A )
2		madjusmdet.a	\|- A = ( ( 1 ... N ) Mat R )
3		madjusmdet.d	\|- D = ( ( 1 ... N ) maDet R )
4		madjusmdet.k	\|- K = ( ( 1 ... N ) maAdju R )
5		madjusmdet.t	\|- .x. = ( .r ` R )
6		madjusmdet.z	\|- Z = ( ZRHom ` R )
7		madjusmdet.e	\|- E = ( ( 1 ... ( N - 1 ) ) maDet R )
8		madjusmdet.n	\|- ( ph -> N e. NN )
9		madjusmdet.r	\|- ( ph -> R e. CRing )
10		madjusmdet.i	\|- ( ph -> I e. ( 1 ... N ) )
11		madjusmdet.j	\|- ( ph -> J e. ( 1 ... N ) )
12		madjusmdet.m	\|- ( ph -> M e. B )
13		eqeq1	\|- ( k = i -> ( k = 1 <-> i = 1 ) )
14		breq1	\|- ( k = i -> ( k <_ I <-> i <_ I ) )
15		oveq1	\|- ( k = i -> ( k - 1 ) = ( i - 1 ) )
16		id	\|- ( k = i -> k = i )
17	14 15 16	ifbieq12d	\|- ( k = i -> if ( k <_ I , ( k - 1 ) , k ) = if ( i <_ I , ( i - 1 ) , i ) )
18	13 17	ifbieq2d	\|- ( k = i -> if ( k = 1 , I , if ( k <_ I , ( k - 1 ) , k ) ) = if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) )
19	18	cbvmptv	\|- ( k e. ( 1 ... N ) \|-> if ( k = 1 , I , if ( k <_ I , ( k - 1 ) , k ) ) ) = ( i e. ( 1 ... N ) \|-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) )
20		breq1	\|- ( k = i -> ( k <_ N <-> i <_ N ) )
21	20 15 16	ifbieq12d	\|- ( k = i -> if ( k <_ N , ( k - 1 ) , k ) = if ( i <_ N , ( i - 1 ) , i ) )
22	13 21	ifbieq2d	\|- ( k = i -> if ( k = 1 , N , if ( k <_ N , ( k - 1 ) , k ) ) = if ( i = 1 , N , if ( i <_ N , ( i - 1 ) , i ) ) )
23	22	cbvmptv	\|- ( k e. ( 1 ... N ) \|-> if ( k = 1 , N , if ( k <_ N , ( k - 1 ) , k ) ) ) = ( i e. ( 1 ... N ) \|-> if ( i = 1 , N , if ( i <_ N , ( i - 1 ) , i ) ) )
24		eqeq1	\|- ( l = j -> ( l = 1 <-> j = 1 ) )
25		breq1	\|- ( l = j -> ( l <_ J <-> j <_ J ) )
26		oveq1	\|- ( l = j -> ( l - 1 ) = ( j - 1 ) )
27		id	\|- ( l = j -> l = j )
28	25 26 27	ifbieq12d	\|- ( l = j -> if ( l <_ J , ( l - 1 ) , l ) = if ( j <_ J , ( j - 1 ) , j ) )
29	24 28	ifbieq2d	\|- ( l = j -> if ( l = 1 , J , if ( l <_ J , ( l - 1 ) , l ) ) = if ( j = 1 , J , if ( j <_ J , ( j - 1 ) , j ) ) )
30	29	cbvmptv	\|- ( l e. ( 1 ... N ) \|-> if ( l = 1 , J , if ( l <_ J , ( l - 1 ) , l ) ) ) = ( j e. ( 1 ... N ) \|-> if ( j = 1 , J , if ( j <_ J , ( j - 1 ) , j ) ) )
31		breq1	\|- ( l = j -> ( l <_ N <-> j <_ N ) )
32	31 26 27	ifbieq12d	\|- ( l = j -> if ( l <_ N , ( l - 1 ) , l ) = if ( j <_ N , ( j - 1 ) , j ) )
33	24 32	ifbieq2d	\|- ( l = j -> if ( l = 1 , N , if ( l <_ N , ( l - 1 ) , l ) ) = if ( j = 1 , N , if ( j <_ N , ( j - 1 ) , j ) ) )
34	33	cbvmptv	\|- ( l e. ( 1 ... N ) \|-> if ( l = 1 , N , if ( l <_ N , ( l - 1 ) , l ) ) ) = ( j e. ( 1 ... N ) \|-> if ( j = 1 , N , if ( j <_ N , ( j - 1 ) , j ) ) )
35	1 2 3 4 5 6 7 8 9 10 11 12 19 23 30 34	madjusmdetlem4	\|- ( ph -> ( J ( K ` M ) I ) = ( ( Z ` ( -u 1 ^ ( I + J ) ) ) .x. ( E ` ( I ( subMat1 ` M ) J ) ) ) )

Metamath Proof Explorer

Theorem madjusmdet

Proof