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

Theorem mdegmullem 21508
Description: Lemma for mdegmulle2 21509. (Contributed by Stefan O'Rear, 26-Mar-2015.)
Hypotheses
Ref Expression
mdegaddle.y  |-  Y  =  ( I mPoly  R )
mdegaddle.d  |-  D  =  ( I mDeg  R )
mdegaddle.i  |-  ( ph  ->  I  e.  V )
mdegaddle.r  |-  ( ph  ->  R  e.  Ring )
mdegmulle2.b  |-  B  =  ( Base `  Y
)
mdegmulle2.t  |-  .x.  =  ( .r `  Y )
mdegmulle2.f  |-  ( ph  ->  F  e.  B )
mdegmulle2.g  |-  ( ph  ->  G  e.  B )
mdegmulle2.j1  |-  ( ph  ->  J  e.  NN0 )
mdegmulle2.k1  |-  ( ph  ->  K  e.  NN0 )
mdegmulle2.j2  |-  ( ph  ->  ( D `  F
)  <_  J )
mdegmulle2.k2  |-  ( ph  ->  ( D `  G
)  <_  K )
mdegmullem.a  |-  A  =  { a  e.  ( NN0  ^m  I )  |  ( `' a
" NN )  e. 
Fin }
mdegmullem.h  |-  H  =  ( b  e.  A  |->  (fld 
gsumg  b ) )
Assertion
Ref Expression
mdegmullem  |-  ( ph  ->  ( D `  ( F  .x.  G ) )  <_  ( J  +  K ) )
Distinct variable groups:    I, a,
b    R, b    V, b    A, b
Allowed substitution hints:    ph( a, b)    A( a)    B( a, b)    D( a, b)    R( a)    .x. ( a, b)    F( a, b)    G( a, b)    H( a, b)    J( a, b)    K( a, b)    V( a)    Y( a, b)

Proof of Theorem mdegmullem
Dummy variables  c 
d  x  e are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mdegaddle.y . . . . . . . 8  |-  Y  =  ( I mPoly  R )
2 mdegmulle2.b . . . . . . . 8  |-  B  =  ( Base `  Y
)
3 eqid 2441 . . . . . . . 8  |-  ( .r
`  R )  =  ( .r `  R
)
4 mdegmulle2.t . . . . . . . 8  |-  .x.  =  ( .r `  Y )
5 mdegmullem.a . . . . . . . 8  |-  A  =  { a  e.  ( NN0  ^m  I )  |  ( `' a
" NN )  e. 
Fin }
6 mdegmulle2.f . . . . . . . 8  |-  ( ph  ->  F  e.  B )
7 mdegmulle2.g . . . . . . . 8  |-  ( ph  ->  G  e.  B )
81, 2, 3, 4, 5, 6, 7mplmul 17500 . . . . . . 7  |-  ( ph  ->  ( F  .x.  G
)  =  ( c  e.  A  |->  ( R 
gsumg  ( d  e.  {
e  e.  A  | 
e  oR  <_ 
c }  |->  ( ( F `  d ) ( .r `  R
) ( G `  ( c  oF  -  d ) ) ) ) ) ) )
98fveq1d 5690 . . . . . 6  |-  ( ph  ->  ( ( F  .x.  G ) `  x
)  =  ( ( c  e.  A  |->  ( R  gsumg  ( d  e.  {
e  e.  A  | 
e  oR  <_ 
c }  |->  ( ( F `  d ) ( .r `  R
) ( G `  ( c  oF  -  d ) ) ) ) ) ) `
 x ) )
109adantr 462 . . . . 5  |-  ( (
ph  /\  ( x  e.  A  /\  ( J  +  K )  <  ( H `  x
) ) )  -> 
( ( F  .x.  G ) `  x
)  =  ( ( c  e.  A  |->  ( R  gsumg  ( d  e.  {
e  e.  A  | 
e  oR  <_ 
c }  |->  ( ( F `  d ) ( .r `  R
) ( G `  ( c  oF  -  d ) ) ) ) ) ) `
 x ) )
11 breq2 4293 . . . . . . . . . 10  |-  ( c  =  x  ->  (
e  oR  <_ 
c  <->  e  oR  <_  x ) )
1211rabbidv 2962 . . . . . . . . 9  |-  ( c  =  x  ->  { e  e.  A  |  e  oR  <_  c }  =  { e  e.  A  |  e  oR  <_  x }
)
13 oveq1 6097 . . . . . . . . . . 11  |-  ( c  =  x  ->  (
c  oF  -  d )  =  ( x  oF  -  d ) )
1413fveq2d 5692 . . . . . . . . . 10  |-  ( c  =  x  ->  ( G `  ( c  oF  -  d
) )  =  ( G `  ( x  oF  -  d
) ) )
1514oveq2d 6106 . . . . . . . . 9  |-  ( c  =  x  ->  (
( F `  d
) ( .r `  R ) ( G `
 ( c  oF  -  d ) ) )  =  ( ( F `  d
) ( .r `  R ) ( G `
 ( x  oF  -  d ) ) ) )
1612, 15mpteq12dv 4367 . . . . . . . 8  |-  ( c  =  x  ->  (
d  e.  { e  e.  A  |  e  oR  <_  c }  |->  ( ( F `
 d ) ( .r `  R ) ( G `  (
c  oF  -  d ) ) ) )  =  ( d  e.  { e  e.  A  |  e  oR  <_  x }  |->  ( ( F `  d ) ( .r
`  R ) ( G `  ( x  oF  -  d
) ) ) ) )
1716oveq2d 6106 . . . . . . 7  |-  ( c  =  x  ->  ( R  gsumg  ( d  e.  {
e  e.  A  | 
e  oR  <_ 
c }  |->  ( ( F `  d ) ( .r `  R
) ( G `  ( c  oF  -  d ) ) ) ) )  =  ( R  gsumg  ( d  e.  {
e  e.  A  | 
e  oR  <_  x }  |->  ( ( F `  d ) ( .r `  R
) ( G `  ( x  oF  -  d ) ) ) ) ) )
18 eqid 2441 . . . . . . 7  |-  ( c  e.  A  |->  ( R 
gsumg  ( d  e.  {
e  e.  A  | 
e  oR  <_ 
c }  |->  ( ( F `  d ) ( .r `  R
) ( G `  ( c  oF  -  d ) ) ) ) ) )  =  ( c  e.  A  |->  ( R  gsumg  ( d  e.  { e  e.  A  |  e  oR  <_  c }  |->  ( ( F `  d ) ( .r
`  R ) ( G `  ( c  oF  -  d
) ) ) ) ) )
19 ovex 6115 . . . . . . 7  |-  ( R 
gsumg  ( d  e.  {
e  e.  A  | 
e  oR  <_  x }  |->  ( ( F `  d ) ( .r `  R
) ( G `  ( x  oF  -  d ) ) ) ) )  e. 
_V
2017, 18, 19fvmpt 5771 . . . . . 6  |-  ( x  e.  A  ->  (
( c  e.  A  |->  ( R  gsumg  ( d  e.  {
e  e.  A  | 
e  oR  <_ 
c }  |->  ( ( F `  d ) ( .r `  R
) ( G `  ( c  oF  -  d ) ) ) ) ) ) `
 x )  =  ( R  gsumg  ( d  e.  {
e  e.  A  | 
e  oR  <_  x }  |->  ( ( F `  d ) ( .r `  R
) ( G `  ( x  oF  -  d ) ) ) ) ) )
2120ad2antrl 722 . . . . 5  |-  ( (
ph  /\  ( x  e.  A  /\  ( J  +  K )  <  ( H `  x
) ) )  -> 
( ( c  e.  A  |->  ( R  gsumg  ( d  e.  { e  e.  A  |  e  oR  <_  c }  |->  ( ( F `  d ) ( .r
`  R ) ( G `  ( c  oF  -  d
) ) ) ) ) ) `  x
)  =  ( R 
gsumg  ( d  e.  {
e  e.  A  | 
e  oR  <_  x }  |->  ( ( F `  d ) ( .r `  R
) ( G `  ( x  oF  -  d ) ) ) ) ) )
22 mdegaddle.d . . . . . . . . . . . . 13  |-  D  =  ( I mDeg  R )
23 eqid 2441 . . . . . . . . . . . . 13  |-  ( 0g
`  R )  =  ( 0g `  R
)
24 mdegmullem.h . . . . . . . . . . . . 13  |-  H  =  ( b  e.  A  |->  (fld 
gsumg  b ) )
256ad2antrr 720 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  ( d  e. 
{ e  e.  A  |  e  oR 
<_  x }  /\  J  <  ( H `  d
) ) )  ->  F  e.  B )
26 elrabi 3111 . . . . . . . . . . . . . . 15  |-  ( d  e.  { e  e.  A  |  e  oR  <_  x }  ->  d  e.  A )
2726adantl 463 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  d  e.  A )
2827adantrr 711 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  ( d  e. 
{ e  e.  A  |  e  oR 
<_  x }  /\  J  <  ( H `  d
) ) )  -> 
d  e.  A )
2922, 1, 2mdegxrcl 21497 . . . . . . . . . . . . . . . . . 18  |-  ( F  e.  B  ->  ( D `  F )  e.  RR* )
306, 29syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D `  F
)  e.  RR* )
3130ad2antrr 720 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  ( D `  F )  e.  RR* )
32 nn0ssre 10579 . . . . . . . . . . . . . . . . . . 19  |-  NN0  C_  RR
33 ressxr 9423 . . . . . . . . . . . . . . . . . . 19  |-  RR  C_  RR*
3432, 33sstri 3362 . . . . . . . . . . . . . . . . . 18  |-  NN0  C_  RR*
35 mdegmulle2.j1 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  J  e.  NN0 )
3634, 35sseldi 3351 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  J  e.  RR* )
3736ad2antrr 720 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  J  e.  RR* )
38 mdegaddle.i . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  I  e.  V )
395, 24tdeglem1 21486 . . . . . . . . . . . . . . . . . . . 20  |-  ( I  e.  V  ->  H : A --> NN0 )
4038, 39syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  H : A --> NN0 )
4140ad2antrr 720 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  H : A --> NN0 )
4241, 27ffvelrnd 5841 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  ( H `  d )  e.  NN0 )
4334, 42sseldi 3351 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  ( H `  d )  e.  RR* )
4431, 37, 433jca 1163 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  (
( D `  F
)  e.  RR*  /\  J  e.  RR*  /\  ( H `
 d )  e. 
RR* ) )
4544adantrr 711 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  ( d  e. 
{ e  e.  A  |  e  oR 
<_  x }  /\  J  <  ( H `  d
) ) )  -> 
( ( D `  F )  e.  RR*  /\  J  e.  RR*  /\  ( H `  d )  e.  RR* ) )
46 mdegmulle2.j2 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D `  F
)  <_  J )
4746ad2antrr 720 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  ( D `  F )  <_  J )
4847anim1i 565 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  /\  J  <  ( H `  d
) )  ->  (
( D `  F
)  <_  J  /\  J  <  ( H `  d ) ) )
4948anasss 642 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  ( d  e. 
{ e  e.  A  |  e  oR 
<_  x }  /\  J  <  ( H `  d
) ) )  -> 
( ( D `  F )  <_  J  /\  J  <  ( H `
 d ) ) )
50 xrlelttr 11126 . . . . . . . . . . . . . 14  |-  ( ( ( D `  F
)  e.  RR*  /\  J  e.  RR*  /\  ( H `
 d )  e. 
RR* )  ->  (
( ( D `  F )  <_  J  /\  J  <  ( H `
 d ) )  ->  ( D `  F )  <  ( H `  d )
) )
5145, 49, 50sylc 60 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  ( d  e. 
{ e  e.  A  |  e  oR 
<_  x }  /\  J  <  ( H `  d
) ) )  -> 
( D `  F
)  <  ( H `  d ) )
5222, 1, 2, 23, 5, 24, 25, 28, 51mdeglt 21495 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  ( d  e. 
{ e  e.  A  |  e  oR 
<_  x }  /\  J  <  ( H `  d
) ) )  -> 
( F `  d
)  =  ( 0g
`  R ) )
5352oveq1d 6105 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  ( d  e. 
{ e  e.  A  |  e  oR 
<_  x }  /\  J  <  ( H `  d
) ) )  -> 
( ( F `  d ) ( .r
`  R ) ( G `  ( x  oF  -  d
) ) )  =  ( ( 0g `  R ) ( .r
`  R ) ( G `  ( x  oF  -  d
) ) ) )
54 mdegaddle.r . . . . . . . . . . . . . 14  |-  ( ph  ->  R  e.  Ring )
5554ad2antrr 720 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  R  e.  Ring )
56 eqid 2441 . . . . . . . . . . . . . . . 16  |-  ( Base `  R )  =  (
Base `  R )
571, 56, 2, 5, 7mplelf 17487 . . . . . . . . . . . . . . 15  |-  ( ph  ->  G : A --> ( Base `  R ) )
5857ad2antrr 720 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  G : A --> ( Base `  R
) )
59 ssrab2 3434 . . . . . . . . . . . . . . 15  |-  { e  e.  A  |  e  oR  <_  x }  C_  A
6038ad2antrr 720 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  I  e.  V )
61 simplrl 754 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  x  e.  A )
62 simpr 458 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  d  e.  { e  e.  A  |  e  oR 
<_  x } )
63 eqid 2441 . . . . . . . . . . . . . . . . 17  |-  { e  e.  A  |  e  oR  <_  x }  =  { e  e.  A  |  e  oR  <_  x }
645, 63psrbagconcl 17421 . . . . . . . . . . . . . . . 16  |-  ( ( I  e.  V  /\  x  e.  A  /\  d  e.  { e  e.  A  |  e  oR  <_  x }
)  ->  ( x  oF  -  d
)  e.  { e  e.  A  |  e  oR  <_  x } )
6560, 61, 62, 64syl3anc 1213 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  (
x  oF  -  d )  e.  {
e  e.  A  | 
e  oR  <_  x } )
6659, 65sseldi 3351 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  (
x  oF  -  d )  e.  A
)
6758, 66ffvelrnd 5841 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  ( G `  ( x  oF  -  d
) )  e.  (
Base `  R )
)
6856, 3, 23rnglz 16671 . . . . . . . . . . . . 13  |-  ( ( R  e.  Ring  /\  ( G `  ( x  oF  -  d
) )  e.  (
Base `  R )
)  ->  ( ( 0g `  R ) ( .r `  R ) ( G `  (
x  oF  -  d ) ) )  =  ( 0g `  R ) )
6955, 67, 68syl2anc 656 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  (
( 0g `  R
) ( .r `  R ) ( G `
 ( x  oF  -  d ) ) )  =  ( 0g `  R ) )
7069adantrr 711 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  ( d  e. 
{ e  e.  A  |  e  oR 
<_  x }  /\  J  <  ( H `  d
) ) )  -> 
( ( 0g `  R ) ( .r
`  R ) ( G `  ( x  oF  -  d
) ) )  =  ( 0g `  R
) )
7153, 70eqtrd 2473 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  ( d  e. 
{ e  e.  A  |  e  oR 
<_  x }  /\  J  <  ( H `  d
) ) )  -> 
( ( F `  d ) ( .r
`  R ) ( G `  ( x  oF  -  d
) ) )  =  ( 0g `  R
) )
7271anassrs 643 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  /\  J  <  ( H `  d
) )  ->  (
( F `  d
) ( .r `  R ) ( G `
 ( x  oF  -  d ) ) )  =  ( 0g `  R ) )
737ad2antrr 720 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  ( d  e. 
{ e  e.  A  |  e  oR 
<_  x }  /\  K  <  ( H `  (
x  oF  -  d ) ) ) )  ->  G  e.  B )
7466adantrr 711 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  ( d  e. 
{ e  e.  A  |  e  oR 
<_  x }  /\  K  <  ( H `  (
x  oF  -  d ) ) ) )  ->  ( x  oF  -  d
)  e.  A )
7522, 1, 2mdegxrcl 21497 . . . . . . . . . . . . . . . . . 18  |-  ( G  e.  B  ->  ( D `  G )  e.  RR* )
767, 75syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D `  G
)  e.  RR* )
7776ad2antrr 720 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  ( D `  G )  e.  RR* )
78 mdegmulle2.k1 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  K  e.  NN0 )
7934, 78sseldi 3351 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  K  e.  RR* )
8079ad2antrr 720 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  K  e.  RR* )
8141, 66ffvelrnd 5841 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  ( H `  ( x  oF  -  d
) )  e.  NN0 )
8234, 81sseldi 3351 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  ( H `  ( x  oF  -  d
) )  e.  RR* )
8377, 80, 823jca 1163 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  (
( D `  G
)  e.  RR*  /\  K  e.  RR*  /\  ( H `
 ( x  oF  -  d ) )  e.  RR* )
)
8483adantrr 711 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  ( d  e. 
{ e  e.  A  |  e  oR 
<_  x }  /\  K  <  ( H `  (
x  oF  -  d ) ) ) )  ->  ( ( D `  G )  e.  RR*  /\  K  e. 
RR*  /\  ( H `  ( x  oF  -  d ) )  e.  RR* ) )
85 mdegmulle2.k2 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D `  G
)  <_  K )
8685ad2antrr 720 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  ( D `  G )  <_  K )
8786anim1i 565 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  /\  K  <  ( H `  (
x  oF  -  d ) ) )  ->  ( ( D `
 G )  <_  K  /\  K  <  ( H `  ( x  oF  -  d
) ) ) )
8887anasss 642 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  ( d  e. 
{ e  e.  A  |  e  oR 
<_  x }  /\  K  <  ( H `  (
x  oF  -  d ) ) ) )  ->  ( ( D `  G )  <_  K  /\  K  < 
( H `  (
x  oF  -  d ) ) ) )
89 xrlelttr 11126 . . . . . . . . . . . . . 14  |-  ( ( ( D `  G
)  e.  RR*  /\  K  e.  RR*  /\  ( H `
 ( x  oF  -  d ) )  e.  RR* )  ->  ( ( ( D `
 G )  <_  K  /\  K  <  ( H `  ( x  oF  -  d
) ) )  -> 
( D `  G
)  <  ( H `  ( x  oF  -  d ) ) ) )
9084, 88, 89sylc 60 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  ( d  e. 
{ e  e.  A  |  e  oR 
<_  x }  /\  K  <  ( H `  (
x  oF  -  d ) ) ) )  ->  ( D `  G )  <  ( H `  ( x  oF  -  d
) ) )
9122, 1, 2, 23, 5, 24, 73, 74, 90mdeglt 21495 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  ( d  e. 
{ e  e.  A  |  e  oR 
<_  x }  /\  K  <  ( H `  (
x  oF  -  d ) ) ) )  ->  ( G `  ( x  oF  -  d ) )  =  ( 0g `  R ) )
9291oveq2d 6106 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  ( d  e. 
{ e  e.  A  |  e  oR 
<_  x }  /\  K  <  ( H `  (
x  oF  -  d ) ) ) )  ->  ( ( F `  d )
( .r `  R
) ( G `  ( x  oF  -  d ) ) )  =  ( ( F `  d ) ( .r `  R
) ( 0g `  R ) ) )
931, 56, 2, 5, 6mplelf 17487 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F : A --> ( Base `  R ) )
9493ad2antrr 720 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  F : A --> ( Base `  R
) )
9594, 27ffvelrnd 5841 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  ( F `  d )  e.  ( Base `  R
) )
9656, 3, 23rngrz 16672 . . . . . . . . . . . . 13  |-  ( ( R  e.  Ring  /\  ( F `  d )  e.  ( Base `  R
) )  ->  (
( F `  d
) ( .r `  R ) ( 0g
`  R ) )  =  ( 0g `  R ) )
9755, 95, 96syl2anc 656 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  (
( F `  d
) ( .r `  R ) ( 0g
`  R ) )  =  ( 0g `  R ) )
9897adantrr 711 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  ( d  e. 
{ e  e.  A  |  e  oR 
<_  x }  /\  K  <  ( H `  (
x  oF  -  d ) ) ) )  ->  ( ( F `  d )
( .r `  R
) ( 0g `  R ) )  =  ( 0g `  R
) )
9992, 98eqtrd 2473 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  ( d  e. 
{ e  e.  A  |  e  oR 
<_  x }  /\  K  <  ( H `  (
x  oF  -  d ) ) ) )  ->  ( ( F `  d )
( .r `  R
) ( G `  ( x  oF  -  d ) ) )  =  ( 0g
`  R ) )
10099anassrs 643 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  /\  K  <  ( H `  (
x  oF  -  d ) ) )  ->  ( ( F `
 d ) ( .r `  R ) ( G `  (
x  oF  -  d ) ) )  =  ( 0g `  R ) )
101 simplrr 755 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  ( J  +  K )  <  ( H `  x
) )
10242nn0red 10633 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  ( H `  d )  e.  RR )
10381nn0red 10633 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  ( H `  ( x  oF  -  d
) )  e.  RR )
10435ad2antrr 720 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  J  e.  NN0 )
105104nn0red 10633 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  J  e.  RR )
10678ad2antrr 720 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  K  e.  NN0 )
107106nn0red 10633 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  K  e.  RR )
108 le2add 9817 . . . . . . . . . . . . 13  |-  ( ( ( ( H `  d )  e.  RR  /\  ( H `  (
x  oF  -  d ) )  e.  RR )  /\  ( J  e.  RR  /\  K  e.  RR ) )  -> 
( ( ( H `
 d )  <_  J  /\  ( H `  ( x  oF  -  d ) )  <_  K )  -> 
( ( H `  d )  +  ( H `  ( x  oF  -  d
) ) )  <_ 
( J  +  K
) ) )
109102, 103, 105, 107, 108syl22anc 1214 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  (
( ( H `  d )  <_  J  /\  ( H `  (
x  oF  -  d ) )  <_  K )  ->  (
( H `  d
)  +  ( H `
 ( x  oF  -  d ) ) )  <_  ( J  +  K )
) )
1105, 24tdeglem3 21487 . . . . . . . . . . . . . . 15  |-  ( ( I  e.  V  /\  d  e.  A  /\  ( x  oF  -  d )  e.  A )  ->  ( H `  ( d  oF  +  (
x  oF  -  d ) ) )  =  ( ( H `
 d )  +  ( H `  (
x  oF  -  d ) ) ) )
11160, 27, 66, 110syl3anc 1213 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  ( H `  ( d  oF  +  (
x  oF  -  d ) ) )  =  ( ( H `
 d )  +  ( H `  (
x  oF  -  d ) ) ) )
1125psrbagf 17410 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( I  e.  V  /\  d  e.  A )  ->  d : I --> NN0 )
1131123adant3 1003 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( I  e.  V  /\  d  e.  A  /\  x  e.  A )  ->  d : I --> NN0 )
114113ffvelrnda 5840 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( I  e.  V  /\  d  e.  A  /\  x  e.  A
)  /\  b  e.  I )  ->  (
d `  b )  e.  NN0 )
115114nn0cnd 10634 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( I  e.  V  /\  d  e.  A  /\  x  e.  A
)  /\  b  e.  I )  ->  (
d `  b )  e.  CC )
1165psrbagf 17410 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( I  e.  V  /\  x  e.  A )  ->  x : I --> NN0 )
1171163adant2 1002 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( I  e.  V  /\  d  e.  A  /\  x  e.  A )  ->  x : I --> NN0 )
118117ffvelrnda 5840 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( I  e.  V  /\  d  e.  A  /\  x  e.  A
)  /\  b  e.  I )  ->  (
x `  b )  e.  NN0 )
119118nn0cnd 10634 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( I  e.  V  /\  d  e.  A  /\  x  e.  A
)  /\  b  e.  I )  ->  (
x `  b )  e.  CC )
120115, 119pncan3d 9718 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( I  e.  V  /\  d  e.  A  /\  x  e.  A
)  /\  b  e.  I )  ->  (
( d `  b
)  +  ( ( x `  b )  -  ( d `  b ) ) )  =  ( x `  b ) )
121120mpteq2dva 4375 . . . . . . . . . . . . . . . . 17  |-  ( ( I  e.  V  /\  d  e.  A  /\  x  e.  A )  ->  ( b  e.  I  |->  ( ( d `  b )  +  ( ( x `  b
)  -  ( d `
 b ) ) ) )  =  ( b  e.  I  |->  ( x `  b ) ) )
122 simp1 983 . . . . . . . . . . . . . . . . . 18  |-  ( ( I  e.  V  /\  d  e.  A  /\  x  e.  A )  ->  I  e.  V )
123 fvex 5698 . . . . . . . . . . . . . . . . . . 19  |-  ( d `
 b )  e. 
_V
124123a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( I  e.  V  /\  d  e.  A  /\  x  e.  A
)  /\  b  e.  I )  ->  (
d `  b )  e.  _V )
125 ovex 6115 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x `  b )  -  ( d `  b ) )  e. 
_V
126125a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( I  e.  V  /\  d  e.  A  /\  x  e.  A
)  /\  b  e.  I )  ->  (
( x `  b
)  -  ( d `
 b ) )  e.  _V )
127113feqmptd 5741 . . . . . . . . . . . . . . . . . 18  |-  ( ( I  e.  V  /\  d  e.  A  /\  x  e.  A )  ->  d  =  ( b  e.  I  |->  ( d `
 b ) ) )
128 fvex 5698 . . . . . . . . . . . . . . . . . . . 20  |-  ( x `
 b )  e. 
_V
129128a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( I  e.  V  /\  d  e.  A  /\  x  e.  A
)  /\  b  e.  I )  ->  (
x `  b )  e.  _V )
130117feqmptd 5741 . . . . . . . . . . . . . . . . . . 19  |-  ( ( I  e.  V  /\  d  e.  A  /\  x  e.  A )  ->  x  =  ( b  e.  I  |->  ( x `
 b ) ) )
131122, 129, 124, 130, 127offval2 6335 . . . . . . . . . . . . . . . . . 18  |-  ( ( I  e.  V  /\  d  e.  A  /\  x  e.  A )  ->  ( x  oF  -  d )  =  ( b  e.  I  |->  ( ( x `  b )  -  (
d `  b )
) ) )
132122, 124, 126, 127, 131offval2 6335 . . . . . . . . . . . . . . . . 17  |-  ( ( I  e.  V  /\  d  e.  A  /\  x  e.  A )  ->  ( d  oF  +  ( x  oF  -  d ) )  =  ( b  e.  I  |->  ( ( d `  b )  +  ( ( x `
 b )  -  ( d `  b
) ) ) ) )
133121, 132, 1303eqtr4d 2483 . . . . . . . . . . . . . . . 16  |-  ( ( I  e.  V  /\  d  e.  A  /\  x  e.  A )  ->  ( d  oF  +  ( x  oF  -  d ) )  =  x )
13460, 27, 61, 133syl3anc 1213 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  (
d  oF  +  ( x  oF  -  d ) )  =  x )
135134fveq2d 5692 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  ( H `  ( d  oF  +  (
x  oF  -  d ) ) )  =  ( H `  x ) )
136111, 135eqtr3d 2475 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  (
( H `  d
)  +  ( H `
 ( x  oF  -  d ) ) )  =  ( H `  x ) )
137136breq1d 4299 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  (
( ( H `  d )  +  ( H `  ( x  oF  -  d
) ) )  <_ 
( J  +  K
)  <->  ( H `  x )  <_  ( J  +  K )
) )
138109, 137sylibd 214 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  (
( ( H `  d )  <_  J  /\  ( H `  (
x  oF  -  d ) )  <_  K )  ->  ( H `  x )  <_  ( J  +  K
) ) )
139102, 105lenltd 9516 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  (
( H `  d
)  <_  J  <->  -.  J  <  ( H `  d
) ) )
140103, 107lenltd 9516 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  (
( H `  (
x  oF  -  d ) )  <_  K 
<->  -.  K  <  ( H `  ( x  oF  -  d
) ) ) )
141139, 140anbi12d 705 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  (
( ( H `  d )  <_  J  /\  ( H `  (
x  oF  -  d ) )  <_  K )  <->  ( -.  J  <  ( H `  d )  /\  -.  K  <  ( H `  ( x  oF  -  d ) ) ) ) )
142 ioran 487 . . . . . . . . . . . 12  |-  ( -.  ( J  <  ( H `  d )  \/  K  <  ( H `
 ( x  oF  -  d ) ) )  <->  ( -.  J  <  ( H `  d )  /\  -.  K  <  ( H `  ( x  oF  -  d ) ) ) )
143141, 142syl6bbr 263 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  (
( ( H `  d )  <_  J  /\  ( H `  (
x  oF  -  d ) )  <_  K )  <->  -.  ( J  <  ( H `  d )  \/  K  <  ( H `  (
x  oF  -  d ) ) ) ) )
14441, 61ffvelrnd 5841 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  ( H `  x )  e.  NN0 )
145144nn0red 10633 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  ( H `  x )  e.  RR )
14635, 78nn0addcld 10636 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( J  +  K
)  e.  NN0 )
147146ad2antrr 720 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  ( J  +  K )  e.  NN0 )
148147nn0red 10633 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  ( J  +  K )  e.  RR )
149145, 148lenltd 9516 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  (
( H `  x
)  <_  ( J  +  K )  <->  -.  ( J  +  K )  <  ( H `  x
) ) )
150138, 143, 1493imtr3d 267 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  ( -.  ( J  <  ( H `  d )  \/  K  <  ( H `
 ( x  oF  -  d ) ) )  ->  -.  ( J  +  K
)  <  ( H `  x ) ) )
151101, 150mt4d 138 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  ( J  <  ( H `  d )  \/  K  <  ( H `  (
x  oF  -  d ) ) ) )
15272, 100, 151mpjaodan 779 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  A  /\  ( J  +  K
)  <  ( H `  x ) ) )  /\  d  e.  {
e  e.  A  | 
e  oR  <_  x } )  ->  (
( F `  d
) ( .r `  R ) ( G `
 ( x  oF  -  d ) ) )  =  ( 0g `  R ) )
153152mpteq2dva 4375 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  A  /\  ( J  +  K )  <  ( H `  x
) ) )  -> 
( d  e.  {
e  e.  A  | 
e  oR  <_  x }  |->  ( ( F `  d ) ( .r `  R
) ( G `  ( x  oF  -  d ) ) ) )  =  ( d  e.  { e  e.  A  |  e  oR  <_  x }  |->  ( 0g `  R ) ) )
154153oveq2d 6106 . . . . . 6  |-  ( (
ph  /\  ( x  e.  A  /\  ( J  +  K )  <  ( H `  x
) ) )  -> 
( R  gsumg  ( d  e.  {
e  e.  A  | 
e  oR  <_  x }  |->  ( ( F `  d ) ( .r `  R
) ( G `  ( x  oF  -  d ) ) ) ) )  =  ( R  gsumg  ( d  e.  {
e  e.  A  | 
e  oR  <_  x }  |->  ( 0g
`  R ) ) ) )
155 rngmnd 16644 . . . . . . . . 9  |-  ( R  e.  Ring  ->  R  e. 
Mnd )
15654, 155syl 16 . . . . . . . 8  |-  ( ph  ->  R  e.  Mnd )
157156adantr 462 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  A  /\  ( J  +  K )  <  ( H `  x
) ) )  ->  R  e.  Mnd )
158 ovex 6115 . . . . . . . . . 10  |-  ( NN0 
^m  I )  e. 
_V
159158rabex 4440 . . . . . . . . 9  |-  { a  e.  ( NN0  ^m  I )  |  ( `' a " NN )  e.  Fin }  e.  _V
1605, 159eqeltri 2511 . . . . . . . 8  |-  A  e. 
_V
161160rabex 4440 . . . . . . 7  |-  { e  e.  A  |  e  oR  <_  x }  e.  _V
16223gsumz 15504 . . . . . . 7  |-  ( ( R  e.  Mnd  /\  { e  e.  A  | 
e  oR  <_  x }  e.  _V )  ->  ( R  gsumg  ( d  e.  { e  e.  A  |  e  oR  <_  x }  |->  ( 0g `  R
) ) )  =  ( 0g `  R
) )
163157, 161, 162sylancl 657 . . . . . 6  |-  ( (
ph  /\  ( x  e.  A  /\  ( J  +  K )  <  ( H `  x
) ) )  -> 
( R  gsumg  ( d  e.  {
e  e.  A  | 
e  oR  <_  x }  |->  ( 0g
`  R ) ) )  =  ( 0g
`  R ) )
164154, 163eqtrd 2473 . . . . 5  |-  ( (
ph  /\  ( x  e.  A  /\  ( J  +  K )  <  ( H `  x
) ) )  -> 
( R  gsumg  ( d  e.  {
e  e.  A  | 
e  oR  <_  x }  |->  ( ( F `  d ) ( .r `  R
) ( G `  ( x  oF  -  d ) ) ) ) )  =  ( 0g `  R
) )
16510, 21, 1643eqtrd 2477 . . . 4  |-  ( (
ph  /\  ( x  e.  A  /\  ( J  +  K )  <  ( H `  x
) ) )  -> 
( ( F  .x.  G ) `  x
)  =  ( 0g
`  R ) )
166165expr 612 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  (
( J  +  K
)  <  ( H `  x )  ->  (
( F  .x.  G
) `  x )  =  ( 0g `  R ) ) )
167166ralrimiva 2797 . 2  |-  ( ph  ->  A. x  e.  A  ( ( J  +  K )  <  ( H `  x )  ->  ( ( F  .x.  G ) `  x
)  =  ( 0g
`  R ) ) )
1681mplrng 17509 . . . . 5  |-  ( ( I  e.  V  /\  R  e.  Ring )  ->  Y  e.  Ring )
16938, 54, 168syl2anc 656 . . . 4  |-  ( ph  ->  Y  e.  Ring )
1702, 4rngcl 16648 . . . 4  |-  ( ( Y  e.  Ring  /\  F  e.  B  /\  G  e.  B )  ->  ( F  .x.  G )  e.  B )
171169, 6, 7, 170syl3anc 1213 . . 3  |-  ( ph  ->  ( F  .x.  G
)  e.  B )
17234, 146sseldi 3351 . . 3  |-  ( ph  ->  ( J  +  K
)  e.  RR* )
17322, 1, 2, 23, 5, 24mdegleb 21494 . . 3  |-  ( ( ( F  .x.  G
)  e.  B  /\  ( J  +  K
)  e.  RR* )  ->  ( ( D `  ( F  .x.  G ) )  <_  ( J  +  K )  <->  A. x  e.  A  ( ( J  +  K )  <  ( H `  x
)  ->  ( ( F  .x.  G ) `  x )  =  ( 0g `  R ) ) ) )
174171, 172, 173syl2anc 656 . 2  |-  ( ph  ->  ( ( D `  ( F  .x.  G ) )  <_  ( J  +  K )  <->  A. x  e.  A  ( ( J  +  K )  <  ( H `  x
)  ->  ( ( F  .x.  G ) `  x )  =  ( 0g `  R ) ) ) )
175167, 174mpbird 232 1  |-  ( ph  ->  ( D `  ( F  .x.  G ) )  <_  ( J  +  K ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    /\ w3a 960    = wceq 1364    e. wcel 1761   A.wral 2713   {crab 2717   _Vcvv 2970   class class class wbr 4289    e. cmpt 4347   `'ccnv 4835   "cima 4839   -->wf 5411   ` cfv 5415  (class class class)co 6090    oFcof 6317    oRcofr 6318    ^m cmap 7210   Fincfn 7306   RRcr 9277    + caddc 9281   RR*cxr 9413    < clt 9414    <_ cle 9415    - cmin 9591   NNcn 10318   NN0cn0 10575   Basecbs 14170   .rcmulr 14235   0gc0g 14374    gsumg cgsu 14375   Mndcmnd 15405   Ringcrg 16635   mPoly cmpl 17398  ℂfldccnfld 17777   mDeg cmdg 21481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-inf2 7843  ax-cnex 9334  ax-resscn 9335  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-addrcl 9339  ax-mulcl 9340  ax-mulrcl 9341  ax-mulcom 9342  ax-addass 9343  ax-mulass 9344  ax-distr 9345  ax-i2m1 9346  ax-1ne0 9347  ax-1rid 9348  ax-rnegex 9349  ax-rrecex 9350  ax-cnre 9351  ax-pre-lttri 9352  ax-pre-lttrn 9353  ax-pre-ltadd 9354  ax-pre-mulgt0 9355  ax-pre-sup 9356  ax-addf 9357  ax-mulf 9358
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-reu 2720  df-rmo 2721  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-int 4126  df-iun 4170  df-iin 4171  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-se 4676  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-isom 5424  df-riota 6049  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-of 6319  df-ofr 6320  df-om 6476  df-1st 6576  df-2nd 6577  df-supp 6690  df-recs 6828  df-rdg 6862  df-1o 6916  df-2o 6917  df-oadd 6920  df-er 7097  df-map 7212  df-pm 7213  df-ixp 7260  df-en 7307  df-dom 7308  df-sdom 7309  df-fin 7310  df-fsupp 7617  df-sup 7687  df-oi 7720  df-card 8105  df-pnf 9416  df-mnf 9417  df-xr 9418  df-ltxr 9419  df-le 9420  df-sub 9593  df-neg 9594  df-nn 10319  df-2 10376  df-3 10377  df-4 10378  df-5 10379  df-6 10380  df-7 10381  df-8 10382  df-9 10383  df-10 10384  df-n0 10576  df-z 10643  df-dec 10752  df-uz 10858  df-fz 11434  df-fzo 11545  df-seq 11803  df-hash 12100  df-struct 14172  df-ndx 14173  df-slot 14174  df-base 14175  df-sets 14176  df-ress 14177  df-plusg 14247  df-mulr 14248  df-starv 14249  df-sca 14250  df-vsca 14251  df-tset 14253  df-ple 14254  df-ds 14256  df-unif 14257  df-0g 14376  df-gsum 14377  df-mre 14520  df-mrc 14521  df-acs 14523  df-mnd 15411  df-mhm 15460  df-submnd 15461  df-grp 15538  df-minusg 15539  df-mulg 15541  df-subg 15671  df-ghm 15738  df-cntz 15828  df-cmn 16272  df-abl 16273  df-mgp 16582  df-ur 16594  df-rng 16637  df-cring 16638  df-subrg 16843  df-psr 17401  df-mpl 17403  df-cnfld 17778  df-mdeg 21483
This theorem is referenced by:  mdegmulle2  21509
  Copyright terms: Public domain W3C validator