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 that
A1: p1 in P and
A2: p2 in P ; :: thesis: S-Poly p1,p2,T in P -Ideal
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 p19 = p1, p29 = p2 as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider p19 = p19, p29 = p29 as Element of (Polynom-Ring n,L) ;
reconsider q19 = Monom (HC p2,T),((lcm (HT p1,T),(HT p2,T)) / (HT p1,T)), q29 = 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 q19 = q19, q29 = q29 as Element of (Polynom-Ring n,L) ;
p29 in P -Ideal by A2, Lm2;
then A3: q29 * p29 in P -Ideal by IDEAL_1:def 2;
p19 in P -Ideal by A1, Lm2;
then q19 * p19 in P -Ideal by IDEAL_1:def 2;
then A4: (q19 * p19) - (q29 * p29) in P -Ideal by A3, IDEAL_1:16;
set q = S-Poly p1,p2,T;
A5: ( (Monom (HC p2,T),((lcm (HT p1,T),(HT p2,T)) / (HT p1,T))) *' p1 = q19 * p19 & (Monom (HC p1,T),((lcm (HT p1,T),(HT p2,T)) / (HT p2,T))) *' p2 = q29 * p29 ) by POLYNOM1:def 27;
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 ;
hence S-Poly p1,p2,T in P -Ideal by A4, A5, Lm3; :: thesis: verum