:: VECTMETR semantic presentation

definition

let c₁ be non empty MetrStruct ;
attr a₁ is convex means :Def1: :: VECTMETR:def 1
for b₁, b₂ being Element of a₁
for b₃ being Real st 0 <= b₃ & b₃ <= 1 holds
ex b₄ being Element of a₁ st
( dist b₁,b₄ = b₃ * (dist b₁,b₂) & dist b₄,b₂ = (1 - b₃) * (dist b₁,b₂) );

end;

:: deftheorem Def1 defines convex VECTMETR:def 1 :

definition

let c₁ be non empty MetrStruct ;
attr a₁ is internal means :: VECTMETR:def 2
for b₁, b₂ being Element of a₁
for b₃, b₄ being Real st b₃ > 0 & b₄ > 0 holds
ex b₅ being FinSequence of the carrier of a₁ st
( b₅ /. 1 = b₁ & b₅ /. (len b₅) = b₂ & ( for b₆ being Nat st 1 <= b₆ & b₆ <= (len b₅) - 1 holds
dist (b₅ /. b₆),(b₅ /. (b₆ + 1)) < b₃ ) & ( for b₆ being FinSequence of REAL st len b₆ = (len b₅) - 1 & ( for b₇ being Nat st 1 <= b₇ & b₇ <= len b₆ holds
b₆ /. b₇ = dist (b₅ /. b₇),(b₅ /. (b₇ + 1)) ) holds
abs ((dist b₁,b₂) - (Sum b₆)) < b₄ ) );

end;

:: deftheorem Def2 defines internal VECTMETR:def 2 :

theorem Th1: :: VECTMETR:1

for b₁ being non empty MetrSpace st b₁ is convex holds
for b₂, b₃ being Element of b₁
for b₄ being Real st b₄ > 0 holds
ex b₅ being FinSequence of the carrier of b₁ st
( b₅ /. 1 = b₂ & b₅ /. (len b₅) = b₃ & ( for b₆ being Nat st 1 <= b₆ & b₆ <= (len b₅) - 1 holds
dist (b₅ /. b₆),(b₅ /. (b₆ + 1)) < b₄ ) & ( for b₆ being FinSequence of REAL st len b₆ = (len b₅) - 1 & ( for b₇ being Nat st 1 <= b₇ & b₇ <= len b₆ holds
b₆ /. b₇ = dist (b₅ /. b₇),(b₅ /. (b₇ + 1)) ) holds
dist b₂,b₃ = Sum b₆ ) )

proof end;

registration

cluster non empty convex -> non empty internal MetrStruct ;
coherence

proof end;

end;

registration

cluster non empty convex internal MetrStruct ;
existence

proof end;

end;

definition

mode Geometry is non empty Reflexive discerning symmetric triangle internal MetrStruct ;

end;

definition

let c₁ be non empty MetrStruct ;
let c₂ be Function of c₁,c₁;
attr a₂ is isometric means :Def3: :: VECTMETR:def 3
( rng a₂ = the carrier of a₁ & ( for b₁, b₂ being Element of a₁ holds dist b₁,b₂ = dist (a₂ . b₁),(a₂ . b₂) ) );

end;

:: deftheorem Def3 defines isometric VECTMETR:def 3 :

definition

let c₁ be non empty MetrStruct ;
func ISOM c₁ -> set means :Def4: :: VECTMETR:def 4
for b₁ being set holds
( b₁ in a₂ iff ex b₂ being Function of a₁,a₁ st
( b₂ = b₁ & b₂ is isometric ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines ISOM VECTMETR:def 4 :

definition

let c₁ be non empty MetrStruct ;
redefine func ISOM as ISOM c₁ -> Subset of (Funcs the carrier of a₁,the carrier of a₁);
coherence

proof end;

end;

theorem Th2: :: VECTMETR:2

for b₁ being non empty Reflexive discerning MetrStruct
for b₂ being Function of b₁,b₁ st b₂ is isometric holds
b₂ is one-to-one

proof end;

registration

let c₁ be non empty Reflexive discerning MetrStruct ;
cluster isometric -> one-to-one Relation of the carrier of a₁,the carrier of a₁;
coherence by Th2;

end;

registration

let c₁ be non empty MetrStruct ;
cluster isometric Relation of the carrier of a₁,the carrier of a₁;
existence

proof end;

end;

theorem Th3: :: VECTMETR:3

for b₁ being non empty Reflexive discerning MetrStruct
for b₂ being isometric Function of b₁,b₁ holds b₂ " is isometric

proof end;

theorem Th4: :: VECTMETR:4

for b₁ being non empty MetrStruct
for b₂, b₃ being isometric Function of b₁,b₁ holds b₂ * b₃ is isometric

proof end;

theorem Th5: :: VECTMETR:5

for b₁ being non empty MetrStruct holds id b₁ is isometric

proof end;

registration

let c₁ be non empty MetrStruct ;
cluster ISOM a₁ -> non empty ;
coherence

proof end;

end;

definition

attr a₁ is strict;
struct RLSMetrStruct -> RLSStruct , MetrStruct ;
aggr RLSMetrStruct(# carrier, distance, Zero, add, Mult #) -> RLSMetrStruct ;

end;

registration

cluster non empty strict RLSMetrStruct ;
existence

proof end;

end;

registration

let c₁ be non empty set ;
let c₂ be Function of [:c₁,c₁:], REAL ;
let c₃ be Element of c₁;
let c₄ be BinOp of c₁;
let c₅ be Function of [:REAL ,c₁:],c₁;
cluster RLSMetrStruct(# a₁,a₂,a₃,a₄,a₅ #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

definition

let c₁ be non empty RLSMetrStruct ;
attr a₁ is homogeneous means :Def5: :: VECTMETR:def 5
for b₁ being Real
for b₂, b₃ being Element of a₁ holds dist (b₁ * b₂),(b₁ * b₃) = (abs b₁) * (dist b₂,b₃);

end;

:: deftheorem Def5 defines homogeneous VECTMETR:def 5 :

definition

let c₁ be non empty RLSMetrStruct ;
attr a₁ is translatible means :Def6: :: VECTMETR:def 6
for b₁, b₂, b₃ being Element of a₁ holds dist b₃,b₂ = dist (b₃ + b₁),(b₂ + b₁);

end;

:: deftheorem Def6 defines translatible VECTMETR:def 6 :

definition

let c₁ be non empty RLSMetrStruct ;
let c₂ be Element of c₁;
func Norm c₂ -> Real equals :: VECTMETR:def 7
dist (0. a₁),a₂;
coherence ;

end;

:: deftheorem Def7 defines Norm VECTMETR:def 7 :

registration

cluster non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like Reflexive discerning symmetric triangle strict homogeneous translatible RLSMetrStruct ;
existence

proof end;

end;

definition

mode RealLinearMetrSpace is non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like Reflexive discerning symmetric triangle homogeneous translatible RLSMetrStruct ;

end;

theorem Th6: :: VECTMETR:6

for b₁ being non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like homogeneous RLSMetrStruct
for b₂ being Real
for b₃ being Element of b₁ holds Norm (b₂ * b₃) = (abs b₂) * (Norm b₃)

proof end;

theorem Th7: :: VECTMETR:7

for b₁ being non empty Abelian add-associative right_zeroed right_complementable triangle translatible RLSMetrStruct
for b₂, b₃ being Element of b₁ holds Norm (b₂ + b₃) <= (Norm b₂) + (Norm b₃)

proof end;

theorem Th8: :: VECTMETR:8

for b₁ being non empty add-associative right_zeroed right_complementable translatible RLSMetrStruct
for b₂, b₃ being Element of b₁ holds dist b₂,b₃ = Norm (b₃ - b₂)

proof end;

definition

let c₁ be Nat;
func RLMSpace c₁ -> strict RealLinearMetrSpace means :Def8: :: VECTMETR:def 8
( the carrier of a₂ = REAL a₁ & the distance of a₂ = Pitag_dist a₁ & the Zero of a₂ = 0* a₁ & ( for b₁, b₂ being Element of REAL a₁ holds the add of a₂ . b₁,b₂ = b₁ + b₂ ) & ( for b₁ being Element of REAL a₁
for b₂ being Element of REAL holds the Mult of a₂ . b₂,b₁ = b₂ * b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines RLMSpace VECTMETR:def 8 :

theorem Th9: :: VECTMETR:9

for b₁ being Nat
for b₂ being isometric Function of (RLMSpace b₁),(RLMSpace b₁) holds rng b₂ = REAL b₁

proof end;

definition

let c₁ be Nat;
func IsomGroup c₁ -> strict HGrStr means :Def9: :: VECTMETR:def 9
( the carrier of a₂ = ISOM (RLMSpace a₁) & ( for b₁, b₂ being Function st b₁ in ISOM (RLMSpace a₁) & b₂ in ISOM (RLMSpace a₁) holds
the mult of a₂ . b₁,b₂ = b₁ * b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines IsomGroup VECTMETR:def 9 :

registration

let c₁ be Nat;
cluster IsomGroup a₁ -> non empty strict ;
coherence

proof end;

end;

registration

let c₁ be Nat;
cluster IsomGroup a₁ -> non empty strict Group-like associative ;
coherence

proof end;

end;

theorem Th10: :: VECTMETR:10

for b₁ being Nat holds 1. (IsomGroup b₁) = id (RLMSpace b₁)

proof end;

theorem Th11: :: VECTMETR:11

for b₁ being Nat
for b₂ being Element of (IsomGroup b₁)
for b₃ being Function of (RLMSpace b₁),(RLMSpace b₁) st b₂ = b₃ holds
b₂ " = b₃ "

proof end;

definition

let c₁ be Nat;
let c₂ be Subgroup of IsomGroup c₁;
func SubIsomGroupRel c₂ -> Relation of the carrier of (RLMSpace a₁) means :Def10: :: VECTMETR:def 10
for b₁, b₂ being Element of (RLMSpace a₁) holds
( [b₁,b₂] in a₃ iff ex b₃ being Function st
( b₃ in the carrier of a₂ & b₃ . b₁ = b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines SubIsomGroupRel VECTMETR:def 10 :

registration

let c₁ be Nat;
let c₂ be Subgroup of IsomGroup c₁;
cluster SubIsomGroupRel a₂ -> symmetric transitive total ;
coherence

proof end;

end;