The abstract of the Mizar article:

On Polynomials with Coefficients in a Ring of Polynomials

by

Barbara Dzienis

Received August 10, 2001

MML identifier: POLYNOM6

[ Mizar article, MML identifier index ]

environ

 vocabulary ORDINAL1, VECTSP_1, QUOFIELD, FUNCT_1, RELAT_1, SUBSET_1, WELLORD1,
      ORDINAL2, BOOLE, ORDINAL3, POLYNOM1, PBOOLE, SEQM_3, ALGSEQ_1, FINSET_1,
      FUNCOP_1, RLVECT_1, LATTICES, BINOP_1, ARYTM_3, FINSEQ_1, FINSEQ_4,
      FINSEQ_2, GROUP_1, REALSET1, TARSKI, DTCONSTR, MATRIX_2, ORDERS_2,
      CARD_1, ARYTM_1, TRIANG_1, VECTSP_2, PRE_TOPC, GRCAT_1, COHSP_1, PRALG_1,
      ENDALG, POLYNOM6;
 notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, VECTSP_1,
      RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, STRUCT_0, NAT_1, TRIANG_1, ORDERS_2,
      PBOOLE, PRE_TOPC, PRALG_1, RLVECT_1, VECTSP_2, FINSET_1, FINSEQ_1,
      FINSEQ_2, FINSEQ_4, SEQM_3, BINARITH, DTCONSTR, ORDINAL1, ORDINAL2,
      ORDINAL3, GROUP_1, REALSET1, QUOFIELD, GRCAT_1, ENDALG, WSIERP_1,
      MATRLIN, TOPREAL1, FVSUM_1, POLYNOM1, POLYNOM3;
 constructors POLYNOM1, ALGSTR_2, QUOFIELD, MONOID_0, GRCAT_1, ORDINAL3,
      REAL_1, FVSUM_1, SETWOP_2, ENDALG, BINARITH, WSIERP_1, ORDERS_2,
      TOPREAL1, TRIANG_1, FINSOP_1, POLYNOM3, MEMBERED;
 clusters XREAL_0, STRUCT_0, FUNCT_1, FINSET_1, RELSET_1, FINSEQ_1, FINSEQ_2,
      PRALG_1, ARYTM_3, POLYNOM2, GOBRD13, POLYNOM1, QUOFIELD, WAYBEL10,
      VECTSP_1, MEMBERED, NUMBERS, ORDINAL2;
 requirements BOOLE, SUBSET, NUMERALS, REAL;


begin :: Preliminaries

reserve o1,o2 for Ordinal;

definition let L1,L2 be non empty doubleLoopStr;
 redefine pred L1 is_ringisomorph_to L2;
 reflexivity;
 synonym L1,L2 are_isomorphic;
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;

definition 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

definition
 let n be Ordinal,
     L be right_zeroed Abelian add-associative right_complementable
          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 unital distributive
          non trivial (non empty 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 a1' being Element of Bags o1,
           Fk being FinSequence of Bags(o1+^o2)
        st Fk = G/.i & (divisors b1)/.i = a1' &
        len Fk = len divisors b2 &
        for m being Nat st m in dom Fk
         ex a1'' being Element of Bags o2 st
          (divisors b2)/.m = a1'' &
          Fk/.m = a1'+^a1''
 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 a1', b1' being Element of Bags o1,
           Fk being FinSequence of 2-tuples_on Bags(o1+^o2)
        st Fk = G/.i & (decomp b1)/.i = <*a1', b1'*> &
        len Fk = len decomp b2 &
        for m being Nat st m in dom Fk
         ex a1'',b1'' being Element of Bags o2 st
          (decomp b2)/.m = <*a1'', b1''*> &
          Fk/.m =<*a1'+^a1'',b1'+^b1''*>
 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
          unital distributive associative well-unital
          non trivial (non empty doubleLoopStr)
 holds Polynom-Ring (o1,Polynom-Ring(o2,L)),Polynom-Ring (o1+^o2,L)
        are_isomorphic;