let n be Ordinal; :: thesis: for T being connected 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 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; :: thesis: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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:9;
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:85
.= (((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:85
.= (((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 23
.= (((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:80
.= ((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:80
.= ((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 23 ;
:: thesis: verum