:: Real Linear-Metric Space and Isometric Functions
:: by Robert Milewski
::
:: Copyright (c) 1998-2021 Association of Mizar Users

definition
let V be non empty MetrStruct ;
attr V is convex means :: 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 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
|.((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
|.((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
coherence
for b1 being non empty MetrSpace st b1 is convex holds
b1 is internal
proof end;
end;

registration
existence
ex b1 being non empty MetrSpace st b1 is convex
proof end;
end;

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 ;
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 Relation-like the carrier of V -defined the carrier of V -valued non empty 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 end;
end;

definition
let V be non empty MetrStruct ;
defpred S1[ object ] means $1 is onto isometric Function of V,V; func ISOM V -> set means :Def4: :: VECTMETR:def 4 for x being object holds ( x in it iff x is onto isometric Function of V,V ); existence ex b1 being set st for x being object 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 object holds ( x in b1 iff x is onto isometric Function of V,V ) ) & ( for x being object 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 object 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 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 end; end; registration let V be non empty Reflexive discerning MetrStruct ; let f be onto isometric Function of V,V; coherence ( f " is onto & f " is isometric ) proof end; end; registration let V be non empty MetrStruct ; let f, g be onto isometric Function of V,V; cluster g * 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 end; end; registration let V be non empty MetrStruct ; cluster ISOM V -> non empty ; coherence not ISOM V is empty proof end; end; definition end; registration 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)) = |.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)) = |.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 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 end; theorem :: VECTMETR:3 canceled; theorem :: VECTMETR:4 canceled; theorem :: VECTMETR:5 canceled; ::$CT 3
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) = |.r.| * (Norm v)
proof 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 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 (),() holds rng f = REAL n
proof end;

definition
let n be Element of NAT ;
func IsomGroup n -> strict multMagma means :Def9: :: VECTMETR:def 9
( the carrier of it = ISOM () & ( for f, g being Function st f in ISOM () & g in ISOM () holds
the multF of it . (f,g) = f * g ) );
existence
ex b1 being strict multMagma st
( the carrier of b1 = ISOM () & ( for f, g being Function st f in ISOM () & g in ISOM () holds
the multF of b1 . (f,g) = f * g ) )
proof end;
uniqueness
for b1, b2 being strict multMagma st the carrier of b1 = ISOM () & ( for f, g being Function st f in ISOM () & g in ISOM () holds
the multF of b1 . (f,g) = f * g ) & the carrier of b2 = ISOM () & ( for f, g being Function st f in ISOM () & g in ISOM () 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 () & ( for f, g being Function st f in ISOM () & g in ISOM () 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 ;
coherence
proof end;
end;

theorem Th7: :: VECTMETR:10
for n being Element of NAT holds 1_ () = id ()
proof end;

theorem Th8: :: VECTMETR:11
for n being Element of NAT
for f being Element of ()
for g being Function of (),() 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 () means :Def10: :: VECTMETR:def 10
for A, B being Element of () 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 () st
for A, B being Element of () 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 () st ( for A, B being Element of () 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 () 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 () holds
( b3 = SubIsomGroupRel G iff for A, B being Element of () 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;
coherence
proof end;
end;