:: Reper Algebras :: by Micha{\l} Muzalewski :: :: Received May 28, 1992 :: Copyright (c) 1992-2021 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 SUBSET_1, NUMBERS, XBOOLE_0, FINSEQ_1, ARYTM_3, ORDINAL4, XXREAL_0, NAT_1, FUNCT_1, ARYTM_1, RELAT_1, FINSEQ_2, FUNCT_4, MIDSP_1, STRUCT_0, BINOP_1, QC_LANG1, PRE_TOPC, CARD_1, TARSKI, MIDSP_2, VECTSP_1, GROUP_4, SUPINF_2, ROBBINS1, MIDSP_3; notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, FUNCT_1, FUNCT_2, BINOP_1, STRUCT_0, ALGSTR_0, PRE_TOPC, FINSEQ_1, FINSEQ_2, ORDINAL1, NUMBERS, NAT_1, FUNCT_7, MIDSP_1, MIDSP_2, XXREAL_0; constructors BINOP_1, NAT_1, FINSEQ_2, FUNCT_7, MIDSP_2, RELSET_1; registrations RELSET_1, XREAL_0, NAT_1, FINSEQ_2, STRUCT_0, ORDINAL1; 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,q9,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 D,n; let p be Element of n-tuples_on D; let i,d; redefine func p+*(i,d) -> Element of n-tuples_on D; 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; registration 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; registration let n; cluster non empty for ReperAlgebraStr over n; end; registration let n; cluster MidSp-like for non empty ReperAlgebraStr over n+2; end; reserve RAS for MidSp-like non empty ReperAlgebraStr over n+2; reserve a,b,d,pii,p9i for Point of RAS; definition let n,RAS,i; mode Tuple of i,RAS is Element of i-tuples_on 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; definition let n,RAS,a,p; func *'(a,p) -> Point of RAS equals :: MIDSP_3:def 1 (the reper of RAS).(<*a*>^p); end; theorem :: MIDSP_3:6 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 2 1<=it & it<=n+1; end; reserve m for Nat of n; theorem :: MIDSP_3:7 i is Nat of n iff i in Seg(n+1); theorem :: MIDSP_3:8 i<=n implies i+1 is Nat of n; theorem :: MIDSP_3:9 (for m holds p.m = q.m) implies p = q; theorem :: MIDSP_3:10 for l being Nat of n st l=i holds (p+*(i,d)).l = d; 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 3 for a,b,p,q st (for m holds a@(q.m ) = b@(p.m)) holds a@*'(b,q) = b@*'(a,p); end; definition let n,RAS,p,i,a; redefine func p+*(i,a) -> Tuple of (n+1),RAS; end; definition let n,i,RAS; pred RAS has_property_of_zero_in i means :: MIDSP_3:def 4 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 5 for a,pii,p st p.i = pii holds *'(a,(p+*(i,a@pii))) = a@*'(a,p); end; theorem :: MIDSP_3:11 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 6 for a,pii,p9i,p st p.i = pii holds *' (a,(p+*(i,pii@p9i))) = *'(a,p)@*'(a,(p+*(i,p9i))); end; definition let n,i,RAS; pred RAS is_alternative_in i means :: MIDSP_3:def 7 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 Element of i-tuples_on the carrier of the algebra of W; end; reserve x,y for Tuple of (n+1),W; theorem :: MIDSP_3:12 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:13 (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:14 (for m holds x.m = y.m) implies x = y; scheme :: MIDSP_3:sch 1 SeqLambdaD9{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 8 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 9 it.m = W.(a,p.m); end; theorem :: MIDSP_3:15 W.(a,p) = x iff (a,x).W = p; theorem :: MIDSP_3:16 W.(a,(a,x).W) = x; theorem :: MIDSP_3:17 (a,W.(a,p)).W = p; definition let n,RAS,W,a,x; func Phi(a,x) -> Vector of W equals :: MIDSP_3:def 10 W.(a,*'(a,(a,x).W)); end; theorem :: MIDSP_3:18 W.(a,p) = x & W.(a,b) = v implies (*'(a,p) = b iff Phi(a,x) = v); theorem :: MIDSP_3:19 RAS is being_invariance iff for a,b,x holds Phi(a,x) = Phi(b,x); theorem :: MIDSP_3:20 1 in Seg(n+1); theorem :: MIDSP_3:21 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 11 it is being_invariance; end; reserve RAS for ReperAlgebra of n; reserve a,b,pm,p9m,p99m 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:22 Phi(a,x) = Phi(b,x); definition let n,RAS,W,x; func Phi(x) -> Vector of W means :: MIDSP_3:def 12 for a holds it = Phi(a,x); end; theorem :: MIDSP_3:23 W.(a,p) = x & W.(a,b) = v & Phi(x) = v implies *'(a,p) = b; theorem :: MIDSP_3:24 (a,x).W = p & (a,v).W = b & *'(a,p) = b implies Phi(x) = v; theorem :: MIDSP_3:25 W.(a,p) = x & W.(a,b) = v implies W.(a,(p+*(m,b))) = (x+*(m,v)); theorem :: MIDSP_3:26 (a,x).W = p & (a,v).W = b implies (a,(x+*(m,v))).W = (p+*(m,b)); theorem :: MIDSP_3:27 RAS has_property_of_zero_in m iff for x holds Phi((x+*(m,0.W))) = 0.W; theorem :: MIDSP_3:28 RAS is_semi_additive_in m iff for x holds Phi((x+*(m,Double(x.m) ))) = Double Phi(x); theorem :: MIDSP_3:29 RAS has_property_of_zero_in m & RAS is_additive_in m implies RAS is_semi_additive_in m; theorem :: MIDSP_3:30 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:31 W.(a,p) = x & m<= n implies W.(a,(p+*(m+1,p.m))) = (x+*(m+1,x.m) ); theorem :: MIDSP_3:32 (a,x).W = p & m<=n implies (a,(x+*(m+1,x.m))).W = (p+*(m+1,p.m)); theorem :: MIDSP_3:33 m<=n implies (RAS is_alternative_in m iff for x holds Phi((x+*(m+1,x.m ))) = 0. W );