:: The Algebra of Polynomials
:: by Ewa Gr\c{a}dzka
::
:: Received February 24, 2001
:: Copyright (c) 2001-2018 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, STRUCT_0, ALGSTR_0, VECTSP_1, FUNCSDOM, BINOP_1,
SUBSET_1, FUNCT_1, ZFMISC_1, XBOOLE_0, CARD_1, FUNCOP_1, RELAT_1,
GROUP_1, LATTICES, MESFUNC1, NAT_1, ARYTM_3, SUPINF_2, POLYNOM3,
RLVECT_1, ARYTM_1, ALGSTR_1, FINSEQ_1, PARTFUN1, CARD_3, REALSET1,
TARSKI, UNIALG_2, RLSUB_1, SETFAM_1, POLYNOM1, ALGSEQ_1, POLYALG1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS,
XCMPLX_0, REALSET1, STRUCT_0, ALGSTR_0, RELAT_1, FUNCT_1, PARTFUN1,
FUNCT_2, FUNCOP_1, FINSEQ_1, BINOP_1, NAT_D, GROUP_1, RLVECT_1, VFUNCT_1,
VECTSP_1, NORMSP_1, POLYNOM1, ALGSTR_1, ALGSEQ_1, POLYNOM3, POLYNOM5,
VECTSP_4, XXREAL_0;
constructors BINOP_1, REALSET1, RFINSEQ, NAT_D, ALGSTR_1, VECTSP_4, POLYNOM3,
POLYNOM5, REAL_1, RELSET_1, FUNCOP_1, FVSUM_1, VFUNCT_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, XREAL_0, NAT_1, FINSEQ_1,
REALSET1, STRUCT_0, VECTSP_1, FVSUM_1, POLYNOM3, POLYNOM5, BINOM,
ORDINAL1, VFUNCT_1, FUNCT_2, RELAT_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries
definition
let F be 1-sorted;
struct (doubleLoopStr,ModuleStr over F) AlgebraStr over F
(# carrier -> set,
addF, multF -> BinOp of the carrier,
ZeroF, OneF -> Element of the carrier,
lmult -> Function of [:the carrier of F,the carrier:], the carrier #);
end;
registration
let L be non empty doubleLoopStr;
cluster strict non empty for AlgebraStr over L;
end;
definition
let L be non empty doubleLoopStr, A be non empty AlgebraStr over L;
attr A is mix-associative means
:: POLYALG1:def 1
for a being Element of L, x,y being Element of A holds a*(x*y) = (a*x)*y;
end;
registration
let L be non empty doubleLoopStr;
cluster unital distributive vector-distributive scalar-distributive
scalar-associative scalar-unital mix-associative for non empty
AlgebraStr over L;
end;
definition
let L be non empty doubleLoopStr;
mode Algebra of L is unital distributive vector-distributive
scalar-distributive scalar-associative scalar-unital mix-associative
non empty AlgebraStr over L;
end;
theorem :: POLYALG1:1
for X,Y being set for f being Function of [:X,Y:],X holds dom f = [:X,Y:];
theorem :: POLYALG1:2
for X,Y being set for f being Function of [:X,Y:],Y holds dom f = [:X,Y:];
begin :: The Algebra of Formal Power Series
definition
let L be non empty doubleLoopStr;
func Formal-Series L -> strict non empty AlgebraStr over L means
:: POLYALG1:def 2
(for x be set holds x in the carrier of it iff x is sequence of L) &
(for x,y be Element of it, p,q be sequence of L st x = p & y = q holds
x+y = p+q) &
(for x,y be Element of it, p,q be sequence of L st x = p & y = q holds
x*y = p*'q) &
(for a be Element of L, x be Element of it, p be sequence of L st x = p
holds a*x = a*p) & 0.it = 0_.L & 1.it = 1_.L;
end;
registration
let L be Abelian non empty doubleLoopStr;
cluster Formal-Series L -> Abelian;
end;
registration
let L be add-associative non empty doubleLoopStr;
cluster Formal-Series L -> add-associative;
end;
registration
let L be right_zeroed non empty doubleLoopStr;
cluster Formal-Series L -> right_zeroed;
end;
registration
let L be add-associative right_zeroed right_complementable non empty
doubleLoopStr;
cluster Formal-Series L -> right_complementable;
end;
registration
let L be Abelian add-associative right_zeroed commutative non empty
doubleLoopStr;
cluster Formal-Series L -> commutative;
end;
registration
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive non empty doubleLoopStr;
cluster Formal-Series L -> associative;
end;
registration
cluster add-associative associative right_zeroed left_zeroed well-unital
right_complementable distributive for non empty doubleLoopStr;
end;
::$CT 3
registration
let L be right_zeroed add-associative right_complementable distributive
well-unital non empty doubleLoopStr;
cluster Formal-Series L -> well-unital;
end;
registration
let L be Abelian add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr;
cluster Formal-Series L -> right-distributive;
cluster Formal-Series L -> left-distributive;
end;
theorem :: POLYALG1:6
for L be Abelian add-associative right_zeroed
right_complementable distributive non empty doubleLoopStr for a being Element
of L, p,q being sequence of L holds a*(p+q)=a*p + a*q;
theorem :: POLYALG1:7
for L be Abelian add-associative right_zeroed
right_complementable distributive non empty doubleLoopStr for a,b being
Element of L, p being sequence of L holds (a+b)*p = a*p + b*p;
theorem :: POLYALG1:8
for L be associative non empty doubleLoopStr
for a,b being Element of L, p being sequence of L holds (a*b)*p = a*(b*p);
theorem :: POLYALG1:9
for L be associative well-unital non empty doubleLoopStr for p
being sequence of L holds 1.L*p = p;
registration
let L be Abelian add-associative associative right_zeroed
right_complementable well-unital distributive non empty doubleLoopStr;
cluster Formal-Series L -> vector-distributive scalar-distributive
scalar-associative scalar-unital;
end;
theorem :: POLYALG1:10
for L be Abelian left_zeroed add-associative associative
right_zeroed right_complementable distributive non empty doubleLoopStr for a
being Element of L, p,q being sequence of L holds a*(p*'q)=(a*p)*'q;
registration
let L be Abelian left_zeroed add-associative associative right_zeroed
right_complementable distributive non empty doubleLoopStr;
cluster Formal-Series L -> mix-associative;
end;
definition
let L be 1-sorted;
let A be AlgebraStr over L;
mode Subalgebra of A -> AlgebraStr over L means
:: POLYALG1:def 3
the carrier of it c= the carrier of A &
1.it = 1.A & 0.it = 0.A &
the addF of it = (the addF of A)||the carrier of it &
the multF of it = (the multF of A)||the carrier of it &
the lmult of it =
(the lmult of A)|[:the carrier of L,the carrier of it:];
end;
theorem :: POLYALG1:11
for L being 1-sorted for A being AlgebraStr over L holds A is Subalgebra of A
;
theorem :: POLYALG1:12
for L being 1-sorted for A,B,C being AlgebraStr over L st
A is Subalgebra of B & B is Subalgebra of C holds A is Subalgebra of C;
theorem :: POLYALG1:13
for L being 1-sorted for A,B being AlgebraStr over L st
A is Subalgebra of B & B is Subalgebra of A holds
the AlgebraStr of A = the AlgebraStr of B;
theorem :: POLYALG1:14
for L being 1-sorted for A,B being AlgebraStr over L st
the AlgebraStr of A = the AlgebraStr of B holds A is Subalgebra of B;
registration
let L be non empty 1-sorted;
cluster non empty strict for AlgebraStr over L;
end;
registration
let L be 1-sorted;
let B be AlgebraStr over L;
cluster strict for Subalgebra of B;
end;
registration
let L be non empty 1-sorted;
let B be non empty AlgebraStr over L;
cluster strict non empty for Subalgebra of B;
end;
definition
let L be non empty multMagma;
let B be non empty AlgebraStr over L;
let A be Subset of B;
attr A is opers_closed means
:: POLYALG1:def 4
A is linearly-closed & (for x,y being
Element of B st x in A & y in A holds x*y in A) & 1.B in A & 0.B in A;
end;
theorem :: POLYALG1:15
for L being non empty multMagma for B being non empty AlgebraStr
over L for A being non empty Subalgebra of B holds for x,y being Element of B,
x9,y9 being Element of A st x = x9 & y = y9 holds x+y = x9+ y9;
theorem :: POLYALG1:16
for L be non empty multMagma for B be non empty AlgebraStr over
L for A be non empty Subalgebra of B holds for x,y being Element of B, x9,y9
being Element of A st x = x9 & y = y9 holds x*y = x9* y9;
theorem :: POLYALG1:17
for L be non empty multMagma for B be non empty AlgebraStr over
L for A be non empty Subalgebra of B holds for a being Element of L for x being
Element of B, x9 being Element of A st x = x9 holds a * x = a * x9;
theorem :: POLYALG1:18
for L be non empty multMagma for B be non empty AlgebraStr over L for
A be non empty Subalgebra of B ex C being Subset of B st the carrier of A = C &
C is opers_closed;
theorem :: POLYALG1:19
for L be non empty multMagma for B be non empty AlgebraStr over
L for A be Subset of B st A is opers_closed ex C being strict Subalgebra of B
st the carrier of C = A;
theorem :: POLYALG1:20
for L being non empty multMagma for B being non empty AlgebraStr
over L for A being non empty Subset of B for X being Subset-Family of B st (for
Y be set holds Y in X iff Y c= the carrier of B & ex C being Subalgebra of B st
Y = the carrier of C & A c= Y) holds meet X is opers_closed;
definition
let L be non empty multMagma;
let B be non empty AlgebraStr over L;
let A be non empty Subset of B;
func GenAlg A -> strict non empty Subalgebra of B means
:: POLYALG1:def 5
A c= the
carrier of it & for C being Subalgebra of B st A c= the carrier of C holds the
carrier of it c= the carrier of C;
end;
theorem :: POLYALG1:21
for L be non empty multMagma for B be non empty AlgebraStr over
L for A be non empty Subset of B st A is opers_closed holds the carrier of
GenAlg A = A;
begin ::The Algebra of Polynomials
definition
let L be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr;
func Polynom-Algebra L -> strict non empty AlgebraStr over L means
:: POLYALG1:def 6
ex
A being non empty Subset of Formal-Series L st A = the carrier of Polynom-Ring
L & it = GenAlg A;
end;
registration
let L be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr;
cluster Polynom-Ring L -> Loop-like;
end;
theorem :: POLYALG1:22
for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr for A being non empty Subset of
Formal-Series L st A = the carrier of Polynom-Ring L holds A is opers_closed;
theorem :: POLYALG1:23
for L be add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr holds the doubleLoopStr of
Polynom-Algebra L = Polynom-Ring L;
theorem :: POLYALG1:24
for L being add-associative right_zeroed right_complementable
well-unital distributive non empty doubleLoopStr holds 1_Formal-Series L =
1_.L;