let n be Ordinal; 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; 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 ; 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; ( 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
; 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; verum