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) = ((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 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) = ((Red (p1,T)) *' p2) - ((Red (p2,T)) *' p1)
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) = ((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 7
.= ((p2 + (- (Red (p2,T)))) *' (Red (p1,T))) - ((p1 + (- (Red (p1,T)))) *' (Red (p2,T))) by POLYNOM1:def 7
.= ((p2 *' (Red (p1,T))) + (r2 *' (Red (p1,T)))) - ((p1 + (- (Red (p1,T)))) *' (Red (p2,T))) by POLYNOM1:26
.= ((p2 *' (Red (p1,T))) + (r2 *' (Red (p1,T)))) - ((p1 *' (Red (p2,T))) + (r1 *' (Red (p2,T)))) by POLYNOM1:26
.= ((p2 *' (Red (p1,T))) + (r2 *' (Red (p1,T)))) + (- ((p1 *' (Red (p2,T))) + (r1 *' (Red (p2,T))))) by POLYNOM1:def 7
.= ((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:21
.= (p2 *' (Red (p1,T))) + ((0_ (n,L)) + (- (p1 *' (Red (p2,T))))) by A1, POLYNOM1:21
.= (p2 *' (Red (p1,T))) + (- (p1 *' (Red (p2,T)))) by POLYRED:2
.= ((Red (p1,T)) *' p2) - ((Red (p2,T)) *' p1) by POLYNOM1:def 7 ;
:: thesis: verum