:: Reper Algebras
:: by Micha{\l} Muzalewski
::
:: Received May 28, 1992
:: Copyright (c) 1992-2026 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;
definitions MIDSP_1;
equalities MIDSP_1;
theorems FINSEQ_1, FINSEQ_2, FUNCT_1, MIDSP_1, MIDSP_2, NAT_1, ZFMISC_1,
FINSEQ_3, XREAL_1, FUNCT_7, XBOOLE_0, TARSKI, ORDINAL1, XXREAL_0, CARD_1;
schemes FINSEQ_2, FUNCT_2;
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
len p = j+1+k implies ex q,r,c st len q = j & len r = k & p = q^<*c*>^ r
proof
assume len p = j+1+k;
then consider q9,r such that
A1: len q9 = j+1 and
A2: len r = k & p = q9^r by FINSEQ_2:23;
consider q,c such that
A3: q9 = q^<*c*> by A1,FINSEQ_2:19;
take q,r,c;
len q9 = len q + 1 by A3,FINSEQ_2:16;
hence thesis by A1,A2,A3;
end;
theorem
i in Seg n implies ex j,k st n = j+1+k & i = j+1
proof
assume
A1: i in Seg(n);
then 1<=i by FINSEQ_1:1;
then consider j being Nat such that
A2: i = 1+j by NAT_1:10;
reconsider j as Element of NAT by ORDINAL1:def 12;
i<=n by A1,FINSEQ_1:1;
then consider k being Nat such that
A3: n = j+1+k by A2,NAT_1:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
take j,k;
thus thesis by A2,A3;
end;
theorem
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)
proof
set q9 = q^<*c*>;
assume that
A1: p = q9^r and
A2: i = len q + 1;
A3: p = q^(<*c*>^r) by A1,FINSEQ_1:32;
thus for l st 1 <= l & l <= len q holds p.l = q.l
proof
let l;
assume 1 <= l & l <= len q;
then l in dom q by FINSEQ_3:25;
hence thesis by A3,FINSEQ_1:def 7;
end;
A4: len q9 = i by A2,FINSEQ_2:16;
i in Seg(i) by A2,FINSEQ_1:3;
then i in dom q9 by A4,FINSEQ_1:def 3;
hence p.i = q9.i by A1,FINSEQ_1:def 7
.= c by A2,FINSEQ_1:42;
len p = len q9 + len r by A1,FINSEQ_1:22;
hence thesis by A1,A4,FINSEQ_1:23;
end;
theorem Th4:
l<=j or l=j+1 or j+2<=l
proof
A1: j+1+1 = j+2;
l<j+1 or l = j+1 or j+1<l by XXREAL_0:1;
hence thesis by A1,NAT_1:13;
end;
theorem
l in Seg(n)\{i} & i=j+1 implies 1<=l & l<=j or i+1<=l & l<=n
proof
assume that
A1: l in Seg(n)\{i} and
A2: i=j+1;
A3: i+1 = j+2 by A2;
l in Seg(n) & l<>i by A1,ZFMISC_1:56;
hence thesis by A2,A3,Th4,FINSEQ_1:1;
end;
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; :: redefines +* (FUNCT_7, definition)
coherence
proof
dom(p+*(i,d)) = dom p by FUNCT_7:30;
then len(p+*(i,d)) = len p by FINSEQ_3:29
.= n by CARD_1:def 7;
hence p+*(i,d) is Element of n-tuples_on D by FINSEQ_2:92;
end;
end;
Lm1: for p being Element of n-tuples_on D st i in Seg n holds p+*(i,d).i = d
proof
let p be Element of n-tuples_on D;
Seg n = dom p by FINSEQ_2:124;
hence thesis by FUNCT_7:31;
end;
Lm2: for p being Element of n-tuples_on D for l st l in (dom p)\{i} holds (p+*
(i,d)).l = p.l
proof
let p being Element of n-tuples_on D;
let l;
assume l in (dom p)\{i};
then not l in {i} by XBOOLE_0:def 5;
then l <> i by TARSKI:def 1;
hence thesis by FUNCT_7:32;
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;
coherence;
end;
Lm3: now
let n;
let M be MidSp;
let R be Function of (n+2)-tuples_on the carrier of M, the carrier of M;
set RA = ReperAlgebraStr (# the carrier of M, the MIDPOINT of M, R #);
thus RA is MidSp-like
proof
let a,b,c,d be Element of RA;
reconsider a9=a,b9=b,c9=c,d9=d as Element of M;
thus a@a = a9@a9 .= a by MIDSP_1:def 3;
consider x9 being Element of M such that
A1: x9@a9 = b9 by MIDSP_1:def 3;
for a,b be Element of RA, a9,b9 be Element of M st a=a9 & b=b9 holds a
@b = a9@b9;
hence a@b = b9@a9 .= b@a;
reconsider x = x9 as Element of RA;
thus (a@b)@(c@d) = (a9@b9)@(c9@d9) .= (a9@c9)@(b9@d9) by MIDSP_1:def 3
.= (a@c)@(b@d);
take x;
thus thesis by A1;
end;
end;
registration
let n;
cluster non empty for ReperAlgebraStr over n;
existence
proof
set A = the non empty set,m = the BinOp of A,r = the Function of n -tuples_on A
,A;
take ReperAlgebraStr(#A,m,r#);
thus thesis;
end;
end;
registration
let n;
cluster MidSp-like for non empty ReperAlgebraStr over n+2;
existence
proof
set M = the MidSp;
set R = the Function of (n+2)-tuples_on the carrier of M, the carrier of M;
take ReperAlgebraStr (# the carrier of M, the MIDPOINT of M, R #);
thus thesis by Lm3;
end;
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; :: redefines <* (FINSEQ_1, definition)
coherence by FINSEQ_2:98;
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; :: redefines ^ (FINSEQ_1, definition)
coherence
proof
reconsider p as Tuple of i,the carrier of RAS;
reconsider q as Tuple of j,the carrier of RAS;
p^q is Tuple of i+j,the carrier of RAS by FINSEQ_2:107;
hence thesis by FINSEQ_2:131;
end;
end;
definition
let n,RAS,a,p;
func *'(a,p) -> Point of RAS equals
(the reper of RAS).(<*a*>^p);
coherence
proof
reconsider p9 = <*a*>^p as Tuple of (n+2),RAS;
(the reper of RAS).p9 is Point of RAS;
hence thesis;
end;
end;
theorem
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 by Lm1,Lm2;
definition
let n;
mode Nat of n -> Nat means
:Def2:
1<=it & it<=n+1;
existence
proof
take 1;
0 <= n by NAT_1:2;
then 0+1 <= n+1 by XREAL_1:7;
hence thesis;
end;
end;
reserve m for Nat of n;
theorem Th7:
i is Nat of n iff i in Seg(n+1)
proof
i is Nat of n iff 1<=i & i<=n+1 by Def2;
hence thesis by FINSEQ_1:1;
end;
theorem Th8:
i<=n implies i+1 is Nat of n
proof
assume i<=n;
then
A1: i+1<=n+1 by XREAL_1:7;
1<=i+1 by NAT_1:11;
hence thesis by A1,Def2;
end;
theorem Th9:
(for m holds p.m = q.m) implies p = q
proof
assume
A1: for m holds p.m = q.m;
for j be Nat st j in Seg(n+1) holds p.j = q.j
proof
let j be Nat;
assume j in Seg(n+1);
then reconsider j as Nat of n by Th7;
p.j = q.j by A1;
hence thesis;
end;
hence thesis by FINSEQ_2:119;
end;
theorem Th10:
for l being Nat of n st l=i holds (p+*(i,d)).l = d
proof
let l be Nat of n such that
A1: l = i;
l in Seg(n+1) by Th7;
hence thesis by A1,Lm1;
end;
definition
let n,D;
let p be Element of (n+1)-tuples_on D;
let m;
redefine func p.m -> Element of D; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider S = Seg(n+1) as non empty set by FINSEQ_1:4;
m in S & len p = n+1 by Th7,CARD_1:def 7;
then m in dom p by FINSEQ_1:def 3;
then rng p c= D & p.m in rng p by FINSEQ_1:def 4,FUNCT_1:def 3;
hence thesis;
end;
end;
definition
let n,RAS;
attr RAS is being_invariance means
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; :: redefines +* (FUNCT_7, definition)
coherence
proof
thus p+*(i,a) is Tuple of (n+1),RAS;
end;
end;
definition
let n,i,RAS;
pred RAS has_property_of_zero_in i means
for a,p holds *'(a,(p+*(i,a) )) = a;
end;
definition
let n,i,RAS;
pred RAS is_semi_additive_in i means
for a,pii,p st p.i = pii holds *'(a,(p+*(i,a@pii))) = a@*'(a,p);
end;
theorem Th11:
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)
proof
assume
A1: RAS is_semi_additive_in m;
let a,d,p,q;
set qq = (q+*(m,a@d));
assume
A2: q = (p+*(m,d));
A3: qq = (p+*(m,a@d))
proof
set pp = (p+*(m,a@d));
for k being Nat of n holds qq.k = pp.k
proof
let k be Nat of n;
now
per cases;
suppose
A4: k = m;
pp.m = a@d by Th10;
hence thesis by A4,Th10;
end;
suppose
A5: k <> m;
hence qq.k = q.k by FUNCT_7:32
.= p.k by A2,A5,FUNCT_7:32
.= pp.k by A5,FUNCT_7:32;
end;
end;
hence thesis;
end;
hence thesis by Th9;
end;
q.m = d by A2,Th10;
hence thesis by A1,A3;
end;
definition
let n,i,RAS;
pred RAS is_additive_in i means
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
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
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 by Lm1,Lm2;
theorem Th13:
(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
proof
thus for l being Nat of n st l=i holds (x+*(i,v)).l = v
proof
let l be Nat of n such that
A1: l = i;
l in Seg(n+1) by Th7;
hence thesis by A1,Lm1;
end;
thus thesis by FUNCT_7:32;
end;
theorem Th14:
(for m holds x.m = y.m) implies x = y
proof
assume
A1: for m holds x.m = y.m;
for j be Nat st j in Seg(n+1) holds x.j = y.j
proof
let j be Nat;
assume j in Seg(n+1);
then reconsider j as Nat of n by Th7;
x.j = y.j by A1;
hence thesis;
end;
hence thesis by FINSEQ_2:119;
end;
scheme
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) proof
reconsider S = Seg(n()+1) as non empty set by FINSEQ_1:4;
consider z being FinSequence of D() such that
A1: len z = n()+1 and
A2: for j be Nat st j in dom z holds z.j = F(j) from FINSEQ_2:sch 1;
take z;
A3: dom z = Seg(n()+1) by A1,FINSEQ_1:def 3;
for j being Nat of n() holds z.j = F(j)
by Th7,A2,A3;
hence thesis by A1;
end;
definition
let n,RAS,W,a,x;
func (a,x).W -> Tuple of (n+1),RAS means
:Def8:
it.m = (a,x.m).W;
existence
proof
deffunc F(Nat of n)=(a,x.$1).W;
consider z being FinSequence of (the carrier of RAS) such that
A1: len z = n+1 and
A2: z.m = F(m) from SeqLambdaD9;
reconsider z as Tuple of (n+1),RAS by A1,FINSEQ_2:92;
take z;
thus thesis by A2;
end;
uniqueness
proof
let p,q such that
A3: for m holds p.m = (a,x.m).W and
A4: for m holds q.m = (a,x.m).W;
for m holds p.m = q.m
proof
let m;
p.m = (a,x.m).W by A3;
hence thesis by A4;
end;
hence thesis by Th9;
end;
end;
definition
let n,RAS,W,a,p;
func W.(a,p) -> Tuple of (n+1),W means
:Def9:
it.m = W.(a,p.m);
existence
proof
deffunc F(Nat of n)=W.(a,p.$1);
consider z being FinSequence of (the carrier of the algebra of W) such
that
A1: len z = n+1 and
A2: z.m = F(m) from SeqLambdaD9;
reconsider z as Tuple of (n+1),W by A1,FINSEQ_2:92;
take z;
thus thesis by A2;
end;
uniqueness
proof
let x,y such that
A3: for m holds x.m = W.(a,p.m) and
A4: for m holds y.m = W.(a,p.m);
for m holds x.m = y.m
proof
let m;
W.(a,p.m) = x.m by A3;
hence thesis by A4;
end;
hence thesis by Th14;
end;
end;
theorem Th15:
W.(a,p) = x iff (a,x).W = p
proof
thus W.(a,p) = x implies (a,x).W = p
proof
assume
A1: W.(a,p) = x;
now
let m;
W.(a,p.m) = x.m by A1,Def9;
hence (a,x.m).W = p.m by MIDSP_2:33;
end;
hence thesis by Def8;
end;
thus (a,x).W = p implies W.(a,p) = x
proof
assume
A2: (a,x).W = p;
now
let m;
(a,x.m).W = p.m by A2,Def8;
hence W.(a,p.m) = x.m by MIDSP_2:33;
end;
hence thesis by Def9;
end;
end;
theorem
W.(a,(a,x).W) = x by Th15;
theorem
(a,W.(a,p)).W = p by Th15;
definition
let n,RAS,W,a,x;
func Phi(a,x) -> Vector of W equals
W.(a,*'(a,(a,x).W));
coherence;
end;
theorem Th18:
W.(a,p) = x & W.(a,b) = v implies (*'(a,p) = b iff Phi(a,x) = v)
proof
assume that
A1: W.(a,p) = x and
A2: W.(a,b) = v;
Phi(a,x) = W.(a,*'(a,p)) by A1,Th15;
hence thesis by A2,MIDSP_2:32;
end;
theorem Th19:
RAS is being_invariance iff for a,b,x holds Phi(a,x) = Phi(b,x)
proof
A1: (for a,b,x holds Phi(a,x) = Phi(b,x)) implies RAS is being_invariance
proof
assume
A2: for a,b,x holds Phi(a,x) = Phi(b,x);
let a,b,p,q;
A3: W.(a,*'(a,(a,W.(a,p)).W)) = Phi(a,W.(a,p)) .= Phi(b,W.(a,p)) by A2
.= W.(b,*'(b,(b,W.(a,p)).W));
assume
A4: for m holds a@(q.m) = b@(p.m);
A5: now
let m;
a@(q.m) = b@(p.m) by A4;
then
A6: W.(a,p.m) = W.(b,q.m) by MIDSP_2:33;
thus W.(a,p).m = W.(a,p.m) by Def9
.= W.(b,q).m by A6,Def9;
end;
W.(a,*'(a,p)) = W.(a,*'(a,(a,W.(a,p)).W)) by Th15
.= W.(b,*'(b,(b,W.(b,q)).W)) by A5,A3,Th14
.= W.(b,*'(b,q)) by Th15;
hence thesis by MIDSP_2:33;
end;
now
assume
A7: RAS is being_invariance;
let a,b,x;
set p = (a,x).W, q = (b,x).W;
A8: W.(a,p) = x by Th15
.= W.(b,q) by Th15;
now
let m;
W.(a,p.m) = W.(a,p).m by Def9
.= W.(b,q.m) by A8,Def9;
hence a@(q.m) = b@(p.m) by MIDSP_2:33;
end;
then a@*'(b,q) = b@*'(a,p) by A7;
hence Phi(a,x) = Phi(b,x) by MIDSP_2:33;
end;
hence thesis by A1;
end;
theorem Th20:
1 in Seg(n+1)
proof
0 <= n by NAT_1:2;
then 0+1 <= n+1 by XREAL_1:7;
hence thesis by FINSEQ_1:1;
end;
theorem Th21:
1 is Nat of n
proof
1 in Seg(n+1) by Th20;
hence thesis by Th7;
end;
::Section 3: Reper Algebra and its atlas
begin
definition
let n;
mode ReperAlgebra of n -> MidSp-like non empty ReperAlgebraStr over n+2
means
:Def11:
it is being_invariance;
existence
proof
reconsider one1 = 1 as Nat of n+1 by Th21;
set M = the MidSp;
set D = the carrier of M, k = (n+1)+1;
set C = k-tuples_on D;
deffunc F(Element of C)=$1.one1;
consider R being Function of C,D such that
A1: for p being Element of C holds R.p = F(p) from FUNCT_2:sch 4;
reconsider R as Function of (n+2)-tuples_on D,D;
reconsider RA = ReperAlgebraStr (# the carrier of M, the MIDPOINT of M, R
#) as MidSp-like non empty ReperAlgebraStr over n+2 by Lm3;
take RA;
for a,b being Point of RA, p,q being Tuple of (n+1),RA st for m holds
a@(q.m) = b@(p.m) holds a@*'(b,q) = b@*'(a,p)
proof
let a,b be Point of RA, p,q be Tuple of (n+1),RA such that
for m holds a@(q.m) = b@(p.m);
A2: *'(a,p) = (<*a*>^p).one1 by A1
.= a by FINSEQ_1:41;
*'(b,q) = (<*b*>^q).one1 by A1
.= b by FINSEQ_1:41;
hence thesis by A2;
end;
hence thesis;
end;
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 Th22:
Phi(a,x) = Phi(b,x)
by Def11,Th19;
definition
let n,RAS,W,x;
func Phi(x) -> Vector of W means
:Def12:
for a holds it = Phi(a,x);
existence
proof
set a = the Point of RAS;
take Phi(a,x);
thus thesis by Th22;
end;
uniqueness
proof
set a = the Point of RAS;
let y,z be Vector of W such that
A1: for a holds y = Phi(a,x) and
A2: for a holds z = Phi(a,x);
y = Phi(a,x) by A1;
hence thesis by A2;
end;
end;
Lm4: W.(a,p) = x implies Phi(x) = W.(a,*'(a,p))
proof
assume
A1: W.(a,p) = x;
thus Phi(x) = Phi(a,x) by Def12
.= W.(a,*'(a,p)) by A1,Th15;
end;
Lm5: (a,x).W = p implies Phi(x) = W.(a,*'(a,p))
proof
assume (a,x).W = p;
then W.(a,p) = x by Th15;
hence thesis by Lm4;
end;
theorem Th23:
W.(a,p) = x & W.(a,b) = v & Phi(x) = v implies *'(a,p) = b
proof
assume
A1: W.(a,p) = x & W.(a,b) = v & Phi(x) = v;
Phi(x) = Phi(a,x) by Def12;
hence thesis by A1,Th18;
end;
theorem Th24:
(a,x).W = p & (a,v).W = b & *'(a,p) = b implies Phi(x) = v
proof
assume (a,x).W = p & (a,v).W = b & *'(a,p) = b;
then Phi(a,x) = v by MIDSP_2:33;
hence thesis by Def12;
end;
theorem Th25:
W.(a,p) = x & W.(a,b) = v implies W.(a,(p+*(m,b))) = (x+*(m,v))
proof
assume that
A1: W.(a,p) = x and
A2: W.(a,b) = v;
set q = (p+*(m,b));
set y = W.(a,q), z = (x+*(m,v));
for k being Nat of n holds y.k = z.k
proof
let k be Nat of n;
now
per cases;
suppose
A3: k = m;
thus y.k = W.(a,q.k) by Def9
.= W.(a,b) by A3,Th10
.= z.k by A2,A3,Th13;
end;
suppose
A4: k <> m;
thus y.k = W.(a,q.k) by Def9
.= W.(a,p.k) by A4,FUNCT_7:32
.= x.k by A1,Def9
.= z.k by A4,FUNCT_7:32;
end;
end;
hence thesis;
end;
hence thesis by Th14;
end;
theorem Th26:
(a,x).W = p & (a,v).W = b implies (a,(x+*(m,v))).W = (p+*(m,b))
proof
assume (a,x).W = p & (a,v).W = b;
then W.(a,p) = x & W.(a,b) = v by Th15,MIDSP_2:33;
then W.(a,(p+*(m,b))) = (x+*(m,v)) by Th25;
hence thesis by Th15;
end;
theorem
RAS has_property_of_zero_in m iff for x holds Phi((x+*(m,0.W))) = 0.W
proof
thus RAS has_property_of_zero_in m implies for x holds Phi((x+*(m,0.W))) =
0.W
proof
set a = the Point of RAS;
assume
A1: RAS has_property_of_zero_in m;
set b = (a,(0.W)).W;
let x;
set p9 = ((a,x).W)+*(m,a);
A2: b = a by MIDSP_2:34;
then
A3: (a,((x+*(m,0.W)))).W = p9 by Th26;
*'(a,p9) = b by A1,A2;
hence thesis by A3,Th24;
end;
thus (for x holds Phi((x+*(m,0.W))) = 0.W) implies RAS
has_property_of_zero_in m
proof
assume
A4: for x holds Phi((x+*(m,0.W))) = 0.W;
for a,p holds *'(a,(p+*(m,a))) = a
proof
let a,p;
set v = W.(a,a);
set x9 = ((W.(a,p))+*(m,0.W));
v = 0.W by MIDSP_2:33;
then W.(a,((p+*(m,a)))) = x9 & Phi(x9) = v by A4,Th25;
hence thesis by Th23;
end;
hence thesis;
end;
end;
theorem Th28:
RAS is_semi_additive_in m iff for x holds Phi((x+*(m,Double(x.m)
))) = Double Phi(x)
proof
thus RAS is_semi_additive_in m implies for x holds Phi((x+*(m,Double(x.m))))
= Double Phi(x)
proof
set a = the Point of RAS;
assume
A1: RAS is_semi_additive_in m;
let x;
set x9 = (x+*(m,Double(x.m)));
set p = (a,x).W, p9 = (a,x9).W;
set q = (p9+*(m,a@(p9.m)));
for i being Nat of n holds p.i = q.i
proof
let i be Nat of n;
now
per cases;
suppose
A2: i = m;
W.(a,p) = x by Th15;
then
A3: W.(a,p.m) = x.m by Def9;
W.(a,p9) = x9 by Th15;
then
A4: W.(a,p9.m) = x9.m by Def9;
x9.m = Double (x.m) by Th13;
then p.m = a@(p9.m) by A3,A4,MIDSP_2:31
.= q.m by Th10;
hence thesis by A2;
end;
suppose
A5: i <> m;
thus p.i = (a,x.i).W by Def8
.= (a,x9.i).W by A5,FUNCT_7:32
.= p9.i by Def8
.= q.i by A5,FUNCT_7:32;
end;
end;
hence thesis;
end;
then p = q by Th9;
then *'(a,p) = a@*'(a,p9) by A1;
then
A6: W.(a,*'(a,p9)) = Double W.(a,*'(a,p)) by MIDSP_2:31;
Phi(x9) = W.(a,*'(a,p9)) by Lm5;
hence thesis by A6,Lm5;
end;
thus (for x holds Phi((x+*(m,Double(x.m)))) = Double Phi(x)) implies RAS
is_semi_additive_in m
proof
assume
A7: for x holds Phi((x+*(m,Double(x.m)))) = Double Phi(x);
let a;
let p9m be Point of RAS, p9 be Tuple of (n+1),RAS such that
A8: p9.m = p9m;
set p = (p9+*(m,a@(p9.m)));
set x = W.(a,p);
set x9 = (x+*(m,Double(x.m)));
W.(a,p9) = x9
proof
set y = W.(a,p9);
for i being Nat of n holds x9.i = y.i
proof
let i be Nat of n;
now
per cases;
suppose
A9: i = m;
A10: W.(a,p.m) = x.m & p.m = a@(p9.m) by Def9,Th10;
x9.m = Double (x.m) & W.(a,p9.m) = y.m by Def9,Th13;
hence thesis by A9,A10,MIDSP_2:31;
end;
suppose
A11: i <> m;
hence x9.i = x.i by FUNCT_7:32
.= W.(a,p.i) by Def9
.= W.(a,p9.i) by A11,FUNCT_7:32
.= y.i by Def9;
end;
end;
hence thesis;
end;
hence thesis by Th14;
end;
then
A12: Phi(x9) = W.(a,*'(a,p9)) by Lm4;
Phi(x) = W.(a,*'(a,p)) by Lm4;
then W.(a,*'(a,p9)) = Double W.(a,*'(a,p)) by A7,A12;
hence thesis by A8,MIDSP_2:31;
end;
end;
theorem Th29:
RAS has_property_of_zero_in m & RAS is_additive_in m implies RAS
is_semi_additive_in m
proof
assume that
A1: RAS has_property_of_zero_in m and
A2: RAS is_additive_in m;
let a,pm,p;
assume p.m = pm;
then *'(a,(p+*(m,a@pm))) = *'(a,p)@*'(a,(p+*(m,a))) by A2
.= a@*'(a,p) by A1;
hence thesis;
end;
Lm6: RAS is_semi_additive_in m implies for a,p9m, p99m,p st a@(p99m) = (p.m)@(
p9m) holds *'(a,(p+*(m,(p.m)@p9m))) = *'(a,p)@*'(a,(p+*(m,p9m))) iff W.(a,*'(a,
(p+*(m,p99m)))) = W.(a,*'(a,p)) + W.(a,*'(a,(p+*(m,p9m))))
proof
assume
A1: RAS is_semi_additive_in m;
let a,p9m, p99m,p;
assume a@(p99m) = (p.m)@(p9m);
then *'(a,(p+*(m,(p.m)@p9m))) = a@*'(a,(p+*(m,p99m))) by A1,Th11;
hence thesis by MIDSP_2:30;
end;
Lm7: (for x,v holds Phi((x+*(m,(x.m)+v))) = Phi(x) + Phi((x+*(m,v)))) implies
RAS is_semi_additive_in m
proof
assume
A1: for x,v holds Phi((x+*(m,(x.m)+v))) = Phi(x) + Phi((x+*(m,v)));
for x holds Phi((x+*(m,Double(x.m)))) = Double Phi(x)
proof
let x;
set v = x.m;
set y = (x+*(m,v));
for k being Nat of n holds y.k = x.k
proof
let k be Nat of n;
now
per cases;
suppose
k = m;
hence thesis by Th13;
end;
suppose
k <> m;
hence thesis by FUNCT_7:32;
end;
end;
hence thesis;
end;
then
A2: y = x by Th14;
thus Phi((x+*(m,Double v))) = Phi((x+*(m,v+v))) by MIDSP_2:def 1
.= Phi(x) + Phi((x+*(m,v))) by A1
.= Double Phi(x) by A2,MIDSP_2:def 1;
end;
hence thesis by Th28;
end;
theorem
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))))
proof
assume
A1: RAS has_property_of_zero_in m;
thus RAS is_additive_in m implies for x,v holds Phi((x+*(m,(x.m)+v))) = Phi(
x) + Phi((x+*(m,v)))
proof
set a = the Point of RAS;
assume
A2: RAS is_additive_in m;
let x,v;
set p = (a,x).W, p9m = (a,v).W;
consider p99m such that
A3: (p99m)@a = (p.m)@(p9m) by MIDSP_1:def 3;
A4: W.(a,p) = x & W.(a,p9m) = v by Th15,MIDSP_2:33;
A5: W.(a,p99m) = W.(a,p.m) + W.(a,p9m) by A3,MIDSP_2:30
.= x.m + v by A4,Def9;
(p+*(m,p99m)) = (a,(x+*(m,(x.m)+v))).W
proof
set pp = (p+*(m,p99m)), xx = (x+*(m,(x.m)+v));
set qq = (a,xx).W;
for i being Nat of n holds pp.i = qq.i
proof
let i be Nat of n;
per cases;
suppose
A6: i = m;
hence pp.i = p99m by Th10
.= (a,(x.m)+v).W by A5,MIDSP_2:33
.= (a,xx.m).W by Th13
.= qq.i by A6,Def8;
end;
suppose
A7: i <> m;
hence pp.i = p.i by FUNCT_7:32
.= (a,x.i).W by Def8
.= (a,xx.i).W by A7,FUNCT_7:32
.= qq.i by Def8;
end;
end;
hence thesis by Th9;
end;
then
A8: Phi((x+*(m,(x.m)+v))) = W.(a,*'(a,(p+*(m,p99m)))) by Lm5;
A9: (p+*(m,p9m)) = (a,(x+*(m,v))).W
proof
set pp = (p+*(m,p9m)), qq = (a,(x+*(m,v))).W;
for i being Nat of n holds pp.i = qq.i
proof
let i be Nat of n;
per cases;
suppose
A10: i = m;
hence pp.i = p9m by Th10
.= (a,(x+*(m,v)).m).W by Th13
.= qq.i by A10,Def8;
end;
suppose
A11: i <> m;
hence pp.i = p.i by FUNCT_7:32
.= (a,x.i).W by Def8
.= (a,(x+*(m,v)).i).W by A11,FUNCT_7:32
.= qq.i by Def8;
end;
end;
hence thesis by Th9;
end;
RAS is_semi_additive_in m & *'(a,(p+*(m,(p.m)@p9m))) = *'(a,p)@*'(a,(p
+*(m, p9m))) by A1,A2,Th29;
then
A12: W.(a,*'(a,(p+*(m,p99m)))) = W.(a,*'(a,p)) + W.(a,*'(a,(p+*(m,p9m)) ))
by A3,Lm6;
Phi(x) = W.(a,*'(a,p)) by Lm5;
hence thesis by A12,A8,A9,Lm5;
end;
thus (for x,v holds Phi((x+*(m,(x.m)+v))) = Phi(x) + Phi((x+*(m,v))))
implies RAS is_additive_in m
proof
assume
A13: for x,v holds Phi((x+*(m,(x.m)+v))) = Phi(x) + Phi ((x+*(m,v)));
then
A14: RAS is_semi_additive_in m by Lm7;
for a,pm,p9m,p st p.m = pm holds *'(a,(p+*(m,pm@p9m))) = *'(a,p)@*'(a
,(p+*(m,p9m)))
proof
let a,pm,p9m,p such that
A15: p.m = pm;
set x = W.(a,p), v = W.(a,p9m);
consider p99m such that
A16: (p99m)@a = (p.m)@(p9m) by MIDSP_1:def 3;
A17: (a,x).W = p by Th15;
A18: W.(a,p99m) = W.(a,p.m) + W.(a,p9m) by A16,MIDSP_2:30
.= x.m + v by Def9;
(p+*(m,p99m)) = (a,(x+*(m,(x.m)+v))).W
proof
set pp = (p+*(m,p99m)), xx = (x+*(m,(x.m)+v));
set qq = (a,xx).W;
for i being Nat of n holds pp.i = qq.i
proof
let i be Nat of n;
per cases;
suppose
A19: i = m;
hence pp.i = p99m by Th10
.= (a,(x.m)+v).W by A18,MIDSP_2:33
.= (a,xx.m).W by Th13
.= qq.i by A19,Def8;
end;
suppose
A20: i <> m;
hence pp.i = p.i by FUNCT_7:32
.= (a,x.i).W by A17,Def8
.= (a,xx.i).W by A20,FUNCT_7:32
.= qq.i by Def8;
end;
end;
hence thesis by Th9;
end;
then
A21: Phi((x+*(m,(x.m)+v))) = W.(a,*'(a,(p+*(m,p99m)))) by Lm5;
A22: (a,v).W = p9m by MIDSP_2:33;
(p+*(m,p9m)) = (a,(x+*(m,v))).W
proof
set pp = (p+*(m,p9m)), qq = (a,(x+*(m,v))).W;
for i being Nat of n holds pp.i = qq.i
proof
let i be Nat of n;
per cases;
suppose
A23: i = m;
hence pp.i = p9m by Th10
.= (a,(x+*(m,v)).m).W by A22,Th13
.= qq.i by A23,Def8;
end;
suppose
A24: i <> m;
hence pp.i = p.i by FUNCT_7:32
.= (a,x.i).W by A17,Def8
.= (a,(x+*(m,v)).i).W by A24,FUNCT_7:32
.= qq.i by Def8;
end;
end;
hence thesis by Th9;
end;
then
A25: Phi((x+*(m,v))) = W.(a,*'(a,(p+*(m,p9m)))) by Lm5;
Phi(x) = W.(a,*'(a,p)) by Lm4;
then
W.(a,*'(a,(p+*(m,p99m)))) = W.(a,*'(a,p)) + W.(a,*' (a,(p+*(m,p9m))
)) by A13,A21,A25;
hence thesis by A14,A15,A16,Lm6;
end;
hence thesis;
end;
end;
theorem Th31:
W.(a,p) = x & m<= n implies W.(a,(p+*(m+1,p.m))) = (x+*(m+1,x.m) )
proof
assume that
A1: W.(a,p) = x and
A2: m<=n;
reconsider m9 = m+1 as Nat of n by A2,Th8;
set y = W.(a,(p+*(m9,p.m))), z = (x+*(m9,x.m));
for k being Nat of n holds y.k = z.k
proof
let k be Nat of n;
now
per cases;
suppose
A3: k = m9;
thus y.k = W.(a,(p+*(m9,p.m)).k) by Def9
.= W.(a,p.m) by A3,Th10
.= x.m by A1,Def9
.= z.k by A3,Th13;
end;
suppose
A4: k <> m9;
thus y.k = W.(a,(p+*(m9,p.m)).k) by Def9
.= W.(a,p.k) by A4,FUNCT_7:32
.= x.k by A1,Def9
.= z.k by A4,FUNCT_7:32;
end;
end;
hence thesis;
end;
hence thesis by Th14;
end;
theorem Th32:
(a,x).W = p & m<=n implies (a,(x+*(m+1,x.m))).W = (p+*(m+1,p.m))
proof
assume that
A1: (a,x).W = p and
A2: m<=n;
W.(a,p) = x by A1,Th15;
then W.(a,(p+*(m+1,p.m))) = (x+*(m+1,x.m)) by A2,Th31;
hence thesis by Th15;
end;
theorem
m<=n implies (RAS is_alternative_in m iff for x holds Phi((x+*(m+1,x.m
))) = 0. W )
proof
assume
A1: m<=n;
thus RAS is_alternative_in m implies for x holds Phi((x+*(m+1,x.m))) = 0.W
proof
set a = the Point of RAS;
assume
A2: RAS is_alternative_in m;
let x;
set p = (a,x).W, b = (a,(0.W)).W;
set p9 = (p+*(m+1,p.m));
b = a by MIDSP_2:34;
then
A3: *'(a,p9) = b by A2;
(a,((x+*(m+1,x.m)))).W = p9 by A1,Th32;
hence thesis by A3,Th24;
end;
assume
A4: for x holds Phi((x+*(m+1,x.m))) = 0.W;
for a,p,pm st p.m = pm holds *'(a,p+*(m+1,pm)) = a
proof
let a,p,pm such that
A5: p.m = pm;
set x = W.(a,p), v = W.(a,a);
set x9 = (x+*(m+1,x.m));
v = 0.W by MIDSP_2:33;
then
A6: Phi(x9) = v by A4;
W.(a,((p+*(m+1,p.m)))) = x9 by A1,Th31;
hence thesis by A5,A6,Th23;
end;
hence thesis;
end;