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

Theorem mplcoe2 16457
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.)
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    k, W    .0. , f,
k, y    f, Y, k, y
Allowed substitution hints:    ph( f)    D( f)    P( y, f)    R( k)    .1. ( f)    .^ ( y, f)    G( y, f)    V( y, f)    W( y, 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 16358 . . . . . . . . . 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 202 . . . . . . . 8  |-  ( ph  ->  ( Y : I --> NN0  /\  ( `' Y " NN )  e.  Fin ) )
76simpld 446 . . . . . . 7  |-  ( ph  ->  Y : I --> NN0 )
87feqmptd 5718 . . . . . 6  |-  ( ph  ->  Y  =  ( i  e.  I  |->  ( Y `
 i ) ) )
9 iftrue 3688 . . . . . . . . 9  |-  ( i  e.  ( `' Y " NN )  ->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 )  =  ( Y `
 i ) )
109adantl 453 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  I )  /\  i  e.  ( `' Y " NN ) )  ->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 )  =  ( Y `
 i ) )
11 eldif 3273 . . . . . . . . . 10  |-  ( i  e.  ( I  \ 
( `' Y " NN ) )  <->  ( i  e.  I  /\  -.  i  e.  ( `' Y " NN ) ) )
12 ifid 3714 . . . . . . . . . . 11  |-  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  ( Y `  i ) )  =  ( Y `
 i )
13 nn0supp 10205 . . . . . . . . . . . . . . 15  |-  ( Y : I --> NN0  ->  ( `' Y " ( _V 
\  { 0 } ) )  =  ( `' Y " NN ) )
147, 13syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( `' Y "
( _V  \  {
0 } ) )  =  ( `' Y " NN ) )
15 eqimss 3343 . . . . . . . . . . . . . 14  |-  ( ( `' Y " ( _V 
\  { 0 } ) )  =  ( `' Y " NN )  ->  ( `' Y " ( _V  \  {
0 } ) ) 
C_  ( `' Y " NN ) )
1614, 15syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( `' Y "
( _V  \  {
0 } ) ) 
C_  ( `' Y " NN ) )
177, 16suppssr 5803 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( I  \  ( `' Y " NN ) ) )  ->  ( Y `  i )  =  0 )
1817ifeq2d 3697 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( I  \  ( `' Y " NN ) ) )  ->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  ( Y `  i ) )  =  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 ) )
1912, 18syl5reqr 2434 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( I  \  ( `' Y " NN ) ) )  ->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 )  =  ( Y `
 i ) )
2011, 19sylan2br 463 . . . . . . . . 9  |-  ( (
ph  /\  ( i  e.  I  /\  -.  i  e.  ( `' Y " NN ) ) )  ->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 )  =  ( Y `
 i ) )
2120anassrs 630 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  I )  /\  -.  i  e.  ( `' Y " NN ) )  ->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 )  =  ( Y `  i
) )
2210, 21pm2.61dan 767 . . . . . . 7  |-  ( (
ph  /\  i  e.  I )  ->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 )  =  ( Y `
 i ) )
2322mpteq2dva 4236 . . . . . 6  |-  ( ph  ->  ( i  e.  I  |->  if ( i  e.  ( `' Y " NN ) ,  ( Y `
 i ) ,  0 ) )  =  ( i  e.  I  |->  ( Y `  i
) ) )
248, 23eqtr4d 2422 . . . . 5  |-  ( ph  ->  Y  =  ( i  e.  I  |->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 ) ) )
2524eqeq2d 2398 . . . 4  |-  ( ph  ->  ( y  =  Y  <-> 
y  =  ( i  e.  I  |->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 ) ) ) )
2625ifbid 3700 . . 3  |-  ( ph  ->  if ( y  =  Y ,  .1.  ,  .0.  )  =  if ( y  =  ( i  e.  I  |->  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 ) ) ,  .1.  ,  .0.  ) )
2726mpteq2dv 4237 . 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.  ) ) )
28 cnvimass 5164 . . . . 5  |-  ( `' Y " NN ) 
C_  dom  Y
29 fdm 5535 . . . . . 6  |-  ( Y : I --> NN0  ->  dom 
Y  =  I )
307, 29syl 16 . . . . 5  |-  ( ph  ->  dom  Y  =  I )
3128, 30syl5sseq 3339 . . . 4  |-  ( ph  ->  ( `' Y " NN )  C_  I )
326simprd 450 . . . . 5  |-  ( ph  ->  ( `' Y " NN )  e.  Fin )
33 sseq1 3312 . . . . . . . 8  |-  ( w  =  (/)  ->  ( w 
C_  I  <->  (/)  C_  I
) )
34 noel 3575 . . . . . . . . . . . . . . . 16  |-  -.  i  e.  (/)
35 eleq2 2448 . . . . . . . . . . . . . . . 16  |-  ( w  =  (/)  ->  ( i  e.  w  <->  i  e.  (/) ) )
3634, 35mtbiri 295 . . . . . . . . . . . . . . 15  |-  ( w  =  (/)  ->  -.  i  e.  w )
37 iffalse 3689 . . . . . . . . . . . . . . 15  |-  ( -.  i  e.  w  ->  if ( i  e.  w ,  ( Y `  i ) ,  0 )  =  0 )
3836, 37syl 16 . . . . . . . . . . . . . 14  |-  ( w  =  (/)  ->  if ( i  e.  w ,  ( Y `  i
) ,  0 )  =  0 )
3938mpteq2dv 4237 . . . . . . . . . . . . 13  |-  ( w  =  (/)  ->  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i
) ,  0 ) )  =  ( i  e.  I  |->  0 ) )
40 fconstmpt 4861 . . . . . . . . . . . . 13  |-  ( I  X.  { 0 } )  =  ( i  e.  I  |->  0 )
4139, 40syl6eqr 2437 . . . . . . . . . . . 12  |-  ( w  =  (/)  ->  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i
) ,  0 ) )  =  ( I  X.  { 0 } ) )
4241eqeq2d 2398 . . . . . . . . . . 11  |-  ( w  =  (/)  ->  ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i ) ,  0 ) )  <-> 
y  =  ( I  X.  { 0 } ) ) )
4342ifbid 3700 . . . . . . . . . 10  |-  ( w  =  (/)  ->  if ( y  =  ( i  e.  I  |->  if ( i  e.  w ,  ( Y `  i
) ,  0 ) ) ,  .1.  ,  .0.  )  =  if ( y  =  ( I  X.  { 0 } ) ,  .1.  ,  .0.  ) )
4443mpteq2dv 4237 . . . . . . . . 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.  ) ) )
45 mpteq1 4230 . . . . . . . . . . . 12  |-  ( w  =  (/)  ->  ( k  e.  w  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) )  =  ( k  e.  (/)  |->  ( ( Y `
 k )  .^  ( V `  k ) ) ) )
46 mpt0 5512 . . . . . . . . . . . 12  |-  ( k  e.  (/)  |->  ( ( Y `
 k )  .^  ( V `  k ) ) )  =  (/)
4745, 46syl6eq 2435 . . . . . . . . . . 11  |-  ( w  =  (/)  ->  ( k  e.  w  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) )  =  (/) )
4847oveq2d 6036 . . . . . . . . . 10  |-  ( w  =  (/)  ->  ( G 
gsumg  ( k  e.  w  |->  ( ( Y `  k )  .^  ( V `  k )
) ) )  =  ( G  gsumg  (/) ) )
49 mplcoe2.g . . . . . . . . . . . 12  |-  G  =  (mulGrp `  P )
50 eqid 2387 . . . . . . . . . . . 12  |-  ( 1r
`  P )  =  ( 1r `  P
)
5149, 50rngidval 15593 . . . . . . . . . . 11  |-  ( 1r
`  P )  =  ( 0g `  G
)
5251gsum0 14707 . . . . . . . . . 10  |-  ( G 
gsumg  (/) )  =  ( 1r
`  P )
5348, 52syl6eq 2435 . . . . . . . . 9  |-  ( w  =  (/)  ->  ( G 
gsumg  ( k  e.  w  |->  ( ( Y `  k )  .^  ( V `  k )
) ) )  =  ( 1r `  P
) )
5444, 53eqeq12d 2401 . . . . . . . 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 ) ) )
5533, 54imbi12d 312 . . . . . . 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
) ) ) )
5655imbi2d 308 . . . . . 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
) ) ) ) )
57 sseq1 3312 . . . . . . . 8  |-  ( w  =  x  ->  (
w  C_  I  <->  x  C_  I
) )
58 eleq2 2448 . . . . . . . . . . . . . 14  |-  ( w  =  x  ->  (
i  e.  w  <->  i  e.  x ) )
5958ifbid 3700 . . . . . . . . . . . . 13  |-  ( w  =  x  ->  if ( i  e.  w ,  ( Y `  i ) ,  0 )  =  if ( i  e.  x ,  ( Y `  i
) ,  0 ) )
6059mpteq2dv 4237 . . . . . . . . . . . 12  |-  ( w  =  x  ->  (
i  e.  I  |->  if ( i  e.  w ,  ( Y `  i ) ,  0 ) )  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) )
6160eqeq2d 2398 . . . . . . . . . . 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 ) ) ) )
6261ifbid 3700 . . . . . . . . . 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.  ) )
6362mpteq2dv 4237 . . . . . . . . 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.  )
) )
64 mpteq1 4230 . . . . . . . . . 10  |-  ( w  =  x  ->  (
k  e.  w  |->  ( ( Y `  k
)  .^  ( V `  k ) ) )  =  ( k  e.  x  |->  ( ( Y `
 k )  .^  ( V `  k ) ) ) )
6564oveq2d 6036 . . . . . . . . 9  |-  ( w  =  x  ->  ( G  gsumg  ( k  e.  w  |->  ( ( Y `  k )  .^  ( V `  k )
) ) )  =  ( G  gsumg  ( k  e.  x  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) )
6663, 65eqeq12d 2401 . . . . . . . 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 )
) ) ) ) )
6757, 66imbi12d 312 . . . . . . 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 )
) ) ) ) ) )
6867imbi2d 308 . . . . . 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 )
) ) ) ) ) ) )
69 sseq1 3312 . . . . . . . 8  |-  ( w  =  ( x  u. 
{ z } )  ->  ( w  C_  I 
<->  ( x  u.  {
z } )  C_  I ) )
70 eleq2 2448 . . . . . . . . . . . . . 14  |-  ( w  =  ( x  u. 
{ z } )  ->  ( i  e.  w  <->  i  e.  ( x  u.  { z } ) ) )
7170ifbid 3700 . . . . . . . . . . . . 13  |-  ( w  =  ( x  u. 
{ z } )  ->  if ( i  e.  w ,  ( Y `  i ) ,  0 )  =  if ( i  e.  ( x  u.  {
z } ) ,  ( Y `  i
) ,  0 ) )
7271mpteq2dv 4237 . . . . . . . . . . . 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 ) ) )
7372eqeq2d 2398 . . . . . . . . . . 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 ) ) ) )
7473ifbid 3700 . . . . . . . . . 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.  )
)
7574mpteq2dv 4237 . . . . . . . . 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.  ) ) )
76 mpteq1 4230 . . . . . . . . . 10  |-  ( w  =  ( x  u. 
{ z } )  ->  ( k  e.  w  |->  ( ( Y `
 k )  .^  ( V `  k ) ) )  =  ( k  e.  ( x  u.  { z } )  |->  ( ( Y `
 k )  .^  ( V `  k ) ) ) )
7776oveq2d 6036 . . . . . . . . 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 ) ) ) ) )
7875, 77eqeq12d 2401 . . . . . . . 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 ) ) ) ) ) )
7969, 78imbi12d 312 . . . . . . 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 ) ) ) ) ) ) )
8079imbi2d 308 . . . . . 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 ) ) ) ) ) ) ) )
81 sseq1 3312 . . . . . . . 8  |-  ( w  =  ( `' Y " NN )  ->  (
w  C_  I  <->  ( `' Y " NN )  C_  I ) )
82 eleq2 2448 . . . . . . . . . . . . . 14  |-  ( w  =  ( `' Y " NN )  ->  (
i  e.  w  <->  i  e.  ( `' Y " NN ) ) )
8382ifbid 3700 . . . . . . . . . . . . 13  |-  ( w  =  ( `' Y " NN )  ->  if ( i  e.  w ,  ( Y `  i ) ,  0 )  =  if ( i  e.  ( `' Y " NN ) ,  ( Y `  i ) ,  0 ) )
8483mpteq2dv 4237 . . . . . . . . . . . 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 ) ) )
8584eqeq2d 2398 . . . . . . . . . . 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 ) ) ) )
8685ifbid 3700 . . . . . . . . . 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.  ) )
8786mpteq2dv 4237 . . . . . . . . 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.  )
) )
88 mpteq1 4230 . . . . . . . . . 10  |-  ( w  =  ( `' Y " NN )  ->  (
k  e.  w  |->  ( ( Y `  k
)  .^  ( V `  k ) ) )  =  ( k  e.  ( `' Y " NN )  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) ) )
8988oveq2d 6036 . . . . . . . . 9  |-  ( w  =  ( `' Y " NN )  ->  ( G  gsumg  ( k  e.  w  |->  ( ( Y `  k )  .^  ( V `  k )
) ) )  =  ( G  gsumg  ( k  e.  ( `' Y " NN ) 
|->  ( ( Y `  k )  .^  ( V `  k )
) ) ) )
9087, 89eqeq12d 2401 . . . . . . . 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 )
) ) ) ) )
9181, 90imbi12d 312 . . . . . . 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 )
) ) ) ) ) )
9291imbi2d 308 . . . . . 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 )
) ) ) ) ) ) )
93 mplcoe1.p . . . . . . . . 9  |-  P  =  ( I mPoly  R )
94 mplcoe1.z . . . . . . . . 9  |-  .0.  =  ( 0g `  R )
95 mplcoe1.o . . . . . . . . 9  |-  .1.  =  ( 1r `  R )
96 mplcoe2.r . . . . . . . . . 10  |-  ( ph  ->  R  e.  CRing )
97 crngrng 15601 . . . . . . . . . 10  |-  ( R  e.  CRing  ->  R  e.  Ring )
9896, 97syl 16 . . . . . . . . 9  |-  ( ph  ->  R  e.  Ring )
9993, 3, 94, 95, 50, 2, 98mpl1 16434 . . . . . . . 8  |-  ( ph  ->  ( 1r `  P
)  =  ( y  e.  D  |->  if ( y  =  ( I  X.  { 0 } ) ,  .1.  ,  .0.  ) ) )
10099eqcomd 2392 . . . . . . 7  |-  ( ph  ->  ( y  e.  D  |->  if ( y  =  ( I  X.  {
0 } ) ,  .1.  ,  .0.  )
)  =  ( 1r
`  P ) )
101100a1d 23 . . . . . 6  |-  ( ph  ->  ( (/)  C_  I  -> 
( y  e.  D  |->  if ( y  =  ( I  X.  {
0 } ) ,  .1.  ,  .0.  )
)  =  ( 1r
`  P ) ) )
102 ssun1 3453 . . . . . . . . . . 11  |-  x  C_  ( x  u.  { z } )
103 sstr2 3298 . . . . . . . . . . 11  |-  ( x 
C_  ( x  u. 
{ z } )  ->  ( ( x  u.  { z } )  C_  I  ->  x 
C_  I ) )
104102, 103ax-mp 8 . . . . . . . . . 10  |-  ( ( x  u.  { z } )  C_  I  ->  x  C_  I )
105104imim1i 56 . . . . . . . . 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 )
) ) ) ) )
106 oveq1 6027 . . . . . . . . . . . 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 )
) ) )
107 eqid 2387 . . . . . . . . . . . . . . 15  |-  ( Base `  P )  =  (
Base `  P )
1082adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  I  e.  W
)
10998adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  R  e.  Ring )
1107adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  Y : I --> NN0 )
111110ffvelrnda 5809 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  /\  i  e.  I
)  ->  ( Y `  i )  e.  NN0 )
112 0nn0 10168 . . . . . . . . . . . . . . . . . 18  |-  0  e.  NN0
113 ifcl 3718 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( Y `  i
)  e.  NN0  /\  0  e.  NN0 )  ->  if ( i  e.  x ,  ( Y `  i ) ,  0 )  e.  NN0 )
114111, 112, 113sylancl 644 . . . . . . . . . . . . . . . . 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 )
115 eqid 2387 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) )  =  ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) )
116114, 115fmptd 5832 . . . . . . . . . . . . . . . 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 )
117 nn0supp 10205 . . . . . . . . . . . . . . . . . 18  |-  ( ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) : I --> NN0  ->  ( `' ( i  e.  I  |->  if ( i  e.  x ,  ( Y `
 i ) ,  0 ) ) "
( _V  \  {
0 } ) )  =  ( `' ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) " NN ) )
118116, 117syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( `' ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) " ( _V  \  { 0 } ) )  =  ( `' ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) )
" NN ) )
119 simprll 739 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  x  e.  Fin )
120 eldifn 3413 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  ( I  \  x )  ->  -.  i  e.  x )
121120adantl 453 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  /\  i  e.  ( I  \  x ) )  ->  -.  i  e.  x )
122 iffalse 3689 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  i  e.  x  ->  if ( i  e.  x ,  ( Y `  i ) ,  0 )  =  0 )
123121, 122syl 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 )
124123suppss2 6239 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( `' ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) " ( _V  \  { 0 } ) )  C_  x
)
125 ssfi 7265 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  Fin  /\  ( `' ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) )
" ( _V  \  { 0 } ) )  C_  x )  ->  ( `' ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) ) " ( _V 
\  { 0 } ) )  e.  Fin )
126119, 124, 125syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( `' ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) ) " ( _V  \  { 0 } ) )  e.  Fin )
127118, 126eqeltrrd 2462 . . . . . . . . . . . . . . . 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 )
1283psrbag 16358 . . . . . . . . . . . . . . . . 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 ) ) )
129108, 128syl 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 ) ) )
130116, 127, 129mpbir2and 889 . . . . . . . . . . . . . . 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 )
131 eqid 2387 . . . . . . . . . . . . . . 15  |-  ( .r
`  P )  =  ( .r `  P
)
132 ssun2 3454 . . . . . . . . . . . . . . . . . . . . . 22  |-  { z }  C_  ( x  u.  { z } )
133 simprr 734 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( x  u. 
{ z } ) 
C_  I )
134132, 133syl5ss 3302 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  { z } 
C_  I )
135 vex 2902 . . . . . . . . . . . . . . . . . . . . . 22  |-  z  e. 
_V
136135snss 3869 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  e.  I  <->  { z }  C_  I )
137134, 136sylibr 204 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  z  e.  I
)
138110, 137ffvelrnd 5810 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( Y `  z )  e.  NN0 )
139138adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  /\  i  e.  I
)  ->  ( Y `  z )  e.  NN0 )
140 ifcl 3718 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( Y `  z
)  e.  NN0  /\  0  e.  NN0 )  ->  if ( i  =  z ,  ( Y `  z ) ,  0 )  e.  NN0 )
141139, 112, 140sylancl 644 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  /\  i  e.  I
)  ->  if (
i  =  z ,  ( Y `  z
) ,  0 )  e.  NN0 )
142 eqid 2387 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z
) ,  0 ) )  =  ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z
) ,  0 ) )
143141, 142fmptd 5832 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z ) ,  0 ) ) : I --> NN0 )
144 nn0supp 10205 . . . . . . . . . . . . . . . . . 18  |-  ( ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z ) ,  0 ) ) : I --> NN0  ->  ( `' ( i  e.  I  |->  if ( i  =  z ,  ( Y `
 z ) ,  0 ) ) "
( _V  \  {
0 } ) )  =  ( `' ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z ) ,  0 ) ) " NN ) )
145143, 144syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( `' ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z ) ,  0 ) ) " ( _V  \  { 0 } ) )  =  ( `' ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z ) ,  0 ) )
" NN ) )
146 snfi 7123 . . . . . . . . . . . . . . . . . 18  |-  { z }  e.  Fin
147 eldifsni 3871 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  e.  ( I  \  { z } )  ->  i  =/=  z
)
148147adantl 453 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  /\  i  e.  ( I  \  { z } ) )  -> 
i  =/=  z )
149148neneqd 2566 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  /\  i  e.  ( I  \  { z } ) )  ->  -.  i  =  z
)
150 iffalse 3689 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  i  =  z  ->  if ( i  =  z ,  ( Y `  z ) ,  0 )  =  0 )
151149, 150syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  /\  i  e.  ( I  \  { z } ) )  ->  if ( i  =  z ,  ( Y `  z ) ,  0 )  =  0 )
152151suppss2 6239 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( `' ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z ) ,  0 ) ) " ( _V  \  { 0 } ) )  C_  { z } )
153 ssfi 7265 . . . . . . . . . . . . . . . . . 18  |-  ( ( { z }  e.  Fin  /\  ( `' ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z ) ,  0 ) ) " ( _V  \  { 0 } ) )  C_  { z } )  ->  ( `' ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z ) ,  0 ) )
" ( _V  \  { 0 } ) )  e.  Fin )
154146, 152, 153sylancr 645 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( `' ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z ) ,  0 ) ) " ( _V  \  { 0 } ) )  e.  Fin )
155145, 154eqeltrrd 2462 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( `' ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z ) ,  0 ) ) " NN )  e.  Fin )
1563psrbag 16358 . . . . . . . . . . . . . . . . 17  |-  ( I  e.  W  ->  (
( i  e.  I  |->  if ( i  =  z ,  ( Y `
 z ) ,  0 ) )  e.  D  <->  ( ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z
) ,  0 ) ) : I --> NN0  /\  ( `' ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z ) ,  0 ) )
" NN )  e. 
Fin ) ) )
157108, 156syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z
) ,  0 ) )  e.  D  <->  ( (
i  e.  I  |->  if ( i  =  z ,  ( Y `  z ) ,  0 ) ) : I --> NN0  /\  ( `' ( i  e.  I  |->  if ( i  =  z ,  ( Y `
 z ) ,  0 ) ) " NN )  e.  Fin ) ) )
158143, 155, 157mpbir2and 889 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z ) ,  0 ) )  e.  D )
15993, 107, 94, 95, 3, 108, 109, 130, 131, 158mplmonmul 16454 . . . . . . . . . . . . . 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 ) )  o F  +  ( i  e.  I  |->  if ( i  =  z ,  ( Y `
 z ) ,  0 ) ) ) ,  .1.  ,  .0.  ) ) )
160 mplcoe2.m . . . . . . . . . . . . . . . 16  |-  .^  =  (.g
`  G )
161 mplcoe2.v . . . . . . . . . . . . . . . 16  |-  V  =  ( I mVar  R )
16293, 3, 94, 95, 108, 49, 160, 161, 109, 137, 138mplcoe3 16456 . . . . . . . . . . . . . . 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 ) ) )
163162oveq2d 6036 . . . . . . . . . . . . . 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 ) ) ) )
164 eqidd 2388 . . . . . . . . . . . . . . . . . . 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 ) ) )
165 eqidd 2388 . . . . . . . . . . . . . . . . . . 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 ) ) )
166108, 114, 141, 164, 165offval2 6261 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) )  o F  +  ( 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 ) ) ) )
167111adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  ( Y `  i )  e.  NN0 )
168167nn0cnd 10208 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  ( Y `  i )  e.  CC )
169168addid2d 9199 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  ( 0  +  ( Y `  i
) )  =  ( Y `  i ) )
170 elsni 3781 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  e.  { z }  ->  i  =  z )
171170adantl 453 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  i  =  z )
172 simprlr 740 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  -.  z  e.  x )
173172ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  -.  z  e.  x )
174171, 173eqneltrd 2480 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  -.  i  e.  x )
175174, 122syl 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 )
176 iftrue 3688 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( i  =  z  ->  if ( i  =  z ,  ( Y `  z ) ,  0 )  =  ( Y `
 z ) )
177171, 176syl 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
) )
178171fveq2d 5672 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  ( Y `  i )  =  ( Y `  z ) )
179177, 178eqtr4d 2422 . . . . . . . . . . . . . . . . . . . . . 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
) )
180175, 179oveq12d 6038 . . . . . . . . . . . . . . . . . . . . 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
) ) )
181 simpr 448 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  i  e.  {
z } )
182132, 181sseldi 3289 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  i  e.  { z } )  ->  i  e.  ( x  u.  { z } ) )
183 iftrue 3688 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  e.  ( x  u. 
{ z } )  ->  if ( i  e.  ( x  u. 
{ z } ) ,  ( Y `  i ) ,  0 )  =  ( Y `
 i ) )
184182, 183syl 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 ) )
185169, 180, 1843eqtr4d 2429 . . . . . . . . . . . . . . . . . . . 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 ) )
186114adantr 452 . . . . . . . . . . . . . . . . . . . . . . 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 )
187186nn0cnd 10208 . . . . . . . . . . . . . . . . . . . . . 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 )
188187addid1d 9198 . . . . . . . . . . . . . . . . . . . . 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 ) )
189 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  -.  i  e.  { z } )  ->  -.  i  e.  { z } )
190 elsn 3772 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( i  e.  { z }  <-> 
i  =  z )
191189, 190sylnib 296 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( ( x  e. 
Fin  /\  -.  z  e.  x )  /\  (
x  u.  { z } )  C_  I
) )  /\  i  e.  I )  /\  -.  i  e.  { z } )  ->  -.  i  =  z )
192191, 150syl 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 )
193192oveq2d 6036 . . . . . . . . . . . . . . . . . . . . 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 ) )
194 biorf 395 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( -.  i  e.  { z }  ->  ( i  e.  x  <->  ( i  e. 
{ z }  \/  i  e.  x )
) )
195 elun 3431 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  e.  ( x  u. 
{ z } )  <-> 
( i  e.  x  \/  i  e.  { z } ) )
196 orcom 377 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( i  e.  x  \/  i  e.  { z } )  <->  ( i  e.  { z }  \/  i  e.  x )
)
197195, 196bitri 241 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( i  e.  ( x  u. 
{ z } )  <-> 
( i  e.  {
z }  \/  i  e.  x ) )
198194, 197syl6rbbr 256 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  i  e.  { z }  ->  ( i  e.  ( x  u.  {
z } )  <->  i  e.  x ) )
199198adantl 453 . . . . . . . . . . . . . . . . . . . . . 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
) )
200199ifbid 3700 . . . . . . . . . . . . . . . . . . . . 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 ) )
201188, 193, 2003eqtr4d 2429 . . . . . . . . . . . . . . . . . . . 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 ) )
202185, 201pm2.61dan 767 . . . . . . . . . . . . . . . . . . 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 ) )
203202mpteq2dva 4236 . . . . . . . . . . . . . . . . . 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 ) ) )
204166, 203eqtrd 2419 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i
) ,  0 ) )  o F  +  ( i  e.  I  |->  if ( i  =  z ,  ( Y `
 z ) ,  0 ) ) )  =  ( i  e.  I  |->  if ( i  e.  ( x  u. 
{ z } ) ,  ( Y `  i ) ,  0 ) ) )
205204eqeq2d 2398 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( y  =  ( ( i  e.  I  |->  if ( i  e.  x ,  ( Y `  i ) ,  0 ) )  o F  +  ( i  e.  I  |->  if ( i  =  z ,  ( Y `  z ) ,  0 ) ) )  <->  y  =  ( i  e.  I  |->  if ( i  e.  ( x  u.  {
z } ) ,  ( Y `  i
) ,  0 ) ) ) )
206205ifbid 3700 . . . . . . . . . . . . . . 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 ) )  o F  +  ( 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.  )
)
207206mpteq2dv 4237 . . . . . . . . . . . . . 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 ) )  o F  +  ( 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.  ) ) )
208159, 163, 2073eqtr3rd 2428 . . . . . . . . . . . . 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 ) ) ) )
20949, 107mgpbas 15581 . . . . . . . . . . . . . 14  |-  ( Base `  P )  =  (
Base `  G )
21049, 131mgpplusg 15579 . . . . . . . . . . . . . 14  |-  ( .r
`  P )  =  ( +g  `  G
)
21193mplcrng 16443 . . . . . . . . . . . . . . . . 17  |-  ( ( I  e.  W  /\  R  e.  CRing )  ->  P  e.  CRing )
2122, 96, 211syl2anc 643 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  P  e.  CRing )
21349crngmgp 15599 . . . . . . . . . . . . . . . 16  |-  ( P  e.  CRing  ->  G  e. CMnd )
214212, 213syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  G  e. CMnd )
215214adantr 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  G  e. CMnd )
216102, 133syl5ss 3302 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  x  C_  I
)
217216sselda 3291 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  /\  k  e.  x
)  ->  k  e.  I )
218 cmnmnd 15354 . . . . . . . . . . . . . . . . . . 19  |-  ( G  e. CMnd  ->  G  e.  Mnd )
219214, 218syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  G  e.  Mnd )
220219adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  I )  ->  G  e.  Mnd )
2217ffvelrnda 5809 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  I )  ->  ( Y `  k )  e.  NN0 )
2222adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  I )  ->  I  e.  W )
22398adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  I )  ->  R  e.  Ring )
224 simpr 448 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  I )  ->  k  e.  I )
22593, 161, 107, 222, 223, 224mvrcl 16439 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  I )  ->  ( V `  k )  e.  ( Base `  P
) )
226209, 160mulgnn0cl 14833 . . . . . . . . . . . . . . . . 17  |-  ( ( G  e.  Mnd  /\  ( Y `  k )  e.  NN0  /\  ( V `  k )  e.  ( Base `  P
) )  ->  (
( Y `  k
)  .^  ( V `  k ) )  e.  ( Base `  P
) )
227220, 221, 225, 226syl3anc 1184 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  I )  ->  (
( Y `  k
)  .^  ( V `  k ) )  e.  ( Base `  P
) )
228227adantlr 696 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  /\  k  e.  I
)  ->  ( ( Y `  k )  .^  ( V `  k
) )  e.  (
Base `  P )
)
229217, 228syldan 457 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
( x  e.  Fin  /\ 
-.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  /\  k  e.  x
)  ->  ( ( Y `  k )  .^  ( V `  k
) )  e.  (
Base `  P )
)
230219adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  G  e.  Mnd )
23193, 161, 107, 108, 109, 137mvrcl 16439 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( V `  z )  e.  (
Base `  P )
)
232209, 160mulgnn0cl 14833 . . . . . . . . . . . . . . 15  |-  ( ( G  e.  Mnd  /\  ( Y `  z )  e.  NN0  /\  ( V `  z )  e.  ( Base `  P
) )  ->  (
( Y `  z
)  .^  ( V `  z ) )  e.  ( Base `  P
) )
233230, 138, 231, 232syl3anc 1184 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Fin  /\  -.  z  e.  x
)  /\  ( x  u.  { z } ) 
C_  I ) )  ->  ( ( Y `
 z )  .^  ( V `  z ) )  e.  ( Base `  P ) )
234 fveq2 5668 . . . . . . . . . . . . . . 15  |-  ( k  =  z  ->  ( Y `  k )  =  ( Y `  z ) )
235 fveq2 5668 . . . . . . . . . . . . . . 15  |-  ( k  =  z  ->  ( V `  k )  =  ( V `  z ) )
236234, 235oveq12d 6038 . . . . . . . . . . . . . 14  |-  ( k  =  z  ->  (
( Y `  k
)  .^  ( V `  k ) )  =  ( ( Y `  z )  .^  ( V `  z )
) )
237209, 210, 215, 119, 229, 137, 172, 233, 236gsumunsn 15471 . . . . . . . . . . . . 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 ) ) ) )
238208, 237eqeq12d 2401 . . . . . . . . . . . 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 )
) ) ) )
239106, 238syl5ibr 213 . . . . . . . . . . 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 ) ) ) ) ) )
240239expr 599 . . . . . . . . . 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 ) ) ) ) ) ) )
241240a2d 24 . . . . . . . . 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 ) ) ) ) ) ) )
242105, 241syl5 30 . . . . . . . 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 ) ) ) ) ) ) )
243242expcom 425 . . . . . . 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 ) ) ) ) ) ) ) )
244243a2d 24 . . . . . 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 ) ) ) ) ) ) ) )
24556, 68, 80, 92, 101, 244findcard2s 7285 . . . . 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 )
) ) ) ) ) )
24632, 245mpcom 34 . . . 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 )
) ) ) ) )
24731, 246mpd 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 )
) ) ) )
248 resmpt 5131 . . . . 5  |-  ( ( `' Y " NN ) 
C_  I  ->  (
( k  e.  I  |->  ( ( Y `  k )  .^  ( V `  k )
) )  |`  ( `' Y " NN ) )  =  ( k  e.  ( `' Y " NN )  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) ) )
24931, 248syl 16 . . . 4  |-  ( ph  ->  ( ( k  e.  I  |->  ( ( Y `
 k )  .^  ( V `  k ) ) )  |`  ( `' Y " NN ) )  =  ( k  e.  ( `' Y " NN )  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) ) )
250249oveq2d 6036 . . 3  |-  ( ph  ->  ( G  gsumg  ( ( k  e.  I  |->  ( ( Y `
 k )  .^  ( V `  k ) ) )  |`  ( `' Y " NN ) ) )  =  ( G  gsumg  ( k  e.  ( `' Y " NN ) 
|->  ( ( Y `  k )  .^  ( V `  k )
) ) ) )
251 eqid 2387 . . . . 5  |-  ( k  e.  I  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) )  =  ( k  e.  I  |->  ( ( Y `
 k )  .^  ( V `  k ) ) )
252227, 251fmptd 5832 . . . 4  |-  ( ph  ->  ( k  e.  I  |->  ( ( Y `  k )  .^  ( V `  k )
) ) : I --> ( Base `  P
) )
2537, 16suppssr 5803 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( I  \  ( `' Y " NN ) ) )  ->  ( Y `  k )  =  0 )
254253oveq1d 6035 . . . . . 6  |-  ( (
ph  /\  k  e.  ( I  \  ( `' Y " NN ) ) )  ->  (
( Y `  k
)  .^  ( V `  k ) )  =  ( 0  .^  ( V `  k )
) )
255 eldifi 3412 . . . . . . . 8  |-  ( k  e.  ( I  \ 
( `' Y " NN ) )  ->  k  e.  I )
256255, 225sylan2 461 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( I  \  ( `' Y " NN ) ) )  ->  ( V `  k )  e.  ( Base `  P
) )
257209, 51, 160mulg0 14822 . . . . . . 7  |-  ( ( V `  k )  e.  ( Base `  P
)  ->  ( 0 
.^  ( V `  k ) )  =  ( 1r `  P
) )
258256, 257syl 16 . . . . . 6  |-  ( (
ph  /\  k  e.  ( I  \  ( `' Y " NN ) ) )  ->  (
0  .^  ( V `  k ) )  =  ( 1r `  P
) )
259254, 258eqtrd 2419 . . . . 5  |-  ( (
ph  /\  k  e.  ( I  \  ( `' Y " NN ) ) )  ->  (
( Y `  k
)  .^  ( V `  k ) )  =  ( 1r `  P
) )
260259suppss2 6239 . . . 4  |-  ( ph  ->  ( `' ( k  e.  I  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) )
" ( _V  \  { ( 1r `  P ) } ) )  C_  ( `' Y " NN ) )
261 ssfi 7265 . . . . 5  |-  ( ( ( `' Y " NN )  e.  Fin  /\  ( `' ( k  e.  I  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) )
" ( _V  \  { ( 1r `  P ) } ) )  C_  ( `' Y " NN ) )  ->  ( `' ( k  e.  I  |->  ( ( Y `  k
)  .^  ( V `  k ) ) )
" ( _V  \  { ( 1r `  P ) } ) )  e.  Fin )
26232, 260, 261syl2anc 643 . . . 4  |-  ( ph  ->  ( `' ( k  e.  I  |->  ( ( Y `  k ) 
.^  ( V `  k ) ) )
" ( _V  \  { ( 1r `  P ) } ) )  e.  Fin )
263209, 51, 214, 2, 252, 260, 262gsumres 15447 . . 3  |-  ( ph  ->  ( G  gsumg  ( ( k  e.  I  |->  ( ( Y `
 k )  .^  ( V `  k ) ) )  |`  ( `' Y " NN ) ) )  =  ( G  gsumg  ( k  e.  I  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) )
264247, 250, 2633eqtr2d 2425 . 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 )
) ) ) )
26527, 264eqtrd 2419 1  |-  ( ph  ->  ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) )  =  ( G  gsumg  ( k  e.  I  |->  ( ( Y `  k )  .^  ( V `  k )
) ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359    = wceq 1649    e. wcel 1717    =/= wne 2550   {crab 2653   _Vcvv 2899    \ cdif 3260    u. cun 3261    C_ wss 3263   (/)c0 3571   ifcif 3682   {csn 3757    e. cmpt 4207    X. cxp 4816   `'ccnv 4817   dom cdm 4818    |` cres 4820   "cima 4821   -->wf 5390   ` cfv 5394  (class class class)co 6020    o Fcof 6242    ^m cmap 6954   Fincfn 7045   0cc0 8923    + caddc 8926   NNcn 9932   NN0cn0 10153   Basecbs 13396   .rcmulr 13457   0gc0g 13650    gsumg cgsu 13651   Mndcmnd 14611  .gcmg 14616  CMndccmn 15339  mulGrpcmgp 15575   Ringcrg 15587   CRingccrg 15588   1rcur 15589   mVar cmvr 16334   mPoly cmpl 16335
This theorem is referenced by:  mplbas2  16458  ply1coe  16611
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-rep 4261  ax-sep 4271  ax-nul 4279  ax-pow 4318  ax-pr 4344  ax-un 4641  ax-inf2 7529  ax-cnex 8979  ax-resscn 8980  ax-1cn 8981  ax-icn 8982  ax-addcl 8983  ax-addrcl 8984  ax-mulcl 8985  ax-mulrcl 8986  ax-mulcom 8987  ax-addass 8988  ax-mulass 8989  ax-distr 8990  ax-i2m1 8991  ax-1ne0 8992  ax-1rid 8993  ax-rnegex 8994  ax-rrecex 8995  ax-cnre 8996  ax-pre-lttri 8997  ax-pre-lttrn 8998  ax-pre-ltadd 8999  ax-pre-mulgt0 9000
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-nel 2553  df-ral 2654  df-rex 2655  df-reu 2656  df-rmo 2657  df-rab 2658  df-v 2901  df-sbc 3105  df-csb 3195  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-pss 3279  df-nul 3572  df-if 3683  df-pw 3744  df-sn 3763  df-pr 3764  df-tp 3765  df-op 3766  df-uni 3958  df-int 3993  df-iun 4037  df-iin 4038  df-br 4154  df-opab 4208  df-mpt 4209  df-tr 4244  df-eprel 4435  df-id 4439  df-po 4444  df-so 4445  df-fr 4482  df-se 4483  df-we 4484  df-ord 4525  df-on 4526  df-lim 4527  df-suc 4528  df-om 4786  df-xp 4824  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-rn 4829  df-res 4830  df-ima 4831  df-iota 5358  df-fun 5396  df-fn 5397  df-f 5398  df-f1 5399  df-fo 5400  df-f1o 5401  df-fv 5402  df-isom 5403  df-ov 6023  df-oprab 6024  df-mpt2 6025  df-of 6244  df-ofr 6245  df-1st 6288  df-2nd 6289  df-riota 6485  df-recs 6569  df-rdg 6604  df-1o 6660  df-2o 6661  df-oadd 6664  df-er 6841  df-map 6956  df-pm 6957  df-ixp 7000  df-en 7046  df-dom 7047  df-sdom 7048  df-fin 7049  df-oi 7412  df-card 7759  df-pnf 9055  df-mnf 9056  df-xr 9057  df-ltxr 9058  df-le 9059  df-sub 9225  df-neg 9226  df-nn 9933  df-2 9990  df-3 9991  df-4 9992  df-5 9993  df-6 9994  df-7 9995  df-8 9996  df-9 9997  df-n0 10154  df-z 10215  df-uz 10421  df-fz 10976  df-fzo 11066  df-seq 11251  df-hash 11546  df-struct 13398  df-ndx 13399  df-slot 13400  df-base 13401  df-sets 13402  df-ress 13403  df-plusg 13469  df-mulr 13470  df-sca 13472  df-vsca 13473  df-tset 13475  df-0g 13654  df-gsum 13655  df-mre 13738  df-mrc 13739  df-acs 13741  df-mnd 14617  df-mhm 14665  df-submnd 14666  df-grp 14739  df-minusg 14740  df-mulg 14742  df-subg 14868  df-ghm 14931  df-cntz 15043  df-cmn 15341  df-abl 15342  df-mgp 15576  df-rng 15590  df-cring 15591  df-ur 15592  df-subrg 15793  df-psr 16344  df-mvr 16345  df-mpl 16346
  Copyright terms: Public domain W3C validator