:: Real Linear-Metric Space and Isometric Functions :: by Robert Milewski :: :: Received November 3, 1998 :: Copyright (c) 1998-2019 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); 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;