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

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 pred L1 is_ringisomorph_to L2;
reflexivity
for L1 being non empty doubleLoopStr holds R86(b₁,b₁)

proof end;

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

proof end;

registration

let o1 be Ordinal;
let o2 be non empty Ordinal;

cluster o1 +^ o2 -> non empty ;

coherence
not o1 +^ o2 is empty by ORDINAL3:26;

cluster o2 +^ 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 & a . o < b . o & ( for l being Ordinal st l in o holds
a . l = b . l ) )

proof end;

definition

let o1, o2 be Ordinal;
let a be Element of Bags o1;
let b be Element of Bags o2;

func a +^ b -> Element of Bags (o1 +^ o2) means :Def1: :: POLYNOM6:def 1
for o being Ordinal holds
( ( o in o1 implies it . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies it . o = b . (o -^ o1) ) );

existence
ex b₁ being Element of Bags (o1 +^ o2) st
for o being Ordinal holds
( ( o in o1 implies b₁ . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies b₁ . o = b . (o -^ o1) ) )

proof end;

uniqueness
for b₁, b₂ being Element of Bags (o1 +^ o2) st ( for o being Ordinal holds
( ( o in o1 implies b₁ . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies b₁ . o = b . (o -^ o1) ) ) ) & ( for o being Ordinal holds
( ( o in o1 implies b₂ . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies b₂ . o = b . (o -^ o1) ) ) ) holds
b₁ = b₂

proof end;

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 b₅ being Element of Bags (o1 +^ o2) holds
( b₅ = a +^ b iff for o being Ordinal holds
( ( o in o1 implies b₅ . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies b₅ . 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

proof end;

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

proof end;

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 & b2 = EmptyBag o2 ) )

proof end;

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

proof end;

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 & b2 = c2 )

proof end;

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)

proof end;

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 & Polynom-Ring (n,L) is distributive )

proof end;

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 & b = b1 +^ b2 & it . b = Q1 . b2 );

existence
ex b₁ 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 & b = b1 +^ b2 & b₁ . b = Q1 . b2 )

proof end;

uniqueness
for b₁, b₂ 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 & b = b1 +^ b2 & b₁ . b = Q1 . b2 ) ) & ( 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 & b = b1 +^ b2 & b₂ . b = Q1 . b2 ) ) holds
b₁ = b₂

proof end;

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 b₅ being Polynomial of (o1 +^ o2),L holds
( b₅ = 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 & b = b1 +^ b2 & b₅ . 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 & b2 divides c2 holds
b1 +^ b2 divides c1 +^ c2

proof end;

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 & c2 divides b2 & b = c1 +^ c2 )

proof end;

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 & a2 < b2 ) ) )

proof end;

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) & ( 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 & (divisors b1) /. i = a19 & len Fk = len (divisors b2) & ( for m being Nat st m in dom Fk holds
ex a199 being Element of Bags o2 st
( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 ) ) ) ) holds
divisors (b1 +^ b2) = FlattenSeq G

proof end;

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 & c2 = b2 -' a2 holds
(b1 +^ b2) -' (a1 +^ a2) = c1 +^ c2

proof end;

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) & ( 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 & (decomp b1) /. i = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) ) ) holds
decomp (b1 +^ b2) = FlattenSeq G

proof end;

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

proof end;