:: VECTMETR semantic presentation begin definition let V be non empty MetrStruct ; attrV is convex means :Def1: :: VECTMETR:def 1 for x, y being Element of V for r being Real st 0 <= r & r <= 1 holds ex z being Element of V st ( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) ); end; :: deftheorem Def1 defines convex VECTMETR:def_1_:_ for V being non empty MetrStruct holds ( V is convex iff for x, y being Element of V for r being Real st 0 <= r & r <= 1 holds ex z being Element of V st ( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) ) ); definition let V be non empty MetrStruct ; attrV is internal means :: VECTMETR:def 2 for x, y being Element of V for p, q being Real st p > 0 & q > 0 holds ex f being FinSequence of the carrier of V st ( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) holds abs ((dist (x,y)) - (Sum F)) < q ) ); end; :: deftheorem defines internal VECTMETR:def_2_:_ for V being non empty MetrStruct holds ( V is internal iff for x, y being Element of V for p, q being Real st p > 0 & q > 0 holds ex f being FinSequence of the carrier of V st ( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) holds abs ((dist (x,y)) - (Sum F)) < q ) ) ); theorem Th1: :: VECTMETR:1 for V being non empty MetrSpace st V is convex holds for x, y being Element of V for p being Real st p > 0 holds ex f being FinSequence of the carrier of V st ( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being 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; ::_thesis: ( V is convex implies for x, y being Element of V for p being Real st p > 0 holds ex f being FinSequence of the carrier of V st ( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) holds dist (x,y) = Sum F ) ) ) assume A1: V is convex ; ::_thesis: for x, y being Element of V for p being Real st p > 0 holds ex f being FinSequence of the carrier of V st ( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) holds dist (x,y) = Sum F ) ) set A = the carrier of V; let x, y be Element of V; ::_thesis: for p being Real st p > 0 holds ex f being FinSequence of the carrier of V st ( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) holds dist (x,y) = Sum F ) ) defpred S1[ set , set , set ] means for a1, a2 being Element of the carrier of V st $1 = [a1,a2] holds ex b being Element of the carrier of V st ( $2 = [a1,b] & $3 = [b,a2] & dist (a1,a2) = 2 * (dist (a1,b)) & dist (a1,a2) = 2 * (dist (b,a2)) ); A2: for a being Element of [: the carrier of V, the carrier of V:] ex c, d being Element of [: the carrier of V, the carrier of V:] st S1[a,c,d] proof let a be Element of [: the carrier of V, the carrier of V:]; ::_thesis: ex c, d being Element of [: the carrier of V, the carrier of V:] st S1[a,c,d] consider a19, a29 being set such that A3: ( a19 in the carrier of V & a29 in the carrier of V ) and A4: a = [a19,a29] by ZFMISC_1:def_2; reconsider a19 = a19, a29 = a29 as Element of the carrier of V by A3; consider z being Element of the carrier of V such that A5: dist (a19,z) = (1 / 2) * (dist (a19,a29)) and A6: dist (z,a29) = (1 - (1 / 2)) * (dist (a19,a29)) by A1, Def1; take c = [a19,z]; ::_thesis: ex d being Element of [: the carrier of V, the carrier of V:] st S1[a,c,d] take d = [z,a29]; ::_thesis: S1[a,c,d] let a1, a2 be Element of the carrier of V; ::_thesis: ( a = [a1,a2] implies ex b being Element of the carrier of V st ( c = [a1,b] & d = [b,a2] & dist (a1,a2) = 2 * (dist (a1,b)) & dist (a1,a2) = 2 * (dist (b,a2)) ) ) assume A7: a = [a1,a2] ; ::_thesis: ex b being Element of the carrier of V st ( c = [a1,b] & d = [b,a2] & dist (a1,a2) = 2 * (dist (a1,b)) & dist (a1,a2) = 2 * (dist (b,a2)) ) take z ; ::_thesis: ( c = [a1,z] & d = [z,a2] & dist (a1,a2) = 2 * (dist (a1,z)) & dist (a1,a2) = 2 * (dist (z,a2)) ) thus c = [a1,z] by A4, A7, XTUPLE_0:1; ::_thesis: ( d = [z,a2] & dist (a1,a2) = 2 * (dist (a1,z)) & dist (a1,a2) = 2 * (dist (z,a2)) ) thus d = [z,a2] by A4, A7, XTUPLE_0:1; ::_thesis: ( dist (a1,a2) = 2 * (dist (a1,z)) & dist (a1,a2) = 2 * (dist (z,a2)) ) a1 = a19 by A4, A7, XTUPLE_0:1; hence dist (a1,a2) = 2 * (dist (a1,z)) by A4, A5, A7, XTUPLE_0:1; ::_thesis: dist (a1,a2) = 2 * (dist (z,a2)) a2 = a29 by A4, A7, XTUPLE_0:1; hence dist (a1,a2) = 2 * (dist (z,a2)) by A4, A6, A7, XTUPLE_0:1; ::_thesis: verum end; consider D being binary DecoratedTree of [: the carrier of V, the carrier of V:] such that A8: dom D = {0,1} * and A9: D . {} = [x,y] and A10: for z being Node of D holds S1[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; ::_thesis: ( p > 0 implies ex f being FinSequence of the carrier of V st ( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) holds dist (x,y) = Sum F ) ) ) assume A11: p > 0 ; ::_thesis: ex f being FinSequence of the carrier of V st ( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) holds dist (x,y) = Sum F ) ) percases ( dist (x,y) >= p or dist (x,y) < p ) ; suppose dist (x,y) >= p ; ::_thesis: ex f being FinSequence of the carrier of V st ( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) holds dist (x,y) = Sum F ) ) 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 S2[ Nat] means for t being Tuple of $1, BOOLEAN st t = 0* $1 holds (D . ('not' t)) `2 = y; defpred S3[ Element of NAT ] means (D . (0* $1)) `1 = x; reconsider n = n1 + 1 as non empty Element of NAT ; reconsider N = 2 to_power n as non empty 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 H1( Nat) -> Element of [: the carrier of V, the carrier of V:] = D . (FSL /. $1); consider g being FinSequence of [: the carrier of V, the carrier of V:] such that A12: len g = N and A13: for k being Nat st k in dom g holds g . k = H1(k) from FINSEQ_2:sch_1(); A14: dom g = Seg N by A12, FINSEQ_1:def_3; A15: for j being Element of NAT st S3[j] holds S3[j + 1] proof let j be Element of NAT ; ::_thesis: ( S3[j] implies S3[j + 1] ) assume A16: (D . (0* j)) `1 = x ; ::_thesis: S3[j + 1] reconsider zj = 0* j as Node of D by A8, BINARI_3:4; consider a, b being set such that A17: ( a in the carrier of V & b in the carrier of V ) and A18: D . zj = [a,b] by ZFMISC_1:def_2; reconsider a1 = a, b1 = b as Element of the carrier of V by A17; A19: ex z1 being Element of the carrier of V 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, MCART_1:7 .= x by A18, A16, MCART_1:7 ; ::_thesis: verum end; A20: S3[ 0 ] by A9, MCART_1:7; A21: for j being Element of NAT holds S3[j] from NAT_1:sch_1(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 being non empty Nat st S2[j] holds S2[j + 1] proof let j be non empty Nat; ::_thesis: ( S2[j] implies S2[j + 1] ) assume A24: for t being Tuple of j, BOOLEAN st t = 0* j holds (D . ('not' t)) `2 = y ; ::_thesis: S2[j + 1] let t be Tuple of j + 1, BOOLEAN ; ::_thesis: ( t = 0* (j + 1) implies (D . ('not' t)) `2 = y ) consider t1 being Element of j -tuples_on BOOLEAN, dd being Element of BOOLEAN such that A25: t = t1 ^ <*dd*> by FINSEQ_2:117; assume A26: t = 0* (j + 1) ; ::_thesis: (D . ('not' t)) `2 = y 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) . (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 being set such that A29: ( a in the carrier of V & b in the carrier of V ) and A30: D . nt1 = [a,b] by ZFMISC_1:def_2; reconsider a1 = a, b1 = b as Element of the carrier of V by A29; ex b being Element of the carrier of V 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, MCART_1:7 .= y by A30, A27, MCART_1:7 ; ::_thesis: verum end; A31: S2[1] proof reconsider pusty = <*> {0,1} as Node of D by A8, FINSEQ_1:def_11; let t be Tuple of 1, BOOLEAN ; ::_thesis: ( t = 0* 1 implies (D . ('not' t)) `2 = y ) A32: ex b being Element of the carrier of V 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 ; ::_thesis: (D . ('not' t)) `2 = y 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, MCART_1:7 ; ::_thesis: verum end; A33: for j being non empty Nat holds S2[j] from NAT_1:sch_10(A31, A23); deffunc H2( Nat) -> Element of the carrier of V = (g /. $1) `1 ; consider h being FinSequence of the carrier of V such that A34: len h = N and A35: for k being Nat st k in dom h holds h . k = H2(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*>; ::_thesis: ( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) holds dist (x,y) = Sum F ) ) 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 ; ::_thesis: ( f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) holds dist (x,y) = Sum F ) ) 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 ; ::_thesis: ( ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) holds dist (x,y) = Sum F ) ) A42: for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) = (dist (x,y)) / N 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 = ze as Element of n -tuples_on BOOLEAN by FINSEQ_2:131; defpred S4[ non empty Nat] means for j being non empty Element of NAT st j <= 2 to_power $1 holds for DF1, DF2 being 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 ; ::_thesis: ( 1 <= i & i <= (len f) - 1 implies dist ((f /. i),(f /. (i + 1))) = (dist (x,y)) / N ) assume that A43: 1 <= i and A44: i <= (len f) - 1 ; ::_thesis: dist ((f /. i),(f /. (i + 1))) = (dist (x,y)) / N A45: len FSL = N by BINTREE2:19; A46: now__::_thesis:_f_/._(i_+_1)_=_(D_._((FinSeqLevel_(n,dD))_._i))_`2 percases ( i < (len f) - 1 or i = (len f) - 1 ) by A44, XXREAL_0:1; suppose i < (len f) - 1 ; ::_thesis: f /. (i + 1) = (D . ((FinSeqLevel (n,dD)) . i)) `2 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 S5[ non empty Nat] means for i being 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 being non empty Nat st S5[n] holds S5[n + 1] proof let n be non empty Nat; ::_thesis: ( S5[n] implies S5[n + 1] ) reconsider nn = n as non empty Element of NAT by ORDINAL1:def_12; reconsider zb = dD -level n as non empty set by A8, BINTREE2:10; assume A50: for i being Nat st 1 <= i & i <= (2 to_power n) - 1 holds (D . ((FinSeqLevel (n,dD)) . (i + 1))) `1 = (D . ((FinSeqLevel (n,dD)) . i)) `2 ; ::_thesis: S5[n + 1] let i be Nat; ::_thesis: ( 1 <= i & i <= (2 to_power (n + 1)) - 1 implies (D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ((n + 1),dD)) . i)) `2 ) assume that A51: 1 <= i and A52: i <= (2 to_power (n + 1)) - 1 ; ::_thesis: (D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ((n + 1),dD)) . i)) `2 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 = 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 being set such that A59: ( a9 in the carrier of V & b9 in the carrier of V ) 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 = 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 being set such that A61: ( a in the carrier of V & b in the carrier of V ) and A62: D . F1 = [a,b] by ZFMISC_1:def_2; reconsider a1 = a, b1 = b, a19 = a9, b19 = b9 as Element of the carrier of V by A61, A59; consider d being Element of the carrier of V 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 being Element of the carrier of V 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__::_thesis:_(D_._((FinSeqLevel_((n_+_1),dD))_._(i_+_1)))_`1_=_(D_._((FinSeqLevel_((n_+_1),dD))_._ii))_`2 percases ( i is odd or i is even ) ; suppose i is odd ; ::_thesis: (D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ((n + 1),dD)) . ii)) `2 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, MCART_1:7 .= (D . (F ^ <*0*>)) `2 by A63, MCART_1:7 .= (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 ; ::_thesis: verum end; suppose i is even ; ::_thesis: (D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ((n + 1),dD)) . ii)) `2 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, MCART_1:7 .= (D . ((FinSeqLevel (n,dD)) . ((i + 1) div 2))) `2 by A50, A54, A74, A75 .= b by A62, MCART_1:7 ; 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, MCART_1:7 .= (D . (F ^ <*1*>)) `2 by A64, A76, MCART_1:7 .= (D . ((FinSeqLevel ((n + 1),dD)) . ii)) `2 by A51, A56, A71, BINTREE2:24 ; ::_thesis: verum end; end; end; hence (D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ((n + 1),dD)) . i)) `2 ; ::_thesis: verum end; A77: S5[1] proof reconsider pusty = <*> {0,1} as Node of D by A8, FINSEQ_1:def_11; let i be Nat; ::_thesis: ( 1 <= i & i <= (2 to_power 1) - 1 implies (D . ((FinSeqLevel (1,dD)) . (i + 1))) `1 = (D . ((FinSeqLevel (1,dD)) . i)) `2 ) A78: (2 to_power 1) - 1 = (1 + 1) - 1 by POWER:25 .= 1 ; consider b being Element of the carrier of V 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 ) ; ::_thesis: (D . ((FinSeqLevel (1,dD)) . (i + 1))) `1 = (D . ((FinSeqLevel (1,dD)) . i)) `2 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, MCART_1:7 .= (D . (pusty ^ <*0*>)) `2 by A79, MCART_1:7 .= (D . <*0*>) `2 by FINSEQ_1:34 .= (D . ((FinSeqLevel (1,dD)) . i)) `2 by A81, BINTREE2:22 ; ::_thesis: verum end; A82: for n being non empty Nat holds S5[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 ; ::_thesis: verum end; supposeA85: i = (len f) - 1 ; ::_thesis: f /. (i + 1) = (D . ((FinSeqLevel (n,dD)) . i)) `2 hence f /. (i + 1) = (D . ('not' ze)) `2 by A33, A41 .= (D . ((FinSeqLevel (n,dD)) . i)) `2 by A34, A40, A85, BINTREE2:16 ; ::_thesis: verum end; end; end; A86: for l being non empty Nat st S4[l] holds S4[l + 1] proof let l be non empty Nat; ::_thesis: ( S4[l] implies S4[l + 1] ) reconsider dDll = dD -level l as non empty set by A8, BINTREE2:10; reconsider ll = l as non empty 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 being non empty Element of NAT st j <= 2 to_power l holds for DF1, DF2 being 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) ; ::_thesis: S4[l + 1] let j be non empty Element of NAT ; ::_thesis: ( j <= 2 to_power (l + 1) implies for DF1, DF2 being Element of V st DF1 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `2 holds dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1)) ) (j + 1) div 2 <> 0 proof assume (j + 1) div 2 = 0 ; ::_thesis: contradiction then j + 1 < 1 + 1 by NAT_2:12; then j < 1 by XREAL_1:6; hence contradiction by NAT_1:14; ::_thesis: verum end; then reconsider j1 = (j + 1) div 2 as non empty Element of NAT ; assume A88: j <= 2 to_power (l + 1) ; ::_thesis: for DF1, DF2 being Element of V st DF1 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `2 holds dist (DF1,DF2) = (dist (x,y)) / (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 = 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 being Element of l -tuples_on BOOLEAN, d being Element of BOOLEAN such that A92: FSLl1 = FSLl ^ <*d*> by FINSEQ_2:117; let DF1, DF2 be Element of V; ::_thesis: ( DF1 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `2 implies dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1)) ) assume ( DF1 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `2 ) ; ::_thesis: dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1)) 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 being set such that A94: ( x1 in the carrier of V & y1 in the carrier of V ) and A95: D . NFSLl = [x1,y1] by ZFMISC_1:def_2; reconsider x1 = x1, y1 = y1 as Element of the carrier of V by A94; consider b being Element of the carrier of V 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, MCART_1:7; A102: d = (j + 1) mod 2 by A92, A100, FINSEQ_2:17; now__::_thesis:_dist_(DF1,DF2)_=_(dist_(x,y))_/_(2_to_power_(l_+_1)) percases ( d = 0 or d = 1 ) by A102, NAT_D:12; suppose d = 0 ; ::_thesis: dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1)) 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 ; ::_thesis: verum end; suppose d = 1 ; ::_thesis: dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 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 ; ::_thesis: verum end; end; end; hence dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1)) ; ::_thesis: verum end; A103: S4[1] proof reconsider pusty = <*> {0,1} as Node of D by A8, FINSEQ_1:def_11; let j be non empty Element of NAT ; ::_thesis: ( j <= 2 to_power 1 implies for DF1, DF2 being 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) ) assume A104: j <= 2 to_power 1 ; ::_thesis: for DF1, DF2 being 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) 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; ::_thesis: ( DF1 = (D . ((FinSeqLevel (1,dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel (1,dD)) . j)) `2 implies dist (DF1,DF2) = (dist (x,y)) / (2 to_power 1) ) assume A106: ( DF1 = (D . ((FinSeqLevel (1,dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel (1,dD)) . j)) `2 ) ; ::_thesis: dist (DF1,DF2) = (dist (x,y)) / (2 to_power 1) ( 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__::_thesis:_dist_(DF1,DF2)_=_(dist_(x,y))_/_2 percases ( j = 1 or j = 2 ) by A107, FINSEQ_1:2, TARSKI:def_2; supposeA108: j = 1 ; ::_thesis: dist (DF1,DF2) = (dist (x,y)) / 2 A109: ex b being Element of the carrier of V 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; ::_thesis: verum end; supposeA111: j = 2 ; ::_thesis: dist (DF1,DF2) = (dist (x,y)) / 2 consider b being Element of the carrier of V 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; ::_thesis: verum end; end; end; hence dist (DF1,DF2) = (dist (x,y)) / (2 to_power 1) by POWER:25; ::_thesis: verum end; A115: for l being non empty Nat holds S4[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 dist ((f /. i),(f /. (i + 1))) = (dist (x,y)) / N by A34, A40, A43, A44, A46, A115; ::_thesis: verum 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 (dist (x,y)) / N < p by XCMPLX_1:87; hence for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p by A42; ::_thesis: for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) holds dist (x,y) = Sum F let F be FinSequence of REAL ; ::_thesis: ( len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) implies dist (x,y) = Sum F ) assume that A117: len F = (len f) - 1 and A118: for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ; ::_thesis: dist (x,y) = Sum F A119: rng F = {((dist (x,y)) / N)} proof thus rng F c= {((dist (x,y)) / N)} :: according to XBOOLE_0:def_10 ::_thesis: {((dist (x,y)) / N)} c= rng F proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng F or a in {((dist (x,y)) / N)} ) assume a in rng F ; ::_thesis: a in {((dist (x,y)) / N)} then consider c being set 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 Element of NAT : ( 1 <= t & t <= len F ) } by FINSEQ_1:def_1; then consider c1 being Element of NAT such that A122: c1 = c and A123: ( 1 <= c1 & c1 <= len F ) ; a = F /. c1 by A121, A122, A123, FINSEQ_4:15 .= dist ((f /. c1),(f /. (c1 + 1))) by A118, A123 .= (dist (x,y)) / N by A42, A117, A123 ; hence a in {((dist (x,y)) / N)} by TARSKI:def_1; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {((dist (x,y)) / N)} or a in rng F ) assume a in {((dist (x,y)) / N)} ; ::_thesis: a in rng F then a = (dist (x,y)) / N 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 a in rng F by A124, FUNCT_1:def_3; ::_thesis: verum end; dom F = Seg (len F) by FINSEQ_1:def_3; then F = (len F) |-> ((dist (x,y)) / N) by A119, FUNCOP_1:9; hence Sum F = ((N + 1) - 1) * ((dist (x,y)) / N) by A34, A40, A117, RVSUM_1:80 .= dist (x,y) by XCMPLX_1:87 ; ::_thesis: verum end; supposeA125: dist (x,y) < p ; ::_thesis: ex f being FinSequence of the carrier of V st ( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) holds dist (x,y) = Sum F ) ) take f = <*x,y*>; ::_thesis: ( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) holds dist (x,y) = Sum F ) ) thus A126: f /. 1 = x by FINSEQ_4:17; ::_thesis: ( f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) holds dist (x,y) = Sum F ) ) len f = 2 by FINSEQ_1:44; hence f /. (len f) = y by FINSEQ_4:17; ::_thesis: ( ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) holds dist (x,y) = Sum F ) ) A127: (len f) - 1 = (1 + 1) - 1 by FINSEQ_1:44 .= 1 ; thus for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p ::_thesis: for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being 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 i be Element of NAT ; ::_thesis: ( 1 <= i & i <= (len f) - 1 implies dist ((f /. i),(f /. (i + 1))) < p ) assume ( 1 <= i & i <= (len f) - 1 ) ; ::_thesis: dist ((f /. i),(f /. (i + 1))) < p then i in Seg 1 by A127, FINSEQ_1:1; then i = 1 by FINSEQ_1:2, TARSKI:def_1; hence dist ((f /. i),(f /. (i + 1))) < p by A125, A126, FINSEQ_4:17; ::_thesis: verum end; let F be FinSequence of REAL ; ::_thesis: ( len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) implies dist (x,y) = Sum F ) assume that A128: len F = (len f) - 1 and A129: for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ; ::_thesis: dist (x,y) = Sum F F /. 1 = dist ((f /. 1),(f /. (1 + 1))) by A127, A128, A129 .= dist (x,y) by A126, FINSEQ_4:17 ; then F = <*(dist (x,y))*> by A127, A128, FINSEQ_5:14; hence dist (x,y) = Sum F by FINSOP_1:11; ::_thesis: verum end; end; end; registration cluster non empty Reflexive discerning symmetric triangle convex -> non empty internal for MetrStruct ; coherence for b1 being non empty MetrSpace st b1 is convex holds b1 is internal proof let V be non empty MetrSpace; ::_thesis: ( V is convex implies V is internal ) assume A1: V is convex ; ::_thesis: V is internal let x, y be Element of V; :: according to VECTMETR:def_2 ::_thesis: for p, q being Real st p > 0 & q > 0 holds ex f being FinSequence of the carrier of V st ( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) holds abs ((dist (x,y)) - (Sum F)) < q ) ) let p, q be Real; ::_thesis: ( p > 0 & q > 0 implies ex f being FinSequence of the carrier of V st ( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) holds abs ((dist (x,y)) - (Sum F)) < q ) ) ) assume that A2: p > 0 and A3: q > 0 ; ::_thesis: ex f being FinSequence of the carrier of V st ( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) holds abs ((dist (x,y)) - (Sum F)) < q ) ) consider f being FinSequence of the carrier of V such that A4: ( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p ) ) and A5: for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being 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 ; ::_thesis: ( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) holds abs ((dist (x,y)) - (Sum F)) < q ) ) thus ( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds dist ((f /. i),(f /. (i + 1))) < p ) ) by A4; ::_thesis: for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) holds abs ((dist (x,y)) - (Sum F)) < q let F be FinSequence of REAL ; ::_thesis: ( len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) implies abs ((dist (x,y)) - (Sum F)) < q ) assume ( len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds F /. i = dist ((f /. i),(f /. (i + 1))) ) ) ; ::_thesis: abs ((dist (x,y)) - (Sum F)) < q then dist (x,y) = Sum F by A5; hence abs ((dist (x,y)) - (Sum F)) < q by A3, ABSVALUE:2; ::_thesis: verum end; end; registration cluster non empty Reflexive discerning symmetric triangle Discerning convex for MetrStruct ; existence ex b1 being non empty MetrSpace st b1 is convex proof reconsider ZS = {0} as non empty set ; deffunc H1( Element of ZS, Element of ZS) -> Element of NAT = 0 ; consider F being Function of [:ZS,ZS:],REAL such that A1: for x, y being Element of ZS holds F . (x,y) = H1(x,y) from BINOP_1:sch_4(); reconsider V = MetrStruct(# ZS,F #) as non empty MetrStruct ; A2: now__::_thesis:_for_a,_b_being_Element_of_V_holds_dist_(a,b)_=_dist_(b,a) let a, b be Element of V; ::_thesis: dist (a,b) = dist (b,a) 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 ; ::_thesis: verum end; A3: now__::_thesis:_for_a_being_Element_of_V_holds_dist_(a,a)_=_0 let a be Element of V; ::_thesis: dist (a,a) = 0 thus dist (a,a) = F . (a,a) by METRIC_1:def_1 .= 0 by A1 ; ::_thesis: verum end; A4: now__::_thesis:_for_a,_b,_c_being_Element_of_V_holds_dist_(a,c)_<=_(dist_(a,b))_+_(dist_(b,c)) let a, b, c be Element of V; ::_thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c)) 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; ::_thesis: verum end; now__::_thesis:_for_a,_b_being_Element_of_V_st_dist_(a,b)_=_0_holds_ a_=_b let a, b be Element of V; ::_thesis: ( dist (a,b) = 0 implies a = b ) assume dist (a,b) = 0 ; ::_thesis: a = b a = 0 by TARSKI:def_1; hence a = b by TARSKI:def_1; ::_thesis: verum end; then reconsider V = V as non empty Reflexive discerning symmetric triangle MetrStruct by A3, A2, A4, METRIC_1:1, METRIC_1:2, METRIC_1:3, METRIC_1:4; take V ; ::_thesis: V is convex let x, y be Element of V; :: according to VECTMETR:def_1 ::_thesis: for r being Real st 0 <= r & r <= 1 holds ex z being Element of V st ( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) ) let r be Real; ::_thesis: ( 0 <= r & r <= 1 implies ex z being Element of V st ( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) ) ) assume that 0 <= r and r <= 1 ; ::_thesis: ex z being Element of V st ( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) ) take z = x; ::_thesis: ( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) ) 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; ::_thesis: verum end; end; begin definition let V be non empty MetrStruct ; let f be Function of V,V; attrf is isometric means :Def3: :: VECTMETR:def 3 for x, y being Element of V holds dist (x,y) = dist ((f . x),(f . y)); end; :: deftheorem Def3 defines isometric VECTMETR:def_3_:_ for V being non empty MetrStruct for f being Function of V,V holds ( f is isometric iff for x, y being Element of V holds dist (x,y) = dist ((f . x),(f . y)) ); registration let V be non empty MetrStruct ; cluster id V -> onto isometric ; coherence ( id V is onto & id V is isometric ) proof thus rng (id V) = the carrier of V by RELAT_1:45; :: according to FUNCT_2:def_3 ::_thesis: id V is isometric let x, y be Element of V; :: according to VECTMETR:def_3 ::_thesis: dist (x,y) = dist (((id V) . x),((id V) . y)) thus dist (x,y) = dist (((id V) . x),y) by FUNCT_1:18 .= dist (((id V) . x),((id V) . y)) by FUNCT_1:18 ; ::_thesis: verum end; end; theorem :: VECTMETR:2 for V being non empty MetrStruct holds ( id V is onto & id V is isometric ) ; registration let V be non empty MetrStruct ; cluster non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like total quasi_total onto isometric for Element of bool [: the carrier of V, the carrier of V:]; existence ex b1 being Function of V,V st ( b1 is onto & b1 is isometric ) proof take f = id the carrier of V; ::_thesis: ( f is onto & f is isometric ) thus rng f = the carrier of V by RELAT_1:45; :: according to FUNCT_2:def_3 ::_thesis: f is isometric let x, y be Element of V; :: according to VECTMETR:def_3 ::_thesis: dist (x,y) = dist ((f . x),(f . y)) thus dist (x,y) = dist ((f . x),y) by FUNCT_1:18 .= dist ((f . x),(f . y)) by FUNCT_1:18 ; ::_thesis: verum end; end; definition let V be non empty MetrStruct ; defpred S1[ set ] means $1 is onto isometric Function of V,V; func ISOM V -> set means :Def4: :: VECTMETR:def 4 for x being set holds ( x in it iff x is onto isometric Function of V,V ); existence ex b1 being set st for x being set holds ( x in b1 iff x is onto isometric Function of V,V ) proof consider X being set such that A1: for x being set holds ( x in X iff ( x in Funcs ( the carrier of V, the carrier of V) & S1[x] ) ) from XBOOLE_0:sch_1(); take X ; ::_thesis: for x being set holds ( x in X iff x is onto isometric Function of V,V ) let x be set ; ::_thesis: ( x in X iff x is onto isometric Function of V,V ) thus ( x in X implies x is onto isometric Function of V,V ) by A1; ::_thesis: ( x is onto isometric Function of V,V implies x in X ) assume A2: x is onto isometric Function of V,V ; ::_thesis: x in X then x in Funcs ( the carrier of V, the carrier of V) by FUNCT_2:8; hence x in X by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff x is onto isometric Function of V,V ) ) & ( for x being set holds ( x in b2 iff x is onto isometric Function of V,V ) ) holds b1 = b2 proof thus for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum end; end; :: deftheorem Def4 defines ISOM VECTMETR:def_4_:_ for V being non empty MetrStruct for b2 being set holds ( b2 = ISOM V iff for x being set holds ( x in b2 iff x is onto isometric Function of V,V ) ); definition let V be non empty MetrStruct ; :: original: ISOM redefine func ISOM V -> Subset of (Funcs ( the carrier of V, the carrier of V)); coherence ISOM V is Subset of (Funcs ( the carrier of V, the carrier of V)) proof now__::_thesis:_for_x_being_set_st_x_in_ISOM_V_holds_ x_in_Funcs_(_the_carrier_of_V,_the_carrier_of_V) let x be set ; ::_thesis: ( x in ISOM V implies x in Funcs ( the carrier of V, the carrier of V) ) assume x in ISOM V ; ::_thesis: x in Funcs ( the carrier of V, the carrier of 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; ::_thesis: verum end; hence ISOM V is Subset of (Funcs ( the carrier of V, the carrier of V)) by TARSKI:def_3; ::_thesis: verum end; end; registration let V be non empty Reflexive discerning MetrStruct ; cluster Function-like quasi_total isometric -> one-to-one for Element of bool [: the carrier of V, the carrier of V:]; coherence for b1 being Function of V,V st b1 is isometric holds b1 is one-to-one proof let f be Function of V,V; ::_thesis: ( f is isometric implies f is one-to-one ) assume A1: f is isometric ; ::_thesis: f is one-to-one now__::_thesis:_for_x,_y_being_set_st_x_in_dom_f_&_y_in_dom_f_&_f_._x_=_f_._y_holds_ x_=_y let x, y be set ; ::_thesis: ( x in dom f & y in dom f & f . x = f . y implies x = y ) assume that A2: ( x in dom f & y in dom f ) and A3: f . x = f . y ; ::_thesis: x = y reconsider x1 = x, y1 = y as Element of V by A2; dist (x1,y1) = dist ((f . x1),(f . y1)) by A1, Def3 .= 0 by A3, METRIC_1:1 ; hence x = y by METRIC_1:2; ::_thesis: verum end; hence f is one-to-one by FUNCT_1:def_4; ::_thesis: verum end; end; theorem :: VECTMETR:3 for V being non empty Reflexive discerning MetrStruct for f being Function of V,V st f is isometric holds f is one-to-one ; registration let V be non empty Reflexive discerning MetrStruct ; let f be onto isometric Function of V,V; clusterf " -> onto isometric ; coherence ( f " is onto & f " is isometric ) proof A1: rng f = [#] V by FUNCT_2:def_3; hence rng (f ") = the carrier of V by TOPS_2:49; :: according to FUNCT_2:def_3 ::_thesis: f " is isometric let x, y be Element of V; :: according to VECTMETR:def_3 ::_thesis: dist (x,y) = dist (((f ") . x),((f ") . y)) 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, FUNCT_1:18 .= (f * (f ")) . y by A1, TOPS_2:52 .= f . ((f ") . y) by A3, FUNCT_1:13 ; x = (id (rng f)) . x by A2, FUNCT_1:18 .= (f * (f ")) . x by A1, TOPS_2:52 .= f . ((f ") . x) by A3, FUNCT_1:13 ; hence dist (x,y) = dist (((f ") . x),((f ") . y)) by A4, Def3; ::_thesis: verum end; end; theorem :: VECTMETR:4 for V being non empty Reflexive discerning MetrStruct for f being onto isometric Function of V,V holds ( f " is onto & f " is isometric ) ; registration let V be non empty MetrStruct ; let f, g be onto isometric Function of V,V; clusterg * f -> onto isometric for Function of V,V; coherence for b1 being Function of V,V st b1 = f * g holds ( b1 is onto & b1 is isometric ) proof ( f * g is onto & f * g is 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 ; :: according to FUNCT_2:def_3 ::_thesis: f * g is isometric let x, y be Element of V; :: according to VECTMETR:def_3 ::_thesis: dist (x,y) = dist (((f * g) . x),((f * g) . y)) 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 ; ::_thesis: verum end; hence for b1 being Function of V,V st b1 = f * g holds ( b1 is onto & b1 is isometric ) ; ::_thesis: verum end; end; theorem :: VECTMETR:5 for V being non empty MetrStruct for f, g being onto isometric Function of V,V holds ( f * g is onto & f * g is isometric ) ; registration let V be non empty MetrStruct ; cluster ISOM V -> non empty ; coherence not ISOM V is empty proof ( id V is onto & id V is isometric ) ; hence not ISOM V is empty by Def4; ::_thesis: verum end; end; begin definition attrc1 is strict ; struct RLSMetrStruct -> RLSStruct , MetrStruct ; aggrRLSMetrStruct(# carrier, distance, ZeroF, addF, Mult #) -> RLSMetrStruct ; end; registration cluster non empty strict for RLSMetrStruct ; existence ex b1 being RLSMetrStruct st ( not b1 is empty & b1 is strict ) proof set X = the non empty set ; set F = the Function of [: the non empty set , the non empty set :],REAL; set O = the Element of the non empty set ; set B = the BinOp of the non empty set ; set G = the Function of [:REAL, the non empty set :], the non empty set ; take RLSMetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL, the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set #) ; ::_thesis: ( not RLSMetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL, the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set #) is empty & RLSMetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL, the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set #) is strict ) thus not the carrier of RLSMetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL, the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: RLSMetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL, the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set #) is strict thus RLSMetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL, the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set #) is strict ; ::_thesis: verum 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 not RLSMetrStruct(# X,F,O,B,G #) is empty ; end; definition let V be non empty RLSMetrStruct ; attrV is homogeneous means :Def5: :: VECTMETR:def 5 for r being Real for v, w being Element of V holds dist ((r * v),(r * w)) = (abs r) * (dist (v,w)); end; :: deftheorem Def5 defines homogeneous VECTMETR:def_5_:_ for V being non empty RLSMetrStruct holds ( V is homogeneous iff for r being Real for v, w being Element of V holds dist ((r * v),(r * w)) = (abs r) * (dist (v,w)) ); definition let V be non empty RLSMetrStruct ; attrV is translatible means :Def6: :: VECTMETR:def 6 for u, w, v being Element of V holds dist (v,w) = dist ((v + u),(w + u)); end; :: deftheorem Def6 defines translatible VECTMETR:def_6_:_ for V being non empty RLSMetrStruct holds ( V is translatible iff for u, w, v being Element of V holds dist (v,w) = dist ((v + u),(w + u)) ); definition let V be non empty RLSMetrStruct ; let v be Element of V; func Norm v -> Real equals :: VECTMETR:def 7 dist ((0. V),v); coherence dist ((0. V),v) is Real ; end; :: deftheorem defines Norm VECTMETR:def_7_:_ for V being non empty RLSMetrStruct for v being Element of V holds Norm v = dist ((0. V),v); registration cluster non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible for RLSMetrStruct ; existence ex b1 being non empty RLSMetrStruct st ( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital & b1 is Reflexive & b1 is discerning & b1 is symmetric & b1 is triangle & b1 is homogeneous & b1 is translatible ) proof reconsider ZS = {0} as non empty set ; reconsider O = 0 as Element of ZS by TARSKI:def_1; deffunc H1( Element of ZS, Element of ZS) -> Element of NAT = 0 ; consider FF being Function of [:ZS,ZS:],REAL such that A1: for x, y being Element of ZS holds FF . (x,y) = H1(x,y) from BINOP_1:sch_4(); deffunc H2( real number , Element of ZS) -> Element of ZS = O; deffunc H3( Element of ZS, Element of ZS) -> Element of ZS = O; consider F being BinOp of ZS such that A2: for x, y being Element of ZS holds F . (x,y) = H3(x,y) from BINOP_1:sch_4(); consider G being Function of [:REAL,ZS:],ZS such that A3: for a being Element of REAL for x being Element of ZS holds G . (a,x) = H2(a,x) from BINOP_1:sch_4(); set W = RLSMetrStruct(# ZS,FF,O,F,G #); A4: for a, b being real number for x being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds (a + b) * x = (a * x) + (b * x) proof let a, b be real number ; ::_thesis: for x being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds (a + b) * x = (a * x) + (b * x) reconsider a = a, b = b as Real by XREAL_0:def_1; let x be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); ::_thesis: (a + b) * x = (a * x) + (b * x) set c = a + b; reconsider X = x as Element of ZS ; (a + b) * x = H2(a + b,X) by A3; hence (a + b) * x = (a * x) + (b * x) by A2; ::_thesis: verum end; take RLSMetrStruct(# ZS,FF,O,F,G #) ; ::_thesis: ( RLSMetrStruct(# ZS,FF,O,F,G #) is strict & RLSMetrStruct(# ZS,FF,O,F,G #) is Abelian & RLSMetrStruct(# ZS,FF,O,F,G #) is add-associative & RLSMetrStruct(# ZS,FF,O,F,G #) is right_zeroed & RLSMetrStruct(# ZS,FF,O,F,G #) is right_complementable & RLSMetrStruct(# ZS,FF,O,F,G #) is vector-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-associative & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-unital & RLSMetrStruct(# ZS,FF,O,F,G #) is Reflexive & RLSMetrStruct(# ZS,FF,O,F,G #) is discerning & RLSMetrStruct(# ZS,FF,O,F,G #) is symmetric & RLSMetrStruct(# ZS,FF,O,F,G #) is triangle & RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous & RLSMetrStruct(# ZS,FF,O,F,G #) is translatible ) thus RLSMetrStruct(# ZS,FF,O,F,G #) is strict ; ::_thesis: ( RLSMetrStruct(# ZS,FF,O,F,G #) is Abelian & RLSMetrStruct(# ZS,FF,O,F,G #) is add-associative & RLSMetrStruct(# ZS,FF,O,F,G #) is right_zeroed & RLSMetrStruct(# ZS,FF,O,F,G #) is right_complementable & RLSMetrStruct(# ZS,FF,O,F,G #) is vector-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-associative & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-unital & RLSMetrStruct(# ZS,FF,O,F,G #) is Reflexive & RLSMetrStruct(# ZS,FF,O,F,G #) is discerning & RLSMetrStruct(# ZS,FF,O,F,G #) is symmetric & RLSMetrStruct(# ZS,FF,O,F,G #) is triangle & RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous & RLSMetrStruct(# ZS,FF,O,F,G #) is translatible ) for x, y being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds x + y = y + x proof let x, y be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); ::_thesis: x + y = y + x reconsider X = x, Y = y as Element of ZS ; x + y = H3(X,Y) by A2; hence x + y = y + x by A2; ::_thesis: verum end; hence RLSMetrStruct(# ZS,FF,O,F,G #) is Abelian by RLVECT_1:def_2; ::_thesis: ( RLSMetrStruct(# ZS,FF,O,F,G #) is add-associative & RLSMetrStruct(# ZS,FF,O,F,G #) is right_zeroed & RLSMetrStruct(# ZS,FF,O,F,G #) is right_complementable & RLSMetrStruct(# ZS,FF,O,F,G #) is vector-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-associative & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-unital & RLSMetrStruct(# ZS,FF,O,F,G #) is Reflexive & RLSMetrStruct(# ZS,FF,O,F,G #) is discerning & RLSMetrStruct(# ZS,FF,O,F,G #) is symmetric & RLSMetrStruct(# ZS,FF,O,F,G #) is triangle & RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous & RLSMetrStruct(# ZS,FF,O,F,G #) is translatible ) for x, y, z being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds (x + y) + z = x + (y + z) proof let x, y, z be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); ::_thesis: (x + y) + z = x + (y + z) reconsider X = x, Y = y, Z = z as Element of ZS ; (x + y) + z = H3(H3(X,Y),Z) by A2; hence (x + y) + z = x + (y + z) by A2; ::_thesis: verum end; hence RLSMetrStruct(# ZS,FF,O,F,G #) is add-associative by RLVECT_1:def_3; ::_thesis: ( RLSMetrStruct(# ZS,FF,O,F,G #) is right_zeroed & RLSMetrStruct(# ZS,FF,O,F,G #) is right_complementable & RLSMetrStruct(# ZS,FF,O,F,G #) is vector-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-associative & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-unital & RLSMetrStruct(# ZS,FF,O,F,G #) is Reflexive & RLSMetrStruct(# ZS,FF,O,F,G #) is discerning & RLSMetrStruct(# ZS,FF,O,F,G #) is symmetric & RLSMetrStruct(# ZS,FF,O,F,G #) is triangle & RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous & RLSMetrStruct(# ZS,FF,O,F,G #) is translatible ) for x being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds x + (0. RLSMetrStruct(# ZS,FF,O,F,G #)) = x proof let x be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); ::_thesis: x + (0. RLSMetrStruct(# ZS,FF,O,F,G #)) = x reconsider X = x as Element of ZS ; x + (0. RLSMetrStruct(# ZS,FF,O,F,G #)) = H3(X,O) by A2; hence x + (0. RLSMetrStruct(# ZS,FF,O,F,G #)) = x by TARSKI:def_1; ::_thesis: verum end; hence RLSMetrStruct(# ZS,FF,O,F,G #) is right_zeroed by RLVECT_1:def_4; ::_thesis: ( RLSMetrStruct(# ZS,FF,O,F,G #) is right_complementable & RLSMetrStruct(# ZS,FF,O,F,G #) is vector-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-associative & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-unital & RLSMetrStruct(# ZS,FF,O,F,G #) is Reflexive & RLSMetrStruct(# ZS,FF,O,F,G #) is discerning & RLSMetrStruct(# ZS,FF,O,F,G #) is symmetric & RLSMetrStruct(# ZS,FF,O,F,G #) is triangle & RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous & RLSMetrStruct(# ZS,FF,O,F,G #) is translatible ) thus RLSMetrStruct(# ZS,FF,O,F,G #) is right_complementable ::_thesis: ( RLSMetrStruct(# ZS,FF,O,F,G #) is vector-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-associative & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-unital & RLSMetrStruct(# ZS,FF,O,F,G #) is Reflexive & RLSMetrStruct(# ZS,FF,O,F,G #) is discerning & RLSMetrStruct(# ZS,FF,O,F,G #) is symmetric & RLSMetrStruct(# ZS,FF,O,F,G #) is triangle & RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous & RLSMetrStruct(# ZS,FF,O,F,G #) is translatible ) proof reconsider y = O as VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) ; let x be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable take y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. RLSMetrStruct(# ZS,FF,O,F,G #) thus x + y = 0. RLSMetrStruct(# ZS,FF,O,F,G #) by A2; ::_thesis: verum end; A5: for a being real number for x, y being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds a * (x + y) = (a * x) + (a * y) proof let a be real number ; ::_thesis: for x, y being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds a * (x + y) = (a * x) + (a * y) reconsider a = a as Real by XREAL_0:def_1; let x, y be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); ::_thesis: a * (x + y) = (a * x) + (a * y) reconsider X = x, Y = y as Element of ZS ; (a * x) + (a * y) = H3(H2(a,X),H2(a,Y)) by A2; hence a * (x + y) = (a * x) + (a * y) by A3; ::_thesis: verum end; A6: for a, b being real number for x being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds (a * b) * x = a * (b * x) proof let a, b be real number ; ::_thesis: for x being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds (a * b) * x = a * (b * x) reconsider a = a, b = b as Real by XREAL_0:def_1; let x be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); ::_thesis: (a * b) * x = a * (b * x) set c = a * b; reconsider X = x as Element of ZS ; (a * b) * x = H2(a * b,X) by A3; hence (a * b) * x = a * (b * x) by A3; ::_thesis: verum end; for x being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds 1 * x = x proof reconsider A9 = 1 as Element of REAL ; let x be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); ::_thesis: 1 * x = x reconsider X = x as Element of ZS ; 1 * x = H2(A9,X) by A3; hence 1 * x = x by TARSKI:def_1; ::_thesis: verum end; hence ( RLSMetrStruct(# ZS,FF,O,F,G #) is vector-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-associative & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-unital ) by A5, A4, A6, RLVECT_1:def_5, RLVECT_1:def_6, RLVECT_1:def_7, RLVECT_1:def_8; ::_thesis: ( RLSMetrStruct(# ZS,FF,O,F,G #) is Reflexive & RLSMetrStruct(# ZS,FF,O,F,G #) is discerning & RLSMetrStruct(# ZS,FF,O,F,G #) is symmetric & RLSMetrStruct(# ZS,FF,O,F,G #) is triangle & RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous & RLSMetrStruct(# ZS,FF,O,F,G #) is translatible ) A7: for a, b, c being Point of RLSMetrStruct(# ZS,FF,O,F,G #) 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 RLSMetrStruct(# ZS,FF,O,F,G #); ::_thesis: ( 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)) ) A8: dist (a,a) = FF . (a,a) by METRIC_1:def_1 .= 0 by A1 ; hence dist (a,a) = 0 ; ::_thesis: ( ( dist (a,b) = 0 implies a = b ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) A9: a = 0 by TARSKI:def_1; hence ( dist (a,b) = 0 implies a = b ) by TARSKI:def_1; ::_thesis: ( dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) A10: b = 0 by TARSKI:def_1; hence dist (a,b) = dist (b,a) by A9; ::_thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c)) thus dist (a,c) <= (dist (a,b)) + (dist (b,c)) by A9, A10, A8; ::_thesis: verum end; hence RLSMetrStruct(# ZS,FF,O,F,G #) is Reflexive by METRIC_1:1; ::_thesis: ( RLSMetrStruct(# ZS,FF,O,F,G #) is discerning & RLSMetrStruct(# ZS,FF,O,F,G #) is symmetric & RLSMetrStruct(# ZS,FF,O,F,G #) is triangle & RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous & RLSMetrStruct(# ZS,FF,O,F,G #) is translatible ) thus RLSMetrStruct(# ZS,FF,O,F,G #) is discerning by A7, METRIC_1:2; ::_thesis: ( RLSMetrStruct(# ZS,FF,O,F,G #) is symmetric & RLSMetrStruct(# ZS,FF,O,F,G #) is triangle & RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous & RLSMetrStruct(# ZS,FF,O,F,G #) is translatible ) thus RLSMetrStruct(# ZS,FF,O,F,G #) is symmetric by A7, METRIC_1:3; ::_thesis: ( RLSMetrStruct(# ZS,FF,O,F,G #) is triangle & RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous & RLSMetrStruct(# ZS,FF,O,F,G #) is translatible ) thus RLSMetrStruct(# ZS,FF,O,F,G #) is triangle by A7, METRIC_1:4; ::_thesis: ( RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous & RLSMetrStruct(# ZS,FF,O,F,G #) is translatible ) for r being Element of REAL for v, w being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds dist ((r * v),(r * w)) = (abs r) * (dist (v,w)) proof let r be Element of REAL ; ::_thesis: for v, w being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds dist ((r * v),(r * w)) = (abs r) * (dist (v,w)) let v, w be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); ::_thesis: dist ((r * v),(r * w)) = (abs r) * (dist (v,w)) reconsider v1 = v, w1 = w as Element of ZS ; A11: FF . (v1,w1) = H1(v1,w1) by A1; thus dist ((r * v),(r * w)) = FF . ((r * v),(r * w)) by METRIC_1:def_1 .= (abs r) * 0 by A1 .= (abs r) * H1(v1,w1) .= (abs r) * (FF . (v1,w1)) by A11 .= (abs r) * (dist (v,w)) by METRIC_1:def_1 ; ::_thesis: verum end; hence RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous by Def5; ::_thesis: RLSMetrStruct(# ZS,FF,O,F,G #) is translatible for u, w, v being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds dist (v,w) = dist ((v + u),(w + u)) proof let u, w, v be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); ::_thesis: dist (v,w) = dist ((v + u),(w + u)) 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 ; ::_thesis: verum end; hence RLSMetrStruct(# ZS,FF,O,F,G #) is translatible by Def6; ::_thesis: verum end; end; definition mode RealLinearMetrSpace is non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital homogeneous translatible RLSMetrStruct ; end; theorem :: VECTMETR:6 for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital homogeneous RLSMetrStruct for r being Real for v being Element of V holds Norm (r * v) = (abs r) * (Norm v) proof let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital homogeneous RLSMetrStruct ; ::_thesis: for r being Real for v being Element of V holds Norm (r * v) = (abs r) * (Norm v) let r be Real; ::_thesis: for v being Element of V holds Norm (r * v) = (abs r) * (Norm v) let v be Element of V; ::_thesis: Norm (r * v) = (abs r) * (Norm v) thus Norm (r * v) = dist ((r * (0. V)),(r * v)) by RLVECT_1:10 .= (abs r) * (Norm v) by Def5 ; ::_thesis: verum end; theorem :: VECTMETR:7 for V being non empty right_complementable triangle Abelian add-associative right_zeroed translatible RLSMetrStruct for v, w being Element of V holds Norm (v + w) <= (Norm v) + (Norm w) proof let V be non empty right_complementable triangle Abelian add-associative right_zeroed translatible RLSMetrStruct ; ::_thesis: for v, w being Element of V holds Norm (v + w) <= (Norm v) + (Norm w) let v, w be Element of V; ::_thesis: Norm (v + w) <= (Norm v) + (Norm w) 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 Norm (v + w) <= (Norm v) + (Norm w) by RLVECT_1:4; ::_thesis: verum end; theorem :: VECTMETR:8 for V being non empty right_complementable add-associative right_zeroed translatible RLSMetrStruct for v, w being Element of V holds dist (v,w) = Norm (w - v) proof let V be non empty right_complementable add-associative right_zeroed translatible RLSMetrStruct ; ::_thesis: for v, w being Element of V holds dist (v,w) = Norm (w - v) let v, w be Element of V; ::_thesis: dist (v,w) = Norm (w - v) thus dist (v,w) = dist ((v + (- v)),(w + (- v))) by Def6 .= Norm (w - v) by RLVECT_1:5 ; ::_thesis: verum end; definition let n be Element of NAT ; func RLMSpace n -> strict RealLinearMetrSpace means :Def8: :: VECTMETR:def 8 ( the carrier of it = REAL n & the distance of it = Pitag_dist n & 0. it = 0* n & ( for x, y being Element of REAL n holds the addF of it . (x,y) = x + y ) & ( for x being Element of REAL n for r being Element of REAL holds the Mult of it . (r,x) = r * x ) ); existence ex b1 being strict RealLinearMetrSpace st ( the carrier of b1 = REAL n & the distance of b1 = Pitag_dist n & 0. b1 = 0* n & ( for x, y being Element of REAL n holds the addF of b1 . (x,y) = x + y ) & ( for x being Element of REAL n for r being Element of REAL holds the Mult of b1 . (r,x) = r * x ) ) proof deffunc H1( Element of REAL , Element of REAL n) -> Element of REAL n = $1 * $2; deffunc H2( Element of REAL n, Element of REAL n) -> Element of REAL n = $1 + $2; consider f being BinOp of (REAL n) such that A1: for x, y being Element of REAL n holds f . (x,y) = H2(x,y) from BINOP_1:sch_4(); consider g being Function of [:REAL,(REAL n):],(REAL n) such that A2: for r being Element of REAL for x being Element of REAL n holds g . (r,x) = H1(r,x) from BINOP_1:sch_4(); set RLSMS = RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); A3: now__::_thesis:_for_u,_v,_w_being_Element_of_RLSMetrStruct(#_(REAL_n),(Pitag_dist_n),(0*_n),f,g_#)_holds_(u_+_v)_+_w_=_u_+_(v_+_w) let u, v, w be Element of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); ::_thesis: (u + v) + w = u + (v + w) 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 ; ::_thesis: verum end; A4: now__::_thesis:_for_v,_w_being_Element_of_RLSMetrStruct(#_(REAL_n),(Pitag_dist_n),(0*_n),f,g_#)_holds_v_+_w_=_w_+_v let v, w be Element of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); ::_thesis: v + w = w + v reconsider v1 = v, w1 = w as Element of REAL n ; thus v + w = v1 + w1 by A1 .= w + v by A1 ; ::_thesis: verum end; A5: now__::_thesis:_for_v_being_Element_of_RLSMetrStruct(#_(REAL_n),(Pitag_dist_n),(0*_n),f,g_#)_holds_v_+_(0._RLSMetrStruct(#_(REAL_n),(Pitag_dist_n),(0*_n),f,g_#))_=_v let v be Element of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); ::_thesis: v + (0. RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #)) = v reconsider v1 = v as Element of n -tuples_on REAL ; thus v + (0. RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #)) = v1 + (n |-> 0) by A1 .= v by RVSUM_1:16 ; ::_thesis: verum end; A6: now__::_thesis:_for_r_being_Real for_v,_w_being_VECTOR_of_RLSMetrStruct(#_(REAL_n),(Pitag_dist_n),(0*_n),f,g_#)_holds_dist_((r_*_v),(r_*_w))_=_(abs_r)_*_(dist_(v,w)) let r be Real; ::_thesis: for v, w being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds dist ((r * v),(r * w)) = (abs r) * (dist (v,w)) let v, w be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); ::_thesis: dist ((r * v),(r * w)) = (abs r) * (dist (v,w)) reconsider v1 = v, w1 = w as Element of REAL n ; reconsider v2 = v1, w2 = w1 as Element of n -tuples_on REAL ; A7: dist (v,w) = (Pitag_dist n) . (v,w) by METRIC_1:def_1 .= |.(v1 - w1).| by EUCLID:def_6 ; A8: ( r * v = r * v1 & r * w = r * w1 ) by A2; thus dist ((r * v),(r * w)) = (Pitag_dist n) . ((r * v),(r * w)) by METRIC_1:def_1 .= |.((r * v2) - (r * w2)).| by A8, 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 .= (abs r) * (dist (v,w)) by A7, EUCLID:11 ; ::_thesis: verum end; A9: now__::_thesis:_for_u,_w,_v_being_VECTOR_of_RLSMetrStruct(#_(REAL_n),(Pitag_dist_n),(0*_n),f,g_#)_holds_dist_(v,w)_=_dist_((v_+_u),(w_+_u)) let u, w, v be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); ::_thesis: dist (v,w) = dist ((v + u),(w + u)) 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 ; A10: ( 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 A10, METRIC_1:def_1 ; ::_thesis: verum end; A11: RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) is right_complementable proof let v be Element of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable reconsider v1 = v as Element of n -tuples_on REAL ; reconsider w = - v1 as Element of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) ; take w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) thus v + w = v1 - v1 by A1 .= 0. RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) by RVSUM_1:37 ; ::_thesis: verum end; A12: now__::_thesis:_(_(_for_a1_being_real_number_ for_v,_w_being_VECTOR_of_RLSMetrStruct(#_(REAL_n),(Pitag_dist_n),(0*_n),f,g_#)_holds_a1_*_(v_+_w)_=_(a1_*_v)_+_(a1_*_w)_)_&_(_for_a1,_b1_being_real_number_ for_v_being_VECTOR_of_RLSMetrStruct(#_(REAL_n),(Pitag_dist_n),(0*_n),f,g_#)_holds_(a1_+_b1)_*_v_=_(a1_*_v)_+_(b1_*_v)_)_&_(_for_a1,_b1_being_real_number_ for_v_being_VECTOR_of_RLSMetrStruct(#_(REAL_n),(Pitag_dist_n),(0*_n),f,g_#)_holds_(a1_*_b1)_*_v_=_a1_*_(b1_*_v)_)_&_(_for_v_being_VECTOR_of_RLSMetrStruct(#_(REAL_n),(Pitag_dist_n),(0*_n),f,g_#)_holds_1_*_v_=_v_)_) hereby ::_thesis: ( ( for a1, b1 being real number for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds (a1 + b1) * v = (a1 * v) + (b1 * v) ) & ( for a1, b1 being real number for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds (a1 * b1) * v = a1 * (b1 * v) ) & ( for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds 1 * v = v ) ) let a1 be real number ; ::_thesis: for v, w being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds a1 * (v + w) = (a1 * v) + (a1 * w) let v, w be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); ::_thesis: a1 * (v + w) = (a1 * v) + (a1 * w) reconsider a = a1 as Real by XREAL_0:def_1; 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 A2 .= (a * v1) + (a * w1) by RVSUM_1:51 .= f . ((a * v1),(a * w1)) by A1 .= f . ((g . (a,v)),(a * w1)) by A2 .= (a * v) + (a * w) by A2 ; hence a1 * (v + w) = (a1 * v) + (a1 * w) ; ::_thesis: verum end; hereby ::_thesis: ( ( for a1, b1 being real number for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds (a1 * b1) * v = a1 * (b1 * v) ) & ( for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds 1 * v = v ) ) let a1, b1 be real number ; ::_thesis: for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds (a1 + b1) * v = (a1 * v) + (b1 * v) let v be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); ::_thesis: (a1 + b1) * v = (a1 * v) + (b1 * v) reconsider a = a1, b = b1 as Real by XREAL_0:def_1; 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 A2 .= (a * v1) + (b * v1) by RVSUM_1:50 .= f . ((a * v1),(b * v1)) by A1 .= f . ((g . (a,v)),(b * v1)) by A2 .= (a * v) + (b * v) by A2 ; hence (a1 + b1) * v = (a1 * v) + (b1 * v) ; ::_thesis: verum end; hereby ::_thesis: for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds 1 * v = v let a1, b1 be real number ; ::_thesis: for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds (a1 * b1) * v = a1 * (b1 * v) let v be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); ::_thesis: (a1 * b1) * v = a1 * (b1 * v) reconsider a = a1, b = b1 as Real by XREAL_0:def_1; 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 A2 .= a * (b * v1) by RVSUM_1:49 .= g . (a,(b * v1)) by A2 .= a * (b * v) by A2 ; hence (a1 * b1) * v = a1 * (b1 * v) ; ::_thesis: verum end; hereby ::_thesis: verum let v be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); ::_thesis: 1 * v = v reconsider v1 = v as Element of n -tuples_on REAL ; thus 1 * v = 1 * v1 by A2 .= v by RVSUM_1:52 ; ::_thesis: verum end; end; A13: now__::_thesis:_for_a,_b,_c_being_VECTOR_of_RLSMetrStruct(#_(REAL_n),(Pitag_dist_n),(0*_n),f,g_#)_holds_ (_(_dist_(a,b)_=_0_implies_a_=_b_)_&_dist_(a,a)_=_0_&_dist_(a,b)_=_dist_(b,a)_&_dist_(a,c)_<=_(dist_(a,b))_+_(dist_(b,c))_) let a, b, c be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); ::_thesis: ( ( dist (a,b) = 0 implies a = b ) & dist (a,a) = 0 & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) reconsider a1 = a, b1 = b, c1 = c as Element of REAL n ; thus ( dist (a,b) = 0 implies a = b ) ::_thesis: ( dist (a,a) = 0 & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) proof assume dist (a,b) = 0 ; ::_thesis: a = b then (Pitag_dist n) . (a,b) = 0 by METRIC_1:def_1; then |.(a1 - b1).| = 0 by EUCLID:def_6; hence a = b by EUCLID:16; ::_thesis: verum end; A14: 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; ::_thesis: ( dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) 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 ; ::_thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c)) A15: 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 A14, A15, EUCLID:19; ::_thesis: verum end; reconsider RLSMS = RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) as non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RLSMetrStruct by A4, A3, A5, A11, A12, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4, RLVECT_1:def_5, RLVECT_1:def_6, RLVECT_1:def_7, RLVECT_1:def_8; reconsider RLSMS = RLSMS as strict RealLinearMetrSpace by A13, A6, A9, Def5, Def6, METRIC_1:1, METRIC_1:2, METRIC_1:3, METRIC_1:4; take RLSMS ; ::_thesis: ( the carrier of RLSMS = REAL n & the distance of RLSMS = Pitag_dist n & 0. RLSMS = 0* n & ( for x, y being Element of REAL n holds the addF of RLSMS . (x,y) = x + y ) & ( for x being Element of REAL n for r being Element of REAL holds the Mult of RLSMS . (r,x) = r * x ) ) thus ( the carrier of RLSMS = REAL n & the distance of RLSMS = Pitag_dist n & 0. RLSMS = 0* n & ( for x, y being Element of REAL n holds the addF of RLSMS . (x,y) = x + y ) & ( for x being Element of REAL n for r being Element of REAL holds the Mult of RLSMS . (r,x) = r * x ) ) by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being strict RealLinearMetrSpace st the carrier of b1 = REAL n & the distance of b1 = Pitag_dist n & 0. b1 = 0* n & ( for x, y being Element of REAL n holds the addF of b1 . (x,y) = x + y ) & ( for x being Element of REAL n for r being Element of REAL holds the Mult of b1 . (r,x) = r * x ) & the carrier of b2 = REAL n & the distance of b2 = Pitag_dist n & 0. b2 = 0* n & ( for x, y being Element of REAL n holds the addF of b2 . (x,y) = x + y ) & ( for x being Element of REAL n for r being Element of REAL holds the Mult of b2 . (r,x) = r * x ) holds b1 = b2 proof let V1, V2 be strict RealLinearMetrSpace; ::_thesis: ( the carrier of V1 = REAL n & the distance of V1 = Pitag_dist n & 0. V1 = 0* n & ( for x, y being Element of REAL n holds the addF of V1 . (x,y) = x + y ) & ( for x being Element of REAL n for r being Element of REAL holds the Mult of V1 . (r,x) = r * x ) & the carrier of V2 = REAL n & the distance of V2 = Pitag_dist n & 0. V2 = 0* n & ( for x, y being Element of REAL n holds the addF of V2 . (x,y) = x + y ) & ( for x being Element of REAL n for r being Element of REAL holds the Mult of V2 . (r,x) = r * x ) implies V1 = V2 ) assume that A16: the carrier of V1 = REAL n and A17: ( the distance of V1 = Pitag_dist n & 0. V1 = 0* n ) and A18: for x, y being Element of REAL n holds the addF of V1 . (x,y) = x + y and A19: for x being Element of REAL n for r being Element of REAL holds the Mult of V1 . (r,x) = r * x and A20: the carrier of V2 = REAL n and A21: ( the distance of V2 = Pitag_dist n & 0. V2 = 0* n ) and A22: for x, y being Element of REAL n holds the addF of V2 . (x,y) = x + y and A23: for x being Element of REAL n for r being Element of REAL holds the Mult of V2 . (r,x) = r * x ; ::_thesis: V1 = V2 now__::_thesis:_for_x,_y_being_Element_of_V1_holds_the_addF_of_V1_._(x,y)_=_the_addF_of_V2_._(x,y) let x, y be Element of V1; ::_thesis: the addF of V1 . (x,y) = the addF of V2 . (x,y) reconsider x1 = x, y1 = y as Element of REAL n by A16; thus the addF of V1 . (x,y) = x1 + y1 by A18 .= the addF of V2 . (x,y) by A22 ; ::_thesis: verum end; then A24: the addF of V1 = the addF of V2 by A16, A20, BINOP_1:2; now__::_thesis:_for_r_being_Element_of_REAL_ for_x_being_Element_of_V1_holds_the_Mult_of_V1_._(r,x)_=_the_Mult_of_V2_._(r,x) let r be Element of REAL ; ::_thesis: for x being Element of V1 holds the Mult of V1 . (r,x) = the Mult of V2 . (r,x) let x be Element of V1; ::_thesis: the Mult of V1 . (r,x) = the Mult of V2 . (r,x) reconsider x1 = x as Element of REAL n by A16; thus the Mult of V1 . (r,x) = r * x1 by A19 .= the Mult of V2 . (r,x) by A23 ; ::_thesis: verum end; hence V1 = V2 by A16, A17, A20, A21, A24, BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def8 defines RLMSpace VECTMETR:def_8_:_ for n being Element of NAT for b2 being strict RealLinearMetrSpace holds ( b2 = RLMSpace n iff ( the carrier of b2 = REAL n & the distance of b2 = Pitag_dist n & 0. b2 = 0* n & ( for x, y being Element of REAL n holds the addF of b2 . (x,y) = x + y ) & ( for x being Element of REAL n for r being Element of REAL holds the Mult of b2 . (r,x) = r * x ) ) ); theorem :: VECTMETR:9 for n being Element of NAT for f being onto isometric Function of (RLMSpace n),(RLMSpace n) holds rng f = REAL n proof let n be Element of NAT ; ::_thesis: for f being onto isometric Function of (RLMSpace n),(RLMSpace n) holds rng f = REAL n let f be onto isometric Function of (RLMSpace n),(RLMSpace n); ::_thesis: rng f = REAL n thus rng f = the carrier of (RLMSpace n) by FUNCT_2:def_3 .= REAL n by Def8 ; ::_thesis: verum end; begin definition let n be Element of NAT ; func IsomGroup n -> strict multMagma means :Def9: :: VECTMETR:def 9 ( the carrier of it = ISOM (RLMSpace n) & ( for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds the multF of it . (f,g) = f * g ) ); existence ex b1 being strict multMagma st ( the carrier of b1 = ISOM (RLMSpace n) & ( for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds the multF of b1 . (f,g) = f * g ) ) proof defpred S1[ set , set , set ] means ex f, g being Function st ( f = $1 & g = $2 & $3 = f * g ); A1: for x, y being Element of ISOM (RLMSpace n) ex z being Element of ISOM (RLMSpace n) st S1[x,y,z] proof let x, y be Element of ISOM (RLMSpace n); ::_thesis: ex z being Element of ISOM (RLMSpace n) st S1[x,y,z] 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 ; ::_thesis: S1[x,y,z] take x1 ; ::_thesis: ex g being Function st ( x1 = x & g = y & z = x1 * g ) take y1 ; ::_thesis: ( x1 = x & y1 = y & z = x1 * y1 ) thus ( x1 = x & y1 = y & z = x1 * y1 ) ; ::_thesis: verum end; consider o being BinOp of (ISOM (RLMSpace n)) such that A2: for a, b being Element of ISOM (RLMSpace n) holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1); take G = multMagma(# (ISOM (RLMSpace n)),o #); ::_thesis: ( the carrier of G = ISOM (RLMSpace n) & ( for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds the multF of G . (f,g) = f * g ) ) for f, g being 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; ::_thesis: ( f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) implies the multF of G . (f,g) = f * g ) assume ( f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) ) ; ::_thesis: the multF of G . (f,g) = f * g then ex f1, g1 being Function st ( f1 = f & g1 = g & o . (f,g) = f1 * g1 ) by A2; hence the multF of G . (f,g) = f * g ; ::_thesis: verum end; hence ( the carrier of G = ISOM (RLMSpace n) & ( for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds the multF of G . (f,g) = f * g ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict multMagma st the carrier of b1 = ISOM (RLMSpace n) & ( for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds the multF of b1 . (f,g) = f * g ) & the carrier of b2 = ISOM (RLMSpace n) & ( for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds the multF of b2 . (f,g) = f * g ) holds b1 = b2 proof set V = RLMSpace n; let G1, G2 be strict multMagma ; ::_thesis: ( the carrier of G1 = ISOM (RLMSpace n) & ( for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds the multF of G1 . (f,g) = f * g ) & the carrier of G2 = ISOM (RLMSpace n) & ( for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds the multF of G2 . (f,g) = f * g ) implies G1 = G2 ) assume that A3: the carrier of G1 = ISOM (RLMSpace n) and A4: for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds the multF of G1 . (f,g) = f * g and A5: the carrier of G2 = ISOM (RLMSpace n) and A6: for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds the multF of G2 . (f,g) = f * g ; ::_thesis: G1 = G2 now__::_thesis:_for_f,_g_being_Element_of_G1_holds_the_multF_of_G1_._(f,g)_=_the_multF_of_G2_._(f,g) let f, g be Element of G1; ::_thesis: the multF of G1 . (f,g) = the multF of G2 . (f,g) 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 ; ::_thesis: verum end; hence G1 = G2 by A3, A5, BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def9 defines IsomGroup VECTMETR:def_9_:_ for n being Element of NAT for b2 being strict multMagma holds ( b2 = IsomGroup n iff ( the carrier of b2 = ISOM (RLMSpace n) & ( for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds the multF of b2 . (f,g) = f * g ) ) ); registration let n be Element of NAT ; cluster IsomGroup n -> non empty strict ; coherence not IsomGroup n is empty proof the carrier of (IsomGroup n) = ISOM (RLMSpace n) by Def9; hence not IsomGroup n is empty ; ::_thesis: verum end; end; registration let n be Element of NAT ; cluster IsomGroup n -> strict Group-like associative ; coherence ( IsomGroup n is associative & IsomGroup n is Group-like ) proof now__::_thesis:_for_x,_y,_z_being_Element_of_(IsomGroup_n)_holds_(x_*_y)_*_z_=_x_*_(y_*_z) let x, y, z be Element of (IsomGroup n); ::_thesis: (x * y) * z = x * (y * z) 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 ; ::_thesis: verum end; hence IsomGroup n is associative by GROUP_1:def_3; ::_thesis: IsomGroup n is Group-like ex e being Element of (IsomGroup n) st for h being Element of (IsomGroup n) holds ( h * e = h & e * h = h & ex g being 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 ; ::_thesis: for h being Element of (IsomGroup n) holds ( h * e = h & e * h = h & ex g being Element of (IsomGroup n) st ( h * g = e & g * h = e ) ) let h be Element of (IsomGroup n); ::_thesis: ( h * e = h & e * h = h & ex g being Element of (IsomGroup n) st ( h * g = e & g * h = e ) ) 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 ; ::_thesis: ( e * h = h & ex g being Element of (IsomGroup n) st ( h * g = e & g * h = e ) ) thus e * h = (id the carrier of (RLMSpace n)) * h1 by A6, A7, Def9 .= h by FUNCT_2:17 ; ::_thesis: ex g being Element of (IsomGroup n) st ( h * g = e & g * h = e ) 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 ; ::_thesis: ( h * g = e & g * h = e ) thus h * g = h1 * (h1 ") by A7, A9, Def9 .= e by A8, TOPS_2:52 ; ::_thesis: g * h = e thus g * h = (h1 ") * h1 by A7, A9, Def9 .= id (dom h1) by A8, TOPS_2:52 .= e by FUNCT_2:def_1 ; ::_thesis: verum end; hence IsomGroup n is Group-like by GROUP_1:def_2; ::_thesis: verum end; end; theorem Th10: :: VECTMETR:10 for n being Element of NAT holds 1_ (IsomGroup n) = id (RLMSpace n) proof let n be Element of NAT ; ::_thesis: 1_ (IsomGroup n) = id (RLMSpace n) A1: id (RLMSpace n) in ISOM (RLMSpace n) by Def4; then reconsider e = id (RLMSpace n) as Element of (IsomGroup n) by Def9; now__::_thesis:_for_h_being_Element_of_(IsomGroup_n)_holds_ (_h_*_e_=_h_&_e_*_h_=_h_) let h be Element of (IsomGroup n); ::_thesis: ( h * e = h & e * h = h ) 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 ; ::_thesis: e * h = h thus e * h = (id the carrier of (RLMSpace n)) * h1 by A1, A2, Def9 .= h by FUNCT_2:17 ; ::_thesis: verum end; hence 1_ (IsomGroup n) = id (RLMSpace n) by GROUP_1:4; ::_thesis: verum end; theorem Th11: :: VECTMETR:11 for n being Element of NAT for f being Element of (IsomGroup n) for g being Function of (RLMSpace n),(RLMSpace n) st f = g holds f " = g " proof let n be Element of NAT ; ::_thesis: for f being Element of (IsomGroup n) for g being Function of (RLMSpace n),(RLMSpace n) st f = g holds f " = g " let f be Element of (IsomGroup n); ::_thesis: for g being Function of (RLMSpace n),(RLMSpace n) st f = g holds f " = g " let g be Function of (RLMSpace n),(RLMSpace n); ::_thesis: ( f = g implies f " = g " ) 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 ; ::_thesis: 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 Th10 ; f * g1 = f1 * (g ") by A1, A3, Def9 .= id (RLMSpace n) by A2, A4, TOPS_2:52 .= 1_ (IsomGroup n) by Th10 ; hence f " = g " by A5, GROUP_1:5; ::_thesis: verum 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: :: VECTMETR:def 10 for A, B being Element of (RLMSpace n) holds ( [A,B] in it iff ex f being Function st ( f in the carrier of G & f . A = B ) ); existence ex b1 being Relation of the carrier of (RLMSpace n) st for A, B being Element of (RLMSpace n) holds ( [A,B] in b1 iff ex f being Function st ( f in the carrier of G & f . A = B ) ) proof defpred S1[ set , set ] means ex f being Function st ( f in the carrier of G & f . $1 = $2 ); consider R being Relation of the carrier of (RLMSpace n), the carrier of (RLMSpace n) such that A1: for x, y being set holds ( [x,y] in R iff ( x in the carrier of (RLMSpace n) & y in the carrier of (RLMSpace n) & S1[x,y] ) ) from RELSET_1:sch_1(); take R ; ::_thesis: for A, B being Element of (RLMSpace n) holds ( [A,B] in R iff ex f being Function st ( f in the carrier of G & f . A = B ) ) let A, B be Element of (RLMSpace n); ::_thesis: ( [A,B] in R iff ex f being Function st ( f in the carrier of G & f . A = B ) ) thus ( [A,B] in R iff ex f being Function st ( f in the carrier of G & f . A = B ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Relation of the carrier of (RLMSpace n) st ( for A, B being Element of (RLMSpace n) holds ( [A,B] in b1 iff ex f being Function st ( f in the carrier of G & f . A = B ) ) ) & ( for A, B being Element of (RLMSpace n) holds ( [A,B] in b2 iff ex f being Function st ( f in the carrier of G & f . A = B ) ) ) holds b1 = b2 proof let R1, R2 be Relation of the carrier of (RLMSpace n); ::_thesis: ( ( for A, B being Element of (RLMSpace n) holds ( [A,B] in R1 iff ex f being Function st ( f in the carrier of G & f . A = B ) ) ) & ( for A, B being Element of (RLMSpace n) holds ( [A,B] in R2 iff ex f being Function st ( f in the carrier of G & f . A = B ) ) ) implies R1 = R2 ) assume that A2: for A, B being Element of (RLMSpace n) holds ( [A,B] in R1 iff ex f being Function st ( f in the carrier of G & f . A = B ) ) and A3: for A, B being Element of (RLMSpace n) holds ( [A,B] in R2 iff ex f being Function st ( f in the carrier of G & f . A = B ) ) ; ::_thesis: R1 = R2 now__::_thesis:_for_a,_b_being_set_holds_ (_(_[a,b]_in_R1_implies_[a,b]_in_R2_)_&_(_[a,b]_in_R2_implies_[a,b]_in_R1_)_) let a, b be set ; ::_thesis: ( ( [a,b] in R1 implies [a,b] in R2 ) & ( [a,b] in R2 implies [a,b] in R1 ) ) thus ( [a,b] in R1 implies [a,b] in R2 ) ::_thesis: ( [a,b] in R2 implies [a,b] in R1 ) proof assume A4: [a,b] in R1 ; ::_thesis: [a,b] in R2 then reconsider a1 = a, b1 = b as Element of (RLMSpace n) by ZFMISC_1:87; ex f being Function st ( f in the carrier of G & f . a1 = b1 ) by A2, A4; hence [a,b] in R2 by A3; ::_thesis: verum end; assume A5: [a,b] in R2 ; ::_thesis: [a,b] in R1 then reconsider a1 = a, b1 = b as Element of (RLMSpace n) by ZFMISC_1:87; ex f being Function st ( f in the carrier of G & f . a1 = b1 ) by A3, A5; hence [a,b] in R1 by A2; ::_thesis: verum end; hence R1 = R2 by RELAT_1:def_2; ::_thesis: verum end; end; :: deftheorem Def10 defines SubIsomGroupRel VECTMETR:def_10_:_ for n being Element of NAT for G being Subgroup of IsomGroup n for b3 being Relation of the carrier of (RLMSpace n) holds ( b3 = SubIsomGroupRel G iff for A, B being Element of (RLMSpace n) holds ( [A,B] in b3 iff ex f being Function st ( f in the carrier of G & f . A = B ) ) ); registration let n be Element of NAT ; let G be Subgroup of IsomGroup n; cluster SubIsomGroupRel G -> total symmetric transitive ; coherence ( SubIsomGroupRel G is total & SubIsomGroupRel G is symmetric & SubIsomGroupRel G is transitive ) proof set S = SubIsomGroupRel G; set X = the carrier of (RLMSpace n); now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(RLMSpace_n)_holds_ [x,x]_in_SubIsomGroupRel_G let x be set ; ::_thesis: ( x in the carrier of (RLMSpace n) implies [x,x] in SubIsomGroupRel G ) assume x in the carrier of (RLMSpace n) ; ::_thesis: [x,x] in SubIsomGroupRel G then reconsider x1 = x as Element of (RLMSpace n) ; 1_ (IsomGroup n) = id (RLMSpace n) by Th10; then id (RLMSpace n) in G by GROUP_2:46; then A1: id (RLMSpace n) in the carrier of G by STRUCT_0:def_5; (id (RLMSpace n)) . x1 = x1 by FUNCT_1:18; hence [x,x] in SubIsomGroupRel G by A1, Def10; ::_thesis: verum end; then A2: SubIsomGroupRel G is_reflexive_in the carrier of (RLMSpace n) by RELAT_2:def_1; then A3: field (SubIsomGroupRel G) = the carrier of (RLMSpace n) by ORDERS_1:13; dom (SubIsomGroupRel G) = the carrier of (RLMSpace n) by A2, ORDERS_1:13; hence SubIsomGroupRel G is total by PARTFUN1:def_2; ::_thesis: ( SubIsomGroupRel G is symmetric & SubIsomGroupRel G is transitive ) now__::_thesis:_for_x,_y_being_set_st_x_in_the_carrier_of_(RLMSpace_n)_&_y_in_the_carrier_of_(RLMSpace_n)_&_[x,y]_in_SubIsomGroupRel_G_holds_ [y,x]_in_SubIsomGroupRel_G let x, y be set ; ::_thesis: ( x in the carrier of (RLMSpace n) & y in the carrier of (RLMSpace n) & [x,y] in SubIsomGroupRel G implies [y,x] in SubIsomGroupRel G ) assume that A4: ( x in the carrier of (RLMSpace n) & y in the carrier of (RLMSpace n) ) and A5: [x,y] in SubIsomGroupRel G ; ::_thesis: [y,x] in SubIsomGroupRel G reconsider x1 = x, y1 = y as Element of (RLMSpace n) by A4; consider f being 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) by TARSKI:def_3; 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 Th11 .= f " by TOPS_2:def_4 ; hence [y,x] in SubIsomGroupRel G by A9, Def10; ::_thesis: verum end; then SubIsomGroupRel G is_symmetric_in the carrier of (RLMSpace n) by RELAT_2:def_3; hence SubIsomGroupRel G is symmetric by A3, RELAT_2:def_11; ::_thesis: SubIsomGroupRel G is transitive now__::_thesis:_for_x,_y,_z_being_set_st_x_in_the_carrier_of_(RLMSpace_n)_&_y_in_the_carrier_of_(RLMSpace_n)_&_z_in_the_carrier_of_(RLMSpace_n)_&_[x,y]_in_SubIsomGroupRel_G_&_[y,z]_in_SubIsomGroupRel_G_holds_ [x,z]_in_SubIsomGroupRel_G let x, y, z be set ; ::_thesis: ( x in the carrier of (RLMSpace n) & y in the carrier of (RLMSpace n) & z in the carrier of (RLMSpace n) & [x,y] in SubIsomGroupRel G & [y,z] in SubIsomGroupRel G implies [x,z] in SubIsomGroupRel G ) assume that A10: ( x in the carrier of (RLMSpace n) & y in the carrier of (RLMSpace n) & z in the carrier of (RLMSpace n) ) and A11: [x,y] in SubIsomGroupRel G and A12: [y,z] in SubIsomGroupRel G ; ::_thesis: [x,z] in SubIsomGroupRel G reconsider x1 = x, y1 = y, z1 = z as Element of (RLMSpace n) by A10; consider f being 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) by TARSKI:def_3; f in the carrier of (IsomGroup n) by A13, A15; then A16: f in ISOM (RLMSpace n) by Def9; consider g being 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, TARSKI:def_3; ( f2 in G & g2 in G ) by STRUCT_0:def_5; 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, STRUCT_0:def_5; 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 SubIsomGroupRel G by A21, Def10; ::_thesis: verum end; then SubIsomGroupRel G is_transitive_in the carrier of (RLMSpace n) by RELAT_2:def_8; hence SubIsomGroupRel G is transitive by A3, RELAT_2:def_16; ::_thesis: verum end; end;