reconsider ZS = as non empty set ;
reconsider O = 0 as Element of ZS by TARSKI:def 1;
deffunc H1( Element of ZS, Element of ZS) -> Element of REAL = In (0,REAL);
consider FF being Function of [:ZS,ZS:],REAL such that
A1: for x, y being Element of ZS holds FF . (x,y) = H1(x,y) from deffunc H2( Real, Element of ZS) -> Element of ZS = O;
deffunc H3( Element of ZS, Element of ZS) -> Element of ZS = O;
consider F being BinOp of ZS such that
A2: for x, y being Element of ZS holds F . (x,y) = H3(x,y) from consider G being Function of [:REAL,ZS:],ZS such that
A3: for a being Element of REAL
for x being Element of ZS holds G . (a,x) = H2(a,x) from A4: for a being Real
for x being Element of ZS holds G . (a,x) = H2(a,x)
proof
let a be Real; :: thesis: for x being Element of ZS holds G . (a,x) = H2(a,x)
let x be Element of ZS; :: thesis: G . (a,x) = H2(a,x)
reconsider a = a as Element of REAL by XREAL_0:def 1;
G . (a,x) = H2(a,x) by A3;
hence G . (a,x) = H2(a,x) ; :: thesis: verum
end;
set W = RLSMetrStruct(# ZS,FF,O,F,G #);
A5: for a, b being Real
for x being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds (a + b) * x = (a * x) + (b * x)
proof
let a, b be Real; :: thesis: for x being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds (a + b) * x = (a * x) + (b * x)
reconsider a = a, b = b as Real ;
let x be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); :: thesis: (a + b) * x = (a * x) + (b * x)
set c = a + b;
reconsider X = x as Element of ZS ;
(a + b) * x = H2(a + b,X) by A4;
hence (a + b) * x = (a * x) + (b * x) by A2; :: thesis: verum
end;
take RLSMetrStruct(# ZS,FF,O,F,G #) ; :: thesis: ( RLSMetrStruct(# ZS,FF,O,F,G #) is strict & RLSMetrStruct(# ZS,FF,O,F,G #) is Abelian & RLSMetrStruct(# ZS,FF,O,F,G #) is add-associative & RLSMetrStruct(# ZS,FF,O,F,G #) is right_zeroed & RLSMetrStruct(# ZS,FF,O,F,G #) is right_complementable & RLSMetrStruct(# ZS,FF,O,F,G #) is vector-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-associative & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-unital & RLSMetrStruct(# ZS,FF,O,F,G #) is Reflexive & RLSMetrStruct(# ZS,FF,O,F,G #) is discerning & RLSMetrStruct(# ZS,FF,O,F,G #) is symmetric & RLSMetrStruct(# ZS,FF,O,F,G #) is triangle & RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous & RLSMetrStruct(# ZS,FF,O,F,G #) is translatible )
thus RLSMetrStruct(# ZS,FF,O,F,G #) is strict ; :: thesis: ( RLSMetrStruct(# ZS,FF,O,F,G #) is Abelian & RLSMetrStruct(# ZS,FF,O,F,G #) is add-associative & RLSMetrStruct(# ZS,FF,O,F,G #) is right_zeroed & RLSMetrStruct(# ZS,FF,O,F,G #) is right_complementable & RLSMetrStruct(# ZS,FF,O,F,G #) is vector-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-associative & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-unital & RLSMetrStruct(# ZS,FF,O,F,G #) is Reflexive & RLSMetrStruct(# ZS,FF,O,F,G #) is discerning & RLSMetrStruct(# ZS,FF,O,F,G #) is symmetric & RLSMetrStruct(# ZS,FF,O,F,G #) is triangle & RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous & RLSMetrStruct(# ZS,FF,O,F,G #) is translatible )
for x, y being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds x + y = y + x
proof
let x, y be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); :: thesis: x + y = y + x
reconsider X = x, Y = y as Element of ZS ;
x + y = H3(X,Y) by A2;
hence x + y = y + x by A2; :: thesis: verum
end;
hence RLSMetrStruct(# ZS,FF,O,F,G #) is Abelian ; :: thesis: ( RLSMetrStruct(# ZS,FF,O,F,G #) is add-associative & RLSMetrStruct(# ZS,FF,O,F,G #) is right_zeroed & RLSMetrStruct(# ZS,FF,O,F,G #) is right_complementable & RLSMetrStruct(# ZS,FF,O,F,G #) is vector-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-associative & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-unital & RLSMetrStruct(# ZS,FF,O,F,G #) is Reflexive & RLSMetrStruct(# ZS,FF,O,F,G #) is discerning & RLSMetrStruct(# ZS,FF,O,F,G #) is symmetric & RLSMetrStruct(# ZS,FF,O,F,G #) is triangle & RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous & RLSMetrStruct(# ZS,FF,O,F,G #) is translatible )
for x, y, z being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds (x + y) + z = x + (y + z)
proof
let x, y, z be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); :: thesis: (x + y) + z = x + (y + z)
reconsider X = x, Y = y, Z = z as Element of ZS ;
(x + y) + z = H3(H3(X,Y),Z) by A2;
hence (x + y) + z = x + (y + z) by A2; :: thesis: verum
end;
hence RLSMetrStruct(# ZS,FF,O,F,G #) is add-associative ; :: thesis: ( RLSMetrStruct(# ZS,FF,O,F,G #) is right_zeroed & RLSMetrStruct(# ZS,FF,O,F,G #) is right_complementable & RLSMetrStruct(# ZS,FF,O,F,G #) is vector-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-associative & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-unital & RLSMetrStruct(# ZS,FF,O,F,G #) is Reflexive & RLSMetrStruct(# ZS,FF,O,F,G #) is discerning & RLSMetrStruct(# ZS,FF,O,F,G #) is symmetric & RLSMetrStruct(# ZS,FF,O,F,G #) is triangle & RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous & RLSMetrStruct(# ZS,FF,O,F,G #) is translatible )
for x being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds x + (0. RLSMetrStruct(# ZS,FF,O,F,G #)) = x
proof
let x be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); :: thesis: x + (0. RLSMetrStruct(# ZS,FF,O,F,G #)) = x
reconsider X = x as Element of ZS ;
x + (0. RLSMetrStruct(# ZS,FF,O,F,G #)) = H3(X,O) by A2;
hence x + (0. RLSMetrStruct(# ZS,FF,O,F,G #)) = x by TARSKI:def 1; :: thesis: verum
end;
hence RLSMetrStruct(# ZS,FF,O,F,G #) is right_zeroed ; :: thesis: ( RLSMetrStruct(# ZS,FF,O,F,G #) is right_complementable & RLSMetrStruct(# ZS,FF,O,F,G #) is vector-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-associative & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-unital & RLSMetrStruct(# ZS,FF,O,F,G #) is Reflexive & RLSMetrStruct(# ZS,FF,O,F,G #) is discerning & RLSMetrStruct(# ZS,FF,O,F,G #) is symmetric & RLSMetrStruct(# ZS,FF,O,F,G #) is triangle & RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous & RLSMetrStruct(# ZS,FF,O,F,G #) is translatible )
thus RLSMetrStruct(# ZS,FF,O,F,G #) is right_complementable :: thesis: ( RLSMetrStruct(# ZS,FF,O,F,G #) is vector-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-associative & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-unital & RLSMetrStruct(# ZS,FF,O,F,G #) is Reflexive & RLSMetrStruct(# ZS,FF,O,F,G #) is discerning & RLSMetrStruct(# ZS,FF,O,F,G #) is symmetric & RLSMetrStruct(# ZS,FF,O,F,G #) is triangle & RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous & RLSMetrStruct(# ZS,FF,O,F,G #) is translatible )
proof
reconsider y = O as VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) ;
let x be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); :: according to ALGSTR_0:def 16 :: thesis:
take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. RLSMetrStruct(# ZS,FF,O,F,G #)
thus x + y = 0. RLSMetrStruct(# ZS,FF,O,F,G #) by A2; :: thesis: verum
end;
A6: for a being Real
for x, y being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds a * (x + y) = (a * x) + (a * y)
proof
let a be Real; :: thesis: for x, y being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds a * (x + y) = (a * x) + (a * y)
reconsider a = a as Real ;
let x, y be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); :: thesis: a * (x + y) = (a * x) + (a * y)
reconsider X = x, Y = y as Element of ZS ;
(a * x) + (a * y) = H3(H2(a,X),H2(a,Y)) by A2;
hence a * (x + y) = (a * x) + (a * y) by A4; :: thesis: verum
end;
A7: for a, b being Real
for x being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds (a * b) * x = a * (b * x)
proof
let a, b be Real; :: thesis: for x being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds (a * b) * x = a * (b * x)
reconsider a = a, b = b as Real ;
let x be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); :: thesis: (a * b) * x = a * (b * x)
set c = a * b;
reconsider X = x as Element of ZS ;
(a * b) * x = H2(a * b,X) by A4;
hence (a * b) * x = a * (b * x) by A4; :: thesis: verum
end;
for x being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds 1 * x = x
proof
reconsider A9 = 1 as Element of REAL by XREAL_0:def 1;
let x be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); :: thesis: 1 * x = x
reconsider X = x as Element of ZS ;
1 * x = H2(A9,X) by A4;
hence 1 * x = x by TARSKI:def 1; :: thesis: verum
end;
hence ( RLSMetrStruct(# ZS,FF,O,F,G #) is vector-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-associative & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-unital ) by A6, A5, A7; :: thesis: ( RLSMetrStruct(# ZS,FF,O,F,G #) is Reflexive & RLSMetrStruct(# ZS,FF,O,F,G #) is discerning & RLSMetrStruct(# ZS,FF,O,F,G #) is symmetric & RLSMetrStruct(# ZS,FF,O,F,G #) is triangle & RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous & RLSMetrStruct(# ZS,FF,O,F,G #) is translatible )
A8: for a, b, c being Point of RLSMetrStruct(# ZS,FF,O,F,G #) holds
( dist (a,a) = 0 & ( dist (a,b) = 0 implies a = b ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
proof
let a, b, c be Point of RLSMetrStruct(# ZS,FF,O,F,G #); :: thesis: ( dist (a,a) = 0 & ( dist (a,b) = 0 implies a = b ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
A9: dist (a,a) = FF . (a,a) by METRIC_1:def 1
.= 0 by A1 ;
hence dist (a,a) = 0 ; :: thesis: ( ( dist (a,b) = 0 implies a = b ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
A10: a = 0 by TARSKI:def 1;
hence ( dist (a,b) = 0 implies a = b ) by TARSKI:def 1; :: thesis: ( dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
A11: b = 0 by TARSKI:def 1;
hence dist (a,b) = dist (b,a) by A10; :: thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c))
thus dist (a,c) <= (dist (a,b)) + (dist (b,c)) by A10, A11, A9; :: thesis: verum
end;
hence RLSMetrStruct(# ZS,FF,O,F,G #) is Reflexive by METRIC_1:1; :: thesis: ( RLSMetrStruct(# ZS,FF,O,F,G #) is discerning & RLSMetrStruct(# ZS,FF,O,F,G #) is symmetric & RLSMetrStruct(# ZS,FF,O,F,G #) is triangle & RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous & RLSMetrStruct(# ZS,FF,O,F,G #) is translatible )
thus RLSMetrStruct(# ZS,FF,O,F,G #) is discerning by ; :: thesis: ( RLSMetrStruct(# ZS,FF,O,F,G #) is symmetric & RLSMetrStruct(# ZS,FF,O,F,G #) is triangle & RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous & RLSMetrStruct(# ZS,FF,O,F,G #) is translatible )
thus RLSMetrStruct(# ZS,FF,O,F,G #) is symmetric by ; :: thesis: ( RLSMetrStruct(# ZS,FF,O,F,G #) is triangle & RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous & RLSMetrStruct(# ZS,FF,O,F,G #) is translatible )
thus RLSMetrStruct(# ZS,FF,O,F,G #) is triangle by ; :: thesis: ( RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous & RLSMetrStruct(# ZS,FF,O,F,G #) is translatible )
for r being Real
for v, w being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds dist ((r * v),(r * w)) = |.r.| * (dist (v,w))
proof
let r be Real; :: thesis: for v, w being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds dist ((r * v),(r * w)) = |.r.| * (dist (v,w))
let v, w be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); :: thesis: dist ((r * v),(r * w)) = |.r.| * (dist (v,w))
reconsider v1 = v, w1 = w as Element of ZS ;
A12: FF . (v1,w1) = H1(v1,w1) by A1;
thus dist ((r * v),(r * w)) = FF . ((r * v),(r * w)) by METRIC_1:def 1
.= |.r.| * 0 by A1
.= |.r.| * H1(v1,w1)
.= |.r.| * (FF . (v1,w1)) by A12
.= |.r.| * (dist (v,w)) by METRIC_1:def 1 ; :: thesis: verum
end;
hence RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous ; :: thesis: RLSMetrStruct(# ZS,FF,O,F,G #) is translatible
for u, w, v being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds dist (v,w) = dist ((v + u),(w + u))
proof
let u, w, v be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); :: thesis: dist (v,w) = dist ((v + u),(w + u))
thus dist ((v + u),(w + u)) = FF . ((v + u),(w + u)) by METRIC_1:def 1
.= 0 by A1
.= FF . (v,w) by A1
.= dist (v,w) by METRIC_1:def 1 ; :: thesis: verum
end;
hence RLSMetrStruct(# ZS,FF,O,F,G #) is translatible ; :: thesis: verum