let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
ex m being Monomial of n,L st
( g = f - (m *' p) & not HT ((m *' p),T) in Support g & HT ((m *' p),T) <= HT (f,T),T )
let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
ex m being Monomial of n,L st
( g = f - (m *' p) & not HT ((m *' p),T) in Support g & HT ((m *' p),T) <= HT (f,T),T )
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
ex m being Monomial of n,L st
( g = f - (m *' p) & not HT ((m *' p),T) in Support g & HT ((m *' p),T) <= HT (f,T),T )
let f, p, g be Polynomial of n,L; :: thesis: ( f reduces_to g,p,T implies ex m being Monomial of n,L st
( g = f - (m *' p) & not HT ((m *' p),T) in Support g & HT ((m *' p),T) <= HT (f,T),T ) )
assume f reduces_to g,p,T ; :: thesis: ex m being Monomial of n,L st
( g = f - (m *' p) & not HT ((m *' p),T) in Support g & HT ((m *' p),T) <= HT (f,T),T )
then consider b being bag of n such that
A1: f reduces_to g,p,b,T by POLYRED:def 6;
b in Support f by A1, POLYRED:def 5;
then A2: f . b <> 0. L by POLYNOM1:def 9;
p <> 0_ (n,L) by A1, POLYRED:def 5;
then reconsider p = p as non-zero Polynomial of n,L by POLYNOM7:def 2;
consider s being bag of n such that
A4: s + (HT (p,T)) = b and
A5: g = f - (((f . b) / (HC (p,T))) * (s *' p)) by A1, POLYRED:def 5;
set m = Monom (((f . b) / (HC (p,T))),s);
A6: (HC (p,T)) " <> 0. L by VECTSP_1:74;
(f . b) / (HC (p,T)) = (f . b) * ((HC (p,T)) ") by VECTSP_1:def 23;
then A7: (f . b) / (HC (p,T)) <> 0. L by A2, A6, VECTSP_2:def 5;
then A8: not (f . b) / (HC (p,T)) is zero by STRUCT_0:def 12;
coefficient (Monom (((f . b) / (HC (p,T))),s)) <> 0. L by A7, POLYNOM7:9;
then HC ((Monom (((f . b) / (HC (p,T))),s)),T) <> 0. L by TERMORD:23;
then Monom (((f . b) / (HC (p,T))),s) <> 0_ (n,L) by TERMORD:17;
then reconsider m = Monom (((f . b) / (HC (p,T))),s) as non-zero Monomial of n,L by POLYNOM7:def 2;
A9: HT ((m *' p),T) = (HT (m,T)) + (HT (p,T)) by TERMORD:31
.= (term m) + (HT (p,T)) by TERMORD:23
.= s + (HT (p,T)) by A8, POLYNOM7:10 ;
then HT ((m *' p),T) in Support f by A1, A4, POLYRED:def 5;
then ( ((f . b) / (HC (p,T))) * (s *' p) = (Monom (((f . b) / (HC (p,T))),s)) *' p & HT ((m *' p),T) <= HT (f,T),T ) by POLYRED:22, TERMORD:def 6;
hence ex m being Monomial of n,L st
( g = f - (m *' p) & not HT ((m *' p),T) in Support g & HT ((m *' p),T) <= HT (f,T),T ) by A1, A4, A5, A9, POLYRED:39; :: thesis: verum