let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, g being non-zero Polynomial of n,L holds f *' g reduces_to (Red f,T) *' g,{g},T
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, g being non-zero Polynomial of n,L holds f *' g reduces_to (Red f,T) *' g,{g},T
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for f, g being non-zero Polynomial of n,L holds f *' g reduces_to (Red f,T) *' g,{g},T
let f, g be non-zero Polynomial of n,L; :: thesis: f *' g reduces_to (Red f,T) *' g,{g},T
set fg = f *' g;
set q = (f *' g) - ((((f *' g) . (HT (f *' g),T)) / (HC g,T)) * ((HT f,T) *' g));
A1: ( f *' g <> 0_ n,L & g <> 0_ n,L ) by POLYNOM7:def 2;
then Support (f *' g) <> {} by POLYNOM7:1;
then A2: HT (f *' g),T in Support (f *' g) by TERMORD:def 6;
A3: g in {g} by TARSKI:def 1;
HT (f *' g),T = (HT f,T) + (HT g,T) by TERMORD:31;
then f *' g reduces_to (f *' g) - ((((f *' g) . (HT (f *' g),T)) / (HC g,T)) * ((HT f,T) *' g)),g, HT (f *' g),T,T by A1, A2, POLYRED:def 5;
then A4: f *' g reduces_to (f *' g) - ((((f *' g) . (HT (f *' g),T)) / (HC g,T)) * ((HT f,T) *' g)),g,T by POLYRED:def 6;
A5: HC g,T <> 0. L by A1, TERMORD:17;
reconsider r = - (HM f,T) as Polynomial of n,L ;
(f *' g) - ((((f *' g) . (HT (f *' g),T)) / (HC g,T)) * ((HT f,T) *' g)) = (f *' g) - (((HC (f *' g),T) / (HC g,T)) * ((HT f,T) *' g)) by TERMORD:def 7
.= (f *' g) - ((((HC f,T) * (HC g,T)) / (HC g,T)) * ((HT f,T) *' g)) by TERMORD:32
.= (f *' g) - ((((HC f,T) * (HC g,T)) * ((HC g,T) " )) * ((HT f,T) *' g)) by VECTSP_1:def 23
.= (f *' g) - (((HC f,T) * ((HC g,T) * ((HC g,T) " ))) * ((HT f,T) *' g)) by GROUP_1:def 4
.= (f *' g) - (((HC f,T) * (1. L)) * ((HT f,T) *' g)) by A5, VECTSP_1:def 22
.= (f *' g) - ((HC f,T) * ((HT f,T) *' g)) by VECTSP_1:def 16
.= (f *' g) - ((Monom (HC f,T),(HT f,T)) *' g) by POLYRED:22
.= (f *' g) - ((HM f,T) *' g) by TERMORD:def 8
.= (f *' g) + (- ((HM f,T) *' g)) by POLYNOM1:def 23
.= (f *' g) + (r *' g) by POLYRED:6
.= g *' (f + (- (HM f,T))) by POLYNOM1:85
.= (f - (HM f,T)) *' g by POLYNOM1:def 23
.= (Red f,T) *' g by TERMORD:def 9 ;
hence f *' g reduces_to (Red f,T) *' g,{g},T by A3, A4, POLYRED:def 7; :: thesis: verum