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 = ((Red p1,T) *' p2) - ((Red p2,T) *' p1)
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 = ((Red p1,T) *' p2) - ((Red p2,T) *' p1)
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 = ((Red p1,T) *' p2) - ((Red p2,T) *' p1)
let p1, p2 be Polynomial of n,L; :: thesis: ( HT p1,T, HT p2,T are_disjoint implies S-Poly p1,p2,T = ((Red p1,T) *' p2) - ((Red p2,T) *' p1) )
reconsider r1 = - (Red p1,T), r2 = - (Red p2,T) as Polynomial of n,L ;
r2 *' (Red p1,T) = - ((Red p2,T) *' (Red p1,T)) by POLYRED:6
.= r1 *' (Red p2,T) by POLYRED:6 ;
then A1: (r2 *' (Red p1,T)) + (- (r1 *' (Red p2,T))) = 0_ n,L by POLYRED:3;
assume HT p1,T, HT p2,T are_disjoint ; :: thesis: S-Poly p1,p2,T = ((Red p1,T) *' p2) - ((Red p2,T) *' p1)
hence S-Poly p1,p2,T = ((HM p2,T) *' (Red p1,T)) - ((HM p1,T) *' (Red p2,T)) by Th53
.= ((p2 - (Red p2,T)) *' (Red p1,T)) - ((HM p1,T) *' (Red p2,T)) by Th15
.= ((p2 - (Red p2,T)) *' (Red p1,T)) - ((p1 - (Red p1,T)) *' (Red p2,T)) by Th15
.= ((p2 + (- (Red p2,T))) *' (Red p1,T)) - ((p1 - (Red p1,T)) *' (Red p2,T)) by POLYNOM1:def 23
.= ((p2 + (- (Red p2,T))) *' (Red p1,T)) - ((p1 + (- (Red p1,T))) *' (Red p2,T)) by POLYNOM1:def 23
.= ((p2 *' (Red p1,T)) + (r2 *' (Red p1,T))) - ((p1 + (- (Red p1,T))) *' (Red p2,T)) by POLYNOM1:85
.= ((p2 *' (Red p1,T)) + (r2 *' (Red p1,T))) - ((p1 *' (Red p2,T)) + (r1 *' (Red p2,T))) by POLYNOM1:85
.= ((p2 *' (Red p1,T)) + (r2 *' (Red p1,T))) + (- ((p1 *' (Red p2,T)) + (r1 *' (Red p2,T)))) by POLYNOM1:def 23
.= ((p2 *' (Red p1,T)) + (r2 *' (Red p1,T))) + ((- (p1 *' (Red p2,T))) + (- (r1 *' (Red p2,T)))) by POLYRED:1
.= (p2 *' (Red p1,T)) + ((r2 *' (Red p1,T)) + ((- (r1 *' (Red p2,T))) + (- (p1 *' (Red p2,T))))) by POLYNOM1:80
.= (p2 *' (Red p1,T)) + ((0_ n,L) + (- (p1 *' (Red p2,T)))) by A1, POLYNOM1:80
.= (p2 *' (Red p1,T)) + (- (p1 *' (Red p2,T))) by POLYRED:2
.= ((Red p1,T) *' p2) - ((Red p2,T) *' p1) by POLYNOM1:def 23 ;
:: thesis: verum