let n be Ordinal; for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative 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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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 1;
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 4;
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 1;
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:15
.=
(f *' g) . (HT ((f *' g),T))
by A1, RLVECT_1:def 4
;
then A6:
HT ((f *' g),T) in Support ((f *' g) + p)
by A2, POLYNOM1:def 4;
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:15
.=
((f *' g) + p) - ((((f *' g) . (HT ((f *' g),T))) / (HC (g,T))) * ((HT (f,T)) *' g))
by RLVECT_1:def 4
.=
((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))
.=
((f *' g) + p) - (((HC (f,T)) * ((HC (g,T)) * ((HC (g,T)) "))) * ((HT (f,T)) *' g))
by GROUP_1:def 3
.=
((f *' g) + p) - (((HC (f,T)) * (1. L)) * ((HT (f,T)) *' g))
by A5, VECTSP_1:def 10
.=
((f *' g) + p) - ((HC (f,T)) * ((HT (f,T)) *' g))
.=
((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 7
.=
((f *' g) + p) + (r *' g)
by POLYRED:6
.=
((f *' g) + (r *' g)) + p
by POLYNOM1:21
.=
(g *' (f + (- (HM (f,T))))) + p
by POLYNOM1:26
.=
((f - (HM (f,T))) *' g) + p
by POLYNOM1:def 7
.=
((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