The abstract of the Mizar article:

Reper Algebras

by

Michal Muzalewski

Received May 28, 1992

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;
 pred RAS is_semi_additive_in i means
:: 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
 RAS is_semi_additive_in m implies
               for a,d,p,q st q = <:p,m,d:> holds *'(a,<:p,m,a@d:>) = a@*'(a,q)
;

definition let n,i,RAS;
 pred RAS is_additive_in i means
:: 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
       implies RAS is_semi_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
);