thus
LinearTopSpaceNorm X is add-continuous
:: thesis: ( LinearTopSpaceNorm X is Mult-continuous & LinearTopSpaceNorm X is TopSpace-like & LinearTopSpaceNorm X is Abelian & LinearTopSpaceNorm X is add-associative & LinearTopSpaceNorm X is right_zeroed & LinearTopSpaceNorm X is right_complementable & LinearTopSpaceNorm X is vector-distributive & LinearTopSpaceNorm X is scalar-distributive & LinearTopSpaceNorm X is scalar-associative & LinearTopSpaceNorm X is scalar-unital )

proof

let x1, x2 be Point of (LinearTopSpaceNorm X); :: according to RLTOPSP1:def 8 :: thesis: for b_{1} being Element of bool the carrier of (LinearTopSpaceNorm X) holds

( not b_{1} is open or not x1 + x2 in b_{1} or ex b_{2}, b_{3} being Element of bool the carrier of (LinearTopSpaceNorm X) st

( b_{2} is open & b_{3} is open & x1 in b_{2} & x2 in b_{3} & b_{2} + b_{3} c= b_{1} ) )

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: ( not V is open or not x1 + x2 in V or ex b_{1}, b_{2} being Element of bool the carrier of (LinearTopSpaceNorm X) st

( b_{1} is open & b_{2} is open & x1 in b_{1} & x2 in b_{2} & b_{1} + b_{2} c= V ) )

assume that

A1: V is open and

A2: x1 + x2 in V ; :: thesis: ex b_{1}, b_{2} being Element of bool the carrier of (LinearTopSpaceNorm X) st

( b_{1} is open & b_{2} is open & x1 in b_{1} & x2 in b_{2} & b_{1} + b_{2} c= V )

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

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_{1}, b_{2} being Element of bool the carrier of (LinearTopSpaceNorm X) st

( b_{1} is open & b_{2} is open & x1 in b_{1} & x2 in b_{2} & b_{1} + b_{2} c= V )
by A14, A13, A12, A6; :: thesis: verum

end;( not b

( b

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: ( not V is open or not x1 + x2 in V or ex b

( b

assume that

A1: V is open and

A2: x1 + x2 in V ; :: thesis: ex b

( b

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

dist (z2,z2) = 0
by METRIC_1:1;
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in V1 + V2 or w in V )

assume w in V1 + V2 ; :: thesis: w in V

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: verum

end;assume w in V1 + V2 ; :: thesis: w in V

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: verum

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

A15: now :: thesis: for a, b being Real

for v being VECTOR of (LinearTopSpaceNorm X) holds (a + b) * v = (a * v) + (b * v)

thus
LinearTopSpaceNorm X is Mult-continuous
:: thesis: ( LinearTopSpaceNorm X is TopSpace-like & LinearTopSpaceNorm X is Abelian & LinearTopSpaceNorm X is add-associative & LinearTopSpaceNorm X is right_zeroed & LinearTopSpaceNorm X is right_complementable & LinearTopSpaceNorm X is vector-distributive & LinearTopSpaceNorm X is scalar-distributive & LinearTopSpaceNorm X is scalar-associative & LinearTopSpaceNorm X is scalar-unital )for v being VECTOR of (LinearTopSpaceNorm X) holds (a + b) * v = (a * v) + (b * v)

let a, b be Real; :: thesis: for v being VECTOR of (LinearTopSpaceNorm X) holds (a + b) * v = (a * v) + (b * v)

let v be VECTOR of (LinearTopSpaceNorm X); :: thesis: (a + b) * v = (a * v) + (b * v)

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: verum

end;let v be VECTOR of (LinearTopSpaceNorm X); :: thesis: (a + b) * v = (a * v) + (b * v)

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: verum

proof

thus
LinearTopSpaceNorm X is TopSpace-like
:: thesis: ( LinearTopSpaceNorm X is Abelian & LinearTopSpaceNorm X is add-associative & LinearTopSpaceNorm X is right_zeroed & LinearTopSpaceNorm X is right_complementable & LinearTopSpaceNorm X is vector-distributive & LinearTopSpaceNorm X is scalar-distributive & LinearTopSpaceNorm X is scalar-associative & LinearTopSpaceNorm X is scalar-unital )
let a be Real; :: according to RLTOPSP1:def 9 :: thesis: for b_{1} being Element of the carrier of (LinearTopSpaceNorm X)

for b_{2} being Element of bool the carrier of (LinearTopSpaceNorm X) holds

( not b_{2} is open or not a * b_{1} in b_{2} or ex b_{3} being object ex b_{4} being Element of bool the carrier of (LinearTopSpaceNorm X) st

( b_{4} is open & b_{1} in b_{4} & ( for b_{5} being object holds

( b_{3} <= |.(b_{5} - a).| or b_{5} * b_{4} c= b_{2} ) ) ) )

let x be Point of (LinearTopSpaceNorm X); :: thesis: for b_{1} being Element of bool the carrier of (LinearTopSpaceNorm X) holds

( not b_{1} is open or not a * x in b_{1} or ex b_{2} being object ex b_{3} being Element of bool the carrier of (LinearTopSpaceNorm X) st

( b_{3} is open & x in b_{3} & ( for b_{4} being object holds

( b_{2} <= |.(b_{4} - a).| or b_{4} * b_{3} c= b_{1} ) ) ) )

let V be Subset of (LinearTopSpaceNorm X); :: thesis: ( not V is open or not a * x in V or ex b_{1} being object ex b_{2} being Element of bool the carrier of (LinearTopSpaceNorm X) st

( b_{2} is open & x in b_{2} & ( for b_{3} being object holds

( b_{1} <= |.(b_{3} - a).| or b_{3} * b_{2} c= V ) ) ) )

assume that

A17: V is open and

A18: a * x in V ; :: thesis: ex b_{1} being object ex b_{2} being Element of bool the carrier of (LinearTopSpaceNorm X) st

( b_{2} is open & x in b_{2} & ( for b_{3} being object holds

( b_{1} <= |.(b_{3} - a).| or b_{3} * b_{2} c= V ) ) )

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

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_{1} being object ex b_{2} being Element of bool the carrier of (LinearTopSpaceNorm X) st

( b_{2} is open & x in b_{2} & ( for b_{3} being object holds

( b_{1} <= |.(b_{3} - a).| or b_{3} * b_{2} c= V ) ) )
by A41, A40, A23; :: thesis: verum

end;for b

( not b

( b

( b

let x be Point of (LinearTopSpaceNorm X); :: thesis: for b

( not b

( b

( b

let V be Subset of (LinearTopSpaceNorm X); :: thesis: ( not V is open or not a * x in V or ex b

( b

( b

assume that

A17: V is open and

A18: a * x in V ; :: thesis: ex b

( b

( b

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

( 0 <= ||.z1.|| & 0 <= |.a.| )
by COMPLEX1:46, NORMSP_1:4;
let s be Real; :: thesis: ( |.(s - a).| < min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1) implies s * W c= V )

assume |.(s - a).| < min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1) ; :: thesis: s * W c= V

then A24: |.(a - s).| <= min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1) by COMPLEX1:60;

thus s * W c= V :: thesis: verum

end;assume |.(s - a).| < min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1) ; :: thesis: s * W c= V

then A24: |.(a - s).| <= min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1) by COMPLEX1:60;

thus s * W c= V :: thesis: verum

proof

let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in s * W or w in V )

assume w in s * W ; :: thesis: w in V

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: verum

end;assume w in s * W ; :: thesis: w in V

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: verum

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

( b

( b

proof

thus
LinearTopSpaceNorm X is Abelian
:: thesis: ( LinearTopSpaceNorm X is add-associative & LinearTopSpaceNorm X is right_zeroed & LinearTopSpaceNorm X is right_complementable & LinearTopSpaceNorm X is vector-distributive & LinearTopSpaceNorm X is scalar-distributive & LinearTopSpaceNorm X is scalar-associative & LinearTopSpaceNorm X is scalar-unital )
set LTSN = LinearTopSpaceNorm X;

A42: the topology of (LinearTopSpaceNorm X) = the topology of (TopSpaceNorm X) by Def4;

then A43: for a, b being Subset of (LinearTopSpaceNorm X) st a in the topology of (LinearTopSpaceNorm X) & b in the topology of (LinearTopSpaceNorm X) holds

a /\ b in the topology of (LinearTopSpaceNorm X) by PRE_TOPC:def 1;

the carrier of (LinearTopSpaceNorm X) = the carrier of (TopSpaceNorm X) by Def4;

then ( the carrier of (LinearTopSpaceNorm X) in the topology of (LinearTopSpaceNorm X) & ( for a being Subset-Family of (LinearTopSpaceNorm X) st a c= the topology of (LinearTopSpaceNorm X) holds

union a in the topology of (LinearTopSpaceNorm X) ) ) by A42, PRE_TOPC:def 1;

hence LinearTopSpaceNorm X is TopSpace-like by A43; :: thesis: verum

end;A42: the topology of (LinearTopSpaceNorm X) = the topology of (TopSpaceNorm X) by Def4;

then A43: for a, b being Subset of (LinearTopSpaceNorm X) st a in the topology of (LinearTopSpaceNorm X) & b in the topology of (LinearTopSpaceNorm X) holds

a /\ b in the topology of (LinearTopSpaceNorm X) by PRE_TOPC:def 1;

the carrier of (LinearTopSpaceNorm X) = the carrier of (TopSpaceNorm X) by Def4;

then ( the carrier of (LinearTopSpaceNorm X) in the topology of (LinearTopSpaceNorm X) & ( for a being Subset-Family of (LinearTopSpaceNorm X) st a c= the topology of (LinearTopSpaceNorm X) holds

union a in the topology of (LinearTopSpaceNorm X) ) ) by A42, PRE_TOPC:def 1;

hence LinearTopSpaceNorm X is TopSpace-like by A43; :: thesis: verum

proof

thus
LinearTopSpaceNorm X is add-associative
:: thesis: ( LinearTopSpaceNorm X is right_zeroed & LinearTopSpaceNorm X is right_complementable & LinearTopSpaceNorm X is vector-distributive & LinearTopSpaceNorm X is scalar-distributive & LinearTopSpaceNorm X is scalar-associative & LinearTopSpaceNorm X is scalar-unital )
let v, w be VECTOR of (LinearTopSpaceNorm X); :: according to RLVECT_1:def 2 :: thesis: v + w = w + v

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: verum

end;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: verum

proof

thus
LinearTopSpaceNorm X is right_zeroed
:: thesis: ( LinearTopSpaceNorm X is right_complementable & LinearTopSpaceNorm X is vector-distributive & LinearTopSpaceNorm X is scalar-distributive & LinearTopSpaceNorm X is scalar-associative & LinearTopSpaceNorm X is scalar-unital )
let v, w, x be VECTOR of (LinearTopSpaceNorm X); :: according to RLVECT_1:def 3 :: thesis: (v + w) + x = v + (w + x)

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: verum

end;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: verum

proof

thus
LinearTopSpaceNorm X is right_complementable
:: thesis: ( LinearTopSpaceNorm X is vector-distributive & LinearTopSpaceNorm X is scalar-distributive & LinearTopSpaceNorm X is scalar-associative & LinearTopSpaceNorm X is scalar-unital )
let v be VECTOR of (LinearTopSpaceNorm X); :: according to RLVECT_1:def 4 :: thesis: v + (0. (LinearTopSpaceNorm X)) = v

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: verum

end;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: verum

proof

let v be VECTOR of (LinearTopSpaceNorm X); :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable

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: v + w = 0. (LinearTopSpaceNorm X)

thus v + w = v1 - v1 by Def4

.= 0. X by RLVECT_1:15

.= 0. (LinearTopSpaceNorm X) by Def4 ; :: thesis: verum

end;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: v + w = 0. (LinearTopSpaceNorm X)

thus v + w = v1 - v1 by Def4

.= 0. X by RLVECT_1:15

.= 0. (LinearTopSpaceNorm X) by Def4 ; :: thesis: verum

A45: now :: thesis: for a, b being Real

for v being VECTOR of (LinearTopSpaceNorm X) holds (a * b) * v = a * (b * v)

for v being VECTOR of (LinearTopSpaceNorm X) holds (a * b) * v = a * (b * v)

let a, b be Real; :: thesis: for v being VECTOR of (LinearTopSpaceNorm X) holds (a * b) * v = a * (b * v)

let v be VECTOR of (LinearTopSpaceNorm X); :: thesis: (a * b) * v = a * (b * v)

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: verum

end;let v be VECTOR of (LinearTopSpaceNorm X); :: thesis: (a * b) * v = a * (b * v)

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: verum

A46: now :: thesis: for a being Real

for v, w being VECTOR of (LinearTopSpaceNorm X) holds a * (v + w) = (a * v) + (a * w)

for v, w being VECTOR of (LinearTopSpaceNorm X) holds a * (v + w) = (a * v) + (a * w)

let a be Real; :: thesis: for v, w being VECTOR of (LinearTopSpaceNorm X) holds a * (v + w) = (a * v) + (a * w)

let v, w be VECTOR of (LinearTopSpaceNorm X); :: thesis: a * (v + w) = (a * v) + (a * w)

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: verum

end;let v, w be VECTOR of (LinearTopSpaceNorm X); :: thesis: a * (v + w) = (a * v) + (a * w)

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: verum

now :: thesis: for v being VECTOR of (LinearTopSpaceNorm X) holds 1 * v = v

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: verumlet v be VECTOR of (LinearTopSpaceNorm X); :: thesis: 1 * v = v

reconsider v1 = v as VECTOR of X by Def4;

thus 1 * v = 1 * v1 by Def4

.= v by RLVECT_1:def 8 ; :: thesis: verum

end;reconsider v1 = v as VECTOR of X by Def4;

thus 1 * v = 1 * v1 by Def4

.= v by RLVECT_1:def 8 ; :: thesis: verum