Metamath Proof Explorer


Theorem maduval

Description: Second substitution for the adjunct (cofactor) matrix. (Contributed by SO, 11-Jul-2018)

Ref Expression
Hypotheses madufval.a
|- A = ( N Mat R )
madufval.d
|- D = ( N maDet R )
madufval.j
|- J = ( N maAdju R )
madufval.b
|- B = ( Base ` A )
madufval.o
|- .1. = ( 1r ` R )
madufval.z
|- .0. = ( 0g ` R )
Assertion 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 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 madufval.a
 |-  A = ( N Mat R )
2 madufval.d
 |-  D = ( N maDet R )
3 madufval.j
 |-  J = ( N maAdju R )
4 madufval.b
 |-  B = ( Base ` A )
5 madufval.o
 |-  .1. = ( 1r ` R )
6 madufval.z
 |-  .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 ) ) ) )
14 13 3ad2ant1
 |-  ( ( m = M /\ i e. N /\ j e. N ) -> ( 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 ) ) ) )
15 14 fveq2d
 |-  ( ( m = 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 ) ) ) ) = ( D ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) ) ) )
16 15 mpoeq3dva
 |-  ( m = 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 ) ) ) ) ) = ( i e. N , j e. N |-> ( D ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) ) ) ) )
17 1 2 3 4 5 6 madufval
 |-  J = ( 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 ) ) ) ) ) )
18 16 17 fvmptg
 |-  ( ( 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 ) -> ( 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 ) ) ) ) ) )
19 10 18 mpdan
 |-  ( 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 ) ) ) ) ) )