:: 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 Association of Mizar Users

environ

 vocabularies BOOLE, NORMSP_1, FUNCT_1, RLVECT_1, RELAT_1, FINSEQ_1, ALGSEQ_1,
      FUNCOP_1, NAT_1, GR_CY_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, NAT_1, RELAT_1, FUNCT_1,
      CARD_1, FUNCOP_1, STRUCT_0, FUNCT_2, XXREAL_0;
 constructors FUNCOP_1, XXREAL_0, XREAL_0, NAT_1, RLVECT_1;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, ARYTM_3, XREAL_0,
      STRUCT_0;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, XBOOLE_0, CARD_1;
 theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, REAL_1, NAT_1, FUNCOP_1, XREAL_1,
      XXREAL_0, CARD_1;
 schemes FUNCT_2, NAT_1;

begin

 reserve i,k,l,m,n for Element of NAT,
         x for set;

canceled 9;

theorem
   k in Segm n iff k < n by CARD_1:98;

theorem
   Segm 0 = {} & Segm 1 = { 0 } & Segm 2 = { 0,1 }
                 by CARD_1:87,88;

theorem
   n in Segm(n+1) by CARD_1:99;

theorem
   n <= m iff Segm n c= Segm m by CARD_1:100;

theorem
   Segm n = Segm m implies n = m;

theorem
   k <= n implies
    Segm k = Segm k /\ Segm n & Segm k = Segm n /\ Segm k by CARD_1:101;

theorem
   (Segm k = Segm k /\ Segm n or Segm k = Segm n /\ Segm k)
    implies k <= n by CARD_1:101;

canceled;

::
::    Algebraic Sequences
::

reserve R for non empty ZeroStr;

definition let R;
 canceled;
  let F be sequence of R;
  attr F is finite-Support means :Def2:
    ex n st for i st i >= n holds F.i = 0.R;
end;

registration let R;
  cluster finite-Support sequence of R;
  existence
  proof
   set f = NAT --> 0.R;
   reconsider f as Function of NAT,the carrier of R by FUNCOP_1:57;
   take f, 0;
   thus thesis by FUNCOP_1:13;
  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,k;
  pred k is_at_least_length_of p means :Def3:
  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 Def2;
      take n;
      thus thesis by A1,Def3;
    end;

Lm2:
  ex k st k is_at_least_length_of p
     & (for n st n is_at_least_length_of p holds k<=n)
    proof
      defpred P[Element of NAT] means $1 is_at_least_length_of p;
      A1:ex m 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;
    end;

Lm3:
  (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)
  implies k=l
     proof
       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 k=l by XXREAL_0:1;
     end;

definition let R,p;
  func len p -> Element of NAT means :Def4:
   it is_at_least_length_of p
    & for m st m is_at_least_length_of p holds it<=m;
  existence by Lm2;
  uniqueness by Lm3;
end;

canceled 4;

theorem
Th22: i>=len p implies p.i=0.R
 proof
  assume A1:i>=len p;
      len p is_at_least_length_of p by Def4;
  hence thesis by A1,Def3;
 end;

canceled;

theorem Th24:
  (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 Th22;
    end;
    hence thesis;
  end;

theorem Th25:
  len p=k+1 implies p.k<>0.R
  proof
    assume A1:len p=k+1;
    then k<len p by XREAL_1:31;
    then not k is_at_least_length_of p by Def4;
    then consider i such that A2:i>=k & p.i<>0.R by Def3;
     i<k+1 by A1,A2,Th22;
    then i<=k by NAT_1:13;
    hence thesis by A2,XXREAL_0:1;
  end;

::
:: SUPPORT
::

definition let R,p;
  func support p -> Subset of NAT equals
    Segm len p;
  coherence;
end;

canceled;

theorem
   k = len p iff Segm k = support p;

 scheme AlgSeqLambdaF{R()->non empty ZeroStr,A()->Element of NAT,
                      F(Element of 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[Element of 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 Function of NAT,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 Function of NAT,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
       take A();
       thus thesis by A2;
     end;
   then reconsider f as AlgSequence of R() by Def2;
   A3:len f <= A()
     proof
        for i st i>=A() holds f.i=0.R() by A2;
       then A() is_at_least_length_of f by Def3;
       hence thesis by Def4;
     end;
   take f;
   thus thesis by A2,A3;
 end;

theorem Th28:
  len p = len q & (for k st k < len p holds p.k = q.k) implies p=q
proof
  assume A1: len p = len q & (for k st k < len p holds p.k = q.k);
  A2: dom p = NAT & dom q = NAT by FUNCT_2:def 1;
      for x st x in NAT holds p.x=q.x
     proof let x;
        assume x in NAT;
        then reconsider k=x as Element of NAT;
          p.k=q.k
         proof
            k >= len p implies p.k = q.k
           proof
            assume k >= len p;
            then p.k = 0.R & q.k = 0.R by A1,Th22;
            hence thesis;
           end;
          hence thesis by A1;
         end;
        hence p.x=q.x;
     end;
  hence thesis by A2,FUNCT_1:9;
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 A1:D <> {0.R};
    let k;
    consider t being set such that A2: t in D & t <> 0.R by A1,ZFMISC_1:41;
    reconsider y=t as Element of R by A2;
    deffunc F(Element of 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 Th24;
    then len p = k by A3,XXREAL_0:1;
  hence thesis;
end;

::
::      The SHORT AlgSequence of R
::

reserve x for Element of R;

definition let R,x;
  func <%x%> -> AlgSequence of R means
:Def6:  len it <= 1 & it.0 = x;
   existence
    proof
      deffunc F(Element of 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 & p.0 = x and
      A3: len q <= 1 & q.0 = x;
      A4:1 = 0 + 1;
      A5:now assume x=0.R;
        then len p <>1 & len q<>1 by A2,A3,A4,Th25;
        then len p<1 & len q<1 by A2,A3,REAL_1:def 5;
        then len p=0 & len q=0 by NAT_1:14;
        hence len p=len q;
      end;
A6:      now assume x<>0.R;
        then len p>0 & len q>0 by A2,A3,Th22;
        then len p=1 & len q=1 by A2,A3,A4,NAT_1:8;
        hence len p=len q;
      end;
          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 A2,A3;
        end;
      hence thesis by A5,A6,Th28;
   end;
end;

Lm4:
  p=<%0.R%> implies len p = 0
    proof
      A1:0+1=1;
      assume p=<%0.R%>;
      then len p<=1 & p.0=0.R by Def6;
      then len p<=1 & len p<>1 by A1,Th25;
      then len p<1 by REAL_1:def 5;
      hence thesis by NAT_1:14;
    end;

canceled;

theorem Th31:
  p=<%0.R%> iff len p = 0
    proof
      thus p=<%0.R%> implies len p = 0 by Lm4;
      thus len p=0 implies p=<%0.R%>
      proof
        assume A1:len p=0;
        then A2:len p=len <%0.R%> by Lm4;
         for k st k < len p holds p.k = <%0.R%>.k by A1,NAT_1:2;
        hence thesis by A2,Th28;
      end;
    end;

theorem
   p=<%0.R%> iff support p = {} by Th31;

theorem Th33:
  <%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 Th31;
      hence p0.i=0.R by Th22;
    end;
    hence thesis by Def6;
  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 set;
          assume x in rng p;
          then consider i being set such that A2:i in dom p & x = p.i by
FUNCT_1:def 5;
          reconsider i as Element of NAT by A2,FUNCT_2:def 1;
              p.i=0.R by A1,Th33;
          hence x in {0.R} by A2,TARSKI:def 1;
      end;
      thus {0.R} c= rng p
        proof
          let x be set;
          assume x in {0.R};
          then x = 0.R by TARSKI:def 1;
          then A3: p.0 = x by A1,Def6;
              dom p = NAT by FUNCT_2:def 1;
          hence x in rng p by A3,FUNCT_1:def 5;
        end;
      end;
  thus rng p={0.R} implies p=<%0.R%>
    proof
      assume A4: rng p={0.R};
         len p=0
        proof
           for k st k>=0 holds p.k=0.R
          proof
            let k;   k in NAT;
            then k in dom p by FUNCT_2:def 1;
            then p.k in rng p by FUNCT_1:def 5;
            hence thesis by A4,TARSKI:def 1;
          end;
          then A5:0 is_at_least_length_of p by Def3;
           for m st m is_at_least_length_of p holds 0<=m by NAT_1:2;
          hence thesis by A5,Def4;
        end;
      hence p=<%0.R%> by Th31;
    end;
end;