This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )