let n be Ordinal; for T being connected 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 p1, p2 being Polynomial of n,L st HT (p1,T), HT (p2,T) are_disjoint holds
S-Poly (p1,p2,T) = ((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T)))
let T be connected 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 p1, p2 being Polynomial of n,L st HT (p1,T), HT (p2,T) are_disjoint holds
S-Poly (p1,p2,T) = ((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T)))
let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; for p1, p2 being Polynomial of n,L st HT (p1,T), HT (p2,T) are_disjoint holds
S-Poly (p1,p2,T) = ((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T)))
let p1, p2 be Polynomial of n,L; ( HT (p1,T), HT (p2,T) are_disjoint implies S-Poly (p1,p2,T) = ((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T))) )
assume
HT (p1,T), HT (p2,T) are_disjoint
; S-Poly (p1,p2,T) = ((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T)))
then
lcm ((HT (p1,T)),(HT (p2,T))) = (HT (p1,T)) + (HT (p2,T))
by GROEB_2:5;
hence S-Poly (p1,p2,T) =
((HC (p2,T)) * ((((HT (p1,T)) + (HT (p2,T))) / (HT (p1,T))) *' p1)) - ((HC (p1,T)) * ((((HT (p1,T)) + (HT (p2,T))) / (HT (p2,T))) *' p2))
by GROEB_2:def 4
.=
((HC (p2,T)) * ((HT (p2,T)) *' p1)) - ((HC (p1,T)) * ((((HT (p1,T)) + (HT (p2,T))) / (HT (p2,T))) *' p2))
by Th1
.=
((HC (p2,T)) * ((HT (p2,T)) *' p1)) - ((HC (p1,T)) * ((HT (p1,T)) *' p2))
by Th1
.=
((HC (p2,T)) * ((HT (p2,T)) *' ((HM (p1,T)) + (Red (p1,T))))) - ((HC (p1,T)) * ((HT (p1,T)) *' p2))
by TERMORD:38
.=
((HC (p2,T)) * ((HT (p2,T)) *' ((HM (p1,T)) + (Red (p1,T))))) - ((HC (p1,T)) * ((HT (p1,T)) *' ((HM (p2,T)) + (Red (p2,T)))))
by TERMORD:38
.=
((Monom ((HC (p2,T)),(HT (p2,T)))) *' ((HM (p1,T)) + (Red (p1,T)))) - ((HC (p1,T)) * ((HT (p1,T)) *' ((HM (p2,T)) + (Red (p2,T)))))
by POLYRED:22
.=
((Monom ((HC (p2,T)),(HT (p2,T)))) *' ((HM (p1,T)) + (Red (p1,T)))) - ((Monom ((HC (p1,T)),(HT (p1,T)))) *' ((HM (p2,T)) + (Red (p2,T))))
by POLYRED:22
.=
((HM (p2,T)) *' ((HM (p1,T)) + (Red (p1,T)))) - ((Monom ((HC (p1,T)),(HT (p1,T)))) *' ((HM (p2,T)) + (Red (p2,T))))
by TERMORD:def 8
.=
((HM (p2,T)) *' ((HM (p1,T)) + (Red (p1,T)))) - ((HM (p1,T)) *' ((HM (p2,T)) + (Red (p2,T))))
by TERMORD:def 8
.=
(((HM (p2,T)) *' (HM (p1,T))) + ((HM (p2,T)) *' (Red (p1,T)))) - ((HM (p1,T)) *' ((HM (p2,T)) + (Red (p2,T))))
by POLYNOM1:26
.=
(((HM (p2,T)) *' (HM (p1,T))) + ((HM (p2,T)) *' (Red (p1,T)))) - (((HM (p1,T)) *' (HM (p2,T))) + ((HM (p1,T)) *' (Red (p2,T))))
by POLYNOM1:26
.=
(((HM (p2,T)) *' (HM (p1,T))) + ((HM (p2,T)) *' (Red (p1,T)))) + (- (((HM (p1,T)) *' (HM (p2,T))) + ((HM (p1,T)) *' (Red (p2,T)))))
by POLYNOM1:def 7
.=
(((HM (p2,T)) *' (HM (p1,T))) + ((HM (p2,T)) *' (Red (p1,T)))) + ((- ((HM (p1,T)) *' (HM (p2,T)))) + (- ((HM (p1,T)) *' (Red (p2,T)))))
by POLYRED:1
.=
((HM (p2,T)) *' (Red (p1,T))) + (((HM (p2,T)) *' (HM (p1,T))) + ((- ((HM (p1,T)) *' (HM (p2,T)))) + (- ((HM (p1,T)) *' (Red (p2,T))))))
by POLYNOM1:21
.=
((HM (p2,T)) *' (Red (p1,T))) + ((((HM (p2,T)) *' (HM (p1,T))) + (- ((HM (p1,T)) *' (HM (p2,T))))) + (- ((HM (p1,T)) *' (Red (p2,T)))))
by POLYNOM1:21
.=
((HM (p2,T)) *' (Red (p1,T))) + ((0_ (n,L)) + (- ((HM (p1,T)) *' (Red (p2,T)))))
by POLYRED:3
.=
((HM (p2,T)) *' (Red (p1,T))) + (- ((HM (p1,T)) *' (Red (p2,T))))
by POLYRED:2
.=
((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T)))
by POLYNOM1:def 7
;
verum