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


begin

definition
let V be non empty MetrStruct ;
attr V 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 ;
attr V 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 end;

registration
cluster non empty Reflexive discerning symmetric triangle convex -> non empty internal MetrStruct ;
coherence
for b1 being non empty MetrSpace st b1 is convex holds
b1 is internal
proof end;
end;

registration
cluster non empty Reflexive discerning symmetric triangle Discerning convex MetrStruct ;
existence
ex b1 being non empty MetrSpace st b1 is convex
proof end;
end;

begin

definition
let V be non empty MetrStruct ;
let f be Function of V,V;
attr f 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 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 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 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 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 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 end;
end;

registration
let V be non empty Reflexive discerning MetrStruct ;
cluster Function-like quasi_total isometric -> one-to-one 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 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;
cluster f " -> onto isometric ;
coherence
( f " is onto & f " is isometric )
proof 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;
cluster g * f -> onto isometric Function of V,V;
coherence
for b1 being Function of V,V st b1 = f * g holds
( b1 is onto & b1 is isometric )
proof 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 end;
end;

begin

definition
attr c1 is strict ;
struct RLSMetrStruct -> RLSStruct , MetrStruct ;
aggr RLSMetrStruct(# carrier, distance, ZeroF, addF, Mult #) -> RLSMetrStruct ;
end;

registration
cluster non empty strict RLSMetrStruct ;
existence
ex b1 being RLSMetrStruct st
( not b1 is empty & b1 is strict )
proof 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 ;
attr V 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 ;
attr V 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 Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Reflexive discerning symmetric triangle strict homogeneous translatible 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 end;
end;

definition
mode RealLinearMetrSpace is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Reflexive discerning symmetric triangle 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 end;

theorem :: VECTMETR:7
for V being non empty right_complementable Abelian add-associative right_zeroed triangle translatible RLSMetrStruct
for v, w being Element of V holds Norm (v + w) <= (Norm v) + (Norm w)
proof 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 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 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 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 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 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 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 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 end;
end;

theorem Th10: :: VECTMETR:10
for n being Element of NAT holds 1_ (IsomGroup n) = id (RLMSpace n)
proof 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 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 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 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 end;
end;