let n be Ordinal; :: thesis: 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; :: thesis: 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 ; :: 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: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 ;
:: thesis: verum