thus LinearTopSpaceNorm X is add-continuous :: thesis:

proof

let x1, x2 be Point of (LinearTopSpaceNorm X); :: according to RLTOPSP1:def 8 :: thesis:
reconsider z2 = x2 as Element of (MetricSpaceNorm X) by Def4;
reconsider z1 = x1 as Element of (MetricSpaceNorm X) by Def4;
reconsider z12 = x1 + x2 as Element of (MetricSpaceNorm X) by Def4;
let V be Subset of (LinearTopSpaceNorm X); :: thesis:
assume that
A1: V is open and
A2: x1 + x2 in V ; :: thesis:
V in the topology of (LinearTopSpaceNorm X) by A1;
then V in the topology of (TopSpaceNorm X) by Def4;
then consider r being Real such that
A3: r > 0 and
A4: Ball (z12,r) c= V by A2, PCOMPS_1:def 4;
set r2 = r / 2;
A5: 0 < r / 2 by A3, XREAL_1:215;
reconsider V1 = Ball (z1,(r / 2)), V2 = Ball (z2,(r / 2)) as Subset of (LinearTopSpaceNorm X) by Def4;
A6: V1 + V2 c= V

proof

let w be object ; :: according to TARSKI:def 3 :: thesis:
assume w in V1 + V2 ; :: thesis:
then consider v, u being VECTOR of (LinearTopSpaceNorm X) such that
A7: w = v + u and
A8: ( v in V1 & u in V2 ) ;
reconsider v1 = v, u1 = u as Element of (MetricSpaceNorm X) by Def4;
reconsider w1 = w as Element of (MetricSpaceNorm X) by A7, Def4;
reconsider zz12 = x1 + x2, zz1 = x1, zz2 = x2, vv1 = v, uu1 = u as Point of X by Def4;
A9: ( ||.((zz1 - vv1) + (zz2 - uu1)).|| <= ||.(zz1 - vv1).|| + ||.(zz2 - uu1).|| & ||.(zz1 - vv1).|| = dist (z1,v1) ) by Def1, NORMSP_1:def 1;
( dist (z1,v1) < r / 2 & dist (z2,u1) < r / 2 ) by A8, METRIC_1:11;
then A10: (dist (z1,v1)) + (dist (z2,u1)) < (r / 2) + (r / 2) by XREAL_1:8;
reconsider ww1 = w as Point of X by A7, Def4;
A11: ||.(zz2 - uu1).|| = dist (z2,u1) by Def1;
dist (z12,w1) = ||.(zz12 - ww1).|| by Def1
.= ||.((zz1 + zz2) - ww1).|| by Def4
.= ||.((zz1 + zz2) - (vv1 + uu1)).|| by A7, Def4
.= ||.((zz1 + zz2) + ((- uu1) + (- vv1))).|| by RLVECT_1:31
.= ||.(((zz1 + zz2) + (- vv1)) + (- uu1)).|| by RLVECT_1:def 3
.= ||.(((zz1 + (- vv1)) + zz2) + (- uu1)).|| by RLVECT_1:def 3
.= ||.((zz1 + (- vv1)) + (zz2 + (- uu1))).|| by RLVECT_1:def 3 ;
then dist (z12,w1) < r by A9, A11, A10, XXREAL_0:2;
then w1 in Ball (z12,r) by METRIC_1:11;
hence w in V by A4; :: thesis:

end;

dist (z2,z2) = 0 by METRIC_1:1;
then A12: x2 in V2 by A5, METRIC_1:11;
Ball (z2,(r / 2)) in the topology of (TopSpaceNorm X) by PCOMPS_1:29;
then Ball (z2,(r / 2)) in the topology of (LinearTopSpaceNorm X) by Def4;
then A13: V2 is open ;
Ball (z1,(r / 2)) in the topology of (TopSpaceNorm X) by PCOMPS_1:29;
then Ball (z1,(r / 2)) in the topology of (LinearTopSpaceNorm X) by Def4;
then A14: V1 is open ;
dist (z1,z1) = 0 by METRIC_1:1;
then x1 in V1 by A5, METRIC_1:11;
hence ex b₁, b₂ being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b₁ is open & b₂ is open & x1 in b₁ & x2 in b₂ & b₁ + b₂ c= V ) by A14, A13, A12, A6; :: thesis:

end;

A15: now :: thesis:

let a, b be Real; :: thesis:
let v be VECTOR of (LinearTopSpaceNorm X); :: thesis:
reconsider v1 = v as VECTOR of X by Def4;
( a * v = a * v1 & b * v = b * v1 ) by Def4;
then A16: (a * v1) + (b * v1) = (a * v) + (b * v) by Def4;
(a + b) * v = (a + b) * v1 by Def4;
hence (a + b) * v = (a * v) + (b * v) by A16, RLVECT_1:def 6; :: thesis:

end;

thus LinearTopSpaceNorm X is Mult-continuous :: thesis:

proof

let a be Real; :: according to RLTOPSP1:def 9 :: thesis:
let x be Point of (LinearTopSpaceNorm X); :: thesis:
let V be Subset of (LinearTopSpaceNorm X); :: thesis:
assume that
A17: V is open and
A18: a * x in V ; :: thesis:
reconsider z = x, az = a * x as Element of (MetricSpaceNorm X) by Def4;
V in the topology of (LinearTopSpaceNorm X) by A17;
then V in the topology of (TopSpaceNorm X) by Def4;
then consider r0 being Real such that
A19: r0 > 0 and
A20: Ball (az,r0) c= V by A18, PCOMPS_1:def 4;
set r = r0 / 2;
r0 / 2 > 0 by A19, XREAL_1:215;
then A21: 0 < (r0 / 2) / 2 by XREAL_1:215;
reconsider z1 = z as Point of X ;
set r2 = min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1);
reconsider W = Ball (z,(min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1))) as Subset of (LinearTopSpaceNorm X) by Def4;
A22: r0 / 2 < r0 / 1 by A19, XREAL_1:76;
A23: for s being Real st |.(s - a).| < min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1) holds
s * W c= V

proof

let s be Real; :: thesis:
assume |.(s - a).| < min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1) ; :: thesis:
then A24: |.(a - s).| <= min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1) by COMPLEX1:60;
thus s * W c= V :: thesis:

proof

let w be object ; :: according to TARSKI:def 3 :: thesis:
assume w in s * W ; :: thesis:
then consider v being VECTOR of (LinearTopSpaceNorm X) such that
A25: w = s * v and
A26: v in W ;
reconsider v1 = v as Element of (MetricSpaceNorm X) by Def4;
A27: dist (z,v1) < min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1) by A26, METRIC_1:11;
reconsider w1 = w as Element of (MetricSpaceNorm X) by A25, Def4;
reconsider zza = a * x, zz = x, vv1 = v as Point of X by Def4;
A28: ||.(zz - vv1).|| = dist (z,v1) by Def1;
min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1) <= 1 by XXREAL_0:17;
then ||.(zz - vv1).|| <= 1 by A28, A27, XXREAL_0:2;
then ||.(vv1 - zz).|| <= 1 by NORMSP_1:7;
then A29: ||.zz.|| + ||.(vv1 - zz).|| <= ||.zz.|| + 1 by XREAL_1:6;
zz + (vv1 - zz) = vv1 - (zz - zz) by RLVECT_1:29
.= vv1 - (0. X) by RLVECT_1:15
.= vv1 by RLVECT_1:13 ;
then ||.vv1.|| <= ||.zz.|| + ||.(vv1 - zz).|| by NORMSP_1:def 1;
then A30: ||.vv1.|| <= ||.zz.|| + 1 by A29, XXREAL_0:2;
A31: 0 <= 1 + ||.z1.|| by NORMSP_1:4, XREAL_1:39;
then A32: (min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1)) * (||.zz.|| + 1) <= (((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)) * (||.zz.|| + 1) by XREAL_1:64, XXREAL_0:17;
( 0 <= |.(a - s).| & 0 <= ||.vv1.|| ) by COMPLEX1:46, NORMSP_1:4;
then |.(a - s).| * ||.vv1.|| <= (min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1)) * (||.zz.|| + 1) by A24, A30, XREAL_1:66;
then |.(a - s).| * ||.vv1.|| <= (((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)) * (||.z1.|| + 1) by A32, XXREAL_0:2;
then A33: |.(a - s).| * ||.vv1.|| <= ((||.z1.|| + 1) / ((1 + ||.z1.||) + |.a.|)) * ((r0 / 2) / 2) by XCMPLX_1:75;
0 <= |.a.| by COMPLEX1:46;
then 0 + (1 + ||.z1.||) <= |.a.| + (1 + ||.z1.||) by XREAL_1:6;
then (||.z1.|| + 1) / ((1 + ||.z1.||) + |.a.|) <= 1 by A31, XREAL_1:183;
then ((||.z1.|| + 1) / ((1 + ||.z1.||) + |.a.|)) * ((r0 / 2) / 2) <= 1 * ((r0 / 2) / 2) by A19, XREAL_1:64;
then A34: |.(a - s).| * ||.vv1.|| <= (r0 / 2) / 2 by A33, XXREAL_0:2;
reconsider ww1 = w as Point of X by A25, Def4;
(a * (zz - vv1)) - ((s - a) * vv1) = ((a * zz) - (a * vv1)) - ((s - a) * vv1) by RLVECT_1:34
.= ((a * zz) - (a * vv1)) - ((s * vv1) - (a * vv1)) by RLVECT_1:35
.= (a * zz) - (((s * vv1) - (a * vv1)) + (a * vv1)) by RLVECT_1:27
.= (a * zz) - ((s * vv1) - ((a * vv1) - (a * vv1))) by RLVECT_1:29
.= (a * zz) - ((s * vv1) - (0. X)) by RLVECT_1:15
.= (a * zz) - (s * vv1) by RLVECT_1:13 ;
then ||.((a * zz) - (s * vv1)).|| <= ||.(a * (zz - vv1)).|| + ||.((s - a) * vv1).|| by NORMSP_1:3;
then ||.((a * zz) - (s * vv1)).|| <= (|.a.| * ||.(zz - vv1).||) + ||.((s - a) * vv1).|| by NORMSP_1:def 1;
then ||.((a * zz) - (s * vv1)).|| <= (|.a.| * ||.(zz - vv1).||) + (|.(s - a).| * ||.vv1.||) by NORMSP_1:def 1;
then A35: ||.((a * zz) - (s * vv1)).|| <= (|.a.| * ||.(zz - vv1).||) + (|.(a - s).| * ||.vv1.||) by COMPLEX1:60;
A36: 0 <= |.a.| by COMPLEX1:46;
then A37: (min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1)) * |.a.| <= (((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)) * |.a.| by XREAL_1:64, XXREAL_0:17;
0 <= 1 + ||.z1.|| by NORMSP_1:4, XREAL_1:39;
then 0 + |.a.| <= (1 + ||.z1.||) + |.a.| by XREAL_1:6;
then |.a.| / ((1 + ||.z1.||) + |.a.|) <= 1 by A36, XREAL_1:183;
then A38: (|.a.| / ((1 + ||.z1.||) + |.a.|)) * ((r0 / 2) / 2) <= 1 * ((r0 / 2) / 2) by A19, XREAL_1:64;
||.(zz - vv1).|| * |.a.| <= (min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1)) * |.a.| by A28, A27, A36, XREAL_1:64;
then |.a.| * ||.(zz - vv1).|| <= |.a.| * (((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)) by A37, XXREAL_0:2;
then |.a.| * ||.(zz - vv1).|| <= (|.a.| / ((1 + ||.z1.||) + |.a.|)) * ((r0 / 2) / 2) by XCMPLX_1:75;
then |.a.| * ||.(zz - vv1).|| <= (r0 / 2) / 2 by A38, XXREAL_0:2;
then A39: (|.a.| * ||.(zz - vv1).||) + (|.(a - s).| * ||.vv1.||) <= ((r0 / 2) / 2) + ((r0 / 2) / 2) by A34, XREAL_1:7;
dist (az,w1) = ||.(zza - ww1).|| by Def1
.= ||.((a * zz) - ww1).|| by Def4
.= ||.((a * zz) - (s * vv1)).|| by A25, Def4 ;
then dist (az,w1) <= r0 / 2 by A35, A39, XXREAL_0:2;
then dist (az,w1) < r0 by A22, XXREAL_0:2;
then w1 in Ball (az,r0) by METRIC_1:11;
hence w in V by A20; :: thesis:

end;

( 0 <= ||.z1.|| & 0 <= |.a.| ) by COMPLEX1:46, NORMSP_1:4;
then 0 / ((1 + ||.z1.||) + |.a.|) < ((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|) by A21, XREAL_1:74;
then A40: 0 < min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1) by XXREAL_0:15;
Ball (z,(min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1))) in the topology of (TopSpaceNorm X) by PCOMPS_1:29;
then Ball (z,(min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1))) in the topology of (LinearTopSpaceNorm X) by Def4;
then A41: W is open ;
dist (z,z) = 0 by METRIC_1:1;
then x in W by A40, METRIC_1:11;
hence ex b₁ being object ex b₂ being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b₂ is open & x in b₂ & ( for b₃ being object holds
( b₁ <= |.(b₃ - a).| or b₃ * b₂ c= V ) ) ) by A41, A40, A23; :: thesis:

end;

thus LinearTopSpaceNorm X is TopSpace-like :: thesis:

proof

end;

thus LinearTopSpaceNorm X is Abelian :: thesis:

proof

let v, w be VECTOR of (LinearTopSpaceNorm X); :: according to RLVECT_1:def 2 :: thesis:
reconsider v1 = v, w1 = w as VECTOR of X by Def4;
thus v + w = v1 + w1 by Def4
.= w1 + v1
.= w + v by Def4 ; :: thesis:

end;

thus LinearTopSpaceNorm X is add-associative :: thesis:

proof

let v, w, x be VECTOR of (LinearTopSpaceNorm X); :: according to RLVECT_1:def 3 :: thesis:
reconsider v1 = v, w1 = w, x1 = x as VECTOR of X by Def4;
A44: w + x = w1 + x1 by Def4;
v + w = v1 + w1 by Def4;
hence (v + w) + x = (v1 + w1) + x1 by Def4
.= v1 + (w1 + x1) by RLVECT_1:def 3
.= v + (w + x) by A44, Def4 ;
:: thesis:

end;

thus LinearTopSpaceNorm X is right_zeroed :: thesis:

proof

let v be VECTOR of (LinearTopSpaceNorm X); :: according to RLVECT_1:def 4 :: thesis:
reconsider v1 = v as VECTOR of X by Def4;
0. (LinearTopSpaceNorm X) = 0. X by Def4;
hence v + (0. (LinearTopSpaceNorm X)) = v1 + (0. X) by Def4
.= v by RLVECT_1:def 4 ;
:: thesis:

end;

thus LinearTopSpaceNorm X is right_complementable :: thesis:

proof

let v be VECTOR of (LinearTopSpaceNorm X); :: according to ALGSTR_0:def 16 :: thesis:
reconsider v1 = v as VECTOR of X by Def4;
reconsider w = - v1 as VECTOR of (LinearTopSpaceNorm X) by Def4;
take w ; :: according to ALGSTR_0:def 11 :: thesis:
thus v + w = v1 - v1 by Def4
.= 0. X by RLVECT_1:15
.= 0. (LinearTopSpaceNorm X) by Def4 ; :: thesis:

end;

A45: now :: thesis:

let a, b be Real; :: thesis:
let v be VECTOR of (LinearTopSpaceNorm X); :: thesis:
reconsider v1 = v as VECTOR of X by Def4;
b * v = b * v1 by Def4;
then a * (b * v1) = a * (b * v) by Def4;
then (a * b) * v1 = a * (b * v) by RLVECT_1:def 7;
hence (a * b) * v = a * (b * v) by Def4; :: thesis:

end;

A46: now :: thesis:

let a be Real; :: thesis:
let v, w be VECTOR of (LinearTopSpaceNorm X); :: thesis:
reconsider v1 = v, w1 = w as VECTOR of X by Def4;
( a * v = a * v1 & a * w = a * w1 ) by Def4;
then A47: (a * v1) + (a * w1) = (a * v) + (a * w) by Def4;
v + w = v1 + w1 by Def4;
then a * (v + w) = a * (v1 + w1) by Def4;
hence a * (v + w) = (a * v) + (a * w) by A47, RLVECT_1:def 5; :: thesis:

end;

now :: thesis:

let v be VECTOR of (LinearTopSpaceNorm X); :: thesis:
reconsider v1 = v as VECTOR of X by Def4;
thus 1 * v = 1 * v1 by Def4
.= v by RLVECT_1:def 8 ; :: thesis:

end;

hence ( LinearTopSpaceNorm X is vector-distributive & LinearTopSpaceNorm X is scalar-distributive & LinearTopSpaceNorm X is scalar-associative & LinearTopSpaceNorm X is scalar-unital ) by A46, A15, A45; :: thesis: