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 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 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 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 st f reduces_to g,p,b,T holds
not b in Support g
let b be bag of ; :: 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 st
( s + (HT p,T) = b & g = f - (((f . b) / (HC p,T)) * (s *' p)) ) ) by Def5;
then consider s being bag of such that
A2: ( b in Support f & s + (HT p,T) = b & g = f - (((f . b) / (HC p,T)) * (s *' p)) ) ;
set q = ((f . b) / (HC p,T)) * (s *' p);
p <> 0_ n,L by A1, Def5;
then A3: HC p,T <> 0. L by TERMORD:17;
A4: (((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 A3, VECTSP_1:def 22
.= f . b by VECTSP_1:def 13 ;
g = f + (- (((f . b) / (HC p,T)) * (s *' p))) by A2, 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 A4, RLVECT_1:16 ;
hence not b in Support g by POLYNOM1:def 9; :: thesis: verum