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 #);
A3:
now 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:29
.=
f . u,
(v1 + w1)
by A1
.=
u + (v + w)
by A1
;
verum end;
A5:
now let 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 |-> 0 )
by A1
.=
v
by RVSUM_1:33
;
verum end;
A6:
now 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) = (abs 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) = (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
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 ;
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
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:58
;
verum
end;
A12:
now hereby ( ( for a1, b1 being real number
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 number
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 number ;
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 by XREAL_0:def 1;
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 A2
.=
(a * v1) + (a * w1)
by RVSUM_1:73
.=
f . (a * v1),
(a * w1)
by A1
.=
f . (g . a,v),
(a * w1)
by A2
.=
(a * v) + (a * w)
by A2
;
hence
a1 * (v + w) = (a1 * v) + (a1 * w)
;
verum
end; hereby ( ( for a1, b1 being real number
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 number ;
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 by XREAL_0:def 1;
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 A2
.=
(a * v1) + (b * v1)
by RVSUM_1:72
.=
f . (a * v1),
(b * v1)
by A1
.=
f . (g . a,v),
(b * v1)
by A2
.=
(a * v) + (b * v)
by A2
;
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 number ;
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 by XREAL_0:def 1;
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 A2
.=
a * (b * v1)
by RVSUM_1:71
.=
g . a,
(b * v1)
by A2
.=
a * (b * v)
by A2
;
hence
(a1 * b1) * v = a1 * (b1 * v)
;
verum
end;
A13:
now 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) )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