Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

### Reper Algebras

by
Michal Muzalewski

MML identifier: MIDSP_3
[ Mizar article, MML identifier index ]

```environ

vocabulary FINSEQ_1, FUNCT_1, ARYTM_1, RELAT_1, BOOLE, FINSEQ_2, MIDSP_1,
BINOP_1, QC_LANG1, PRE_TOPC, ARYTM_3, PARTFUN1, MIDSP_2, VECTSP_1,
GROUP_4, RLVECT_1, MIDSP_3;
notation TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XREAL_0, FUNCT_1, FUNCT_2,
BINOP_1, STRUCT_0, PRE_TOPC, FINSEQ_1, FINSEQ_2, NAT_1, RLVECT_1,
MIDSP_1, MIDSP_2;
constructors BINOP_1, FINSEQ_2, NAT_1, MIDSP_2, XREAL_0, XBOOLE_0;
clusters FINSEQ_2, STRUCT_0, RELSET_1, NAT_1, ZFMISC_1, XBOOLE_0;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;

begin

reserve n,i,j,k,l for Nat;
reserve D for non empty set;
reserve c,d for Element of D;
reserve p,q,q',r for FinSequence of D;

theorem :: MIDSP_3:1
len p = j+1+k implies ex q,r,c st len q = j & len r = k & p = q^<*c*>^r;

theorem :: MIDSP_3:2
i in Seg(n) implies ex j,k st n = j+1+k & i = j+1;

theorem :: MIDSP_3:3
p = q^<*c*>^r & i = len q + 1
implies (for l st 1 <= l & l <= len q holds p.l = q.l)
& p.i = c
& (for l st i + 1 <= l & l <= len p holds p.l = r.(l-i));

theorem :: MIDSP_3:4
l<=j or l=j+1 or j+2<=l;

theorem :: MIDSP_3:5
l in Seg(n)\{i} & i=j+1 implies 1<=l & l<=j or i+1<=l & l<=n;

definition let n,i,D,d;let p be Element of (n+1)-tuples_on D;
assume  i in Seg(n+1);
func sub(p,i,d) -> Element of (n+1)-tuples_on D means
:: MIDSP_3:def 1
it.i = d & for l st l in (dom p)\{i} holds it.l = p.l;
end;

::Section 2: Reper Algebra Structure and its properties
begin

definition let n;
struct(MidStr) ReperAlgebraStr over n
(#carrier -> set,
MIDPOINT -> BinOp of the carrier,
reper -> Function of n-tuples_on the carrier, the carrier#);
end;

definition let n; let A be non empty set, m be BinOp of A,
r be Function of n-tuples_on A,A;
cluster ReperAlgebraStr(#A,m,r#) -> non empty;
end;

definition let n;
cluster non empty ReperAlgebraStr over n;
end;

definition let n;
cluster MidSp-like (non empty ReperAlgebraStr over n+2);
end;

reserve RAS for MidSp-like (non empty ReperAlgebraStr over n+2);
reserve a,b,d,pii,p'i for Point of RAS;

definition let i,D;
mode Tuple of i,D is Element of i-tuples_on D;
end;

definition let n,RAS,i;
mode Tuple of i,RAS is Tuple of i,the carrier of RAS;
end;

reserve p,q for Tuple of (n+1),RAS;

definition let n,RAS,a;
redefine func <*a*> -> Tuple of 1,RAS;
end;

definition let n,RAS,i,j; let p be Tuple of i,RAS, q be Tuple of j,RAS;
redefine func p^q -> Tuple of (i+j),RAS;
end;

theorem :: MIDSP_3:6
<*a*>^p is Tuple of (n+2),RAS;

definition let n,RAS,a,p;
func *'(a,p) -> Point of RAS equals
:: MIDSP_3:def 2
(the reper of RAS).(<*a*>^p);
end;

definition let n,i,RAS,d,p;
func <:p,i,d:> -> Tuple of (n+1),RAS means
:: MIDSP_3:def 3
for D
for p' being Element of (n+1)-tuples_on D
for d' being Element of D
st D = the carrier of RAS & p' = p & d' = d
holds it = sub(p',i,d');
end;

theorem :: MIDSP_3:7
i in Seg(n+1) implies <:p,i,d:>.i = d
& for l st l in (dom p)\{i} holds <:p,i,d:>.l = p.l;

definition let n;
mode Nat of n -> Nat means
:: MIDSP_3:def 4
1<=it & it<=n+1;
end;

reserve m for Nat of n;

theorem :: MIDSP_3:8
i is Nat of n iff i in Seg(n+1);

canceled;

theorem :: MIDSP_3:10
i<=n implies i+1 is Nat of n;

theorem :: MIDSP_3:11
(for m holds p.m = q.m) implies p = q;

theorem :: MIDSP_3:12
(for l being Nat of n st l=i holds <:p,i,d:>.l = d)
& for l,i being Nat of n st l<>i holds <:p,i,d:>.l = p.l;

definition let n,D; let p be Element of (n+1)-tuples_on D; let m;
redefine func p.m -> Element of D;
end;

definition let n,RAS;
attr RAS is being_invariance means
:: MIDSP_3:def 5
for a,b,p,q st (for m holds a@(q.m) = b@(p.m))
holds a@*'(b,q) = b@*'(a,p);
synonym RAS is_invariance;
end;

definition let n,i,RAS;
pred RAS has_property_of_zero_in i means
:: MIDSP_3:def 6
for a,p holds *'(a,<:p,i,a:>) = a;
end;

definition let n,i,RAS;
:: MIDSP_3:def 7
for a,pii,p st p.i = pii holds *'(a,<:p,i,a@pii:>) = a@*'(a,p);
end;

theorem :: MIDSP_3:13
for a,d,p,q st q = <:p,m,d:> holds *'(a,<:p,m,a@d:>) = a@*'(a,q)
;

definition let n,i,RAS;
:: MIDSP_3:def 8
for a,pii,p'i,p st p.i = pii
holds *'(a,<:p,i,pii@p'i:>) = *'(a,p)@*'(a,<:p,i,p'i:>);
end;

definition let n,i,RAS;
pred RAS is_alternative_in i means
:: MIDSP_3:def 9
for a,p,pii st p.i = pii holds *'(a,<:p,i+1,pii:>) = a;
end;

reserve W for ATLAS of RAS;
reserve v for Vector of W;

definition let n,RAS,W,i;
mode Tuple of i,W is Tuple of i,the carrier of the algebra of W;
end;

reserve x,y for Tuple of (n+1),W;

definition
let n,RAS,W,x,i,v;
func <:x,i,v:> -> Tuple of (n+1),W means
:: MIDSP_3:def 10
for D
for x' being Element of (n+1)-tuples_on D
for v' being Element of D
st D = the carrier of the algebra of W & x' = x & v' = v
holds it = sub(x',i,v');
end;

theorem :: MIDSP_3:14
i in Seg(n+1) implies <:x,i,v:>.i = v
& for l st l in (dom x)\{i} holds <:x,i,v:>.l = x.l;

theorem :: MIDSP_3:15
(for l being Nat of n st l=i holds <:x,i,v:>.l = v)
& for l,i being Nat of n st l<>i holds <:x,i,v:>.l = x.l;

theorem :: MIDSP_3:16
(for m holds x.m = y.m) implies x = y;

scheme SeqLambdaD'{n()->Nat,D()->non empty set,F(set)->Element of D()}:
ex z being FinSequence of D() st len z = n()+1 &
for j being Nat of n() holds z.j = F(j);

definition let n,RAS,W,a,x;
func (a,x).W -> Tuple of (n+1),RAS means
:: MIDSP_3:def 11
it.m = (a,x.m).W;
end;

definition let n,RAS,W,a,p;
func W.(a,p) -> Tuple of (n+1),W means
:: MIDSP_3:def 12
it.m = W.(a,p.m);
end;

theorem :: MIDSP_3:17
W.(a,p) = x iff (a,x).W = p;

theorem :: MIDSP_3:18
W.(a,(a,x).W) = x;

theorem :: MIDSP_3:19
(a,W.(a,p)).W = p;

definition let n,RAS,W,a,x;
func Phi(a,x) -> Vector of W equals
:: MIDSP_3:def 13
W.(a,*'(a,(a,x).W));
end;

theorem :: MIDSP_3:20
W.(a,p) = x & W.(a,b) = v implies (*'(a,p) = b iff Phi(a,x) = v);

theorem :: MIDSP_3:21
RAS is_invariance iff for a,b,x holds Phi(a,x) = Phi(b,x);

theorem :: MIDSP_3:22
1 in Seg(n+1);

canceled;

theorem :: MIDSP_3:24
1 is Nat of n;

::Section 3: Reper Algebra and its atlas
begin

definition let n;
mode ReperAlgebra of n -> MidSp-like (non empty ReperAlgebraStr over n+2)
means
:: MIDSP_3:def 14
it is_invariance;
end;

reserve RAS for ReperAlgebra of n;
reserve a,b,pm,p'm,p''m for Point of RAS;
reserve p for Tuple of (n+1),RAS;
reserve W for ATLAS of RAS;
reserve v for Vector of W;
reserve x for Tuple of (n+1),W;

theorem :: MIDSP_3:25
Phi(a,x) = Phi(b,x);

definition let n,RAS,W,x;
func Phi(x) -> Vector of W means
:: MIDSP_3:def 15
for a holds it = Phi(a,x);
end;

theorem :: MIDSP_3:26
W.(a,p) = x & W.(a,b) = v & Phi(x) = v implies *'(a,p) = b;

theorem :: MIDSP_3:27
(a,x).W = p & (a,v).W = b & *'(a,p) = b implies Phi(x) = v;

theorem :: MIDSP_3:28
W.(a,p) = x & W.(a,b) = v implies W.(a,<:p,m,b:>) = <:x,m,v:>;

theorem :: MIDSP_3:29
(a,x).W = p & (a,v).W = b implies (a,<:x,m,v:>).W = <:p,m,b:>;

theorem :: MIDSP_3:30
RAS has_property_of_zero_in m iff for x holds Phi(<:x,m,0.W:>) = 0.W;

theorem :: MIDSP_3:31
RAS is_semi_additive_in m iff for x holds
Phi(<:x,m,Double (x.m):>) = Double Phi(x);

theorem :: MIDSP_3:32
RAS has_property_of_zero_in m & RAS is_additive_in m

theorem :: MIDSP_3:33
RAS has_property_of_zero_in m implies (RAS is_additive_in m
iff for x,v holds Phi(<:x,m,(x.m)+v:>) = Phi(x) + Phi
(<:x,m,v:>));

theorem :: MIDSP_3:34
W.(a,p) = x & m<= n implies W.(a,<:p,m+1,p.m:>) = <:x,m+1,x.m:>;

theorem :: MIDSP_3:35
(a,x).W = p & m<=n implies (a,<:x,m+1,x.m:>).W = <:p,m+1,p.m:>;

theorem :: MIDSP_3:36
m<=n implies (RAS is_alternative_in m iff for x holds Phi(<:x,m+1,x.m:>) = 0.
W
);

```