:: 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-2019 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 i<k holds len p>i
  proof
    let i;
    assume i<k;
    then p.i<>0.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<len p by XREAL_1:29;
  then not k is_at_least_length_of p by Def3;
  then consider i such that
A2: i>=k and
A3: p.i<>0.R;
  i<k+1 by A1,A3,Th1;
  then i<=k by NAT_1:13;
  hence thesis by A2,A3,XXREAL_0:1;
end;

scheme
  AlgSeqLambdaF{R()->non 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=F($1) or $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() implies x < A() & (F(x)) = F(x);
    hence thesis;
  end;
  ex f being sequence of the carrier of R() st for x being Element of
  NAT holds P[x,f.x] from FUNCT_2:sch 3(A1);
  then consider f being sequence of the carrier of R() such that
A2: for x being Element of NAT holds x<A()&f.x=F(x) or 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 k<len p;
      then k<1 by A2,XXREAL_0:2;
      then k=0 by NAT_1:14;
      hence thesis by A3,A5;
    end;
    now
      assume
A11:  x<>0.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;