let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for f, f1, g, p being Polynomial of n,L st f reduces_to f1,{p},T & ( for b1 being bag of n st b1 in Support g holds
not HT (p,T) divides b1 ) holds
f + g reduces_to f1 + g,{p},T
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for f, f1, g, p being Polynomial of n,L st f reduces_to f1,{p},T & ( for b1 being bag of n st b1 in Support g holds
not HT (p,T) divides b1 ) holds
f + g reduces_to f1 + g,{p},T
let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for f, f1, g, p being Polynomial of n,L st f reduces_to f1,{p},T & ( for b1 being bag of n st b1 in Support g holds
not HT (p,T) divides b1 ) holds
f + g reduces_to f1 + g,{p},T
let f, f1, g, p be Polynomial of n,L; :: thesis: ( f reduces_to f1,{p},T & ( for b1 being bag of n st b1 in Support g holds
not HT (p,T) divides b1 ) implies f + g reduces_to f1 + g,{p},T )
assume that
A1: f reduces_to f1,{p},T and
A2: for b1 being bag of n st b1 in Support g holds
not HT (p,T) divides b1 ; :: thesis: f + g reduces_to f1 + g,{p},T
consider q being Polynomial of n,L such that
A3: q in {p} and
A4: f reduces_to f1,q,T by A1, POLYRED:def 7;
p = q by A3, TARSKI:def 1;
then consider br being bag of n such that
A5: f reduces_to f1,p,br,T by A4, POLYRED:def 6;
consider s being bag of n such that
A6: s + (HT (p,T)) = br and
A7: f1 = f - (((f . br) / (HC (p,T))) * (s *' p)) by A5, POLYRED:def 5;
A8: not br in Support g by A6, TERMORD:1, A2;
A9: br is Element of Bags n by PRE_POLY:def 12;
A10: p in {p} by TARSKI:def 1;
A11: br in Support f by A5, POLYRED:def 5;
A12: (f + g) . br = (f . br) + (g . br) by POLYNOM1:15
.= (f . br) + (0. L) by A8, A9, POLYNOM1:def 4
.= f . br by RLVECT_1:def 4 ;
A13: p <> 0_ (n,L) by A5, POLYRED:def 5;
now :: thesis: ( ( f + g = 0_ (n,L) & contradiction ) or ( f + g <> 0_ (n,L) & f + g reduces_to f1 + g,{p},T ) )
per cases ( f + g = 0_ (n,L) or f + g <> 0_ (n,L) ) ;
case f + g = 0_ (n,L) ; :: thesis: contradiction
then (f + g) - f = - f by Th14;
then (f + g) + (- f) = - f by POLYNOM1:def 7;
then (f + (- f)) + g = - f by POLYNOM1:21;
then (0_ (n,L)) + g = - f by POLYRED:3;
then g = - f by POLYRED:2;
hence contradiction by A11, A8, GROEB_1:5; :: thesis: verum
end;
case A14: f + g <> 0_ (n,L) ; :: thesis: f + g reduces_to f1 + g,{p},T
set g1 = (f + g) - ((((f + g) . br) / (HC (p,T))) * (s *' p));
(f + g) . br <> 0. L by A11, A12, POLYNOM1:def 4;
then br in Support (f + g) by A11, POLYNOM1:def 4;
then f + g reduces_to (f + g) - ((((f + g) . br) / (HC (p,T))) * (s *' p)),p,br,T by A13, A6, A14, POLYRED:def 5;
then A15: f + g reduces_to (f + g) - ((((f + g) . br) / (HC (p,T))) * (s *' p)),p,T by POLYRED:def 6;
(f + g) - ((((f + g) . br) / (HC (p,T))) * (s *' p)) = (f + g) + (- (((f . br) / (HC (p,T))) * (s *' p))) by A12, POLYNOM1:def 7
.= (f + (- (((f . br) / (HC (p,T))) * (s *' p)))) + g by POLYNOM1:21
.= f1 + g by A7, POLYNOM1:def 7 ;
hence f + g reduces_to f1 + g,{p},T by A10, A15, POLYRED:def 7; :: thesis: verum
end;
end;
end;
hence f + g reduces_to f1 + g,{p},T ; :: thesis: verum