:: 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;