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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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 4;
p <> 0_ (n,L) by A1, POLYRED:def 5;
then reconsider p = p as non-zero Polynomial of n,L by POLYNOM7:def 1;
consider s being bag of n such that
A3: s + (HT (p,T)) = b and
A4: g = f - (((f . b) / (HC (p,T))) * (s *' p)) by A1, POLYRED:def 5;
set m = Monom (((f . b) / (HC (p,T))),s);
A5: (HC (p,T)) " <> 0. L by VECTSP_1:25;
A6: (f . b) / (HC (p,T)) <> 0. L by A2, A5, VECTSP_2:def 1;
then A7: not (f . b) / (HC (p,T)) is zero ;
coefficient (Monom (((f . b) / (HC (p,T))),s)) <> 0. L by A6, 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 1;
A8: 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 A7, POLYNOM7:10 ;
then HT ((m *' p),T) in Support f by A1, A3, 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, A3, A4, A8, POLYRED:39; :: thesis: verum