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

Theorem mplcoe2 17524
Description: Decompose a monomial into a finite product of powers of variables. (The assumption that  R is a commutative ring is not strictly necessary, because the submonoid of monomials is in the center of the multiplicative monoid of polynomials, but it simplifies the proof.) (Contributed by Mario Carneiro, 10-Jan-2015.) (Proof shortened by AV, 18-Jul-2019.)
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 )
mplcoe2.g  |-  G  =  (mulGrp `  P )
mplcoe2.m  |-  .^  =  (.g
`  G )
mplcoe2.v  |-  V  =  ( I mVar  R )
mplcoe2.r  |-  ( ph  ->  R  e.  CRing )
mplcoe2.y  |-  ( ph  ->  Y  e.  D )
Assertion
Ref Expression
mplcoe2  |-  ( ph  ->  ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  I  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) )
Distinct variable groups:    .^ , k    y,
k,  .1.    k, G    f,
k, y, I    ph, k,
y    R, f, y    D, k, y    P, k    k, V    .0. , f, k, y   
f, Y, k, y   
k, W, y
Allowed substitution hints:    ph( f)    D( f)    P( y, f)    R( k)    .1. ( f)    .^ ( y, f)    G( y, f)    V( y, f)    W( f)

Proof of Theorem mplcoe2
Dummy variables  i  w  x  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mplcoe2.y . . . . . . . . 9  |-  ( ph  ->  Y  e.  D )
2 mplcoe1.i . . . . . . . . . 10  |-  ( ph  ->  I  e.  W )
3 mplcoe1.d . . . . . . . . . . 11  |-  D  =  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin }
43psrbag 17408 . . . . . . . . . 10  |-  ( I  e.  W  ->  ( Y  e.  D  <->  ( Y : I --> NN0  /\  ( `' Y " NN )  e.  Fin ) ) )
52, 4syl 16 . . . . . . . . 9  |-  ( ph  ->  ( Y  e.  D  <->  ( Y : I --> NN0  /\  ( `' Y " NN )  e.  Fin ) ) )
61, 5mpbid 210 . . . . . . . 8  |-  ( ph  ->  ( Y : I --> NN0  /\  ( `' Y " NN )  e.  Fin ) )
76simpld 459 . . . . . . 7  |-  ( ph  ->  Y : I --> NN0 )
87feqmptd 5739 . . . . . 6  |-  ( ph  ->  Y  =  ( i  e.  I  |->  ( Y `
 i ) ) )
9 iftrue 3792 . . . . . . . . 9  |-  ( i  e.  ( `' Y " NN )  ->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 )  =  ( Y `
 i ) )
109adantl 466 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  I )  /\  i  e.  ( `' Y " NN ) )  ->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 )  =  ( Y `
 i ) )
11 eldif 3333 . . . . . . . . . 10  |-  ( i  e.  ( I  \ 
( `' Y " NN ) )  <->  ( i  e.  I  /\  -.  i  e.  ( `' Y " NN ) ) )
12 ifid 3821 . . . . . . . . . . 11  |-  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  ( Y `  i ) )  =  ( Y `
 i )
13 frnnn0supp 10625 . . . . . . . . . . . . . . 15  |-  ( ( I  e.  W  /\  Y : I --> NN0 )  ->  ( Y supp  0 )  =  ( `' Y " NN ) )
142, 7, 13syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Y supp  0 )  =  ( `' Y " NN ) )
15 eqimss 3403 . . . . . . . . . . . . . 14  |-  ( ( Y supp  0 )  =  ( `' Y " NN )  ->  ( Y supp  0 )  C_  ( `' Y " NN ) )
1614, 15syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Y supp  0 ) 
C_  ( `' Y " NN ) )
17 c0ex 9372 . . . . . . . . . . . . . 14  |-  0  e.  _V
1817a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  0  e.  _V )
197, 16, 2, 18suppssr 6715 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( I  \  ( `' Y " NN ) ) )  ->  ( Y `  i )  =  0 )
2019ifeq2d 3803 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( I  \  ( `' Y " NN ) ) )  ->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  ( Y `  i ) )  =  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 ) )
2112, 20syl5reqr 2485 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( I  \  ( `' Y " NN ) ) )  ->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 )  =  ( Y `
 i ) )
2211, 21sylan2br 476 . . . . . . . . 9  |-  ( (
ph  /\  ( i  e.  I  /\  -.  i  e.  ( `' Y " NN ) ) )  ->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 )  =  ( Y `
 i ) )
2322anassrs 648 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  I )  /\  -.  i  e.  ( `' Y " NN ) )  ->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 )  =  ( Y `  i
) )
2410, 23pm2.61dan 789 . . . . . . 7  |-  ( (
ph  /\  i  e.  I )  ->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 )  =  ( Y `
 i ) )
2524mpteq2dva 4373 . . . . . 6  |-  ( ph  ->  ( i  e.  I  |->  if ( i  e.  ( `' Y " NN ) ,  ( Y `
 i ) ,  0 ) )  =  ( i  e.  I  |->  ( Y `  i
) ) )
268, 25eqtr4d 2473 . . . . 5  |-  ( ph  ->  Y  =  ( i  e.  I  |->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 ) ) )
2726eqeq2d 2449 . . . 4  |-  ( ph  ->  ( y  =  Y  <-> 
y  =  ( i  e.  I  |->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 ) ) ) )
2827ifbid 3806 . . 3  |-  ( ph  ->  if ( y  =  Y ,  .1.  ,  .0.  )  =  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )
2928mpteq2dv 4374 . 2  |-  ( ph  ->  ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) )  =  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) ) )
30 cnvimass 5184 . . . . 5  |-  ( `' Y " NN ) 
C_  dom  Y
31 fdm 5558 . . . . . 6  |-  ( Y : I --> NN0  ->  dom 
Y  =  I )
327, 31syl 16 . . . . 5  |-  ( ph  ->  dom  Y  =  I )
3330, 32syl5sseq 3399 . . . 4  |-  ( ph  ->  ( `' Y " NN )  C_  I )
346simprd 463 . . . . 5  |-  ( ph  ->  ( `' Y " NN )  e.  Fin )
35 sseq1 3372 . . . . . . . 8  |-  ( w  =  (/)  ->  ( w 
C_  I  <->  (/)  C_  I
) )
36 noel 3636 . . . . . . . . . . . . . . . 16  |-  -.  i  e.  (/)
37 eleq2 2499 . . . . . . . . . . . . . . . 16  |-  ( w  =  (/)  ->  ( i  e.  w  <->  i  e.  (/) ) )
3836, 37mtbiri 303 . . . . . . . . . . . . . . 15  |-  ( w  =  (/)  ->  -.  i  e.  w )
39 iffalse 3794 . . . . . . . . . . . . . . 15  |-  ( -.  i  e.  w  ->  if ( i  e.  w ,  ( Y `  i ) ,  0 )  =  0 )
4038, 39syl 16 . . . . . . . . . . . . . 14  |-  ( w  =  (/)  ->  if ( i  e.  w ,  ( Y `  i
) ,  0 )  =  0 )
4140mpteq2dv 4374 . . . . . . . . . . . . 13  |-  ( w  =  (/)  ->  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i
) ,  0 ) )  =  ( i  e.  I  |->  0 ) )
42 fconstmpt 4877 . . . . . . . . . . . . 13  |-  ( I  X.  { 0 } )  =  ( i  e.  I  |->  0 )
4341, 42syl6eqr 2488 . . . . . . . . . . . 12  |-  ( w  =  (/)  ->  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i
) ,  0 ) )  =  ( I  X.  { 0 } ) )
4443eqeq2d 2449 . . . . . . . . . . 11  |-  ( w  =  (/)  ->  ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i ) ,  0 ) )  <-> 
y  =  ( I  X.  { 0 } ) ) )
4544ifbid 3806 . . . . . . . . . 10  |-  ( w  =  (/)  ->  if ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i
) ,  0 ) ) ,  .1.  ,  .0.  )  =  if ( y  =  ( I  X.  { 0 } ) ,  .1.  ,  .0.  ) )
4645mpteq2dv 4374 . . . . . . . . 9  |-  ( w  =  (/)  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i
) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( y  e.  D  |->  if ( y  =  ( I  X.  { 0 } ) ,  .1.  ,  .0.  ) ) )
47 mpteq1 4367 . . . . . . . . . . . 12  |-  ( w  =  (/)  ->  ( k  e.  w  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) )  =  ( k  e.  (/)  |->  ( ( Y `
 k )  .^  ( V `  k ) ) ) )
48 mpt0 5533 . . . . . . . . . . . 12  |-  ( k  e.  (/)  |->  ( ( Y `
 k )  .^  ( V `  k ) ) )  =  (/)
4947, 48syl6eq 2486 . . . . . . . . . . 11  |-  ( w  =  (/)  ->  ( k  e.  w  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) )  =  (/) )
5049oveq2d 6102 . . . . . . . . . 10  |-  ( w  =  (/)  ->  ( G 
gsumg  ( k  e.  w  |->  ( ( Y `  k )  .^  ( V `  k )
) ) )  =  ( G  gsumg  (/) ) )
51 mplcoe2.g . . . . . . . . . . . 12  |-  G  =  (mulGrp `  P )
52 eqid 2438 . . . . . . . . . . . 12  |-  ( 1r
`  P )  =  ( 1r `  P
)
5351, 52rngidval 16593 . . . . . . . . . . 11  |-  ( 1r
`  P )  =  ( 0g `  G
)
5453gsum0 15501 . . . . . . . . . 10  |-  ( G 
gsumg  (/) )  =  ( 1r
`  P )
5550, 54syl6eq 2486 . . . . . . . . 9  |-  ( w  =  (/)  ->  ( G 
gsumg  ( k  e.  w  |->  ( ( Y `  k )  .^  ( V `  k )
) ) )  =  ( 1r `  P
) )
5646, 55eqeq12d 2452 . . . . . . . 8  |-  ( w  =  (/)  ->  ( ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  w  |->  ( ( Y `  k )  .^  ( V `  k )
) ) )  <->  ( y  e.  D  |->  if ( y  =  ( I  X.  { 0 } ) ,  .1.  ,  .0.  ) )  =  ( 1r `  P ) ) )
5735, 56imbi12d 320 . . . . . . 7  |-  ( w  =  (/)  ->  ( ( w  C_  I  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  w  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) )  <-> 
( (/)  C_  I  ->  ( y  e.  D  |->  if ( y  =  ( I  X.  { 0 } ) ,  .1.  ,  .0.  ) )  =  ( 1r `  P
) ) ) )
5857imbi2d 316 . . . . . 6  |-  ( w  =  (/)  ->  ( (
ph  ->  ( w  C_  I  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  w  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) ) )  <->  ( ph  ->  (
(/)  C_  I  ->  (
y  e.  D  |->  if ( y  =  ( I  X.  { 0 } ) ,  .1.  ,  .0.  ) )  =  ( 1r `  P
) ) ) ) )
59 sseq1 3372 . . . . . . . 8  |-  ( w  =  x  ->  (
w  C_  I  <->  x  C_  I
) )
60 eleq2 2499 . . . . . . . . . . . . . 14  |-  ( w  =  x  ->  (
i  e.  w  <->  i  e.  x ) )
6160ifbid 3806 . . . . . . . . . . . . 13  |-  ( w  =  x  ->  if ( i  e.  w ,  ( Y `  i ) ,  0 )  =  if ( i  e.  x ,  ( Y `  i
) ,  0 ) )
6261mpteq2dv 4374 . . . . . . . . . . . 12  |-  ( w  =  x  ->  (
i  e.  I  |->  if ( i  e.  w ,  ( Y `  i ) ,  0 ) )  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) )
6362eqeq2d 2449 . . . . . . . . . . 11  |-  ( w  =  x  ->  (
y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i
) ,  0 ) )  <->  y  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) ) )
6463ifbid 3806 . . . . . . . . . 10  |-  ( w  =  x  ->  if ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  )  =  if ( y  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )
6564mpteq2dv 4374 . . . . . . . . 9  |-  ( w  =  x  ->  (
y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `
 i ) ,  0 ) ) ,  .1.  ,  .0.  )
) )
66 mpteq1 4367 . . . . . . . . . 10  |-  ( w  =  x  ->  (
k  e.  w  |->  ( ( Y `  k
)  .^  ( V `  k ) ) )  =  ( k  e.  x  |->  ( ( Y `
 k )  .^  ( V `  k ) ) ) )
6766oveq2d 6102 . . . . . . . . 9  |-  ( w  =  x  ->  ( G  gsumg  ( k  e.  w  |->  ( ( Y `  k )  .^  ( V `  k )
) ) )  =  ( G  gsumg  ( k  e.  x  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) )
6865, 67eqeq12d 2452 . . . . . . . 8  |-  ( w  =  x  ->  (
( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `
 i ) ,  0 ) ) ,  .1.  ,  .0.  )
)  =  ( G 
gsumg  ( k  e.  w  |->  ( ( Y `  k )  .^  ( V `  k )
) ) )  <->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  x  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) ) )
6959, 68imbi12d 320 . . . . . . 7  |-  ( w  =  x  ->  (
( w  C_  I  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `
 i ) ,  0 ) ) ,  .1.  ,  .0.  )
)  =  ( G 
gsumg  ( k  e.  w  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) )  <-> 
( x  C_  I  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `
 i ) ,  0 ) ) ,  .1.  ,  .0.  )
)  =  ( G 
gsumg  ( k  e.  x  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) ) ) )
7069imbi2d 316 . . . . . 6  |-  ( w  =  x  ->  (
( ph  ->  ( w 
C_  I  ->  (
y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  w  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) ) )  <->  ( ph  ->  ( x  C_  I  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  x  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) ) ) ) )
71 sseq1 3372 . . . . . . . 8  |-  ( w  =  ( x  u. 
{ z } )  ->  ( w  C_  I 
<->  ( x  u.  {
z } )  C_  I ) )
72 eleq2 2499 . . . . . . . . . . . . . 14  |-  ( w  =  ( x  u. 
{ z } )  ->  ( i  e.  w  <->  i  e.  ( x  u.  { z } ) ) )
7372ifbid 3806 . . . . . . . . . . . . 13  |-  ( w  =  ( x  u. 
{ z } )  ->  if ( i  e.  w ,  ( Y `  i ) ,  0 )  =  if ( i  e.  ( x  u.  {
z } ) ,  ( Y `  i
) ,  0 ) )
7473mpteq2dv 4374 . . . . . . . . . . . 12  |-  ( w  =  ( x  u. 
{ z } )  ->  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i ) ,  0 ) )  =  ( i  e.  I  |->  if ( i  e.  ( x  u. 
{ z } ) ,  ( Y `  i ) ,  0 ) ) )
7574eqeq2d 2449 . . . . . . . . . . 11  |-  ( w  =  ( x  u. 
{ z } )  ->  ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `
 i ) ,  0 ) )  <->  y  =  ( i  e.  I  |->  if ( i  e.  ( x  u.  {
z } ) ,  ( Y `  i
) ,  0 ) ) ) )
7675ifbid 3806 . . . . . . . . . 10  |-  ( w  =  ( x  u. 
{ z } )  ->  if ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  )  =  if (
y  =  ( i  e.  I  |->  if ( i  e.  ( x  u.  { z } ) ,  ( Y `
 i ) ,  0 ) ) ,  .1.  ,  .0.  )
)
7776mpteq2dv 4374 . . . . . . . . 9  |-  ( w  =  ( x  u. 
{ z } )  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( x  u.  { z } ) ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) ) )
78 mpteq1 4367 . . . . . . . . . 10  |-  ( w  =  ( x  u. 
{ z } )  ->  ( k  e.  w  |->  ( ( Y `
 k )  .^  ( V `  k ) ) )  =  ( k  e.  ( x  u.  { z } )  |->  ( ( Y `
 k )  .^  ( V `  k ) ) ) )
7978oveq2d 6102 . . . . . . . . 9  |-  ( w  =  ( x  u. 
{ z } )  ->  ( G  gsumg  ( k  e.  w  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) ) )  =  ( G 
gsumg  ( k  e.  ( x  u.  { z } )  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) ) ) )
8077, 79eqeq12d 2452 . . . . . . . 8  |-  ( w  =  ( x  u. 
{ z } )  ->  ( ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i
) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  w  |->  ( ( Y `  k )  .^  ( V `  k )
) ) )  <->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( x  u.  { z } ) ,  ( Y `
 i ) ,  0 ) ) ,  .1.  ,  .0.  )
)  =  ( G 
gsumg  ( k  e.  ( x  u.  { z } )  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) ) ) ) )
8171, 80imbi12d 320 . . . . . . 7  |-  ( w  =  ( x  u. 
{ z } )  ->  ( ( w 
C_  I  ->  (
y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  w  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) )  <-> 
( ( x  u. 
{ z } ) 
C_  I  ->  (
y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( x  u.  { z } ) ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  ( x  u.  { z } )  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) ) ) ) ) )
8281imbi2d 316 . . . . . 6  |-  ( w  =  ( x  u. 
{ z } )  ->  ( ( ph  ->  ( w  C_  I  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `
 i ) ,  0 ) ) ,  .1.  ,  .0.  )
)  =  ( G 
gsumg  ( k  e.  w  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) ) )  <->  ( ph  ->  ( ( x  u.  {
z } )  C_  I  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( x  u. 
{ z } ) ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  ( x  u.  { z } )  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) ) ) ) ) ) )
83 sseq1 3372 . . . . . . . 8  |-  ( w  =  ( `' Y " NN )  ->  (
w  C_  I  <->  ( `' Y " NN )  C_  I ) )
84 eleq2 2499 . . . . . . . . . . . . . 14  |-  ( w  =  ( `' Y " NN )  ->  (
i  e.  w  <->  i  e.  ( `' Y " NN ) ) )
8584ifbid 3806 . . . . . . . . . . . . 13  |-  ( w  =  ( `' Y " NN )  ->  if ( i  e.  w ,  ( Y `  i ) ,  0 )  =  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 ) )
8685mpteq2dv 4374 . . . . . . . . . . . 12  |-  ( w  =  ( `' Y " NN )  ->  (
i  e.  I  |->  if ( i  e.  w ,  ( Y `  i ) ,  0 ) )  =  ( i  e.  I  |->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 ) ) )
8786eqeq2d 2449 . . . . . . . . . . 11  |-  ( w  =  ( `' Y " NN )  ->  (
y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i
) ,  0 ) )  <->  y  =  ( i  e.  I  |->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 ) ) ) )
8887ifbid 3806 . . . . . . . . . 10  |-  ( w  =  ( `' Y " NN )  ->  if ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  )  =  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )
8988mpteq2dv 4374 . . . . . . . . 9  |-  ( w  =  ( `' Y " NN )  ->  (
y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( `' Y " NN ) ,  ( Y `
 i ) ,  0 ) ) ,  .1.  ,  .0.  )
) )
90 mpteq1 4367 . . . . . . . . . 10  |-  ( w  =  ( `' Y " NN )  ->  (
k  e.  w  |->  ( ( Y `  k
)  .^  ( V `  k ) ) )  =  ( k  e.  ( `' Y " NN )  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) ) )
9190oveq2d 6102 . . . . . . . . 9  |-  ( w  =  ( `' Y " NN )  ->  ( G  gsumg  ( k  e.  w  |->  ( ( Y `  k )  .^  ( V `  k )
) ) )  =  ( G  gsumg  ( k  e.  ( `' Y " NN ) 
|->  ( ( Y `  k )  .^  ( V `  k )
) ) ) )
9289, 91eqeq12d 2452 . . . . . . . 8  |-  ( w  =  ( `' Y " NN )  ->  (
( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `
 i ) ,  0 ) ) ,  .1.  ,  .0.  )
)  =  ( G 
gsumg  ( k  e.  w  |->  ( ( Y `  k )  .^  ( V `  k )
) ) )  <->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  ( `' Y " NN ) 
|->  ( ( Y `  k )  .^  ( V `  k )
) ) ) ) )
9383, 92imbi12d 320 . . . . . . 7  |-  ( w  =  ( `' Y " NN )  ->  (
( w  C_  I  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `
 i ) ,  0 ) ) ,  .1.  ,  .0.  )
)  =  ( G 
gsumg  ( k  e.  w  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) )  <-> 
( ( `' Y " NN )  C_  I  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( `' Y " NN ) ,  ( Y `
 i ) ,  0 ) ) ,  .1.  ,  .0.  )
)  =  ( G 
gsumg  ( k  e.  ( `' Y " NN ) 
|->  ( ( Y `  k )  .^  ( V `  k )
) ) ) ) ) )
9493imbi2d 316 . . . . . 6  |-  ( w  =  ( `' Y " NN )  ->  (
( ph  ->  ( w 
C_  I  ->  (
y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  w  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) ) )  <->  ( ph  ->  ( ( `' Y " NN )  C_  I  -> 
( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( `' Y " NN ) ,  ( Y `
 i ) ,  0 ) ) ,  .1.  ,  .0.  )
)  =  ( G 
gsumg  ( k  e.  ( `' Y " NN ) 
|->  ( ( Y `  k )  .^  ( V `  k )
) ) ) ) ) ) )
95 mplcoe1.p . . . . . . . . 9  |-  P  =  ( I mPoly  R )
96 mplcoe1.z . . . . . . . . 9  |-  .0.  =  ( 0g `  R )
97 mplcoe1.o . . . . . . . . 9  |-  .1.  =  ( 1r `  R )
98 mplcoe2.r . . . . . . . . . 10  |-  ( ph  ->  R  e.  CRing )
99 crngrng 16643 . . . . . . . . . 10  |-  ( R  e.  CRing  ->  R  e.  Ring )
10098, 99syl 16 . . . . . . . . 9  |-  ( ph  ->  R  e.  Ring )
10195, 3, 96, 97, 52, 2, 100mpl1 17500 . . . . . . . 8  |-  ( ph  ->  ( 1r `  P
)  =  ( y  e.  D  |->  if ( y  =  ( I  X.  { 0 } ) ,  .1.  ,  .0.  ) ) )
102101eqcomd 2443 . . . . . . 7  |-  ( ph  ->  ( y  e.  D  |->  if ( y  =  ( I  X.  {
0 } ) ,  .1.  ,  .0.  )
)  =  ( 1r
`  P ) )
103102a1d 25 . . . . . 6  |-  ( ph  ->  ( (/)  C_  I  -> 
( y  e.  D  |->  if ( y  =  ( I  X.  {
0 } ) ,  .1.  ,  .0.  )
)  =  ( 1r
`  P ) ) )
104 ssun1 3514 . . . . . . . . . . 11  |-  x  C_  ( x  u.  { z } )
105 sstr2 3358 . . . . . . . . . . 11  |-  ( x 
C_  ( x  u. 
{ z } )  ->  ( ( x  u.  { z } )  C_  I  ->  x 
C_  I ) )
106104, 105ax-mp 5 . . . . . . . . . 10  |-  ( ( x  u.  { z } )  C_  I  ->  x  C_  I )
107106imim1i 58 . . . . . . . . 9  |-  ( ( x  C_  I  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  x  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) )  ->  ( ( x  u.  { z } )  C_  I  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  x  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) ) )
108 oveq1 6093 . . . . . . . . . . . 12  |-  ( ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  x  |->  ( ( Y `  k )  .^  ( V `  k )
) ) )  -> 
( ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) ) ( .r
`  P ) ( ( Y `  z
)  .^  ( V `  z ) ) )  =  ( ( G 
gsumg  ( k  e.  x  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) ( .r `  P ) ( ( Y `  z )  .^  ( V `  z )
) ) )
109 eqid 2438 . . . . . . . . . . . . . . 15  |-  ( Base `  P )  =  (
Base `  P )
1102adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  I  e.  W
)
111100adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  R  e.  Ring )
1127adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  Y : I --> NN0 )
113112ffvelrnda 5838 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  /\  i  e.  I
)  ->  ( Y `  i )  e.  NN0 )
114 0nn0 10586 . . . . . . . . . . . . . . . . . 18  |-  0  e.  NN0
115 ifcl 3826 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( Y `  i
)  e.  NN0  /\  0  e.  NN0 )  ->  if ( i  e.  x ,  ( Y `  i ) ,  0 )  e.  NN0 )
116113, 114, 115sylancl 662 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  /\  i  e.  I
)  ->  if (
i  e.  x ,  ( Y `  i
) ,  0 )  e.  NN0 )
117 eqid 2438 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) )  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) )
118116, 117fmptd 5862 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) : I --> NN0 )
119 frnnn0supp 10625 . . . . . . . . . . . . . . . . . 18  |-  ( ( I  e.  W  /\  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `
 i ) ,  0 ) ) : I --> NN0 )  ->  (
( i  e.  I  |->  if ( i  e.  x ,  ( Y `
 i ) ,  0 ) ) supp  0
)  =  ( `' ( i  e.  I  |->  if ( i  e.  x ,  ( Y `
 i ) ,  0 ) ) " NN ) )
120110, 118, 119syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) ) supp  0 )  =  ( `' ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) ) " NN ) )
121 simprll 761 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  x  e.  Fin )
122 eldifn 3474 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  ( I  \  x )  ->  -.  i  e.  x )
123122adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  /\  i  e.  ( I  \  x ) )  ->  -.  i  e.  x )
124 iffalse 3794 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  i  e.  x  ->  if ( i  e.  x ,  ( Y `  i ) ,  0 )  =  0 )
125123, 124syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  /\  i  e.  ( I  \  x ) )  ->  if (
i  e.  x ,  ( Y `  i
) ,  0 )  =  0 )
126125, 110suppss2 6718 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) ) supp  0 )  C_  x )
127 ssfi 7525 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  Fin  /\  ( ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) supp  0 )  C_  x
)  ->  ( (
i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) supp  0 )  e.  Fin )
128121, 126, 127syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) ) supp  0 )  e. 
Fin )
129120, 128eqeltrrd 2513 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( `' ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) " NN )  e.  Fin )
1303psrbag 17408 . . . . . . . . . . . . . . . . 17  |-  ( I  e.  W  ->  (
( i  e.  I  |->  if ( i  e.  x ,  ( Y `
 i ) ,  0 ) )  e.  D  <->  ( ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) ) : I --> NN0  /\  ( `' ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) )
" NN )  e. 
Fin ) ) )
131110, 130syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) )  e.  D  <->  ( (
i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) : I --> NN0  /\  ( `' ( i  e.  I  |->  if ( i  e.  x ,  ( Y `
 i ) ,  0 ) ) " NN )  e.  Fin ) ) )
132118, 129, 131mpbir2and 913 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) )  e.  D )
133 eqid 2438 . . . . . . . . . . . . . . 15  |-  ( .r
`  P )  =  ( .r `  P
)
134 ssun2 3515 . . . . . . . . . . . . . . . . . . 19  |-  { z }  C_  ( x  u.  { z } )
135 simprr 756 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( x  u. 
{ z } ) 
C_  I )
136134, 135syl5ss 3362 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  { z } 
C_  I )
137 vex 2970 . . . . . . . . . . . . . . . . . . 19  |-  z  e. 
_V
138137snss 3994 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  I  <->  { z }  C_  I )
139136, 138sylibr 212 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  z  e.  I
)
140112, 139ffvelrnd 5839 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( Y `  z )  e.  NN0 )
1413snifpsrbag 17410 . . . . . . . . . . . . . . . 16  |-  ( ( I  e.  W  /\  ( Y `  z )  e.  NN0 )  -> 
( i  e.  I  |->  if ( i  =  z ,  ( Y `
 z ) ,  0 ) )  e.  D )
142110, 140, 141syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z ) ,  0 ) )  e.  D )
14395, 109, 96, 97, 3, 110, 111, 132, 133, 142mplmonmul 17520 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) ) ,  .1.  ,  .0.  ) ) ( .r
`  P ) ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z ) ,  0 ) ) ,  .1.  ,  .0.  ) ) )  =  ( y  e.  D  |->  if ( y  =  ( ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) )  oF  +  ( i  e.  I  |->  if ( i  =  z ,  ( Y `
 z ) ,  0 ) ) ) ,  .1.  ,  .0.  ) ) )
144 mplcoe2.m . . . . . . . . . . . . . . . 16  |-  .^  =  (.g
`  G )
145 mplcoe2.v . . . . . . . . . . . . . . . 16  |-  V  =  ( I mVar  R )
14695, 3, 96, 97, 110, 51, 144, 145, 111, 139, 140mplcoe3 17522 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( ( Y `  z
)  .^  ( V `  z ) ) )
147146oveq2d 6102 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) ) ,  .1.  ,  .0.  ) ) ( .r
`  P ) ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z ) ,  0 ) ) ,  .1.  ,  .0.  ) ) )  =  ( ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) ) ,  .1.  ,  .0.  ) ) ( .r
`  P ) ( ( Y `  z
)  .^  ( V `  z ) ) ) )
148140adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  /\  i  e.  I
)  ->  ( Y `  z )  e.  NN0 )
149 ifcl 3826 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( Y `  z
)  e.  NN0  /\  0  e.  NN0 )  ->  if ( i  =  z ,  ( Y `  z ) ,  0 )  e.  NN0 )
150148, 114, 149sylancl 662 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  /\  i  e.  I
)  ->  if (
i  =  z ,  ( Y `  z
) ,  0 )  e.  NN0 )
151 eqidd 2439 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) )  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) )
152 eqidd 2439 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z ) ,  0 ) )  =  ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z ) ,  0 ) ) )
153110, 116, 150, 151, 152offval2 6331 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) )  oF  +  ( i  e.  I  |->  if ( i  =  z ,  ( Y `
 z ) ,  0 ) ) )  =  ( i  e.  I  |->  ( if ( i  e.  x ,  ( Y `  i
) ,  0 )  +  if ( i  =  z ,  ( Y `  z ) ,  0 ) ) ) )
154113adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  ( Y `  i )  e.  NN0 )
155154nn0cnd 10630 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  ( Y `  i )  e.  CC )
156155addid2d 9562 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  ( 0  +  ( Y `  i
) )  =  ( Y `  i ) )
157 elsni 3897 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  e.  { z }  ->  i  =  z )
158157adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  i  =  z )
159 simprlr 762 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  -.  z  e.  x )
160159ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  -.  z  e.  x )
161158, 160eqneltrd 2531 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  -.  i  e.  x )
162161, 124syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  if ( i  e.  x ,  ( Y `  i ) ,  0 )  =  0 )
163 iftrue 3792 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( i  =  z  ->  if ( i  =  z ,  ( Y `  z ) ,  0 )  =  ( Y `
 z ) )
164158, 163syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  if ( i  =  z ,  ( Y `  z ) ,  0 )  =  ( Y `  z
) )
165158fveq2d 5690 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  ( Y `  i )  =  ( Y `  z ) )
166164, 165eqtr4d 2473 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  if ( i  =  z ,  ( Y `  z ) ,  0 )  =  ( Y `  i
) )
167162, 166oveq12d 6104 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  ( if ( i  e.  x ,  ( Y `  i
) ,  0 )  +  if ( i  =  z ,  ( Y `  z ) ,  0 ) )  =  ( 0  +  ( Y `  i
) ) )
168 simpr 461 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  i  e.  {
z } )
169134, 168sseldi 3349 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  i  e.  ( x  u.  { z } ) )
170 iftrue 3792 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  e.  ( x  u. 
{ z } )  ->  if ( i  e.  ( x  u. 
{ z } ) ,  ( Y `  i ) ,  0 )  =  ( Y `
 i ) )
171169, 170syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  if ( i  e.  ( x  u. 
{ z } ) ,  ( Y `  i ) ,  0 )  =  ( Y `
 i ) )
172156, 167, 1713eqtr4d 2480 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  ( if ( i  e.  x ,  ( Y `  i
) ,  0 )  +  if ( i  =  z ,  ( Y `  z ) ,  0 ) )  =  if ( i  e.  ( x  u. 
{ z } ) ,  ( Y `  i ) ,  0 ) )
173116adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  -.  i  e.  { z } )  ->  if ( i  e.  x ,  ( Y `  i ) ,  0 )  e.  NN0 )
174173nn0cnd 10630 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  -.  i  e.  { z } )  ->  if ( i  e.  x ,  ( Y `  i ) ,  0 )  e.  CC )
175174addid1d 9561 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  -.  i  e.  { z } )  ->  ( if ( i  e.  x ,  ( Y `  i ) ,  0 )  +  0 )  =  if ( i  e.  x ,  ( Y `  i ) ,  0 ) )
176 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  -.  i  e.  { z } )  ->  -.  i  e.  { z } )
177 elsn 3886 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( i  e.  { z }  <-> 
i  =  z )
178176, 177sylnib 304 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  -.  i  e.  { z } )  ->  -.  i  =  z )
179 iffalse 3794 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  i  =  z  ->  if ( i  =  z ,  ( Y `  z ) ,  0 )  =  0 )
180178, 179syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  -.  i  e.  { z } )  ->  if ( i  =  z ,  ( Y `  z ) ,  0 )  =  0 )
181180oveq2d 6102 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  -.  i  e.  { z } )  ->  ( if ( i  e.  x ,  ( Y `  i ) ,  0 )  +  if ( i  =  z ,  ( Y `  z
) ,  0 ) )  =  ( if ( i  e.  x ,  ( Y `  i ) ,  0 )  +  0 ) )
182 biorf 405 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( -.  i  e.  { z }  ->  ( i  e.  x  <->  ( i  e. 
{ z }  \/  i  e.  x )
) )
183 elun 3492 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  e.  ( x  u. 
{ z } )  <-> 
( i  e.  x  \/  i  e.  { z } ) )
184 orcom 387 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( i  e.  x  \/  i  e.  { z } )  <->  ( i  e.  { z }  \/  i  e.  x )
)
185183, 184bitri 249 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( i  e.  ( x  u. 
{ z } )  <-> 
( i  e.  {
z }  \/  i  e.  x ) )
186182, 185syl6rbbr 264 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  i  e.  { z }  ->  ( i  e.  ( x  u.  {
z } )  <->  i  e.  x ) )
187186adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  -.  i  e.  { z } )  ->  (
i  e.  ( x  u.  { z } )  <->  i  e.  x
) )
188187ifbid 3806 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  -.  i  e.  { z } )  ->  if ( i  e.  ( x  u.  { z } ) ,  ( Y `  i ) ,  0 )  =  if ( i  e.  x ,  ( Y `
 i ) ,  0 ) )
189175, 181, 1883eqtr4d 2480 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  -.  i  e.  { z } )  ->  ( if ( i  e.  x ,  ( Y `  i ) ,  0 )  +  if ( i  =  z ,  ( Y `  z
) ,  0 ) )  =  if ( i  e.  ( x  u.  { z } ) ,  ( Y `
 i ) ,  0 ) )
190172, 189pm2.61dan 789 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  /\  i  e.  I
)  ->  ( if ( i  e.  x ,  ( Y `  i ) ,  0 )  +  if ( i  =  z ,  ( Y `  z
) ,  0 ) )  =  if ( i  e.  ( x  u.  { z } ) ,  ( Y `
 i ) ,  0 ) )
191190mpteq2dva 4373 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( i  e.  I  |->  ( if ( i  e.  x ,  ( Y `  i
) ,  0 )  +  if ( i  =  z ,  ( Y `  z ) ,  0 ) ) )  =  ( i  e.  I  |->  if ( i  e.  ( x  u.  { z } ) ,  ( Y `
 i ) ,  0 ) ) )
192153, 191eqtrd 2470 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) )  oF  +  ( i  e.  I  |->  if ( i  =  z ,  ( Y `
 z ) ,  0 ) ) )  =  ( i  e.  I  |->  if ( i  e.  ( x  u. 
{ z } ) ,  ( Y `  i ) ,  0 ) ) )
193192eqeq2d 2449 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( y  =  ( ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) )  oF  +  ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z ) ,  0 ) ) )  <->  y  =  ( i  e.  I  |->  if ( i  e.  ( x  u.  {
z } ) ,  ( Y `  i
) ,  0 ) ) ) )
194193ifbid 3806 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  if ( y  =  ( ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) )  oF  +  ( i  e.  I  |->  if ( i  =  z ,  ( Y `
 z ) ,  0 ) ) ) ,  .1.  ,  .0.  )  =  if (
y  =  ( i  e.  I  |->  if ( i  e.  ( x  u.  { z } ) ,  ( Y `
 i ) ,  0 ) ) ,  .1.  ,  .0.  )
)
195194mpteq2dv 4374 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( y  e.  D  |->  if ( y  =  ( ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) )  oF  +  ( i  e.  I  |->  if ( i  =  z ,  ( Y `
 z ) ,  0 ) ) ) ,  .1.  ,  .0.  ) )  =  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( x  u.  { z } ) ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) ) )
196143, 147, 1953eqtr3rd 2479 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( x  u. 
{ z } ) ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) ) ( .r
`  P ) ( ( Y `  z
)  .^  ( V `  z ) ) ) )
19751, 109mgpbas 16585 . . . . . . . . . . . . . 14  |-  ( Base `  P )  =  (
Base `  G )
19851, 133mgpplusg 16583 . . . . . . . . . . . . . 14  |-  ( .r
`  P )  =  ( +g  `  G
)
19995mplcrng 17509 . . . . . . . . . . . . . . . . 17  |-  ( ( I  e.  W  /\  R  e.  CRing )  ->  P  e.  CRing )
2002, 98, 199syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  P  e.  CRing )
20151crngmgp 16641 . . . . . . . . . . . . . . . 16  |-  ( P  e.  CRing  ->  G  e. CMnd )
202200, 201syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  G  e. CMnd )
203202adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  G  e. CMnd )
204104, 135syl5ss 3362 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  x  C_  I
)
205204sselda 3351 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  /\  k  e.  x
)  ->  k  e.  I )
206 cmnmnd 16283 . . . . . . . . . . . . . . . . . . 19  |-  ( G  e. CMnd  ->  G  e.  Mnd )
207202, 206syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  G  e.  Mnd )
208207adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  I )  ->  G  e.  Mnd )
2097ffvelrnda 5838 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  I )  ->  ( Y `  k )  e.  NN0 )
2102adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  I )  ->  I  e.  W )
211100adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  I )  ->  R  e.  Ring )
212 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  I )  ->  k  e.  I )
21395, 145, 109, 210, 211, 212mvrcl 17505 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  I )  ->  ( V `  k )  e.  ( Base `  P
) )
214197, 144mulgnn0cl 15634 . . . . . . . . . . . . . . . . 17  |-  ( ( G  e.  Mnd  /\  ( Y `  k )  e.  NN0  /\  ( V `  k )  e.  ( Base `  P
) )  ->  (
( Y `  k
)  .^  ( V `  k ) )  e.  ( Base `  P
) )
215208, 209, 213, 214syl3anc 1218 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  I )  ->  (
( Y `  k
)  .^  ( V `  k ) )  e.  ( Base `  P
) )
216215adantlr 714 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  /\  k  e.  I
)  ->  ( ( Y `  k )  .^  ( V `  k
) )  e.  (
Base `  P )
)
217205, 216syldan 470 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  /\  k  e.  x
)  ->  ( ( Y `  k )  .^  ( V `  k
) )  e.  (
Base `  P )
)
218207adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  G  e.  Mnd )
21995, 145, 109, 110, 111, 139mvrcl 17505 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( V `  z )  e.  (
Base `  P )
)
220197, 144mulgnn0cl 15634 . . . . . . . . . . . . . . 15  |-  ( ( G  e.  Mnd  /\  ( Y `  z )  e.  NN0  /\  ( V `  z )  e.  ( Base `  P
) )  ->  (
( Y `  z
)  .^  ( V `  z ) )  e.  ( Base `  P
) )
221218, 140, 219, 220syl3anc 1218 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( ( Y `
 z )  .^  ( V `  z ) )  e.  ( Base `  P ) )
222 fveq2 5686 . . . . . . . . . . . . . . 15  |-  ( k  =  z  ->  ( Y `  k )  =  ( Y `  z ) )
223 fveq2 5686 . . . . . . . . . . . . . . 15  |-  ( k  =  z  ->  ( V `  k )  =  ( V `  z ) )
224222, 223oveq12d 6104 . . . . . . . . . . . . . 14  |-  ( k  =  z  ->  (
( Y `  k
)  .^  ( V `  k ) )  =  ( ( Y `  z )  .^  ( V `  z )
) )
225197, 198, 203, 121, 217, 139, 159, 221, 224gsumunsn 16442 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( G  gsumg  ( k  e.  ( x  u. 
{ z } ) 
|->  ( ( Y `  k )  .^  ( V `  k )
) ) )  =  ( ( G  gsumg  ( k  e.  x  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) ) ) ( .r `  P ) ( ( Y `  z ) 
.^  ( V `  z ) ) ) )
226196, 225eqeq12d 2452 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( x  u.  { z } ) ,  ( Y `
 i ) ,  0 ) ) ,  .1.  ,  .0.  )
)  =  ( G 
gsumg  ( k  e.  ( x  u.  { z } )  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) ) )  <->  ( ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) ) ,  .1.  ,  .0.  ) ) ( .r
`  P ) ( ( Y `  z
)  .^  ( V `  z ) ) )  =  ( ( G 
gsumg  ( k  e.  x  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) ( .r `  P ) ( ( Y `  z )  .^  ( V `  z )
) ) ) )
227108, 226syl5ibr 221 . . . . . . . . . . 11  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  x  |->  ( ( Y `  k )  .^  ( V `  k )
) ) )  -> 
( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( x  u.  {
z } ) ,  ( Y `  i
) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  ( x  u.  { z } )  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) ) ) ) )
228227expr 615 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  Fin  /\  -.  z  e.  x ) )  -> 
( ( x  u. 
{ z } ) 
C_  I  ->  (
( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `
 i ) ,  0 ) ) ,  .1.  ,  .0.  )
)  =  ( G 
gsumg  ( k  e.  x  |->  ( ( Y `  k )  .^  ( V `  k )
) ) )  -> 
( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( x  u.  {
z } ) ,  ( Y `  i
) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  ( x  u.  { z } )  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) ) ) ) ) )
229228a2d 26 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  Fin  /\  -.  z  e.  x ) )  -> 
( ( ( x  u.  { z } )  C_  I  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  x  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) )  ->  ( ( x  u.  { z } )  C_  I  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( x  u.  { z } ) ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  ( x  u.  { z } )  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) ) ) ) ) )
230107, 229syl5 32 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  Fin  /\  -.  z  e.  x ) )  -> 
( ( x  C_  I  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  x  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) )  ->  ( ( x  u.  { z } )  C_  I  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( x  u.  { z } ) ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  ( x  u.  { z } )  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) ) ) ) ) )
231230expcom 435 . . . . . . 7  |-  ( ( x  e.  Fin  /\  -.  z  e.  x
)  ->  ( ph  ->  ( ( x  C_  I  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  x  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) )  ->  ( ( x  u.  { z } )  C_  I  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( x  u.  { z } ) ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  ( x  u.  { z } )  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) ) ) ) ) ) )
232231a2d 26 . . . . . 6  |-  ( ( x  e.  Fin  /\  -.  z  e.  x
)  ->  ( ( ph  ->  ( x  C_  I  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  x  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) ) )  ->  ( ph  ->  ( ( x  u. 
{ z } ) 
C_  I  ->  (
y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( x  u.  { z } ) ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  ( x  u.  { z } )  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) ) ) ) ) ) )
23358, 70, 82, 94, 103, 232findcard2s 7545 . . . . 5  |-  ( ( `' Y " NN )  e.  Fin  ->  ( ph  ->  ( ( `' Y " NN ) 
C_  I  ->  (
y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  ( `' Y " NN ) 
|->  ( ( Y `  k )  .^  ( V `  k )
) ) ) ) ) )
23434, 233mpcom 36 . . . 4  |-  ( ph  ->  ( ( `' Y " NN )  C_  I  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( `' Y " NN ) ,  ( Y `
 i ) ,  0 ) ) ,  .1.  ,  .0.  )
)  =  ( G 
gsumg  ( k  e.  ( `' Y " NN ) 
|->  ( ( Y `  k )  .^  ( V `  k )
) ) ) ) )
23533, 234mpd 15 . . 3  |-  ( ph  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( `' Y " NN ) ,  ( Y `
 i ) ,  0 ) ) ,  .1.  ,  .0.  )
)  =  ( G 
gsumg  ( k  e.  ( `' Y " NN ) 
|->  ( ( Y `  k )  .^  ( V `  k )
) ) ) )
236 resmpt 5151 . . . . 5  |-  ( ( `' Y " NN ) 
C_  I  ->  (
( k  e.  I  |->  ( ( Y `  k )  .^  ( V `  k )
) )  |`  ( `' Y " NN ) )  =  ( k  e.  ( `' Y " NN )  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) ) )
23733, 236syl 16 . . . 4  |-  ( ph  ->  ( ( k  e.  I  |->  ( ( Y `
 k )  .^  ( V `  k ) ) )  |`  ( `' Y " NN ) )  =  ( k  e.  ( `' Y " NN )  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) ) )
238237oveq2d 6102 . . 3  |-  ( ph  ->  ( G  gsumg  ( ( k  e.  I  |->  ( ( Y `
 k )  .^  ( V `  k ) ) )  |`  ( `' Y " NN ) ) )  =  ( G  gsumg  ( k  e.  ( `' Y " NN ) 
|->  ( ( Y `  k )  .^  ( V `  k )
) ) ) )
239 eqid 2438 . . . . 5  |-  ( k  e.  I  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) )  =  ( k  e.  I  |->  ( ( Y `
 k )  .^  ( V `  k ) ) )
240215, 239fmptd 5862 . . . 4  |-  ( ph  ->  ( k  e.  I  |->  ( ( Y `  k )  .^  ( V `  k )
) ) : I --> ( Base `  P
) )
2417, 16, 2, 18suppssr 6715 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( I  \  ( `' Y " NN ) ) )  ->  ( Y `  k )  =  0 )
242241oveq1d 6101 . . . . . 6  |-  ( (
ph  /\  k  e.  ( I  \  ( `' Y " NN ) ) )  ->  (
( Y `  k
)  .^  ( V `  k ) )  =  ( 0  .^  ( V `  k )
) )
243 eldifi 3473 . . . . . . . 8  |-  ( k  e.  ( I  \ 
( `' Y " NN ) )  ->  k  e.  I )
244243, 213sylan2 474 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( I  \  ( `' Y " NN ) ) )  ->  ( V `  k )  e.  ( Base `  P
) )
245197, 53, 144mulg0 15623 . . . . . . 7  |-  ( ( V `  k )  e.  ( Base `  P
)  ->  ( 0 
.^  ( V `  k ) )  =  ( 1r `  P
) )
246244, 245syl 16 . . . . . 6  |-  ( (
ph  /\  k  e.  ( I  \  ( `' Y " NN ) ) )  ->  (
0  .^  ( V `  k ) )  =  ( 1r `  P
) )
247242, 246eqtrd 2470 . . . . 5  |-  ( (
ph  /\  k  e.  ( I  \  ( `' Y " NN ) ) )  ->  (
( Y `  k
)  .^  ( V `  k ) )  =  ( 1r `  P
) )
248247, 2suppss2 6718 . . . 4  |-  ( ph  ->  ( ( k  e.  I  |->  ( ( Y `
 k )  .^  ( V `  k ) ) ) supp  ( 1r
`  P ) ) 
C_  ( `' Y " NN ) )
249 mptexg 5942 . . . . . 6  |-  ( I  e.  W  ->  (
k  e.  I  |->  ( ( Y `  k
)  .^  ( V `  k ) ) )  e.  _V )
2502, 249syl 16 . . . . 5  |-  ( ph  ->  ( k  e.  I  |->  ( ( Y `  k )  .^  ( V `  k )
) )  e.  _V )
251 funmpt 5449 . . . . . 6  |-  Fun  (
k  e.  I  |->  ( ( Y `  k
)  .^  ( V `  k ) ) )
252251a1i 11 . . . . 5  |-  ( ph  ->  Fun  ( k  e.  I  |->  ( ( Y `
 k )  .^  ( V `  k ) ) ) )
253 fvex 5696 . . . . . 6  |-  ( 1r
`  P )  e. 
_V
254253a1i 11 . . . . 5  |-  ( ph  ->  ( 1r `  P
)  e.  _V )
255 suppssfifsupp 7627 . . . . 5  |-  ( ( ( ( k  e.  I  |->  ( ( Y `
 k )  .^  ( V `  k ) ) )  e.  _V  /\ 
Fun  ( k  e.  I  |->  ( ( Y `
 k )  .^  ( V `  k ) ) )  /\  ( 1r `  P )  e. 
_V )  /\  (
( `' Y " NN )  e.  Fin  /\  ( ( k  e.  I  |->  ( ( Y `
 k )  .^  ( V `  k ) ) ) supp  ( 1r
`  P ) ) 
C_  ( `' Y " NN ) ) )  ->  ( k  e.  I  |->  ( ( Y `
 k )  .^  ( V `  k ) ) ) finSupp  ( 1r
`  P ) )
256250, 252, 254, 34, 248, 255syl32anc 1226 . . . 4  |-  ( ph  ->  ( k  e.  I  |->  ( ( Y `  k )  .^  ( V `  k )
) ) finSupp  ( 1r `  P ) )
257197, 53, 202, 2, 240, 248, 256gsumres 16386 . . 3  |-  ( ph  ->  ( G  gsumg  ( ( k  e.  I  |->  ( ( Y `
 k )  .^  ( V `  k ) ) )  |`  ( `' Y " NN ) ) )  =  ( G  gsumg  ( k  e.  I  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) )
258235, 238, 2573eqtr2d 2476 . 2  |-  ( ph  ->  ( y  e.  D  |->  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( `' Y " NN ) ,  ( Y `
 i ) ,  0 ) ) ,  .1.  ,  .0.  )
)  =  ( G 
gsumg  ( k  e.  I  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) )
25929, 258eqtrd 2470 1  |-  ( ph  ->  ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  I  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    = wceq 1369    e. wcel 1756   {crab 2714   _Vcvv 2967    \ cdif 3320    u. cun 3321    C_ wss 3323   (/)c0 3632   ifcif 3786   {csn 3872   class class class wbr 4287    e. cmpt 4345    X. cxp 4833   `'ccnv 4834   dom cdm 4835    |` cres 4837   "cima 4838   Fun wfun 5407   -->wf 5409   ` cfv 5413  (class class class)co 6086    oFcof 6313   supp csupp 6685    ^m cmap 7206   Fincfn 7302   finSupp cfsupp 7612   0cc0 9274    + caddc 9277   NNcn 10314   NN0cn0 10571   Basecbs 14166   .rcmulr 14231   0gc0g 14370    gsumg cgsu 14371   Mndcmnd 15401  .gcmg 15406  CMndccmn 16268  mulGrpcmgp 16579   1rcur 16591   Ringcrg 16633   CRingccrg 16634   mVar cmvr 17396   mPoly cmpl 17397
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-rep 4398  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-inf2 7839  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rmo 2718  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-int 4124  df-iun 4168  df-iin 4169  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-se 4675  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-of 6315  df-ofr 6316  df-om 6472  df-1st 6572  df-2nd 6573  df-supp 6686  df-recs 6824  df-rdg 6858  df-1o 6912  df-2o 6913  df-oadd 6916  df-er 7093  df-map 7208  df-pm 7209  df-ixp 7256  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-fsupp 7613  df-oi 7716  df-card 8101  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-nn 10315  df-2 10372  df-3 10373  df-4 10374  df-5 10375  df-6 10376  df-7 10377  df-8 10378  df-9 10379  df-n0 10572  df-z 10639  df-uz 10854  df-fz 11430  df-fzo 11541  df-seq 11799  df-hash 12096  df-struct 14168  df-ndx 14169  df-slot 14170  df-base 14171  df-sets 14172  df-ress 14173  df-plusg 14243  df-mulr 14244  df-sca 14246  df-vsca 14247  df-tset 14249  df-0g 14372  df-gsum 14373  df-mre 14516  df-mrc 14517  df-acs 14519  df-mnd 15407  df-mhm 15456  df-submnd 15457  df-grp 15536  df-minusg 15537  df-mulg 15539  df-subg 15669  df-ghm 15736  df-cntz 15826  df-cmn 16270  df-abl 16271  df-mgp 16580  df-ur 16592  df-rng 16635  df-cring 16636  df-subrg 16841  df-psr 17400  df-mvr 17401  df-mpl 17402
This theorem is referenced by:  mplbas2  17526  mplbas2OLD  17527  ply1coe  17721  ply1coeOLD  17722
  Copyright terms: Public domain W3C validator