Metamath Proof Explorer

Theorem mdegmullem

Description: Lemma for mdegmulle2 . (Contributed by Stefan O'Rear, 26-Mar-2015)

Ref Expression
Hypotheses 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 |-> ( CCfld gsum b ) )
Assertion mdegmullem 
|- ( ph -> ( D ` ( F .x. G ) ) <_ ( J + K ) )

Proof

Step Hyp Ref Expression
1 mdegaddle.y 
 |-  Y = ( I mPoly R )
2 mdegaddle.d 
 |-  D = ( I mDeg R )
3 mdegaddle.i 
 |-  ( ph -> I e. V )
4 mdegaddle.r 
 |-  ( ph -> R e. Ring )
5 mdegmulle2.b 
 |-  B = ( Base ` Y )
6 mdegmulle2.t 
 |-  .x. = ( .r ` Y )
7 mdegmulle2.f 
 |-  ( ph -> F e. B )
8 mdegmulle2.g 
 |-  ( ph -> G e. B )
9 mdegmulle2.j1 
 |-  ( ph -> J e. NN0 )
10 mdegmulle2.k1 
 |-  ( ph -> K e. NN0 )
11 mdegmulle2.j2 
 |-  ( ph -> ( D ` F ) <_ J )
12 mdegmulle2.k2 
 |-  ( ph -> ( D ` G ) <_ K )
13 mdegmullem.a 
 |-  A = { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin }
14 mdegmullem.h 
 |-  H = ( b e. A |-> ( CCfld gsum b ) )
15 eqid 
 |-  ( .r ` R ) = ( .r ` R )
16 1 5 15 6 13 7 8 mplmul 
 |-  ( ph -> ( F .x. G ) = ( c e. A |-> ( R gsum ( d e. { e e. A | e oR <_ c } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( c oF - d ) ) ) ) ) ) )
17 16 fveq1d 
 |-  ( ph -> ( ( F .x. G ) ` x ) = ( ( c e. A |-> ( R gsum ( d e. { e e. A | e oR <_ c } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( c oF - d ) ) ) ) ) ) ` x ) )
18 17 adantr 
 |-  ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) -> ( ( F .x. G ) ` x ) = ( ( c e. A |-> ( R gsum ( d e. { e e. A | e oR <_ c } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( c oF - d ) ) ) ) ) ) ` x ) )
19 breq2 
 |-  ( c = x -> ( e oR <_ c <-> e oR <_ x ) )
20 19 rabbidv 
 |-  ( c = x -> { e e. A | e oR <_ c } = { e e. A | e oR <_ x } )
21 fvoveq1 
 |-  ( c = x -> ( G ` ( c oF - d ) ) = ( G ` ( x oF - d ) ) )
22 21 oveq2d 
 |-  ( c = x -> ( ( F ` d ) ( .r ` R ) ( G ` ( c oF - d ) ) ) = ( ( F ` d ) ( .r ` R ) ( G ` ( x oF - d ) ) ) )
23 20 22 mpteq12dv 
 |-  ( 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 ) ) ) ) )
24 23 oveq2d 
 |-  ( c = x -> ( R gsum ( d e. { e e. A | e oR <_ c } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( c oF - d ) ) ) ) ) = ( R gsum ( d e. { e e. A | e oR <_ x } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( x oF - d ) ) ) ) ) )
25 eqid 
 |-  ( c e. A |-> ( R gsum ( d e. { e e. A | e oR <_ c } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( c oF - d ) ) ) ) ) ) = ( c e. A |-> ( R gsum ( d e. { e e. A | e oR <_ c } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( c oF - d ) ) ) ) ) )
26 ovex 
 |-  ( R gsum ( d e. { e e. A | e oR <_ x } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( x oF - d ) ) ) ) ) e. _V
27 24 25 26 fvmpt 
 |-  ( x e. A -> ( ( c e. A |-> ( R gsum ( d e. { e e. A | e oR <_ c } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( c oF - d ) ) ) ) ) ) ` x ) = ( R gsum ( d e. { e e. A | e oR <_ x } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( x oF - d ) ) ) ) ) )
28 27 ad2antrl 
 |-  ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) -> ( ( c e. A |-> ( R gsum ( d e. { e e. A | e oR <_ c } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( c oF - d ) ) ) ) ) ) ` x ) = ( R gsum ( d e. { e e. A | e oR <_ x } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( x oF - d ) ) ) ) ) )
29 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
30 7 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ ( d e. { e e. A | e oR <_ x } /\ J < ( H ` d ) ) ) -> F e. B )
31 elrabi 
 |-  ( d e. { e e. A | e oR <_ x } -> d e. A )
32 31 adantl 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> d e. A )
33 32 adantrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ ( d e. { e e. A | e oR <_ x } /\ J < ( H ` d ) ) ) -> d e. A )
34 2 1 5 mdegxrcl 
 |-  ( F e. B -> ( D ` F ) e. RR* )
35 7 34 syl 
 |-  ( ph -> ( D ` F ) e. RR* )
36 35 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( D ` F ) e. RR* )
37 nn0ssre 
 |-  NN0 C_ RR
38 ressxr 
 |-  RR C_ RR*
39 37 38 sstri 
 |-  NN0 C_ RR*
40 39 9 sseldi 
 |-  ( ph -> J e. RR* )
41 40 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> J e. RR* )
42 13 14 tdeglem1 
 |-  ( I e. V -> H : A --> NN0 )
43 3 42 syl 
 |-  ( ph -> H : A --> NN0 )
44 43 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> H : A --> NN0 )
45 44 32 ffvelrnd 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( H ` d ) e. NN0 )
46 39 45 sseldi 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( H ` d ) e. RR* )
47 36 41 46 3jca 
 |-  ( ( ( 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* ) )
48 47 adantrr 
 |-  ( ( ( 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* ) )
49 11 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( D ` F ) <_ J )
50 49 anim1i 
 |-  ( ( ( ( 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 ) ) )
51 50 anasss 
 |-  ( ( ( 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 ) ) )
52 xrlelttr 
 |-  ( ( ( D ` F ) e. RR* /\ J e. RR* /\ ( H ` d ) e. RR* ) -> ( ( ( D ` F ) <_ J /\ J < ( H ` d ) ) -> ( D ` F ) < ( H ` d ) ) )
53 48 51 52 sylc 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ ( d e. { e e. A | e oR <_ x } /\ J < ( H ` d ) ) ) -> ( D ` F ) < ( H ` d ) )
54 2 1 5 29 13 14 30 33 53 mdeglt 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ ( d e. { e e. A | e oR <_ x } /\ J < ( H ` d ) ) ) -> ( F ` d ) = ( 0g ` R ) )
55 54 oveq1d 
 |-  ( ( ( 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 ) ) ) )
56 4 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> R e. Ring )
57 eqid 
 |-  ( Base ` R ) = ( Base ` R )
58 1 57 5 13 8 mplelf 
 |-  ( ph -> G : A --> ( Base ` R ) )
59 58 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> G : A --> ( Base ` R ) )
60 ssrab2 
 |-  { e e. A | e oR <_ x } C_ A
61 3 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> I e. V )
62 simplrl 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> x e. A )
63 simpr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> d e. { e e. A | e oR <_ x } )
64 eqid 
 |-  { e e. A | e oR <_ x } = { e e. A | e oR <_ x }
65 13 64 psrbagconcl 
 |-  ( ( I e. V /\ x e. A /\ d e. { e e. A | e oR <_ x } ) -> ( x oF - d ) e. { e e. A | e oR <_ x } )
66 61 62 63 65 syl3anc 
 |-  ( ( ( 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 } )
67 60 66 sseldi 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( x oF - d ) e. A )
68 59 67 ffvelrnd 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( G ` ( x oF - d ) ) e. ( Base ` R ) )
69 57 15 29 ringlz 
 |-  ( ( R e. Ring /\ ( G ` ( x oF - d ) ) e. ( Base ` R ) ) -> ( ( 0g ` R ) ( .r ` R ) ( G ` ( x oF - d ) ) ) = ( 0g ` R ) )
70 56 68 69 syl2anc 
 |-  ( ( ( 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 ) )
71 70 adantrr 
 |-  ( ( ( 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 ) )
72 55 71 eqtrd 
 |-  ( ( ( 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 ) )
73 72 anassrs 
 |-  ( ( ( ( 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 ) )
74 8 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ ( d e. { e e. A | e oR <_ x } /\ K < ( H ` ( x oF - d ) ) ) ) -> G e. B )
75 67 adantrr 
 |-  ( ( ( 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 )
76 2 1 5 mdegxrcl 
 |-  ( G e. B -> ( D ` G ) e. RR* )
77 8 76 syl 
 |-  ( ph -> ( D ` G ) e. RR* )
78 77 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( D ` G ) e. RR* )
79 39 10 sseldi 
 |-  ( ph -> K e. RR* )
80 79 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> K e. RR* )
81 44 67 ffvelrnd 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( H ` ( x oF - d ) ) e. NN0 )
82 39 81 sseldi 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( H ` ( x oF - d ) ) e. RR* )
83 78 80 82 3jca 
 |-  ( ( ( 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* ) )
84 83 adantrr 
 |-  ( ( ( 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 12 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( D ` G ) <_ K )
86 85 anim1i 
 |-  ( ( ( ( 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 ) ) ) )
87 86 anasss 
 |-  ( ( ( 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 ) ) ) )
88 xrlelttr 
 |-  ( ( ( 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 ) ) ) )
89 84 87 88 sylc 
 |-  ( ( ( 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 ) ) )
90 2 1 5 29 13 14 74 75 89 mdeglt 
 |-  ( ( ( 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 ) )
91 90 oveq2d 
 |-  ( ( ( 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 ) ) )
92 1 57 5 13 7 mplelf 
 |-  ( ph -> F : A --> ( Base ` R ) )
93 92 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> F : A --> ( Base ` R ) )
94 93 32 ffvelrnd 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( F ` d ) e. ( Base ` R ) )
95 57 15 29 ringrz 
 |-  ( ( R e. Ring /\ ( F ` d ) e. ( Base ` R ) ) -> ( ( F ` d ) ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
96 56 94 95 syl2anc 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( ( F ` d ) ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
97 96 adantrr 
 |-  ( ( ( 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 ) )
98 91 97 eqtrd 
 |-  ( ( ( 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 ) )
99 98 anassrs 
 |-  ( ( ( ( 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 ) )
100 simplrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( J + K ) < ( H ` x ) )
101 45 nn0red 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( H ` d ) e. RR )
102 81 nn0red 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( H ` ( x oF - d ) ) e. RR )
103 9 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> J e. NN0 )
104 103 nn0red 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> J e. RR )
105 10 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> K e. NN0 )
106 105 nn0red 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> K e. RR )
107 le2add 
 |-  ( ( ( ( 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 ) ) )
108 101 102 104 106 107 syl22anc 
 |-  ( ( ( 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 ) ) )
109 13 14 tdeglem3 
 |-  ( ( I e. V /\ d e. A /\ ( x oF - d ) e. A ) -> ( H ` ( d oF + ( x oF - d ) ) ) = ( ( H ` d ) + ( H ` ( x oF - d ) ) ) )
110 61 32 67 109 syl3anc 
 |-  ( ( ( 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 ) ) ) )
111 13 psrbagf 
 |-  ( ( I e. V /\ d e. A ) -> d : I --> NN0 )
112 111 3adant3 
 |-  ( ( I e. V /\ d e. A /\ x e. A ) -> d : I --> NN0 )
113 112 ffvelrnda 
 |-  ( ( ( I e. V /\ d e. A /\ x e. A ) /\ b e. I ) -> ( d ` b ) e. NN0 )
114 113 nn0cnd 
 |-  ( ( ( I e. V /\ d e. A /\ x e. A ) /\ b e. I ) -> ( d ` b ) e. CC )
115 13 psrbagf 
 |-  ( ( I e. V /\ x e. A ) -> x : I --> NN0 )
116 115 3adant2 
 |-  ( ( I e. V /\ d e. A /\ x e. A ) -> x : I --> NN0 )
117 116 ffvelrnda 
 |-  ( ( ( I e. V /\ d e. A /\ x e. A ) /\ b e. I ) -> ( x ` b ) e. NN0 )
118 117 nn0cnd 
 |-  ( ( ( I e. V /\ d e. A /\ x e. A ) /\ b e. I ) -> ( x ` b ) e. CC )
119 114 118 pncan3d 
 |-  ( ( ( I e. V /\ d e. A /\ x e. A ) /\ b e. I ) -> ( ( d ` b ) + ( ( x ` b ) - ( d ` b ) ) ) = ( x ` b ) )
120 119 mpteq2dva 
 |-  ( ( I e. V /\ d e. A /\ x e. A ) -> ( b e. I |-> ( ( d ` b ) + ( ( x ` b ) - ( d ` b ) ) ) ) = ( b e. I |-> ( x ` b ) ) )
121 simp1 
 |-  ( ( I e. V /\ d e. A /\ x e. A ) -> I e. V )
122 fvexd 
 |-  ( ( ( I e. V /\ d e. A /\ x e. A ) /\ b e. I ) -> ( d ` b ) e. _V )
123 ovexd 
 |-  ( ( ( I e. V /\ d e. A /\ x e. A ) /\ b e. I ) -> ( ( x ` b ) - ( d ` b ) ) e. _V )
124 112 feqmptd 
 |-  ( ( I e. V /\ d e. A /\ x e. A ) -> d = ( b e. I |-> ( d ` b ) ) )
125 fvexd 
 |-  ( ( ( I e. V /\ d e. A /\ x e. A ) /\ b e. I ) -> ( x ` b ) e. _V )
126 116 feqmptd 
 |-  ( ( I e. V /\ d e. A /\ x e. A ) -> x = ( b e. I |-> ( x ` b ) ) )
127 121 125 122 126 124 offval2 
 |-  ( ( I e. V /\ d e. A /\ x e. A ) -> ( x oF - d ) = ( b e. I |-> ( ( x ` b ) - ( d ` b ) ) ) )
128 121 122 123 124 127 offval2 
 |-  ( ( I e. V /\ d e. A /\ x e. A ) -> ( d oF + ( x oF - d ) ) = ( b e. I |-> ( ( d ` b ) + ( ( x ` b ) - ( d ` b ) ) ) ) )
129 120 128 126 3eqtr4d 
 |-  ( ( I e. V /\ d e. A /\ x e. A ) -> ( d oF + ( x oF - d ) ) = x )
130 61 32 62 129 syl3anc 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( d oF + ( x oF - d ) ) = x )
131 130 fveq2d 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( H ` ( d oF + ( x oF - d ) ) ) = ( H ` x ) )
132 110 131 eqtr3d 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( ( H ` d ) + ( H ` ( x oF - d ) ) ) = ( H ` x ) )
133 132 breq1d 
 |-  ( ( ( 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 ) ) )
134 108 133 sylibd 
 |-  ( ( ( 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 ) ) )
135 101 104 lenltd 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( ( H ` d ) <_ J <-> -. J < ( H ` d ) ) )
136 102 106 lenltd 
 |-  ( ( ( 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 ) ) ) )
137 135 136 anbi12d 
 |-  ( ( ( 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 ) ) ) ) )
138 ioran 
 |-  ( -. ( J < ( H ` d ) \/ K < ( H ` ( x oF - d ) ) ) <-> ( -. J < ( H ` d ) /\ -. K < ( H ` ( x oF - d ) ) ) )
139 137 138 syl6bbr 
 |-  ( ( ( 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 ) ) ) ) )
140 44 62 ffvelrnd 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( H ` x ) e. NN0 )
141 140 nn0red 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( H ` x ) e. RR )
142 9 10 nn0addcld 
 |-  ( ph -> ( J + K ) e. NN0 )
143 142 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( J + K ) e. NN0 )
144 143 nn0red 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( J + K ) e. RR )
145 141 144 lenltd 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( ( H ` x ) <_ ( J + K ) <-> -. ( J + K ) < ( H ` x ) ) )
146 134 139 145 3imtr3d 
 |-  ( ( ( 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 ) ) )
147 100 146 mt4d 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( J < ( H ` d ) \/ K < ( H ` ( x oF - d ) ) ) )
148 73 99 147 mpjaodan 
 |-  ( ( ( 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 ) )
149 148 mpteq2dva 
 |-  ( ( 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 ) ) )
150 149 oveq2d 
 |-  ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) -> ( R gsum ( d e. { e e. A | e oR <_ x } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( x oF - d ) ) ) ) ) = ( R gsum ( d e. { e e. A | e oR <_ x } |-> ( 0g ` R ) ) ) )
151 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
152 4 151 syl 
 |-  ( ph -> R e. Mnd )
153 152 adantr 
 |-  ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) -> R e. Mnd )
154 ovex 
 |-  ( NN0 ^m I ) e. _V
155 13 154 rab2ex 
 |-  { e e. A | e oR <_ x } e. _V
156 29 gsumz 
 |-  ( ( R e. Mnd /\ { e e. A | e oR <_ x } e. _V ) -> ( R gsum ( d e. { e e. A | e oR <_ x } |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
157 153 155 156 sylancl 
 |-  ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) -> ( R gsum ( d e. { e e. A | e oR <_ x } |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
158 150 157 eqtrd 
 |-  ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) -> ( R gsum ( d e. { e e. A | e oR <_ x } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( x oF - d ) ) ) ) ) = ( 0g ` R ) )
159 18 28 158 3eqtrd 
 |-  ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) -> ( ( F .x. G ) ` x ) = ( 0g ` R ) )
160 159 expr 
 |-  ( ( ph /\ x e. A ) -> ( ( J + K ) < ( H ` x ) -> ( ( F .x. G ) ` x ) = ( 0g ` R ) ) )
161 160 ralrimiva 
 |-  ( ph -> A. x e. A ( ( J + K ) < ( H ` x ) -> ( ( F .x. G ) ` x ) = ( 0g ` R ) ) )
162 1 mplring 
 |-  ( ( I e. V /\ R e. Ring ) -> Y e. Ring )
163 3 4 162 syl2anc 
 |-  ( ph -> Y e. Ring )
164 5 6 ringcl 
 |-  ( ( Y e. Ring /\ F e. B /\ G e. B ) -> ( F .x. G ) e. B )
165 163 7 8 164 syl3anc 
 |-  ( ph -> ( F .x. G ) e. B )
166 39 142 sseldi 
 |-  ( ph -> ( J + K ) e. RR* )
167 2 1 5 29 13 14 mdegleb 
 |-  ( ( ( 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 ) ) ) )
168 165 166 167 syl2anc 
 |-  ( ph -> ( ( D ` ( F .x. G ) ) <_ ( J + K ) <-> A. x e. A ( ( J + K ) < ( H ` x ) -> ( ( F .x. G ) ` x ) = ( 0g ` R ) ) ) )
169 161 168 mpbird 
 |-  ( ph -> ( D ` ( F .x. G ) ) <_ ( J + K ) )