# Metamath Proof Explorer

Description: Second substitution for 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 -> ( 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 ) ) ) ) ) )

### 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 4 matrcl
|-  ( M e. B -> ( N e. Fin /\ R e. _V ) )
8 7 simpld
|-  ( M e. B -> N e. Fin )
9 mpoexga
|-  ( ( N e. Fin /\ N e. Fin ) -> ( i e. N , j e. N |-> ( D ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) ) ) ) e. _V )
10 8 8 9 syl2anc
|-  ( M e. B -> ( i e. N , j e. N |-> ( D ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) ) ) ) e. _V )
11 oveq
|-  ( m = M -> ( k m l ) = ( k M l ) )
12 11 ifeq2d
|-  ( m = M -> if ( k = j , if ( l = i , .1. , .0. ) , ( k m l ) ) = if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) )
13 12 mpoeq3dv
|-  ( m = M -> ( 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 = j , if ( l = i , .1. , .0. ) , ( k M l ) ) ) )