deffunc H1( Element of 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 #);
A6:
now let r be
Real;
for v, w being VECTOR of holds dist (r * v),(r * w) = (abs r) * (dist v,w)let v,
w be
VECTOR of ;
dist (r * v),(r * w) = (abs 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 ;
A7:
dist v,
w =
(Pitag_dist n) . v,
w
by METRIC_1:def 1
.=
|.(v1 - w1).|
by EUCLID:def 6
;
A8:
(
r * v = r * v1 &
r * w = r * w1 )
by A2;
thus dist (r * v),
(r * w) =
(Pitag_dist n) . (r * v),
(r * w)
by METRIC_1:def 1
.=
|.((r * v2) - (r * w2)).|
by A8, EUCLID:def 6
.=
|.((r * v2) + (((- 1) * r) * w2)).|
by RVSUM_1:71
.=
|.((r * v2) + (r * (- w2))).|
by RVSUM_1:71
.=
|.(r * (v1 - w1)).|
by RVSUM_1:73
.=
(abs r) * (dist v,w)
by A7, EUCLID:14
;
verum end;
A9:
now let u,
w,
v be
VECTOR of ;
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 ;
A10:
(
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:63
.=
|.((v2 + u2) - (u2 + w2)).|
by RVSUM_1:60
.=
(Pitag_dist n) . (v1 + u1),
(w1 + u1)
by EUCLID:def 6
.=
dist (v + u),
(w + u)
by A10, METRIC_1:def 1
;
verum end;
A11:
RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) is right_complementable
A12:
now hereby ( ( for a1, b1 being real number
for v being VECTOR of holds (a1 * b1) * v = a1 * (b1 * v) ) & ( for v being VECTOR of holds 1 * v = v ) )
end; hereby for v being VECTOR of holds 1 * v = v
end;
A13:
now let a,
b,
c be
VECTOR of ;
( ( 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) )A14:
dist a,
c =
(Pitag_dist n) . a,
c
by METRIC_1:def 1
.=
|.(a1 - c1).|
by EUCLID:def 6
;
|.(a1 - a1).| = 0
by EUCLID:19;
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:21
.=
(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)A15:
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 A14, A15, EUCLID:22;
verum end;
reconsider RLSMS = RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) as non empty right_complementable Abelian add-associative right_zeroed RealLinearSpace-like strict RLSMetrStruct by A4, A3, A5, A11, A12, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 9;
reconsider RLSMS = RLSMS as strict RealLinearMetrSpace by A13, A6, A9, 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, A2; verum