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 sselid 
 |-  ( 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 
 |-  H : A --> NN0
43 42 a1i 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> H : A --> NN0 )
44 43 32 ffvelrnd 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( H ` d ) e. NN0 )
45 39 44 sselid 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( H ` d ) e. RR* )
46 36 41 45 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* ) )
47 46 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* ) )
48 11 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( D ` F ) <_ J )
49 48 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 ) ) )
50 49 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 ) ) )
51 xrlelttr 
 |-  ( ( ( D ` F ) e. RR* /\ J e. RR* /\ ( H ` d ) e. RR* ) -> ( ( ( D ` F ) <_ J /\ J < ( H ` d ) ) -> ( D ` F ) < ( H ` d ) ) )
52 47 50 51 sylc 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ ( d e. { e e. A | e oR <_ x } /\ J < ( H ` d ) ) ) -> ( D ` F ) < ( H ` d ) )
53 2 1 5 29 13 14 30 33 52 mdeglt 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ ( d e. { e e. A | e oR <_ x } /\ J < ( H ` d ) ) ) -> ( F ` d ) = ( 0g ` R ) )
54 53 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 ) ) ) )
55 4 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> R e. Ring )
56 eqid 
 |-  ( Base ` R ) = ( Base ` R )
57 1 56 5 13 8 mplelf 
 |-  ( ph -> G : A --> ( Base ` R ) )
58 57 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> G : A --> ( Base ` R ) )
59 ssrab2 
 |-  { e e. A | e oR <_ x } C_ A
60 simplrl 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> x e. A )
61 eqid 
 |-  { e e. A | e oR <_ x } = { e e. A | e oR <_ x }
62 13 61 psrbagconcl 
 |-  ( ( x e. A /\ d e. { e e. A | e oR <_ x } ) -> ( x oF - d ) e. { e e. A | e oR <_ x } )
63 60 62 sylancom 
 |-  ( ( ( 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 } )
64 59 63 sselid 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( x oF - d ) e. A )
65 58 64 ffvelrnd 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( G ` ( x oF - d ) ) e. ( Base ` R ) )
66 56 15 29 ringlz 
 |-  ( ( R e. Ring /\ ( G ` ( x oF - d ) ) e. ( Base ` R ) ) -> ( ( 0g ` R ) ( .r ` R ) ( G ` ( x oF - d ) ) ) = ( 0g ` R ) )
67 55 65 66 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 ) )
68 67 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 ) )
69 54 68 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 ) )
70 69 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 ) )
71 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 )
72 64 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 )
73 2 1 5 mdegxrcl 
 |-  ( G e. B -> ( D ` G ) e. RR* )
74 8 73 syl 
 |-  ( ph -> ( D ` G ) e. RR* )
75 74 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( D ` G ) e. RR* )
76 39 10 sselid 
 |-  ( ph -> K e. RR* )
77 76 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> K e. RR* )
78 43 64 ffvelrnd 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( H ` ( x oF - d ) ) e. NN0 )
79 39 78 sselid 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( H ` ( x oF - d ) ) e. RR* )
80 75 77 79 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* ) )
81 80 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* ) )
82 12 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( D ` G ) <_ K )
83 82 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 ) ) ) )
84 83 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 ) ) ) )
85 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 ) ) ) )
86 81 84 85 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 ) ) )
87 2 1 5 29 13 14 71 72 86 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 ) )
88 87 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 ) ) )
89 1 56 5 13 7 mplelf 
 |-  ( ph -> F : A --> ( Base ` R ) )
90 89 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> F : A --> ( Base ` R ) )
91 90 32 ffvelrnd 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( F ` d ) e. ( Base ` R ) )
92 56 15 29 ringrz 
 |-  ( ( R e. Ring /\ ( F ` d ) e. ( Base ` R ) ) -> ( ( F ` d ) ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
93 55 91 92 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 ) )
94 93 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 ) )
95 88 94 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 ) )
96 95 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 ) )
97 simplrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( J + K ) < ( H ` x ) )
98 44 nn0red 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( H ` d ) e. RR )
99 78 nn0red 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( H ` ( x oF - d ) ) e. RR )
100 9 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> J e. NN0 )
101 100 nn0red 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> J e. RR )
102 10 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> K e. NN0 )
103 102 nn0red 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> K e. RR )
104 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 ) ) )
105 98 99 101 103 104 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 ) ) )
106 13 14 tdeglem3 
 |-  ( ( d e. A /\ ( x oF - d ) e. A ) -> ( H ` ( d oF + ( x oF - d ) ) ) = ( ( H ` d ) + ( H ` ( x oF - d ) ) ) )
107 32 64 106 syl2anc 
 |-  ( ( ( 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 ) ) ) )
108 3 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> I e. V )
109 13 psrbagf 
 |-  ( d e. A -> d : I --> NN0 )
110 109 3ad2ant2 
 |-  ( ( I e. V /\ d e. A /\ x e. A ) -> d : I --> NN0 )
111 110 ffvelrnda 
 |-  ( ( ( I e. V /\ d e. A /\ x e. A ) /\ b e. I ) -> ( d ` b ) e. NN0 )
112 111 nn0cnd 
 |-  ( ( ( I e. V /\ d e. A /\ x e. A ) /\ b e. I ) -> ( d ` b ) e. CC )
113 13 psrbagf 
 |-  ( x e. A -> x : I --> NN0 )
114 113 3ad2ant3 
 |-  ( ( I e. V /\ d e. A /\ x e. A ) -> x : I --> NN0 )
115 114 ffvelrnda 
 |-  ( ( ( I e. V /\ d e. A /\ x e. A ) /\ b e. I ) -> ( x ` b ) e. NN0 )
116 115 nn0cnd 
 |-  ( ( ( I e. V /\ d e. A /\ x e. A ) /\ b e. I ) -> ( x ` b ) e. CC )
117 112 116 pncan3d 
 |-  ( ( ( I e. V /\ d e. A /\ x e. A ) /\ b e. I ) -> ( ( d ` b ) + ( ( x ` b ) - ( d ` b ) ) ) = ( x ` b ) )
118 117 mpteq2dva 
 |-  ( ( I e. V /\ d e. A /\ x e. A ) -> ( b e. I |-> ( ( d ` b ) + ( ( x ` b ) - ( d ` b ) ) ) ) = ( b e. I |-> ( x ` b ) ) )
119 simp1 
 |-  ( ( I e. V /\ d e. A /\ x e. A ) -> I e. V )
120 fvexd 
 |-  ( ( ( I e. V /\ d e. A /\ x e. A ) /\ b e. I ) -> ( d ` b ) e. _V )
121 ovexd 
 |-  ( ( ( I e. V /\ d e. A /\ x e. A ) /\ b e. I ) -> ( ( x ` b ) - ( d ` b ) ) e. _V )
122 110 feqmptd 
 |-  ( ( I e. V /\ d e. A /\ x e. A ) -> d = ( b e. I |-> ( d ` b ) ) )
123 fvexd 
 |-  ( ( ( I e. V /\ d e. A /\ x e. A ) /\ b e. I ) -> ( x ` b ) e. _V )
124 114 feqmptd 
 |-  ( ( I e. V /\ d e. A /\ x e. A ) -> x = ( b e. I |-> ( x ` b ) ) )
125 119 123 120 124 122 offval2 
 |-  ( ( I e. V /\ d e. A /\ x e. A ) -> ( x oF - d ) = ( b e. I |-> ( ( x ` b ) - ( d ` b ) ) ) )
126 119 120 121 122 125 offval2 
 |-  ( ( I e. V /\ d e. A /\ x e. A ) -> ( d oF + ( x oF - d ) ) = ( b e. I |-> ( ( d ` b ) + ( ( x ` b ) - ( d ` b ) ) ) ) )
127 118 126 124 3eqtr4d 
 |-  ( ( I e. V /\ d e. A /\ x e. A ) -> ( d oF + ( x oF - d ) ) = x )
128 108 32 60 127 syl3anc 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( d oF + ( x oF - d ) ) = x )
129 128 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 ) )
130 107 129 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 ) )
131 130 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 ) ) )
132 105 131 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 ) ) )
133 98 101 lenltd 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( ( H ` d ) <_ J <-> -. J < ( H ` d ) ) )
134 99 103 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 ) ) ) )
135 133 134 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 ) ) ) ) )
136 ioran 
 |-  ( -. ( J < ( H ` d ) \/ K < ( H ` ( x oF - d ) ) ) <-> ( -. J < ( H ` d ) /\ -. K < ( H ` ( x oF - d ) ) ) )
137 135 136 bitr4di 
 |-  ( ( ( 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 43 60 ffvelrnd 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( H ` x ) e. NN0 )
139 138 nn0red 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( H ` x ) e. RR )
140 9 10 nn0addcld 
 |-  ( ph -> ( J + K ) e. NN0 )
141 140 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( J + K ) e. NN0 )
142 141 nn0red 
 |-  ( ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) /\ d e. { e e. A | e oR <_ x } ) -> ( J + K ) e. RR )
143 139 142 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 ) ) )
144 132 137 143 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 ) ) )
145 97 144 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 ) ) ) )
146 70 96 145 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 ) )
147 146 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 ) ) )
148 147 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 ) ) ) )
149 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
150 4 149 syl 
 |-  ( ph -> R e. Mnd )
151 150 adantr 
 |-  ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) -> R e. Mnd )
152 ovex 
 |-  ( NN0 ^m I ) e. _V
153 13 152 rab2ex 
 |-  { e e. A | e oR <_ x } e. _V
154 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 ) )
155 151 153 154 sylancl 
 |-  ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) -> ( R gsum ( d e. { e e. A | e oR <_ x } |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
156 148 155 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 ) )
157 18 28 156 3eqtrd 
 |-  ( ( ph /\ ( x e. A /\ ( J + K ) < ( H ` x ) ) ) -> ( ( F .x. G ) ` x ) = ( 0g ` R ) )
158 157 expr 
 |-  ( ( ph /\ x e. A ) -> ( ( J + K ) < ( H ` x ) -> ( ( F .x. G ) ` x ) = ( 0g ` R ) ) )
159 158 ralrimiva 
 |-  ( ph -> A. x e. A ( ( J + K ) < ( H ` x ) -> ( ( F .x. G ) ` x ) = ( 0g ` R ) ) )
160 1 mplring 
 |-  ( ( I e. V /\ R e. Ring ) -> Y e. Ring )
161 3 4 160 syl2anc 
 |-  ( ph -> Y e. Ring )
162 5 6 ringcl 
 |-  ( ( Y e. Ring /\ F e. B /\ G e. B ) -> ( F .x. G ) e. B )
163 161 7 8 162 syl3anc 
 |-  ( ph -> ( F .x. G ) e. B )
164 39 140 sselid 
 |-  ( ph -> ( J + K ) e. RR* )
165 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 ) ) ) )
166 163 164 165 syl2anc 
 |-  ( ph -> ( ( D ` ( F .x. G ) ) <_ ( J + K ) <-> A. x e. A ( ( J + K ) < ( H ` x ) -> ( ( F .x. G ) ` x ) = ( 0g ` R ) ) ) )
167 159 166 mpbird 
 |-  ( ph -> ( D ` ( F .x. G ) ) <_ ( J + K ) )