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

Theorem mplmonmul 18737
Description: The product of two monomials adds the exponent vectors together. For example, the product of  ( x ^ 2 ) ( y ^
2 ) with  ( y ^ 1 ) ( z ^ 3 ) is  ( x ^ 2 ) ( y ^
3 ) ( z ^ 3 ), where the exponent vectors  <. 2 ,  2 ,  0 >. and  <. 0 ,  1 ,  3
>. are added to give  <. 2 ,  3 ,  3 >.. (Contributed by Mario Carneiro, 9-Jan-2015.)
Hypotheses
Ref Expression
mplmon.s  |-  P  =  ( I mPoly  R )
mplmon.b  |-  B  =  ( Base `  P
)
mplmon.z  |-  .0.  =  ( 0g `  R )
mplmon.o  |-  .1.  =  ( 1r `  R )
mplmon.d  |-  D  =  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin }
mplmon.i  |-  ( ph  ->  I  e.  W )
mplmon.r  |-  ( ph  ->  R  e.  Ring )
mplmon.x  |-  ( ph  ->  X  e.  D )
mplmonmul.t  |-  .x.  =  ( .r `  P )
mplmonmul.x  |-  ( ph  ->  Y  e.  D )
Assertion
Ref Expression
mplmonmul  |-  ( ph  ->  ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) )  .x.  ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) )  =  ( y  e.  D  |->  if ( y  =  ( X  oF  +  Y ) ,  .1.  ,  .0.  )
) )
Distinct variable groups:    y, D    f, I    ph, y    y, f, X    y,  .0.    y,  .1.    y, R    f, Y, y
Allowed substitution hints:    ph( f)    B( y, f)    D( f)    P( y, f)    R( f)    .x. ( y,
f)    .1. ( f)    I( y)    W( y, f)    .0. ( f)

Proof of Theorem mplmonmul
Dummy variables  j 
k  x  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mplmon.s . . 3  |-  P  =  ( I mPoly  R )
2 mplmon.b . . 3  |-  B  =  ( Base `  P
)
3 eqid 2462 . . 3  |-  ( .r
`  R )  =  ( .r `  R
)
4 mplmonmul.t . . 3  |-  .x.  =  ( .r `  P )
5 mplmon.d . . 3  |-  D  =  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin }
6 mplmon.z . . . 4  |-  .0.  =  ( 0g `  R )
7 mplmon.o . . . 4  |-  .1.  =  ( 1r `  R )
8 mplmon.i . . . 4  |-  ( ph  ->  I  e.  W )
9 mplmon.r . . . 4  |-  ( ph  ->  R  e.  Ring )
10 mplmon.x . . . 4  |-  ( ph  ->  X  e.  D )
111, 2, 6, 7, 5, 8, 9, 10mplmon 18736 . . 3  |-  ( ph  ->  ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) )  e.  B
)
12 mplmonmul.x . . . 4  |-  ( ph  ->  Y  e.  D )
131, 2, 6, 7, 5, 8, 9, 12mplmon 18736 . . 3  |-  ( ph  ->  ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) )  e.  B
)
141, 2, 3, 4, 5, 11, 13mplmul 18716 . 2  |-  ( ph  ->  ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) )  .x.  ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) )  =  ( k  e.  D  |->  ( R  gsumg  ( j  e.  {
x  e.  D  |  x  oR  <_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) ) ) ) )
15 eqeq1 2466 . . . . 5  |-  ( y  =  k  ->  (
y  =  ( X  oF  +  Y
)  <->  k  =  ( X  oF  +  Y ) ) )
1615ifbid 3915 . . . 4  |-  ( y  =  k  ->  if ( y  =  ( X  oF  +  Y ) ,  .1.  ,  .0.  )  =  if ( k  =  ( X  oF  +  Y ) ,  .1.  ,  .0.  ) )
1716cbvmptv 4509 . . 3  |-  ( y  e.  D  |->  if ( y  =  ( X  oF  +  Y
) ,  .1.  ,  .0.  ) )  =  ( k  e.  D  |->  if ( k  =  ( X  oF  +  Y ) ,  .1.  ,  .0.  ) )
18 simpr 467 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  ->  X  e.  { x  e.  D  |  x  oR  <_  k } )
1918snssd 4130 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  ->  { X }  C_  { x  e.  D  |  x  oR  <_  k } )
2019resmptd 5175 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( ( j  e. 
{ x  e.  D  |  x  oR 
<_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) )  |`  { X } )  =  ( j  e.  { X }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) ) )
2120oveq2d 6331 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( R  gsumg  ( ( j  e. 
{ x  e.  D  |  x  oR 
<_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) )  |`  { X } ) )  =  ( R  gsumg  ( j  e.  { X }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) ) ) )
229ad2antrr 737 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  ->  R  e.  Ring )
23 ringmnd 17838 . . . . . . . . 9  |-  ( R  e.  Ring  ->  R  e. 
Mnd )
2422, 23syl 17 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  ->  R  e.  Mnd )
2510ad2antrr 737 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  ->  X  e.  D )
26 iftrue 3899 . . . . . . . . . . . . 13  |-  ( y  =  X  ->  if ( y  =  X ,  .1.  ,  .0.  )  =  .1.  )
27 eqid 2462 . . . . . . . . . . . . 13  |-  ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) )  =  ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) )
28 fvex 5898 . . . . . . . . . . . . . 14  |-  ( 1r
`  R )  e. 
_V
297, 28eqeltri 2536 . . . . . . . . . . . . 13  |-  .1.  e.  _V
3026, 27, 29fvmpt 5971 . . . . . . . . . . . 12  |-  ( X  e.  D  ->  (
( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  X
)  =  .1.  )
3125, 30syl 17 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  X )  =  .1.  )
32 ssrab2 3526 . . . . . . . . . . . . 13  |-  { x  e.  D  |  x  oR  <_  k } 
C_  D
338ad2antrr 737 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  ->  I  e.  W )
34 simplr 767 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
k  e.  D )
35 eqid 2462 . . . . . . . . . . . . . . 15  |-  { x  e.  D  |  x  oR  <_  k }  =  { x  e.  D  |  x  oR  <_  k }
365, 35psrbagconcl 18646 . . . . . . . . . . . . . 14  |-  ( ( I  e.  W  /\  k  e.  D  /\  X  e.  { x  e.  D  |  x  oR  <_  k } )  ->  ( k  oF  -  X
)  e.  { x  e.  D  |  x  oR  <_  k } )
3733, 34, 18, 36syl3anc 1276 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( k  oF  -  X )  e. 
{ x  e.  D  |  x  oR 
<_  k } )
3832, 37sseldi 3442 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( k  oF  -  X )  e.  D )
39 eqeq1 2466 . . . . . . . . . . . . . 14  |-  ( y  =  ( k  oF  -  X )  ->  ( y  =  Y  <->  ( k  oF  -  X )  =  Y ) )
4039ifbid 3915 . . . . . . . . . . . . 13  |-  ( y  =  ( k  oF  -  X )  ->  if ( y  =  Y ,  .1.  ,  .0.  )  =  if ( ( k  oF  -  X )  =  Y ,  .1.  ,  .0.  ) )
41 eqid 2462 . . . . . . . . . . . . 13  |-  ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) )  =  ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) )
42 fvex 5898 . . . . . . . . . . . . . . 15  |-  ( 0g
`  R )  e. 
_V
436, 42eqeltri 2536 . . . . . . . . . . . . . 14  |-  .0.  e.  _V
4429, 43ifex 3961 . . . . . . . . . . . . 13  |-  if ( ( k  oF  -  X )  =  Y ,  .1.  ,  .0.  )  e.  _V
4540, 41, 44fvmpt 5971 . . . . . . . . . . . 12  |-  ( ( k  oF  -  X )  e.  D  ->  ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  ( k  oF  -  X ) )  =  if ( ( k  oF  -  X )  =  Y ,  .1.  ,  .0.  ) )
4638, 45syl 17 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  ( k  oF  -  X ) )  =  if ( ( k  oF  -  X )  =  Y ,  .1.  ,  .0.  ) )
4731, 46oveq12d 6333 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `
 X ) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  ( k  oF  -  X ) ) )  =  (  .1.  ( .r `  R
) if ( ( k  oF  -  X )  =  Y ,  .1.  ,  .0.  ) ) )
48 eqid 2462 . . . . . . . . . . . . . 14  |-  ( Base `  R )  =  (
Base `  R )
4948, 7ringidcl 17850 . . . . . . . . . . . . 13  |-  ( R  e.  Ring  ->  .1.  e.  ( Base `  R )
)
5048, 6ring0cl 17851 . . . . . . . . . . . . 13  |-  ( R  e.  Ring  ->  .0.  e.  ( Base `  R )
)
5149, 50ifcld 3936 . . . . . . . . . . . 12  |-  ( R  e.  Ring  ->  if ( ( k  oF  -  X )  =  Y ,  .1.  ,  .0.  )  e.  ( Base `  R ) )
5222, 51syl 17 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  ->  if ( ( k  oF  -  X )  =  Y ,  .1.  ,  .0.  )  e.  (
Base `  R )
)
5348, 3, 7ringlidm 17853 . . . . . . . . . . 11  |-  ( ( R  e.  Ring  /\  if ( ( k  oF  -  X )  =  Y ,  .1.  ,  .0.  )  e.  (
Base `  R )
)  ->  (  .1.  ( .r `  R ) if ( ( k  oF  -  X
)  =  Y ,  .1.  ,  .0.  ) )  =  if ( ( k  oF  -  X )  =  Y ,  .1.  ,  .0.  ) )
5422, 52, 53syl2anc 671 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
(  .1.  ( .r
`  R ) if ( ( k  oF  -  X )  =  Y ,  .1.  ,  .0.  ) )  =  if ( ( k  oF  -  X
)  =  Y ,  .1.  ,  .0.  ) )
555psrbagf 18638 . . . . . . . . . . . . . . . . . 18  |-  ( ( I  e.  W  /\  k  e.  D )  ->  k : I --> NN0 )
5633, 34, 55syl2anc 671 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
k : I --> NN0 )
5756ffvelrnda 6045 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR  <_  k } )  /\  z  e.  I )  ->  (
k `  z )  e.  NN0 )
588adantr 471 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  D )  ->  I  e.  W )
5910adantr 471 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  D )  ->  X  e.  D )
605psrbagf 18638 . . . . . . . . . . . . . . . . . . 19  |-  ( ( I  e.  W  /\  X  e.  D )  ->  X : I --> NN0 )
6158, 59, 60syl2anc 671 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  D )  ->  X : I --> NN0 )
6261ffvelrnda 6045 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  D )  /\  z  e.  I )  ->  ( X `  z )  e.  NN0 )
6362adantlr 726 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR  <_  k } )  /\  z  e.  I )  ->  ( X `  z )  e.  NN0 )
645psrbagf 18638 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( I  e.  W  /\  Y  e.  D )  ->  Y : I --> NN0 )
658, 12, 64syl2anc 671 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  Y : I --> NN0 )
6665adantr 471 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  D )  ->  Y : I --> NN0 )
6766ffvelrnda 6045 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  D )  /\  z  e.  I )  ->  ( Y `  z )  e.  NN0 )
6867adantlr 726 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR  <_  k } )  /\  z  e.  I )  ->  ( Y `  z )  e.  NN0 )
69 nn0cn 10908 . . . . . . . . . . . . . . . . 17  |-  ( ( k `  z )  e.  NN0  ->  ( k `
 z )  e.  CC )
70 nn0cn 10908 . . . . . . . . . . . . . . . . 17  |-  ( ( X `  z )  e.  NN0  ->  ( X `
 z )  e.  CC )
71 nn0cn 10908 . . . . . . . . . . . . . . . . 17  |-  ( ( Y `  z )  e.  NN0  ->  ( Y `
 z )  e.  CC )
72 subadd 9904 . . . . . . . . . . . . . . . . 17  |-  ( ( ( k `  z
)  e.  CC  /\  ( X `  z )  e.  CC  /\  ( Y `  z )  e.  CC )  ->  (
( ( k `  z )  -  ( X `  z )
)  =  ( Y `
 z )  <->  ( ( X `  z )  +  ( Y `  z ) )  =  ( k `  z
) ) )
7369, 70, 71, 72syl3an 1318 . . . . . . . . . . . . . . . 16  |-  ( ( ( k `  z
)  e.  NN0  /\  ( X `  z )  e.  NN0  /\  ( Y `  z )  e.  NN0 )  ->  (
( ( k `  z )  -  ( X `  z )
)  =  ( Y `
 z )  <->  ( ( X `  z )  +  ( Y `  z ) )  =  ( k `  z
) ) )
7457, 63, 68, 73syl3anc 1276 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR  <_  k } )  /\  z  e.  I )  ->  (
( ( k `  z )  -  ( X `  z )
)  =  ( Y `
 z )  <->  ( ( X `  z )  +  ( Y `  z ) )  =  ( k `  z
) ) )
75 eqcom 2469 . . . . . . . . . . . . . . 15  |-  ( ( ( X `  z
)  +  ( Y `
 z ) )  =  ( k `  z )  <->  ( k `  z )  =  ( ( X `  z
)  +  ( Y `
 z ) ) )
7674, 75syl6bb 269 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR  <_  k } )  /\  z  e.  I )  ->  (
( ( k `  z )  -  ( X `  z )
)  =  ( Y `
 z )  <->  ( k `  z )  =  ( ( X `  z
)  +  ( Y `
 z ) ) ) )
7776ralbidva 2836 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( A. z  e.  I  ( ( k `
 z )  -  ( X `  z ) )  =  ( Y `
 z )  <->  A. z  e.  I  ( k `  z )  =  ( ( X `  z
)  +  ( Y `
 z ) ) ) )
78 mpteqb 5987 . . . . . . . . . . . . . 14  |-  ( A. z  e.  I  (
( k `  z
)  -  ( X `
 z ) )  e.  _V  ->  (
( z  e.  I  |->  ( ( k `  z )  -  ( X `  z )
) )  =  ( z  e.  I  |->  ( Y `  z ) )  <->  A. z  e.  I 
( ( k `  z )  -  ( X `  z )
)  =  ( Y `
 z ) ) )
79 ovex 6343 . . . . . . . . . . . . . . 15  |-  ( ( k `  z )  -  ( X `  z ) )  e. 
_V
8079a1i 11 . . . . . . . . . . . . . 14  |-  ( z  e.  I  ->  (
( k `  z
)  -  ( X `
 z ) )  e.  _V )
8178, 80mprg 2763 . . . . . . . . . . . . 13  |-  ( ( z  e.  I  |->  ( ( k `  z
)  -  ( X `
 z ) ) )  =  ( z  e.  I  |->  ( Y `
 z ) )  <->  A. z  e.  I 
( ( k `  z )  -  ( X `  z )
)  =  ( Y `
 z ) )
82 mpteqb 5987 . . . . . . . . . . . . . 14  |-  ( A. z  e.  I  (
k `  z )  e.  _V  ->  ( (
z  e.  I  |->  ( k `  z ) )  =  ( z  e.  I  |->  ( ( X `  z )  +  ( Y `  z ) ) )  <->  A. z  e.  I 
( k `  z
)  =  ( ( X `  z )  +  ( Y `  z ) ) ) )
83 fvex 5898 . . . . . . . . . . . . . . 15  |-  ( k `
 z )  e. 
_V
8483a1i 11 . . . . . . . . . . . . . 14  |-  ( z  e.  I  ->  (
k `  z )  e.  _V )
8582, 84mprg 2763 . . . . . . . . . . . . 13  |-  ( ( z  e.  I  |->  ( k `  z ) )  =  ( z  e.  I  |->  ( ( X `  z )  +  ( Y `  z ) ) )  <->  A. z  e.  I 
( k `  z
)  =  ( ( X `  z )  +  ( Y `  z ) ) )
8677, 81, 853bitr4g 296 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( ( z  e.  I  |->  ( ( k `
 z )  -  ( X `  z ) ) )  =  ( z  e.  I  |->  ( Y `  z ) )  <->  ( z  e.  I  |->  ( k `  z ) )  =  ( z  e.  I  |->  ( ( X `  z )  +  ( Y `  z ) ) ) ) )
8756feqmptd 5941 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
k  =  ( z  e.  I  |->  ( k `
 z ) ) )
8861feqmptd 5941 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  D )  ->  X  =  ( z  e.  I  |->  ( X `  z ) ) )
8988adantr 471 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  ->  X  =  ( z  e.  I  |->  ( X `
 z ) ) )
9033, 57, 63, 87, 89offval2 6575 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( k  oF  -  X )  =  ( z  e.  I  |->  ( ( k `  z )  -  ( X `  z )
) ) )
9166feqmptd 5941 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  D )  ->  Y  =  ( z  e.  I  |->  ( Y `  z ) ) )
9291adantr 471 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  ->  Y  =  ( z  e.  I  |->  ( Y `
 z ) ) )
9390, 92eqeq12d 2477 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( ( k  oF  -  X )  =  Y  <->  ( z  e.  I  |->  ( ( k `  z )  -  ( X `  z ) ) )  =  ( z  e.  I  |->  ( Y `  z ) ) ) )
9458, 62, 67, 88, 91offval2 6575 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  D )  ->  ( X  oF  +  Y
)  =  ( z  e.  I  |->  ( ( X `  z )  +  ( Y `  z ) ) ) )
9594adantr 471 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( X  oF  +  Y )  =  ( z  e.  I  |->  ( ( X `  z )  +  ( Y `  z ) ) ) )
9687, 95eqeq12d 2477 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( k  =  ( X  oF  +  Y )  <->  ( z  e.  I  |->  ( k `
 z ) )  =  ( z  e.  I  |->  ( ( X `
 z )  +  ( Y `  z
) ) ) ) )
9786, 93, 963bitr4d 293 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( ( k  oF  -  X )  =  Y  <->  k  =  ( X  oF  +  Y ) ) )
9897ifbid 3915 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  ->  if ( ( k  oF  -  X )  =  Y ,  .1.  ,  .0.  )  =  if ( k  =  ( X  oF  +  Y ) ,  .1.  ,  .0.  ) )
9947, 54, 983eqtrd 2500 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `
 X ) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  ( k  oF  -  X ) ) )  =  if ( k  =  ( X  oF  +  Y
) ,  .1.  ,  .0.  ) )
10098, 52eqeltrrd 2541 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  ->  if ( k  =  ( X  oF  +  Y ) ,  .1.  ,  .0.  )  e.  (
Base `  R )
)
10199, 100eqeltrd 2540 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `
 X ) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  ( k  oF  -  X ) ) )  e.  ( Base `  R ) )
102 fveq2 5888 . . . . . . . . . 10  |-  ( j  =  X  ->  (
( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
)  =  ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  X
) )
103 oveq2 6323 . . . . . . . . . . 11  |-  ( j  =  X  ->  (
k  oF  -  j )  =  ( k  oF  -  X ) )
104103fveq2d 5892 . . . . . . . . . 10  |-  ( j  =  X  ->  (
( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) )  =  ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  ( k  oF  -  X ) ) )
105102, 104oveq12d 6333 . . . . . . . . 9  |-  ( j  =  X  ->  (
( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j ) ( .r
`  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) )  =  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  X
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  X ) ) ) )
10648, 105gsumsn 17636 . . . . . . . 8  |-  ( ( R  e.  Mnd  /\  X  e.  D  /\  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `
 X ) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  ( k  oF  -  X ) ) )  e.  ( Base `  R ) )  -> 
( R  gsumg  ( j  e.  { X }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) ) )  =  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  X ) ( .r
`  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  X ) ) ) )
10724, 25, 101, 106syl3anc 1276 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( R  gsumg  ( j  e.  { X }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) ) )  =  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  X ) ( .r
`  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  X ) ) ) )
10821, 107, 993eqtrd 2500 . . . . . 6  |-  ( ( ( ph  /\  k  e.  D )  /\  X  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( R  gsumg  ( ( j  e. 
{ x  e.  D  |  x  oR 
<_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) )  |`  { X } ) )  =  if ( k  =  ( X  oF  +  Y ) ,  .1.  ,  .0.  )
)
1096gsum0 16570 . . . . . . 7  |-  ( R 
gsumg  (/) )  =  .0.
110 disjsn 4044 . . . . . . . . 9  |-  ( ( { x  e.  D  |  x  oR 
<_  k }  i^i  { X } )  =  (/)  <->  -.  X  e.  { x  e.  D  |  x  oR  <_  k } )
1119ad2antrr 737 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  D )  /\  j  e.  { x  e.  D  |  x  oR 
<_  k } )  ->  R  e.  Ring )
1121, 48, 2, 5, 11mplelf 18706 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) : D --> ( Base `  R )
)
113112ad2antrr 737 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  D )  /\  j  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) : D --> ( Base `  R )
)
114 simpr 467 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  D )  /\  j  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
j  e.  { x  e.  D  |  x  oR  <_  k } )
11532, 114sseldi 3442 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  D )  /\  j  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
j  e.  D )
116113, 115ffvelrnd 6046 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  D )  /\  j  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j )  e.  (
Base `  R )
)
1171, 48, 2, 5, 13mplelf 18706 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) : D --> ( Base `  R )
)
118117ad2antrr 737 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  D )  /\  j  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) : D --> ( Base `  R )
)
1198ad2antrr 737 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  D )  /\  j  e.  { x  e.  D  |  x  oR 
<_  k } )  ->  I  e.  W )
120 simplr 767 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  D )  /\  j  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
k  e.  D )
1215, 35psrbagconcl 18646 . . . . . . . . . . . . . . . 16  |-  ( ( I  e.  W  /\  k  e.  D  /\  j  e.  { x  e.  D  |  x  oR  <_  k } )  ->  ( k  oF  -  j
)  e.  { x  e.  D  |  x  oR  <_  k } )
122119, 120, 114, 121syl3anc 1276 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  D )  /\  j  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( k  oF  -  j )  e. 
{ x  e.  D  |  x  oR 
<_  k } )
12332, 122sseldi 3442 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  D )  /\  j  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( k  oF  -  j )  e.  D )
124118, 123ffvelrnd 6046 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  D )  /\  j  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  ( k  oF  -  j ) )  e.  ( Base `  R
) )
12548, 3ringcl 17843 . . . . . . . . . . . . 13  |-  ( ( R  e.  Ring  /\  (
( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
)  e.  ( Base `  R )  /\  (
( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) )  e.  ( Base `  R
) )  ->  (
( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j ) ( .r
`  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) )  e.  ( Base `  R
) )
126111, 116, 124, 125syl3anc 1276 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  D )  /\  j  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `
 j ) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  ( k  oF  -  j ) ) )  e.  ( Base `  R ) )
127 eqid 2462 . . . . . . . . . . . 12  |-  ( j  e.  { x  e.  D  |  x  oR  <_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `
 j ) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  ( k  oF  -  j ) ) ) )  =  ( j  e.  { x  e.  D  |  x  oR  <_  k } 
|->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `
 j ) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  ( k  oF  -  j ) ) ) )
128126, 127fmptd 6069 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  D )  ->  (
j  e.  { x  e.  D  |  x  oR  <_  k } 
|->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `
 j ) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  ( k  oF  -  j ) ) ) ) : {
x  e.  D  |  x  oR  <_  k }
--> ( Base `  R
) )
129 ffn 5751 . . . . . . . . . . 11  |-  ( ( j  e.  { x  e.  D  |  x  oR  <_  k } 
|->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `
 j ) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  ( k  oF  -  j ) ) ) ) : {
x  e.  D  |  x  oR  <_  k }
--> ( Base `  R
)  ->  ( j  e.  { x  e.  D  |  x  oR 
<_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) )  Fn  { x  e.  D  |  x  oR  <_  k } )
130 fnresdisj 5708 . . . . . . . . . . 11  |-  ( ( j  e.  { x  e.  D  |  x  oR  <_  k } 
|->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `
 j ) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  ( k  oF  -  j ) ) ) )  Fn  {
x  e.  D  |  x  oR  <_  k }  ->  ( ( { x  e.  D  |  x  oR  <_  k }  i^i  { X }
)  =  (/)  <->  ( (
j  e.  { x  e.  D  |  x  oR  <_  k } 
|->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `
 j ) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  ( k  oF  -  j ) ) ) )  |`  { X } )  =  (/) ) )
131128, 129, 1303syl 18 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  D )  ->  (
( { x  e.  D  |  x  oR  <_  k }  i^i  { X } )  =  (/)  <->  ( ( j  e.  { x  e.  D  |  x  oR  <_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `
 j ) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  ( k  oF  -  j ) ) ) )  |`  { X } )  =  (/) ) )
132131biimpa 491 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  D )  /\  ( { x  e.  D  |  x  oR 
<_  k }  i^i  { X } )  =  (/) )  ->  ( ( j  e.  { x  e.  D  |  x  oR  <_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `
 j ) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  ( k  oF  -  j ) ) ) )  |`  { X } )  =  (/) )
133110, 132sylan2br 483 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  D )  /\  -.  X  e.  { x  e.  D  |  x  oR  <_  k } )  ->  ( (
j  e.  { x  e.  D  |  x  oR  <_  k } 
|->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `
 j ) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  ( k  oF  -  j ) ) ) )  |`  { X } )  =  (/) )
134133oveq2d 6331 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  D )  /\  -.  X  e.  { x  e.  D  |  x  oR  <_  k } )  ->  ( R  gsumg  ( ( j  e.  {
x  e.  D  |  x  oR  <_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) )  |`  { X } ) )  =  ( R  gsumg  (/) ) )
13562nn0red 10955 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  D )  /\  z  e.  I )  ->  ( X `  z )  e.  RR )
136 nn0addge1 10945 . . . . . . . . . . . . . 14  |-  ( ( ( X `  z
)  e.  RR  /\  ( Y `  z )  e.  NN0 )  -> 
( X `  z
)  <_  ( ( X `  z )  +  ( Y `  z ) ) )
137135, 67, 136syl2anc 671 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  D )  /\  z  e.  I )  ->  ( X `  z )  <_  ( ( X `  z )  +  ( Y `  z ) ) )
138137ralrimiva 2814 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  D )  ->  A. z  e.  I  ( X `  z )  <_  (
( X `  z
)  +  ( Y `
 z ) ) )
139 ovex 6343 . . . . . . . . . . . . . 14  |-  ( ( X `  z )  +  ( Y `  z ) )  e. 
_V
140139a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  D )  /\  z  e.  I )  ->  (
( X `  z
)  +  ( Y `
 z ) )  e.  _V )
14158, 62, 140, 88, 94ofrfval2 6576 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  D )  ->  ( X  oR  <_  ( X  oF  +  Y
)  <->  A. z  e.  I 
( X `  z
)  <_  ( ( X `  z )  +  ( Y `  z ) ) ) )
142138, 141mpbird 240 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  D )  ->  X  oR  <_  ( X  oF  +  Y
) )
143 breq1 4419 . . . . . . . . . . . 12  |-  ( x  =  X  ->  (
x  oR  <_ 
( X  oF  +  Y )  <->  X  oR  <_  ( X  oF  +  Y )
) )
144143elrab 3208 . . . . . . . . . . 11  |-  ( X  e.  { x  e.  D  |  x  oR  <_  ( X  oF  +  Y
) }  <->  ( X  e.  D  /\  X  oR  <_  ( X  oF  +  Y )
) )
14559, 142, 144sylanbrc 675 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  D )  ->  X  e.  { x  e.  D  |  x  oR 
<_  ( X  oF  +  Y ) } )
146 breq2 4420 . . . . . . . . . . . 12  |-  ( k  =  ( X  oF  +  Y )  ->  ( x  oR  <_  k  <->  x  oR  <_  ( X  oF  +  Y )
) )
147146rabbidv 3048 . . . . . . . . . . 11  |-  ( k  =  ( X  oF  +  Y )  ->  { x  e.  D  |  x  oR 
<_  k }  =  {
x  e.  D  |  x  oR  <_  ( X  oF  +  Y
) } )
148147eleq2d 2525 . . . . . . . . . 10  |-  ( k  =  ( X  oF  +  Y )  ->  ( X  e.  {
x  e.  D  |  x  oR  <_  k } 
<->  X  e.  { x  e.  D  |  x  oR  <_  ( X  oF  +  Y
) } ) )
149145, 148syl5ibrcom 230 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  D )  ->  (
k  =  ( X  oF  +  Y
)  ->  X  e.  { x  e.  D  |  x  oR  <_  k } ) )
150149con3dimp 447 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  D )  /\  -.  X  e.  { x  e.  D  |  x  oR  <_  k } )  ->  -.  k  =  ( X  oF  +  Y )
)
151150iffalsed 3904 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  D )  /\  -.  X  e.  { x  e.  D  |  x  oR  <_  k } )  ->  if (
k  =  ( X  oF  +  Y
) ,  .1.  ,  .0.  )  =  .0.  )
152109, 134, 1513eqtr4a 2522 . . . . . 6  |-  ( ( ( ph  /\  k  e.  D )  /\  -.  X  e.  { x  e.  D  |  x  oR  <_  k } )  ->  ( R  gsumg  ( ( j  e.  {
x  e.  D  |  x  oR  <_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) )  |`  { X } ) )  =  if ( k  =  ( X  oF  +  Y ) ,  .1.  ,  .0.  )
)
153108, 152pm2.61dan 805 . . . . 5  |-  ( (
ph  /\  k  e.  D )  ->  ( R  gsumg  ( ( j  e. 
{ x  e.  D  |  x  oR 
<_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) )  |`  { X } ) )  =  if ( k  =  ( X  oF  +  Y ) ,  .1.  ,  .0.  )
)
1549adantr 471 . . . . . . 7  |-  ( (
ph  /\  k  e.  D )  ->  R  e.  Ring )
155 ringcmn 17860 . . . . . . 7  |-  ( R  e.  Ring  ->  R  e. CMnd
)
156154, 155syl 17 . . . . . 6  |-  ( (
ph  /\  k  e.  D )  ->  R  e. CMnd )
1575psrbaglefi 18645 . . . . . . 7  |-  ( ( I  e.  W  /\  k  e.  D )  ->  { x  e.  D  |  x  oR 
<_  k }  e.  Fin )
1588, 157sylan 478 . . . . . 6  |-  ( (
ph  /\  k  e.  D )  ->  { x  e.  D  |  x  oR  <_  k }  e.  Fin )
159 ssdif 3580 . . . . . . . . . . . 12  |-  ( { x  e.  D  |  x  oR  <_  k }  C_  D  ->  ( { x  e.  D  |  x  oR 
<_  k }  \  { X } )  C_  ( D  \  { X }
) )
16032, 159ax-mp 5 . . . . . . . . . . 11  |-  ( { x  e.  D  |  x  oR  <_  k }  \  { X }
)  C_  ( D  \  { X } )
161160sseli 3440 . . . . . . . . . 10  |-  ( j  e.  ( { x  e.  D  |  x  oR  <_  k } 
\  { X }
)  ->  j  e.  ( D  \  { X } ) )
162112adantr 471 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  D )  ->  (
y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) : D --> ( Base `  R )
)
163 eldifsni 4111 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( D  \  { X } )  -> 
y  =/=  X )
164163adantl 472 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  D )  /\  y  e.  ( D  \  { X } ) )  -> 
y  =/=  X )
165164neneqd 2640 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  D )  /\  y  e.  ( D  \  { X } ) )  ->  -.  y  =  X
)
166165iffalsed 3904 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  D )  /\  y  e.  ( D  \  { X } ) )  ->  if ( y  =  X ,  .1.  ,  .0.  )  =  .0.  )
167 ovex 6343 . . . . . . . . . . . . . 14  |-  ( NN0 
^m  I )  e. 
_V
1685, 167rabex2 4570 . . . . . . . . . . . . 13  |-  D  e. 
_V
169168a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  D )  ->  D  e.  _V )
170166, 169suppss2 6976 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  D )  ->  (
( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) supp  .0.  )  C_ 
{ X } )
17143a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  D )  ->  .0.  e.  _V )
172162, 170, 169, 171suppssr 6973 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  D )  /\  j  e.  ( D  \  { X } ) )  -> 
( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j )  =  .0.  )
173161, 172sylan2 481 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  D )  /\  j  e.  ( { x  e.  D  |  x  oR  <_  k }  \  { X } ) )  ->  ( (
y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
)  =  .0.  )
174173oveq1d 6330 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  D )  /\  j  e.  ( { x  e.  D  |  x  oR  <_  k }  \  { X } ) )  ->  ( (
( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) )  =  (  .0.  ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) )
175 eldifi 3567 . . . . . . . . 9  |-  ( j  e.  ( { x  e.  D  |  x  oR  <_  k } 
\  { X }
)  ->  j  e.  { x  e.  D  |  x  oR  <_  k } )
17648, 3, 6ringlz 17866 . . . . . . . . . 10  |-  ( ( R  e.  Ring  /\  (
( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) )  e.  ( Base `  R
) )  ->  (  .0.  ( .r `  R
) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `
 ( k  oF  -  j ) ) )  =  .0.  )
177111, 124, 176syl2anc 671 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  D )  /\  j  e.  { x  e.  D  |  x  oR 
<_  k } )  -> 
(  .0.  ( .r
`  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) )  =  .0.  )
178175, 177sylan2 481 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  D )  /\  j  e.  ( { x  e.  D  |  x  oR  <_  k }  \  { X } ) )  ->  (  .0.  ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  ( k  oF  -  j ) ) )  =  .0.  )
179174, 178eqtrd 2496 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  D )  /\  j  e.  ( { x  e.  D  |  x  oR  <_  k }  \  { X } ) )  ->  ( (
( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) )  =  .0.  )
180168rabex 4568 . . . . . . . 8  |-  { x  e.  D  |  x  oR  <_  k }  e.  _V
181180a1i 11 . . . . . . 7  |-  ( (
ph  /\  k  e.  D )  ->  { x  e.  D  |  x  oR  <_  k }  e.  _V )
182179, 181suppss2 6976 . . . . . 6  |-  ( (
ph  /\  k  e.  D )  ->  (
( j  e.  {
x  e.  D  |  x  oR  <_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) ) supp  .0.  )  C_  { X } )
183168mptrabex 6162 . . . . . . . . 9  |-  ( j  e.  { x  e.  D  |  x  oR  <_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `
 j ) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  ( k  oF  -  j ) ) ) )  e.  _V
184 funmpt 5637 . . . . . . . . 9  |-  Fun  (
j  e.  { x  e.  D  |  x  oR  <_  k } 
|->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `
 j ) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  ( k  oF  -  j ) ) ) )
185183, 184, 433pm3.2i 1192 . . . . . . . 8  |-  ( ( j  e.  { x  e.  D  |  x  oR  <_  k } 
|->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `
 j ) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  ( k  oF  -  j ) ) ) )  e.  _V  /\ 
Fun  ( j  e. 
{ x  e.  D  |  x  oR 
<_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) )  /\  .0.  e.  _V )
186185a1i 11 . . . . . . 7  |-  ( (
ph  /\  k  e.  D )  ->  (
( j  e.  {
x  e.  D  |  x  oR  <_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) )  e.  _V  /\  Fun  ( j  e.  {
x  e.  D  |  x  oR  <_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) )  /\  .0.  e.  _V ) )
187 snfi 7676 . . . . . . . 8  |-  { X }  e.  Fin
188187a1i 11 . . . . . . 7  |-  ( (
ph  /\  k  e.  D )  ->  { X }  e.  Fin )
189 suppssfifsupp 7924 . . . . . . 7  |-  ( ( ( ( j  e. 
{ x  e.  D  |  x  oR 
<_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) )  e.  _V  /\  Fun  ( j  e.  {
x  e.  D  |  x  oR  <_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) )  /\  .0.  e.  _V )  /\  ( { X }  e.  Fin  /\  ( ( j  e. 
{ x  e.  D  |  x  oR 
<_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) ) supp  .0.  )  C_  { X } ) )  ->  ( j  e. 
{ x  e.  D  |  x  oR 
<_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) ) finSupp  .0.  )
190186, 188, 182, 189syl12anc 1274 . . . . . 6  |-  ( (
ph  /\  k  e.  D )  ->  (
j  e.  { x  e.  D  |  x  oR  <_  k } 
|->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `
 j ) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  ( k  oF  -  j ) ) ) ) finSupp  .0.  )
19148, 6, 156, 158, 128, 182, 190gsumres 17596 . . . . 5  |-  ( (
ph  /\  k  e.  D )  ->  ( R  gsumg  ( ( j  e. 
{ x  e.  D  |  x  oR 
<_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) )  |`  { X } ) )  =  ( R  gsumg  ( j  e.  {
x  e.  D  |  x  oR  <_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) ) ) )
192153, 191eqtr3d 2498 . . . 4  |-  ( (
ph  /\  k  e.  D )  ->  if ( k  =  ( X  oF  +  Y ) ,  .1.  ,  .0.  )  =  ( R  gsumg  ( j  e.  {
x  e.  D  |  x  oR  <_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) ) ) )
193192mpteq2dva 4503 . . 3  |-  ( ph  ->  ( k  e.  D  |->  if ( k  =  ( X  oF  +  Y ) ,  .1.  ,  .0.  )
)  =  ( k  e.  D  |->  ( R 
gsumg  ( j  e.  {
x  e.  D  |  x  oR  <_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) ) ) ) )
19417, 193syl5eq 2508 . 2  |-  ( ph  ->  ( y  e.  D  |->  if ( y  =  ( X  oF  +  Y ) ,  .1.  ,  .0.  )
)  =  ( k  e.  D  |->  ( R 
gsumg  ( j  e.  {
x  e.  D  |  x  oR  <_  k }  |->  ( ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) ) `  j
) ( .r `  R ) ( ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) `  (
k  oF  -  j ) ) ) ) ) ) )
19514, 194eqtr4d 2499 1  |-  ( ph  ->  ( ( y  e.  D  |->  if ( y  =  X ,  .1.  ,  .0.  ) )  .x.  ( y  e.  D  |->  if ( y  =  Y ,  .1.  ,  .0.  ) ) )  =  ( y  e.  D  |->  if ( y  =  ( X  oF  +  Y ) ,  .1.  ,  .0.  )
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 375    /\ w3a 991    = wceq 1455    e. wcel 1898    =/= wne 2633   A.wral 2749   {crab 2753   _Vcvv 3057    \ cdif 3413    i^i cin 3415    C_ wss 3416   (/)c0 3743   ifcif 3893   {csn 3980   class class class wbr 4416    |-> cmpt 4475   `'ccnv 4852    |` cres 4855   "cima 4856   Fun wfun 5595    Fn wfn 5596   -->wf 5597   ` cfv 5601  (class class class)co 6315    oFcof 6556    oRcofr 6557   supp csupp 6941    ^m cmap 7498   Fincfn 7595   finSupp cfsupp 7909   CCcc 9563   RRcr 9564    + caddc 9568    <_ cle 9702    - cmin 9886   NNcn 10637   NN0cn0 10898   Basecbs 15170   .rcmulr 15240   0gc0g 15387    gsumg cgsu 15388   Mndcmnd 16584  CMndccmn 17479   1rcur 17784   Ringcrg 17829   mPoly cmpl 18626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-inf2 8172  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-se 4813  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-of 6558  df-ofr 6559  df-om 6720  df-1st 6820  df-2nd 6821  df-supp 6942  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-1o 7208  df-2o 7209  df-oadd 7212  df-er 7389  df-map 7500  df-pm 7501  df-ixp 7549  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-fsupp 7910  df-oi 8051  df-card 8399  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-nn 10638  df-2 10696  df-3 10697  df-4 10698  df-5 10699  df-6 10700  df-7 10701  df-8 10702  df-9 10703  df-n0 10899  df-z 10967  df-uz 11189  df-fz 11814  df-fzo 11947  df-seq 12246  df-hash 12548  df-struct 15172  df-ndx 15173  df-slot 15174  df-base 15175  df-sets 15176  df-ress 15177  df-plusg 15252  df-mulr 15253  df-sca 15255  df-vsca 15256  df-tset 15258  df-0g 15389  df-gsum 15390  df-mgm 16537  df-sgrp 16576  df-mnd 16586  df-grp 16722  df-minusg 16723  df-mulg 16725  df-cntz 17020  df-cmn 17481  df-abl 17482  df-mgp 17773  df-ur 17785  df-ring 17831  df-psr 18629  df-mpl 18631
This theorem is referenced by:  mplcoe3  18739  mplcoe5  18741  mplmon2mul  18773
  Copyright terms: Public domain W3C validator