deffunc H1( Real, Element of REAL n) -> Element of REAL n = $1 * $2;
deffunc H2( Element of REAL n, Element of REAL n) -> Element of REAL n = $1 + $2;
consider f being BinOp of (REAL n) such that
A1:
for x, y being Element of REAL n holds f . (x,y) = H2(x,y)
from BINOP_1:sch 4();
consider g being Function of [:REAL,(REAL n):],(REAL n) such that
A2:
for r being Element of REAL
for x being Element of REAL n holds g . (r,x) = H1(r,x)
from BINOP_1:sch 4();
set RLSMS = RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #);
A3:
for r being Real
for x being Element of REAL n holds g . (r,x) = H1(r,x)
A4:
now for u, v, w being Element of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds (u + v) + w = u + (v + w)let u,
v,
w be
Element of
RLSMetrStruct(#
(REAL n),
(Pitag_dist n),
(0* n),
f,
g #);
(u + v) + w = u + (v + w)reconsider u1 =
u,
v1 =
v,
w1 =
w as
Element of
REAL n ;
thus (u + v) + w =
f . (
(u1 + v1),
w)
by A1
.=
(u1 + v1) + w1
by A1
.=
u1 + (v1 + w1)
by FINSEQOP:28
.=
f . (
u,
(v1 + w1))
by A1
.=
u + (v + w)
by A1
;
verum end;
A6:
now for v being Element of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds v + (0. RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #)) = vlet v be
Element of
RLSMetrStruct(#
(REAL n),
(Pitag_dist n),
(0* n),
f,
g #);
v + (0. RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #)) = vreconsider v1 =
v as
Element of
n -tuples_on REAL ;
thus v + (0. RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #)) =
v1 + (n |-> (In (0,REAL)))
by A1
.=
v
by RVSUM_1:16
;
verum end;
A7:
now for r being Real
for v, w being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds dist ((r * v),(r * w)) = |.r.| * (dist (v,w))let r be
Real;
for v, w being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds dist ((r * v),(r * w)) = |.r.| * (dist (v,w))let v,
w be
VECTOR of
RLSMetrStruct(#
(REAL n),
(Pitag_dist n),
(0* n),
f,
g #);
dist ((r * v),(r * w)) = |.r.| * (dist (v,w))reconsider v1 =
v,
w1 =
w as
Element of
REAL n ;
reconsider v2 =
v1,
w2 =
w1 as
Element of
n -tuples_on REAL ;
A8:
dist (
v,
w) =
(Pitag_dist n) . (
v,
w)
by METRIC_1:def 1
.=
|.(v1 - w1).|
by EUCLID:def 6
;
A9:
(
r * v = r * v1 &
r * w = r * w1 )
by A3;
thus dist (
(r * v),
(r * w)) =
(Pitag_dist n) . (
(r * v),
(r * w))
by METRIC_1:def 1
.=
|.((r * v2) - (r * w2)).|
by A9, EUCLID:def 6
.=
|.((r * v2) + (((- 1) * r) * w2)).|
by RVSUM_1:49
.=
|.((r * v2) + (r * (- w2))).|
by RVSUM_1:49
.=
|.(r * (v1 - w1)).|
by RVSUM_1:51
.=
|.r.| * (dist (v,w))
by A8, EUCLID:11
;
verum end;
A10:
now for u, w, v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds dist (v,w) = dist ((v + u),(w + u))let u,
w,
v be
VECTOR of
RLSMetrStruct(#
(REAL n),
(Pitag_dist n),
(0* n),
f,
g #);
dist (v,w) = dist ((v + u),(w + u))reconsider u1 =
u,
w1 =
w,
v1 =
v as
Element of
REAL n ;
reconsider u2 =
u1,
w2 =
w1,
v2 =
v1 as
Element of
n -tuples_on REAL ;
A11:
(
v + u = v1 + u1 &
w + u = w1 + u1 )
by A1;
thus dist (
v,
w) =
(Pitag_dist n) . (
v,
w)
by METRIC_1:def 1
.=
|.(v1 - w1).|
by EUCLID:def 6
.=
|.(((v2 + u2) - u2) - w2).|
by RVSUM_1:42
.=
|.((v2 + u2) - (u2 + w2)).|
by RVSUM_1:39
.=
(Pitag_dist n) . (
(v1 + u1),
(w1 + u1))
by EUCLID:def 6
.=
dist (
(v + u),
(w + u))
by A11, METRIC_1:def 1
;
verum end;
A12:
RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) is right_complementable
proof
let v be
Element of
RLSMetrStruct(#
(REAL n),
(Pitag_dist n),
(0* n),
f,
g #);
ALGSTR_0:def 16 v is right_complementable
reconsider v1 =
v as
Element of
n -tuples_on REAL ;
reconsider w =
- v1 as
Element of
RLSMetrStruct(#
(REAL n),
(Pitag_dist n),
(0* n),
f,
g #) ;
take
w
;
ALGSTR_0:def 11 v + w = 0. RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #)
thus v + w =
v1 - v1
by A1
.=
0. RLSMetrStruct(#
(REAL n),
(Pitag_dist n),
(0* n),
f,
g #)
by RVSUM_1:37
;
verum
end;
A13:
now ( ( for a1 being Real
for v, w being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds a1 * (v + w) = (a1 * v) + (a1 * w) ) & ( for a1, b1 being Real
for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds (a1 + b1) * v = (a1 * v) + (b1 * v) ) & ( for a1, b1 being Real
for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds (a1 * b1) * v = a1 * (b1 * v) ) & ( for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds 1 * v = v ) )hereby ( ( for a1, b1 being Real
for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds (a1 + b1) * v = (a1 * v) + (b1 * v) ) & ( for a1, b1 being Real
for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds (a1 * b1) * v = a1 * (b1 * v) ) & ( for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds 1 * v = v ) )
let a1 be
Real;
for v, w being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds a1 * (v + w) = (a1 * v) + (a1 * w)let v,
w be
VECTOR of
RLSMetrStruct(#
(REAL n),
(Pitag_dist n),
(0* n),
f,
g #);
a1 * (v + w) = (a1 * v) + (a1 * w)reconsider a =
a1 as
Real ;
reconsider v1 =
v,
w1 =
w as
Element of
REAL n ;
reconsider v2 =
v1,
w2 =
w1 as
Element of
n -tuples_on REAL ;
a * (v + w) =
g . (
a,
(v1 + w1))
by A1
.=
a * (v2 + w2)
by A3
.=
(a * v1) + (a * w1)
by RVSUM_1:51
.=
f . (
(a * v1),
(a * w1))
by A1
.=
f . (
(g . (a,v)),
(a * w1))
by A3
.=
(a * v) + (a * w)
by A3
;
hence
a1 * (v + w) = (a1 * v) + (a1 * w)
;
verum
end; hereby ( ( for a1, b1 being Real
for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds (a1 * b1) * v = a1 * (b1 * v) ) & ( for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds 1 * v = v ) )
let a1,
b1 be
Real;
for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds (a1 + b1) * v = (a1 * v) + (b1 * v)let v be
VECTOR of
RLSMetrStruct(#
(REAL n),
(Pitag_dist n),
(0* n),
f,
g #);
(a1 + b1) * v = (a1 * v) + (b1 * v)reconsider a =
a1,
b =
b1 as
Real ;
reconsider v1 =
v as
Element of
REAL n ;
reconsider v2 =
v1 as
Element of
n -tuples_on REAL ;
(a + b) * v =
(a + b) * v2
by A3
.=
(a * v1) + (b * v1)
by RVSUM_1:50
.=
f . (
(a * v1),
(b * v1))
by A1
.=
f . (
(g . (a,v)),
(b * v1))
by A3
.=
(a * v) + (b * v)
by A3
;
hence
(a1 + b1) * v = (a1 * v) + (b1 * v)
;
verum
end; hereby for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds 1 * v = v
let a1,
b1 be
Real;
for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds (a1 * b1) * v = a1 * (b1 * v)let v be
VECTOR of
RLSMetrStruct(#
(REAL n),
(Pitag_dist n),
(0* n),
f,
g #);
(a1 * b1) * v = a1 * (b1 * v)reconsider a =
a1,
b =
b1 as
Real ;
reconsider v1 =
v as
Element of
REAL n ;
reconsider v2 =
v1 as
Element of
n -tuples_on REAL ;
(a * b) * v =
(a * b) * v2
by A3
.=
a * (b * v1)
by RVSUM_1:49
.=
g . (
a,
(b * v1))
by A3
.=
a * (b * v)
by A3
;
hence
(a1 * b1) * v = a1 * (b1 * v)
;
verum
end; end;
A14:
now for a, b, c being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds
( ( dist (a,b) = 0 implies a = b ) & dist (a,a) = 0 & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )let a,
b,
c be
VECTOR of
RLSMetrStruct(#
(REAL n),
(Pitag_dist n),
(0* n),
f,
g #);
( ( dist (a,b) = 0 implies a = b ) & dist (a,a) = 0 & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )reconsider a1 =
a,
b1 =
b,
c1 =
c as
Element of
REAL n ;
thus
(
dist (
a,
b)
= 0 implies
a = b )
( dist (a,a) = 0 & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )A15:
dist (
a,
c) =
(Pitag_dist n) . (
a,
c)
by METRIC_1:def 1
.=
|.(a1 - c1).|
by EUCLID:def 6
;
|.(a1 - a1).| = 0
;
then
(Pitag_dist n) . (
a,
a)
= 0
by EUCLID:def 6;
hence
dist (
a,
a)
= 0
by METRIC_1:def 1;
( dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )thus dist (
a,
b) =
(Pitag_dist n) . (
a,
b)
by METRIC_1:def 1
.=
|.(a1 - b1).|
by EUCLID:def 6
.=
|.(b1 - a1).|
by EUCLID:18
.=
(Pitag_dist n) . (
b,
a)
by EUCLID:def 6
.=
dist (
b,
a)
by METRIC_1:def 1
;
dist (a,c) <= (dist (a,b)) + (dist (b,c))A16:
dist (
b,
c) =
(Pitag_dist n) . (
b,
c)
by METRIC_1:def 1
.=
|.(b1 - c1).|
by EUCLID:def 6
;
dist (
a,
b) =
(Pitag_dist n) . (
a,
b)
by METRIC_1:def 1
.=
|.(a1 - b1).|
by EUCLID:def 6
;
hence
dist (
a,
c)
<= (dist (a,b)) + (dist (b,c))
by A15, A16, EUCLID:19;
verum end;
reconsider RLSMS = RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) as non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RLSMetrStruct by A5, A4, A6, A12, A13, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 8;
reconsider RLSMS = RLSMS as strict RealLinearMetrSpace by A14, A7, A10, Def5, Def6, METRIC_1:1, METRIC_1:2, METRIC_1:3, METRIC_1:4;
take
RLSMS
; ( the carrier of RLSMS = REAL n & the distance of RLSMS = Pitag_dist n & 0. RLSMS = 0* n & ( for x, y being Element of REAL n holds the addF of RLSMS . (x,y) = x + y ) & ( for x being Element of REAL n
for r being Element of REAL holds the Mult of RLSMS . (r,x) = r * x ) )
thus
( the carrier of RLSMS = REAL n & the distance of RLSMS = Pitag_dist n & 0. RLSMS = 0* n & ( for x, y being Element of REAL n holds the addF of RLSMS . (x,y) = x + y ) & ( for x being Element of REAL n
for r being Element of REAL holds the Mult of RLSMS . (r,x) = r * x ) )
by A1, A3; verum