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

begin

theorem :: ALGSEQ_1:1

canceled;

theorem :: ALGSEQ_1:2

canceled;

theorem :: ALGSEQ_1:3

canceled;

theorem :: ALGSEQ_1:4

canceled;

theorem :: ALGSEQ_1:5

canceled;

theorem :: ALGSEQ_1:6

canceled;

theorem :: ALGSEQ_1:7

canceled;

theorem :: ALGSEQ_1:8

canceled;

theorem :: ALGSEQ_1:9

canceled;

theorem :: ALGSEQ_1:10

for k, n being Nat holds
( k in Segm n iff k < n ) by NAT_1:45;

theorem :: ALGSEQ_1:11

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

theorem :: ALGSEQ_1:12

for n being Nat holds n in Segm (n + 1) by NAT_1:46;

theorem :: ALGSEQ_1:13

for n, m being Nat holds
( n <= m iff Segm n c= Segm m ) by NAT_1:40;

theorem :: ALGSEQ_1:14

for n, m being Nat st Segm n = Segm m holds
n = m ;

theorem :: ALGSEQ_1:15

for k, n being Nat st k <= n holds
( Segm k = (Segm k) /\ (Segm n) & Segm k = (Segm n) /\ (Segm k) ) by NAT_1:47;

theorem :: ALGSEQ_1:16

for k, n being Nat st ( Segm k = (Segm k) /\ (Segm n) or Segm k = (Segm n) /\ (Segm k) ) holds
k <= n by NAT_1:47;

theorem :: ALGSEQ_1:17

canceled;

definition

let R be non empty ZeroStr ;
canceled;
let F be sequence of R;
attr F is finite-Support means :Def2: :: ALGSEQ_1:def 2
ex n being Nat st
for i being Nat st i >= n holds
F . i = 0. R;

end;

:: deftheorem ALGSEQ_1:def 1 :
canceled;

:: deftheorem Def2 defines finite-Support ALGSEQ_1:def 2 :
for R being non empty ZeroStr
for F being sequence of R holds
( F is finite-Support iff ex n being Nat st
for i being Nat st i >= n holds
F . i = 0. R );

registration

let R be non empty ZeroStr ;
cluster Relation-like NAT -defined the carrier of R -valued Function-like V15( NAT , the carrier of R) finite-Support Element of K21(K22(NAT, the carrier of R));
existence
ex b₁ being sequence of R st b₁ is finite-Support

proof end;

end;

definition

let R be non empty ZeroStr ;
mode AlgSequence of R is finite-Support sequence of R;

end;

definition

let R be non empty ZeroStr ;
let p be AlgSequence of R;
let k be Nat;
pred k is_at_least_length_of p means :Def3: :: ALGSEQ_1:def 3
for i being Nat st i >= k holds
p . i = 0. R;

end;

:: deftheorem Def3 defines is_at_least_length_of ALGSEQ_1:def 3 :
for R being non empty ZeroStr
for p being AlgSequence of R
for k being Nat holds
( k is_at_least_length_of p iff for i being Nat st i >= k holds
p . i = 0. R );

Lm1: for R being non empty ZeroStr
for p being AlgSequence of R ex m being Nat st m is_at_least_length_of p

proof end;

Lm2: for R being non empty ZeroStr
for p being AlgSequence of R ex k being Element of NAT st
( k is_at_least_length_of p & ( for n being Nat st n is_at_least_length_of p holds
k <= n ) )

proof end;

Lm3: for k, l being Nat
for R being non empty ZeroStr
for p being AlgSequence of R st k is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
k <= m ) & l is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
l <= m ) holds
k = l

proof end;

definition

let R be non empty ZeroStr ;
let p be AlgSequence of R;
func len p -> Element of NAT means :Def4: :: ALGSEQ_1:def 4
( it is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
it <= m ) );
existence
ex b₁ being Element of NAT st
( b₁ is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
b₁ <= m ) ) by Lm2;
uniqueness
for b₁, b₂ being Element of NAT st b₁ is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
b₁ <= m ) & b₂ is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
b₂ <= m ) holds
b₁ = b₂ by Lm3;

end;

:: deftheorem Def4 defines len ALGSEQ_1:def 4 :
for R being non empty ZeroStr
for p being AlgSequence of R
for b₃ being Element of NAT holds
( b₃ = len p iff ( b₃ is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
b₃ <= m ) ) );

theorem :: ALGSEQ_1:18

canceled;

theorem :: ALGSEQ_1:19

canceled;

theorem :: ALGSEQ_1:20

canceled;

theorem :: ALGSEQ_1:21

canceled;

theorem Th22: :: ALGSEQ_1:22

for i being Nat
for R being non empty ZeroStr
for p being AlgSequence of R st i >= len p holds
p . i = 0. R

proof end;

theorem :: ALGSEQ_1:23

canceled;

theorem Th24: :: ALGSEQ_1:24

for k being Nat
for R being non empty ZeroStr
for p being AlgSequence of R st ( for i being Nat st i < k holds
p . i <> 0. R ) holds
len p >= k

proof end;

theorem Th25: :: ALGSEQ_1:25

for k being Nat
for R being non empty ZeroStr
for p being AlgSequence of R st len p = k + 1 holds
p . k <> 0. R

proof end;

definition

let R be non empty ZeroStr ;
let p be AlgSequence of R;
func support p -> Subset of NAT equals :: ALGSEQ_1:def 5
Segm (len p);
coherence
Segm (len p) is Subset of NAT ;

end;

:: deftheorem defines support ALGSEQ_1:def 5 :
for R being non empty ZeroStr
for p being AlgSequence of R holds support p = Segm (len p);

theorem :: ALGSEQ_1:26

canceled;

theorem :: ALGSEQ_1:27

for k being Nat
for R being non empty ZeroStr
for p being AlgSequence of R holds
( k = len p iff Segm k = support p ) ;

scheme :: ALGSEQ_1:sch 1
AlgSeqLambdaF{ F₁() -> non empty ZeroStr , F₂() -> Nat, F₃( Nat) -> Element of F₁() } :

ex p being AlgSequence of F₁() st
( len p <= F₂() & ( for k being Nat st k < F₂() holds
p . k = F₃(k) ) )

proof end;

theorem Th28: :: ALGSEQ_1:28

for R being non empty ZeroStr
for p, q being AlgSequence of R st len p = len q & ( for k being Nat st k < len p holds
p . k = q . k ) holds
p = q

proof end;

theorem :: ALGSEQ_1:29

for R being non empty ZeroStr st the carrier of R <> {(0. R)} holds
for k being Nat ex p being AlgSequence of R st len p = k

proof end;

definition

let R be non empty ZeroStr ;
let x be Element of R;
func <%x%> -> AlgSequence of R means :Def6: :: ALGSEQ_1:def 6
( len it <= 1 & it . 0 = x );
existence
ex b₁ being AlgSequence of R st
( len b₁ <= 1 & b₁ . 0 = x )

proof end;

uniqueness
for b₁, b₂ being AlgSequence of R st len b₁ <= 1 & b₁ . 0 = x & len b₂ <= 1 & b₂ . 0 = x holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines <% ALGSEQ_1:def 6 :
for R being non empty ZeroStr
for x being Element of R
for b₃ being AlgSequence of R holds
( b₃ = <%x%> iff ( len b₃ <= 1 & b₃ . 0 = x ) );

Lm4: for R being non empty ZeroStr
for p being AlgSequence of R st p = <%(0. R)%> holds
len p = 0

proof end;

theorem :: ALGSEQ_1:30

canceled;

theorem Th31: :: ALGSEQ_1:31

for R being non empty ZeroStr
for p being AlgSequence of R holds
( p = <%(0. R)%> iff len p = 0 )

proof end;

theorem :: ALGSEQ_1:32

for R being non empty ZeroStr
for p being AlgSequence of R holds
( p = <%(0. R)%> iff support p = {} ) by Th31;

theorem Th33: :: ALGSEQ_1:33

for i being Nat
for R being non empty ZeroStr holds <%(0. R)%> . i = 0. R

proof end;

theorem :: ALGSEQ_1:34

for R being non empty ZeroStr
for p being AlgSequence of R holds
( p = <%(0. R)%> iff rng p = {(0. R)} )

proof end;