:: by Robert Milewski

::

:: Received November 3, 1998

:: Copyright (c) 1998-2021 Association of Mizar Users

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

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 ;

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

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

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

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

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

for b_{1} being non empty MetrSpace st b_{1} is convex holds

b_{1} is internal
end;

cluster non empty Reflexive discerning symmetric triangle convex -> non empty internal for MetrStruct ;

coherence for b

b

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

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

registration

let V be non empty MetrStruct ;

ex b_{1} being Function of V,V st

( b_{1} is onto & b_{1} is isometric )

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

( b

proof end;

definition

let V be non empty MetrStruct ;

defpred S_{1}[ object ] means $1 is onto isometric Function of V,V;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff x is onto isometric Function of V,V )

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff x is onto isometric Function of V,V ) ) & ( for x being object holds

( x in b_{2} iff x is onto isometric Function of V,V ) ) holds

b_{1} = b_{2}

end;
defpred S

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 for x being object holds

( x in it iff x is onto isometric Function of V,V );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def4 defines ISOM VECTMETR:def 4 :

for V being non empty MetrStruct

for b_{2} being set holds

( b_{2} = ISOM V iff for x being object holds

( x in b_{2} iff x is onto isometric Function of V,V ) );

for V being non empty MetrStruct

for b

( b

( x in b

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

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

registration

let V be non empty Reflexive discerning MetrStruct ;

for b_{1} being Function of V,V st b_{1} is isometric holds

b_{1} is one-to-one

end;
cluster Function-like quasi_total isometric -> one-to-one for Element of bool [: the carrier of V, the carrier of V:];

coherence for b

b

proof 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 )

end;
let f be onto isometric Function of V,V;

coherence

( f " is onto & f " is isometric )

proof end;

registration

let V be non empty MetrStruct ;

let f, g be onto isometric Function of V,V;

coherence

for b_{1} being Function of V,V st b_{1} = f * g holds

( b_{1} is onto & b_{1} is isometric )

end;
let f, g be onto isometric Function of V,V;

coherence

for b

( b

proof end;

definition

attr c_{1} is strict ;

struct RLSMetrStruct -> RLSStruct , MetrStruct ;

aggr RLSMetrStruct(# carrier, distance, ZeroF, addF, Mult #) -> RLSMetrStruct ;

end;
struct RLSMetrStruct -> RLSStruct , MetrStruct ;

aggr RLSMetrStruct(# carrier, distance, ZeroF, addF, Mult #) -> RLSMetrStruct ;

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

coherence

not RLSMetrStruct(# X,F,O,B,G #) is empty ;

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

coherence

not RLSMetrStruct(# X,F,O,B,G #) is empty ;

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

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 ;

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

for u, w, v being Element of V holds dist (v,w) = dist ((v + u),(w + u));

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

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

for V being non empty RLSMetrStruct

for v being Element of V holds Norm v = dist ((0. V),v);

registration

ex b_{1} being non empty RLSMetrStruct st

( b_{1} is strict & b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is vector-distributive & b_{1} is scalar-distributive & b_{1} is scalar-associative & b_{1} is scalar-unital & b_{1} is Reflexive & b_{1} is discerning & b_{1} is symmetric & b_{1} is triangle & b_{1} is homogeneous & b_{1} is translatible )
end;

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 b

( b

proof 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;
::$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)

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)

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)

for v, w being Element of V holds dist (v,w) = Norm (w - v)

proof end;

definition

let n be Element of NAT ;

ex b_{1} being strict RealLinearMetrSpace st

( the carrier of b_{1} = REAL n & the distance of b_{1} = Pitag_dist n & 0. b_{1} = 0* n & ( for x, y being Element of REAL n holds the addF of b_{1} . (x,y) = x + y ) & ( for x being Element of REAL n

for r being Element of REAL holds the Mult of b_{1} . (r,x) = r * x ) )

for b_{1}, b_{2} being strict RealLinearMetrSpace st the carrier of b_{1} = REAL n & the distance of b_{1} = Pitag_dist n & 0. b_{1} = 0* n & ( for x, y being Element of REAL n holds the addF of b_{1} . (x,y) = x + y ) & ( for x being Element of REAL n

for r being Element of REAL holds the Mult of b_{1} . (r,x) = r * x ) & the carrier of b_{2} = REAL n & the distance of b_{2} = Pitag_dist n & 0. b_{2} = 0* n & ( for x, y being Element of REAL n holds the addF of b_{2} . (x,y) = x + y ) & ( for x being Element of REAL n

for r being Element of REAL holds the Mult of b_{2} . (r,x) = r * x ) holds

b_{1} = b_{2}

end;
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 ( 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 ) );

ex b

( the carrier of b

for r being Element of REAL holds the Mult of b

proof end;

uniqueness for b

for r being Element of REAL holds the Mult of b

for r being Element of REAL holds the Mult of b

b

proof end;

:: deftheorem Def8 defines RLMSpace VECTMETR:def 8 :

for n being Element of NAT

for b_{2} being strict RealLinearMetrSpace holds

( b_{2} = RLMSpace n iff ( the carrier of b_{2} = REAL n & the distance of b_{2} = Pitag_dist n & 0. b_{2} = 0* n & ( for x, y being Element of REAL n holds the addF of b_{2} . (x,y) = x + y ) & ( for x being Element of REAL n

for r being Element of REAL holds the Mult of b_{2} . (r,x) = r * x ) ) );

for n being Element of NAT

for b

( b

for r being Element of REAL holds the Mult of b

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

for f being onto isometric Function of (RLMSpace n),(RLMSpace n) holds rng f = REAL n

proof end;

definition

let n be Element of NAT ;

ex b_{1} being strict multMagma st

( the carrier of b_{1} = ISOM (RLMSpace n) & ( for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds

the multF of b_{1} . (f,g) = f * g ) )

for b_{1}, b_{2} being strict multMagma st the carrier of b_{1} = ISOM (RLMSpace n) & ( for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds

the multF of b_{1} . (f,g) = f * g ) & the carrier of b_{2} = ISOM (RLMSpace n) & ( for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds

the multF of b_{2} . (f,g) = f * g ) holds

b_{1} = b_{2}

end;
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 ( 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 ) );

ex b

( the carrier of b

the multF of b

proof end;

uniqueness for b

the multF of b

the multF of b

b

proof end;

:: deftheorem Def9 defines IsomGroup VECTMETR:def 9 :

for n being Element of NAT

for b_{2} being strict multMagma holds

( b_{2} = IsomGroup n iff ( the carrier of b_{2} = ISOM (RLMSpace n) & ( for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds

the multF of b_{2} . (f,g) = f * g ) ) );

for n being Element of NAT

for b

( b

the multF of b

registration

let n be Element of NAT ;

coherence

( IsomGroup n is associative & IsomGroup n is Group-like )

end;
coherence

( IsomGroup n is associative & IsomGroup n is Group-like )

proof end;

theorem Th8: :: 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 "

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;

ex b_{1} being Relation of the carrier of (RLMSpace n) st

for A, B being Element of (RLMSpace n) holds

( [A,B] in b_{1} iff ex f being Function st

( f in the carrier of G & f . A = B ) )

for b_{1}, b_{2} being Relation of the carrier of (RLMSpace n) st ( for A, B being Element of (RLMSpace n) holds

( [A,B] in b_{1} 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_{2} iff ex f being Function st

( f in the carrier of G & f . A = B ) ) ) holds

b_{1} = b_{2}

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

ex b

for A, B being Element of (RLMSpace n) holds

( [A,B] in b

( f in the carrier of G & f . A = B ) )

proof end;

uniqueness for b

( [A,B] in b

( f in the carrier of G & f . A = B ) ) ) & ( for A, B being Element of (RLMSpace n) holds

( [A,B] in b

( f in the carrier of G & f . A = B ) ) ) holds

b

proof end;

:: deftheorem Def10 defines SubIsomGroupRel VECTMETR:def 10 :

for n being Element of NAT

for G being Subgroup of IsomGroup n

for b_{3} being Relation of the carrier of (RLMSpace n) holds

( b_{3} = SubIsomGroupRel G iff for A, B being Element of (RLMSpace n) holds

( [A,B] in b_{3} iff ex f being Function st

( f in the carrier of G & f . A = B ) ) );

for n being Element of NAT

for G being Subgroup of IsomGroup n

for b

( b

( [A,B] in b

( f in the carrier of G & f . A = B ) ) );

registration

let n be Element of NAT ;

let G be Subgroup of IsomGroup n;

coherence

( SubIsomGroupRel G is total & SubIsomGroupRel G is symmetric & SubIsomGroupRel G is transitive )

end;
let G be Subgroup of IsomGroup n;

coherence

( SubIsomGroupRel G is total & SubIsomGroupRel G is symmetric & SubIsomGroupRel G is transitive )

proof end;