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

Theorem madugsum 19652
Description: The determinant of a matrix with a row  L consisting of the same element  X is the sum of the elements of the  L-th column of the adjunct of the matrix multiplied with  X. (Contributed by Stefan O'Rear, 16-Jul-2018.)
Hypotheses
Ref Expression
maduf.a  |-  A  =  ( N Mat  R )
maduf.j  |-  J  =  ( N maAdju  R )
maduf.b  |-  B  =  ( Base `  A
)
madugsum.d  |-  D  =  ( N maDet  R )
madugsum.t  |-  .x.  =  ( .r `  R )
madugsum.k  |-  K  =  ( Base `  R
)
madugsum.m  |-  ( ph  ->  M  e.  B )
madugsum.r  |-  ( ph  ->  R  e.  CRing )
madugsum.x  |-  ( (
ph  /\  i  e.  N )  ->  X  e.  K )
madugsum.l  |-  ( ph  ->  L  e.  N )
Assertion
Ref Expression
madugsum  |-  ( ph  ->  ( R  gsumg  ( i  e.  N  |->  ( X  .x.  (
i ( J `  M ) L ) ) ) )  =  ( D `  (
j  e.  N , 
i  e.  N  |->  if ( j  =  L ,  X ,  ( j M i ) ) ) ) )
Distinct variable groups:    i, N, j    R, i, j    B, i, j    ph, i, j   
i, J    i, K, j    i, M, j    j, X    .x. , i    i, L, j
Allowed substitution hints:    A( i, j)    D( i, j)    .x. ( j)    J( j)    X( i)

Proof of Theorem madugsum
Dummy variables  a 
b  c  d  e are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mpteq1 4501 . . . . 5  |-  ( c  =  (/)  ->  ( b  e.  c  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `
 M ) L ) ) )  =  ( b  e.  (/)  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `  M
) L ) ) ) )
21oveq2d 6317 . . . 4  |-  ( c  =  (/)  ->  ( R 
gsumg  ( b  e.  c 
|->  ( [_ b  / 
i ]_ X  .x.  (
b ( J `  M ) L ) ) ) )  =  ( R  gsumg  ( b  e.  (/)  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `  M
) L ) ) ) ) )
3 eleq2 2495 . . . . . . . 8  |-  ( c  =  (/)  ->  ( b  e.  c  <->  b  e.  (/) ) )
43ifbid 3931 . . . . . . 7  |-  ( c  =  (/)  ->  if ( b  e.  c , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) )  =  if ( b  e.  (/) ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) )
54ifeq1d 3927 . . . . . 6  |-  ( c  =  (/)  ->  if ( a  =  L ,  if ( b  e.  c ,  [_ b  / 
i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) )  =  if ( a  =  L ,  if ( b  e.  (/) , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) ) ,  ( a M b ) ) )
65mpt2eq3dv 6367 . . . . 5  |-  ( c  =  (/)  ->  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  c ,  [_ b  / 
i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) )  =  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  (/) , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) ) ,  ( a M b ) ) ) )
76fveq2d 5881 . . . 4  |-  ( c  =  (/)  ->  ( D `
 ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  c ,  [_ b  / 
i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) )  =  ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  (/) , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) ) ,  ( a M b ) ) ) ) )
82, 7eqeq12d 2444 . . 3  |-  ( c  =  (/)  ->  ( ( R  gsumg  ( b  e.  c 
|->  ( [_ b  / 
i ]_ X  .x.  (
b ( J `  M ) L ) ) ) )  =  ( D `  (
a  e.  N , 
b  e.  N  |->  if ( a  =  L ,  if ( b  e.  c ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) )  <-> 
( R  gsumg  ( b  e.  (/)  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `  M
) L ) ) ) )  =  ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  (/) , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) ) ,  ( a M b ) ) ) ) ) )
9 mpteq1 4501 . . . . 5  |-  ( c  =  d  ->  (
b  e.  c  |->  (
[_ b  /  i ]_ X  .x.  ( b ( J `  M
) L ) ) )  =  ( b  e.  d  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `
 M ) L ) ) ) )
109oveq2d 6317 . . . 4  |-  ( c  =  d  ->  ( R  gsumg  ( b  e.  c 
|->  ( [_ b  / 
i ]_ X  .x.  (
b ( J `  M ) L ) ) ) )  =  ( R  gsumg  ( b  e.  d 
|->  ( [_ b  / 
i ]_ X  .x.  (
b ( J `  M ) L ) ) ) ) )
11 eleq2 2495 . . . . . . . 8  |-  ( c  =  d  ->  (
b  e.  c  <->  b  e.  d ) )
1211ifbid 3931 . . . . . . 7  |-  ( c  =  d  ->  if ( b  e.  c ,  [_ b  / 
i ]_ X ,  ( 0g `  R ) )  =  if ( b  e.  d , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) ) )
1312ifeq1d 3927 . . . . . 6  |-  ( c  =  d  ->  if ( a  =  L ,  if ( b  e.  c ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) )  =  if ( a  =  L ,  if ( b  e.  d ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) )
1413mpt2eq3dv 6367 . . . . 5  |-  ( c  =  d  ->  (
a  e.  N , 
b  e.  N  |->  if ( a  =  L ,  if ( b  e.  c ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) )  =  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  d , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) ) ,  ( a M b ) ) ) )
1514fveq2d 5881 . . . 4  |-  ( c  =  d  ->  ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  c ,  [_ b  / 
i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) )  =  ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  d ,  [_ b  / 
i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) ) )
1610, 15eqeq12d 2444 . . 3  |-  ( c  =  d  ->  (
( R  gsumg  ( b  e.  c 
|->  ( [_ b  / 
i ]_ X  .x.  (
b ( J `  M ) L ) ) ) )  =  ( D `  (
a  e.  N , 
b  e.  N  |->  if ( a  =  L ,  if ( b  e.  c ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) )  <-> 
( R  gsumg  ( b  e.  d 
|->  ( [_ b  / 
i ]_ X  .x.  (
b ( J `  M ) L ) ) ) )  =  ( D `  (
a  e.  N , 
b  e.  N  |->  if ( a  =  L ,  if ( b  e.  d ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) ) ) )
17 mpteq1 4501 . . . . 5  |-  ( c  =  ( d  u. 
{ e } )  ->  ( b  e.  c  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `
 M ) L ) ) )  =  ( b  e.  ( d  u.  { e } )  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `
 M ) L ) ) ) )
1817oveq2d 6317 . . . 4  |-  ( c  =  ( d  u. 
{ e } )  ->  ( R  gsumg  ( b  e.  c  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `
 M ) L ) ) ) )  =  ( R  gsumg  ( b  e.  ( d  u. 
{ e } ) 
|->  ( [_ b  / 
i ]_ X  .x.  (
b ( J `  M ) L ) ) ) ) )
19 eleq2 2495 . . . . . . . 8  |-  ( c  =  ( d  u. 
{ e } )  ->  ( b  e.  c  <->  b  e.  ( d  u.  { e } ) ) )
2019ifbid 3931 . . . . . . 7  |-  ( c  =  ( d  u. 
{ e } )  ->  if ( b  e.  c ,  [_ b  /  i ]_ X ,  ( 0g `  R ) )  =  if ( b  e.  ( d  u.  {
e } ) , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) ) )
2120ifeq1d 3927 . . . . . 6  |-  ( c  =  ( d  u. 
{ e } )  ->  if ( a  =  L ,  if ( b  e.  c ,  [_ b  / 
i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) )  =  if ( a  =  L ,  if ( b  e.  ( d  u.  { e } ) ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) )
2221mpt2eq3dv 6367 . . . . 5  |-  ( c  =  ( d  u. 
{ e } )  ->  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  c ,  [_ b  / 
i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) )  =  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  ( d  u.  { e } ) ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) )
2322fveq2d 5881 . . . 4  |-  ( c  =  ( d  u. 
{ e } )  ->  ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  c , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) ) ,  ( a M b ) ) ) )  =  ( D `
 ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  ( d  u.  { e } ) ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) ) )
2418, 23eqeq12d 2444 . . 3  |-  ( c  =  ( d  u. 
{ e } )  ->  ( ( R 
gsumg  ( b  e.  c 
|->  ( [_ b  / 
i ]_ X  .x.  (
b ( J `  M ) L ) ) ) )  =  ( D `  (
a  e.  N , 
b  e.  N  |->  if ( a  =  L ,  if ( b  e.  c ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) )  <-> 
( R  gsumg  ( b  e.  ( d  u.  { e } )  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `
 M ) L ) ) ) )  =  ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  ( d  u.  { e } ) ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) ) ) )
25 mpteq1 4501 . . . . 5  |-  ( c  =  N  ->  (
b  e.  c  |->  (
[_ b  /  i ]_ X  .x.  ( b ( J `  M
) L ) ) )  =  ( b  e.  N  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `
 M ) L ) ) ) )
2625oveq2d 6317 . . . 4  |-  ( c  =  N  ->  ( R  gsumg  ( b  e.  c 
|->  ( [_ b  / 
i ]_ X  .x.  (
b ( J `  M ) L ) ) ) )  =  ( R  gsumg  ( b  e.  N  |->  ( [_ b  / 
i ]_ X  .x.  (
b ( J `  M ) L ) ) ) ) )
27 eleq2 2495 . . . . . . . 8  |-  ( c  =  N  ->  (
b  e.  c  <->  b  e.  N ) )
2827ifbid 3931 . . . . . . 7  |-  ( c  =  N  ->  if ( b  e.  c ,  [_ b  / 
i ]_ X ,  ( 0g `  R ) )  =  if ( b  e.  N ,  [_ b  /  i ]_ X ,  ( 0g
`  R ) ) )
2928ifeq1d 3927 . . . . . 6  |-  ( c  =  N  ->  if ( a  =  L ,  if ( b  e.  c ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) )  =  if ( a  =  L ,  if ( b  e.  N ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) )
3029mpt2eq3dv 6367 . . . . 5  |-  ( c  =  N  ->  (
a  e.  N , 
b  e.  N  |->  if ( a  =  L ,  if ( b  e.  c ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) )  =  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  N ,  [_ b  /  i ]_ X ,  ( 0g
`  R ) ) ,  ( a M b ) ) ) )
3130fveq2d 5881 . . . 4  |-  ( c  =  N  ->  ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  c ,  [_ b  / 
i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) )  =  ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  N ,  [_ b  /  i ]_ X ,  ( 0g
`  R ) ) ,  ( a M b ) ) ) ) )
3226, 31eqeq12d 2444 . . 3  |-  ( c  =  N  ->  (
( R  gsumg  ( b  e.  c 
|->  ( [_ b  / 
i ]_ X  .x.  (
b ( J `  M ) L ) ) ) )  =  ( D `  (
a  e.  N , 
b  e.  N  |->  if ( a  =  L ,  if ( b  e.  c ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) )  <-> 
( R  gsumg  ( b  e.  N  |->  ( [_ b  / 
i ]_ X  .x.  (
b ( J `  M ) L ) ) ) )  =  ( D `  (
a  e.  N , 
b  e.  N  |->  if ( a  =  L ,  if ( b  e.  N ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) ) ) )
33 noel 3765 . . . . . . . . 9  |-  -.  b  e.  (/)
34 iffalse 3918 . . . . . . . . 9  |-  ( -.  b  e.  (/)  ->  if ( b  e.  (/) , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) )  =  ( 0g `  R ) )
3533, 34mp1i 13 . . . . . . . 8  |-  ( ( a  e.  N  /\  b  e.  N )  ->  if ( b  e.  (/) ,  [_ b  / 
i ]_ X ,  ( 0g `  R ) )  =  ( 0g
`  R ) )
3635ifeq1d 3927 . . . . . . 7  |-  ( ( a  e.  N  /\  b  e.  N )  ->  if ( a  =  L ,  if ( b  e.  (/) ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) )  =  if ( a  =  L ,  ( 0g `  R ) ,  ( a M b ) ) )
3736mpt2eq3ia 6366 . . . . . 6  |-  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  (/) , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) ) ,  ( a M b ) ) )  =  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  ( 0g `  R ) ,  ( a M b ) ) )
3837fveq2i 5880 . . . . 5  |-  ( D `
 ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  (/) , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) ) ,  ( a M b ) ) ) )  =  ( D `
 ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  ( 0g `  R ) ,  ( a M b ) ) ) )
39 madugsum.d . . . . . 6  |-  D  =  ( N maDet  R )
40 madugsum.k . . . . . 6  |-  K  =  ( Base `  R
)
41 eqid 2422 . . . . . 6  |-  ( 0g
`  R )  =  ( 0g `  R
)
42 madugsum.r . . . . . 6  |-  ( ph  ->  R  e.  CRing )
43 madugsum.m . . . . . . . 8  |-  ( ph  ->  M  e.  B )
44 maduf.a . . . . . . . . 9  |-  A  =  ( N Mat  R )
45 maduf.b . . . . . . . . 9  |-  B  =  ( Base `  A
)
4644, 45matrcl 19421 . . . . . . . 8  |-  ( M  e.  B  ->  ( N  e.  Fin  /\  R  e.  _V ) )
4743, 46syl 17 . . . . . . 7  |-  ( ph  ->  ( N  e.  Fin  /\  R  e.  _V )
)
4847simpld 460 . . . . . 6  |-  ( ph  ->  N  e.  Fin )
4944, 40, 45matbas2i 19431 . . . . . . . . 9  |-  ( M  e.  B  ->  M  e.  ( K  ^m  ( N  X.  N ) ) )
50 elmapi 7497 . . . . . . . . 9  |-  ( M  e.  ( K  ^m  ( N  X.  N
) )  ->  M : ( N  X.  N ) --> K )
5143, 49, 503syl 18 . . . . . . . 8  |-  ( ph  ->  M : ( N  X.  N ) --> K )
5251fovrnda 6450 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  N  /\  b  e.  N ) )  -> 
( a M b )  e.  K )
53523impb 1201 . . . . . 6  |-  ( (
ph  /\  a  e.  N  /\  b  e.  N
)  ->  ( a M b )  e.  K )
54 madugsum.l . . . . . 6  |-  ( ph  ->  L  e.  N )
5539, 40, 41, 42, 48, 53, 54mdetr0 19614 . . . . 5  |-  ( ph  ->  ( D `  (
a  e.  N , 
b  e.  N  |->  if ( a  =  L ,  ( 0g `  R ) ,  ( a M b ) ) ) )  =  ( 0g `  R
) )
5638, 55syl5eq 2475 . . . 4  |-  ( ph  ->  ( D `  (
a  e.  N , 
b  e.  N  |->  if ( a  =  L ,  if ( b  e.  (/) ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) )  =  ( 0g `  R ) )
57 mpt0 5719 . . . . . 6  |-  ( b  e.  (/)  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `
 M ) L ) ) )  =  (/)
5857oveq2i 6312 . . . . 5  |-  ( R 
gsumg  ( b  e.  (/)  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `  M
) L ) ) ) )  =  ( R  gsumg  (/) )
5941gsum0 16506 . . . . 5  |-  ( R 
gsumg  (/) )  =  ( 0g
`  R )
6058, 59eqtri 2451 . . . 4  |-  ( R 
gsumg  ( b  e.  (/)  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `  M
) L ) ) ) )  =  ( 0g `  R )
6156, 60syl6reqr 2482 . . 3  |-  ( ph  ->  ( R  gsumg  ( b  e.  (/)  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `  M
) L ) ) ) )  =  ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  (/) , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) ) ,  ( a M b ) ) ) ) )
62 eqid 2422 . . . . . . 7  |-  ( +g  `  R )  =  ( +g  `  R )
6342adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  ->  R  e.  CRing )
64 crngring 17776 . . . . . . . . 9  |-  ( R  e.  CRing  ->  R  e.  Ring )
6563, 64syl 17 . . . . . . . 8  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  ->  R  e.  Ring )
66 ringcmn 17796 . . . . . . . 8  |-  ( R  e.  Ring  ->  R  e. CMnd
)
6765, 66syl 17 . . . . . . 7  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  ->  R  e. CMnd )
6848adantr 466 . . . . . . . 8  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  ->  N  e.  Fin )
69 simprl 762 . . . . . . . 8  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
d  C_  N )
70 ssfi 7794 . . . . . . . 8  |-  ( ( N  e.  Fin  /\  d  C_  N )  -> 
d  e.  Fin )
7168, 69, 70syl2anc 665 . . . . . . 7  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
d  e.  Fin )
7265adantr 466 . . . . . . . 8  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  b  e.  d )  ->  R  e.  Ring )
7369sselda 3464 . . . . . . . . 9  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  b  e.  d )  ->  b  e.  N )
74 madugsum.x . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  N )  ->  X  e.  K )
7574ralrimiva 2839 . . . . . . . . . 10  |-  ( ph  ->  A. i  e.  N  X  e.  K )
7675ad2antrr 730 . . . . . . . . 9  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  b  e.  d )  ->  A. i  e.  N  X  e.  K )
77 rspcsbela 3823 . . . . . . . . 9  |-  ( ( b  e.  N  /\  A. i  e.  N  X  e.  K )  ->  [_ b  /  i ]_ X  e.  K )
7873, 76, 77syl2anc 665 . . . . . . . 8  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  b  e.  d )  ->  [_ b  / 
i ]_ X  e.  K
)
79 maduf.j . . . . . . . . . . . . . 14  |-  J  =  ( N maAdju  R )
8044, 79, 45maduf 19650 . . . . . . . . . . . . 13  |-  ( R  e.  CRing  ->  J : B
--> B )
8142, 80syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  J : B --> B )
8281, 43ffvelrnd 6034 . . . . . . . . . . 11  |-  ( ph  ->  ( J `  M
)  e.  B )
8344, 40, 45matbas2i 19431 . . . . . . . . . . 11  |-  ( ( J `  M )  e.  B  ->  ( J `  M )  e.  ( K  ^m  ( N  X.  N ) ) )
84 elmapi 7497 . . . . . . . . . . 11  |-  ( ( J `  M )  e.  ( K  ^m  ( N  X.  N
) )  ->  ( J `  M ) : ( N  X.  N ) --> K )
8582, 83, 843syl 18 . . . . . . . . . 10  |-  ( ph  ->  ( J `  M
) : ( N  X.  N ) --> K )
8685ad2antrr 730 . . . . . . . . 9  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  b  e.  d )  ->  ( J `  M ) : ( N  X.  N ) --> K )
8754ad2antrr 730 . . . . . . . . 9  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  b  e.  d )  ->  L  e.  N )
8886, 73, 87fovrnd 6451 . . . . . . . 8  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  b  e.  d )  ->  ( b
( J `  M
) L )  e.  K )
89 madugsum.t . . . . . . . . 9  |-  .x.  =  ( .r `  R )
9040, 89ringcl 17779 . . . . . . . 8  |-  ( ( R  e.  Ring  /\  [_ b  /  i ]_ X  e.  K  /\  (
b ( J `  M ) L )  e.  K )  -> 
( [_ b  /  i ]_ X  .x.  ( b ( J `  M
) L ) )  e.  K )
9172, 78, 88, 90syl3anc 1264 . . . . . . 7  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  b  e.  d )  ->  ( [_ b  /  i ]_ X  .x.  ( b ( J `
 M ) L ) )  e.  K
)
92 vex 3084 . . . . . . . 8  |-  e  e. 
_V
9392a1i 11 . . . . . . 7  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
e  e.  _V )
94 eldifn 3588 . . . . . . . 8  |-  ( e  e.  ( N  \ 
d )  ->  -.  e  e.  d )
9594ad2antll 733 . . . . . . 7  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  ->  -.  e  e.  d
)
96 eldifi 3587 . . . . . . . . . 10  |-  ( e  e.  ( N  \ 
d )  ->  e  e.  N )
9796ad2antll 733 . . . . . . . . 9  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
e  e.  N )
9875adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  ->  A. i  e.  N  X  e.  K )
99 rspcsbela 3823 . . . . . . . . 9  |-  ( ( e  e.  N  /\  A. i  e.  N  X  e.  K )  ->  [_ e  /  i ]_ X  e.  K )
10097, 98, 99syl2anc 665 . . . . . . . 8  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  ->  [_ e  /  i ]_ X  e.  K
)
10185adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
( J `  M
) : ( N  X.  N ) --> K )
10254adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  ->  L  e.  N )
103101, 97, 102fovrnd 6451 . . . . . . . 8  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
( e ( J `
 M ) L )  e.  K )
10440, 89ringcl 17779 . . . . . . . 8  |-  ( ( R  e.  Ring  /\  [_ e  /  i ]_ X  e.  K  /\  (
e ( J `  M ) L )  e.  K )  -> 
( [_ e  /  i ]_ X  .x.  ( e ( J `  M
) L ) )  e.  K )
10565, 100, 103, 104syl3anc 1264 . . . . . . 7  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
( [_ e  /  i ]_ X  .x.  ( e ( J `  M
) L ) )  e.  K )
106 csbeq1 3398 . . . . . . . 8  |-  ( b  =  e  ->  [_ b  /  i ]_ X  =  [_ e  /  i ]_ X )
107 oveq1 6308 . . . . . . . 8  |-  ( b  =  e  ->  (
b ( J `  M ) L )  =  ( e ( J `  M ) L ) )
108106, 107oveq12d 6319 . . . . . . 7  |-  ( b  =  e  ->  ( [_ b  /  i ]_ X  .x.  ( b ( J `  M
) L ) )  =  ( [_ e  /  i ]_ X  .x.  ( e ( J `
 M ) L ) ) )
10940, 62, 67, 71, 91, 93, 95, 105, 108gsumunsn 17577 . . . . . 6  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
( R  gsumg  ( b  e.  ( d  u.  { e } )  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `
 M ) L ) ) ) )  =  ( ( R 
gsumg  ( b  e.  d 
|->  ( [_ b  / 
i ]_ X  .x.  (
b ( J `  M ) L ) ) ) ) ( +g  `  R ) ( [_ e  / 
i ]_ X  .x.  (
e ( J `  M ) L ) ) ) )
110109adantr 466 . . . . 5  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  ( R  gsumg  ( b  e.  d  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `
 M ) L ) ) ) )  =  ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  d , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) ) ,  ( a M b ) ) ) ) )  ->  ( R  gsumg  ( b  e.  ( d  u.  { e } )  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `
 M ) L ) ) ) )  =  ( ( R 
gsumg  ( b  e.  d 
|->  ( [_ b  / 
i ]_ X  .x.  (
b ( J `  M ) L ) ) ) ) ( +g  `  R ) ( [_ e  / 
i ]_ X  .x.  (
e ( J `  M ) L ) ) ) )
111 oveq1 6308 . . . . . 6  |-  ( ( R  gsumg  ( b  e.  d 
|->  ( [_ b  / 
i ]_ X  .x.  (
b ( J `  M ) L ) ) ) )  =  ( D `  (
a  e.  N , 
b  e.  N  |->  if ( a  =  L ,  if ( b  e.  d ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) )  ->  ( ( R 
gsumg  ( b  e.  d 
|->  ( [_ b  / 
i ]_ X  .x.  (
b ( J `  M ) L ) ) ) ) ( +g  `  R ) ( [_ e  / 
i ]_ X  .x.  (
e ( J `  M ) L ) ) )  =  ( ( D `  (
a  e.  N , 
b  e.  N  |->  if ( a  =  L ,  if ( b  e.  d ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) ) ( +g  `  R
) ( [_ e  /  i ]_ X  .x.  ( e ( J `
 M ) L ) ) ) )
112111adantl 467 . . . . 5  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  ( R  gsumg  ( b  e.  d  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `
 M ) L ) ) ) )  =  ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  d , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) ) ,  ( a M b ) ) ) ) )  ->  (
( R  gsumg  ( b  e.  d 
|->  ( [_ b  / 
i ]_ X  .x.  (
b ( J `  M ) L ) ) ) ) ( +g  `  R ) ( [_ e  / 
i ]_ X  .x.  (
e ( J `  M ) L ) ) )  =  ( ( D `  (
a  e.  N , 
b  e.  N  |->  if ( a  =  L ,  if ( b  e.  d ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) ) ( +g  `  R
) ( [_ e  /  i ]_ X  .x.  ( e ( J `
 M ) L ) ) ) )
113 elun 3606 . . . . . . . . . . . . . 14  |-  ( b  e.  ( d  u. 
{ e } )  <-> 
( b  e.  d  \/  b  e.  {
e } ) )
114 elsn 4010 . . . . . . . . . . . . . . 15  |-  ( b  e.  { e }  <-> 
b  =  e )
115114orbi2i 521 . . . . . . . . . . . . . 14  |-  ( ( b  e.  d  \/  b  e.  { e } )  <->  ( b  e.  d  \/  b  =  e ) )
116113, 115bitri 252 . . . . . . . . . . . . 13  |-  ( b  e.  ( d  u. 
{ e } )  <-> 
( b  e.  d  \/  b  =  e ) )
117 ifbi 3930 . . . . . . . . . . . . 13  |-  ( ( b  e.  ( d  u.  { e } )  <->  ( b  e.  d  \/  b  =  e ) )  ->  if ( b  e.  ( d  u.  { e } ) ,  [_ b  /  i ]_ X ,  ( 0g `  R ) )  =  if ( ( b  e.  d  \/  b  =  e ) , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) ) )
118116, 117ax-mp 5 . . . . . . . . . . . 12  |-  if ( b  e.  ( d  u.  { e } ) ,  [_ b  /  i ]_ X ,  ( 0g `  R ) )  =  if ( ( b  e.  d  \/  b  =  e ) , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) )
119 ringmnd 17774 . . . . . . . . . . . . . . 15  |-  ( R  e.  Ring  ->  R  e. 
Mnd )
12065, 119syl 17 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  ->  R  e.  Mnd )
1211203ad2ant1 1026 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  a  e.  N  /\  b  e.  N
)  ->  R  e.  Mnd )
122 simp3 1007 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  a  e.  N  /\  b  e.  N
)  ->  b  e.  N )
123983ad2ant1 1026 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  a  e.  N  /\  b  e.  N
)  ->  A. i  e.  N  X  e.  K )
124122, 123, 77syl2anc 665 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  a  e.  N  /\  b  e.  N
)  ->  [_ b  / 
i ]_ X  e.  K
)
125 elequ1 1871 . . . . . . . . . . . . . . . 16  |-  ( b  =  e  ->  (
b  e.  d  <->  e  e.  d ) )
126125biimpac 488 . . . . . . . . . . . . . . 15  |-  ( ( b  e.  d  /\  b  =  e )  ->  e  e.  d )
12795, 126nsyl 124 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  ->  -.  ( b  e.  d  /\  b  =  e ) )
1281273ad2ant1 1026 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  a  e.  N  /\  b  e.  N
)  ->  -.  (
b  e.  d  /\  b  =  e )
)
12940, 41, 62mndifsplit 19645 . . . . . . . . . . . . 13  |-  ( ( R  e.  Mnd  /\  [_ b  /  i ]_ X  e.  K  /\  -.  ( b  e.  d  /\  b  =  e ) )  ->  if ( ( b  e.  d  \/  b  =  e ) ,  [_ b  /  i ]_ X ,  ( 0g `  R ) )  =  ( if ( b  e.  d ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ( +g  `  R ) if ( b  =  e ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ) )
130121, 124, 128, 129syl3anc 1264 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  a  e.  N  /\  b  e.  N
)  ->  if (
( b  e.  d  \/  b  =  e ) ,  [_ b  /  i ]_ X ,  ( 0g `  R ) )  =  ( if ( b  e.  d ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ( +g  `  R ) if ( b  =  e ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ) )
131118, 130syl5eq 2475 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  a  e.  N  /\  b  e.  N
)  ->  if (
b  e.  ( d  u.  { e } ) ,  [_ b  /  i ]_ X ,  ( 0g `  R ) )  =  ( if ( b  e.  d ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ( +g  `  R ) if ( b  =  e ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ) )
132106adantl 467 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  b  =  e )  ->  [_ b  / 
i ]_ X  =  [_ e  /  i ]_ X
)
133132ifeq1da 3939 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  ->  if ( b  =  e ,  [_ b  / 
i ]_ X ,  ( 0g `  R ) )  =  if ( b  =  e , 
[_ e  /  i ]_ X ,  ( 0g
`  R ) ) )
134 ovif2 6384 . . . . . . . . . . . . . . 15  |-  ( [_ e  /  i ]_ X  .x.  if ( b  =  e ,  ( 1r
`  R ) ,  ( 0g `  R
) ) )  =  if ( b  =  e ,  ( [_ e  /  i ]_ X  .x.  ( 1r `  R
) ) ,  (
[_ e  /  i ]_ X  .x.  ( 0g
`  R ) ) )
135 eqid 2422 . . . . . . . . . . . . . . . . . 18  |-  ( 1r
`  R )  =  ( 1r `  R
)
13640, 89, 135ringridm 17790 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  Ring  /\  [_ e  /  i ]_ X  e.  K )  ->  ( [_ e  /  i ]_ X  .x.  ( 1r
`  R ) )  =  [_ e  / 
i ]_ X )
13765, 100, 136syl2anc 665 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
( [_ e  /  i ]_ X  .x.  ( 1r
`  R ) )  =  [_ e  / 
i ]_ X )
13840, 89, 41ringrz 17803 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  Ring  /\  [_ e  /  i ]_ X  e.  K )  ->  ( [_ e  /  i ]_ X  .x.  ( 0g
`  R ) )  =  ( 0g `  R ) )
13965, 100, 138syl2anc 665 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
( [_ e  /  i ]_ X  .x.  ( 0g
`  R ) )  =  ( 0g `  R ) )
140137, 139ifeq12d 3929 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  ->  if ( b  =  e ,  ( [_ e  /  i ]_ X  .x.  ( 1r `  R
) ) ,  (
[_ e  /  i ]_ X  .x.  ( 0g
`  R ) ) )  =  if ( b  =  e , 
[_ e  /  i ]_ X ,  ( 0g
`  R ) ) )
141134, 140syl5eq 2475 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
( [_ e  /  i ]_ X  .x.  if ( b  =  e ,  ( 1r `  R
) ,  ( 0g
`  R ) ) )  =  if ( b  =  e , 
[_ e  /  i ]_ X ,  ( 0g
`  R ) ) )
142133, 141eqtr4d 2466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  ->  if ( b  =  e ,  [_ b  / 
i ]_ X ,  ( 0g `  R ) )  =  ( [_ e  /  i ]_ X  .x.  if ( b  =  e ,  ( 1r
`  R ) ,  ( 0g `  R
) ) ) )
143142oveq2d 6317 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
( if ( b  e.  d ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ( +g  `  R ) if ( b  =  e ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) )  =  ( if ( b  e.  d , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) ) ( +g  `  R
) ( [_ e  /  i ]_ X  .x.  if ( b  =  e ,  ( 1r
`  R ) ,  ( 0g `  R
) ) ) ) )
1441433ad2ant1 1026 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  a  e.  N  /\  b  e.  N
)  ->  ( if ( b  e.  d ,  [_ b  / 
i ]_ X ,  ( 0g `  R ) ) ( +g  `  R
) if ( b  =  e ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) )  =  ( if ( b  e.  d , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) ) ( +g  `  R
) ( [_ e  /  i ]_ X  .x.  if ( b  =  e ,  ( 1r
`  R ) ,  ( 0g `  R
) ) ) ) )
145131, 144eqtrd 2463 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  a  e.  N  /\  b  e.  N
)  ->  if (
b  e.  ( d  u.  { e } ) ,  [_ b  /  i ]_ X ,  ( 0g `  R ) )  =  ( if ( b  e.  d ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ( +g  `  R ) ( [_ e  / 
i ]_ X  .x.  if ( b  =  e ,  ( 1r `  R ) ,  ( 0g `  R ) ) ) ) )
146145ifeq1d 3927 . . . . . . . . 9  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  a  e.  N  /\  b  e.  N
)  ->  if (
a  =  L ,  if ( b  e.  ( d  u.  { e } ) ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) )  =  if ( a  =  L ,  ( if ( b  e.  d , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) ) ( +g  `  R
) ( [_ e  /  i ]_ X  .x.  if ( b  =  e ,  ( 1r
`  R ) ,  ( 0g `  R
) ) ) ) ,  ( a M b ) ) )
147146mpt2eq3dva 6365 . . . . . . . 8  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  ( d  u.  { e } ) ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) )  =  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  ( if ( b  e.  d ,  [_ b  / 
i ]_ X ,  ( 0g `  R ) ) ( +g  `  R
) ( [_ e  /  i ]_ X  .x.  if ( b  =  e ,  ( 1r
`  R ) ,  ( 0g `  R
) ) ) ) ,  ( a M b ) ) ) )
148147fveq2d 5881 . . . . . . 7  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
( D `  (
a  e.  N , 
b  e.  N  |->  if ( a  =  L ,  if ( b  e.  ( d  u. 
{ e } ) ,  [_ b  / 
i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) )  =  ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L , 
( if ( b  e.  d ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ( +g  `  R ) ( [_ e  / 
i ]_ X  .x.  if ( b  =  e ,  ( 1r `  R ) ,  ( 0g `  R ) ) ) ) ,  ( a M b ) ) ) ) )
14940, 41ring0cl 17787 . . . . . . . . . . 11  |-  ( R  e.  Ring  ->  ( 0g
`  R )  e.  K )
15065, 149syl 17 . . . . . . . . . 10  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
( 0g `  R
)  e.  K )
1511503ad2ant1 1026 . . . . . . . . 9  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  a  e.  N  /\  b  e.  N
)  ->  ( 0g `  R )  e.  K
)
152124, 151ifcld 3952 . . . . . . . 8  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  a  e.  N  /\  b  e.  N
)  ->  if (
b  e.  d , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) )  e.  K )
15340, 135ringidcl 17786 . . . . . . . . . . . 12  |-  ( R  e.  Ring  ->  ( 1r
`  R )  e.  K )
15465, 153syl 17 . . . . . . . . . . 11  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
( 1r `  R
)  e.  K )
155154, 150ifcld 3952 . . . . . . . . . 10  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  ->  if ( b  =  e ,  ( 1r `  R ) ,  ( 0g `  R ) )  e.  K )
15640, 89ringcl 17779 . . . . . . . . . 10  |-  ( ( R  e.  Ring  /\  [_ e  /  i ]_ X  e.  K  /\  if ( b  =  e ,  ( 1r `  R
) ,  ( 0g
`  R ) )  e.  K )  -> 
( [_ e  /  i ]_ X  .x.  if ( b  =  e ,  ( 1r `  R
) ,  ( 0g
`  R ) ) )  e.  K )
15765, 100, 155, 156syl3anc 1264 . . . . . . . . 9  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
( [_ e  /  i ]_ X  .x.  if ( b  =  e ,  ( 1r `  R
) ,  ( 0g
`  R ) ) )  e.  K )
1581573ad2ant1 1026 . . . . . . . 8  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  a  e.  N  /\  b  e.  N
)  ->  ( [_ e  /  i ]_ X  .x.  if ( b  =  e ,  ( 1r
`  R ) ,  ( 0g `  R
) ) )  e.  K )
15951adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  ->  M : ( N  X.  N ) --> K )
160159fovrnda 6450 . . . . . . . . 9  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  ( a  e.  N  /\  b  e.  N ) )  -> 
( a M b )  e.  K )
1611603impb 1201 . . . . . . . 8  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  a  e.  N  /\  b  e.  N
)  ->  ( a M b )  e.  K )
16239, 40, 62, 63, 68, 152, 158, 161, 102mdetrlin2 19616 . . . . . . 7  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
( D `  (
a  e.  N , 
b  e.  N  |->  if ( a  =  L ,  ( if ( b  e.  d , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) ) ( +g  `  R
) ( [_ e  /  i ]_ X  .x.  if ( b  =  e ,  ( 1r
`  R ) ,  ( 0g `  R
) ) ) ) ,  ( a M b ) ) ) )  =  ( ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  d ,  [_ b  / 
i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) ) ( +g  `  R ) ( D `
 ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  (
[_ e  /  i ]_ X  .x.  if ( b  =  e ,  ( 1r `  R
) ,  ( 0g
`  R ) ) ) ,  ( a M b ) ) ) ) ) )
1631553ad2ant1 1026 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  a  e.  N  /\  b  e.  N
)  ->  if (
b  =  e ,  ( 1r `  R
) ,  ( 0g
`  R ) )  e.  K )
16439, 40, 89, 63, 68, 163, 161, 100, 102mdetrsca2 19613 . . . . . . . . 9  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
( D `  (
a  e.  N , 
b  e.  N  |->  if ( a  =  L ,  ( [_ e  /  i ]_ X  .x.  if ( b  =  e ,  ( 1r
`  R ) ,  ( 0g `  R
) ) ) ,  ( a M b ) ) ) )  =  ( [_ e  /  i ]_ X  .x.  ( D `  (
a  e.  N , 
b  e.  N  |->  if ( a  =  L ,  if ( b  =  e ,  ( 1r `  R ) ,  ( 0g `  R ) ) ,  ( a M b ) ) ) ) ) )
16543adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  ->  M  e.  B )
16644, 39, 79, 45, 135, 41maducoeval 19648 . . . . . . . . . . 11  |-  ( ( M  e.  B  /\  e  e.  N  /\  L  e.  N )  ->  ( e ( J `
 M ) L )  =  ( D `
 ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  =  e ,  ( 1r `  R ) ,  ( 0g `  R ) ) ,  ( a M b ) ) ) ) )
167165, 97, 102, 166syl3anc 1264 . . . . . . . . . 10  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
( e ( J `
 M ) L )  =  ( D `
 ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  =  e ,  ( 1r `  R ) ,  ( 0g `  R ) ) ,  ( a M b ) ) ) ) )
168167oveq2d 6317 . . . . . . . . 9  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
( [_ e  /  i ]_ X  .x.  ( e ( J `  M
) L ) )  =  ( [_ e  /  i ]_ X  .x.  ( D `  (
a  e.  N , 
b  e.  N  |->  if ( a  =  L ,  if ( b  =  e ,  ( 1r `  R ) ,  ( 0g `  R ) ) ,  ( a M b ) ) ) ) ) )
169164, 168eqtr4d 2466 . . . . . . . 8  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
( D `  (
a  e.  N , 
b  e.  N  |->  if ( a  =  L ,  ( [_ e  /  i ]_ X  .x.  if ( b  =  e ,  ( 1r
`  R ) ,  ( 0g `  R
) ) ) ,  ( a M b ) ) ) )  =  ( [_ e  /  i ]_ X  .x.  ( e ( J `
 M ) L ) ) )
170169oveq2d 6317 . . . . . . 7  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
( ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  d , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) ) ,  ( a M b ) ) ) ) ( +g  `  R
) ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  ( [_ e  /  i ]_ X  .x.  if ( b  =  e ,  ( 1r
`  R ) ,  ( 0g `  R
) ) ) ,  ( a M b ) ) ) ) )  =  ( ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  d ,  [_ b  / 
i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) ) ( +g  `  R ) ( [_ e  /  i ]_ X  .x.  ( e ( J `
 M ) L ) ) ) )
171148, 162, 1703eqtrrd 2468 . . . . . 6  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
( ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  d , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) ) ,  ( a M b ) ) ) ) ( +g  `  R
) ( [_ e  /  i ]_ X  .x.  ( e ( J `
 M ) L ) ) )  =  ( D `  (
a  e.  N , 
b  e.  N  |->  if ( a  =  L ,  if ( b  e.  ( d  u. 
{ e } ) ,  [_ b  / 
i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) ) )
172171adantr 466 . . . . 5  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  ( R  gsumg  ( b  e.  d  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `
 M ) L ) ) ) )  =  ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  d , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) ) ,  ( a M b ) ) ) ) )  ->  (
( D `  (
a  e.  N , 
b  e.  N  |->  if ( a  =  L ,  if ( b  e.  d ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) ) ( +g  `  R
) ( [_ e  /  i ]_ X  .x.  ( e ( J `
 M ) L ) ) )  =  ( D `  (
a  e.  N , 
b  e.  N  |->  if ( a  =  L ,  if ( b  e.  ( d  u. 
{ e } ) ,  [_ b  / 
i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) ) )
173110, 112, 1723eqtrd 2467 . . . 4  |-  ( ( ( ph  /\  (
d  C_  N  /\  e  e.  ( N  \  d ) ) )  /\  ( R  gsumg  ( b  e.  d  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `
 M ) L ) ) ) )  =  ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  d , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) ) ,  ( a M b ) ) ) ) )  ->  ( R  gsumg  ( b  e.  ( d  u.  { e } )  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `
 M ) L ) ) ) )  =  ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  ( d  u.  { e } ) ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) ) )
174173ex 435 . . 3  |-  ( (
ph  /\  ( d  C_  N  /\  e  e.  ( N  \  d
) ) )  -> 
( ( R  gsumg  ( b  e.  d  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `
 M ) L ) ) ) )  =  ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  d , 
[_ b  /  i ]_ X ,  ( 0g
`  R ) ) ,  ( a M b ) ) ) )  ->  ( R  gsumg  ( b  e.  ( d  u.  { e } )  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `
 M ) L ) ) ) )  =  ( D `  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  ( d  u.  { e } ) ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) ) ) )
1758, 16, 24, 32, 61, 174, 48findcard2d 7815 . 2  |-  ( ph  ->  ( R  gsumg  ( b  e.  N  |->  ( [_ b  / 
i ]_ X  .x.  (
b ( J `  M ) L ) ) ) )  =  ( D `  (
a  e.  N , 
b  e.  N  |->  if ( a  =  L ,  if ( b  e.  N ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) ,  ( a M b ) ) ) ) )
176 nfcv 2584 . . . 4  |-  F/_ b
( X  .x.  (
i ( J `  M ) L ) )
177 nfcsb1v 3411 . . . . 5  |-  F/_ i [_ b  /  i ]_ X
178 nfcv 2584 . . . . 5  |-  F/_ i  .x.
179 nfcv 2584 . . . . 5  |-  F/_ i
( b ( J `
 M ) L )
180177, 178, 179nfov 6327 . . . 4  |-  F/_ i
( [_ b  /  i ]_ X  .x.  ( b ( J `  M
) L ) )
181 csbeq1a 3404 . . . . 5  |-  ( i  =  b  ->  X  =  [_ b  /  i ]_ X )
182 oveq1 6308 . . . . 5  |-  ( i  =  b  ->  (
i ( J `  M ) L )  =  ( b ( J `  M ) L ) )
183181, 182oveq12d 6319 . . . 4  |-  ( i  =  b  ->  ( X  .x.  ( i ( J `  M ) L ) )  =  ( [_ b  / 
i ]_ X  .x.  (
b ( J `  M ) L ) ) )
184176, 180, 183cbvmpt 4512 . . 3  |-  ( i  e.  N  |->  ( X 
.x.  ( i ( J `  M ) L ) ) )  =  ( b  e.  N  |->  ( [_ b  /  i ]_ X  .x.  ( b ( J `
 M ) L ) ) )
185184oveq2i 6312 . 2  |-  ( R 
gsumg  ( i  e.  N  |->  ( X  .x.  (
i ( J `  M ) L ) ) ) )  =  ( R  gsumg  ( b  e.  N  |->  ( [_ b  / 
i ]_ X  .x.  (
b ( J `  M ) L ) ) ) )
186 nfcv 2584 . . . . 5  |-  F/_ a if ( j  =  L ,  X ,  ( j M i ) )
187 nfcv 2584 . . . . 5  |-  F/_ b if ( j  =  L ,  X ,  ( j M i ) )
188 nfcv 2584 . . . . 5  |-  F/_ j if ( a  =  L ,  [_ b  / 
i ]_ X ,  ( a M b ) )
189 nfv 1751 . . . . . 6  |-  F/ i  a  =  L
190 nfcv 2584 . . . . . 6  |-  F/_ i
( a M b )
191189, 177, 190nfif 3938 . . . . 5  |-  F/_ i if ( a  =  L ,  [_ b  / 
i ]_ X ,  ( a M b ) )
192 eqeq1 2426 . . . . . . 7  |-  ( j  =  a  ->  (
j  =  L  <->  a  =  L ) )
193192adantr 466 . . . . . 6  |-  ( ( j  =  a  /\  i  =  b )  ->  ( j  =  L  <-> 
a  =  L ) )
194181adantl 467 . . . . . 6  |-  ( ( j  =  a  /\  i  =  b )  ->  X  =  [_ b  /  i ]_ X
)
195 oveq12 6310 . . . . . 6  |-  ( ( j  =  a  /\  i  =  b )  ->  ( j M i )  =  ( a M b ) )
196193, 194, 195ifbieq12d 3936 . . . . 5  |-  ( ( j  =  a  /\  i  =  b )  ->  if ( j  =  L ,  X , 
( j M i ) )  =  if ( a  =  L ,  [_ b  / 
i ]_ X ,  ( a M b ) ) )
197186, 187, 188, 191, 196cbvmpt2 6380 . . . 4  |-  ( j  e.  N ,  i  e.  N  |->  if ( j  =  L ,  X ,  ( j M i ) ) )  =  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  [_ b  /  i ]_ X ,  ( a M b ) ) )
198 iftrue 3915 . . . . . . . 8  |-  ( b  e.  N  ->  if ( b  e.  N ,  [_ b  /  i ]_ X ,  ( 0g
`  R ) )  =  [_ b  / 
i ]_ X )
199198eqcomd 2430 . . . . . . 7  |-  ( b  e.  N  ->  [_ b  /  i ]_ X  =  if ( b  e.  N ,  [_ b  /  i ]_ X ,  ( 0g `  R ) ) )
200199adantl 467 . . . . . 6  |-  ( ( a  e.  N  /\  b  e.  N )  ->  [_ b  /  i ]_ X  =  if ( b  e.  N ,  [_ b  /  i ]_ X ,  ( 0g
`  R ) ) )
201200ifeq1d 3927 . . . . 5  |-  ( ( a  e.  N  /\  b  e.  N )  ->  if ( a  =  L ,  [_ b  /  i ]_ X ,  ( a M b ) )  =  if ( a  =  L ,  if ( b  e.  N ,  [_ b  /  i ]_ X ,  ( 0g
`  R ) ) ,  ( a M b ) ) )
202201mpt2eq3ia 6366 . . . 4  |-  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  [_ b  /  i ]_ X ,  ( a M b ) ) )  =  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  N ,  [_ b  /  i ]_ X ,  ( 0g
`  R ) ) ,  ( a M b ) ) )
203197, 202eqtri 2451 . . 3  |-  ( j  e.  N ,  i  e.  N  |->  if ( j  =  L ,  X ,  ( j M i ) ) )  =  ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  N ,  [_ b  /  i ]_ X ,  ( 0g
`  R ) ) ,  ( a M b ) ) )
204203fveq2i 5880 . 2  |-  ( D `
 ( j  e.  N ,  i  e.  N  |->  if ( j  =  L ,  X ,  ( j M i ) ) ) )  =  ( D `
 ( a  e.  N ,  b  e.  N  |->  if ( a  =  L ,  if ( b  e.  N ,  [_ b  /  i ]_ X ,  ( 0g
`  R ) ) ,  ( a M b ) ) ) )
205175, 185, 2043eqtr4g 2488 1  |-  ( ph  ->  ( R  gsumg  ( i  e.  N  |->  ( X  .x.  (
i ( J `  M ) L ) ) ) )  =  ( D `  (
j  e.  N , 
i  e.  N  |->  if ( j  =  L ,  X ,  ( j M i ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1868   A.wral 2775   _Vcvv 3081   [_csb 3395    \ cdif 3433    u. cun 3434    C_ wss 3436   (/)c0 3761   ifcif 3909   {csn 3996    |-> cmpt 4479    X. cxp 4847   -->wf 5593   ` cfv 5597  (class class class)co 6301    |-> cmpt2 6303    ^m cmap 7476   Fincfn 7573   Basecbs 15106   +g cplusg 15175   .rcmulr 15176   0gc0g 15323    gsumg cgsu 15324   Mndcmnd 16520  CMndccmn 17415   1rcur 17720   Ringcrg 17765   CRingccrg 17766   Mat cmat 19416   maDet cmdat 19593   maAdju cmadu 19641
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-inf2 8148  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616  ax-addf 9618  ax-mulf 9619
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-xor 1401  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-ot 4005  df-uni 4217  df-int 4253  df-iun 4298  df-iin 4299  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-se 4809  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-isom 5606  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-of 6541  df-om 6703  df-1st 6803  df-2nd 6804  df-supp 6922  df-tpos 6977  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-1o 7186  df-2o 7187  df-oadd 7190  df-er 7367  df-map 7478  df-pm 7479  df-ixp 7527  df-en 7574  df-dom 7575  df-sdom 7576  df-fin 7577  df-fsupp 7886  df-sup 7958  df-oi 8027  df-card 8374  df-cda 8598  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-div 10270  df-nn 10610  df-2 10668  df-3 10669  df-4 10670  df-5 10671  df-6 10672  df-7 10673  df-8 10674  df-9 10675  df-10 10676  df-n0 10870  df-z 10938  df-dec 11052  df-uz 11160  df-rp 11303  df-fz 11785  df-fzo 11916  df-seq 12213  df-exp 12272  df-hash 12515  df-word 12654  df-lsw 12655  df-concat 12656  df-s1 12657  df-substr 12658  df-splice 12659  df-reverse 12660  df-s2 12932  df-struct 15108  df-ndx 15109  df-slot 15110  df-base 15111  df-sets 15112  df-ress 15113  df-plusg 15188  df-mulr 15189  df-starv 15190  df-sca 15191  df-vsca 15192  df-ip 15193  df-tset 15194  df-ple 15195  df-ds 15197  df-unif 15198  df-hom 15199  df-cco 15200  df-0g 15325  df-gsum 15326  df-prds 15331  df-pws 15333  df-mre 15477  df-mrc 15478  df-acs 15480  df-mgm 16473  df-sgrp 16512  df-mnd 16522  df-mhm 16567  df-submnd 16568  df-grp 16658  df-minusg 16659  df-mulg 16661  df-subg 16799  df-ghm 16866  df-gim 16908  df-cntz 16956  df-oppg 16982  df-symg 17004  df-pmtr 17068  df-psgn 17117  df-cmn 17417  df-abl 17418  df-mgp 17709  df-ur 17721  df-ring 17767  df-cring 17768  df-oppr 17836  df-dvdsr 17854  df-unit 17855  df-invr 17885  df-dvr 17896  df-rnghom 17928  df-drng 17962  df-subrg 17991  df-sra 18380  df-rgmod 18381  df-cnfld 18956  df-zring 19024  df-zrh 19059  df-dsmm 19279  df-frlm 19294  df-mat 19417  df-mdet 19594  df-madu 19643
This theorem is referenced by:  madurid  19653  mdetlap1  28645
  Copyright terms: Public domain W3C validator