:: Construction of Finite Sequences over Ring and Left-, Right-,
:: and Bi-Modules over a Ring
:: by Micha{\l} Muzalewski and Les{\l}aw W. Szczerba
::
:: Received September 13, 1990
:: Copyright (c) 1990-2016 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, NAT_1, CARD_1, ARYTM_3, XBOOLE_0, XXREAL_0, TARSKI,
STRUCT_0, FUNCT_1, SUPINF_2, FUNCOP_1, SUBSET_1, FINSEQ_1, RELAT_1,
AFINSQ_1, ALGSEQ_1, POLYNOM1, FINSET_1;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, FINSET_1, ORDINAL1, NUMBERS,
MEMBERED, XCMPLX_0, NAT_1, XXREAL_2, RELAT_1, FUNCT_1, FUNCOP_1,
STRUCT_0, FUNCT_2, XXREAL_0, POLYNOM1;
constructors FUNCOP_1, XXREAL_0, XREAL_0, NAT_1, RLVECT_1, RELSET_1, POLYNOM1,
XXREAL_2;
registrations ORDINAL1, RELSET_1, XREAL_0, STRUCT_0, FINSET_1, CARD_1,
XXREAL_2, MEMBERED;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0, POLYNOM1;
equalities XBOOLE_0;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, NAT_1, FUNCOP_1, XREAL_1,
XXREAL_0, ORDINAL1, POLYNOM1, XXREAL_2;
schemes FUNCT_2, NAT_1;
begin
reserve i,k,l,m,n for Nat,
x for set;
::
:: Algebraic Sequences
::
reserve R for non empty ZeroStr;
definition
let R;
let F be sequence of R;
redefine attr F is finite-Support means
:Def1:
ex n st for i st i >= n holds F.i = 0. R;
compatibility
proof
thus F is finite-Support implies
ex n st for i st i >= n holds F.i = 0. R
proof assume
A1: Support F is finite;
per cases;
suppose
A2: Support F = {};
take 0; let i;
assume i >= 0;
assume
A3: F.i <> 0. R;
reconsider i as Element of NAT by ORDINAL1:def 12;
i in Support F by A3,POLYNOM1:def 4;
hence contradiction by A2;
end;
suppose Support F <> {};
then reconsider A = Support F as non empty finite Subset of NAT by A1;
take n = max A + 1;
let i;
assume i >= n;
then
A4: i > max A by NAT_1:13;
assume
A5: F.i <> 0. R;
reconsider i as Element of NAT by ORDINAL1:def 12;
i in Support F by A5,POLYNOM1:def 4;
hence contradiction by A4,XXREAL_2:def 8;
end;
end;
given n such that
A6: for i st i >= n holds F.i = 0. R;
Support F c= Segm n
proof let e be object;
assume
A7: e in Support F;
then reconsider i = e as Nat;
F.i <> 0.R by A7,POLYNOM1:def 3;
hence e in Segm n by A6,NAT_1:44;
end;
hence Support F is finite;
end;
end;
registration
let R;
cluster finite-Support for sequence of R;
existence
proof
reconsider f = NAT --> 0.R as sequence of the carrier of R;
take f, 0;
let i;
thus thesis by FUNCOP_1:7,ORDINAL1:def 12;
end;
end;
definition
let R;
mode AlgSequence of R is finite-Support sequence of R;
end;
reserve p,q for AlgSequence of R;
definition
let R,p;
let k be Nat;
pred k is_at_least_length_of p means
:Def2:
for i st i>=k holds p.i=0.R;
end;
Lm1: ex m st m is_at_least_length_of p
proof
consider n such that
A1: for i st i >= n holds p.i = 0.R by Def1;
take n;
thus thesis by A1;
end;
definition
let R,p;
func len p -> Element of NAT means
:Def3:
it is_at_least_length_of p & for m st m is_at_least_length_of p holds it<=m;
existence
proof
defpred P[Nat] means $1 is_at_least_length_of p;
A1: ex m being Nat st P[m] by Lm1;
ex k st P[k] & for n st P[n] holds k<=n from NAT_1:sch 5(A1);
then consider k such that
A2: k is_at_least_length_of p & for n st n is_at_least_length_of p holds k<=n;
take k;
thus thesis by A2,ORDINAL1:def 12;
end;
uniqueness
proof let k,l be Element of NAT;
assume k is_at_least_length_of p & ( for m st m is_at_least_length_of p
holds k<= m) & l is_at_least_length_of p & for m st m is_at_least_length_of p
holds l <=m;
then k<=l & l<=k;
hence thesis by XXREAL_0:1;
end;
end;
::$CT 7
theorem Th1:
i>=len p implies p.i=0.R
proof
assume
A1: i>=len p;
len p is_at_least_length_of p by Def3;
hence thesis by A1;
end;
theorem Th2:
(for i st i < k holds p.i<>0.R) implies len p>=k
proof
assume
A1: for i st i < k holds p.i<>0.R;
for i st ii
proof
let i;
assume i0.R by A1;
hence thesis by Th1;
end;
hence thesis;
end;
theorem Th3:
len p=k+1 implies p.k<>0.R
proof
assume
A1: len p=k+1;
then k=k and
A3: p.i<>0.R;
inon empty ZeroStr,A()->Nat, F(Nat)->Element of R()}: ex p
being AlgSequence of R() st len p <= A() & for k st k < A() holds p.k=F(k)
proof
defpred P[Nat, Element of R()] means $1=A() & $2=0.R();
A1: for x being Element of NAT ex y being Element of R() st P[x,y]
proof
let x be Element of NAT;
x =A()&f.x=0.R();
ex n st for i st i >= n holds f.i = 0.R()
proof
reconsider n=A() as Element of NAT by ORDINAL1:def 12;
take n;
let i;
i in NAT by ORDINAL1:def 12;
hence thesis by A2;
end;
then reconsider f as AlgSequence of R() by Def1;
take f;
now
let i;
assume
A3: i>=A();
i in NAT by ORDINAL1:def 12;
hence f.i=0.R() by A2,A3;
end;
then A() is_at_least_length_of f;
hence len f <= A() by Def3;
let k;
k in NAT by ORDINAL1:def 12;
hence thesis by A2;
end;
::$CT
theorem Th4:
len p = len q & (for k st k < len p holds p.k = q.k) implies p=q
proof
assume that
A1: len p = len q and
A2: for k st k < len p holds p.k = q.k;
A3: for x being object st x in NAT holds p.x=q.x
proof
let x be object;
assume x in NAT;
then reconsider k=x as Element of NAT;
k >= len p implies p.k = q.k
proof
assume
A4: k >= len p;
then p.k = 0.R by Th1;
hence thesis by A1,A4,Th1;
end;
hence thesis by A2;
end;
dom p = NAT & dom q = NAT by FUNCT_2:def 1;
hence thesis by A3,FUNCT_1:2;
end;
theorem
the carrier of R <> {0.R} implies for k ex p being AlgSequence of R st
len p = k
proof
set D = the carrier of R;
assume D <> {0.R};
then consider t being object such that
A1: t in D and
A2: t <> 0.R by ZFMISC_1:35;
reconsider y=t as Element of R by A1;
let k;
deffunc F(Nat) = y;
consider p being AlgSequence of R such that
A3: len p <= k & for i st i < k holds p.i=F(i) from AlgSeqLambdaF;
for i st i < k holds p.i<>0.R by A2,A3;
then len p >= k by Th2;
hence thesis by A3,XXREAL_0:1;
end;
::
:: The Short AlgSequence of R
::
reserve x for Element of R;
definition
::$CD
let R,x;
func <%x%> -> AlgSequence of R means
:Def4:
len it <= 1 & it.0 = x;
existence
proof
deffunc F(Nat) = x;
consider p such that
A1: len p <= 1 & for k st k < 1 holds p.k=F(k) from AlgSeqLambdaF;
take p;
thus thesis by A1;
end;
uniqueness
proof
let p,q such that
A2: len p <= 1 and
A3: p.0 = x and
A4: len q <= 1 and
A5: q.0 = x;
A6: 1 = 0 + 1;
A7: now
assume
A8: x=0.R;
then len p<1 by A2,A3,A6,Th3,XXREAL_0:1;
then
A9: len p=0 by NAT_1:14;
len q<1 by A4,A5,A6,A8,Th3,XXREAL_0:1;
hence len p=len q by A9,NAT_1:14;
end;
A10: for k st k < len p holds p.k = q.k
proof
let k;
assume k0.R;
then len p=1 by A2,A3,A6,Th1,NAT_1:8;
hence len p=len q by A4,A5,A6,A11,Th1,NAT_1:8;
end;
hence thesis by A7,A10,Th4;
end;
end;
Lm2: p=<%0.R%> implies len p = 0
proof
assume p=<%0.R%>;
then
A1: p.0=0.R & len p<=1 by Def4;
0+1=1;
then len p<1 by A1,Th3,XXREAL_0:1;
hence thesis by NAT_1:14;
end;
theorem Th6:
p=<%0.R%> iff len p = 0
proof
thus p=<%0.R%> implies len p = 0 by Lm2;
thus len p=0 implies p=<%0.R%>
proof
assume len p=0;
then len p=len <%0.R%> & for k st k < len p holds p.k = <%0.R%>.k
by Lm2,NAT_1:2;
hence thesis by Th4;
end;
end;
::$CT
theorem Th7:
<%0.R%>.i=0.R
proof
set p0=<%0.R%>;
now
assume i<>0;
then i>0 by NAT_1:3;
then i>=len p0 by Th6;
hence thesis by Th1;
end;
hence thesis by Def4;
end;
theorem
p=<%0.R%> iff rng p = {0.R}
proof
thus p=<%0.R%> implies rng p= {0.R}
proof
assume
A1: p=<%0.R%>;
thus rng p c= {0.R}
proof
let x be object;
assume x in rng p;
then consider i being object such that
A2: i in dom p and
A3: x = p.i by FUNCT_1:def 3;
reconsider i as Element of NAT by A2,FUNCT_2:def 1;
p.i=0.R by A1,Th7;
hence thesis by A3,TARSKI:def 1;
end;
thus {0.R} c= rng p
proof
let x be object;
assume x in {0.R};
then x = 0.R by TARSKI:def 1;
then
A4: p.0 = x by A1,Def4;
dom p = NAT by FUNCT_2:def 1;
hence thesis by A4,FUNCT_1:def 3;
end;
end;
thus rng p={0.R} implies p=<%0.R%>
proof
assume
A5: rng p={0.R};
A6: for k st k>=0 holds p.k=0.R
proof
let k;
k in NAT by ORDINAL1:def 12;
then k in dom p by FUNCT_2:def 1;
then p.k in rng p by FUNCT_1:def 3;
hence thesis by A5,TARSKI:def 1;
end;
for m st m is_at_least_length_of p holds 0<=m by NAT_1:2;
then len p=0 by A6,Def2,Def3;
hence thesis by Th6;
end;
end;