let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being non-zero Polynomial of n,L holds HT ((p *' q),T) = (HT (p,T)) + (HT (q,T))
let O be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being non-zero Polynomial of n,L holds HT ((p *' q),O) = (HT (p,O)) + (HT (q,O))
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for p, q being non-zero Polynomial of n,L holds HT ((p *' q),O) = (HT (p,O)) + (HT (q,O))
let p, q be non-zero Polynomial of n,L; :: thesis: HT ((p *' q),O) = (HT (p,O)) + (HT (q,O))
A1: (HT (p,O)) + (HT (q,O)) is Element of Bags n by PRE_POLY:def 12;
(HT (p,O)) + (HT (q,O)) in Support (p *' q) by Th29;
then (HT (p,O)) + (HT (q,O)) <= HT ((p *' q),O),O by Def6;
then A2: [((HT (p,O)) + (HT (q,O))),(HT ((p *' q),O))] in O ;
Support (p *' q) <> {} by Th29;
then A3: HT ((p *' q),O) in Support (p *' q) by Def6;
Support (p *' q) c= { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) } by Th30;
then HT ((p *' q),O) in { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) } by A3;
then consider s, t being Element of Bags n such that
A4: HT ((p *' q),O) = s + t and
A5: s in Support p and
A6: t in Support q ;
s <= HT (p,O),O by A5, Def6;
then [s,(HT (p,O))] in O ;
then A7: [(s + t),((HT (p,O)) + t)] in O by BAGORDER:def 5;
t <= HT (q,O),O by A6, Def6;
then [t,(HT (q,O))] in O ;
then A8: [(t + (HT (p,O))),((HT (p,O)) + (HT (q,O)))] in O by BAGORDER:def 5;
( s + t is Element of Bags n & (HT (p,O)) + t is Element of Bags n ) by PRE_POLY:def 12;
then [(s + t),((HT (p,O)) + (HT (q,O)))] in O by A1, A7, A8, ORDERS_1:5;
hence HT ((p *' q),O) = (HT (p,O)) + (HT (q,O)) by A2, A4, A1, ORDERS_1:4; :: thesis: verum