:: Real Linear-Metric Space and Isometric Functions
:: by Robert Milewski
::
:: Received November 3, 1998
:: Copyright (c) 1998-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 NUMBERS, XBOOLE_0, METRIC_1, CONVEX1, SUBSET_1, REAL_1, CARD_1,
XXREAL_0, RELAT_1, ARYTM_1, FINSEQ_1, STRUCT_0, PARTFUN1, ARYTM_3,
COMPLEX1, CARD_3, ZFMISC_1, BINTREE1, TREES_2, FUNCT_1, TREES_4,
ORDINAL4, CAT_1, TREES_1, POWER, INT_1, NAT_1, FINSEQ_2, MARGREL1,
EUCLID, XBOOLEAN, MCART_1, BINTREE2, ABIAN, TARSKI, RELAT_2, FUNCT_2,
RLVECT_1, ALGSTR_0, BINOP_1, UNIALG_1, SUPINF_2, PRE_TOPC, GROUP_1,
GROUP_2, VECTMETR, FUNCT_7, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS,
MCART_1, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, RELAT_2, XXREAL_0, INT_1,
NAT_1, NAT_D, POWER, ABIAN, SERIES_1, RELAT_1, RELSET_1, MARGREL1,
BINOP_1, DOMAIN_1, FUNCT_1, PARTFUN1, FUNCT_2, STRUCT_0, ALGSTR_0,
PRE_TOPC, FINSEQ_1, FINSEQ_2, FINSEQ_4, BINARITH, TREES_1, TREES_2,
TREES_4, BINTREE1, BINTREE2, RVSUM_1, RLVECT_1, GROUP_1, GROUP_2, TOPS_2,
METRIC_1, EUCLID;
constructors REAL_1, NAT_D, FINSEQOP, FINSEQ_4, FINSOP_1, SERIES_1, REALSET1,
BINARITH, ABIAN, TOPS_2, GROUP_2, EUCLID, BINTREE2, RVSUM_1, RELSET_1,
XTUPLE_0, BINOP_1, BINOP_2, NUMBERS;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS,
XXREAL_0, NAT_1, FINSEQ_1, BINOP_2, MARGREL1, FINSEQ_2, TREES_2,
STRUCT_0, METRIC_1, GROUP_2, BINTREE1, BINTREE2, VALUED_0, XREAL_0,
RELAT_1, INT_1, EUCLID, ORDINAL1, CARD_1, XTUPLE_0;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions FUNCT_2, STRUCT_0, TARSKI, XBOOLE_0, ALGSTR_0;
equalities STRUCT_0, MARGREL1, XBOOLEAN, RLVECT_1, RVSUM_1, EUCLID, FINSEQ_2,
ALGSTR_0, VALUED_1;
expansions STRUCT_0, TARSKI, RLVECT_1;
theorems TARSKI, MCART_1, NAT_1, NAT_2, ZFMISC_1, BINOP_1, RELAT_1, FUNCT_1,
FUNCT_2, POWER, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSEQ_5, BINARI_2,
BINARI_3, ABSVALUE, TOPS_2, FUNCOP_1, BINTREE2, PRE_FF, RLVECT_1,
METRIC_1, RVSUM_1, EUCLID, GROUP_1, GROUP_2, RELAT_2, XCMPLX_1, PARTFUN1,
INT_1, ORDERS_1, XREAL_1, FINSEQOP, XXREAL_0, FINSOP_1, NAT_D, ORDINAL1,
XREAL_0, XTUPLE_0, FINSEQ_3;
schemes BINOP_1, NAT_1, FINSEQ_2, BINTREE2, RELSET_1, XBOOLE_0;
begin :: Convex and Internal Metric Spaces
definition
let V be non empty MetrStruct;
attr V is convex means
for x,y be Element of V for r be Real st 0 <= r & r <= 1
ex z be Element of V st dist(x,z) = r * dist(x,y) &
dist(z,y) = (1 - r) * dist(x,y);
end;
definition
let V be non empty MetrStruct;
attr V is internal means
for x,y be Element of V for p,q be Real st p > 0 &
q > 0 ex f be FinSequence of the carrier of V st f/.1 = x & f/.len f = y & (for
i be Element of NAT st 1 <= i & i <= len f - 1 holds dist(f/.i,f/.(i+1)) < p) &
for F be FinSequence of REAL st len F = len f - 1 & for i be Element of NAT st
1 <= i & i <= len F holds F/.i = dist(f/.i,f/.(i+1)) holds |.dist(x,y) - Sum
F.| < q;
end;
theorem Th1:
for V be non empty MetrSpace st V is convex
for x,y be Element of V
for p be Real st p > 0
ex f be FinSequence of the carrier of V st
f/.1 = x & f/.len f = y &
(for i be Element of NAT st 1 <= i & i <= len f - 1
holds dist(f/.i,f/.(i+1)) < p) &
for F be FinSequence of REAL st len F = len f - 1 &
for i be Element of NAT st 1 <= i & i <= len F
holds F/.i = dist(f/.i,f/.(i+1))
holds dist(x,y) = Sum F
proof
let V be non empty MetrSpace;
assume
A1: V is convex;
set A = the carrier of V;
let x,y be Element of V;
defpred P[set,set,set] means for a1,a2 be Element of A st $1 = [a1,a2] ex b
be Element of A st $2 = [a1,b] & $3 = [b,a2] & dist(a1,a2) = 2 * dist(a1,b) &
dist(a1,a2) = 2 * dist(b,a2);
A2: for a be Element of [:A,A:] ex c,d be Element of [:A,A:] st P[a,c,d]
proof
let a be Element of [:A,A:];
consider a19,a29 be object such that
A3: a19 in A & a29 in A and
A4: a = [a19,a29] by ZFMISC_1:def 2;
reconsider a19, a29 as Element of A by A3;
consider z be Element of A such that
A5: dist(a19,z) = 1/2 * dist(a19,a29) and
A6: dist(z,a29) = (1 - 1/2) * dist(a19,a29) by A1;
take c = [a19,z];
take d = [z,a29];
let a1,a2 be Element of A;
assume
A7: a = [a1,a2];
take z;
thus c = [a1,z] by A4,A7,XTUPLE_0:1;
thus d = [z,a2] by A4,A7,XTUPLE_0:1;
a1 = a19 by A4,A7,XTUPLE_0:1;
hence dist(a1,a2) = 2 * dist(a1,z) by A4,A5,A7,XTUPLE_0:1;
a2 = a29 by A4,A7,XTUPLE_0:1;
hence thesis by A4,A6,A7,XTUPLE_0:1;
end;
consider D be binary DecoratedTree of [:A,A:] such that
A8: dom D = {0,1}* and
A9: D.{} = [x,y] and
A10: for z be Node of D holds P[D.z, D.(z ^ <* 0 *>), D.(z ^ <*1*>)]
from BINTREE2:sch 1(A2);
reconsider dD = dom D as full Tree by A8,BINTREE2:def 2;
let p be Real such that
A11: p > 0;
per cases;
suppose
dist(x,y) >= p;
then dist(x,y)/p >= 1 by A11,XREAL_1:181;
then log(2,dist(x,y)/p) >= log(2,1) by PRE_FF:10;
then log(2,dist(x,y)/p) >= 0 by POWER:51;
then reconsider n1 = [\ log(2,dist(x,y)/p) /] as Element of NAT
by INT_1:53;
defpred Q[Nat] means for t be Tuple of $1,BOOLEAN st t = 0*$1 holds (D.
'not' t)`2 = y;
defpred P[Nat] means (D.(0*$1))`1 = x;
reconsider n = n1 + 1 as non zero Element of NAT;
reconsider N = 2 to_power n as non zero Element of NAT by POWER:34;
set r = dist(x,y) / N;
reconsider FSL = FinSeqLevel(n,dD) as FinSequence of dom D by FINSEQ_2:24;
deffunc G(Nat) = D.(FSL/.$1);
consider g be FinSequence of [:A,A:] such that
A12: len g = N and
A13: for k be Nat st k in dom g holds g.k = G(k) from FINSEQ_2:sch 1;
A14: dom g = Seg N by A12,FINSEQ_1:def 3;
A15: for j be Nat st P[j] holds P[j+1]
proof
let j be Nat;
assume
A16: (D.(0*j))`1 = x;
reconsider zj = 0*j as Node of D by A8,BINARI_3:4;
consider a,b be object such that
A17: a in A & b in A and
A18: D.zj = [a,b] by ZFMISC_1:def 2;
reconsider a1 = a, b1 = b as Element of A by A17;
A19: ex z1 be Element of A st D.(zj^<* 0 *>) = [a1,z1] & D.(zj ^<* 1 *>)
= [z1,b1] & dist(a1,b1) = 2 * dist(a1,z1) & dist(a1,b1) = 2 * dist( z1,b1) by
A10,A18;
thus (D.(0*(j+1)))`1 = (D.(zj^<* 0 *>))`1 by FINSEQ_2:60
.= a1 by A19
.= x by A18,A16;
end;
A20: P[0] by A9;
A21: for j be Nat holds P[j] from NAT_1:sch 2(A20,A15);
2 to_power n > 0 by POWER:34;
then 0 + 1 <= 2 to_power n by NAT_1:13;
then
A22: 1 <= len FinSeqLevel(n,dD) by BINTREE2:19;
A23: for j be non zero Nat st Q[j] holds Q[j+1]
proof
let j be non zero Nat;
assume
A24: for t be Tuple of j,BOOLEAN st t = 0*j holds (D.'not' t)`2 = y;
let t be Tuple of j+1,BOOLEAN;
consider t1 be Element of j-tuples_on BOOLEAN,
dd be Element of BOOLEAN
such that
A25: t = t1^<*dd*> by FINSEQ_2:117;
assume
A26: t = 0*(j+1);
then t = 0*j ^ <* 0 *> by FINSEQ_2:60;
then t1 = 0*j by A25,FINSEQ_2:17;
then
A27: (D.'not' t1)`2 = y by A24;
dd = t.(len t1 + 1) by A25,FINSEQ_1:42
.= ((j + 1) |-> (0 qua Real)).(j + 1) by A26
.= FALSE;
then 'not' dd = 1;
then
A28: 'not' t = 'not' t1^<* 1 *> by A25,BINARI_2:9;
reconsider nt1 = 'not' t1 as Node of D by A8,FINSEQ_1:def 11;
consider a,b be object such that
A29: a in A & b in A and
A30: D.nt1 = [a,b] by ZFMISC_1:def 2;
reconsider a1 = a, b1 = b as Element of A by A29;
ex b be Element of A st D.(nt1^<* 0 *>) = [a1,b] & D.(nt1 ^<* 1 *>)
= [b,b1] & dist(a1,b1) = 2 * dist(a1,b) & dist(a1,b1) = 2 * dist(b, b1) by A10
,A30;
hence (D.'not' t)`2 = b1 by A28
.= y by A30,A27;
end;
A31: Q[1]
proof
reconsider pusty = <*>({0,1}) as Node of D by A8,FINSEQ_1:def 11;
let t be Tuple of 1,BOOLEAN;
A32: ex b be Element of A st D.(pusty^<* 0 *>) = [x,b] & D.( pusty^<* 1
*>) = [b,y] & dist(x,y) = 2 * dist(x,b) & dist(x,y) = 2 * dist(b,y ) by A9,A10;
assume t = 0*1;
then t = <*FALSE*> by FINSEQ_2:59;
hence (D.'not' t)`2 = (D.(pusty^<* 1 *>))`2 by BINARI_3:14,FINSEQ_1:34
.= y by A32;
end;
A33: for j be non zero Nat holds Q[j] from NAT_1:sch 10(A31,A23);
deffunc F(Nat) = (g/.$1)`1;
consider h be FinSequence of the carrier of V such that
A34: len h = N and
A35: for k be Nat st k in dom h holds h.k = F(k) from FINSEQ_2:sch 1;
A36: dom h = Seg N by A34,FINSEQ_1:def 3;
A37: 1 <= N by NAT_1:14;
then
A38: 1 in Seg N by FINSEQ_1:1;
then
A39: 1 in dom h by A34,FINSEQ_1:def 3;
take f = h^<*y*>;
A40: len f = len h + len <*y*> by FINSEQ_1:22
.= len h + 1 by FINSEQ_1:39;
1 <= N + 1 by NAT_1:11;
hence f/.1 = f.1 by A34,A40,FINSEQ_4:15
.= h.1 by A39,FINSEQ_1:def 7
.= (g/.1)`1 by A35,A36,A38
.= (g.1)`1 by A12,A37,FINSEQ_4:15
.= (D.(FSL/.1))`1 by A13,A14,A38
.= (D.(FinSeqLevel(n,dD).1))`1 by A22,FINSEQ_4:15
.= (D.(0*n))`1 by BINTREE2:15
.= x by A21;
len f in Seg (len f) by A40,FINSEQ_1:4;
then len f in dom f by FINSEQ_1:def 3;
hence
A41: f/.len f = (h^<*y*>).(len h + 1) by A40,PARTFUN1:def 6
.= y by FINSEQ_1:42;
A42: for i be Element of NAT st 1 <= i & i <= len f - 1 holds dist(f/.i,f
/.(i+1)) = r
proof
0*n in BOOLEAN* by BINARI_3:4;
then reconsider ze = 0*n as Tuple of n,BOOLEAN by FINSEQ_1:def 11;
reconsider ze as Element of n-tuples_on BOOLEAN by FINSEQ_2:131;
defpred S[non zero Nat] means for j be non zero Element of NAT st j <=
2 to_power $1 for DF1,DF2 be Element of V st DF1 = (D.(FinSeqLevel($1,dD).j))`1
& DF2 = (D.(FinSeqLevel($1,dD).j))`2 holds dist(DF1,DF2) = dist(x,y) / 2
to_power $1;
let i be Element of NAT;
assume that
A43: 1 <= i and
A44: i <= len f - 1;
A45: len FSL = N by BINTREE2:19;
A46: now
per cases by A44,XXREAL_0:1;
suppose
i < len f - 1;
then i < len f-'1 by A40,NAT_1:11,XREAL_1:233;
then i + 1 <= len f-'1 by NAT_1:13;
then
A47: i + 1 <= len f - 1 by A40,NAT_1:11,XREAL_1:233;
then
A48: i + 1 - 1 <= (2 to_power n) - 1 by A34,A40,XREAL_1:9;
defpred R[non zero Nat] means for i be Nat st 1 <= i & i <= (2
to_power $1) - 1 holds (D.(FinSeqLevel($1,dD).(i+1)))`1 = (D.(FinSeqLevel($1,dD
).i))`2;
A49: for n be non zero Nat st R[n] holds R[n+1]
proof
let n be non zero Nat;
reconsider nn=n as non zero Element of NAT by ORDINAL1:def 12;
reconsider zb = dD-level n as non empty set by A8,BINTREE2:10;
assume
A50: for i be Nat st 1 <= i & i <= (2 to_power n) - 1 holds (D
.(FinSeqLevel(n,dD).(i+1)))`1 = (D.(FinSeqLevel(n,dD).i))`2;
let i be Nat;
assume that
A51: 1 <= i and
A52: i <= (2 to_power (n+1)) - 1;
reconsider ii=i as Element of NAT by ORDINAL1:def 12;
A53: 1 + 1 <= i + 1 by A51,XREAL_1:6;
then
A54: (i+1) div 2 >= 1 by NAT_2:13;
2 to_power (n+1) > 0 by POWER:34;
then
A55: 2 to_power (n+1) >= 0 + 1 by NAT_1:13;
then i <= (2 to_power (n+1)) -' 1 by A52,XREAL_1:233;
then i < (2 to_power (n+1)) -' 1 + 1 by NAT_1:13;
then
A56: i < (2 to_power (n+1)) - 1 + 1 by A55,XREAL_1:233;
then
A57: i + 1 <= 2 to_power (n+1) by NAT_1:13;
then i + 1 <= (2 to_power n) * (2 to_power 1) by POWER:27;
then i + 1 <= (2 to_power n) * 2 by POWER:25;
then
A58: (i+1+1) div 2 <= 2 to_power n by NAT_2:25;
i + 1 <= i + 1 + 1 by NAT_1:11;
then 2 <= i + 1 + 1 by A53,XXREAL_0:2;
then (i+1+1) div 2 >= 1 by NAT_2:13;
then (i+1+1) div 2 in Seg (2 to_power n) by A58,FINSEQ_1:1;
then (i+1+1) div 2 in dom FinSeqLevel(nn,dD) by BINTREE2:20;
then FinSeqLevel(n,dD).((i+1+1) div 2) in zb by FINSEQ_2:11;
then reconsider
FF = FinSeqLevel(nn,dD).((i+1+1) div 2) as Tuple of n,
BOOLEAN by BINTREE2:5;
reconsider FF as Element of n-tuples_on BOOLEAN
by FINSEQ_2:131;
reconsider FF1 = FF as Node of D by A8,FINSEQ_1:def 11;
consider a9,b9 be object such that
A59: a9 in A & b9 in A and
A60: D.FF1 = [a9,b9] by ZFMISC_1:def 2;
i <= (2 to_power n) * (2 to_power 1) by A56,POWER:27;
then i <= (2 to_power n) * 2 by POWER:25;
then (i+1) div 2 <= 2 to_power n by NAT_2:25;
then (i+1) div 2 in Seg (2 to_power n) by A54,FINSEQ_1:1;
then (i+1) div 2 in dom FinSeqLevel(nn,dD) by BINTREE2:20;
then FinSeqLevel(n,dD).((i+1) div 2) in zb by FINSEQ_2:11;
then reconsider F = FinSeqLevel(nn,dD).((i+1) div 2)
as Tuple of n, BOOLEAN by BINTREE2:5;
reconsider F as Element of n-tuples_on BOOLEAN
by FINSEQ_2:131;
reconsider F1 = F as Node of D by A8,FINSEQ_1:def 11;
consider a,b be object such that
A61: a in A & b in A and
A62: D.F1 = [a,b] by ZFMISC_1:def 2;
reconsider a1 = a, b1 = b, a19 = a9, b19 = b9 as Element of A by
A61,A59;
consider d be Element of A such that
A63: D.(F1^<* 0 *>) = [a1,d] and
A64: D.(F1^<* 1 *>) = [d,b1] and
dist(a1,b1) = 2 * dist(a1,d) and
dist(a1,b1) = 2 * dist(d,b1) by A10,A62;
consider d9 be Element of A such that
A65: D.(FF1^<* 0 *>) = [a19,d9] and
A66: D.(FF1^<* 1 *>) = [d9,b19] and
dist(a19,b19) = 2 * dist(a19,d9) and
dist(a19,b19) = 2 * dist(d9,b19) by A10,A60;
A67: i = i + 1 - 1 .= i + 1 -' 1 by NAT_1:11,XREAL_1:233;
now
per cases;
suppose
i is odd;
then
A68: i mod 2 = 1 by NAT_2:22;
then (i + 1) mod 2 = 0 by A67,NAT_2:18;
then i + 1 is even by NAT_2:21;
then (i+1) div 2 = (i+1+1) div 2 by NAT_2:26;
then
A69: d = d9 by A63,A65,XTUPLE_0:1;
thus (D.(FinSeqLevel(n+1,dD).(i+1)))`1 = (D.(FF^<*(2*1+i) mod
2*>)) `1 by A57,BINTREE2:24
.= (D.(FF^<* 1 *>))`1 by A68,NAT_D:21
.= d by A66,A69
.= (D.(F^<* 0 *>))`2 by A63
.= (D.(F^<*(ii+1) mod 2*>))`2 by A67,A68,NAT_2:18
.= (D.(FinSeqLevel(n+1,dD).ii))`2 by A51,A56,BINTREE2:24;
end;
suppose
i is even;
then
A70: i mod 2 = 0 by NAT_2:21;
then
A71: 1 = (i -' 1) mod 2 by A51,NAT_2:18
.= (i -' 1 + 2 * 1) mod 2 by NAT_D:21
.= (i -' 1 + 1 + 1) mod 2
.= (i + 1) mod 2 by A51,XREAL_1:235;
A72: 1 + (1 + i) >= 1 by NAT_1:11;
1 + 1 + (i -' 1) = 1 + 1 + (i - 1) by A51,XREAL_1:233
.= 1 + 1 + i - 1;
then 1 = (1 + 1 + i -' 1) mod 2 by A71,A72,XREAL_1:233;
then (1 + 1 + i) mod 2 = 0 by NAT_2:18;
then i + 1 + 1 = 2 * ((i + 1 + 1) div 2) + 0 by NAT_D:2;
then
A73: 2 divides i + 1 + 1 by NAT_D:3;
1 <= i + 1 + 1 by NAT_1:11;
then (i + 1 + 1 -' 1) div 2 = ((i + 1 + 1) div 2) - 1 by A73,
NAT_2:15;
then (i + 1) div 2 = ((i + 1 + 1) div 2) - 1 by NAT_D:34;
then
A74: ((i + 1) div 2) + 1 = (i + 1 + 1) div 2;
then
A75: (i+1) div 2 <= (2 to_power n) - 1 by A58,XREAL_1:19;
A76: a9 = (D.(FinSeqLevel(n,dD).((i+1+1) div 2)))`1 by A60
.= (D.(FinSeqLevel(n,dD).((i+1) div 2)))`2 by A50,A54,A74,A75
.= b by A62;
thus (D.(FinSeqLevel(n+1,dD).(i+1)))`1 = (D.(FF^<*(2*1+i) mod
2*>))`1 by A57,BINTREE2:24
.= (D.(FF^<* 0 *>))`1 by A70,NAT_D:21
.= a19 by A65
.= (D.(F^<* 1 *>))`2 by A64,A76
.= (D.(FinSeqLevel(n+1,dD).ii))`2 by A51,A56,A71,BINTREE2:24;
end;
end;
hence thesis;
end;
A77: R[1]
proof
reconsider pusty = <*>({0,1}) as Node of D by A8,FINSEQ_1:def 11;
let i be Nat;
A78: (2 to_power 1) - 1 = 1 + 1 - 1 by POWER:25
.= 1;
consider b be Element of A such that
A79: D.(pusty^<* 0 *>) = [x,b] and
A80: D.(pusty^<* 1 *>) = [b,y] and
dist(x,y) = 2 * dist(x,b) and
dist(x,y) = 2 * dist(b,y) by A9,A10;
assume 1 <= i & i <= (2 to_power 1) - 1;
then
A81: i = 1 by A78,XXREAL_0:1;
hence (D.(FinSeqLevel(1,dD).(i+1)))`1 = (D.<* 1 *>)`1 by
BINTREE2:23
.= (D.(pusty^<* 1 *>))`1 by FINSEQ_1:34
.= b by A80
.= (D.(pusty^<* 0 *>))`2 by A79
.= (D.<* 0 *>)`2 by FINSEQ_1:34
.= (D.(FinSeqLevel(1,dD).i))`2 by A81,BINTREE2:22;
end;
A82: for n be non zero Nat holds R[n] from NAT_1:sch 10(A77,A49);
A83: 1 <= 1 + i by NAT_1:11;
then
A84: i + 1 in Seg len h by A40,A47,FINSEQ_1:1;
then i + 1 in dom h by FINSEQ_1:def 3;
hence f/.(i+1) = h/.(i+1) by FINSEQ_4:68
.= h.(i+1) by A40,A47,A83,FINSEQ_4:15
.= (g/.(i+1))`1 by A34,A35,A36,A84
.= (g.(i+1))`1 by A12,A34,A40,A47,A83,FINSEQ_4:15
.= (D.(FSL/.(i+1)))`1 by A13,A14,A34,A84
.= (D.(FinSeqLevel(n,dD).(i+1)))`1 by A34,A40,A45,A47,A83,
FINSEQ_4:15
.= (D.(FinSeqLevel(n,dD).i))`2 by A43,A48,A82;
end;
suppose
A85: i = len f - 1;
hence f/.(i+1) = (D.'not' ze)`2 by A33,A41
.= (D.(FinSeqLevel(n,dD).i))`2 by A34,A40,A85,BINTREE2:16;
end;
end;
A86: for l be non zero Nat st S[l] holds S[l+1]
proof
let l be non zero Nat;
reconsider dDll = dD-level l as non empty set by A8,BINTREE2:10;
reconsider ll=l as non zero Element of NAT by ORDINAL1:def 12;
reconsider dDll1 = dD-level (l+1) as non empty set by A8,BINTREE2:10;
assume
A87: for j be non zero Element of NAT st j <= 2 to_power l for
DF1,DF2 be Element of V st DF1 = (D.(FinSeqLevel(l,dD).j))`1 & DF2 = (D.(
FinSeqLevel(l,dD).j))`2 holds dist(DF1,DF2) = dist(x,y) / 2 to_power l;
let j be non zero Element of NAT;
(j + 1) div 2 <> 0
proof
assume (j + 1) div 2 = 0;
then j + 1 < 1 + 1 by NAT_2:12;
then j < 1 by XREAL_1:6;
hence contradiction by NAT_1:14;
end;
then reconsider j1 = (j+1) div 2 as non zero Element of NAT;
assume
A88: j <= 2 to_power (l+1);
then j <= (2 to_power l) * (2 to_power 1) by POWER:27;
then
A89: j <= (2 to_power l) * 2 by POWER:25;
then j1 >= 1 & j1 <= 2 to_power l by NAT_1:14,NAT_2:25;
then j1 in Seg (2 to_power l) by FINSEQ_1:1;
then (j+1) div 2 in dom FinSeqLevel(ll,dD) by BINTREE2:20;
then FinSeqLevel(l,dD).((j+1) div 2) in dDll by FINSEQ_2:11;
then reconsider
FSLlprim = FinSeqLevel(ll,dD).((j+1) div 2) as Tuple of l,
BOOLEAN by BINTREE2:5;
reconsider FSLlprim as Element of l-tuples_on BOOLEAN by FINSEQ_2:131;
A90: FinSeqLevel(l+1,dD) is FinSequence of dom D by FINSEQ_2:24;
j >= 1 by NAT_1:14;
then j in Seg (2 to_power (l+1)) by A88,FINSEQ_1:1;
then
A91: j in dom FinSeqLevel(l+1,dD) by BINTREE2:20;
then reconsider Fj = (FinSeqLevel(l+1,dD).j) as Element of dom D
by A90,FINSEQ_2:11;
FinSeqLevel(l+1,dD).j in dDll1 by A91,FINSEQ_2:11;
then reconsider
FSLl1 = FinSeqLevel(l+1,dD).j as Tuple of l+1,BOOLEAN by BINTREE2:5;
consider FSLl be Element of l-tuples_on BOOLEAN,
d be Element of BOOLEAN
such that
A92: FSLl1 = FSLl^<*d*> by FINSEQ_2:117;
let DF1,DF2 be Element of V;
assume DF1 = (D.(FinSeqLevel(l+1,dD).j))`1 & DF2 = (D.(FinSeqLevel(
l+1,dD).j))`2;
then
A93: D.Fj = [DF1,DF2] by MCART_1:21;
reconsider NFSLl = FSLl as Node of D by A8,FINSEQ_1:def 11;
consider x1,y1 be object such that
A94: x1 in A & y1 in A and
A95: D.NFSLl = [x1,y1] by ZFMISC_1:def 2;
reconsider x1, y1 as Element of A by A94;
consider b be Element of A such that
A96: D.(NFSLl^<* 0 *>) = [x1,b] and
A97: D.(NFSLl^<* 1 *>) = [b,y1] and
A98: dist(x1,y1) = 2 * dist(x1,b) and
A99: dist(x1,y1) = 2 * dist(b,y1) by A10,A95;
A100: FinSeqLevel(ll+1,dD).j = FSLlprim^<*(j+1) mod 2*> by A88,BINTREE2:24;
then FSLl = FSLlprim by A92,FINSEQ_2:17;
then
A101: x1 = (D.(FinSeqLevel(l,dD).j1))`1 & y1 = (D.(FinSeqLevel(l,dD).
j1))`2 by A95;
A102: d = (j+1) mod 2 by A92,A100,FINSEQ_2:17;
now
per cases by A102,NAT_D:12;
suppose
d = 0;
then DF1 = x1 & DF2 = b by A93,A92,A96,XTUPLE_0:1;
then 2 * dist(DF1,DF2) = (dist(x,y) / 2 to_power l) / 2 * 2 by A87
,A89,A98,A101,NAT_2:25;
hence dist(DF1,DF2) = dist(x,y) / ((2 to_power l) * 2) by
XCMPLX_1:78
.= dist(x,y) / ((2 to_power l) * (2 to_power 1)) by POWER:25
.= dist(x,y) / (2 to_power (l+1)) by POWER:27;
end;
suppose
d = 1;
then DF1 = b & DF2 = y1 by A93,A92,A97,XTUPLE_0:1;
then 2 * dist(DF1,DF2) = (dist(x,y) / 2 to_power l) / 2 * 2 by A87
,A89,A99,A101,NAT_2:25;
hence dist(DF1,DF2) = dist(x,y) / ((2 to_power l) * 2) by
XCMPLX_1:78
.= dist(x,y) / ((2 to_power l) * (2 to_power 1)) by POWER:25
.= dist(x,y) / (2 to_power (l+1)) by POWER:27;
end;
end;
hence thesis;
end;
A103: S[1]
proof
reconsider pusty = <*>({0,1}) as Node of D by A8,FINSEQ_1:def 11;
let j be non zero Element of NAT;
assume
A104: j <= 2 to_power 1;
A105: FinSeqLevel(1,dD) is FinSequence of dom D by FINSEQ_2:24;
j >= 1 by NAT_1:14;
then j in Seg (2 to_power 1) by A104,FINSEQ_1:1;
then j in dom FinSeqLevel(1,dD) by BINTREE2:20;
then reconsider FSL1j = FinSeqLevel(1,dD).j as Element of dom D
by A105,FINSEQ_2:11;
let DF1,DF2 be Element of V;
assume
A106: DF1 = (D.(FinSeqLevel(1,dD).j))`1 & DF2 = (D.(FinSeqLevel(1, dD).j))`2;
2 to_power 1 = 2 & j >= 1 by NAT_1:14,POWER:25;
then
A107: j in Seg 2 by A104,FINSEQ_1:1;
now
per cases by A107,FINSEQ_1:2,TARSKI:def 2;
suppose
A108: j = 1;
A109: ex b be Element of A st D.(pusty^<* 0 *>) = [x,b] & D.( pusty
^<* 1 *>) = [b,y] & dist(x,y) = 2 * dist(x,b) & dist(x,y) = 2 * dist(b,y ) by
A9,A10;
A110: D.(pusty ^ <* 0 *>) = D.(<* 0 *>) by FINSEQ_1:34
.= D.FSL1j by A108,BINTREE2:22
.= [DF1,DF2] by A106,MCART_1:21;
then DF1 = x by A109,XTUPLE_0:1;
hence dist(DF1,DF2) = dist(x,y) / 2 by A110,A109,XTUPLE_0:1;
end;
suppose
A111: j = 2;
consider b be Element of A such that
D.(pusty^<* 0 *>) = [x,b] and
A112: D.(pusty^<* 1 *>) = [b,y] and
dist(x,y) = 2 * dist(x,b) and
A113: dist(x,y) = 2 * dist(b,y) by A9,A10;
A114: D.(pusty ^ <* 1 *>) = D.(<* 1 *>) by FINSEQ_1:34
.= D.FSL1j by A111,BINTREE2:23
.= [DF1,DF2] by A106,MCART_1:21;
then DF1 = b by A112,XTUPLE_0:1;
hence dist(DF1,DF2) = dist(x,y) / 2 by A114,A112,A113,XTUPLE_0:1;
end;
end;
hence thesis by POWER:25;
end;
A115: for l be non zero Nat holds S[l] from NAT_1:sch 10(A103,A86);
A116: i in Seg len h by A40,A43,A44,FINSEQ_1:1;
then i in dom h by FINSEQ_1:def 3;
then f/.i = h/.i by FINSEQ_4:68
.= h.i by A40,A43,A44,FINSEQ_4:15
.= (g/.i)`1 by A34,A35,A36,A116
.= (g.i)`1 by A12,A34,A40,A43,A44,FINSEQ_4:15
.= (D.(FSL/.i))`1 by A13,A14,A34,A116
.= (D.(FinSeqLevel(n,dD).i))`1 by A34,A40,A43,A44,A45,FINSEQ_4:15;
hence thesis by A34,A40,A43,A44,A46,A115;
end;
log(2,dist(x,y)/p) < n * 1 by INT_1:29;
then log(2,dist(x,y)/p) < n * log(2,2) by POWER:52;
then log(2,dist(x,y)/p) < log(2,2 to_power n) by POWER:55;
then dist(x,y)/p < N by PRE_FF:10;
then dist(x,y)/p*p < N*p by A11,XREAL_1:68;
then dist(x,y) < N*p by A11,XCMPLX_1:87;
then dist(x,y)/N < N*p/N by XREAL_1:74;
then dist(x,y)/N < p/N*N by XCMPLX_1:74;
then r < p by XCMPLX_1:87;
hence for i be Element of NAT st 1 <= i & i <= len f - 1 holds dist(f/.i,f
/.(i+1)) < p by A42;
let F be FinSequence of REAL such that
A117: len F = len f - 1 and
A118: for i be Element of NAT st 1 <= i & i <= len F holds F/.i = dist
(f/.i,f/.(i+1));
A119: rng F = {r}
proof
thus rng F c= {r}
proof
let a be object;
assume a in rng F;
then consider c be object such that
A120: c in dom F and
A121: F.c = a by FUNCT_1:def 3;
c in Seg len F by A120,FINSEQ_1:def 3;
then c in { t where t is Nat : 1 <= t & t <= len F } by FINSEQ_1:def 1;
then consider c1 be Nat such that
A122: c1 = c and
A123: 1 <= c1 & c1 <= len F;
reconsider c1 as Element of NAT by ORDINAL1:def 12;
a = F/.c1 by A121,A122,A123,FINSEQ_4:15
.= dist(f/.c1,f/.(c1+1)) by A118,A123
.= r by A42,A117,A123;
hence thesis by TARSKI:def 1;
end;
let a be object;
assume a in {r};
then a = r by TARSKI:def 1;
then
A124: a = dist(f/.1,f/.(1+1)) by A34,A40,A37,A42
.= F/.1 by A34,A40,A37,A117,A118
.= F.1 by A34,A40,A37,A117,FINSEQ_4:15;
1 in Seg len F by A34,A40,A37,A117,FINSEQ_1:1;
then 1 in dom F by FINSEQ_1:def 3;
hence thesis by A124,FUNCT_1:def 3;
end;
dom F = Seg len F by FINSEQ_1:def 3;
then F = len F |-> r by A119,FUNCOP_1:9;
hence Sum F = (N + 1 - 1) * r by A34,A40,A117,RVSUM_1:80
.= dist(x,y) by XCMPLX_1:87;
end;
suppose
A125: dist(x,y) < p;
take f = <*x,y*>;
thus
A126: f/.1 = x by FINSEQ_4:17;
len f = 2 by FINSEQ_1:44;
hence f/.len f = y by FINSEQ_4:17;
A127: len f - 1 = 1 + 1 - 1 by FINSEQ_1:44
.= 1;
thus for i be Element of NAT st 1 <= i & i <= len f - 1 holds dist(f/.i,f
/.(i+1)) < p
proof
let i be Element of NAT;
assume 1 <= i & i <= len f - 1;
then i in Seg 1 by A127,FINSEQ_1:1;
then i = 1 by FINSEQ_1:2,TARSKI:def 1;
hence thesis by A125,A126,FINSEQ_4:17;
end;
let F be FinSequence of REAL;
assume that
A128: len F = len f - 1 and
A129: for i be Element of NAT st 1 <= i & i <= len F holds F/.i = dist
(f/.i,f/.(i+1));
reconsider dxy = dist(x,y) as Element of REAL by XREAL_0:def 1;
1 <= len F by A127,A128; then
1 in dom F by FINSEQ_3:25; then
F/.1 = F.1 by PARTFUN1:def 6; then
F.1 = dist(f/.1,f/.(1+1)) by A127,A128,A129
.= dist(x,y) by A126,FINSEQ_4:17;
then F = <*dxy*> by A127,A128,FINSEQ_5:14;
then Sum F = dxy by FINSOP_1:11;
hence thesis;
end;
end;
registration
cluster convex -> internal for non empty MetrSpace;
coherence
proof
let V be non empty MetrSpace;
assume
A1: V is convex;
let x,y be Element of V;
let p,q be Real such that
A2: p > 0 and
A3: q > 0;
consider f be FinSequence of the carrier of V such that
A4: f/.1 = x & f/.len f = y & for i be Element of NAT st 1 <= i & i <=
len f - 1 holds dist(f/.i,f/.(i+1)) < p and
A5: for F be FinSequence of REAL st len F = len f - 1 & for i be
Element of NAT st 1 <= i & i <= len F holds F/.i = dist(f/.i,f/.(i+1)) holds
dist(x,y) = Sum F by A1,A2,Th1;
take f;
thus f/.1 = x & f/.len f = y & for i be Element of NAT st 1 <= i & i <=
len f - 1 holds dist(f/.i,f/.(i+1)) < p by A4;
let F be FinSequence of REAL;
assume len F = len f - 1 & for i be Element of NAT st 1 <= i & i <= len F
holds F/. i = dist(f/.i,f/.(i+1));
then dist(x,y) = Sum F by A5;
hence |.dist(x,y) - Sum F.| < q by A3,ABSVALUE:2;
end;
end;
registration
cluster convex for non empty MetrSpace;
existence
proof
reconsider ZS = {0} as non empty set;
deffunc T((Element of ZS), Element of ZS) = In(0,REAL);
consider F be Function of [:ZS,ZS:],REAL such that
A1: for x,y be Element of ZS holds F.(x,y) = T(x,y) from BINOP_1:sch 4;
reconsider V = MetrStruct (# ZS,F #) as non empty MetrStruct;
A2: now
let a,b be Element of V;
thus dist(a,b) = F.(a,b) by METRIC_1:def 1
.= 0 by A1
.= F.(b,a) by A1
.= dist(b,a) by METRIC_1:def 1;
end;
A3: now
let a be Element of V;
thus dist(a,a) = F.(a,a) by METRIC_1:def 1
.= 0 by A1;
end;
A4: now
let a,b,c be Element of V;
A5: c = 0 by TARSKI:def 1;
a = 0 by TARSKI:def 1;
then b = 0 & dist(a,c) = 0 by A3,A5,TARSKI:def 1;
hence dist(a,c) <= dist(a,b) + dist(b,c) by A3,A5;
end;
now
let a,b be Element of V;
assume dist(a,b) = 0;
a = 0 by TARSKI:def 1;
hence a = b by TARSKI:def 1;
end;
then reconsider V as discerning Reflexive symmetric triangle non empty
MetrStruct by A3,A2,A4,METRIC_1:1,2,3,4;
take V;
let x,y be Element of V;
let r be Real such that
0 <= r and
r <= 1;
take z = x;
A6: dist(z,y) = F.(z,y) by METRIC_1:def 1
.= 0 by A1;
dist(x,z) = F.(x,z) by METRIC_1:def 1
.= 0 by A1;
hence dist(x,z) = r * dist(x,y) & dist(z,y) = (1 - r) * dist(x,y) by A6;
end;
end;
begin :: Isometric Functions
definition
let V be non empty MetrStruct;
let f be Function of V,V;
attr f is isometric means
:Def3:
for x,y be Element of V holds dist(x,y) = dist(f.x,f.y);
end;
registration
let V be non empty MetrStruct;
cluster id(V) -> onto isometric;
coherence
proof
thus rng id(V) = the carrier of V;
let x,y be Element of V;
thus dist(x,y) = dist(id(V).x,y)
.= dist(id(V).x,id(V).y);
end;
end;
theorem
for V be non empty MetrStruct holds id(V) is onto isometric;
registration
let V be non empty MetrStruct;
cluster onto isometric for Function of V,V;
existence
proof
take f = id (the carrier of V);
thus rng f = the carrier of V;
let x,y be Element of V;
thus dist(x,y) = dist(f.x,y)
.= dist(f.x,f.y);
end;
end;
definition
let V be non empty MetrStruct;
defpred P[object] means $1 is onto isometric Function of V,V;
func ISOM(V) -> set means
:Def4:
for x be object holds x in it iff x is onto isometric Function of V,V;
existence
proof
consider X be set such that
A1: for x be object holds x in X iff x in Funcs(the carrier of V,the
carrier of V) & P[x] from XBOOLE_0:sch 1;
take X;
let x be object;
thus x in X implies x is onto isometric Function of V,V by A1;
assume
A2: x is onto isometric Function of V,V;
then x in Funcs(the carrier of V,the carrier of V) by FUNCT_2:8;
hence thesis by A1,A2;
end;
uniqueness
proof
thus for X1,X2 being set st
(for x being object holds x in X1 iff P[x]) & (
for x being object holds x in X2 iff P[x]) holds X1 = X2
from XBOOLE_0:sch 3;
end;
end;
definition
let V be non empty MetrStruct;
redefine func ISOM(V) -> Subset of Funcs(the carrier of V,the carrier of V); :: redefines ISOM (VECTMETR, definition)
coherence
proof
now
let x be object;
assume x in ISOM(V);
then x is Function of V,V by Def4;
hence x in Funcs(the carrier of V,the carrier of V) by FUNCT_2:8;
end;
hence thesis by TARSKI:def 3;
end;
end;
registration
let V be discerning Reflexive non empty MetrStruct;
cluster isometric -> one-to-one for Function of V,V;
coherence
proof
let f be Function of V,V;
assume
A1: f is isometric;
now
let x,y be object;
assume that
A2: x in dom f & y in dom f and
A3: f.x = f.y;
reconsider x1 = x, y1 = y as Element of V by A2;
dist(x1,y1) = dist(f.x1,f.y1) by A1
.= 0 by A3,METRIC_1:1;
hence x = y by METRIC_1:2;
end;
hence thesis by FUNCT_1:def 4;
end;
end;
registration
let V be discerning Reflexive non empty MetrStruct;
let f be onto isometric Function of V,V;
cluster f" -> onto isometric;
coherence
proof
A1: rng f = [#]V by FUNCT_2:def 3;
hence rng (f") = the carrier of V by TOPS_2:49;
let x,y be Element of V;
A2: rng f = the carrier of V by A1;
then
A3: dom (f") = [#]V by TOPS_2:49;
A4: y = (id rng f).y by A2
.= (f*f").y by A1,TOPS_2:52
.= f.(f".y) by A3,FUNCT_1:13;
x = (id rng f).x by A2
.= (f*f").x by A1,TOPS_2:52
.= f.(f".x) by A3,FUNCT_1:13;
hence thesis by A4,Def3;
end;
end;
registration
let V be non empty MetrStruct;
let f,g be onto isometric Function of V,V;
cluster f*g -> onto isometric for Function of V,V;
coherence
proof
f*g is onto isometric
proof
rng g = the carrier of V by FUNCT_2:def 3
.= dom f by FUNCT_2:def 1;
hence rng (f*g) = rng f by RELAT_1:28
.= the carrier of V by FUNCT_2:def 3;
let x,y be Element of V;
x in the carrier of V;
then
A1: x in dom g by FUNCT_2:def 1;
y in the carrier of V;
then
A2: y in dom g by FUNCT_2:def 1;
thus dist(x,y) = dist(g.x,g.y) by Def3
.= dist(f.(g.x),f.(g.y)) by Def3
.= dist((f*g).x,f.(g.y)) by A1,FUNCT_1:13
.= dist((f*g).x,(f*g).y) by A2,FUNCT_1:13;
end;
hence thesis;
end;
end;
registration
let V be non empty MetrStruct;
cluster ISOM V -> non empty;
coherence
proof
id(V) is onto isometric;
hence thesis by Def4;
end;
end;
begin :: Real Linear-Metric Spaces
definition
struct(RLSStruct,MetrStruct) RLSMetrStruct (# carrier -> set, distance ->
Function of [:the carrier,the carrier:],REAL, ZeroF -> Element of the carrier,
addF -> BinOp of the carrier, Mult -> Function of [:REAL, the carrier:],the
carrier #);
end;
registration
cluster non empty strict for RLSMetrStruct;
existence
proof
set X = the non empty set,F = the Function of [:X,X:],REAL,O = the Element of X
,B = the BinOp of X,G = the Function of [:REAL,X:],X;
take RLSMetrStruct (# X,F,O,B,G #);
thus the carrier of RLSMetrStruct (# X,F,O,B,G #) is non empty;
thus thesis;
end;
end;
registration
let X be non empty set;
let F be Function of [:X,X:],REAL;
let O be Element of X;
let B be BinOp of X;
let G be Function of [:REAL,X:],X;
cluster RLSMetrStruct (# X,F,O,B,G #) -> non empty;
coherence;
end;
definition
let V be non empty RLSMetrStruct;
attr V is homogeneous means
:Def5:
for r be Real for v,w be Element of V
holds dist(r*v,r*w) = |.r.| * dist(v,w);
end;
definition
let V be non empty RLSMetrStruct;
attr V is translatible means
:Def6:
for u,w,v be Element of V holds dist(v,w) = dist(v+u,w+u);
end;
definition
let V be non empty RLSMetrStruct;
let v be Element of V;
func Norm(v) -> Real equals
dist(0.V,v);
coherence;
end;
registration
cluster strict Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
Reflexive discerning symmetric triangle homogeneous
translatible for non empty RLSMetrStruct;
existence
proof
reconsider ZS = {0} as non empty set;
reconsider O = 0 as Element of ZS by TARSKI:def 1;
deffunc T((Element of ZS), Element of ZS) = In(0,REAL);
consider FF be Function of [:ZS,ZS:],REAL such that
A1: for x,y be Element of ZS holds FF.(x,y) = T(x,y) from BINOP_1:sch
4;
deffunc M(Real, Element of ZS) = O;
deffunc A((Element of ZS), Element of ZS) = O;
consider F be BinOp of ZS such that
A2: for x,y be Element of ZS holds F.(x,y) = A(x,y) from BINOP_1:sch 4;
consider G be Function of [:REAL,ZS:],ZS such that
A3: for a be Element of REAL for x be Element of ZS holds G.(a,x) = M(a,x)
from BINOP_1:sch 4;
A4: for a be Real for x be Element of ZS holds G.(a,x) = M(a,x)
proof let a be Real, x be Element of ZS;
reconsider a as Element of REAL by XREAL_0:def 1;
G.(a,x) = M(a,x) by A3;
hence thesis;
end;
set W = RLSMetrStruct (# ZS,FF,O,F,G #);
A5: for a,b be Real for x be VECTOR of W holds (a + b) * x = a * x
+ b * x
proof
let a,b be Real;
reconsider a,b as Real;
let x be VECTOR of W;
set c = a + b;
reconsider X = x as Element of ZS;
c * x = M(c,X) by A4;
hence thesis by A2;
end;
take W;
thus W is strict;
for x,y be VECTOR of W holds x + y = y + x
proof
let x,y be VECTOR of W;
reconsider X = x, Y = y as Element of ZS;
x + y = A(X,Y) by A2;
hence thesis by A2;
end;
hence W is Abelian;
for x,y,z be VECTOR of W holds (x + y) + z = x + (y + z)
proof
let x,y,z be VECTOR of W;
reconsider X = x, Y = y, Z = z as Element of ZS;
(x + y) + z = A(A(X,Y),Z) by A2;
hence thesis by A2;
end;
hence W is add-associative;
for x be VECTOR of W holds x + 0.W = x
proof
let x be VECTOR of W;
reconsider X = x as Element of ZS;
x + 0.W = A(X,O) by A2;
hence thesis by TARSKI:def 1;
end;
hence W is right_zeroed;
thus W is right_complementable
proof
reconsider y = O as VECTOR of W;
let x be VECTOR of W;
take y;
thus thesis by A2;
end;
A6: for a be Real for x,y be VECTOR of W holds a * (x + y) = a * x
+ a * y
proof
let a be Real;
reconsider a as Real;
let x,y be VECTOR of W;
reconsider X = x, Y = y as Element of ZS;
a * x + a * y = A(M(a,X),M(a,Y)) by A2;
hence thesis by A4;
end;
A7: for a,b be Real for x be VECTOR of W holds (a * b) * x = a * (
b * x)
proof
let a,b be Real;
reconsider a,b as Real;
let x be VECTOR of W;
set c = a * b;
reconsider X = x as Element of ZS;
c * x = M(c,X) by A4;
hence thesis by A4;
end;
for x be VECTOR of W holds 1 * x = x
proof
reconsider A9 = 1 as Element of REAL by XREAL_0:def 1;
let x be VECTOR of W;
reconsider X = x as Element of ZS;
1 * x = M(A9,X) by A4;
hence thesis by TARSKI:def 1;
end;
hence W is vector-distributive scalar-distributive scalar-associative
scalar-unital by A6,A5,A7;
A8: for a,b,c be Point of W holds dist (a,a) = 0 & (dist(a,b) = 0 implies
a=b) & dist(a,b) = dist(b,a) & dist(a,c)<=dist(a,b)+dist(b,c)
proof
let a,b,c be Point of W;
A9: dist(a,a) = FF.(a,a) by METRIC_1:def 1
.= 0 by A1;
hence dist(a,a) = 0;
A10: a = 0 by TARSKI:def 1;
hence dist(a,b) = 0 implies a = b by TARSKI:def 1;
A11: b = 0 by TARSKI:def 1;
hence dist(a,b) = dist(b,a) by A10;
thus thesis by A10,A11,A9;
end;
hence W is Reflexive by METRIC_1:1;
thus W is discerning by A8,METRIC_1:2;
thus W is symmetric by A8,METRIC_1:3;
thus W is triangle by A8,METRIC_1:4;
for r be Real for v,w be VECTOR of W holds dist(r*v,r*w) =
|.r.| * dist(v,w)
proof
let r be Real;
let v,w be VECTOR of W;
reconsider v1 = v, w1 = w as Element of ZS;
A12: FF.(v1,w1) = T(v1,w1) by A1;
thus dist(r*v,r*w) = FF.(r*v,r*w) by METRIC_1:def 1
.= |.r.| * 0 by A1
.= |.r.| * T(v1,w1)
.= |.r.| * FF.(v1,w1) by A12
.= |.r.| * dist(v,w) by METRIC_1:def 1;
end;
hence W is homogeneous;
for u,w,v be VECTOR of W holds dist(v,w) = dist(v + u,w + u)
proof
let u,w,v be VECTOR of W;
thus dist(v + u,w + u) = FF.(v + u,w + u) by METRIC_1:def 1
.= 0 by A1
.= FF.(v,w) by A1
.= dist(v,w) by METRIC_1:def 1;
end;
hence thesis;
end;
end;
definition
mode RealLinearMetrSpace is Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital Reflexive discerning symmetric
triangle homogeneous translatible non empty RLSMetrStruct;
end;
::$CT 3
theorem
for V be homogeneous Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty RLSMetrStruct for r be
Real for v be Element of V holds Norm (r * v) = |.r.| * Norm v
proof
let V be homogeneous Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty RLSMetrStruct;
let r be Real;
let v be Element of V;
thus Norm (r * v) = dist(r*(0.V),r * v) by RLVECT_1:10
.= |.r.| * Norm (v) by Def5;
end;
theorem
for V be translatible Abelian add-associative right_zeroed
right_complementable triangle non empty RLSMetrStruct for v,w be Element of V
holds Norm (v + w) <= Norm v + Norm w
proof
let V be translatible Abelian add-associative right_zeroed
right_complementable triangle non empty RLSMetrStruct;
let v,w be Element of V;
Norm (v + w) <= dist(0.V,v) + dist(v,v + w) by METRIC_1:4;
then Norm (v + w) <= Norm v + dist(v + -v,v + w + -v) by Def6;
then Norm (v + w) <= Norm v + dist(0.V,v + w + -v) by RLVECT_1:5;
then Norm (v + w) <= Norm v + dist(0.V,w + ((-v) + v)) by RLVECT_1:def 3;
then Norm (v + w) <= Norm v + dist(0.V,w + (0.V)) by RLVECT_1:5;
hence thesis by RLVECT_1:4;
end;
theorem
for V be translatible add-associative right_zeroed
right_complementable non empty RLSMetrStruct for v,w be Element of V holds
dist(v,w) = Norm (w - v)
proof
let V be translatible add-associative right_zeroed right_complementable non
empty RLSMetrStruct;
let v,w be Element of V;
thus dist(v,w) = dist(v + -v,w + -v) by Def6
.= Norm (w - v) by RLVECT_1:5;
end;
definition
let n be Element of NAT;
func RLMSpace n -> strict RealLinearMetrSpace means
:Def8:
the carrier of it = REAL n &
the distance of it = Pitag_dist n &
0.it = 0*n &
(for x,y be Element of REAL n holds (the addF of it).(x,y) = x + y) &
for x be Element of REAL n,r be Element of REAL holds
(the Mult of it).(r,x) = r * x;
existence
proof
deffunc G(Real, Element of REAL n) = $1*$2;
deffunc F(Element of REAL n, Element of REAL n) = $1+$2;
consider f be BinOp of REAL n such that
A1: for x,y be Element of REAL n holds f.(x,y) = F(x,y) from BINOP_1:
sch 4;
consider g be Function of [:REAL, REAL n:],REAL n such that
A2: for r be Element of REAL, x be Element of REAL n holds g.(r,x) = G(r,x)
from BINOP_1:sch 4;
set RLSMS = RLSMetrStruct (# REAL n, Pitag_dist n, 0*n, f, g #);
A3: for r be Real, x be Element of REAL n holds g.(r,x) = G(r,x)
proof let r be Real, x be Element of REAL n;
reconsider r as Element of REAL by XREAL_0:def 1;
g.(r,x) = G(r,x) by A2;
hence thesis;
end;
A4: now
let u,v,w be Element of RLSMS;
reconsider u1 = u, v1 = v, w1 = w as Element of REAL n;
thus (u + v) + w = f.(u1 + v1,w) by A1
.= (u1 + v1) + w1 by A1
.= u1 + (v1 + w1) by FINSEQOP:28
.= f.(u,v1 + w1) by A1
.= u + (v + w) by A1;
end;
A5: now
let v,w be Element of RLSMS;
reconsider v1 = v, w1 = w as Element of REAL n;
thus v + w = v1 + w1 by A1
.= w + v by A1;
end;
A6: now
let v be Element of RLSMS;
reconsider v1 = v as Element of n-tuples_on REAL;
thus v + 0.RLSMS = v1 + (n |-> In(0,REAL)) by A1
.= v by RVSUM_1:16;
end;
A7: now
let r be Real, v,w be VECTOR of RLSMS;
reconsider v1 = v, w1 = w as Element of REAL n;
reconsider v2 = v1, w2 = w1 as Element of n-tuples_on REAL;
A8: dist(v,w) = (Pitag_dist n).(v,w) by METRIC_1:def 1
.= |.v1 - w1.| by EUCLID:def 6;
A9: r * v = r * v1 & r * w = r * w1 by A3;
thus dist(r*v,r*w) = (Pitag_dist n).(r*v,r*w) by METRIC_1:def 1
.= |.r*v2 - r*w2.| by A9,EUCLID:def 6
.= |.r*v2 + (-1) * r * w2.| by RVSUM_1:49
.= |.r * v2 + r * (-w2).| by RVSUM_1:49
.= |.r*(v1 - w1).| by RVSUM_1:51
.= |.r.| * dist(v,w) by A8,EUCLID:11;
end;
A10: now
let u,w,v be VECTOR of RLSMS;
reconsider u1 = u, w1 = w, v1 = v as Element of REAL n;
reconsider u2 = u1, w2 = w1, v2 = v1 as Element of n-tuples_on REAL;
A11: v + u = v1 + u1 & w + u = w1 + u1 by A1;
thus dist(v,w) = (Pitag_dist n).(v,w) by METRIC_1:def 1
.= |.v1 - w1.| by EUCLID:def 6
.= |.(v2 + u2 - u2) - w2.| by RVSUM_1:42
.= |.(v2 + u2) - (u2 + w2).| by RVSUM_1:39
.= (Pitag_dist n).(v1 + u1,w1 + u1) by EUCLID:def 6
.= dist(v + u,w + u) by A11,METRIC_1:def 1;
end;
A12: RLSMS is right_complementable
proof
let v be Element of RLSMS;
reconsider v1 = v as Element of n-tuples_on REAL;
reconsider w = -v1 as Element of RLSMS;
take w;
thus v + w = v1 - v1 by A1
.= 0.RLSMS by RVSUM_1:37;
end;
A13: now
hereby
let a1 be Real, v,w be VECTOR of RLSMS;
reconsider a=a1 as Real;
reconsider v1 = v, w1 = w as Element of REAL n;
reconsider v2 = v1, w2 = w1 as Element of n-tuples_on REAL;
a * (v + w) = g.(a,v1 + w1) by A1
.= a * (v2 + w2) by A3
.= a * v1 + a * w1 by RVSUM_1:51
.= f.(a * v1,a * w1) by A1
.= f.(g.(a,v),a * w1) by A3
.= a * v + a * w by A3;
hence a1 * (v + w) = a1 * v + a1 * w;
end;
hereby
let a1,b1 be Real, v be VECTOR of RLSMS;
reconsider a=a1,b=b1 as Real;
reconsider v1 = v as Element of REAL n;
reconsider v2 = v1 as Element of n-tuples_on REAL;
(a + b) * v = (a + b) * v2 by A3
.= a * v1 + b * v1 by RVSUM_1:50
.= f.(a * v1,b * v1) by A1
.= f.(g.(a,v),b * v1) by A3
.= a * v + b * v by A3;
hence (a1 + b1) * v = a1 * v + b1 * v;
end;
hereby
let a1,b1 be Real, v be VECTOR of RLSMS;
reconsider a=a1,b=b1 as Real;
reconsider v1 = v as Element of REAL n;
reconsider v2 = v1 as Element of n-tuples_on REAL;
(a * b) * v = (a * b) * v2 by A3
.= a * (b * v1) by RVSUM_1:49
.= g.(a,b * v1) by A3
.= a * (b * v) by A3;
hence (a1 * b1) * v = a1 * (b1 * v);
end;
hereby
let v be VECTOR of RLSMS;
reconsider v1 = v as Element of n-tuples_on REAL;
thus 1 * v = 1 * v1 by A3
.= v by RVSUM_1:52;
end;
end;
A14: now
let a,b,c be VECTOR of RLSMS;
reconsider a1 = a, b1 = b, c1 = c as Element of REAL n;
thus dist(a,b) = 0 implies a = b
proof
assume dist(a,b) = 0;
then (Pitag_dist n).(a,b) = 0 by METRIC_1:def 1;
then |.a1 - b1.| = 0 by EUCLID:def 6;
hence thesis by EUCLID:16;
end;
A15: dist(a,c) = (Pitag_dist n).(a,c) by METRIC_1:def 1
.= |.a1 - c1.| by EUCLID:def 6;
|.a1 - a1.| = 0;
then (Pitag_dist n).(a,a) = 0 by EUCLID:def 6;
hence dist(a,a) = 0 by METRIC_1:def 1;
thus dist(a,b) = (Pitag_dist n).(a,b) by METRIC_1:def 1
.= |.a1 - b1.| by EUCLID:def 6
.= |.b1 - a1.| by EUCLID:18
.= (Pitag_dist n).(b,a) by EUCLID:def 6
.= dist(b,a) by METRIC_1:def 1;
A16: dist(b,c) = (Pitag_dist n).(b,c) by METRIC_1:def 1
.= |.b1 - c1.| by EUCLID:def 6;
dist(a,b) = (Pitag_dist n).(a,b) by METRIC_1:def 1
.= |.a1 - b1.| by EUCLID:def 6;
hence dist(a,c) <= dist(a,b) + dist(b,c) by A15,A16,EUCLID:19;
end;
reconsider RLSMS as strict Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital
non empty RLSMetrStruct by A5,A4,A6,A12,A13,RLVECT_1:def 2,def 3,def 4,def 5
,def 6,def 7,def 8;
reconsider RLSMS as strict RealLinearMetrSpace by A14,A7,A10,Def5,Def6,
METRIC_1:1,2,3,4;
take RLSMS;
thus thesis by A1,A3;
end;
uniqueness
proof
let V1,V2 be strict RealLinearMetrSpace such that
A17: the carrier of V1 = REAL n and
A18: the distance of V1 = Pitag_dist n & 0.V1 = 0*n and
A19: for x,y be Element of REAL n holds (the addF of V1).(x,y) = x + y and
A20: for x be Element of REAL n,r be Element of REAL holds (the Mult
of V1).(r,x) = r*x and
A21: the carrier of V2 = REAL n and
A22: the distance of V2 = Pitag_dist n & 0.V2 = 0*n and
A23: for x,y be Element of REAL n holds (the addF of V2).(x,y) = x + y and
A24: for x be Element of REAL n,r be Element of REAL holds (the Mult
of V2).(r,x) = r*x;
now
let x,y be Element of V1;
reconsider x1 = x, y1 = y as Element of REAL n by A17;
thus (the addF of V1).(x,y) = x1 + y1 by A19
.= (the addF of V2).(x,y) by A23;
end;
then
A25: the addF of V1 = the addF of V2 by A17,A21,BINOP_1:2;
now
let r be Element of REAL, x be Element of V1;
reconsider x1 = x as Element of REAL n by A17;
thus (the Mult of V1).(r,x) = r*x1 by A20
.= (the Mult of V2).(r,x) by A24;
end;
hence thesis by A17,A18,A21,A22,A25,BINOP_1:2;
end;
end;
theorem
for n be Element of NAT for f be onto isometric Function of RLMSpace n,
RLMSpace n holds rng f = REAL n
proof
let n be Element of NAT;
let f be onto isometric Function of RLMSpace n,RLMSpace n;
thus rng f = the carrier of RLMSpace n by FUNCT_2:def 3
.= REAL n by Def8;
end;
begin :: Groups of Onto Isometric Functions
definition
let n be Element of NAT;
func IsomGroup n -> strict multMagma means
:Def9:
the carrier of it = ISOM RLMSpace n &
for f,g be Function st f in ISOM RLMSpace n & g in ISOM RLMSpace n
holds (the multF of it).(f,g) = f*g;
existence
proof
defpred P[set, set, set] means ex f,g be Function st f = $1 & g = $2 & $3
= f*g;
A1: for x,y be Element of ISOM RLMSpace n ex z be Element of ISOM RLMSpace
n st P[x,y,z]
proof
let x,y be Element of ISOM RLMSpace n;
reconsider x1=x as onto isometric Function of RLMSpace n,RLMSpace n
by Def4;
reconsider y1=y as onto isometric Function of RLMSpace n,RLMSpace n
by Def4;
reconsider z = x1*y1 as Element of ISOM RLMSpace n by Def4;
take z;
take x1,y1;
thus thesis;
end;
consider o be BinOp of ISOM RLMSpace n such that
A2: for a,b be Element of ISOM RLMSpace n holds P[a,b, o.(a,b)] from
BINOP_1:sch 3(A1);
take G = multMagma(#ISOM RLMSpace n,o#);
for f,g be Function st f in ISOM RLMSpace n & g in ISOM RLMSpace n
holds (the multF of G).(f,g) = f*g
proof
let f,g be Function;
assume f in ISOM RLMSpace n & g in ISOM RLMSpace n;
then ex f1,g1 be Function st f1 = f & g1 = g & o.(f,g) = f1* g1 by A2;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
set V = RLMSpace n;
let G1,G2 be strict multMagma such that
A3: the carrier of G1 = ISOM V and
A4: for f,g be Function st f in ISOM V & g in ISOM V holds (the multF
of G1).(f,g) = f*g and
A5: the carrier of G2 = ISOM V and
A6: for f,g be Function st f in ISOM V & g in ISOM V holds (the multF
of G2).(f,g) = f*g;
now
let f,g be Element of G1;
reconsider f1=f as Function of RLMSpace n,RLMSpace n by A3,Def4;
reconsider g1=g as Function of RLMSpace n,RLMSpace n by A3,Def4;
thus (the multF of G1).(f,g) = f1*g1 by A3,A4
.= (the multF of G2).(f,g) by A3,A6;
end;
hence thesis by A3,A5,BINOP_1:2;
end;
end;
registration
let n be Element of NAT;
cluster IsomGroup n -> non empty;
coherence
proof
the carrier of IsomGroup n = ISOM RLMSpace n by Def9;
hence thesis;
end;
end;
registration
let n be Element of NAT;
cluster IsomGroup n -> associative Group-like;
coherence
proof
now
let x,y,z be Element of IsomGroup n;
x in the carrier of IsomGroup n;
then
A1: x in ISOM RLMSpace n by Def9;
then reconsider x1=x as onto isometric Function of RLMSpace n,RLMSpace n
by Def4;
y in the carrier of IsomGroup n;
then
A2: y in ISOM RLMSpace n by Def9;
then reconsider y1=y as onto isometric Function of RLMSpace n,RLMSpace n
by Def4;
A3: x1*y1 in ISOM RLMSpace n by Def4;
z in the carrier of IsomGroup n;
then
A4: z in ISOM RLMSpace n by Def9;
then reconsider z1=z as onto isometric Function of RLMSpace n,RLMSpace n
by Def4;
A5: y1*z1 in ISOM RLMSpace n by Def4;
thus (x*y)*z = (the multF of IsomGroup n).(x1*y1,z) by A1,A2,Def9
.= (x1*y1)*z1 by A4,A3,Def9
.= x1*(y1*z1) by RELAT_1:36
.= (the multF of IsomGroup n).(x,y1*z1) by A1,A5,Def9
.= x*(y*z) by A2,A4,Def9;
end;
hence IsomGroup n is associative by GROUP_1:def 3;
ex e be Element of IsomGroup n st for h be Element of IsomGroup n
holds h * e = h & e * h = h & ex g be Element of IsomGroup n st h * g = e & g *
h = e
proof
A6: id(RLMSpace n) in ISOM RLMSpace n by Def4;
then reconsider e = id(RLMSpace n) as Element of IsomGroup n by Def9;
take e;
let h be Element of IsomGroup n;
h in the carrier of IsomGroup n;
then
A7: h in ISOM RLMSpace n by Def9;
then reconsider h1=h as onto isometric Function of RLMSpace n,RLMSpace n
by Def4;
thus h * e = h1*id(the carrier of RLMSpace n) by A6,A7,Def9
.= h by FUNCT_2:17;
thus e * h = id(the carrier of RLMSpace n)*h1 by A6,A7,Def9
.= h by FUNCT_2:17;
A8: rng h1 = [#](RLMSpace n) by FUNCT_2:def 3;
A9: h1" in ISOM RLMSpace n by Def4;
then reconsider g = h1" as Element of IsomGroup n by Def9;
take g;
thus h * g = h1*h1" by A7,A9,Def9
.= e by A8,TOPS_2:52;
thus g * h = h1"*h1 by A7,A9,Def9
.= id dom h1 by A8,TOPS_2:52
.= e by FUNCT_2:def 1;
end;
hence thesis by GROUP_1:def 2;
end;
end;
theorem Th7:
for n be Element of NAT holds 1_IsomGroup n = id (RLMSpace n)
proof
let n be Element of NAT;
A1: id(RLMSpace n) in ISOM RLMSpace n by Def4;
then reconsider e = id(RLMSpace n) as Element of IsomGroup n by Def9;
now
let h be Element of IsomGroup n;
h in the carrier of IsomGroup n;
then
A2: h in ISOM RLMSpace n by Def9;
then reconsider h1=h as Function of RLMSpace n,RLMSpace n by Def4;
thus h * e = h1*id(the carrier of RLMSpace n) by A1,A2,Def9
.= h by FUNCT_2:17;
thus e * h = id(the carrier of RLMSpace n)*h1 by A1,A2,Def9
.= h by FUNCT_2:17;
end;
hence thesis by GROUP_1:4;
end;
theorem Th8:
for n be Element of NAT for f be Element of IsomGroup n for g be
Function of RLMSpace n,RLMSpace n st f = g holds f" = g"
proof
let n be Element of NAT;
let f be Element of IsomGroup n;
let g be Function of RLMSpace n,RLMSpace n;
f in the carrier of IsomGroup n;
then
A1: f in ISOM RLMSpace n by Def9;
then reconsider f1=f as onto isometric Function of RLMSpace n,RLMSpace n
by Def4;
assume
A2: f = g;
then f1 = g;
then
A3: g" in ISOM RLMSpace n by Def4;
then reconsider g1 = g" as Element of IsomGroup n by Def9;
A4: rng f1 = [#](RLMSpace n) by FUNCT_2:def 3;
A5: g1 * f = g"*f1 by A1,A3,Def9
.= id dom f1 by A2,A4,TOPS_2:52
.= id(RLMSpace n) by FUNCT_2:def 1
.= 1_IsomGroup n by Th7;
f * g1 = f1*g" by A1,A3,Def9
.= id(RLMSpace n) by A2,A4,TOPS_2:52
.= 1_IsomGroup n by Th7;
hence thesis by A5,GROUP_1:5;
end;
definition
let n be Element of NAT;
let G be Subgroup of IsomGroup n;
func SubIsomGroupRel G -> Relation of the carrier of RLMSpace n means
:Def10:
for A,B be Element of RLMSpace n holds [A,B] in it iff ex f be Function st f
in the carrier of G & f.A = B;
existence
proof
defpred P[object, object] means
ex f be Function st f in the carrier of G & f.$1
= $2;
consider R be Relation of the carrier of RLMSpace n,the carrier of
RLMSpace n such that
A1: for x,y be object holds [x,y] in R iff x in the carrier of RLMSpace n
& y in the carrier of RLMSpace n & P[x,y] from RELSET_1:sch 1;
take R;
let A,B be Element of RLMSpace n;
thus thesis by A1;
end;
uniqueness
proof
let R1,R2 be Relation of the carrier of RLMSpace n such that
A2: for A,B be Element of RLMSpace n holds [A,B] in R1 iff ex f be
Function st f in the carrier of G & f.A = B and
A3: for A,B be Element of RLMSpace n holds [A,B] in R2 iff ex f be
Function st f in the carrier of G & f.A = B;
now
let a,b be object;
thus [a,b] in R1 implies [a,b] in R2
proof
assume
A4: [a,b] in R1;
then reconsider a1 = a, b1 = b as Element of RLMSpace n by ZFMISC_1:87;
ex f be Function st f in the carrier of G & f.a1 = b1 by A2,A4;
hence thesis by A3;
end;
assume
A5: [a,b] in R2;
then reconsider a1 = a, b1 = b as Element of RLMSpace n by ZFMISC_1:87;
ex f be Function st f in the carrier of G & f.a1 = b1 by A3,A5;
hence [a,b] in R1 by A2;
end;
hence R1 = R2 by RELAT_1:def 2;
end;
end;
registration
let n be Element of NAT;
let G be Subgroup of IsomGroup n;
cluster SubIsomGroupRel G -> total symmetric transitive;
coherence
proof
set S = SubIsomGroupRel G;
set X = the carrier of RLMSpace n;
now
let x be object;
assume x in X;
then reconsider x1 = x as Element of RLMSpace n;
1_IsomGroup n = id (RLMSpace n) by Th7;
then id(RLMSpace n) in G by GROUP_2:46;
then
A1: id(RLMSpace n) in the carrier of G;
id(RLMSpace n).x1 = x1;
hence [x,x] in S by A1,Def10;
end;
then
A2: S is_reflexive_in X by RELAT_2:def 1;
then
A3: field S = X by ORDERS_1:13;
dom S = X by A2,ORDERS_1:13;
hence S is total by PARTFUN1:def 2;
now
let x,y be object;
assume that
A4: x in X & y in X and
A5: [x,y] in S;
reconsider x1 = x, y1 = y as Element of RLMSpace n by A4;
consider f be Function such that
A6: f in the carrier of G and
A7: f.x1 = y1 by A5,Def10;
reconsider f1 = f as Element of G by A6;
A8: the carrier of G c= the carrier of IsomGroup n by GROUP_2:def 5;
then reconsider f3 = f1 as Element of IsomGroup n;
f in the carrier of IsomGroup n by A6,A8;
then f in ISOM RLMSpace n by Def9;
then reconsider f2=f as onto isometric Function of RLMSpace n,RLMSpace n
by Def4;
x1 in the carrier of RLMSpace n;
then x1 in dom f2 by FUNCT_2:def 1;
then
A9: f".y1 = x1 by A7,FUNCT_1:34;
f1" = f3" by GROUP_2:48
.= f2" by Th8
.= f" by TOPS_2:def 4;
hence [y,x] in S by A9,Def10;
end;
then S is_symmetric_in X by RELAT_2:def 3;
hence S is symmetric by A3,RELAT_2:def 11;
now
let x,y,z be object;
assume that
A10: x in X & y in X & z in X and
A11: [x,y] in S and
A12: [y,z] in S;
reconsider x1 = x, y1 = y, z1 = z as Element of RLMSpace n by A10;
consider f be Function such that
A13: f in the carrier of G and
A14: f.x1 = y1 by A11,Def10;
reconsider f2 = f as Element of G by A13;
A15: the carrier of G c= the carrier of IsomGroup n by GROUP_2:def 5;
then reconsider f3 = f2 as Element of IsomGroup n;
f in the carrier of IsomGroup n by A13,A15;
then
A16: f in ISOM RLMSpace n by Def9;
consider g be Function such that
A17: g in the carrier of G and
A18: g.y1 = z1 by A12,Def10;
reconsider g2 = g as Element of G by A17;
A19: x1 in the carrier of RLMSpace n;
reconsider g3 = g2 as Element of IsomGroup n by A15;
f2 in G & g2 in G;
then
A20: g3*f3 in G by GROUP_2:50;
g in the carrier of IsomGroup n by A17,A15;
then g in ISOM RLMSpace n by Def9;
then g3*f3 = g*f by A16,Def9;
then
A21: g*f in the carrier of G by A20;
f is onto isometric Function of RLMSpace n,RLMSpace n by A16,Def4;
then x1 in dom f by A19,FUNCT_2:def 1;
then (g*f).x1 = z1 by A14,A18,FUNCT_1:13;
hence [x,z] in S by A21,Def10;
end;
then S is_transitive_in X by RELAT_2:def 8;
hence thesis by A3,RELAT_2:def 16;
end;
end;