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 & len s = len (decomp ((HT p,O) + (HT q,O))) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of 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
A2: ( divisors ((HT p,O) + (HT q,O)) = SgmX (BagOrder n),S & ( for p being bag of holds
( p in S iff p divides (HT p,O) + (HT q,O) ) ) ) by POLYNOM1:def 18;
HT p,O divides (HT p,O) + (HT q,O) by POLYNOM1:54;
then A3: HT p,O in S by A2;
set sgm = SgmX (BagOrder n),S;
BagOrder n linearly_orders S by Lm13;
then HT p,O in rng (SgmX (BagOrder n),S) by A3, TRIANG_1:def 2;
then consider i being set such that
A4: ( i in dom (SgmX (BagOrder n),S) & (SgmX (BagOrder n),S) . i = HT p,O ) by FUNCT_1:def 5;
A5: i in dom (decomp ((HT p,O) + (HT q,O))) by A2, A4, POLYNOM1:def 19;
(divisors ((HT p,O) + (HT q,O))) /. i = HT p,O by A2, A4, PARTFUN1:def 8;
then A6: (decomp ((HT p,O) + (HT q,O))) /. i = <*(HT p,O),(((HT p,O) + (HT q,O)) -' (HT p,O))*> by A5, POLYNOM1:def 19;
then A7: (decomp ((HT p,O) + (HT q,O))) /. i = <*(HT p,O),(HT q,O)*> by POLYNOM1:52;
A8: dom s = Seg (len (decomp ((HT p,O) + (HT q,O)))) by A1, FINSEQ_1:def 3
.= dom (decomp ((HT p,O) + (HT q,O))) by FINSEQ_1:def 3 ;
then A9: i in dom s by A2, A4, POLYNOM1:def 19;
reconsider i = i as Element of NAT by A4;
A10: now
let k be Element of NAT ; :: thesis: ( k in dom s & k <> i implies s /. k = 0. L )
assume A11: ( k in dom s & k <> i ) ; :: thesis: s /. k = 0. L
then consider b1', b2' being bag of such that
A12: ( (decomp ((HT p,O) + (HT q,O))) /. k = <*b1',b2'*> & (HT p,O) + (HT q,O) = b1' + b2' ) by A8, POLYNOM1:72;
consider b1, b2 being bag of such that
A13: ( (decomp ((HT p,O) + (HT q,O))) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) by A1, A11;
A14: b1 = <*b1',b2'*> . 1 by A12, A13, FINSEQ_1:61
.= b1' by FINSEQ_1:61 ;
A15: b2 = <*b1',b2'*> . 2 by A12, A13, FINSEQ_1:61
.= b2' by FINSEQ_1:61 ;
A16: now
assume A17: ( p . b1 <> 0. L & q . b2 <> 0. L ) ; :: thesis: contradiction
( b1 is Element of Bags n & b2 is Element of Bags n ) by POLYNOM1:def 14;
then ( b1 in Support p & b2 in Support q ) by A17, POLYNOM1:def 9;
then ( b1 <= HT p,O,O & b2 <= HT q,O,O ) by Def6;
then A18: ( [b1,(HT p,O)] in O & [b2,(HT q,O)] in O ) by Def2;
A19: 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 A8, A11, A13, PARTFUN1:def 8
.= (decomp ((HT p,O) + (HT q,O))) /. i by A6, POLYNOM1:52
.= (decomp ((HT p,O) + (HT q,O))) . i by A5, PARTFUN1:def 8 ;
hence contradiction by A5, A8, A11, FUNCT_1:def 8; :: thesis: verum
end;
now
per cases ( b1 <> HT p,O or b2 <> HT q,O ) by A19;
case A20: b1 <> HT p,O ; :: thesis: contradiction
A21: now
assume b1 + b2 = (HT p,O) + b2 ; :: thesis: contradiction
then b1 = ((HT p,O) + b2) -' b2 by POLYNOM1:52;
hence contradiction by A20, POLYNOM1:52; :: thesis: verum
end;
A22: [((HT p,O) + (HT q,O)),((HT p,O) + b2)] in O by A12, A14, A15, A18, BAGORDER:def 7;
A23: [((HT p,O) + b2),((HT p,O) + (HT q,O))] in O by A18, BAGORDER:def 7;
( (HT p,O) + b2 is Element of Bags n & (HT p,O) + (HT q,O) is Element of Bags n ) by POLYNOM1:def 14;
hence contradiction by A12, A14, A15, A21, A22, A23, ORDERS_1:13; :: thesis: verum
end;
case A24: b2 <> HT q,O ; :: thesis: contradiction
A25: now
assume b2 + b1 = (HT q,O) + b1 ; :: thesis: contradiction
then b2 = ((HT q,O) + b1) -' b1 by POLYNOM1:52;
hence contradiction by A24, POLYNOM1:52; :: thesis: verum
end;
A26: [((HT p,O) + (HT q,O)),((HT q,O) + b1)] in O by A12, A14, A15, A18, BAGORDER:def 7;
A27: [((HT q,O) + b1),((HT p,O) + (HT q,O))] in O by A18, BAGORDER:def 7;
( (HT q,O) + b1 is Element of Bags n & (HT p,O) + (HT q,O) is Element of Bags n ) by POLYNOM1:def 14;
hence contradiction by A12, A14, A15, A25, A26, A27, 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 A16;
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 A13; :: thesis: verum
end;
consider b1, b2 being bag of such that
A28: ( (decomp ((HT p,O) + (HT q,O))) /. i = <*b1,b2*> & s /. i = (p . b1) * (q . b2) ) by A1, A9;
A29: b1 = <*(HT p,O),(HT q,O)*> . 1 by A7, A28, FINSEQ_1:61
.= HT p,O by FINSEQ_1:61 ;
b2 = <*(HT p,O),(HT q,O)*> . 2 by A7, A28, FINSEQ_1:61
.= HT q,O by FINSEQ_1:61 ;
hence (p *' q) . ((HT p,O) + (HT q,O)) = (p . (HT p,O)) * (q . (HT q,O)) by A1, A9, A10, A28, A29, POLYNOM2:5; :: thesis: verum