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 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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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 11;

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 11;

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 11;

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

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative 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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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 11;

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 11;

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 11;

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