# Metamath Proof Explorer

Description: An entry of the adjunct (cofactor) matrix. (Contributed by SO, 11-Jul-2018)

Ref Expression
`|- A = ( N Mat R )`
`|- D = ( N maDet R )`
`|- J = ( N maAdju R )`
`|- B = ( Base ` A )`
`|- .1. = ( 1r ` R )`
`|- .0. = ( 0g ` R )`
`|- ( ( M e. B /\ I e. N /\ H e. N ) -> ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) ) ) )`

### Proof

Step Hyp Ref Expression
` |-  A = ( N Mat R )`
` |-  D = ( N maDet R )`
` |-  J = ( N maAdju R )`
` |-  B = ( Base ` A )`
` |-  .1. = ( 1r ` R )`
` |-  .0. = ( 0g ` R )`
7 1 2 3 4 5 6 maduval
` |-  ( M e. B -> ( J ` M ) = ( i e. N , j e. N |-> ( D ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) ) ) ) )`
` |-  ( ( M e. B /\ I e. N /\ H e. N ) -> ( J ` M ) = ( i e. N , j e. N |-> ( D ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) ) ) ) )`
9 simp1r
` |-  ( ( ( i = I /\ j = H ) /\ k e. N /\ l e. N ) -> j = H )`
10 9 eqeq2d
` |-  ( ( ( i = I /\ j = H ) /\ k e. N /\ l e. N ) -> ( k = j <-> k = H ) )`
11 simp1l
` |-  ( ( ( i = I /\ j = H ) /\ k e. N /\ l e. N ) -> i = I )`
12 11 eqeq2d
` |-  ( ( ( i = I /\ j = H ) /\ k e. N /\ l e. N ) -> ( l = i <-> l = I ) )`
13 12 ifbid
` |-  ( ( ( i = I /\ j = H ) /\ k e. N /\ l e. N ) -> if ( l = i , .1. , .0. ) = if ( l = I , .1. , .0. ) )`
14 10 13 ifbieq1d
` |-  ( ( ( i = I /\ j = H ) /\ k e. N /\ l e. N ) -> if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) = if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) )`
15 14 mpoeq3dva
` |-  ( ( i = I /\ j = H ) -> ( k e. N , l e. N |-> if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) ) = ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) ) )`
16 15 fveq2d
` |-  ( ( i = I /\ j = H ) -> ( D ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) ) ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) ) ) )`
` |-  ( ( ( M e. B /\ I e. N /\ H e. N ) /\ ( i = I /\ j = H ) ) -> ( D ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) ) ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) ) ) )`
` |-  ( ( M e. B /\ I e. N /\ H e. N ) -> I e. N )`
` |-  ( ( M e. B /\ I e. N /\ H e. N ) -> H e. N )`
` |-  ( ( M e. B /\ I e. N /\ H e. N ) -> ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) ) ) e. _V )`
` |-  ( ( M e. B /\ I e. N /\ H e. N ) -> ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) ) ) )`