:: Real Linear-Metric Space and Isometric Functions
:: by Robert Milewski
::
:: Received November 3, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


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 &amp; r <= 1 holds
ex z being Element of V st
( dist (x,z) = r * (dist (x,y)) &amp; 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 &amp; r <= 1 holds
ex z being Element of V st
( dist (x,z) = r * (dist (x,y)) &amp; 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 &amp; q > 0 holds
ex f being FinSequence of the carrier of V st
( f /. 1 = x &amp; f /. (len f) = y &amp; ( for i being Element of NAT st 1 <= i &amp; i <= (len f) - 1 holds
dist ((f /. i),(f /. (i + 1))) < p ) &amp; ( for F being FinSequence of REAL st len F = (len f) - 1 &amp; ( for i being Element of NAT st 1 <= i &amp; 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 &amp; q > 0 holds
ex f being FinSequence of the carrier of V st
( f /. 1 = x &amp; f /. (len f) = y &amp; ( for i being Element of NAT st 1 <= i &amp; i <= (len f) - 1 holds
dist ((f /. i),(f /. (i + 1))) < p ) &amp; ( for F being FinSequence of REAL st len F = (len f) - 1 &amp; ( for i being Element of NAT st 1 <= i &amp; 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 &amp; f /. (len f) = y &amp; ( for i being Element of NAT st 1 <= i &amp; i <= (len f) - 1 holds
dist ((f /. i),(f /. (i + 1))) < p ) &amp; ( for F being FinSequence of REAL st len F = (len f) - 1 &amp; ( for i being Element of NAT st 1 <= i &amp; i <= len F holds
F /. i = dist ((f /. i),(f /. (i + 1))) ) holds
dist (x,y) = Sum F ) )
proofend;

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
proofend;
end;

registration
cluster non empty Reflexive discerning symmetric triangle Discerning convex for MetrStruct ;
existence
 ex b1 being non empty MetrSpace st b1 is convex
proofend;
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 &amp; id V is isometric )
proofend;
end;

theorem :: VECTMETR:2
for V being non empty MetrStruct holds
( id V is onto &amp; 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 &amp; b1 is isometric )
proofend;
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 )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is onto isometric Function of V,V ) ) &amp; ( for x being set holds
( x in b2 iff x is onto isometric Function of V,V ) ) holds
b1 = b2
proofend;
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))
proofend;
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
proofend;
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 &amp; f " is isometric )
proofend;
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 &amp; 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 &amp; b1 is isometric )
proofend;
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 &amp; f * g is isometric ) ;

registration
let V be non empty MetrStruct ;
cluster ISOM V ->  non empty ;
coherence
 not ISOM V is empty
proofend;
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 &amp; b1 is strict )
proofend;
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 &amp; b1 is Abelian &amp; b1 is add-associative &amp; b1 is right_zeroed &amp; b1 is right_complementable &amp; b1 is vector-distributive &amp; b1 is scalar-distributive &amp; b1 is scalar-associative &amp; b1 is scalar-unital &amp; b1 is Reflexive &amp; b1 is discerning &amp; b1 is symmetric &amp; b1 is triangle &amp; b1 is homogeneous &amp; b1 is translatible )
proofend;
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)
proofend;

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)
proofend;

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)
proofend;

definition
let n be Element of NAT ;
func RLMSpace n ->  strict RealLinearMetrSpace means :Def8: :: VECTMETR:def 8
( the carrier of it = REAL n &amp; the distance of it = Pitag_dist n &amp; 0. it = 0* n &amp; ( for x, y being Element of REAL n holds the addF of it . (x,y) = x + y ) &amp; ( 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 &amp; the distance of b1 = Pitag_dist n &amp; 0. b1 = 0* n &amp; ( for x, y being Element of REAL n holds the addF of b1 . (x,y) = x + y ) &amp; ( for x being Element of REAL n
for r being Element of REAL holds the Mult of b1 . (r,x) = r * x ) )
proofend;
uniqueness
 for b1, b2 being strict RealLinearMetrSpace st the carrier of b1 = REAL n &amp; the distance of b1 = Pitag_dist n &amp; 0. b1 = 0* n &amp; ( for x, y being Element of REAL n holds the addF of b1 . (x,y) = x + y ) &amp; ( for x being Element of REAL n
for r being Element of REAL holds the Mult of b1 . (r,x) = r * x ) &amp; the carrier of b2 = REAL n &amp; the distance of b2 = Pitag_dist n &amp; 0. b2 = 0* n &amp; ( for x, y being Element of REAL n holds the addF of b2 . (x,y) = x + y ) &amp; ( 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
proofend;
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 &amp; the distance of b2 = Pitag_dist n &amp; 0. b2 = 0* n &amp; ( for x, y being Element of REAL n holds the addF of b2 . (x,y) = x + y ) &amp; ( 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
proofend;

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) &amp; ( for f, g being Function st f in ISOM (RLMSpace n) &amp; 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) &amp; ( for f, g being Function st f in ISOM (RLMSpace n) &amp; g in ISOM (RLMSpace n) holds
the multF of b1 . (f,g) = f * g ) )
proofend;
uniqueness
 for b1, b2 being strict multMagma st the carrier of b1 = ISOM (RLMSpace n) &amp; ( for f, g being Function st f in ISOM (RLMSpace n) &amp; g in ISOM (RLMSpace n) holds
the multF of b1 . (f,g) = f * g ) &amp; the carrier of b2 = ISOM (RLMSpace n) &amp; ( for f, g being Function st f in ISOM (RLMSpace n) &amp; g in ISOM (RLMSpace n) holds
the multF of b2 . (f,g) = f * g ) holds
b1 = b2
proofend;
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) &amp; ( for f, g being Function st f in ISOM (RLMSpace n) &amp; 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
proofend;
end;

registration
let n be Element of NAT ;
cluster IsomGroup n ->  strict Group-like associative ;
coherence
 ( IsomGroup n is associative &amp; IsomGroup n is Group-like )
proofend;
end;

theorem Th10: :: VECTMETR:10
for n being Element of NAT holds 1_ (IsomGroup n) = id (RLMSpace n)
proofend;

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 "
proofend;

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 &amp; 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 &amp; f . A = B ) )
proofend;
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 &amp; f . A = B ) ) ) &amp; ( 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 &amp; f . A = B ) ) ) holds
b1 = b2
proofend;
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 &amp; 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 &amp; SubIsomGroupRel G is symmetric &amp; SubIsomGroupRel G is transitive )
proofend;
end;