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
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
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
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 ; :: 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 p1' = p1, p2' = p2 as Element of by POLYNOM1:def 27;
reconsider p1' = p1', p2' = p2' as Element of ;
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 by POLYNOM1:def 27;
reconsider q1' = q1', q2' = q2' as Element of ;
p2' in P -Ideal by A2, Lm2;
then A3: q2' * p2' in P -Ideal by IDEAL_1:def 2;
p1' in P -Ideal by A1, Lm2;
then q1' * p1' in P -Ideal by IDEAL_1:def 2;
then A4: (q1' * p1') - (q2' * p2') 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 = q1' * p1' & (Monom (HC p1,T),((lcm (HT p1,T),(HT p2,T)) / (HT p2,T))) *' p2 = q2' * p2' ) 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