let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed 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 associative commutative well-unital distributive add-associative right_zeroed 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 associative commutative well-unital distributive add-associative right_zeroed 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)) ) ) by Def5;
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, Def5;
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 10
.= ((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)) by VECTSP_1:def 23
.= (f . b) * (((HC (p,T)) ") * (HC (p,T))) by GROUP_1:def 4
.= (f . b) * (1. L) by A4, VECTSP_1:def 22
.= f . b by VECTSP_1:def 13 ;
g = f + (- (((f . b) / (HC (p,T))) * (s *' p))) by A3, POLYNOM1:def 23;
then g . b = (f . b) + ((- (((f . b) / (HC (p,T))) * (s *' p))) . b) by POLYNOM1:def 21
.= (f . b) + (- ((((f . b) / (HC (p,T))) * (s *' p)) . b)) by POLYNOM1:def 22
.= 0. L by A5, RLVECT_1:16 ;
hence not b in Support g by POLYNOM1:def 9; :: thesis: verum