let n be Ordinal; 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; 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 ; 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; 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; ( 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
; (f *' g) + p reduces_to ((Red f,T) *' g) + p,{g},T
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;
reconsider r = - (HM f,T) as Polynomial of n,L ;
set fg = (f *' g) + p;
set q = ((f *' g) + p) - (((((f *' g) + p) . (HT (f *' g),T)) / (HC g,T)) * ((HT f,T) *' g));
A3:
HT (f *' g),T = (HT f,T) + (HT g,T)
by TERMORD:31;
A4:
g <> 0_ n,L
by POLYNOM7:def 2;
A5:
HC g,T <> 0. L
;
((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 A6:
HT (f *' g),T in Support ((f *' g) + p)
by A2, POLYNOM1:def 9;
then
(f *' g) + p <> 0_ n,L
by POLYNOM7:1;
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 A6, A4, A3, POLYRED:def 5;
then A7:
( g in {g} & (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, TARSKI:def 1;
((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 A5, 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 A7, POLYRED:def 7; verum