let n be Ordinal; :: thesis: for O being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed left_zeroed doubleLoopStr
for p, q being non-zero Polynomial of n,L holds (p *' q) . ((HT p,O) + (HT q,O)) = (p . (HT p,O)) * (q . (HT q,O))
let O be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed left_zeroed doubleLoopStr
for p, q being non-zero Polynomial of n,L holds (p *' q) . ((HT p,O) + (HT q,O)) = (p . (HT p,O)) * (q . (HT q,O))
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed left_zeroed doubleLoopStr ; :: thesis: for p, q being non-zero Polynomial of n,L holds (p *' q) . ((HT p,O) + (HT q,O)) = (p . (HT p,O)) * (q . (HT q,O))
let p, q be non-zero Polynomial of n,L; :: thesis: (p *' q) . ((HT p,O) + (HT q,O)) = (p . (HT p,O)) * (q . (HT q,O))
set b = (HT p,O) + (HT q,O);
consider s being FinSequence of L such that
A1: (p *' q) . ((HT p,O) + (HT q,O)) = Sum s and
A2: len s = len (decomp ((HT p,O) + (HT q,O))) and
A3: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp ((HT p,O) + (HT q,O))) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) by POLYNOM1:def 26;
consider S being non empty finite Subset of (Bags n) such that
A4: divisors ((HT p,O) + (HT q,O)) = SgmX (BagOrder n),S and
A5: for p being bag of n holds
( p in S iff p divides (HT p,O) + (HT q,O) ) by PRE_POLY:def 16;
set sgm = SgmX (BagOrder n),S;
A6: BagOrder n linearly_orders S by Lm13;
HT p,O divides (HT p,O) + (HT q,O) by PRE_POLY:50;
then HT p,O in S by A5;
then HT p,O in rng (SgmX (BagOrder n),S) by A6, PRE_POLY:def 2;
then consider i being set such that
A7: i in dom (SgmX (BagOrder n),S) and
A8: (SgmX (BagOrder n),S) . i = HT p,O by FUNCT_1:def 5;
A9: i in dom (decomp ((HT p,O) + (HT q,O))) by A4, A7, PRE_POLY:def 17;
(divisors ((HT p,O) + (HT q,O))) /. i = HT p,O by A4, A7, A8, PARTFUN1:def 8;
then A10: (decomp ((HT p,O) + (HT q,O))) /. i = <*(HT p,O),(((HT p,O) + (HT q,O)) -' (HT p,O))*> by A9, PRE_POLY:def 17;
then A11: (decomp ((HT p,O) + (HT q,O))) /. i = <*(HT p,O),(HT q,O)*> by PRE_POLY:48;
A12: dom s = Seg (len (decomp ((HT p,O) + (HT q,O)))) by A2, FINSEQ_1:def 3
.= dom (decomp ((HT p,O) + (HT q,O))) by FINSEQ_1:def 3 ;
then A13: i in dom s by A4, A7, PRE_POLY:def 17;
reconsider i = i as Element of NAT by A7;
consider b1, b2 being bag of n such that
A14: (decomp ((HT p,O) + (HT q,O))) /. i = <*b1,b2*> and
A15: s /. i = (p . b1) * (q . b2) by A3, A13;
A16: b2 = <*(HT p,O),(HT q,O)*> . 2 by A11, A14, FINSEQ_1:61
.= HT q,O by FINSEQ_1:61 ;

A17: now

let k be Element of NAT ; :: thesis: ( k in dom s & k <> i implies s /. k = 0. L )
assume that
A18: k in dom s and
A19: k <> i ; :: thesis: s /. k = 0. L
consider b1, b2 being bag of n such that
A20: (decomp ((HT p,O) + (HT q,O))) /. k = <*b1,b2*> and
A21: s /. k = (p . b1) * (q . b2) by A3, A18;
consider b19, b29 being bag of n such that
A22: (decomp ((HT p,O) + (HT q,O))) /. k = <*b19,b29*> and
A23: (HT p,O) + (HT q,O) = b19 + b29 by A12, A18, PRE_POLY:68;
A24: b2 = <*b19,b29*> . 2 by A22, A20, FINSEQ_1:61
.= b29 by FINSEQ_1:61 ;
A25: b1 = <*b19,b29*> . 1 by A22, A20, FINSEQ_1:61
.= b19 by FINSEQ_1:61 ;

A26: now

assume that
A27: p . b1 <> 0. L and
A28: q . b2 <> 0. L ; :: thesis: contradiction
b1 is Element of Bags n by PRE_POLY:def 12;
then b1 in Support p by A27, POLYNOM1:def 9;
then b1 <= HT p,O,O by Def6;
then A29: [b1,(HT p,O)] in O by Def2;
b2 is Element of Bags n by PRE_POLY:def 12;
then b2 in Support q by A28, POLYNOM1:def 9;
then b2 <= HT q,O,O by Def6;
then A30: [b2,(HT q,O)] in O by Def2;

A31: now

assume ( b1 = HT p,O & b2 = HT q,O ) ; :: thesis: contradiction
then (decomp ((HT p,O) + (HT q,O))) . k = <*(HT p,O),(HT q,O)*> by A12, A18, A20, PARTFUN1:def 8
.= (decomp ((HT p,O) + (HT q,O))) /. i by A10, PRE_POLY:48
.= (decomp ((HT p,O) + (HT q,O))) . i by A9, PARTFUN1:def 8 ;
hence contradiction by A9, A12, A18, A19, FUNCT_1:def 8; :: thesis: verum

end;

now

per cases ( b1 <> HT p,O or b2 <> HT q,O ) by A31;

case A32: b1 <> HT p,O ; :: thesis: contradiction

A33: now

assume b1 + b2 = (HT p,O) + b2 ; :: thesis: contradiction
then b1 = ((HT p,O) + b2) -' b2 by PRE_POLY:48;
hence contradiction by A32, PRE_POLY:48; :: thesis: verum

end;

A34: ( (HT p,O) + b2 is Element of Bags n & (HT p,O) + (HT q,O) is Element of Bags n ) by PRE_POLY:def 12;
( [((HT p,O) + (HT q,O)),((HT p,O) + b2)] in O & [((HT p,O) + b2),((HT p,O) + (HT q,O))] in O ) by A23, A25, A24, A29, A30, BAGORDER:def 7;
hence contradiction by A23, A25, A24, A33, A34, ORDERS_1:13; :: thesis: verum

end;

case A35: b2 <> HT q,O ; :: thesis: contradiction

A36: now

assume b2 + b1 = (HT q,O) + b1 ; :: thesis: contradiction
then b2 = ((HT q,O) + b1) -' b1 by PRE_POLY:48;
hence contradiction by A35, PRE_POLY:48; :: thesis: verum

end;

A37: ( (HT q,O) + b1 is Element of Bags n & (HT p,O) + (HT q,O) is Element of Bags n ) by PRE_POLY:def 12;
( [((HT p,O) + (HT q,O)),((HT q,O) + b1)] in O & [((HT q,O) + b1),((HT p,O) + (HT q,O))] in O ) by A23, A25, A24, A29, A30, BAGORDER:def 7;
hence contradiction by A23, A25, A24, A36, A37, ORDERS_1:13; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

now

per cases ( p . b1 = 0. L or q . b2 = 0. L ) by A26;

case p . b1 = 0. L ; :: thesis: (p . b1) * (q . b2) = 0. L

hence (p . b1) * (q . b2) = 0. L by BINOM:1; :: thesis: verum

end;

case q . b2 = 0. L ; :: thesis: (p . b1) * (q . b2) = 0. L

hence (p . b1) * (q . b2) = 0. L by BINOM:2; :: thesis: verum

end;

end;

end;

hence s /. k = 0. L by A21; :: thesis: verum

end;

b1 = <*(HT p,O),(HT q,O)*> . 1 by A11, A14, FINSEQ_1:61
.= HT p,O by FINSEQ_1:61 ;
hence (p *' q) . ((HT p,O) + (HT q,O)) = (p . (HT p,O)) * (q . (HT q,O)) by A1, A13, A17, A15, A16, POLYNOM2:5; :: thesis: verum