Theorem maducoevalmin1

Description: The coefficients of an adjunct (matrix of cofactors) expressed as determinants of the minor matrices (alternative definition) of the original matrix. (Contributed by AV, 31-Dec-2018)

	Ref	Expression
Hypotheses	maducoevalmin1.a	|- A = ( N Mat R )
	maducoevalmin1.b	|- B = ( Base ` A )
	maducoevalmin1.d	|- D = ( N maDet R )
	maducoevalmin1.j	|- J = ( N maAdju R )
Assertion	maducoevalmin1	|- ( ( M e. B /\ I e. N /\ H e. N ) -> ( I ( J ` M ) H ) = ( D ` ( H ( ( N minMatR1 R ) ` M ) I ) ) )

Proof

Step	Hyp	Ref	Expression
1		maducoevalmin1.a	|- A = ( N Mat R )
2		maducoevalmin1.b	|- B = ( Base ` A )
3		maducoevalmin1.d	|- D = ( N maDet R )
4		maducoevalmin1.j	|- J = ( N maAdju R )
5		eqid	|- ( 1r ` R ) = ( 1r ` R )
6		eqid	|- ( 0g ` R ) = ( 0g ` R )
7	1 3 4 2 5 6	maducoeval	|- ( ( M e. B /\ I e. N /\ H e. N ) -> ( I ( J ` M ) H ) = ( D ` ( i e. N , j e. N |-> if ( i = H , if ( j = I , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) ) ) )
8		eqid	|- ( N minMatR1 R ) = ( N minMatR1 R )
9	1 2 8 5 6	minmar1val	|- ( ( M e. B /\ H e. N /\ I e. N ) -> ( H ( ( N minMatR1 R ) ` M ) I ) = ( i e. N , j e. N |-> if ( i = H , if ( j = I , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) ) )
10	9	3com23	|- ( ( M e. B /\ I e. N /\ H e. N ) -> ( H ( ( N minMatR1 R ) ` M ) I ) = ( i e. N , j e. N |-> if ( i = H , if ( j = I , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) ) )
11	10	eqcomd	|- ( ( M e. B /\ I e. N /\ H e. N ) -> ( i e. N , j e. N |-> if ( i = H , if ( j = I , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) ) = ( H ( ( N minMatR1 R ) ` M ) I ) )
12	11	fveq2d	|- ( ( M e. B /\ I e. N /\ H e. N ) -> ( D ` ( i e. N , j e. N |-> if ( i = H , if ( j = I , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) ) ) = ( D ` ( H ( ( N minMatR1 R ) ` M ) I ) ) )
13	7 12	eqtrd	|- ( ( M e. B /\ I e. N /\ H e. N ) -> ( I ( J ` M ) H ) = ( D ` ( H ( ( N minMatR1 R ) ` M ) I ) ) )