Metamath Proof Explorer

Theorem madufval

Description: First 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 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 ) ) ) ) ) )

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 fvoveq1 
 |-  ( n = N -> ( Base ` ( n Mat r ) ) = ( Base ` ( N Mat r ) ) )
8 id 
 |-  ( n = N -> n = N )
9 oveq1 
 |-  ( n = N -> ( n maDet r ) = ( N maDet r ) )
10 eqidd 
 |-  ( n = N -> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) = if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) )
11 8 8 10 mpoeq123dv 
 |-  ( n = N -> ( k e. n , l e. n |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) = ( k e. N , l e. N |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) )
12 9 11 fveq12d 
 |-  ( n = N -> ( ( n maDet r ) ` ( k e. n , l e. n |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) ) = ( ( N maDet r ) ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) ) )
13 8 8 12 mpoeq123dv 
 |-  ( n = N -> ( i e. n , j e. n |-> ( ( n maDet r ) ` ( k e. n , l e. n |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) ) ) = ( i e. N , j e. N |-> ( ( N maDet r ) ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) ) ) )
14 7 13 mpteq12dv 
 |-  ( n = N -> ( m e. ( Base ` ( n Mat r ) ) |-> ( i e. n , j e. n |-> ( ( n maDet r ) ` ( k e. n , l e. n |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) ) ) ) = ( m e. ( Base ` ( N Mat r ) ) |-> ( i e. N , j e. N |-> ( ( N maDet r ) ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) ) ) ) )
15 oveq2 
 |-  ( r = R -> ( N Mat r ) = ( N Mat R ) )
16 15 fveq2d 
 |-  ( r = R -> ( Base ` ( N Mat r ) ) = ( Base ` ( N Mat R ) ) )
17 oveq2 
 |-  ( r = R -> ( N maDet r ) = ( N maDet R ) )
18 fveq2 
 |-  ( r = R -> ( 1r ` r ) = ( 1r ` R ) )
19 fveq2 
 |-  ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
20 18 19 ifeq12d 
 |-  ( r = R -> if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) = if ( l = i , ( 1r ` R ) , ( 0g ` R ) ) )
21 20 ifeq1d 
 |-  ( r = R -> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) = if ( k = j , if ( l = i , ( 1r ` R ) , ( 0g ` R ) ) , ( k m l ) ) )
22 21 mpoeq3dv 
 |-  ( r = R -> ( k e. N , l e. N |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) = ( k e. N , l e. N |-> if ( k = j , if ( l = i , ( 1r ` R ) , ( 0g ` R ) ) , ( k m l ) ) ) )
23 17 22 fveq12d 
 |-  ( r = R -> ( ( N maDet r ) ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) ) = ( ( N maDet R ) ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , ( 1r ` R ) , ( 0g ` R ) ) , ( k m l ) ) ) ) )
24 23 mpoeq3dv 
 |-  ( r = R -> ( i e. N , j e. N |-> ( ( N maDet r ) ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) ) ) = ( i e. N , j e. N |-> ( ( N maDet R ) ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , ( 1r ` R ) , ( 0g ` R ) ) , ( k m l ) ) ) ) ) )
25 16 24 mpteq12dv 
 |-  ( r = R -> ( m e. ( Base ` ( N Mat r ) ) |-> ( i e. N , j e. N |-> ( ( N maDet r ) ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) ) ) ) = ( m e. ( Base ` ( N Mat R ) ) |-> ( i e. N , j e. N |-> ( ( N maDet R ) ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , ( 1r ` R ) , ( 0g ` R ) ) , ( k m l ) ) ) ) ) ) )
26 df-madu 
 |-  maAdju = ( n e. _V , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( i e. n , j e. n |-> ( ( n maDet r ) ` ( k e. n , l e. n |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) ) ) ) )
27 fvex 
 |-  ( Base ` ( N Mat R ) ) e. _V
28 27 mptex 
 |-  ( m e. ( Base ` ( N Mat R ) ) |-> ( i e. N , j e. N |-> ( ( N maDet R ) ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , ( 1r ` R ) , ( 0g ` R ) ) , ( k m l ) ) ) ) ) ) e. _V
29 14 25 26 28 ovmpo 
 |-  ( ( N e. _V /\ R e. _V ) -> ( N maAdju R ) = ( m e. ( Base ` ( N Mat R ) ) |-> ( i e. N , j e. N |-> ( ( N maDet R ) ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , ( 1r ` R ) , ( 0g ` R ) ) , ( k m l ) ) ) ) ) ) )
30 1 fveq2i 
 |-  ( Base ` A ) = ( Base ` ( N Mat R ) )
31 4 30 eqtri 
 |-  B = ( Base ` ( N Mat R ) )
32 5 a1i 
 |-  ( ( k e. N /\ l e. N ) -> .1. = ( 1r ` R ) )
33 6 a1i 
 |-  ( ( k e. N /\ l e. N ) -> .0. = ( 0g ` R ) )
34 32 33 ifeq12d 
 |-  ( ( k e. N /\ l e. N ) -> if ( l = i , .1. , .0. ) = if ( l = i , ( 1r ` R ) , ( 0g ` R ) ) )
35 34 ifeq1d 
 |-  ( ( k e. N /\ l e. N ) -> if ( k = j , if ( l = i , .1. , .0. ) , ( k m l ) ) = if ( k = j , if ( l = i , ( 1r ` R ) , ( 0g ` R ) ) , ( k m l ) ) )
36 35 mpoeq3ia 
 |-  ( 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 , ( 1r ` R ) , ( 0g ` R ) ) , ( k m l ) ) )
37 2 36 fveq12i 
 |-  ( D ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , .1. , .0. ) , ( k m l ) ) ) ) = ( ( N maDet R ) ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , ( 1r ` R ) , ( 0g ` R ) ) , ( k m l ) ) ) )
38 37 a1i 
 |-  ( ( i e. N /\ j e. N ) -> ( D ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , .1. , .0. ) , ( k m l ) ) ) ) = ( ( N maDet R ) ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , ( 1r ` R ) , ( 0g ` R ) ) , ( k m l ) ) ) ) )
39 38 mpoeq3ia 
 |-  ( 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 |-> ( ( N maDet R ) ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , ( 1r ` R ) , ( 0g ` R ) ) , ( k m l ) ) ) ) )
40 31 39 mpteq12i 
 |-  ( 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 ) ) ) ) ) ) = ( m e. ( Base ` ( N Mat R ) ) |-> ( i e. N , j e. N |-> ( ( N maDet R ) ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , ( 1r ` R ) , ( 0g ` R ) ) , ( k m l ) ) ) ) ) )
41 29 40 eqtr4di 
 |-  ( ( N e. _V /\ R e. _V ) -> ( N maAdju R ) = ( 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 ) ) ) ) ) ) )
42 26 reldmmpo 
 |-  Rel dom maAdju
43 42 ovprc 
 |-  ( -. ( N e. _V /\ R e. _V ) -> ( N maAdju R ) = (/) )
44 df-mat 
 |-  Mat = ( n e. Fin , r e. _V |-> ( ( r freeLMod ( n X. n ) ) sSet <. ( .r ` ndx ) , ( r maMul <. n , n , n >. ) >. ) )
45 44 reldmmpo 
 |-  Rel dom Mat
46 45 ovprc 
 |-  ( -. ( N e. _V /\ R e. _V ) -> ( N Mat R ) = (/) )
47 1 46 eqtrid 
 |-  ( -. ( N e. _V /\ R e. _V ) -> A = (/) )
48 47 fveq2d 
 |-  ( -. ( N e. _V /\ R e. _V ) -> ( Base ` A ) = ( Base ` (/) ) )
49 base0 
 |-  (/) = ( Base ` (/) )
50 48 4 49 3eqtr4g 
 |-  ( -. ( N e. _V /\ R e. _V ) -> B = (/) )
51 50 mpteq1d 
 |-  ( -. ( N e. _V /\ R e. _V ) -> ( 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 ) ) ) ) ) ) = ( m e. (/) |-> ( i e. N , j e. N |-> ( D ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , .1. , .0. ) , ( k m l ) ) ) ) ) ) )
52 mpt0 
 |-  ( m e. (/) |-> ( i e. N , j e. N |-> ( D ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , .1. , .0. ) , ( k m l ) ) ) ) ) ) = (/)
53 51 52 eqtrdi 
 |-  ( -. ( N e. _V /\ R e. _V ) -> ( 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 ) ) ) ) ) ) = (/) )
54 43 53 eqtr4d 
 |-  ( -. ( N e. _V /\ R e. _V ) -> ( N maAdju R ) = ( 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 ) ) ) ) ) ) )
55 41 54 pm2.61i 
 |-  ( N maAdju R ) = ( 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 ) ) ) ) ) )
56 3 55 eqtri 
 |-  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 ) ) ) ) ) )