reconsider ZS = {0} 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 BINOP_1:sch 4();
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 BINOP_1:sch 4();
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 BINOP_1:sch 4();
A4:
for a being Real
for x being Element of ZS holds G . (a,x) = H2(a,x)
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;
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 #);
(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;
verum
end;
take
RLSMetrStruct(# ZS,FF,O,F,G #)
; ( 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
; ( 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
hence
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, 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 #);
(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;
verum
end;
hence
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 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 #);
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;
verum
end;
hence
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 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 )proof
reconsider y =
O as
VECTOR of
RLSMetrStruct(#
ZS,
FF,
O,
F,
G #) ;
let x be
VECTOR of
RLSMetrStruct(#
ZS,
FF,
O,
F,
G #);
ALGSTR_0:def 16 x is right_complementable
take
y
;
ALGSTR_0:def 11 x + y = 0. RLSMetrStruct(# ZS,FF,O,F,G #)
thus
x + y = 0. RLSMetrStruct(#
ZS,
FF,
O,
F,
G #)
by A2;
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;
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 #);
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;
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;
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 #);
(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;
verum
end;
for x being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds 1 * x = x
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; ( 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 #);
( 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
;
( ( 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;
( 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;
dist (a,c) <= (dist (a,b)) + (dist (b,c))
thus
dist (
a,
c)
<= (dist (a,b)) + (dist (b,c))
by A10, A11, A9;
verum
end;
hence
RLSMetrStruct(# ZS,FF,O,F,G #) is Reflexive
by METRIC_1:1; ( 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 A8, METRIC_1:2; ( 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 A8, METRIC_1:3; ( 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 A8, METRIC_1:4; ( 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;
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 #);
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
;
verum
end;
hence
RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous
; 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 #);
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
;
verum
end;
hence
RLSMetrStruct(# ZS,FF,O,F,G #) is translatible
; verum