MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  madufval Structured version   Unicode version

Theorem madufval 18574
Description: First substitution for the adjunct (cofactor) matrix. (Contributed by SO, 11-Jul-2018.)
Hypotheses
Ref Expression
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
Ref Expression
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 ) ) ) ) ) )
Distinct variable groups:    m, N, i, j, k, l    R, m, i, j, k, l    B, m
Allowed substitution hints:    A( i, j, k, m, l)    B( i, j, k, l)    D( i, j, k, m, l)    .1. ( i, j, k, m, l)    J( i, j, k, m, l)    .0. ( i,
j, k, m, l)

Proof of Theorem madufval
Dummy variables  n  r are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 madufval.j . 2  |-  J  =  ( N maAdju  R )
2 oveq1 6206 . . . . . . 7  |-  ( n  =  N  ->  (
n Mat  r )  =  ( N Mat  r ) )
32fveq2d 5802 . . . . . 6  |-  ( n  =  N  ->  ( Base `  ( n Mat  r
) )  =  (
Base `  ( N Mat  r ) ) )
4 id 22 . . . . . . 7  |-  ( n  =  N  ->  n  =  N )
5 oveq1 6206 . . . . . . . 8  |-  ( n  =  N  ->  (
n maDet  r )  =  ( N maDet  r ) )
6 eqidd 2455 . . . . . . . . 9  |-  ( 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 ) ) )
74, 4, 6mpt2eq123dv 6256 . . . . . . . 8  |-  ( 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 ) ) ) )
85, 7fveq12d 5804 . . . . . . 7  |-  ( 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 ) ) ) ) )
94, 4, 8mpt2eq123dv 6256 . . . . . 6  |-  ( 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 ) ) ) ) ) )
103, 9mpteq12dv 4477 . . . . 5  |-  ( 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 ) ) ) ) ) ) )
11 oveq2 6207 . . . . . . 7  |-  ( r  =  R  ->  ( N Mat  r )  =  ( N Mat  R ) )
1211fveq2d 5802 . . . . . 6  |-  ( r  =  R  ->  ( Base `  ( N Mat  r
) )  =  (
Base `  ( N Mat  R ) ) )
13 oveq2 6207 . . . . . . . . 9  |-  ( r  =  R  ->  ( N maDet  r )  =  ( N maDet  R ) )
14 fveq2 5798 . . . . . . . . . . . . 13  |-  ( r  =  R  ->  ( 1r `  r )  =  ( 1r `  R
) )
15 fveq2 5798 . . . . . . . . . . . . 13  |-  ( r  =  R  ->  ( 0g `  r )  =  ( 0g `  R
) )
1614, 15ifeq12d 3916 . . . . . . . . . . . 12  |-  ( r  =  R  ->  if ( l  =  i ,  ( 1r `  r ) ,  ( 0g `  r ) )  =  if ( l  =  i ,  ( 1r `  R
) ,  ( 0g
`  R ) ) )
1716ifeq1d 3914 . . . . . . . . . . 11  |-  ( 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 ) ) )
18173ad2ant1 1009 . . . . . . . . . 10  |-  ( ( r  =  R  /\  k  e.  N  /\  l  e.  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 ) ) )
1918mpt2eq3dva 6258 . . . . . . . . 9  |-  ( 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 ) ) ) )
2013, 19fveq12d 5804 . . . . . . . 8  |-  ( 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 ) ) ) ) )
21203ad2ant1 1009 . . . . . . 7  |-  ( ( 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 ) ) ) )  =  ( ( N maDet  R ) `
 ( k  e.  N ,  l  e.  N  |->  if ( k  =  j ,  if ( l  =  i ,  ( 1r `  R ) ,  ( 0g `  R ) ) ,  ( k m l ) ) ) ) )
2221mpt2eq3dva 6258 . . . . . 6  |-  ( 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 ) ) ) ) ) )
2312, 22mpteq12dv 4477 . . . . 5  |-  ( 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 ) ) ) ) ) ) )
24 df-madu 18571 . . . . 5  |- 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 ) ) ) ) ) ) )
25 fvex 5808 . . . . . 6  |-  ( Base `  ( N Mat  R ) )  e.  _V
2625mptex 6056 . . . . 5  |-  ( 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
2710, 23, 24, 26ovmpt2 6335 . . . 4  |-  ( ( 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 ) ) ) ) ) ) )
28 madufval.b . . . . . 6  |-  B  =  ( Base `  A
)
29 madufval.a . . . . . . 7  |-  A  =  ( N Mat  R )
3029fveq2i 5801 . . . . . 6  |-  ( Base `  A )  =  (
Base `  ( N Mat  R ) )
3128, 30eqtri 2483 . . . . 5  |-  B  =  ( Base `  ( N Mat  R ) )
32 madufval.d . . . . . . . 8  |-  D  =  ( N maDet  R )
33 madufval.o . . . . . . . . . . . 12  |-  .1.  =  ( 1r `  R )
3433a1i 11 . . . . . . . . . . 11  |-  ( ( k  e.  N  /\  l  e.  N )  ->  .1.  =  ( 1r
`  R ) )
35 madufval.z . . . . . . . . . . . 12  |-  .0.  =  ( 0g `  R )
3635a1i 11 . . . . . . . . . . 11  |-  ( ( k  e.  N  /\  l  e.  N )  ->  .0.  =  ( 0g
`  R ) )
3734, 36ifeq12d 3916 . . . . . . . . . 10  |-  ( ( k  e.  N  /\  l  e.  N )  ->  if ( l  =  i ,  .1.  ,  .0.  )  =  if ( l  =  i ,  ( 1r `  R ) ,  ( 0g `  R ) ) )
3837ifeq1d 3914 . . . . . . . . 9  |-  ( ( 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 ) ) )
3938mpt2eq3ia 6259 . . . . . . . 8  |-  ( 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 ) ) )
4032, 39fveq12i 5803 . . . . . . 7  |-  ( 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 ) ) ) )
4140a1i 11 . . . . . 6  |-  ( ( 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 ) ) ) ) )
4241mpt2eq3ia 6259 . . . . 5  |-  ( 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 ) ) ) ) )
4331, 42mpteq12i 4483 . . . 4  |-  ( 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 ) ) ) ) ) )
4427, 43syl6eqr 2513 . . 3  |-  ( ( 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 ) ) ) ) ) ) )
4524reldmmpt2 6310 . . . . 5  |-  Rel  dom maAdju
4645ovprc 6226 . . . 4  |-  ( -.  ( N  e.  _V  /\  R  e.  _V )  ->  ( N maAdju  R )  =  (/) )
47 df-mat 18406 . . . . . . . . . . 11  |- Mat  =  ( n  e.  Fin , 
r  e.  _V  |->  ( ( r freeLMod  ( n  X.  n ) ) sSet  <. ( .r `  ndx ) ,  ( r maMul  <.
n ,  n ,  n >. ) >. )
)
4847reldmmpt2 6310 . . . . . . . . . 10  |-  Rel  dom Mat
4948ovprc 6226 . . . . . . . . 9  |-  ( -.  ( N  e.  _V  /\  R  e.  _V )  ->  ( N Mat  R )  =  (/) )
5029, 49syl5eq 2507 . . . . . . . 8  |-  ( -.  ( N  e.  _V  /\  R  e.  _V )  ->  A  =  (/) )
5150fveq2d 5802 . . . . . . 7  |-  ( -.  ( N  e.  _V  /\  R  e.  _V )  ->  ( Base `  A
)  =  ( Base `  (/) ) )
52 base0 14330 . . . . . . 7  |-  (/)  =  (
Base `  (/) )
5351, 28, 523eqtr4g 2520 . . . . . 6  |-  ( -.  ( N  e.  _V  /\  R  e.  _V )  ->  B  =  (/) )
5453mpteq1d 4480 . . . . 5  |-  ( -.  ( 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 ) ) ) ) ) ) )
55 mpt0 5645 . . . . 5  |-  ( 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 ) ) ) ) ) )  =  (/)
5654, 55syl6eq 2511 . . . 4  |-  ( -.  ( 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 ) ) ) ) ) )  =  (/) )
5746, 56eqtr4d 2498 . . 3  |-  ( -.  ( 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 ) ) ) ) ) ) )
5844, 57pm2.61i 164 . 2  |-  ( 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 ) ) ) ) ) )
591, 58eqtri 2483 1  |-  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 ) ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    /\ wa 369    = wceq 1370    e. wcel 1758   _Vcvv 3076   (/)c0 3744   ifcif 3898   <.cop 3990   <.cotp 3992    |-> cmpt 4457    X. cxp 4945   ` cfv 5525  (class class class)co 6199    |-> cmpt2 6201   Fincfn 7419   ndxcnx 14288   sSet csts 14289   Basecbs 14291   .rcmulr 14357   0gc0g 14496   1rcur 16724   freeLMod cfrlm 18295   maMul cmmul 18403   Mat cmat 18404   maDet cmdat 18521   maAdju cmadu 18569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4510  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-reu 2805  df-rab 2807  df-v 3078  df-sbc 3293  df-csb 3395  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-iun 4280  df-br 4400  df-opab 4458  df-mpt 4459  df-id 4743  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-ov 6202  df-oprab 6203  df-mpt2 6204  df-slot 14295  df-base 14296  df-mat 18406  df-madu 18571
This theorem is referenced by:  maduval  18575  maduf  18578
  Copyright terms: Public domain W3C validator