:: On polynomials with coefficients in a ring of polynomials
:: by Barbara Dzienis
::
:: Received August 10, 2001
:: Copyright (c) 2001-2012 Association of Mizar Users


begin

notation
let L1, L2 be non empty doubleLoopStr ;
synonym L1,L2 are_isomorphic for L1 is_ringisomorph_to L2;
end;

definition
let L1, L2 be non empty doubleLoopStr ;
:: original:are_isomorphic
redefine predL1 is_ringisomorph_to L2;
reflexivity
 for L1 being non empty doubleLoopStr holds R83(b1,b1)
proofend;
end;

theorem Th1: :: POLYNOM6:1
for o1, o2 being Ordinal
for B being set st ( for x being set holds
( x in B iff ex o being Ordinal st
( x = o1 +^ o & o in o2 ) ) ) holds
o1 +^ o2 = o1 \/ B
proofend;

registration
let o1 be Ordinal;
let o2 be non empty Ordinal;
clustero1 +^ o2 ->  non empty ;
coherence
 not o1 +^ o2 is empty by ORDINAL3:26;
clustero2 +^ o1 ->  non empty ;
coherence
 not o2 +^ o1 is empty by ORDINAL3:26;
end;

theorem Th2: :: POLYNOM6:2
for n being Ordinal
for a, b being bag of n st a < b holds
ex o being Ordinal st
( o in n &amp; a . o < b . o &amp; ( for l being Ordinal st l in o holds
a . l = b . l ) )
proofend;

begin

definition
let o1, o2 be Ordinal;
let a be Element of Bags o1;
let b be Element of Bags o2;
funca +^ b ->  Element of Bags (o1 +^ o2) means :Def1: :: POLYNOM6:def 1
 for o being Ordinal holds
( ( o in o1 implies it . o = a . o ) &amp; ( o in (o1 +^ o2) \ o1 implies it . o = b . (o -^ o1) ) );
existence
 ex b1 being Element of Bags (o1 +^ o2) st
for o being Ordinal holds
( ( o in o1 implies b1 . o = a . o ) &amp; ( o in (o1 +^ o2) \ o1 implies b1 . o = b . (o -^ o1) ) )
proofend;
uniqueness
 for b1, b2 being Element of Bags (o1 +^ o2) st ( for o being Ordinal holds
( ( o in o1 implies b1 . o = a . o ) &amp; ( o in (o1 +^ o2) \ o1 implies b1 . o = b . (o -^ o1) ) ) ) &amp; ( for o being Ordinal holds
( ( o in o1 implies b2 . o = a . o ) &amp; ( o in (o1 +^ o2) \ o1 implies b2 . o = b . (o -^ o1) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines +^ POLYNOM6:def_1_:_
 for o1, o2 being Ordinal
for a being Element of Bags o1
for b being Element of Bags o2
for b5 being Element of Bags (o1 +^ o2) holds
( b5 = a +^ b iff for o being Ordinal holds
( ( o in o1 implies b5 . o = a . o ) &amp; ( o in (o1 +^ o2) \ o1 implies b5 . o = b . (o -^ o1) ) ) );

theorem Th3: :: POLYNOM6:3
for o1, o2 being Ordinal
for a being Element of Bags o1
for b being Element of Bags o2 st o2 = {} holds
a +^ b = a
proofend;

theorem :: POLYNOM6:4
for o1, o2 being Ordinal
for a being Element of Bags o1
for b being Element of Bags o2 st o1 = {} holds
a +^ b = b
proofend;

theorem Th5: :: POLYNOM6:5
for o1, o2 being Ordinal
for b1 being Element of Bags o1
for b2 being Element of Bags o2 holds
( b1 +^ b2 = EmptyBag (o1 +^ o2) iff ( b1 = EmptyBag o1 &amp; b2 = EmptyBag o2 ) )
proofend;

theorem Th6: :: POLYNOM6:6
for o1, o2 being Ordinal
for c being Element of Bags (o1 +^ o2) ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st c = c1 +^ c2
proofend;

theorem Th7: :: POLYNOM6:7
for o1, o2 being Ordinal
for b1, c1 being Element of Bags o1
for b2, c2 being Element of Bags o2 st b1 +^ b2 = c1 +^ c2 holds
( b1 = c1 &amp; b2 = c2 )
proofend;

theorem Th8: :: POLYNOM6:8
for n being Ordinal
for L being non empty right_complementable Abelian add-associative right_zeroed associative distributive doubleLoopStr
for p, q, r being Series of n,L holds (p + q) *' r = (p *' r) + (q *' r)
proofend;

begin

registration
let n be Ordinal;
let L be non empty non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
cluster Polynom-Ring (n,L) ->  non trivial distributive ;
coherence
 ( not Polynom-Ring (n,L) is trivial &amp; Polynom-Ring (n,L) is distributive )
proofend;
end;

definition
let o1, o2 be non empty Ordinal;
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ;
let P be Polynomial of o1,(Polynom-Ring (o2,L));
func Compress P ->  Polynomial of (o1 +^ o2),L means :Def2: :: POLYNOM6:def 2
 for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 &amp; b = b1 +^ b2 &amp; it . b = Q1 . b2 );
existence
 ex b1 being Polynomial of (o1 +^ o2),L st
for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 &amp; b = b1 +^ b2 &amp; b1 . b = Q1 . b2 )
proofend;
uniqueness
 for b1, b2 being Polynomial of (o1 +^ o2),L st ( for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 &amp; b = b1 +^ b2 &amp; b1 . b = Q1 . b2 ) ) &amp; ( for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 &amp; b = b1 +^ b2 &amp; b2 . b = Q1 . b2 ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines Compress POLYNOM6:def_2_:_
 for o1, o2 being non empty Ordinal
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for P being Polynomial of o1,(Polynom-Ring (o2,L))
for b5 being Polynomial of (o1 +^ o2),L holds
( b5 = Compress P iff for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 &amp; b = b1 +^ b2 &amp; b5 . b = Q1 . b2 ) );

theorem Th9: :: POLYNOM6:9
for o1, o2 being Ordinal
for b1, c1 being Element of Bags o1
for b2, c2 being Element of Bags o2 st b1 divides c1 &amp; b2 divides c2 holds
b1 +^ b2 divides c1 +^ c2
proofend;

theorem Th10: :: POLYNOM6:10
for o1, o2 being Ordinal
for b being bag of o1 +^ o2
for b1 being Element of Bags o1
for b2 being Element of Bags o2 st b divides b1 +^ b2 holds
ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st
( c1 divides b1 &amp; c2 divides b2 &amp; b = c1 +^ c2 )
proofend;

theorem Th11: :: POLYNOM6:11
for o1, o2 being Ordinal
for a1, b1 being Element of Bags o1
for a2, b2 being Element of Bags o2 holds
( a1 +^ a2 < b1 +^ b2 iff ( a1 < b1 or ( a1 = b1 &amp; a2 < b2 ) ) )
proofend;

theorem Th12: :: POLYNOM6:12
for o1, o2 being Ordinal
for b1 being Element of Bags o1
for b2 being Element of Bags o2
for G being FinSequence of (Bags (o1 +^ o2)) * st dom G = dom (divisors b1) &amp; ( for i being Nat st i in dom (divisors b1) holds
ex a19 being Element of Bags o1 ex Fk being FinSequence of Bags (o1 +^ o2) st
( Fk = G /. i &amp; (divisors b1) /. i = a19 &amp; len Fk = len (divisors b2) &amp; ( for m being Nat st m in dom Fk holds
ex a199 being Element of Bags o2 st
( (divisors b2) /. m = a199 &amp; Fk /. m = a19 +^ a199 ) ) ) ) holds
divisors (b1 +^ b2) = FlattenSeq G
proofend;

theorem Th13: :: POLYNOM6:13
for o1, o2 being Ordinal
for a1, b1, c1 being Element of Bags o1
for a2, b2, c2 being Element of Bags o2 st c1 = b1 -' a1 &amp; c2 = b2 -' a2 holds
(b1 +^ b2) -' (a1 +^ a2) = c1 +^ c2
proofend;

theorem Th14: :: POLYNOM6:14
for o1, o2 being Ordinal
for b1 being Element of Bags o1
for b2 being Element of Bags o2
for G being FinSequence of (2 -tuples_on (Bags (o1 +^ o2))) * st dom G = dom (decomp b1) &amp; ( for i being Nat st i in dom (decomp b1) holds
ex a19, b19 being Element of Bags o1 ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Fk = G /. i &amp; (decomp b1) /. i = <*a19,b19*> &amp; len Fk = len (decomp b2) &amp; ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> &amp; Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) ) ) holds
decomp (b1 +^ b2) = FlattenSeq G
proofend;

theorem :: POLYNOM6:15
for o1, o2 being non empty Ordinal
for L being non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr holds Polynom-Ring (o1,(Polynom-Ring (o2,L))), Polynom-Ring ((o1 +^ o2),L) are_isomorphic
proofend;