let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, g being non-zero Polynomial of n,L
for p being Polynomial of n,L st p . (HT (f *' g),T) = 0. L holds
(f *' g) + p reduces_to ((Red f,T) *' g) + p,{g},T
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, g being non-zero Polynomial of n,L
for p being Polynomial of n,L st p . (HT (f *' g),T) = 0. L holds
(f *' g) + p reduces_to ((Red f,T) *' g) + p,{g},T
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for f, g being non-zero Polynomial of n,L
for p being Polynomial of n,L st p . (HT (f *' g),T) = 0. L holds
(f *' g) + p reduces_to ((Red f,T) *' g) + p,{g},T
let f, g be non-zero Polynomial of n,L; :: thesis: for p being Polynomial of n,L st p . (HT (f *' g),T) = 0. L holds
(f *' g) + p reduces_to ((Red f,T) *' g) + p,{g},T
let p be Polynomial of n,L; :: thesis: ( p . (HT (f *' g),T) = 0. L implies (f *' g) + p reduces_to ((Red f,T) *' g) + p,{g},T )
assume A1: p . (HT (f *' g),T) = 0. L ; :: thesis: (f *' g) + p reduces_to ((Red f,T) *' g) + p,{g},T
set fg = (f *' g) + p;
set q = ((f *' g) + p) - (((((f *' g) + p) . (HT (f *' g),T)) / (HC g,T)) * ((HT f,T) *' g));
f *' g <> 0_ n,L by POLYNOM7:def 2;
then Support (f *' g) <> {} by POLYNOM7:1;
then HT (f *' g),T in Support (f *' g) by TERMORD:def 6;
then A2: (f *' g) . (HT (f *' g),T) <> 0. L by POLYNOM1:def 9;
((f *' g) + p) . (HT (f *' g),T) = ((f *' g) . (HT (f *' g),T)) + (p . (HT (f *' g),T)) by POLYNOM1:def 21
.= (f *' g) . (HT (f *' g),T) by A1, RLVECT_1:def 7 ;
then A3: HT (f *' g),T in Support ((f *' g) + p) by A2, POLYNOM1:def 9;
then A4: ( (f *' g) + p <> 0_ n,L & g <> 0_ n,L ) by POLYNOM7:1, POLYNOM7:def 2;
A5: g in {g} by TARSKI:def 1;
HT (f *' g),T = (HT f,T) + (HT g,T) by TERMORD:31;
then (f *' g) + p reduces_to ((f *' g) + p) - (((((f *' g) + p) . (HT (f *' g),T)) / (HC g,T)) * ((HT f,T) *' g)),g, HT (f *' g),T,T by A3, A4, POLYRED:def 5;
then A6: (f *' g) + p reduces_to ((f *' g) + p) - (((((f *' g) + p) . (HT (f *' g),T)) / (HC g,T)) * ((HT f,T) *' g)),g,T by POLYRED:def 6;
A7: HC g,T <> 0. L by A4, TERMORD:17;
reconsider r = - (HM f,T) as Polynomial of n,L ;
((f *' g) + p) - (((((f *' g) + p) . (HT (f *' g),T)) / (HC g,T)) * ((HT f,T) *' g)) = ((f *' g) + p) - (((((f *' g) . (HT (f *' g),T)) + (0. L)) / (HC g,T)) * ((HT f,T) *' g)) by A1, POLYNOM1:def 21
.= ((f *' g) + p) - ((((f *' g) . (HT (f *' g),T)) / (HC g,T)) * ((HT f,T) *' g)) by RLVECT_1:def 7
.= ((f *' g) + p) - (((HC (f *' g),T) / (HC g,T)) * ((HT f,T) *' g)) by TERMORD:def 7
.= ((f *' g) + p) - ((((HC f,T) * (HC g,T)) / (HC g,T)) * ((HT f,T) *' g)) by TERMORD:32
.= ((f *' g) + p) - ((((HC f,T) * (HC g,T)) * ((HC g,T) " )) * ((HT f,T) *' g)) by VECTSP_1:def 23
.= ((f *' g) + p) - (((HC f,T) * ((HC g,T) * ((HC g,T) " ))) * ((HT f,T) *' g)) by GROUP_1:def 4
.= ((f *' g) + p) - (((HC f,T) * (1. L)) * ((HT f,T) *' g)) by A7, VECTSP_1:def 22
.= ((f *' g) + p) - ((HC f,T) * ((HT f,T) *' g)) by VECTSP_1:def 16
.= ((f *' g) + p) - ((Monom (HC f,T),(HT f,T)) *' g) by POLYRED:22
.= ((f *' g) + p) - ((HM f,T) *' g) by TERMORD:def 8
.= ((f *' g) + p) + (- ((HM f,T) *' g)) by POLYNOM1:def 23
.= ((f *' g) + p) + (r *' g) by POLYRED:6
.= ((f *' g) + (r *' g)) + p by POLYNOM1:80
.= (g *' (f + (- (HM f,T)))) + p by POLYNOM1:85
.= ((f - (HM f,T)) *' g) + p by POLYNOM1:def 23
.= ((Red f,T) *' g) + p by TERMORD:def 9 ;
hence (f *' g) + p reduces_to ((Red f,T) *' g) + p,{g},T by A5, A6, POLYRED:def 7; :: thesis: verum