let n be Ordinal; :: thesis:
let T be connected TermOrder of n; :: thesis:
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis:
let p1, p2 be non-zero Polynomial of n,L; :: thesis:
assume A1: HT p2,T divides HT p1,T ; :: thesis:
A2: ( p1 <> 0_ n,L & p2 <> 0_ n,L ) by POLYNOM7:def 2;
then Support p1 <> {} by POLYNOM7:1;
then A3: HT p1,T in Support p1 by TERMORD:def 6;
set hcp2 = HC p2,T;
A4: HC p2,T <> 0. L by A2, TERMORD:17;
A5: HT ((HC p2,T) * p1),T = HT p1,T by POLYRED:21;
consider b being bag of such that
A6: HT p1,T = (HT p2,T) + b by A1, TERMORD:1;
set g = ((HC p2,T) * p1) - (((((HC p2,T) * p1) . (HT p1,T)) / (HC p2,T)) * (b *' p2));
A7: Support p1 c= Support ((HC p2,T) * p1) by POLYRED:20;
then (HC p2,T) * p1 <> 0_ n,L by A3, POLYNOM7:1;
then A8: (HC p2,T) * p1 reduces_to ((HC p2,T) * p1) - (((((HC p2,T) * p1) . (HT p1,T)) / (HC p2,T)) * (b *' p2)),p2, HT p1,T,T by A2, A3, A6, A7, POLYRED:def 5;
A9: lcm (HT p1,T),(HT p2,T) = HT p1,T by A1, Th11;
((HC p2,T) * p1) - (((((HC p2,T) * p1) . (HT p1,T)) / (HC p2,T)) * (b *' p2)) = ((HC p2,T) * p1) - ((((HC p2,T) * (p1 . (HT p1,T))) / (HC p2,T)) * (b *' p2)) by POLYNOM7:def 10
.= ((HC p2,T) * p1) - ((((HC p2,T) * (HC p1,T)) / (HC p2,T)) * (b *' p2)) by TERMORD:def 7
.= ((HC p2,T) * p1) - ((((HC p2,T) * (HC p1,T)) * ((HC p2,T) " )) * (b *' p2)) by VECTSP_1:def 23
.= ((HC p2,T) * p1) - (((HC p1,T) * ((HC p2,T) * ((HC p2,T) " ))) * (b *' p2)) by GROUP_1:def 4
.= ((HC p2,T) * p1) - (((HC p1,T) * (1. L)) * (b *' p2)) by A4, VECTSP_1:def 22
.= ((HC p2,T) * p1) - ((HC p1,T) * (b *' p2)) by VECTSP_1:def 13
.= ((HC p2,T) * ((EmptyBag n) *' p1)) - ((HC p1,T) * (b *' p2)) by POLYRED:17
.= ((HC p2,T) * (((HT p1,T) / (HT p1,T)) *' p1)) - ((HC p1,T) * (b *' p2)) by Th10
.= S-Poly p1,p2,T by A1, A6, A9, Def1 ;
hence (HC p2,T) * p1 top_reduces_to S-Poly p1,p2,T,p2,T by A5, A8, POLYRED:def 10; :: thesis: