:: Real Linear-Metric Space and Isometric Functions
:: by Robert Milewski
::
:: Received November 3, 1998
:: Copyright (c) 1998 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 b₁ being non empty MetrSpace st b₁ is convex holds
b₁ is internal

proof end;

end;

registration

cluster non empty Reflexive discerning symmetric triangle Discerning convex MetrStruct ;
existence
ex b₁ being non empty MetrSpace st b₁ 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 b₁ being Function of V,V st
( b₁ is onto & b₁ is isometric )

proof end;

end;

definition

let V be non empty MetrStruct ;
defpred S₁[ 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 b₁ being set st
for x being set holds
( x in b₁ iff x is onto isometric Function of V,V )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being set holds
( x in b₁ iff x is onto isometric Function of V,V ) ) & ( for x being set holds
( x in b₂ iff x is onto isometric Function of V,V ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines ISOM VECTMETR:def 4 :
for V being non empty MetrStruct
for b₂ being set holds
( b₂ = ISOM V iff for x being set holds
( x in b₂ 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 b₁ being Function of V,V st b₁ is isometric holds
b₁ 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 b₁ being Function of V,V st b₁ = f * g holds
( b₁ is onto & b₁ 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 c₁ is strict ;
struct RLSMetrStruct -> RLSStruct , MetrStruct ;
aggr RLSMetrStruct(# carrier, distance, ZeroF, addF, Mult #) -> RLSMetrStruct ;

end;

registration

cluster non empty strict RLSMetrStruct ;
existence
ex b₁ being RLSMetrStruct st
( not b₁ is empty & b₁ 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 b₁ being non empty RLSMetrStruct st
( b₁ is strict & b₁ is Abelian & b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable & b₁ is vector-distributive & b₁ is scalar-distributive & b₁ is scalar-associative & b₁ is scalar-unital & b₁ is Reflexive & b₁ is discerning & b₁ is symmetric & b₁ is triangle & b₁ is homogeneous & b₁ 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 b₁ being strict RealLinearMetrSpace st
( the carrier of b₁ = REAL n & the distance of b₁ = Pitag_dist n & 0. b₁ = 0* n & ( for x, y being Element of REAL n holds the addF of b₁ . (x,y) = x + y ) & ( for x being Element of REAL n
for r being Element of REAL holds the Mult of b₁ . (r,x) = r * x ) )

proof end;

uniqueness
for b₁, b₂ being strict RealLinearMetrSpace st the carrier of b₁ = REAL n & the distance of b₁ = Pitag_dist n & 0. b₁ = 0* n & ( for x, y being Element of REAL n holds the addF of b₁ . (x,y) = x + y ) & ( for x being Element of REAL n
for r being Element of REAL holds the Mult of b₁ . (r,x) = r * x ) & the carrier of b₂ = REAL n & the distance of b₂ = Pitag_dist n & 0. b₂ = 0* n & ( for x, y being Element of REAL n holds the addF of b₂ . (x,y) = x + y ) & ( for x being Element of REAL n
for r being Element of REAL holds the Mult of b₂ . (r,x) = r * x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines RLMSpace VECTMETR:def 8 :
for n being Element of NAT
for b₂ being strict RealLinearMetrSpace holds
( b₂ = RLMSpace n iff ( the carrier of b₂ = REAL n & the distance of b₂ = Pitag_dist n & 0. b₂ = 0* n & ( for x, y being Element of REAL n holds the addF of b₂ . (x,y) = x + y ) & ( for x being Element of REAL n
for r being Element of REAL holds the Mult of b₂ . (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 b₁ being strict multMagma st
( the carrier of b₁ = ISOM (RLMSpace n) & ( for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds
the multF of b₁ . (f,g) = f * g ) )

proof end;

uniqueness
for b₁, b₂ being strict multMagma st the carrier of b₁ = ISOM (RLMSpace n) & ( for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds
the multF of b₁ . (f,g) = f * g ) & the carrier of b₂ = ISOM (RLMSpace n) & ( for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds
the multF of b₂ . (f,g) = f * g ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines IsomGroup VECTMETR:def 9 :
for n being Element of NAT
for b₂ being strict multMagma holds
( b₂ = IsomGroup n iff ( the carrier of b₂ = ISOM (RLMSpace n) & ( for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds
the multF of b₂ . (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 b₁ being Relation of the carrier of (RLMSpace n) st
for A, B being Element of (RLMSpace n) holds
( [A,B] in b₁ iff ex f being Function st
( f in the carrier of G & f . A = B ) )

proof end;

uniqueness
for b₁, b₂ being Relation of the carrier of (RLMSpace n) st ( for A, B being Element of (RLMSpace n) holds
( [A,B] in b₁ 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 b₂ iff ex f being Function st
( f in the carrier of G & f . A = B ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines SubIsomGroupRel VECTMETR:def 10 :
for n being Element of NAT
for G being Subgroup of IsomGroup n
for b₃ being Relation of the carrier of (RLMSpace n) holds
( b₃ = SubIsomGroupRel G iff for A, B being Element of (RLMSpace n) holds
( [A,B] in b₃ 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;