let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for p1, p2 being Polynomial of n,L holds
( S-Poly (p1,p2,T) = 0_ (n,L) or HT ((S-Poly (p1,p2,T)),T) < lcm ((HT (p1,T)),(HT (p2,T))),T )
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for p1, p2 being Polynomial of n,L holds
( S-Poly (p1,p2,T) = 0_ (n,L) or HT ((S-Poly (p1,p2,T)),T) < lcm ((HT (p1,T)),(HT (p2,T))),T )
let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for p1, p2 being Polynomial of n,L holds
( S-Poly (p1,p2,T) = 0_ (n,L) or HT ((S-Poly (p1,p2,T)),T) < lcm ((HT (p1,T)),(HT (p2,T))),T )
let p1, p2 be Polynomial of n,L; :: thesis: ( S-Poly (p1,p2,T) = 0_ (n,L) or HT ((S-Poly (p1,p2,T)),T) < lcm ((HT (p1,T)),(HT (p2,T))),T )
assume A1: S-Poly (p1,p2,T) <> 0_ (n,L) ; :: thesis: HT ((S-Poly (p1,p2,T)),T) < lcm ((HT (p1,T)),(HT (p2,T))),T
set sp = S-Poly (p1,p2,T);
set g1 = (HC (p2,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))) *' p1);
set g2 = (HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2);

per cases ( p1 = 0_ (n,L) or p2 = 0_ (n,L) or ( p1 <> 0_ (n,L) & p2 <> 0_ (n,L) ) ) ;

suppose ( p1 = 0_ (n,L) or p2 = 0_ (n,L) ) ; :: thesis: HT ((S-Poly (p1,p2,T)),T) < lcm ((HT (p1,T)),(HT (p2,T))),T

hence HT ((S-Poly (p1,p2,T)),T) < lcm ((HT (p1,T)),(HT (p2,T))),T by A1, Th20; :: thesis: verum

end;

suppose A2: ( p1 <> 0_ (n,L) & p2 <> 0_ (n,L) ) ; :: thesis: HT ((S-Poly (p1,p2,T)),T) < lcm ((HT (p1,T)),(HT (p2,T))),T

then A3: HC (p2,T) <> 0. L by TERMORD:17;
then A4: not HC (p2,T) is zero ;
A5: HT ((Monom ((HC (p2,T)),((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))))),T) = term (Monom ((HC (p2,T)),((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))))) by TERMORD:23
.= (lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T)) by A4, POLYNOM7:10 ;
A6: p1 is non-zero by A2, POLYNOM7:def 1;
HC ((Monom ((HC (p2,T)),((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))))),T) = coefficient (Monom ((HC (p2,T)),((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))))) by TERMORD:23
.= HC (p2,T) by POLYNOM7:9 ;
then Monom ((HC (p2,T)),((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T)))) <> 0_ (n,L) by A3, TERMORD:17;
then A7: Monom ((HC (p2,T)),((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T)))) is non-zero by POLYNOM7:def 1;
A8: HC (((HC (p2,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))) *' p1)),T) = HC (((Monom ((HC (p2,T)),((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))))) *' p1),T) by POLYRED:22
.= (HC ((Monom ((HC (p2,T)),((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))))),T)) * (HC (p1,T)) by A6, A7, TERMORD:32
.= (coefficient (Monom ((HC (p2,T)),((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T)))))) * (HC (p1,T)) by TERMORD:23
.= (HC (p1,T)) * (HC (p2,T)) by POLYNOM7:9 ;
A9: HT (p1,T) divides lcm ((HT (p1,T)),(HT (p2,T))) by Th3;
A10: HT (((HC (p2,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))) *' p1)),T) = HT (((Monom ((HC (p2,T)),((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))))) *' p1),T) by POLYRED:22
.= (HT ((Monom ((HC (p2,T)),((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))))),T)) + (HT (p1,T)) by A6, A7, TERMORD:31
.= lcm ((HT (p1,T)),(HT (p2,T))) by A9, A5, Def1 ;
A11: HC (p1,T) <> 0. L by A2, TERMORD:17;
then A12: not HC (p1,T) is zero ;
A13: HT ((Monom ((HC (p1,T)),((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))))),T) = term (Monom ((HC (p1,T)),((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))))) by TERMORD:23
.= (lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T)) by A12, POLYNOM7:10 ;
A14: p2 is non-zero by A2, POLYNOM7:def 1;
HC ((Monom ((HC (p1,T)),((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))))),T) = coefficient (Monom ((HC (p1,T)),((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))))) by TERMORD:23
.= HC (p1,T) by POLYNOM7:9 ;
then Monom ((HC (p1,T)),((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T)))) <> 0_ (n,L) by A11, TERMORD:17;
then A15: Monom ((HC (p1,T)),((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T)))) is non-zero by POLYNOM7:def 1;
Support (S-Poly (p1,p2,T)) <> {} by A1, POLYNOM7:1;
then A16: HT ((S-Poly (p1,p2,T)),T) in Support (S-Poly (p1,p2,T)) by TERMORD:def 6;
A17: HT (p2,T) divides lcm ((HT (p1,T)),(HT (p2,T))) by Th3;
A18: HC (((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2)),T) = HC (((Monom ((HC (p1,T)),((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))))) *' p2),T) by POLYRED:22
.= (HC ((Monom ((HC (p1,T)),((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))))),T)) * (HC (p2,T)) by A14, A15, TERMORD:32
.= (coefficient (Monom ((HC (p1,T)),((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T)))))) * (HC (p2,T)) by TERMORD:23
.= (HC (p1,T)) * (HC (p2,T)) by POLYNOM7:9 ;
A19: HT (((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2)),T) = HT (((Monom ((HC (p1,T)),((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))))) *' p2),T) by POLYRED:22
.= (HT ((Monom ((HC (p1,T)),((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))))),T)) + (HT (p2,T)) by A14, A15, TERMORD:31
.= lcm ((HT (p1,T)),(HT (p2,T))) by A17, A13, Def1 ;
then (S-Poly (p1,p2,T)) . (lcm ((HT (p1,T)),(HT (p2,T)))) = (((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)))) . (HT (((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2)),T)) by POLYNOM1:def 7
.= (((HC (p2,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))) *' p1)) . (HT (((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2)),T))) + ((- ((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2))) . (HT (((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2)),T))) by POLYNOM1:15
.= (((HC (p2,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))) *' p1)) . (HT (((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2)),T))) + (- (((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2)) . (HT (((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2)),T)))) by POLYNOM1:17
.= (HC (((HC (p2,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))) *' p1)),T)) + (- (((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2)) . (HT (((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2)),T)))) by A10, A19, TERMORD:def 7
.= (HC (((HC (p2,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))) *' p1)),T)) + (- (HC (((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2)),T))) by TERMORD:def 7
.= 0. L by A8, A18, RLVECT_1:5 ;
then A20: not lcm ((HT (p1,T)),(HT (p2,T))) in Support (S-Poly (p1,p2,T)) by POLYNOM1:def 4;
HT ((S-Poly (p1,p2,T)),T) <= max ((HT (((HC (p2,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))) *' p1)),T)),(HT (((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2)),T)),T),T by GROEB_1:7;
then HT ((S-Poly (p1,p2,T)),T) <= lcm ((HT (p1,T)),(HT (p2,T))),T by A10, A19, TERMORD:12;
hence HT ((S-Poly (p1,p2,T)),T) < lcm ((HT (p1,T)),(HT (p2,T))),T by A16, A20, TERMORD:def 3; :: thesis: verum

end;

end;