:: On polynomials with coefficients in a ring of polynomials
::  by Barbara Dzienis
::
:: Received August 10, 2001
:: Copyright (c) 2001-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, ORDINAL1, XBOOLE_0, ALGSTR_0, WELLORD1, QUOFIELD,
      RELAT_1, FUNCT_1, SUBSET_1, STRUCT_0, ORDINAL2, TARSKI, ORDINAL3,
      PRE_POLY, ARYTM_3, CARD_1, PBOOLE, FINSET_1, VALUED_0, FUNCOP_1,
      RLVECT_1, LATTICES, BINOP_1, POLYNOM1, FINSEQ_1, CARD_3, PARTFUN1,
      FINSEQ_2, NAT_1, VECTSP_1, ZFMISC_1, GROUP_1, SUPINF_2, XXREAL_0,
      FINSEQ_3, ORDINAL4, ARYTM_1, ORDERS_1, MSSUBFAM, POLYNOM6;
 notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0,
      VALUED_0, VECTSP_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1,
      POLYNOM1, STRUCT_0, ALGSTR_0, NAT_1, NAT_D, ORDERS_1, PBOOLE, RLVECT_1,
      FINSET_1, FINSEQ_1, FINSEQ_2, ORDINAL2, ORDINAL3, GROUP_1, QUOFIELD,
      GRCAT_1, WSIERP_1, PRE_POLY, FVSUM_1, POLYNOM3, GROUP_6, XXREAL_0,
      MATRLIN;
 constructors ORDINAL3, BINARITH, WSIERP_1, GRCAT_1, GROUP_6, TRIANG_1,
      QUOFIELD, POLYNOM1, POLYNOM3, NAT_D, RELSET_1, MATRLIN, FVSUM_1,
      RINGCAT1, MOD_4;
 registrations FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1, XREAL_0,
      FINSEQ_1, FINSEQ_2, STRUCT_0, VECTSP_1, QUOFIELD, PRE_POLY, POLYNOM1,
      POLYNOM2, VALUED_0, CARD_1;
 requirements BOOLE, SUBSET, NUMERALS, REAL;


begin :: Preliminaries

reserve o1,o2 for Ordinal;

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;
  redefine pred L1 is_ringisomorph_to L2;
  reflexivity;
end;

theorem :: POLYNOM6:1
  for B be set st for x be set holds x in B iff ex o be Ordinal st
  x=o1+^o & o in o2 holds o1+^o2 = o1 \/ B;

registration
  let o1 be Ordinal, o2 be non empty Ordinal;
  cluster o1 +^ o2 -> non empty;
  cluster o2 +^ o1 -> non empty;
end;

theorem :: POLYNOM6:2
  for n being Ordinal, a,b being bag of n st a < b 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
;

begin ::About Bags

definition
  let o1,o2 be Ordinal;
  let a be Element of Bags o1,b be Element of Bags o2;
  func a +^ b -> Element of Bags (o1+^o2) means
:: POLYNOM6:def 1

  for o be Ordinal holds
  (o in o1 implies it.o = a.o) & (o in (o1+^o2) \ o1 implies it.o=b.(o-^o1));
end;

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

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

theorem :: POLYNOM6:5
  for b1 be Element of Bags o1,b2 be Element of Bags o2 holds b1+^
  b2 = EmptyBag(o1+^o2) iff b1 = EmptyBag o1 & b2 = EmptyBag o2;

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

theorem :: POLYNOM6:7
  for b1,c1 be Element of Bags o1 for b2,c2 be Element of Bags o2
  st b1+^b2 = c1+^c2 holds b1=c1 & b2=c2;

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

begin :: Main results

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

definition
  let o1,o2 be non empty Ordinal, L be right_zeroed add-associative
  right_complementable well-unital distributive non trivial
  doubleLoopStr;
  let P be Polynomial of o1,Polynom-Ring(o2,L);
  func Compress P -> Polynomial of o1+^o2,L means
:: POLYNOM6:def 2

  for b be Element of
  Bags (o1+^o2) ex b1 be Element of Bags o1, b2 be Element of Bags o2, Q1 be
  Polynomial of o2,L st Q1 = P.b1 & b = b1+^b2 & it.b = Q1.b2;
end;

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

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

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

theorem :: POLYNOM6:12
  for b1 being Element of Bags o1, 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, 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 ex a199 being Element of Bags
  o2 st (divisors b2)/.m = a199 & Fk/.m = a19+^a199 holds divisors(b1+^b2) =
  FlattenSeq G;

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

theorem :: POLYNOM6:14
  for b1 being Element of Bags o1, 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, 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 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;

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