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

Theorem mplcoe1 18449
Description: Decompose a polynomial into a finite sum of monomials. (Contributed by Mario Carneiro, 9-Jan-2015.)
Hypotheses
Ref Expression
mplcoe1.p  |-  P  =  ( I mPoly  R )
mplcoe1.d  |-  D  =  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin }
mplcoe1.z  |-  .0.  =  ( 0g `  R )
mplcoe1.o  |-  .1.  =  ( 1r `  R )
mplcoe1.i  |-  ( ph  ->  I  e.  W )
mplcoe1.b  |-  B  =  ( Base `  P
)
mplcoe1.n  |-  .x.  =  ( .s `  P )
mplcoe1.r  |-  ( ph  ->  R  e.  Ring )
mplcoe1.x  |-  ( ph  ->  X  e.  B )
Assertion
Ref Expression
mplcoe1  |-  ( ph  ->  X  =  ( P 
gsumg  ( k  e.  D  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) ) )
Distinct variable groups:    y, k,  .1.    B, k    f, k, y, I    ph, k,
y    R, f, y    D, k, y    P, k    .0. , f, k, y    f, X, k, y    k, W, y    .x. , k
Allowed substitution hints:    ph( f)    B( y, f)    D( f)    P( y, f)    R( k)    .x. ( y,
f)    .1. ( f)    W( f)

Proof of Theorem mplcoe1
Dummy variables  w  x  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mplcoe1.p . . . . . 6  |-  P  =  ( I mPoly  R )
2 eqid 2404 . . . . . 6  |-  ( Base `  R )  =  (
Base `  R )
3 mplcoe1.b . . . . . 6  |-  B  =  ( Base `  P
)
4 mplcoe1.d . . . . . 6  |-  D  =  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin }
5 mplcoe1.x . . . . . 6  |-  ( ph  ->  X  e.  B )
61, 2, 3, 4, 5mplelf 18414 . . . . 5  |-  ( ph  ->  X : D --> ( Base `  R ) )
76feqmptd 5904 . . . 4  |-  ( ph  ->  X  =  ( y  e.  D  |->  ( X `
 y ) ) )
8 iftrue 3893 . . . . . . 7  |-  ( y  e.  ( X supp  .0.  )  ->  if ( y  e.  ( X supp  .0.  ) ,  ( X `  y ) ,  .0.  )  =  ( X `  y ) )
98adantl 466 . . . . . 6  |-  ( ( ( ph  /\  y  e.  D )  /\  y  e.  ( X supp  .0.  )
)  ->  if (
y  e.  ( X supp 
.0.  ) ,  ( X `  y ) ,  .0.  )  =  ( X `  y
) )
10 eldif 3426 . . . . . . . 8  |-  ( y  e.  ( D  \ 
( X supp  .0.  )
)  <->  ( y  e.  D  /\  -.  y  e.  ( X supp  .0.  )
) )
11 ifid 3924 . . . . . . . . 9  |-  if ( y  e.  ( X supp 
.0.  ) ,  ( X `  y ) ,  ( X `  y ) )  =  ( X `  y
)
12 ssid 3463 . . . . . . . . . . . 12  |-  ( X supp 
.0.  )  C_  ( X supp  .0.  )
1312a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  ( X supp  .0.  )  C_  ( X supp  .0.  )
)
14 ovex 6308 . . . . . . . . . . . . 13  |-  ( NN0 
^m  I )  e. 
_V
154, 14rabex2 4549 . . . . . . . . . . . 12  |-  D  e. 
_V
1615a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  D  e.  _V )
17 mplcoe1.z . . . . . . . . . . . . 13  |-  .0.  =  ( 0g `  R )
18 fvex 5861 . . . . . . . . . . . . 13  |-  ( 0g
`  R )  e. 
_V
1917, 18eqeltri 2488 . . . . . . . . . . . 12  |-  .0.  e.  _V
2019a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  .0.  e.  _V )
216, 13, 16, 20suppssr 6936 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( D  \  ( X supp  .0.  ) ) )  ->  ( X `  y )  =  .0.  )
2221ifeq2d 3906 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( D  \  ( X supp  .0.  ) ) )  ->  if ( y  e.  ( X supp  .0.  ) ,  ( X `  y ) ,  ( X `  y ) )  =  if ( y  e.  ( X supp 
.0.  ) ,  ( X `  y ) ,  .0.  ) )
2311, 22syl5reqr 2460 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( D  \  ( X supp  .0.  ) ) )  ->  if ( y  e.  ( X supp  .0.  ) ,  ( X `  y ) ,  .0.  )  =  ( X `  y ) )
2410, 23sylan2br 476 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  D  /\  -.  y  e.  ( X supp  .0.  )
) )  ->  if ( y  e.  ( X supp  .0.  ) , 
( X `  y
) ,  .0.  )  =  ( X `  y ) )
2524anassrs 648 . . . . . 6  |-  ( ( ( ph  /\  y  e.  D )  /\  -.  y  e.  ( X supp  .0.  ) )  ->  if ( y  e.  ( X supp  .0.  ) , 
( X `  y
) ,  .0.  )  =  ( X `  y ) )
269, 25pm2.61dan 794 . . . . 5  |-  ( (
ph  /\  y  e.  D )  ->  if ( y  e.  ( X supp  .0.  ) , 
( X `  y
) ,  .0.  )  =  ( X `  y ) )
2726mpteq2dva 4483 . . . 4  |-  ( ph  ->  ( y  e.  D  |->  if ( y  e.  ( X supp  .0.  ) ,  ( X `  y ) ,  .0.  ) )  =  ( y  e.  D  |->  ( X `  y ) ) )
287, 27eqtr4d 2448 . . 3  |-  ( ph  ->  X  =  ( y  e.  D  |->  if ( y  e.  ( X supp 
.0.  ) ,  ( X `  y ) ,  .0.  ) ) )
29 suppssdm 6917 . . . . 5  |-  ( X supp 
.0.  )  C_  dom  X
30 fdm 5720 . . . . . 6  |-  ( X : D --> ( Base `  R )  ->  dom  X  =  D )
316, 30syl 17 . . . . 5  |-  ( ph  ->  dom  X  =  D )
3229, 31syl5sseq 3492 . . . 4  |-  ( ph  ->  ( X supp  .0.  )  C_  D )
33 eqid 2404 . . . . . . . . 9  |-  ( I mPwSer  R )  =  ( I mPwSer  R )
34 eqid 2404 . . . . . . . . 9  |-  ( Base `  ( I mPwSer  R ) )  =  ( Base `  ( I mPwSer  R ) )
351, 33, 34, 17, 3mplelbas 18409 . . . . . . . 8  |-  ( X  e.  B  <->  ( X  e.  ( Base `  (
I mPwSer  R ) )  /\  X finSupp  .0.  ) )
3635simprbi 464 . . . . . . 7  |-  ( X  e.  B  ->  X finSupp  .0.  )
375, 36syl 17 . . . . . 6  |-  ( ph  ->  X finSupp  .0.  )
3837fsuppimpd 7872 . . . . 5  |-  ( ph  ->  ( X supp  .0.  )  e.  Fin )
39 sseq1 3465 . . . . . . . 8  |-  ( w  =  (/)  ->  ( w 
C_  D  <->  (/)  C_  D
) )
40 mpteq1 4477 . . . . . . . . . . . 12  |-  ( w  =  (/)  ->  ( k  e.  w  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) )  =  ( k  e.  (/)  |->  ( ( X `
 k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )
41 mpt0 5693 . . . . . . . . . . . 12  |-  ( k  e.  (/)  |->  ( ( X `
 k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) )  =  (/)
4240, 41syl6eq 2461 . . . . . . . . . . 11  |-  ( w  =  (/)  ->  ( k  e.  w  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) )  =  (/) )
4342oveq2d 6296 . . . . . . . . . 10  |-  ( w  =  (/)  ->  ( P 
gsumg  ( k  e.  w  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( P 
gsumg  (/) ) )
44 eqid 2404 . . . . . . . . . . 11  |-  ( 0g
`  P )  =  ( 0g `  P
)
4544gsum0 16231 . . . . . . . . . 10  |-  ( P 
gsumg  (/) )  =  ( 0g
`  P )
4643, 45syl6eq 2461 . . . . . . . . 9  |-  ( w  =  (/)  ->  ( P 
gsumg  ( k  e.  w  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( 0g
`  P ) )
47 noel 3744 . . . . . . . . . . . 12  |-  -.  y  e.  (/)
48 eleq2 2477 . . . . . . . . . . . 12  |-  ( w  =  (/)  ->  ( y  e.  w  <->  y  e.  (/) ) )
4947, 48mtbiri 303 . . . . . . . . . . 11  |-  ( w  =  (/)  ->  -.  y  e.  w )
5049iffalsed 3898 . . . . . . . . . 10  |-  ( w  =  (/)  ->  if ( y  e.  w ,  ( X `  y
) ,  .0.  )  =  .0.  )
5150mpteq2dv 4484 . . . . . . . . 9  |-  ( w  =  (/)  ->  ( y  e.  D  |->  if ( y  e.  w ,  ( X `  y
) ,  .0.  )
)  =  ( y  e.  D  |->  .0.  )
)
5246, 51eqeq12d 2426 . . . . . . . 8  |-  ( w  =  (/)  ->  ( ( P  gsumg  ( k  e.  w  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  w ,  ( X `  y
) ,  .0.  )
)  <->  ( 0g `  P )  =  ( y  e.  D  |->  .0.  ) ) )
5339, 52imbi12d 320 . . . . . . 7  |-  ( w  =  (/)  ->  ( ( w  C_  D  ->  ( P  gsumg  ( k  e.  w  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  w ,  ( X `  y
) ,  .0.  )
) )  <->  ( (/)  C_  D  ->  ( 0g `  P
)  =  ( y  e.  D  |->  .0.  )
) ) )
5453imbi2d 316 . . . . . 6  |-  ( w  =  (/)  ->  ( (
ph  ->  ( w  C_  D  ->  ( P  gsumg  ( k  e.  w  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  w ,  ( X `  y ) ,  .0.  ) ) ) )  <-> 
( ph  ->  ( (/)  C_  D  ->  ( 0g `  P )  =  ( y  e.  D  |->  .0.  ) ) ) ) )
55 sseq1 3465 . . . . . . . 8  |-  ( w  =  x  ->  (
w  C_  D  <->  x  C_  D
) )
56 mpteq1 4477 . . . . . . . . . 10  |-  ( w  =  x  ->  (
k  e.  w  |->  ( ( X `  k
)  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  )
) ) )  =  ( k  e.  x  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )
5756oveq2d 6296 . . . . . . . . 9  |-  ( w  =  x  ->  ( P  gsumg  ( k  e.  w  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( P 
gsumg  ( k  e.  x  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) ) )
58 eleq2 2477 . . . . . . . . . . 11  |-  ( w  =  x  ->  (
y  e.  w  <->  y  e.  x ) )
5958ifbid 3909 . . . . . . . . . 10  |-  ( w  =  x  ->  if ( y  e.  w ,  ( X `  y ) ,  .0.  )  =  if (
y  e.  x ,  ( X `  y
) ,  .0.  )
)
6059mpteq2dv 4484 . . . . . . . . 9  |-  ( w  =  x  ->  (
y  e.  D  |->  if ( y  e.  w ,  ( X `  y ) ,  .0.  ) )  =  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) ) )
6157, 60eqeq12d 2426 . . . . . . . 8  |-  ( w  =  x  ->  (
( P  gsumg  ( k  e.  w  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  w ,  ( X `  y
) ,  .0.  )
)  <->  ( P  gsumg  ( k  e.  x  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) ) ) )
6255, 61imbi12d 320 . . . . . . 7  |-  ( w  =  x  ->  (
( w  C_  D  ->  ( P  gsumg  ( k  e.  w  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  w ,  ( X `  y
) ,  .0.  )
) )  <->  ( x  C_  D  ->  ( P  gsumg  ( k  e.  x  |->  ( ( X `  k
)  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  )
) ) ) )  =  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) ) ) ) )
6362imbi2d 316 . . . . . 6  |-  ( w  =  x  ->  (
( ph  ->  ( w 
C_  D  ->  ( P  gsumg  ( k  e.  w  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  w ,  ( X `  y
) ,  .0.  )
) ) )  <->  ( ph  ->  ( x  C_  D  ->  ( P  gsumg  ( k  e.  x  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y
) ,  .0.  )
) ) ) ) )
64 sseq1 3465 . . . . . . . 8  |-  ( w  =  ( x  u. 
{ z } )  ->  ( w  C_  D 
<->  ( x  u.  {
z } )  C_  D ) )
65 mpteq1 4477 . . . . . . . . . 10  |-  ( w  =  ( x  u. 
{ z } )  ->  ( k  e.  w  |->  ( ( X `
 k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) )  =  ( k  e.  ( x  u.  {
z } )  |->  ( ( X `  k
)  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  )
) ) ) )
6665oveq2d 6296 . . . . . . . . 9  |-  ( w  =  ( x  u. 
{ z } )  ->  ( P  gsumg  ( k  e.  w  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( P  gsumg  ( k  e.  ( x  u.  { z } )  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) ) )
67 eleq2 2477 . . . . . . . . . . 11  |-  ( w  =  ( x  u. 
{ z } )  ->  ( y  e.  w  <->  y  e.  ( x  u.  { z } ) ) )
6867ifbid 3909 . . . . . . . . . 10  |-  ( w  =  ( x  u. 
{ z } )  ->  if ( y  e.  w ,  ( X `  y ) ,  .0.  )  =  if ( y  e.  ( x  u.  {
z } ) ,  ( X `  y
) ,  .0.  )
)
6968mpteq2dv 4484 . . . . . . . . 9  |-  ( w  =  ( x  u. 
{ z } )  ->  ( y  e.  D  |->  if ( y  e.  w ,  ( X `  y ) ,  .0.  ) )  =  ( y  e.  D  |->  if ( y  e.  ( x  u. 
{ z } ) ,  ( X `  y ) ,  .0.  ) ) )
7066, 69eqeq12d 2426 . . . . . . . 8  |-  ( w  =  ( x  u. 
{ z } )  ->  ( ( P 
gsumg  ( k  e.  w  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  w ,  ( X `  y
) ,  .0.  )
)  <->  ( P  gsumg  ( k  e.  ( x  u. 
{ z } ) 
|->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  ( x  u.  { z } ) ,  ( X `
 y ) ,  .0.  ) ) ) )
7164, 70imbi12d 320 . . . . . . 7  |-  ( w  =  ( x  u. 
{ z } )  ->  ( ( w 
C_  D  ->  ( P  gsumg  ( k  e.  w  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  w ,  ( X `  y
) ,  .0.  )
) )  <->  ( (
x  u.  { z } )  C_  D  ->  ( P  gsumg  ( k  e.  ( x  u.  { z } )  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  ( x  u.  { z } ) ,  ( X `  y ) ,  .0.  ) ) ) ) )
7271imbi2d 316 . . . . . 6  |-  ( w  =  ( x  u. 
{ z } )  ->  ( ( ph  ->  ( w  C_  D  ->  ( P  gsumg  ( k  e.  w  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  w ,  ( X `  y
) ,  .0.  )
) ) )  <->  ( ph  ->  ( ( x  u. 
{ z } ) 
C_  D  ->  ( P  gsumg  ( k  e.  ( x  u.  { z } )  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  ( x  u.  { z } ) ,  ( X `  y ) ,  .0.  ) ) ) ) ) )
73 sseq1 3465 . . . . . . . 8  |-  ( w  =  ( X supp  .0.  )  ->  ( w  C_  D 
<->  ( X supp  .0.  )  C_  D ) )
74 mpteq1 4477 . . . . . . . . . 10  |-  ( w  =  ( X supp  .0.  )  ->  ( k  e.  w  |->  ( ( X `
 k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) )  =  ( k  e.  ( X supp  .0.  )  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )
7574oveq2d 6296 . . . . . . . . 9  |-  ( w  =  ( X supp  .0.  )  ->  ( P  gsumg  ( k  e.  w  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( P  gsumg  ( k  e.  ( X supp  .0.  )  |->  ( ( X `  k
)  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  )
) ) ) ) )
76 eleq2 2477 . . . . . . . . . . 11  |-  ( w  =  ( X supp  .0.  )  ->  ( y  e.  w  <->  y  e.  ( X supp  .0.  ) )
)
7776ifbid 3909 . . . . . . . . . 10  |-  ( w  =  ( X supp  .0.  )  ->  if ( y  e.  w ,  ( X `  y ) ,  .0.  )  =  if ( y  e.  ( X supp  .0.  ) ,  ( X `  y ) ,  .0.  ) )
7877mpteq2dv 4484 . . . . . . . . 9  |-  ( w  =  ( X supp  .0.  )  ->  ( y  e.  D  |->  if ( y  e.  w ,  ( X `  y ) ,  .0.  ) )  =  ( y  e.  D  |->  if ( y  e.  ( X supp  .0.  ) ,  ( X `  y ) ,  .0.  ) ) )
7975, 78eqeq12d 2426 . . . . . . . 8  |-  ( w  =  ( X supp  .0.  )  ->  ( ( P 
gsumg  ( k  e.  w  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  w ,  ( X `  y
) ,  .0.  )
)  <->  ( P  gsumg  ( k  e.  ( X supp  .0.  )  |->  ( ( X `
 k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  ( X supp 
.0.  ) ,  ( X `  y ) ,  .0.  ) ) ) )
8073, 79imbi12d 320 . . . . . . 7  |-  ( w  =  ( X supp  .0.  )  ->  ( ( w 
C_  D  ->  ( P  gsumg  ( k  e.  w  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  w ,  ( X `  y
) ,  .0.  )
) )  <->  ( ( X supp  .0.  )  C_  D  ->  ( P  gsumg  ( k  e.  ( X supp  .0.  )  |->  ( ( X `  k
)  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  )
) ) ) )  =  ( y  e.  D  |->  if ( y  e.  ( X supp  .0.  ) ,  ( X `  y ) ,  .0.  ) ) ) ) )
8180imbi2d 316 . . . . . 6  |-  ( w  =  ( X supp  .0.  )  ->  ( ( ph  ->  ( w  C_  D  ->  ( P  gsumg  ( k  e.  w  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  w ,  ( X `  y
) ,  .0.  )
) ) )  <->  ( ph  ->  ( ( X supp  .0.  )  C_  D  ->  ( P  gsumg  ( k  e.  ( X supp  .0.  )  |->  ( ( X `  k
)  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  )
) ) ) )  =  ( y  e.  D  |->  if ( y  e.  ( X supp  .0.  ) ,  ( X `  y ) ,  .0.  ) ) ) ) ) )
82 mplcoe1.i . . . . . . . . 9  |-  ( ph  ->  I  e.  W )
83 mplcoe1.r . . . . . . . . . 10  |-  ( ph  ->  R  e.  Ring )
84 ringgrp 17525 . . . . . . . . . 10  |-  ( R  e.  Ring  ->  R  e. 
Grp )
8583, 84syl 17 . . . . . . . . 9  |-  ( ph  ->  R  e.  Grp )
861, 4, 17, 44, 82, 85mpl0 18425 . . . . . . . 8  |-  ( ph  ->  ( 0g `  P
)  =  ( D  X.  {  .0.  }
) )
87 fconstmpt 4869 . . . . . . . 8  |-  ( D  X.  {  .0.  }
)  =  ( y  e.  D  |->  .0.  )
8886, 87syl6eq 2461 . . . . . . 7  |-  ( ph  ->  ( 0g `  P
)  =  ( y  e.  D  |->  .0.  )
)
8988a1d 26 . . . . . 6  |-  ( ph  ->  ( (/)  C_  D  -> 
( 0g `  P
)  =  ( y  e.  D  |->  .0.  )
) )
90 ssun1 3608 . . . . . . . . . . 11  |-  x  C_  ( x  u.  { z } )
91 sstr2 3451 . . . . . . . . . . 11  |-  ( x 
C_  ( x  u. 
{ z } )  ->  ( ( x  u.  { z } )  C_  D  ->  x 
C_  D ) )
9290, 91ax-mp 5 . . . . . . . . . 10  |-  ( ( x  u.  { z } )  C_  D  ->  x  C_  D )
9392imim1i 59 . . . . . . . . 9  |-  ( ( x  C_  D  ->  ( P  gsumg  ( k  e.  x  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y
) ,  .0.  )
) )  ->  (
( x  u.  {
z } )  C_  D  ->  ( P  gsumg  ( k  e.  x  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) ) ) )
94 oveq1 6287 . . . . . . . . . . . 12  |-  ( ( P  gsumg  ( k  e.  x  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y
) ,  .0.  )
)  ->  ( ( P  gsumg  ( k  e.  x  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) ) ( +g  `  P
) ( ( X `
 z )  .x.  ( y  e.  D  |->  if ( y  =  z ,  .1.  ,  .0.  ) ) ) )  =  ( ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y
) ,  .0.  )
) ( +g  `  P
) ( ( X `
 z )  .x.  ( y  e.  D  |->  if ( y  =  z ,  .1.  ,  .0.  ) ) ) ) )
95 eqid 2404 . . . . . . . . . . . . . 14  |-  ( +g  `  P )  =  ( +g  `  P )
961mplring 18436 . . . . . . . . . . . . . . . . 17  |-  ( ( I  e.  W  /\  R  e.  Ring )  ->  P  e.  Ring )
9782, 83, 96syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  P  e.  Ring )
98 ringcmn 17551 . . . . . . . . . . . . . . . 16  |-  ( P  e.  Ring  ->  P  e. CMnd
)
9997, 98syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  P  e. CMnd )
10099adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  P  e. CMnd )
101 simprll 766 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  x  e.  Fin )
102 simprr 760 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( x  u. 
{ z } ) 
C_  D )
103102unssad 3622 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  x  C_  D
)
104103sselda 3444 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  /\  k  e.  x
)  ->  k  e.  D )
10582adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  D )  ->  I  e.  W )
10683adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  D )  ->  R  e.  Ring )
1071mpllmod 18435 . . . . . . . . . . . . . . . . . 18  |-  ( ( I  e.  W  /\  R  e.  Ring )  ->  P  e.  LMod )
108105, 106, 107syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  D )  ->  P  e.  LMod )
1096ffvelrnda 6011 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  D )  ->  ( X `  k )  e.  ( Base `  R
) )
1101, 82, 83mplsca 18429 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  R  =  (Scalar `  P ) )
111110adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  D )  ->  R  =  (Scalar `  P )
)
112111fveq2d 5855 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  D )  ->  ( Base `  R )  =  ( Base `  (Scalar `  P ) ) )
113109, 112eleqtrd 2494 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  D )  ->  ( X `  k )  e.  ( Base `  (Scalar `  P ) ) )
114 mplcoe1.o . . . . . . . . . . . . . . . . . 18  |-  .1.  =  ( 1r `  R )
115 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  D )  ->  k  e.  D )
1161, 3, 17, 114, 4, 105, 106, 115mplmon 18447 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  D )  ->  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) )  e.  B
)
117 eqid 2404 . . . . . . . . . . . . . . . . . 18  |-  (Scalar `  P )  =  (Scalar `  P )
118 mplcoe1.n . . . . . . . . . . . . . . . . . 18  |-  .x.  =  ( .s `  P )
119 eqid 2404 . . . . . . . . . . . . . . . . . 18  |-  ( Base `  (Scalar `  P )
)  =  ( Base `  (Scalar `  P )
)
1203, 117, 118, 119lmodvscl 17851 . . . . . . . . . . . . . . . . 17  |-  ( ( P  e.  LMod  /\  ( X `  k )  e.  ( Base `  (Scalar `  P ) )  /\  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) )  e.  B
)  ->  ( ( X `  k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) )  e.  B )
121108, 113, 116, 120syl3anc 1232 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  D )  ->  (
( X `  k
)  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  )
) )  e.  B
)
122121adantlr 715 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  /\  k  e.  D
)  ->  ( ( X `  k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) )  e.  B )
123104, 122syldan 470 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  /\  k  e.  x
)  ->  ( ( X `  k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) )  e.  B )
124 vex 3064 . . . . . . . . . . . . . . 15  |-  z  e. 
_V
125124a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  z  e.  _V )
126 simprlr 767 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  -.  z  e.  x )
12782, 83, 107syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  P  e.  LMod )
128127adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  P  e.  LMod )
1296adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  X : D --> ( Base `  R )
)
130102unssbd 3623 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  { z } 
C_  D )
131124snss 4098 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  D  <->  { z }  C_  D )
132130, 131sylibr 214 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  z  e.  D
)
133129, 132ffvelrnd 6012 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( X `  z )  e.  (
Base `  R )
)
134110adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  R  =  (Scalar `  P ) )
135134fveq2d 5855 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( Base `  R
)  =  ( Base `  (Scalar `  P )
) )
136133, 135eleqtrd 2494 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( X `  z )  e.  (
Base `  (Scalar `  P
) ) )
13782adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  I  e.  W
)
13883adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  R  e.  Ring )
1391, 3, 17, 114, 4, 137, 138, 132mplmon 18447 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( y  e.  D  |->  if ( y  =  z ,  .1.  ,  .0.  ) )  e.  B )
1403, 117, 118, 119lmodvscl 17851 . . . . . . . . . . . . . . 15  |-  ( ( P  e.  LMod  /\  ( X `  z )  e.  ( Base `  (Scalar `  P ) )  /\  ( y  e.  D  |->  if ( y  =  z ,  .1.  ,  .0.  ) )  e.  B
)  ->  ( ( X `  z )  .x.  ( y  e.  D  |->  if ( y  =  z ,  .1.  ,  .0.  ) ) )  e.  B )
141128, 136, 139, 140syl3anc 1232 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( ( X `
 z )  .x.  ( y  e.  D  |->  if ( y  =  z ,  .1.  ,  .0.  ) ) )  e.  B )
142 fveq2 5851 . . . . . . . . . . . . . . 15  |-  ( k  =  z  ->  ( X `  k )  =  ( X `  z ) )
143 equequ2 1825 . . . . . . . . . . . . . . . . 17  |-  ( k  =  z  ->  (
y  =  k  <->  y  =  z ) )
144143ifbid 3909 . . . . . . . . . . . . . . . 16  |-  ( k  =  z  ->  if ( y  =  k ,  .1.  ,  .0.  )  =  if (
y  =  z ,  .1.  ,  .0.  )
)
145144mpteq2dv 4484 . . . . . . . . . . . . . . 15  |-  ( k  =  z  ->  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) )  =  ( y  e.  D  |->  if ( y  =  z ,  .1.  ,  .0.  ) ) )
146142, 145oveq12d 6298 . . . . . . . . . . . . . 14  |-  ( k  =  z  ->  (
( X `  k
)  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  )
) )  =  ( ( X `  z
)  .x.  ( y  e.  D  |->  if ( y  =  z ,  .1.  ,  .0.  )
) ) )
1473, 95, 100, 101, 123, 125, 126, 141, 146gsumunsn 17309 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( P  gsumg  ( k  e.  ( x  u. 
{ z } ) 
|->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( ( P  gsumg  ( k  e.  x  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) ) ( +g  `  P
) ( ( X `
 z )  .x.  ( y  e.  D  |->  if ( y  =  z ,  .1.  ,  .0.  ) ) ) ) )
148 eqid 2404 . . . . . . . . . . . . . . 15  |-  ( +g  `  R )  =  ( +g  `  R )
149129ffvelrnda 6011 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  /\  y  e.  D
)  ->  ( X `  y )  e.  (
Base `  R )
)
1502, 17ring0cl 17542 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( R  e.  Ring  ->  .0.  e.  ( Base `  R )
)
15183, 150syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  .0.  e.  ( Base `  R ) )
152151ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  /\  y  e.  D
)  ->  .0.  e.  ( Base `  R )
)
153149, 152ifcld 3930 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  /\  y  e.  D
)  ->  if (
y  e.  x ,  ( X `  y
) ,  .0.  )  e.  ( Base `  R
) )
154 eqid 2404 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y
) ,  .0.  )
)  =  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y
) ,  .0.  )
)
155153, 154fmptd 6035 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) ) : D --> ( Base `  R ) )
156 fvex 5861 . . . . . . . . . . . . . . . . . . 19  |-  ( Base `  R )  e.  _V
157156, 15elmap 7487 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) )  e.  ( ( Base `  R
)  ^m  D )  <->  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) ) : D --> ( Base `  R )
)
158155, 157sylibr 214 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) )  e.  ( ( Base `  R )  ^m  D
) )
15933, 2, 4, 34, 137psrbas 18352 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( Base `  (
I mPwSer  R ) )  =  ( ( Base `  R
)  ^m  D )
)
160158, 159eleqtrrd 2495 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) )  e.  ( Base `  (
I mPwSer  R ) ) )
16115mptex 6126 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y
) ,  .0.  )
)  e.  _V
162 funmpt 5607 . . . . . . . . . . . . . . . . . . 19  |-  Fun  (
y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) )
163161, 162, 193pm3.2i 1177 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) )  e.  _V  /\ 
Fun  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) )  /\  .0.  e.  _V )
164163a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y
) ,  .0.  )
)  e.  _V  /\  Fun  ( y  e.  D  |->  if ( y  e.  x ,  ( X `
 y ) ,  .0.  ) )  /\  .0.  e.  _V ) )
165 eldifn 3568 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( D  \  x )  ->  -.  y  e.  x )
166165adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  /\  y  e.  ( D  \  x ) )  ->  -.  y  e.  x )
167166iffalsed 3898 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  /\  y  e.  ( D  \  x ) )  ->  if (
y  e.  x ,  ( X `  y
) ,  .0.  )  =  .0.  )
16815a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  D  e.  _V )
169167, 168suppss2 6939 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y
) ,  .0.  )
) supp  .0.  )  C_  x )
170 suppssfifsupp 7880 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) )  e.  _V  /\  Fun  ( y  e.  D  |->  if ( y  e.  x ,  ( X `
 y ) ,  .0.  ) )  /\  .0.  e.  _V )  /\  ( x  e.  Fin  /\  ( ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) ) supp 
.0.  )  C_  x
) )  ->  (
y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) ) finSupp  .0.  )
171164, 101, 169, 170syl12anc 1230 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) ) finSupp  .0.  )
1721, 33, 34, 17, 3mplelbas 18409 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) )  e.  B  <->  ( ( y  e.  D  |->  if ( y  e.  x ,  ( X `
 y ) ,  .0.  ) )  e.  ( Base `  (
I mPwSer  R ) )  /\  ( y  e.  D  |->  if ( y  e.  x ,  ( X `
 y ) ,  .0.  ) ) finSupp  .0.  ) )
173160, 171, 172sylanbrc 664 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) )  e.  B )
1741, 3, 148, 95, 173, 141mpladd 18426 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y
) ,  .0.  )
) ( +g  `  P
) ( ( X `
 z )  .x.  ( y  e.  D  |->  if ( y  =  z ,  .1.  ,  .0.  ) ) ) )  =  ( ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y
) ,  .0.  )
)  oF ( +g  `  R ) ( ( X `  z )  .x.  (
y  e.  D  |->  if ( y  =  z ,  .1.  ,  .0.  ) ) ) ) )
175 ovex 6308 . . . . . . . . . . . . . . . 16  |-  ( ( X `  z ) ( .r `  R
) if ( y  =  z ,  .1.  ,  .0.  ) )  e. 
_V
176175a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  /\  y  e.  D
)  ->  ( ( X `  z )
( .r `  R
) if ( y  =  z ,  .1.  ,  .0.  ) )  e. 
_V )
177 eqidd 2405 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) )  =  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) ) )
178 eqid 2404 . . . . . . . . . . . . . . . . 17  |-  ( .r
`  R )  =  ( .r `  R
)
1791, 118, 2, 3, 178, 4, 133, 139mplvsca 18431 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( ( X `
 z )  .x.  ( y  e.  D  |->  if ( y  =  z ,  .1.  ,  .0.  ) ) )  =  ( ( D  X.  { ( X `  z ) } )  oF ( .r
`  R ) ( y  e.  D  |->  if ( y  =  z ,  .1.  ,  .0.  ) ) ) )
180133adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  /\  y  e.  D
)  ->  ( X `  z )  e.  (
Base `  R )
)
1812, 114ringidcl 17541 . . . . . . . . . . . . . . . . . . . 20  |-  ( R  e.  Ring  ->  .1.  e.  ( Base `  R )
)
182181, 150ifcld 3930 . . . . . . . . . . . . . . . . . . 19  |-  ( R  e.  Ring  ->  if ( y  =  z ,  .1.  ,  .0.  )  e.  ( Base `  R
) )
18383, 182syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  if ( y  =  z ,  .1.  ,  .0.  )  e.  ( Base `  R ) )
184183ad2antrr 726 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  /\  y  e.  D
)  ->  if (
y  =  z ,  .1.  ,  .0.  )  e.  ( Base `  R
) )
185 fconstmpt 4869 . . . . . . . . . . . . . . . . . 18  |-  ( D  X.  { ( X `
 z ) } )  =  ( y  e.  D  |->  ( X `
 z ) )
186185a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( D  X.  { ( X `  z ) } )  =  ( y  e.  D  |->  ( X `  z ) ) )
187 eqidd 2405 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( y  e.  D  |->  if ( y  =  z ,  .1.  ,  .0.  ) )  =  ( y  e.  D  |->  if ( y  =  z ,  .1.  ,  .0.  ) ) )
188168, 180, 184, 186, 187offval2 6540 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( ( D  X.  { ( X `
 z ) } )  oF ( .r `  R ) ( y  e.  D  |->  if ( y  =  z ,  .1.  ,  .0.  ) ) )  =  ( y  e.  D  |->  ( ( X `  z ) ( .r
`  R ) if ( y  =  z ,  .1.  ,  .0.  ) ) ) )
189179, 188eqtrd 2445 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( ( X `
 z )  .x.  ( y  e.  D  |->  if ( y  =  z ,  .1.  ,  .0.  ) ) )  =  ( y  e.  D  |->  ( ( X `  z ) ( .r
`  R ) if ( y  =  z ,  .1.  ,  .0.  ) ) ) )
190168, 153, 176, 177, 189offval2 6540 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y
) ,  .0.  )
)  oF ( +g  `  R ) ( ( X `  z )  .x.  (
y  e.  D  |->  if ( y  =  z ,  .1.  ,  .0.  ) ) ) )  =  ( y  e.  D  |->  ( if ( y  e.  x ,  ( X `  y
) ,  .0.  )
( +g  `  R ) ( ( X `  z ) ( .r
`  R ) if ( y  =  z ,  .1.  ,  .0.  ) ) ) ) )
191138, 84syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  R  e.  Grp )
1922, 148, 17grplid 16406 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R  e.  Grp  /\  ( X `  z )  e.  ( Base `  R
) )  ->  (  .0.  ( +g  `  R
) ( X `  z ) )  =  ( X `  z
) )
193191, 133, 192syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  (  .0.  ( +g  `  R ) ( X `  z ) )  =  ( X `
 z ) )
194193ad2antrr 726 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  y  e.  { z } )  ->  (  .0.  ( +g  `  R ) ( X `  z ) )  =  ( X `
 z ) )
195 simpr 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  y  e.  { z } )  ->  y  e.  {
z } )
196 elsn 3988 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  { z }  <-> 
y  =  z )
197195, 196sylib 198 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  y  e.  { z } )  ->  y  =  z )
198197fveq2d 5855 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  y  e.  { z } )  ->  ( X `  y )  =  ( X `  z ) )
199194, 198eqtr4d 2448 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  y  e.  { z } )  ->  (  .0.  ( +g  `  R ) ( X `  z ) )  =  ( X `
 y ) )
200126ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  y  e.  { z } )  ->  -.  z  e.  x )
201197, 200eqneltrd 2513 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  y  e.  { z } )  ->  -.  y  e.  x )
202201iffalsed 3898 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  y  e.  { z } )  ->  if ( y  e.  x ,  ( X `  y ) ,  .0.  )  =  .0.  )
203197iftrued 3895 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  y  e.  { z } )  ->  if ( y  =  z ,  .1.  ,  .0.  )  =  .1.  )
204203oveq2d 6296 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  y  e.  { z } )  ->  ( ( X `
 z ) ( .r `  R ) if ( y  =  z ,  .1.  ,  .0.  ) )  =  ( ( X `  z
) ( .r `  R )  .1.  )
)
2052, 178, 114ringridm 17545 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e.  Ring  /\  ( X `  z )  e.  ( Base `  R
) )  ->  (
( X `  z
) ( .r `  R )  .1.  )  =  ( X `  z ) )
206138, 133, 205syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( ( X `
 z ) ( .r `  R )  .1.  )  =  ( X `  z ) )
207206ad2antrr 726 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  y  e.  { z } )  ->  ( ( X `
 z ) ( .r `  R )  .1.  )  =  ( X `  z ) )
208204, 207eqtrd 2445 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  y  e.  { z } )  ->  ( ( X `
 z ) ( .r `  R ) if ( y  =  z ,  .1.  ,  .0.  ) )  =  ( X `  z ) )
209202, 208oveq12d 6298 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  y  e.  { z } )  ->  ( if ( y  e.  x ,  ( X `  y
) ,  .0.  )
( +g  `  R ) ( ( X `  z ) ( .r
`  R ) if ( y  =  z ,  .1.  ,  .0.  ) ) )  =  (  .0.  ( +g  `  R ) ( X `
 z ) ) )
210 elun2 3613 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  { z }  ->  y  e.  ( x  u.  { z } ) )
211210adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  y  e.  { z } )  ->  y  e.  ( x  u.  { z } ) )
212211iftrued 3895 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  y  e.  { z } )  ->  if ( y  e.  ( x  u. 
{ z } ) ,  ( X `  y ) ,  .0.  )  =  ( X `  y ) )
213199, 209, 2123eqtr4d 2455 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  y  e.  { z } )  ->  ( if ( y  e.  x ,  ( X `  y
) ,  .0.  )
( +g  `  R ) ( ( X `  z ) ( .r
`  R ) if ( y  =  z ,  .1.  ,  .0.  ) ) )  =  if ( y  e.  ( x  u.  {
z } ) ,  ( X `  y
) ,  .0.  )
)
21485ad2antrr 726 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  /\  y  e.  D
)  ->  R  e.  Grp )
2152, 148, 17grprid 16407 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  Grp  /\  if ( y  e.  x ,  ( X `  y ) ,  .0.  )  e.  ( Base `  R ) )  -> 
( if ( y  e.  x ,  ( X `  y ) ,  .0.  ) ( +g  `  R )  .0.  )  =  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) )
216214, 153, 215syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  /\  y  e.  D
)  ->  ( if ( y  e.  x ,  ( X `  y ) ,  .0.  ) ( +g  `  R
)  .0.  )  =  if ( y  e.  x ,  ( X `
 y ) ,  .0.  ) )
217216adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  -.  y  e.  { z } )  ->  ( if ( y  e.  x ,  ( X `  y ) ,  .0.  ) ( +g  `  R
)  .0.  )  =  if ( y  e.  x ,  ( X `
 y ) ,  .0.  ) )
218 simpr 461 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  -.  y  e.  { z } )  ->  -.  y  e.  { z } )
219218, 196sylnib 304 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  -.  y  e.  { z } )  ->  -.  y  =  z )
220219iffalsed 3898 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  -.  y  e.  { z } )  ->  if ( y  =  z ,  .1.  ,  .0.  )  =  .0.  )
221220oveq2d 6296 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  -.  y  e.  { z } )  ->  (
( X `  z
) ( .r `  R ) if ( y  =  z ,  .1.  ,  .0.  )
)  =  ( ( X `  z ) ( .r `  R
)  .0.  ) )
2222, 178, 17ringrz 17558 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e.  Ring  /\  ( X `  z )  e.  ( Base `  R
) )  ->  (
( X `  z
) ( .r `  R )  .0.  )  =  .0.  )
223138, 133, 222syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( ( X `
 z ) ( .r `  R )  .0.  )  =  .0.  )
224223ad2antrr 726 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  -.  y  e.  { z } )  ->  (
( X `  z
) ( .r `  R )  .0.  )  =  .0.  )
225221, 224eqtrd 2445 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  -.  y  e.  { z } )  ->  (
( X `  z
) ( .r `  R ) if ( y  =  z ,  .1.  ,  .0.  )
)  =  .0.  )
226225oveq2d 6296 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  -.  y  e.  { z } )  ->  ( if ( y  e.  x ,  ( X `  y ) ,  .0.  ) ( +g  `  R
) ( ( X `
 z ) ( .r `  R ) if ( y  =  z ,  .1.  ,  .0.  ) ) )  =  ( if ( y  e.  x ,  ( X `  y ) ,  .0.  ) ( +g  `  R )  .0.  ) )
227 biorf 405 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  y  e.  { z }  ->  ( y  e.  x  <->  ( y  e. 
{ z }  \/  y  e.  x )
) )
228 elun 3586 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( x  u. 
{ z } )  <-> 
( y  e.  x  \/  y  e.  { z } ) )
229 orcom 387 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  e.  x  \/  y  e.  { z } )  <->  ( y  e.  { z }  \/  y  e.  x )
)
230228, 229bitri 251 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( x  u. 
{ z } )  <-> 
( y  e.  {
z }  \/  y  e.  x ) )
231227, 230syl6rbbr 266 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  y  e.  { z }  ->  ( y  e.  ( x  u.  {
z } )  <->  y  e.  x ) )
232231adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  -.  y  e.  { z } )  ->  (
y  e.  ( x  u.  { z } )  <->  y  e.  x
) )
233232ifbid 3909 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  -.  y  e.  { z } )  ->  if ( y  e.  ( x  u.  { z } ) ,  ( X `  y ) ,  .0.  )  =  if ( y  e.  x ,  ( X `
 y ) ,  .0.  ) )
234217, 226, 2333eqtr4d 2455 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  -.  y  e.  { z } )  ->  ( if ( y  e.  x ,  ( X `  y ) ,  .0.  ) ( +g  `  R
) ( ( X `
 z ) ( .r `  R ) if ( y  =  z ,  .1.  ,  .0.  ) ) )  =  if ( y  e.  ( x  u.  {
z } ) ,  ( X `  y
) ,  .0.  )
)
235213, 234pm2.61dan 794 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  /\  y  e.  D
)  ->  ( if ( y  e.  x ,  ( X `  y ) ,  .0.  ) ( +g  `  R
) ( ( X `
 z ) ( .r `  R ) if ( y  =  z ,  .1.  ,  .0.  ) ) )  =  if ( y  e.  ( x  u.  {
z } ) ,  ( X `  y
) ,  .0.  )
)
236235mpteq2dva 4483 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( y  e.  D  |->  ( if ( y  e.  x ,  ( X `  y
) ,  .0.  )
( +g  `  R ) ( ( X `  z ) ( .r
`  R ) if ( y  =  z ,  .1.  ,  .0.  ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  ( x  u. 
{ z } ) ,  ( X `  y ) ,  .0.  ) ) )
237174, 190, 2363eqtrrd 2450 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( y  e.  D  |->  if ( y  e.  ( x  u. 
{ z } ) ,  ( X `  y ) ,  .0.  ) )  =  ( ( y  e.  D  |->  if ( y  e.  x ,  ( X `
 y ) ,  .0.  ) ) ( +g  `  P ) ( ( X `  z )  .x.  (
y  e.  D  |->  if ( y  =  z ,  .1.  ,  .0.  ) ) ) ) )
238147, 237eqeq12d 2426 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( ( P 
gsumg  ( k  e.  ( x  u.  { z } )  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  ( x  u.  { z } ) ,  ( X `  y ) ,  .0.  ) )  <-> 
( ( P  gsumg  ( k  e.  x  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) ) ( +g  `  P ) ( ( X `  z ) 
.x.  ( y  e.  D  |->  if ( y  =  z ,  .1.  ,  .0.  ) ) ) )  =  ( ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) ) ( +g  `  P ) ( ( X `  z ) 
.x.  ( y  e.  D  |->  if ( y  =  z ,  .1.  ,  .0.  ) ) ) ) ) )
23994, 238syl5ibr 223 . . . . . . . . . . 11  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( ( P 
gsumg  ( k  e.  x  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y
) ,  .0.  )
)  ->  ( P  gsumg  ( k  e.  ( x  u.  { z } )  |->  ( ( X `
 k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  ( x  u.  { z } ) ,  ( X `
 y ) ,  .0.  ) ) ) )
240239expr 615 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  Fin  /\  -.  z  e.  x ) )  -> 
( ( x  u. 
{ z } ) 
C_  D  ->  (
( P  gsumg  ( k  e.  x  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y
) ,  .0.  )
)  ->  ( P  gsumg  ( k  e.  ( x  u.  { z } )  |->  ( ( X `
 k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  ( x  u.  { z } ) ,  ( X `
 y ) ,  .0.  ) ) ) ) )
241240a2d 28 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  Fin  /\  -.  z  e.  x ) )  -> 
( ( ( x  u.  { z } )  C_  D  ->  ( P  gsumg  ( k  e.  x  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y
) ,  .0.  )
) )  ->  (
( x  u.  {
z } )  C_  D  ->  ( P  gsumg  ( k  e.  ( x  u. 
{ z } ) 
|->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  ( x  u.  { z } ) ,  ( X `
 y ) ,  .0.  ) ) ) ) )
24293, 241syl5 32 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  Fin  /\  -.  z  e.  x ) )  -> 
( ( x  C_  D  ->  ( P  gsumg  ( k  e.  x  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) ) )  -> 
( ( x  u. 
{ z } ) 
C_  D  ->  ( P  gsumg  ( k  e.  ( x  u.  { z } )  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  ( x  u.  { z } ) ,  ( X `  y ) ,  .0.  ) ) ) ) )
243242expcom 435 . . . . . . 7  |-  ( ( x  e.  Fin  /\  -.  z  e.  x
)  ->  ( ph  ->  ( ( x  C_  D  ->  ( P  gsumg  ( k  e.  x  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) ) )  -> 
( ( x  u. 
{ z } ) 
C_  D  ->  ( P  gsumg  ( k  e.  ( x  u.  { z } )  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  ( x  u.  { z } ) ,  ( X `  y ) ,  .0.  ) ) ) ) ) )
244243a2d 28 . . . . . 6  |-  ( ( x  e.  Fin  /\  -.  z  e.  x
)  ->  ( ( ph  ->  ( x  C_  D  ->  ( P  gsumg  ( k  e.  x  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) ) ) )  ->  ( ph  ->  ( ( x  u.  {
z } )  C_  D  ->  ( P  gsumg  ( k  e.  ( x  u. 
{ z } ) 
|->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  ( x  u.  { z } ) ,  ( X `
 y ) ,  .0.  ) ) ) ) ) )
24554, 63, 72, 81, 89, 244findcard2s 7797 . . . . 5  |-  ( ( X supp  .0.  )  e.  Fin  ->  ( ph  ->  ( ( X supp  .0.  )  C_  D  ->  ( P  gsumg  ( k  e.  ( X supp 
.0.  )  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( y  e.  D  |->  if ( y  e.  ( X supp  .0.  ) , 
( X `  y
) ,  .0.  )
) ) ) )
24638, 245mpcom 36 . . . 4  |-  ( ph  ->  ( ( X supp  .0.  )  C_  D  ->  ( P  gsumg  ( k  e.  ( X supp  .0.  )  |->  ( ( X `  k
)  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  )
) ) ) )  =  ( y  e.  D  |->  if ( y  e.  ( X supp  .0.  ) ,  ( X `  y ) ,  .0.  ) ) ) )
24732, 246mpd 15 . . 3  |-  ( ph  ->  ( P  gsumg  ( k  e.  ( X supp  .0.  )  |->  ( ( X `  k
)  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  )
) ) ) )  =  ( y  e.  D  |->  if ( y  e.  ( X supp  .0.  ) ,  ( X `  y ) ,  .0.  ) ) )
24828, 247eqtr4d 2448 . 2  |-  ( ph  ->  X  =  ( P 
gsumg  ( k  e.  ( X supp  .0.  )  |->  ( ( X `  k
)  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  )
) ) ) ) )
24932resmptd 5147 . . . 4  |-  ( ph  ->  ( ( k  e.  D  |->  ( ( X `
 k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) )  |`  ( X supp  .0.  )
)  =  ( k  e.  ( X supp  .0.  )  |->  ( ( X `
 k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )
250249oveq2d 6296 . . 3  |-  ( ph  ->  ( P  gsumg  ( ( k  e.  D  |->  ( ( X `
 k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) )  |`  ( X supp  .0.  )
) )  =  ( P  gsumg  ( k  e.  ( X supp  .0.  )  |->  ( ( X `  k
)  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  )
) ) ) ) )
251 eqid 2404 . . . . 5  |-  ( k  e.  D  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) )  =  ( k  e.  D  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) )
252121, 251fmptd 6035 . . . 4  |-  ( ph  ->  ( k  e.  D  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) : D --> B )
2536, 13, 16, 20suppssr 6936 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( D  \  ( X supp  .0.  ) ) )  ->  ( X `  k )  =  .0.  )
254253oveq1d 6295 . . . . . 6  |-  ( (
ph  /\  k  e.  ( D  \  ( X supp  .0.  ) ) )  ->  ( ( X `
 k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) )  =  (  .0.  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) )
255 eldifi 3567 . . . . . . 7  |-  ( k  e.  ( D  \ 
( X supp  .0.  )
)  ->  k  e.  D )
256111fveq2d 5855 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  D )  ->  ( 0g `  R )  =  ( 0g `  (Scalar `  P ) ) )
25717, 256syl5eq 2457 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  D )  ->  .0.  =  ( 0g `  (Scalar `  P ) ) )
258257oveq1d 6295 . . . . . . . 8  |-  ( (
ph  /\  k  e.  D )  ->  (  .0.  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) )  =  ( ( 0g
`  (Scalar `  P )
)  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  )
) ) )
259 eqid 2404 . . . . . . . . . 10  |-  ( 0g
`  (Scalar `  P )
)  =  ( 0g
`  (Scalar `  P )
)
2603, 117, 118, 259, 44lmod0vs 17867 . . . . . . . . 9  |-  ( ( P  e.  LMod  /\  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) )  e.  B
)  ->  ( ( 0g `  (Scalar `  P
) )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) )  =  ( 0g `  P
) )
261108, 116, 260syl2anc 661 . . . . . . . 8  |-  ( (
ph  /\  k  e.  D )  ->  (
( 0g `  (Scalar `  P ) )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) )  =  ( 0g `  P
) )
262258, 261eqtrd 2445 . . . . . . 7  |-  ( (
ph  /\  k  e.  D )  ->  (  .0.  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) )  =  ( 0g `  P ) )
263255, 262sylan2 474 . . . . . 6  |-  ( (
ph  /\  k  e.  ( D  \  ( X supp  .0.  ) ) )  ->  (  .0.  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) )  =  ( 0g `  P
) )
264254, 263eqtrd 2445 . . . . 5  |-  ( (
ph  /\  k  e.  ( D  \  ( X supp  .0.  ) ) )  ->  ( ( X `
 k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) )  =  ( 0g `  P
) )
265264, 16suppss2 6939 . . . 4  |-  ( ph  ->  ( ( k  e.  D  |->  ( ( X `
 k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) supp  ( 0g `  P
) )  C_  ( X supp  .0.  ) )
26615mptex 6126 . . . . . . 7  |-  ( k  e.  D  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) )  e.  _V
267 funmpt 5607 . . . . . . 7  |-  Fun  (
k  e.  D  |->  ( ( X `  k
)  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  )
) ) )
268 fvex 5861 . . . . . . 7  |-  ( 0g
`  P )  e. 
_V
269266, 267, 2683pm3.2i 1177 . . . . . 6  |-  ( ( k  e.  D  |->  ( ( X `  k
)  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  )
) ) )  e. 
_V  /\  Fun  ( k  e.  D  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) )  /\  ( 0g
`  P )  e. 
_V )
270269a1i 11 . . . . 5  |-  ( ph  ->  ( ( k  e.  D  |->  ( ( X `
 k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) )  e.  _V  /\  Fun  ( k  e.  D  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) )  /\  ( 0g `  P )  e.  _V ) )
271 suppssfifsupp 7880 . . . . 5  |-  ( ( ( ( k  e.  D  |->  ( ( X `
 k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) )  e.  _V  /\  Fun  ( k  e.  D  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) )  /\  ( 0g `  P )  e.  _V )  /\  ( ( X supp 
.0.  )  e.  Fin  /\  ( ( k  e.  D  |->  ( ( X `
 k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) supp  ( 0g `  P
) )  C_  ( X supp  .0.  ) ) )  ->  ( k  e.  D  |->  ( ( X `
 k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) finSupp 
( 0g `  P
) )
272270, 38, 265, 271syl12anc 1230 . . . 4  |-  ( ph  ->  ( k  e.  D  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) finSupp 
( 0g `  P
) )
2733, 44, 99, 16, 252, 265, 272gsumres 17247 . . 3  |-  ( ph  ->  ( P  gsumg  ( ( k  e.  D  |->  ( ( X `
 k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) )  |`  ( X supp  .0.  )
) )  =  ( P  gsumg  ( k  e.  D  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) ) )
274250, 273eqtr3d 2447 . 2  |-  ( ph  ->  ( P  gsumg  ( k  e.  ( X supp  .0.  )  |->  ( ( X `  k
)  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  )
) ) ) )  =  ( P  gsumg  ( k  e.  D  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) ) )
275248, 274eqtrd 2445 1  |-  ( ph  ->  X  =  ( P 
gsumg  ( k  e.  D  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 186    \/ wo 368    /\ wa 369    /\ w3a 976    = wceq 1407    e. wcel 1844   {crab 2760   _Vcvv 3061    \ cdif 3413    u. cun 3414    C_ wss 3416   (/)c0 3740   ifcif 3887   {csn 3974   class class class wbr 4397    |-> cmpt 4455    X. cxp 4823   `'ccnv 4824   dom cdm 4825    |` cres 4827   "cima 4828   Fun wfun 5565   -->wf 5567   ` cfv 5571  (class class class)co 6280    oFcof 6521   supp csupp 6904    ^m cmap 7459   Fincfn 7556   finSupp cfsupp 7865   NNcn 10578   NN0cn0 10838   Basecbs 14843   +g cplusg 14911   .rcmulr 14912  Scalarcsca 14914   .scvsca 14915   0gc0g 15056    gsumg cgsu 15057   Grpcgrp 16379  CMndccmn 17124   1rcur 17475   Ringcrg 17520   LModclmod 17834   mPwSer cmps 18322   mPoly cmpl 18324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-8 1846  ax-9 1848  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-rep 4509  ax-sep 4519  ax-nul 4527  ax-pow 4574  ax-pr 4632  ax-un 6576  ax-inf2 8093  ax-cnex 9580  ax-resscn 9581  ax-1cn 9582  ax-icn 9583  ax-addcl 9584  ax-addrcl 9585  ax-mulcl 9586  ax-mulrcl 9587  ax-mulcom 9588  ax-addass 9589  ax-mulass 9590  ax-distr 9591  ax-i2m1 9592  ax-1ne0 9593  ax-1rid 9594  ax-rnegex 9595  ax-rrecex 9596  ax-cnre 9597  ax-pre-lttri 9598  ax-pre-lttrn 9599  ax-pre-ltadd 9600  ax-pre-mulgt0 9601
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3or 977  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-eu 2244  df-mo 2245  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-nel 2603  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3063  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3741  df-if 3888  df-pw 3959  df-sn 3975  df-pr 3977  df-tp 3979  df-op 3981  df-uni 4194  df-int 4230  df-iun 4275  df-iin 4276  df-br 4398  df-opab 4456  df-mpt 4457  df-tr 4492  df-eprel 4736  df-id 4740  df-po 4746  df-so 4747  df-fr 4784  df-se 4785  df-we 4786  df-xp 4831  df-rel 4832  df-cnv 4833  df-co 4834  df-dm 4835  df-rn 4836  df-res 4837  df-ima 4838  df-pred 5369  df-ord 5415  df-on 5416  df-lim 5417  df-suc 5418  df-iota 5535  df-fun 5573  df-fn 5574  df-f 5575  df-f1 5576  df-fo 5577  df-f1o 5578  df-fv 5579  df-isom 5580  df-riota 6242  df-ov 6283  df-oprab 6284  df-mpt2 6285  df-of 6523  df-ofr 6524  df-om 6686  df-1st 6786  df-2nd 6787  df-supp 6905  df-wrecs 7015  df-recs 7077  df-rdg 7115  df-1o 7169  df-2o 7170  df-oadd 7173  df-er 7350  df-map 7461  df-pm 7462  df-ixp 7510  df-en 7557  df-dom 7558  df-sdom 7559  df-fin 7560  df-fsupp 7866  df-oi 7971  df-card 8354  df-pnf 9662  df-mnf 9663  df-xr 9664  df-ltxr 9665  df-le 9666  df-sub 9845  df-neg 9846  df-nn 10579  df-2 10637  df-3 10638  df-4 10639  df-5 10640  df-6 10641  df-7 10642  df-8 10643  df-9 10644  df-n0 10839  df-z 10908  df-uz 11130  df-fz 11729  df-fzo 11857  df-seq 12154  df-hash 12455  df-struct 14845  df-ndx 14846  df-slot 14847  df-base 14848  df-sets 14849  df-ress 14850  df-plusg 14924  df-mulr 14925  df-sca 14927  df-vsca 14928  df-tset 14930  df-0g 15058  df-gsum 15059  df-mre 15202  df-mrc 15203  df-acs 15205  df-mgm 16198  df-sgrp 16237  df-mnd 16247  df-mhm 16292  df-submnd 16293  df-grp 16383  df-minusg 16384  df-sbg 16385  df-mulg 16386  df-subg 16524  df-ghm 16591  df-cntz 16681  df-cmn 17126  df-abl 17127  df-mgp 17464  df-ur 17476  df-ring 17522  df-subrg 17749  df-lmod 17836  df-lss 17901  df-psr 18327  df-mpl 18329
This theorem is referenced by:  mplbas2  18456  mplbas2OLD  18457  mplcoe4  18490  ply1coe  18659  ply1coeOLD  18660
  Copyright terms: Public domain W3C validator