let n be Ordinal; 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 p1, p2 being non-zero Polynomial of n,L st HT p2,T divides HT p1,T holds
(HC p2,T) * p1 top_reduces_to S-Poly p1,p2,T,p2,T
let T be 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 p1, p2 being non-zero Polynomial of n,L st HT p2,T divides HT p1,T holds
(HC p2,T) * p1 top_reduces_to S-Poly p1,p2,T,p2,T
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; for p1, p2 being non-zero Polynomial of n,L st HT p2,T divides HT p1,T holds
(HC p2,T) * p1 top_reduces_to S-Poly p1,p2,T,p2,T
let p1, p2 be non-zero Polynomial of n,L; ( HT p2,T divides HT p1,T implies (HC p2,T) * p1 top_reduces_to S-Poly p1,p2,T,p2,T )
set hcp2 = HC p2,T;
assume A1:
HT p2,T divides HT p1,T
; (HC p2,T) * p1 top_reduces_to S-Poly p1,p2,T,p2,T
then consider b being bag of n such that
A2:
HT p1,T = (HT p2,T) + b
by TERMORD:1;
set g = ((HC p2,T) * p1) - (((((HC p2,T) * p1) . (HT p1,T)) / (HC p2,T)) * (b *' p2));
A3:
p2 <> 0_ n,L
by POLYNOM7:def 2;
A4:
HC p2,T <> 0. L
;
p1 <> 0_ n,L
by POLYNOM7:def 2;
then
Support p1 <> {}
by POLYNOM7:1;
then A5:
HT p1,T in Support p1
by TERMORD:def 6;
A6:
Support p1 c= Support ((HC p2,T) * p1)
by POLYRED:20;
then
(HC p2,T) * p1 <> 0_ n,L
by A5, POLYNOM7:1;
then A7:
( HT ((HC p2,T) * p1),T = HT p1,T & (HC p2,T) * p1 reduces_to ((HC p2,T) * p1) - (((((HC p2,T) * p1) . (HT p1,T)) / (HC p2,T)) * (b *' p2)),p2, HT p1,T,T )
by A3, A5, A2, A6, POLYRED:21, POLYRED:def 5;
A8:
lcm (HT p1,T),(HT p2,T) = HT p1,T
by A1, Th11;
((HC p2,T) * p1) - (((((HC p2,T) * p1) . (HT p1,T)) / (HC p2,T)) * (b *' p2)) =
((HC p2,T) * p1) - ((((HC p2,T) * (p1 . (HT p1,T))) / (HC p2,T)) * (b *' p2))
by POLYNOM7:def 10
.=
((HC p2,T) * p1) - ((((HC p2,T) * (HC p1,T)) / (HC p2,T)) * (b *' p2))
by TERMORD:def 7
.=
((HC p2,T) * p1) - ((((HC p2,T) * (HC p1,T)) * ((HC p2,T) " )) * (b *' p2))
by VECTSP_1:def 23
.=
((HC p2,T) * p1) - (((HC p1,T) * ((HC p2,T) * ((HC p2,T) " ))) * (b *' p2))
by GROUP_1:def 4
.=
((HC p2,T) * p1) - (((HC p1,T) * (1. L)) * (b *' p2))
by A4, VECTSP_1:def 22
.=
((HC p2,T) * p1) - ((HC p1,T) * (b *' p2))
by VECTSP_1:def 13
.=
((HC p2,T) * ((EmptyBag n) *' p1)) - ((HC p1,T) * (b *' p2))
by POLYRED:17
.=
((HC p2,T) * (((HT p1,T) / (HT p1,T)) *' p1)) - ((HC p1,T) * (b *' p2))
by Th10
.=
S-Poly p1,p2,T
by A1, A2, A8, Def1
;
hence
(HC p2,T) * p1 top_reduces_to S-Poly p1,p2,T,p2,T
by A7, POLYRED:def 10; verum