let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f, p, g being Polynomial of n,L
for b being bag of n st f reduces_to g,p,b,T holds
not b in Support g
let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f, p, g being Polynomial of n,L
for b being bag of n st f reduces_to g,p,b,T holds
not b in Support g
let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for f, p, g being Polynomial of n,L
for b being bag of n st f reduces_to g,p,b,T holds
not b in Support g
let f, p, g be Polynomial of n,L; :: thesis: for b being bag of n st f reduces_to g,p,b,T holds
not b in Support g
let b be bag of n; :: thesis: ( f reduces_to g,p,b,T implies not b in Support g )
assume A1: f reduces_to g,p,b,T ; :: thesis: not b in Support g
then ( b in Support f & ex s being bag of n st
( s + (HT (p,T)) = b & g = f - (((f . b) / (HC (p,T))) * (s *' p)) ) ) ;
then consider s being bag of n such that
b in Support f and
A2: s + (HT (p,T)) = b and
A3: g = f - (((f . b) / (HC (p,T))) * (s *' p)) ;
p <> 0_ (n,L) by A1;
then A4: HC (p,T) <> 0. L by TERMORD:17;
set q = ((f . b) / (HC (p,T))) * (s *' p);
A5: (((f . b) / (HC (p,T))) * (s *' p)) . b = ((f . b) / (HC (p,T))) * ((s *' p) . b) by POLYNOM7:def 9
.= ((f . b) / (HC (p,T))) * (p . (HT (p,T))) by A2, Lm9
.= ((f . b) / (HC (p,T))) * (HC (p,T)) by TERMORD:def 7
.= ((f . b) * ((HC (p,T)) ")) * (HC (p,T))
.= (f . b) * (((HC (p,T)) ") * (HC (p,T))) by GROUP_1:def 3
.= (f . b) * (1. L) by A4, VECTSP_1:def 10
.= f . b ;
g = f + (- (((f . b) / (HC (p,T))) * (s *' p))) by A3, POLYNOM1:def 7;
then g . b = (f . b) + ((- (((f . b) / (HC (p,T))) * (s *' p))) . b) by POLYNOM1:15
.= (f . b) + (- ((((f . b) / (HC (p,T))) * (s *' p)) . b)) by POLYNOM1:17
.= 0. L by A5, RLVECT_1:5 ;
hence not b in Support g by POLYNOM1:def 4; :: thesis: verum