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