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 P being Subset of (Polynom-Ring n,L)
for p1, p2 being Polynomial of n,L st p1 in P & p2 in P holds
S-Poly p1,p2,T in P -Ideal
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 P being Subset of (Polynom-Ring n,L)
for p1, p2 being Polynomial of n,L st p1 in P & p2 in P holds
S-Poly p1,p2,T in P -Ideal
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for P being Subset of (Polynom-Ring n,L)
for p1, p2 being Polynomial of n,L st p1 in P & p2 in P holds
S-Poly p1,p2,T in P -Ideal
let P be Subset of (Polynom-Ring n,L); :: thesis: for p1, p2 being Polynomial of n,L st p1 in P & p2 in P holds
S-Poly p1,p2,T in P -Ideal
let p1, p2 be Polynomial of n,L; :: thesis: ( p1 in P & p2 in P implies S-Poly p1,p2,T in P -Ideal )
assume A1: ( p1 in P & p2 in P ) ; :: thesis: S-Poly p1,p2,T in P -Ideal
set q = S-Poly p1,p2,T;
reconsider p1' = p1, p2' = p2 as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider p1' = p1', p2' = p2' as Element of (Polynom-Ring n,L) ;
set q1 = Monom (HC p2,T),((lcm (HT p1,T),(HT p2,T)) / (HT p1,T));
set q2 = Monom (HC p1,T),((lcm (HT p1,T),(HT p2,T)) / (HT p2,T));
reconsider q1' = Monom (HC p2,T),((lcm (HT p1,T),(HT p2,T)) / (HT p1,T)), q2' = Monom (HC p1,T),((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider q1' = q1', q2' = q2' as Element of (Polynom-Ring n,L) ;
A2: S-Poly p1,p2,T = ((Monom (HC p2,T),((lcm (HT p1,T),(HT p2,T)) / (HT p1,T))) *' p1) - ((HC p1,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) *' p2)) by POLYRED:22
.= ((Monom (HC p2,T),((lcm (HT p1,T),(HT p2,T)) / (HT p1,T))) *' p1) - ((Monom (HC p1,T),((lcm (HT p1,T),(HT p2,T)) / (HT p2,T))) *' p2) by POLYRED:22 ;
( p1' in P -Ideal & p2' in P -Ideal ) by A1, Lm2;
then ( q1' * p1' in P -Ideal & q2' * p2' in P -Ideal ) by IDEAL_1:def 2;
then A3: (q1' * p1') - (q2' * p2') in P -Ideal by IDEAL_1:16;
( (Monom (HC p2,T),((lcm (HT p1,T),(HT p2,T)) / (HT p1,T))) *' p1 = q1' * p1' & (Monom (HC p1,T),((lcm (HT p1,T),(HT p2,T)) / (HT p2,T))) *' p2 = q2' * p2' ) by POLYNOM1:def 27;
hence S-Poly p1,p2,T in P -Ideal by A2, A3, Lm3; :: thesis: verum