thus LinearTopSpaceNorm X is add-continuous :: thesis:
proof
let x1, x2 be Point of ; :: according to RLTOPSP1:def 8 :: thesis: for b1 being Element of bool the carrier of holds
( not b1 is open or not x1 + x2 in b1 or ex b2, b3 being Element of bool the carrier of st
( b2 is open & b3 is open & x1 in b2 & x2 in b3 & b2 + b3 c= b1 ) )

reconsider z2 = x2 as Element of () by Def4;
reconsider z1 = x1 as Element of () by Def4;
reconsider z12 = x1 + x2 as Element of () by Def4;
let V be Subset of ; :: thesis: ( not V is open or not x1 + x2 in V or ex b1, b2 being Element of bool the carrier of st
( b1 is open & b2 is open & x1 in b1 & x2 in b2 & b1 + b2 c= V ) )

assume that
A1: V is open and
A2: x1 + x2 in V ; :: thesis: ex b1, b2 being Element of bool the carrier of st
( b1 is open & b2 is open & x1 in b1 & x2 in b2 & b1 + b2 c= V )

V in the topology of by A1;
then V in the topology of () by Def4;
then consider r being Real such that
A3: r > 0 and
A4: Ball (z12,r) c= V by ;
set r2 = r / 2;
A5: 0 < r / 2 by ;
reconsider V1 = Ball (z1,(r / 2)), V2 = Ball (z2,(r / 2)) as Subset of by Def4;
A6: V1 + V2 c= V
proof
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 such that
A7: w = v + u and
A8: ( v in V1 & u in V2 ) ;
reconsider v1 = v, u1 = u as Element of () by Def4;
reconsider w1 = w as Element of () by ;
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 ;
( dist (z1,v1) < r / 2 & dist (z2,u1) < r / 2 ) by ;
then A10: (dist (z1,v1)) + (dist (z2,u1)) < (r / 2) + (r / 2) by XREAL_1:8;
reconsider ww1 = w as Point of X by ;
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
.= ||.((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 ;
then w1 in Ball (z12,r) by METRIC_1:11;
hence w in V by A4; :: thesis: verum
end;
dist (z2,z2) = 0 by METRIC_1:1;
then A12: x2 in V2 by ;
Ball (z2,(r / 2)) in the topology of () by PCOMPS_1:29;
then Ball (z2,(r / 2)) in the topology of by Def4;
then A13: V2 is open ;
Ball (z1,(r / 2)) in the topology of () by PCOMPS_1:29;
then Ball (z1,(r / 2)) in the topology of by Def4;
then A14: V1 is open ;
dist (z1,z1) = 0 by METRIC_1:1;
then x1 in V1 by ;
hence ex b1, b2 being Element of bool the carrier of st
( b1 is open & b2 is open & x1 in b1 & x2 in b2 & b1 + b2 c= V ) by A14, A13, A12, A6; :: thesis: verum
end;
A15: now :: thesis: for a, b being Real
for v being VECTOR of holds (a + b) * v = (a * v) + (b * v)
let a, b be Real; :: thesis: for v being VECTOR of holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of ; :: 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 ; :: thesis: verum
end;
thus LinearTopSpaceNorm X is Mult-continuous :: thesis:
proof
let a be Real; :: according to RLTOPSP1:def 9 :: thesis: for b1 being Element of the carrier of
for b2 being Element of bool the carrier of holds
( not b2 is open or not a * b1 in b2 or ex b3 being object ex b4 being Element of bool the carrier of st
( b4 is open & b1 in b4 & ( for b5 being object holds
( b3 <= |.(b5 - a).| or b5 * b4 c= b2 ) ) ) )

let x be Point of ; :: thesis: for b1 being Element of bool the carrier of holds
( not b1 is open or not a * x in b1 or ex b2 being object ex b3 being Element of bool the carrier of st
( b3 is open & x in b3 & ( for b4 being object holds
( b2 <= |.(b4 - a).| or b4 * b3 c= b1 ) ) ) )

let V be Subset of ; :: thesis: ( not V is open or not a * x in V or ex b1 being object ex b2 being Element of bool the carrier of st
( b2 is open & x in b2 & ( for b3 being object holds
( b1 <= |.(b3 - a).| or b3 * b2 c= V ) ) ) )

assume that
A17: V is open and
A18: a * x in V ; :: thesis: ex b1 being object ex b2 being Element of bool the carrier of st
( b2 is open & x in b2 & ( for b3 being object holds
( b1 <= |.(b3 - a).| or b3 * b2 c= V ) ) )

reconsider z = x, az = a * x as Element of () by Def4;
V in the topology of by A17;
then V in the topology of () by Def4;
then consider r0 being Real such that
A19: r0 > 0 and
A20: Ball (az,r0) c= V by ;
set r = r0 / 2;
r0 / 2 > 0 by ;
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 by Def4;
A22: r0 / 2 < r0 / 1 by ;
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: ( |.(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
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 such that
A25: w = s * v and
A26: v in W ;
reconsider v1 = v as Element of () by Def4;
A27: dist (z,v1) < min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1) by ;
reconsider w1 = w as Element of () by ;
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 ;
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 ;
A31: 0 <= 1 + ||.z1.|| by ;
then A32: (min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1)) * (||.zz.|| + 1) <= (((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)) * (||.zz.|| + 1) by ;
( 0 <= |.(a - s).| & 0 <= ||.vv1.|| ) by ;
then |.(a - s).| * ||.vv1.|| <= (min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1)) * (||.zz.|| + 1) by ;
then |.(a - s).| * ||.vv1.|| <= (((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)) * (||.z1.|| + 1) by ;
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 ;
then ((||.z1.|| + 1) / ((1 + ||.z1.||) + |.a.|)) * ((r0 / 2) / 2) <= 1 * ((r0 / 2) / 2) by ;
then A34: |.(a - s).| * ||.vv1.|| <= (r0 / 2) / 2 by ;
reconsider ww1 = w as Point of X by ;
(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 ;
0 <= 1 + ||.z1.|| by ;
then 0 + |.a.| <= (1 + ||.z1.||) + |.a.| by XREAL_1:6;
then |.a.| / ((1 + ||.z1.||) + |.a.|) <= 1 by ;
then A38: (|.a.| / ((1 + ||.z1.||) + |.a.|)) * ((r0 / 2) / 2) <= 1 * ((r0 / 2) / 2) by ;
||.(zz - vv1).|| * |.a.| <= (min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1)) * |.a.| by ;
then |.a.| * ||.(zz - vv1).|| <= |.a.| * (((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)) by ;
then |.a.| * ||.(zz - vv1).|| <= (|.a.| / ((1 + ||.z1.||) + |.a.|)) * ((r0 / 2) / 2) by XCMPLX_1:75;
then |.a.| * ||.(zz - vv1).|| <= (r0 / 2) / 2 by ;
then A39: (|.a.| * ||.(zz - vv1).||) + (|.(a - s).| * ||.vv1.||) <= ((r0 / 2) / 2) + ((r0 / 2) / 2) by ;
dist (az,w1) = ||.(zza - ww1).|| by Def1
.= ||.((a * zz) - ww1).|| by Def4
.= ||.((a * zz) - (s * vv1)).|| by ;
then dist (az,w1) <= r0 / 2 by ;
then dist (az,w1) < r0 by ;
then w1 in Ball (az,r0) by METRIC_1:11;
hence w in V by A20; :: thesis: verum
end;
end;
( 0 <= ||.z1.|| & 0 <= |.a.| ) by ;
then 0 / ((1 + ||.z1.||) + |.a.|) < ((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|) by ;
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 () by PCOMPS_1:29;
then Ball (z,(min ((((r0 / 2) / 2) / ((1 + ||.z1.||) + |.a.|)),1))) in the topology of by Def4;
then A41: W is open ;
dist (z,z) = 0 by METRIC_1:1;
then x in W by ;
hence ex b1 being object ex b2 being Element of bool the carrier of st
( b2 is open & x in b2 & ( for b3 being object holds
( b1 <= |.(b3 - a).| or b3 * b2 c= V ) ) ) by ; :: thesis: verum
end;
thus LinearTopSpaceNorm X is TopSpace-like :: thesis:
proof
set LTSN = LinearTopSpaceNorm X;
A42: the topology of = the topology of () by Def4;
then A43: for a, b being Subset of st a in the topology of & b in the topology of holds
a /\ b in the topology of by PRE_TOPC:def 1;
the carrier of = the carrier of () by Def4;
then ( the carrier of in the topology of & ( for a being Subset-Family of st a c= the topology of holds
union a in the topology of ) ) by ;
hence LinearTopSpaceNorm X is TopSpace-like by A43; :: thesis: verum
end;
thus LinearTopSpaceNorm X is Abelian :: thesis:
proof
let v, w be VECTOR of ; :: 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;
thus LinearTopSpaceNorm X is add-associative :: thesis:
proof
let v, w, x be VECTOR of ; :: 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 ;
:: thesis: verum
end;
thus LinearTopSpaceNorm X is right_zeroed :: thesis:
proof
let v be VECTOR of ; :: according to RLVECT_1:def 4 :: thesis: v + () = v
reconsider v1 = v as VECTOR of X by Def4;
0. = 0. X by Def4;
hence v + () = v1 + (0. X) by Def4
.= v by RLVECT_1:def 4 ;
:: thesis: verum
end;
thus LinearTopSpaceNorm X is right_complementable :: thesis:
proof
let v be VECTOR of ; :: according to ALGSTR_0:def 16 :: thesis:
reconsider v1 = v as VECTOR of X by Def4;
reconsider w = - v1 as VECTOR of by Def4;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0.
thus v + w = v1 - v1 by Def4
.= 0. X by RLVECT_1:15
.= 0. by Def4 ; :: thesis: verum
end;
A45: now :: thesis: for a, b being Real
for v being VECTOR of holds (a * b) * v = a * (b * v)
let a, b be Real; :: thesis: for v being VECTOR of holds (a * b) * v = a * (b * v)
let v be VECTOR of ; :: 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;
A46: now :: thesis: for a being Real
for v, w being VECTOR of holds a * (v + w) = (a * v) + (a * w)
let a be Real; :: thesis: for v, w being VECTOR of holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of ; :: 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 ; :: thesis: verum
end;
now :: thesis: for v being VECTOR of holds 1 * v = v
let v be VECTOR of ; :: 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;
hence ( LinearTopSpaceNorm X is vector-distributive & LinearTopSpaceNorm X is scalar-distributive & LinearTopSpaceNorm X is scalar-associative & LinearTopSpaceNorm X is scalar-unital ) by ; :: thesis: verum