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

Theorem mplcoe1 17926
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 2467 . . . . . 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 17891 . . . . 5  |-  ( ph  ->  X : D --> ( Base `  R ) )
76feqmptd 5920 . . . 4  |-  ( ph  ->  X  =  ( y  e.  D  |->  ( X `
 y ) ) )
8 iftrue 3945 . . . . . . 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 3486 . . . . . . . 8  |-  ( y  e.  ( D  \ 
( X supp  .0.  )
)  <->  ( y  e.  D  /\  -.  y  e.  ( X supp  .0.  )
) )
11 ifid 3976 . . . . . . . . 9  |-  if ( y  e.  ( X supp 
.0.  ) ,  ( X `  y ) ,  ( X `  y ) )  =  ( X `  y
)
12 ssid 3523 . . . . . . . . . . . 12  |-  ( X supp 
.0.  )  C_  ( X supp  .0.  )
1312a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  ( X supp  .0.  )  C_  ( X supp  .0.  )
)
14 ovex 6309 . . . . . . . . . . . . 13  |-  ( NN0 
^m  I )  e. 
_V
154, 14rabex2 4600 . . . . . . . . . . . 12  |-  D  e. 
_V
1615a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  D  e.  _V )
17 mplcoe1.z . . . . . . . . . . . . 13  |-  .0.  =  ( 0g `  R )
18 fvex 5876 . . . . . . . . . . . . 13  |-  ( 0g
`  R )  e. 
_V
1917, 18eqeltri 2551 . . . . . . . . . . . 12  |-  .0.  e.  _V
2019a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  .0.  e.  _V )
216, 13, 16, 20suppssr 6931 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( D  \  ( X supp  .0.  ) ) )  ->  ( X `  y )  =  .0.  )
2221ifeq2d 3958 . . . . . . . . 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 2523 . . . . . . . 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 789 . . . . 5  |-  ( (
ph  /\  y  e.  D )  ->  if ( y  e.  ( X supp  .0.  ) , 
( X `  y
) ,  .0.  )  =  ( X `  y ) )
2726mpteq2dva 4533 . . . 4  |-  ( ph  ->  ( y  e.  D  |->  if ( y  e.  ( X supp  .0.  ) ,  ( X `  y ) ,  .0.  ) )  =  ( y  e.  D  |->  ( X `  y ) ) )
287, 27eqtr4d 2511 . . 3  |-  ( ph  ->  X  =  ( y  e.  D  |->  if ( y  e.  ( X supp 
.0.  ) ,  ( X `  y ) ,  .0.  ) ) )
29 suppssdm 6914 . . . . 5  |-  ( X supp 
.0.  )  C_  dom  X
30 fdm 5735 . . . . . 6  |-  ( X : D --> ( Base `  R )  ->  dom  X  =  D )
316, 30syl 16 . . . . 5  |-  ( ph  ->  dom  X  =  D )
3229, 31syl5sseq 3552 . . . 4  |-  ( ph  ->  ( X supp  .0.  )  C_  D )
33 eqid 2467 . . . . . . . . 9  |-  ( I mPwSer  R )  =  ( I mPwSer  R )
34 eqid 2467 . . . . . . . . 9  |-  ( Base `  ( I mPwSer  R ) )  =  ( Base `  ( I mPwSer  R ) )
351, 33, 34, 17, 3mplelbas 17886 . . . . . . . 8  |-  ( X  e.  B  <->  ( X  e.  ( Base `  (
I mPwSer  R ) )  /\  X finSupp  .0.  ) )
3635simprbi 464 . . . . . . 7  |-  ( X  e.  B  ->  X finSupp  .0.  )
375, 36syl 16 . . . . . 6  |-  ( ph  ->  X finSupp  .0.  )
3837fsuppimpd 7836 . . . . 5  |-  ( ph  ->  ( X supp  .0.  )  e.  Fin )
39 sseq1 3525 . . . . . . . 8  |-  ( w  =  (/)  ->  ( w 
C_  D  <->  (/)  C_  D
) )
40 mpteq1 4527 . . . . . . . . . . . 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 5708 . . . . . . . . . . . 12  |-  ( k  e.  (/)  |->  ( ( X `
 k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) )  =  (/)
4240, 41syl6eq 2524 . . . . . . . . . . 11  |-  ( w  =  (/)  ->  ( k  e.  w  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) )  =  (/) )
4342oveq2d 6300 . . . . . . . . . 10  |-  ( w  =  (/)  ->  ( P 
gsumg  ( k  e.  w  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( P 
gsumg  (/) ) )
44 eqid 2467 . . . . . . . . . . 11  |-  ( 0g
`  P )  =  ( 0g `  P
)
4544gsum0 15832 . . . . . . . . . 10  |-  ( P 
gsumg  (/) )  =  ( 0g
`  P )
4643, 45syl6eq 2524 . . . . . . . . 9  |-  ( w  =  (/)  ->  ( P 
gsumg  ( k  e.  w  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) )  =  ( 0g
`  P ) )
47 noel 3789 . . . . . . . . . . . 12  |-  -.  y  e.  (/)
48 eleq2 2540 . . . . . . . . . . . 12  |-  ( w  =  (/)  ->  ( y  e.  w  <->  y  e.  (/) ) )
4947, 48mtbiri 303 . . . . . . . . . . 11  |-  ( w  =  (/)  ->  -.  y  e.  w )
50 iffalse 3948 . . . . . . . . . . 11  |-  ( -.  y  e.  w  ->  if ( y  e.  w ,  ( X `  y ) ,  .0.  )  =  .0.  )
5149, 50syl 16 . . . . . . . . . 10  |-  ( w  =  (/)  ->  if ( y  e.  w ,  ( X `  y
) ,  .0.  )  =  .0.  )
5251mpteq2dv 4534 . . . . . . . . 9  |-  ( w  =  (/)  ->  ( y  e.  D  |->  if ( y  e.  w ,  ( X `  y
) ,  .0.  )
)  =  ( y  e.  D  |->  .0.  )
)
5346, 52eqeq12d 2489 . . . . . . . 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.  ) ) )
5439, 53imbi12d 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.  )
) ) )
5554imbi2d 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.  ) ) ) ) )
56 sseq1 3525 . . . . . . . 8  |-  ( w  =  x  ->  (
w  C_  D  <->  x  C_  D
) )
57 mpteq1 4527 . . . . . . . . . 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.  ) ) ) ) )
5857oveq2d 6300 . . . . . . . . 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.  ) ) ) ) ) )
59 eleq2 2540 . . . . . . . . . . 11  |-  ( w  =  x  ->  (
y  e.  w  <->  y  e.  x ) )
6059ifbid 3961 . . . . . . . . . 10  |-  ( w  =  x  ->  if ( y  e.  w ,  ( X `  y ) ,  .0.  )  =  if (
y  e.  x ,  ( X `  y
) ,  .0.  )
)
6160mpteq2dv 4534 . . . . . . . . 9  |-  ( w  =  x  ->  (
y  e.  D  |->  if ( y  e.  w ,  ( X `  y ) ,  .0.  ) )  =  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) ) )
6258, 61eqeq12d 2489 . . . . . . . 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.  ) ) ) )
6356, 62imbi12d 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.  ) ) ) ) )
6463imbi2d 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.  )
) ) ) ) )
65 sseq1 3525 . . . . . . . 8  |-  ( w  =  ( x  u. 
{ z } )  ->  ( w  C_  D 
<->  ( x  u.  {
z } )  C_  D ) )
66 mpteq1 4527 . . . . . . . . . 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.  )
) ) ) )
6766oveq2d 6300 . . . . . . . . 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.  ) ) ) ) ) )
68 eleq2 2540 . . . . . . . . . . 11  |-  ( w  =  ( x  u. 
{ z } )  ->  ( y  e.  w  <->  y  e.  ( x  u.  { z } ) ) )
6968ifbid 3961 . . . . . . . . . 10  |-  ( w  =  ( x  u. 
{ z } )  ->  if ( y  e.  w ,  ( X `  y ) ,  .0.  )  =  if ( y  e.  ( x  u.  {
z } ) ,  ( X `  y
) ,  .0.  )
)
7069mpteq2dv 4534 . . . . . . . . 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.  ) ) )
7167, 70eqeq12d 2489 . . . . . . . 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.  ) ) ) )
7265, 71imbi12d 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.  ) ) ) ) )
7372imbi2d 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.  ) ) ) ) ) )
74 sseq1 3525 . . . . . . . 8  |-  ( w  =  ( X supp  .0.  )  ->  ( w  C_  D 
<->  ( X supp  .0.  )  C_  D ) )
75 mpteq1 4527 . . . . . . . . . 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.  ) ) ) ) )
7675oveq2d 6300 . . . . . . . . 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.  )
) ) ) ) )
77 eleq2 2540 . . . . . . . . . . 11  |-  ( w  =  ( X supp  .0.  )  ->  ( y  e.  w  <->  y  e.  ( X supp  .0.  ) )
)
7877ifbid 3961 . . . . . . . . . 10  |-  ( w  =  ( X supp  .0.  )  ->  if ( y  e.  w ,  ( X `  y ) ,  .0.  )  =  if ( y  e.  ( X supp  .0.  ) ,  ( X `  y ) ,  .0.  ) )
7978mpteq2dv 4534 . . . . . . . . 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.  ) ) )
8076, 79eqeq12d 2489 . . . . . . . 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.  ) ) ) )
8174, 80imbi12d 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.  ) ) ) ) )
8281imbi2d 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.  ) ) ) ) ) )
83 mplcoe1.i . . . . . . . . 9  |-  ( ph  ->  I  e.  W )
84 mplcoe1.r . . . . . . . . . 10  |-  ( ph  ->  R  e.  Ring )
85 rnggrp 17005 . . . . . . . . . 10  |-  ( R  e.  Ring  ->  R  e. 
Grp )
8684, 85syl 16 . . . . . . . . 9  |-  ( ph  ->  R  e.  Grp )
871, 4, 17, 44, 83, 86mpl0 17902 . . . . . . . 8  |-  ( ph  ->  ( 0g `  P
)  =  ( D  X.  {  .0.  }
) )
88 fconstmpt 5043 . . . . . . . 8  |-  ( D  X.  {  .0.  }
)  =  ( y  e.  D  |->  .0.  )
8987, 88syl6eq 2524 . . . . . . 7  |-  ( ph  ->  ( 0g `  P
)  =  ( y  e.  D  |->  .0.  )
)
9089a1d 25 . . . . . 6  |-  ( ph  ->  ( (/)  C_  D  -> 
( 0g `  P
)  =  ( y  e.  D  |->  .0.  )
) )
91 ssun1 3667 . . . . . . . . . . 11  |-  x  C_  ( x  u.  { z } )
92 sstr2 3511 . . . . . . . . . . 11  |-  ( x 
C_  ( x  u. 
{ z } )  ->  ( ( x  u.  { z } )  C_  D  ->  x 
C_  D ) )
9391, 92ax-mp 5 . . . . . . . . . 10  |-  ( ( x  u.  { z } )  C_  D  ->  x  C_  D )
9493imim1i 58 . . . . . . . . 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.  ) ) ) )
95 oveq1 6291 . . . . . . . . . . . 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.  ) ) ) ) )
96 eqid 2467 . . . . . . . . . . . . . 14  |-  ( +g  `  P )  =  ( +g  `  P )
971mplrng 17913 . . . . . . . . . . . . . . . . 17  |-  ( ( I  e.  W  /\  R  e.  Ring )  ->  P  e.  Ring )
9883, 84, 97syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  P  e.  Ring )
99 rngcmn 17030 . . . . . . . . . . . . . . . 16  |-  ( P  e.  Ring  ->  P  e. CMnd
)
10098, 99syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  P  e. CMnd )
101100adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  P  e. CMnd )
102 simprll 761 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  x  e.  Fin )
103 simprr 756 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( x  u. 
{ z } ) 
C_  D )
104103unssad 3681 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  x  C_  D
)
105104sselda 3504 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  /\  k  e.  x
)  ->  k  e.  D )
10683adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  D )  ->  I  e.  W )
10784adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  D )  ->  R  e.  Ring )
1081mpllmod 17912 . . . . . . . . . . . . . . . . . 18  |-  ( ( I  e.  W  /\  R  e.  Ring )  ->  P  e.  LMod )
109106, 107, 108syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  D )  ->  P  e.  LMod )
1106ffvelrnda 6021 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  D )  ->  ( X `  k )  e.  ( Base `  R
) )
1111, 83, 84mplsca 17906 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  R  =  (Scalar `  P ) )
112111adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  D )  ->  R  =  (Scalar `  P )
)
113112fveq2d 5870 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  D )  ->  ( Base `  R )  =  ( Base `  (Scalar `  P ) ) )
114110, 113eleqtrd 2557 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  D )  ->  ( X `  k )  e.  ( Base `  (Scalar `  P ) ) )
115 mplcoe1.o . . . . . . . . . . . . . . . . . 18  |-  .1.  =  ( 1r `  R )
116 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  D )  ->  k  e.  D )
1171, 3, 17, 115, 4, 106, 107, 116mplmon 17924 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  D )  ->  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) )  e.  B
)
118 eqid 2467 . . . . . . . . . . . . . . . . . 18  |-  (Scalar `  P )  =  (Scalar `  P )
119 mplcoe1.n . . . . . . . . . . . . . . . . . 18  |-  .x.  =  ( .s `  P )
120 eqid 2467 . . . . . . . . . . . . . . . . . 18  |-  ( Base `  (Scalar `  P )
)  =  ( Base `  (Scalar `  P )
)
1213, 118, 119, 120lmodvscl 17329 . . . . . . . . . . . . . . . . 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 )
122109, 114, 117, 121syl3anc 1228 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  D )  ->  (
( X `  k
)  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  )
) )  e.  B
)
123122adantlr 714 . . . . . . . . . . . . . . 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 )
124105, 123syldan 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 )
125 vex 3116 . . . . . . . . . . . . . . 15  |-  z  e. 
_V
126125a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  z  e.  _V )
127 simprlr 762 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  -.  z  e.  x )
12883, 84, 108syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  P  e.  LMod )
129128adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  P  e.  LMod )
1306adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  X : D --> ( Base `  R )
)
131103unssbd 3682 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  { z } 
C_  D )
132125snss 4151 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  D  <->  { z }  C_  D )
133131, 132sylibr 212 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  z  e.  D
)
134130, 133ffvelrnd 6022 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( X `  z )  e.  (
Base `  R )
)
135111adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  R  =  (Scalar `  P ) )
136135fveq2d 5870 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( Base `  R
)  =  ( Base `  (Scalar `  P )
) )
137134, 136eleqtrd 2557 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( X `  z )  e.  (
Base `  (Scalar `  P
) ) )
13883adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  I  e.  W
)
13984adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  R  e.  Ring )
1401, 3, 17, 115, 4, 138, 139, 133mplmon 17924 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( y  e.  D  |->  if ( y  =  z ,  .1.  ,  .0.  ) )  e.  B )
1413, 118, 119, 120lmodvscl 17329 . . . . . . . . . . . . . . 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 )
142129, 137, 140, 141syl3anc 1228 . . . . . . . . . . . . . 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 )
143 fveq2 5866 . . . . . . . . . . . . . . 15  |-  ( k  =  z  ->  ( X `  k )  =  ( X `  z ) )
144 equequ2 1748 . . . . . . . . . . . . . . . . 17  |-  ( k  =  z  ->  (
y  =  k  <->  y  =  z ) )
145144ifbid 3961 . . . . . . . . . . . . . . . 16  |-  ( k  =  z  ->  if ( y  =  k ,  .1.  ,  .0.  )  =  if (
y  =  z ,  .1.  ,  .0.  )
)
146145mpteq2dv 4534 . . . . . . . . . . . . . . 15  |-  ( k  =  z  ->  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) )  =  ( y  e.  D  |->  if ( y  =  z ,  .1.  ,  .0.  ) ) )
147143, 146oveq12d 6302 . . . . . . . . . . . . . 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.  )
) ) )
1483, 96, 101, 102, 124, 126, 127, 142, 147gsumunsn 16789 . . . . . . . . . . . . 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.  ) ) ) ) )
149 eqid 2467 . . . . . . . . . . . . . . 15  |-  ( +g  `  R )  =  ( +g  `  R )
150130ffvelrnda 6021 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  /\  y  e.  D
)  ->  ( X `  y )  e.  (
Base `  R )
)
1512, 17rng0cl 17021 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( R  e.  Ring  ->  .0.  e.  ( Base `  R )
)
15284, 151syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  .0.  e.  ( Base `  R ) )
153152ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  /\  y  e.  D
)  ->  .0.  e.  ( Base `  R )
)
154150, 153ifcld 3982 . . . . . . . . . . . . . . . . . . 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
) )
155 eqid 2467 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y
) ,  .0.  )
)  =  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y
) ,  .0.  )
)
156154, 155fmptd 6045 . . . . . . . . . . . . . . . . . 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 ) )
157 fvex 5876 . . . . . . . . . . . . . . . . . . 19  |-  ( Base `  R )  e.  _V
158157, 15elmap 7447 . . . . . . . . . . . . . . . . . 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 )
)
159156, 158sylibr 212 . . . . . . . . . . . . . . . . 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
) )
16033, 2, 4, 34, 138psrbas 17829 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( Base `  (
I mPwSer  R ) )  =  ( ( Base `  R
)  ^m  D )
)
161159, 160eleqtrrd 2558 . . . . . . . . . . . . . . . 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 ) ) )
16215mptex 6131 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  D  |->  if ( y  e.  x ,  ( X `  y
) ,  .0.  )
)  e.  _V
163 funmpt 5624 . . . . . . . . . . . . . . . . . . 19  |-  Fun  (
y  e.  D  |->  if ( y  e.  x ,  ( X `  y ) ,  .0.  ) )
164162, 163, 193pm3.2i 1174 . . . . . . . . . . . . . . . . . 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 )
165164a1i 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 ) )
166 eldifn 3627 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( D  \  x )  ->  -.  y  e.  x )
167166adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  /\  y  e.  ( D  \  x ) )  ->  -.  y  e.  x )
168 iffalse 3948 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  y  e.  x  ->  if ( y  e.  x ,  ( X `  y ) ,  .0.  )  =  .0.  )
169167, 168syl 16 . . . . . . . . . . . . . . . . . 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.  )
17015a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  D  e.  _V )
171169, 170suppss2 6934 . . . . . . . . . . . . . . . . 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 )
172 suppssfifsupp 7844 . . . . . . . . . . . . . . . . 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.  )
173165, 102, 171, 172syl12anc 1226 . . . . . . . . . . . . . . . 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.  )
1741, 33, 34, 17, 3mplelbas 17886 . . . . . . . . . . . . . . . 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.  ) )
175161, 173, 174sylanbrc 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 )
1761, 3, 149, 96, 175, 142mpladd 17903 . . . . . . . . . . . . . 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.  ) ) ) ) )
177 ovex 6309 . . . . . . . . . . . . . . . 16  |-  ( ( X `  z ) ( .r `  R
) if ( y  =  z ,  .1.  ,  .0.  ) )  e. 
_V
178177a1i 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 )
179 eqidd 2468 . . . . . . . . . . . . . . 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.  ) ) )
180 eqid 2467 . . . . . . . . . . . . . . . . 17  |-  ( .r
`  R )  =  ( .r `  R
)
1811, 119, 2, 3, 180, 4, 134, 140mplvsca 17908 . . . . . . . . . . . . . . . 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.  ) ) ) )
182134adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  /\  y  e.  D
)  ->  ( X `  z )  e.  (
Base `  R )
)
1832, 115rngidcl 17020 . . . . . . . . . . . . . . . . . . . 20  |-  ( R  e.  Ring  ->  .1.  e.  ( Base `  R )
)
184183, 151ifcld 3982 . . . . . . . . . . . . . . . . . . 19  |-  ( R  e.  Ring  ->  if ( y  =  z ,  .1.  ,  .0.  )  e.  ( Base `  R
) )
18584, 184syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  if ( y  =  z ,  .1.  ,  .0.  )  e.  ( Base `  R ) )
186185ad2antrr 725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  /\  y  e.  D
)  ->  if (
y  =  z ,  .1.  ,  .0.  )  e.  ( Base `  R
) )
187 fconstmpt 5043 . . . . . . . . . . . . . . . . . 18  |-  ( D  X.  { ( X `
 z ) } )  =  ( y  e.  D  |->  ( X `
 z ) )
188187a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( D  X.  { ( X `  z ) } )  =  ( y  e.  D  |->  ( X `  z ) ) )
189 eqidd 2468 . . . . . . . . . . . . . . . . 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.  ) ) )
190170, 182, 186, 188, 189offval2 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.  ) ) ) )
191181, 190eqtrd 2508 . . . . . . . . . . . . . . 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.  ) ) ) )
192170, 154, 178, 179, 191offval2 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.  ) ) ) ) )
193139, 85syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  R  e.  Grp )
1942, 149, 17grplid 15890 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R  e.  Grp  /\  ( X `  z )  e.  ( Base `  R
) )  ->  (  .0.  ( +g  `  R
) ( X `  z ) )  =  ( X `  z
) )
195193, 134, 194syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  (  .0.  ( +g  `  R ) ( X `  z ) )  =  ( X `
 z ) )
196195ad2antrr 725 . . . . . . . . . . . . . . . . . 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 ) )
197 simpr 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  y  e.  { z } )  ->  y  e.  {
z } )
198 elsn 4041 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  { z }  <-> 
y  =  z )
199197, 198sylib 196 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  y  e.  { z } )  ->  y  =  z )
200199fveq2d 5870 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  y  e.  { z } )  ->  ( X `  y )  =  ( X `  z ) )
201196, 200eqtr4d 2511 . . . . . . . . . . . . . . . . 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 ) )
202127ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  y  e.  { z } )  ->  -.  z  e.  x )
203199, 202eqneltrd 2576 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  y  e.  { z } )  ->  -.  y  e.  x )
204203, 168syl 16 . . . . . . . . . . . . . . . . . 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.  )
205 iftrue 3945 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  z  ->  if ( y  =  z ,  .1.  ,  .0.  )  =  .1.  )
206199, 205syl 16 . . . . . . . . . . . . . . . . . . . 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.  )
207206oveq2d 6300 . . . . . . . . . . . . . . . . . . 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.  )
)
2082, 180, 115rngridm 17024 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e.  Ring  /\  ( X `  z )  e.  ( Base `  R
) )  ->  (
( X `  z
) ( .r `  R )  .1.  )  =  ( X `  z ) )
209139, 134, 208syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( ( X `
 z ) ( .r `  R )  .1.  )  =  ( X `  z ) )
210209ad2antrr 725 . . . . . . . . . . . . . . . . . . 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 ) )
211207, 210eqtrd 2508 . . . . . . . . . . . . . . . . . 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 ) )
212204, 211oveq12d 6302 . . . . . . . . . . . . . . . . 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 ) ) )
213 elun2 3672 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  { z }  ->  y  e.  ( x  u.  { z } ) )
214213adantl 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 } ) )
215 iftrue 3945 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( x  u. 
{ z } )  ->  if ( y  e.  ( x  u. 
{ z } ) ,  ( X `  y ) ,  .0.  )  =  ( X `  y ) )
216214, 215syl 16 . . . . . . . . . . . . . . . . 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 ) )
217201, 212, 2163eqtr4d 2518 . . . . . . . . . . . . . . . 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.  )
)
21886ad2antrr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  /\  y  e.  D
)  ->  R  e.  Grp )
2192, 149, 17grprid 15891 . . . . . . . . . . . . . . . . . . 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.  ) )
220218, 154, 219syl2anc 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.  ) )
221220adantr 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.  ) )
222 simpr 461 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  -.  y  e.  { z } )  ->  -.  y  e.  { z } )
223222, 198sylnib 304 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  D
) )  /\  y  e.  D )  /\  -.  y  e.  { z } )  ->  -.  y  =  z )
224 iffalse 3948 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -.  y  =  z  ->  if ( y  =  z ,  .1.  ,  .0.  )  =  .0.  )
225223, 224syl 16 . . . . . . . . . . . . . . . . . . . 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.  )
226225oveq2d 6300 . . . . . . . . . . . . . . . . . . 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.  ) )
2272, 180, 17rngrz 17037 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e.  Ring  /\  ( X `  z )  e.  ( Base `  R
) )  ->  (
( X `  z
) ( .r `  R )  .0.  )  =  .0.  )
228139, 134, 227syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  D ) )  ->  ( ( X `
 z ) ( .r `  R )  .0.  )  =  .0.  )
229228ad2antrr 725 . . . . . . . . . . . . . . . . . . 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.  )
230226, 229eqtrd 2508 . . . . . . . . . . . . . . . . . 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.  )
231230oveq2d 6300 . . . . . . . . . . . . . . . . 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.  ) )
232 biorf 405 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  y  e.  { z }  ->  ( y  e.  x  <->  ( y  e. 
{ z }  \/  y  e.  x )
) )
233 elun 3645 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( x  u. 
{ z } )  <-> 
( y  e.  x  \/  y  e.  { z } ) )
234 orcom 387 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  e.  x  \/  y  e.  { z } )  <->  ( y  e.  { z }  \/  y  e.  x )
)
235233, 234bitri 249 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( x  u. 
{ z } )  <-> 
( y  e.  {
z }  \/  y  e.  x ) )
236232, 235syl6rbbr 264 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  y  e.  { z }  ->  ( y  e.  ( x  u.  {
z } )  <->  y  e.  x ) )
237236adantl 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
) )
238237ifbid 3961 . . . . . . . . . . . . . . . . 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.  ) )
239221, 231, 2383eqtr4d 2518 . . . . . . . . . . . . . . . 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.  )
)
240217, 239pm2.61dan 789 . . . . . . . . . . . . . . 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.  )
)
241240mpteq2dva 4533 . . . . . . . . . . . . . 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.  ) ) )
242176, 192, 2413eqtrrd 2513 . . . . . . . . . . . . 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.  ) ) ) ) )
243148, 242eqeq12d 2489 . . . . . . . . . . . 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.  ) ) ) ) ) )
24495, 243syl5ibr 221 . . . . . . . . . . 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.  ) ) ) )
245244expr 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.  ) ) ) ) )
246245a2d 26 . . . . . . . . 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.  ) ) ) ) )
24794, 246syl5 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.  ) ) ) ) )
248247expcom 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.  ) ) ) ) ) )
249248a2d 26 . . . . . 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.  ) ) ) ) ) )
25055, 64, 73, 82, 90, 249findcard2s 7761 . . . . 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.  )
) ) ) )
25138, 250mpcom 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.  ) ) ) )
25232, 251mpd 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.  ) ) )
25328, 252eqtr4d 2511 . 2  |-  ( ph  ->  X  =  ( P 
gsumg  ( k  e.  ( X supp  .0.  )  |->  ( ( X `  k
)  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  )
) ) ) ) )
254 resmpt 5323 . . . . 5  |-  ( ( X supp  .0.  )  C_  D  ->  ( ( 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.  ) ) ) ) )
25532, 254syl 16 . . . 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.  ) ) ) ) )
256255oveq2d 6300 . . 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.  )
) ) ) ) )
257 eqid 2467 . . . . 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.  ) ) ) )
258122, 257fmptd 6045 . . . 4  |-  ( ph  ->  ( k  e.  D  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) : D --> B )
2596, 13, 16, 20suppssr 6931 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( D  \  ( X supp  .0.  ) ) )  ->  ( X `  k )  =  .0.  )
260259oveq1d 6299 . . . . . 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.  ) ) ) )
261 eldifi 3626 . . . . . . 7  |-  ( k  e.  ( D  \ 
( X supp  .0.  )
)  ->  k  e.  D )
262112fveq2d 5870 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  D )  ->  ( 0g `  R )  =  ( 0g `  (Scalar `  P ) ) )
26317, 262syl5eq 2520 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  D )  ->  .0.  =  ( 0g `  (Scalar `  P ) ) )
264263oveq1d 6299 . . . . . . . 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.  )
) ) )
265 eqid 2467 . . . . . . . . . 10  |-  ( 0g
`  (Scalar `  P )
)  =  ( 0g
`  (Scalar `  P )
)
2663, 118, 119, 265, 44lmod0vs 17345 . . . . . . . . 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
) )
267109, 117, 266syl2anc 661 . . . . . . . 8  |-  ( (
ph  /\  k  e.  D )  ->  (
( 0g `  (Scalar `  P ) )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) )  =  ( 0g `  P
) )
268264, 267eqtrd 2508 . . . . . . 7  |-  ( (
ph  /\  k  e.  D )  ->  (  .0.  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) )  =  ( 0g `  P ) )
269261, 268sylan2 474 . . . . . 6  |-  ( (
ph  /\  k  e.  ( D  \  ( X supp  .0.  ) ) )  ->  (  .0.  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) )  =  ( 0g `  P
) )
270260, 269eqtrd 2508 . . . . 5  |-  ( (
ph  /\  k  e.  ( D  \  ( X supp  .0.  ) ) )  ->  ( ( X `
 k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) )  =  ( 0g `  P
) )
271270, 16suppss2 6934 . . . 4  |-  ( ph  ->  ( ( k  e.  D  |->  ( ( X `
 k )  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) supp  ( 0g `  P
) )  C_  ( X supp  .0.  ) )
27215mptex 6131 . . . . . . 7  |-  ( k  e.  D  |->  ( ( X `  k ) 
.x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) )  e.  _V
273 funmpt 5624 . . . . . . 7  |-  Fun  (
k  e.  D  |->  ( ( X `  k
)  .x.  ( y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  )
) ) )
274 fvex 5876 . . . . . . 7  |-  ( 0g
`  P )  e. 
_V
275272, 273, 2743pm3.2i 1174 . . . . . 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 )
276275a1i 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 ) )
277 suppssfifsupp 7844 . . . . 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
) )
278276, 38, 271, 277syl12anc 1226 . . . 4  |-  ( ph  ->  ( k  e.  D  |->  ( ( X `  k )  .x.  (
y  e.  D  |->  if ( y  =  k ,  .1.  ,  .0.  ) ) ) ) finSupp 
( 0g `  P
) )
2793, 44, 100, 16, 258, 271, 278gsumres 16724 . . 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.  ) ) ) ) ) )
280256, 279eqtr3d 2510 . 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.  ) ) ) ) ) )
281253, 280eqtrd 2508 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 184    \/ wo 368    /\ wa 369    /\ w3a 973    = wceq 1379    e. wcel 1767   {crab 2818   _Vcvv 3113    \ cdif 3473    u. cun 3474    C_ wss 3476   (/)c0 3785   ifcif 3939   {csn 4027   class class class wbr 4447    |-> cmpt 4505    X. cxp 4997   `'ccnv 4998   dom cdm 4999    |` cres 5001   "cima 5002   Fun wfun 5582   -->wf 5584   ` cfv 5588  (class class class)co 6284    oFcof 6522   supp csupp 6901    ^m cmap 7420   Fincfn 7516   finSupp cfsupp 7829   NNcn 10536   NN0cn0 10795   Basecbs 14490   +g cplusg 14555   .rcmulr 14556  Scalarcsca 14558   .scvsca 14559   0gc0g 14695    gsumg cgsu 14696   Grpcgrp 15727  CMndccmn 16604   1rcur 16955   Ringcrg 17000   LModclmod 17312   mPwSer cmps 17799   mPoly cmpl 17801
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-inf2 8058  ax-cnex 9548  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-mulcom 9556  ax-addass 9557  ax-mulass 9558  ax-distr 9559  ax-i2m1 9560  ax-1ne0 9561  ax-1rid 9562  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565  ax-pre-lttri 9566  ax-pre-lttrn 9567  ax-pre-ltadd 9568  ax-pre-mulgt0 9569
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-iin 4328  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-isom 5597  df-riota 6245  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-of 6524  df-ofr 6525  df-om 6685  df-1st 6784  df-2nd 6785  df-supp 6902  df-recs 7042  df-rdg 7076  df-1o 7130  df-2o 7131  df-oadd 7134  df-er 7311  df-map 7422  df-pm 7423  df-ixp 7470  df-en 7517  df-dom 7518  df-sdom 7519  df-fin 7520  df-fsupp 7830  df-oi 7935  df-card 8320  df-pnf 9630  df-mnf 9631  df-xr 9632  df-ltxr 9633  df-le 9634  df-sub 9807  df-neg 9808  df-nn 10537  df-2 10594  df-3 10595  df-4 10596  df-5 10597  df-6 10598  df-7 10599  df-8 10600  df-9 10601  df-n0 10796  df-z 10865  df-uz 11083  df-fz 11673  df-fzo 11793  df-seq 12076  df-hash 12374  df-struct 14492  df-ndx 14493  df-slot 14494  df-base 14495  df-sets 14496  df-ress 14497  df-plusg 14568  df-mulr 14569  df-sca 14571  df-vsca 14572  df-tset 14574  df-0g 14697  df-gsum 14698  df-mre 14841  df-mrc 14842  df-acs 14844  df-mnd 15732  df-mhm 15786  df-submnd 15787  df-grp 15867  df-minusg 15868  df-sbg 15869  df-mulg 15870  df-subg 16003  df-ghm 16070  df-cntz 16160  df-cmn 16606  df-abl 16607  df-mgp 16944  df-ur 16956  df-rng 17002  df-subrg 17227  df-lmod 17314  df-lss 17379  df-psr 17804  df-mpl 17806
This theorem is referenced by:  mplbas2  17933  mplbas2OLD  17934  mplcoe4  17967  ply1coe  18136  ply1coeOLD  18137
  Copyright terms: Public domain W3C validator