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 such that
A1: f reduces_to g,p,b,T by POLYRED:def 6;
A2: 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 such that
A3: ( s + (HT p,T) = b & g = f - (((f . b) / (HC p,T)) * (s *' p)) ) by A1, POLYRED:def 5;
A4: ((f . b) / (HC p,T)) * (s *' p) = (Monom ((f . b) / (HC p,T)),s) *' p by POLYRED:22;
set m = Monom ((f . b) / (HC p,T)),s;
b in Support f by A1, POLYRED:def 5;
then A5: f . b <> 0. L by POLYNOM1:def 9;
HC p,T <> 0. L by A2, TERMORD:17;
then 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 A5, A6, VECTSP_2:def 5;
then A8: not (f . b) / (HC p,T) is zero by STRUCT_0:def 15;
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, A3, POLYRED:def 5;
then HT (m *' p),T <= HT f,T,T by 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, A9, POLYRED:39; :: thesis: verum