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