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 RealLinearSpace-like )
proof
let x1, x2 be Point of (LinearTopSpaceNorm X); :: according to RLTOPSP1:def 8 :: thesis: for b1 being Element of bool the carrier of (LinearTopSpaceNorm X) holds
( not b1 is open or not x1 + x2 in b1 or ex b2, b3 being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b2 is open & b3 is open & x1 in b2 & x2 in b3 & b2 + b3 c= b1 ) )
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 b1, b2 being Element of bool the carrier of (LinearTopSpaceNorm X) 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 (LinearTopSpaceNorm X) st
( b1 is open & b2 is open & x1 in b1 & x2 in b2 & b1 + b2 c= V )
V in the topology of (LinearTopSpaceNorm X) by A1, PRE_TOPC:def 5;
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 5;
set r2 = r / 2;
A5: 0 < r / 2 by A3, XREAL_1:217;
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 set ; :: 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 2;
( dist z1,v1 < r / 2 & dist z2,u1 < r / 2 ) by A8, METRIC_1:12;
then A10: (dist z1,v1) + (dist z2,u1) < (r / 2) + (r / 2) by XREAL_1:10;
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:45
.= ||.(((zz1 + zz2) + (- vv1)) + (- uu1)).|| by RLVECT_1:def 6
.= ||.(((zz1 + (- vv1)) + zz2) + (- uu1)).|| by RLVECT_1:def 6
.= ||.((zz1 + (- vv1)) + (zz2 + (- uu1))).|| by RLVECT_1:def 6 ;
then dist z12,w1 < r by A9, A11, A10, XXREAL_0:2;
then w1 in Ball z12,r by METRIC_1:12;
hence w in V by A4; :: thesis: verum
end;
dist z2,z2 = 0 by METRIC_1:1;
then A12: x2 in V2 by A5, METRIC_1:12;
Ball z2,(r / 2) in the topology of (TopSpaceNorm X) by PCOMPS_1:33;
then Ball z2,(r / 2) in the topology of (LinearTopSpaceNorm X) by Def4;
then A13: V2 is open by PRE_TOPC:def 5;
Ball z1,(r / 2) in the topology of (TopSpaceNorm X) by PCOMPS_1:33;
then Ball z1,(r / 2) in the topology of (LinearTopSpaceNorm X) by Def4;
then A14: V1 is open by PRE_TOPC:def 5;
dist z1,z1 = 0 by METRIC_1:1;
then x1 in V1 by A5, METRIC_1:12;
hence ex b1, b2 being Element of bool the carrier of (LinearTopSpaceNorm X) 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
let a, b be real number ; :: 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 9; :: thesis: verum
end;
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 RealLinearSpace-like )
proof
let a be Real; :: according to RLTOPSP1:def 9 :: thesis: for b1 being Element of the carrier of (LinearTopSpaceNorm X)
for b2 being Element of bool the carrier of (LinearTopSpaceNorm X) holds
( not b2 is open or not a * b1 in b2 or ex b3 being Element of REAL ex b4 being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b4 is open & b1 in b4 & ( for b5 being Element of REAL holds
( b3 <= abs (b5 - a) or b5 * b4 c= b2 ) ) ) )
let x be Point of (LinearTopSpaceNorm X); :: thesis: for b1 being Element of bool the carrier of (LinearTopSpaceNorm X) holds
( not b1 is open or not a * x in b1 or ex b2 being Element of REAL ex b3 being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b3 is open & x in b3 & ( for b4 being Element of REAL holds
( b2 <= abs (b4 - a) or b4 * b3 c= b1 ) ) ) )
let V be Subset of (LinearTopSpaceNorm X); :: thesis: ( not V is open or not a * x in V or ex b1 being Element of REAL ex b2 being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b2 is open & x in b2 & ( for b3 being Element of REAL holds
( b1 <= abs (b3 - a) or b3 * b2 c= V ) ) ) )
assume that
A17: V is open and
A18: a * x in V ; :: thesis: ex b1 being Element of REAL ex b2 being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b2 is open & x in b2 & ( for b3 being Element of REAL holds
( b1 <= abs (b3 - a) or b3 * b2 c= V ) ) )
reconsider z = x, az = a * x as Element of (MetricSpaceNorm X) by Def4;
V in the topology of (LinearTopSpaceNorm X) by A17, PRE_TOPC:def 5;
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 5;
set r = r0 / 2;
r0 / 2 > 0 by A19, XREAL_1:217;
then A21: 0 < (r0 / 2) / 2 by XREAL_1:217;
reconsider z1 = z as Point of X ;
set r2 = min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1;
reconsider W = Ball z,(min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1) as Subset of (LinearTopSpaceNorm X) by Def4;
A22: r0 / 2 < r0 / 1 by A19, XREAL_1:78;
A23: for s being Real st abs (s - a) < min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1 holds
s * W c= V
proof
let s be Real; :: thesis: ( abs (s - a) < min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1 implies s * W c= V )
assume abs (s - a) < min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1 ; :: thesis: s * W c= V
then A24: abs (a - s) <= min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1 by COMPLEX1:146;
thus s * W c= V :: thesis: verum
proof
let w be set ; :: 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.||) + (abs a))),1 by A26, METRIC_1:12;
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.||) + (abs a))),1 <= 1 by XXREAL_0:17;
then ||.(zz - vv1).|| <= 1 by A28, A27, XXREAL_0:2;
then ||.(vv1 - zz).|| <= 1 by NORMSP_1:11;
then A29: ||.zz.|| + ||.(vv1 - zz).|| <= ||.zz.|| + 1 by XREAL_1:8;
zz + (vv1 - zz) = vv1 - (zz - zz) by RLVECT_1:43
.= vv1 - (0. X) by RLVECT_1:28
.= vv1 by RLVECT_1:26 ;
then ||.vv1.|| <= ||.zz.|| + ||.(vv1 - zz).|| by NORMSP_1:def 2;
then A30: ||.vv1.|| <= ||.zz.|| + 1 by A29, XXREAL_0:2;
A31: 0 <= 1 + ||.z1.|| by NORMSP_1:8, XREAL_1:41;
then A32: (min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1) * (||.zz.|| + 1) <= (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))) * (||.zz.|| + 1) by XREAL_1:66, XXREAL_0:17;
( 0 <= abs (a - s) & 0 <= ||.vv1.|| ) by COMPLEX1:132, NORMSP_1:8;
then (abs (a - s)) * ||.vv1.|| <= (min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1) * (||.zz.|| + 1) by A24, A30, XREAL_1:68;
then (abs (a - s)) * ||.vv1.|| <= (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))) * (||.z1.|| + 1) by A32, XXREAL_0:2;
then A33: (abs (a - s)) * ||.vv1.|| <= ((||.z1.|| + 1) / ((1 + ||.z1.||) + (abs a))) * ((r0 / 2) / 2) by XCMPLX_1:76;
0 <= abs a by COMPLEX1:132;
then 0 + (1 + ||.z1.||) <= (abs a) + (1 + ||.z1.||) by XREAL_1:8;
then (||.z1.|| + 1) / ((1 + ||.z1.||) + (abs a)) <= 1 by A31, XREAL_1:185;
then ((||.z1.|| + 1) / ((1 + ||.z1.||) + (abs a))) * ((r0 / 2) / 2) <= 1 * ((r0 / 2) / 2) by A19, XREAL_1:66;
then A34: (abs (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:48
.= ((a * zz) - (a * vv1)) - ((s * vv1) - (a * vv1)) by RLVECT_1:49
.= (a * zz) - (((s * vv1) - (a * vv1)) + (a * vv1)) by RLVECT_1:41
.= (a * zz) - ((s * vv1) - ((a * vv1) - (a * vv1))) by RLVECT_1:43
.= (a * zz) - ((s * vv1) - (0. X)) by RLVECT_1:28
.= (a * zz) - (s * vv1) by RLVECT_1:26 ;
then ||.((a * zz) - (s * vv1)).|| <= ||.(a * (zz - vv1)).|| + ||.((s - a) * vv1).|| by NORMSP_1:7;
then ||.((a * zz) - (s * vv1)).|| <= ((abs a) * ||.(zz - vv1).||) + ||.((s - a) * vv1).|| by NORMSP_1:def 2;
then ||.((a * zz) - (s * vv1)).|| <= ((abs a) * ||.(zz - vv1).||) + ((abs (s - a)) * ||.vv1.||) by NORMSP_1:def 2;
then A35: ||.((a * zz) - (s * vv1)).|| <= ((abs a) * ||.(zz - vv1).||) + ((abs (a - s)) * ||.vv1.||) by COMPLEX1:146;
A36: 0 <= abs a by COMPLEX1:132;
then A37: (min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1) * (abs a) <= (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))) * (abs a) by XREAL_1:66, XXREAL_0:17;
0 <= 1 + ||.z1.|| by NORMSP_1:8, XREAL_1:41;
then 0 + (abs a) <= (1 + ||.z1.||) + (abs a) by XREAL_1:8;
then (abs a) / ((1 + ||.z1.||) + (abs a)) <= 1 by A36, XREAL_1:185;
then A38: ((abs a) / ((1 + ||.z1.||) + (abs a))) * ((r0 / 2) / 2) <= 1 * ((r0 / 2) / 2) by A19, XREAL_1:66;
||.(zz - vv1).|| * (abs a) <= (min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1) * (abs a) by A28, A27, A36, XREAL_1:66;
then (abs a) * ||.(zz - vv1).|| <= (abs a) * (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))) by A37, XXREAL_0:2;
then (abs a) * ||.(zz - vv1).|| <= ((abs a) / ((1 + ||.z1.||) + (abs a))) * ((r0 / 2) / 2) by XCMPLX_1:76;
then (abs a) * ||.(zz - vv1).|| <= (r0 / 2) / 2 by A38, XXREAL_0:2;
then A39: ((abs a) * ||.(zz - vv1).||) + ((abs (a - s)) * ||.vv1.||) <= ((r0 / 2) / 2) + ((r0 / 2) / 2) by A34, XREAL_1:9;
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:12;
hence w in V by A20; :: thesis: verum
end;
end;
( 0 <= ||.z1.|| & 0 <= abs a ) by COMPLEX1:132, NORMSP_1:8;
then 0 / ((1 + ||.z1.||) + (abs a)) < ((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a)) by A21, XREAL_1:76;
then A40: 0 < min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1 by XXREAL_0:15;
Ball z,(min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1) in the topology of (TopSpaceNorm X) by PCOMPS_1:33;
then Ball z,(min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1) in the topology of (LinearTopSpaceNorm X) by Def4;
then A41: W is open by PRE_TOPC:def 5;
dist z,z = 0 by METRIC_1:1;
then x in W by A40, METRIC_1:12;
hence ex b1 being Element of REAL ex b2 being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b2 is open & x in b2 & ( for b3 being Element of REAL holds
( b1 <= abs (b3 - a) or b3 * b2 c= V ) ) ) by A41, A40, A23; :: thesis: verum
end;
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 RealLinearSpace-like )
proof
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, PRE_TOPC:def 1; :: thesis: verum
end;
thus LinearTopSpaceNorm X is Abelian :: thesis: ( LinearTopSpaceNorm X is add-associative & LinearTopSpaceNorm X is right_zeroed & LinearTopSpaceNorm X is right_complementable & LinearTopSpaceNorm X is RealLinearSpace-like )
proof
let v, w be VECTOR of (LinearTopSpaceNorm X); :: according to RLVECT_1:def 5 :: 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: ( LinearTopSpaceNorm X is right_zeroed & LinearTopSpaceNorm X is right_complementable & LinearTopSpaceNorm X is RealLinearSpace-like )
proof
let v, w, x be VECTOR of (LinearTopSpaceNorm X); :: according to RLVECT_1:def 6 :: 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 6
.= v + (w + x) by A44, Def4 ;
:: thesis: verum
end;
thus LinearTopSpaceNorm X is right_zeroed :: thesis: ( LinearTopSpaceNorm X is right_complementable & LinearTopSpaceNorm X is RealLinearSpace-like )
proof
let v be VECTOR of (LinearTopSpaceNorm X); :: according to RLVECT_1:def 7 :: 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 7 ;
:: thesis: verum
end;
thus LinearTopSpaceNorm X is right_complementable :: thesis: LinearTopSpaceNorm X is RealLinearSpace-like
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:28
.= 0. (LinearTopSpaceNorm X) by Def4 ; :: thesis: verum
end;
A45: now
let a, b be real number ; :: 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 9;
hence (a * b) * v = a * (b * v) by Def4; :: thesis: verum
end;
A46: now
let a be real number ; :: 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 9; :: thesis: verum
end;
now
let 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 9 ; :: thesis: verum
end;
hence LinearTopSpaceNorm X is RealLinearSpace-like by A46, A15, A45, RLVECT_1:def 9; :: thesis: verum