consider CY being Subset of X such that
A2: ( CY = the carrier of Y & CY is closed ) by A1;
set S = VectQuot (X,Y);
A3: the carrier of (VectQuot (X,Y)) = CosetSet (X,Y) by LMQ06;
then reconsider NF = NormCoset (X,Y) as Function of the carrier of (VectQuot (X,Y)),REAL ;
reconsider T = NORMSTR(# the carrier of (VectQuot (X,Y)),(0. (VectQuot (X,Y))), the addF of (VectQuot (X,Y)), the Mult of (VectQuot (X,Y)),NF #) as non empty NORMSTR ;
now :: thesis: for v, w being Element of T holds v + w = w + v
let v, w be Element of T; :: thesis: v + w = w + v
reconsider v1 = v, w1 = w as Element of (VectQuot (X,Y)) ;
thus v + w = v1 + w1
.= w1 + v1
.= w + v ; :: thesis: verum
end;
then A4: T is Abelian ;
now :: thesis: for u, v, w being Element of T holds (u + v) + w = u + (v + w)
let u, v, w be Element of T; :: thesis: (u + v) + w = u + (v + w)
reconsider u1 = u, v1 = v, w1 = w as Element of (VectQuot (X,Y)) ;
thus (u + v) + w = (u1 + v1) + w1
.= u1 + (v1 + w1) by RLVECT_1:def 3
.= u + (v + w) ; :: thesis: verum
end;
then A5: T is add-associative ;
now :: thesis: for v being Element of T holds v + (0. T) = v
let v be Element of T; :: thesis: v + (0. T) = v
reconsider v1 = v as Element of (VectQuot (X,Y)) ;
thus v + (0. T) = v1 + (0. (VectQuot (X,Y)))
.= v by RLVECT_1:def 4 ; :: thesis: verum
end;
then A6: T is right_zeroed ;
A7: T is right_complementable
proof
let v be Element of T; :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
reconsider v1 = v as Element of (VectQuot (X,Y)) ;
reconsider w1 = - v1 as Element of (VectQuot (X,Y)) ;
reconsider w = w1 as Element of T ;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. T
thus v + w = v1 + w1
.= 0. T by RLVECT_1:5 ; :: thesis: verum
end;
now :: thesis: for a, b being Real
for v being Element of T holds (a + b) * v = (a * v) + (b * v)
let a, b be Real; :: thesis: for v being Element of T holds (a + b) * v = (a * v) + (b * v)
let v be Element of T; :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider v1 = v as Element of (VectQuot (X,Y)) ;
thus (a + b) * v = (a + b) * v1
.= (a * v1) + (b * v1) by RLVECT_1:def 6
.= (a * v) + (b * v) ; :: thesis: verum
end;
then A8: T is scalar-distributive ;
now :: thesis: for a being Real
for v, w being Element of T holds a * (v + w) = (a * v) + (a * w)
let a be Real; :: thesis: for v, w being Element of T holds a * (v + w) = (a * v) + (a * w)
let v, w be Element of T; :: thesis: a * (v + w) = (a * v) + (a * w)
reconsider v1 = v, w1 = w as Element of (VectQuot (X,Y)) ;
thus a * (v + w) = a * (v1 + w1)
.= (a * v1) + (a * w1) by RLVECT_1:def 5
.= (a * v) + (a * w) ; :: thesis: verum
end;
then A9: T is vector-distributive ;
now :: thesis: for a, b being Real
for v being Element of T holds (a * b) * v = a * (b * v)
let a, b be Real; :: thesis: for v being Element of T holds (a * b) * v = a * (b * v)
let v be Element of T; :: thesis: (a * b) * v = a * (b * v)
reconsider v1 = v as Element of (VectQuot (X,Y)) ;
thus (a * b) * v = (a * b) * v1
.= a * (b * v1) by RLVECT_1:def 7
.= a * (b * v) ; :: thesis: verum
end;
then A10: T is scalar-associative ;
now :: thesis: for v being Element of T holds 1 * v = v
let v be Element of T; :: thesis: 1 * v = v
reconsider v1 = v as Element of (VectQuot (X,Y)) ;
thus 1 * v = 1 * v1
.= v by RLVECT_1:def 8 ; :: thesis: verum
end;
then A11: T is scalar-unital ;
A13: ||.(0. T).|| = lower_bound (NormVSets (X,Y,(0. X))) by A3, DeNorm, LMQ13;
then A14: ||.(0. T).|| <= ||.(0. X).|| by LMQ23;
then A15: T is reflexive by A13, LMQ23;
now :: thesis: for z being Element of T st ||.z.|| = 0 holds
z = 0. T
let z be Element of T; :: thesis: ( ||.z.|| = 0 implies z = 0. T )
assume A16: ||.z.|| = 0 ; :: thesis: z = 0. T
reconsider z1 = z as Element of (VectQuot (X,Y)) ;
consider v being Point of X such that
A17: z1 = v + Y by LMQ07;
A18: 0 = lower_bound (NormVSets (X,Y,v)) by A3, A16, A17, DeNorm;
for e being Real st 0 < e holds
ex w being VECTOR of X st
( w in CY & ||.(v - w).|| <= e )
proof
let e be Real; :: thesis: ( 0 < e implies ex w being VECTOR of X st
( w in CY & ||.(v - w).|| <= e ) )
set g = lower_bound (NormVSets (X,Y,v));
assume 0 < e ; :: thesis: ex w being VECTOR of X st
( w in CY & ||.(v - w).|| <= e )
then consider r being Real such that
A19: ( r in NormVSets (X,Y,v) & r < (lower_bound (NormVSets (X,Y,v))) + e ) by SEQ_4:def 2;
consider x being VECTOR of X such that
A20: ( r = ||.x.|| & x in v + Y ) by A19;
consider u being Point of X such that
A21: ( x = v + u & u in Y ) by A20;
set w = - u;
take - u ; :: thesis: ( - u in CY & ||.(v - (- u)).|| <= e )
- u in Y by A21, RLSUB_1:22;
hence - u in CY by A2; :: thesis: ||.(v - (- u)).|| <= e
thus ||.(v - (- u)).|| <= e by A18, A19, A20, A21, RLVECT_1:17; :: thesis: verum
end;
then v in Y by A2, CLOSE1;
then v + Y = the carrier of Y by RLSUB_1:48;
hence z = 0. T by A17, LMQ13; :: thesis: verum
end;
then A22: T is discerning ;
now :: thesis: for a being Real
for v, w being Element of T holds
( ||.(a * v).|| = |.a.| * ||.v.|| & ||.(v + w).|| <= ||.v.|| + ||.w.|| )
let a be Real; :: thesis: for v, w being Element of T holds
( ||.(a * v).|| = |.a.| * ||.v.|| & ||.(v + w).|| <= ||.v.|| + ||.w.|| )
let v, w be Element of T; :: thesis: ( ||.(a * v).|| = |.a.| * ||.v.|| & ||.(v + w).|| <= ||.v.|| + ||.w.|| )
reconsider v1 = v, w1 = w as Element of (VectQuot (X,Y)) ;
thus ||.(a * v).|| = |.a.| * ||.v.|| :: thesis: ||.(v + w).|| <= ||.v.|| + ||.w.||
proof
per cases ( a = 0 or not a = 0 ) ;
suppose A23: a = 0 ; :: thesis: ||.(a * v).|| = |.a.| * ||.v.||
then 0. T = a * v1 by RLVECT_1:10
.= a * v ;
hence ||.(a * v).|| = |.a.| * ||.v.|| by A13, A14, A23, COMPLEX1:44, LMQ23; :: thesis: verum
end;
suppose A24: not a = 0 ; :: thesis: ||.(a * v).|| = |.a.| * ||.v.||
then A25: 0 < |.a.| by COMPLEX1:47;
consider vv1 being Point of X such that
A26: v1 = vv1 + Y by LMQ07;
A27: ||.v.|| = lower_bound (NormVSets (X,Y,vv1)) by A3, A26, DeNorm;
a * v = a * v1
.= (a * vv1) + Y by A26, LMQ09 ;
then A29: ||.(a * v).|| = lower_bound (NormVSets (X,Y,(a * vv1))) by A3, DeNorm;
for r being ExtReal st r in NormVSets (X,Y,(a * vv1)) holds
|.a.| * ||.v.|| <= r
proof
let r be ExtReal; :: thesis: ( r in NormVSets (X,Y,(a * vv1)) implies |.a.| * ||.v.|| <= r )
assume r in NormVSets (X,Y,(a * vv1)) ; :: thesis: |.a.| * ||.v.|| <= r
then consider x being VECTOR of X such that
A30: ( r = ||.x.|| & x in (a * vv1) + Y ) ;
consider y being VECTOR of X such that
A31: ( x = (a * vv1) + y & y in Y ) by A30;
A32: (a * vv1) + y = (a * vv1) + (1 * y) by RLVECT_1:def 8
.= (a * vv1) + ((a * (1 / a)) * y) by A24, XCMPLX_1:106
.= (a * vv1) + (a * ((1 / a) * y)) by RLVECT_1:def 7
.= a * (vv1 + ((1 / a) * y)) by RLVECT_1:def 5 ;
A33: (1 / a) * y in Y by A31, RLSUB_1:21;
A34: ||.((a * vv1) + y).|| = |.a.| * ||.(vv1 + ((1 / a) * y)).|| by A32, NORMSP_1:def 1;
vv1 + ((1 / a) * y) in vv1 + Y by A33;
then ||.(vv1 + ((1 / a) * y)).|| in NormVSets (X,Y,vv1) ;
then ||.v.|| <= ||.(vv1 + ((1 / a) * y)).|| by A27, SEQ_4:def 2;
hence |.a.| * ||.v.|| <= r by A25, A30, A31, A34, XREAL_1:64; :: thesis: verum
end;
then |.a.| * ||.v.|| is LowerBound of NormVSets (X,Y,(a * vv1)) by XXREAL_2:def 2;
then A36: |.a.| * ||.v.|| <= ||.(a * v).|| by A29, XXREAL_2:def 4;
for r being ExtReal st r in NormVSets (X,Y,vv1) holds
(1 / |.a.|) * ||.(a * v).|| <= r
proof
let r be ExtReal; :: thesis: ( r in NormVSets (X,Y,vv1) implies (1 / |.a.|) * ||.(a * v).|| <= r )
assume r in NormVSets (X,Y,vv1) ; :: thesis: (1 / |.a.|) * ||.(a * v).|| <= r
then consider x being VECTOR of X such that
A37: ( r = ||.x.|| & x in vv1 + Y ) ;
consider y being VECTOR of X such that
A38: ( x = vv1 + y & y in Y ) by A37;
A39: vv1 + y = 1 * (vv1 + y) by RLVECT_1:def 8
.= ((1 / a) * a) * (vv1 + y) by A24, XCMPLX_1:106
.= (1 / a) * (a * (vv1 + y)) by RLVECT_1:def 7
.= (1 / a) * ((a * vv1) + (a * y)) by RLVECT_1:def 5 ;
A40: a * y in Y by A38, RLSUB_1:21;
A41: ||.(vv1 + y).|| = |.(1 / a).| * ||.((a * vv1) + (a * y)).|| by A39, NORMSP_1:def 1;
(a * vv1) + (a * y) in (a * vv1) + Y by A40;
then ||.((a * vv1) + (a * y)).|| in NormVSets (X,Y,(a * vv1)) ;
then A42: ||.(a * v).|| <= ||.((a * vv1) + (a * y)).|| by A29, SEQ_4:def 2;
0 <= |.(1 / a).| by COMPLEX1:46;
then |.(1 / a).| * ||.(a * v).|| <= |.(1 / a).| * ||.((a * vv1) + (a * y)).|| by A42, XREAL_1:64;
hence (1 / |.a.|) * ||.(a * v).|| <= r by A37, A38, A41, COMPLEX1:80; :: thesis: verum
end;
then A43: (1 / |.a.|) * ||.(a * v).|| is LowerBound of NormVSets (X,Y,vv1) by XXREAL_2:def 2;
0 <= |.a.| by COMPLEX1:46;
then |.a.| * ((1 / |.a.|) * ||.(a * v).||) <= |.a.| * ||.v.|| by A27, A43, XREAL_1:64, XXREAL_2:def 4;
then (|.a.| * (1 / |.a.|)) * ||.(a * v).|| <= |.a.| * ||.v.|| ;
then 1 * ||.(a * v).|| <= |.a.| * ||.v.|| by A25, XCMPLX_1:106;
hence ||.(a * v).|| = |.a.| * ||.v.|| by A36, XXREAL_0:1; :: thesis: verum
end;
end;
end;
thus ||.(v + w).|| <= ||.v.|| + ||.w.|| :: thesis: verum
proof
consider vv1 being Point of X such that
A44: v1 = vv1 + Y by LMQ07;
A45: ||.v.|| = lower_bound (NormVSets (X,Y,vv1)) by A3, A44, DeNorm;
consider ww1 being Point of X such that
A46: w1 = ww1 + Y by LMQ07;
A47: ||.w.|| = lower_bound (NormVSets (X,Y,ww1)) by A3, A46, DeNorm;
v + w = v1 + w1
.= (vv1 + ww1) + Y by A44, A46, LMQ11 ;
then A49: ||.(v + w).|| = lower_bound (NormVSets (X,Y,(vv1 + ww1))) by A3, DeNorm;
A50: for y1, y2 being Point of X st y1 in Y & y2 in Y holds
||.(v + w).|| <= ||.(vv1 + y1).|| + ||.(ww1 + y2).||
proof
let y1, y2 be Point of X; :: thesis: ( y1 in Y & y2 in Y implies ||.(v + w).|| <= ||.(vv1 + y1).|| + ||.(ww1 + y2).|| )
assume ( y1 in Y & y2 in Y ) ; :: thesis: ||.(v + w).|| <= ||.(vv1 + y1).|| + ||.(ww1 + y2).||
then y1 + y2 in Y by RLSUB_1:20;
then (vv1 + ww1) + (y1 + y2) in (vv1 + ww1) + Y ;
then ||.((vv1 + ww1) + (y1 + y2)).|| in NormVSets (X,Y,(vv1 + ww1)) ;
then A51: lower_bound (NormVSets (X,Y,(vv1 + ww1))) <= ||.((vv1 + ww1) + (y1 + y2)).|| by SEQ_4:def 2;
||.((vv1 + ww1) + (y1 + y2)).|| = ||.(((vv1 + ww1) + y1) + y2).|| by RLVECT_1:def 3
.= ||.(((vv1 + y1) + ww1) + y2).|| by RLVECT_1:def 3
.= ||.((vv1 + y1) + (ww1 + y2)).|| by RLVECT_1:def 3 ;
then ||.((vv1 + ww1) + (y1 + y2)).|| <= ||.(vv1 + y1).|| + ||.(ww1 + y2).|| by NORMSP_1:def 1;
hence ||.(v + w).|| <= ||.(vv1 + y1).|| + ||.(ww1 + y2).|| by A49, A51, XXREAL_0:2; :: thesis: verum
end;
A52: for y1 being Point of X st y1 in Y holds
||.(v + w).|| - ||.w.|| <= ||.(vv1 + y1).||
proof
let y1 be Point of X; :: thesis: ( y1 in Y implies ||.(v + w).|| - ||.w.|| <= ||.(vv1 + y1).|| )
assume A53: y1 in Y ; :: thesis: ||.(v + w).|| - ||.w.|| <= ||.(vv1 + y1).||
A54: now :: thesis: for y2 being Point of X st y2 in Y holds
||.(v + w).|| - ||.(vv1 + y1).|| <= ||.(ww1 + y2).||
let y2 be Point of X; :: thesis: ( y2 in Y implies ||.(v + w).|| - ||.(vv1 + y1).|| <= ||.(ww1 + y2).|| )
assume y2 in Y ; :: thesis: ||.(v + w).|| - ||.(vv1 + y1).|| <= ||.(ww1 + y2).||
then ||.(v + w).|| - ||.(vv1 + y1).|| <= (||.(vv1 + y1).|| + ||.(ww1 + y2).||) - ||.(vv1 + y1).|| by A50, A53, XREAL_1:9;
hence ||.(v + w).|| - ||.(vv1 + y1).|| <= ||.(ww1 + y2).|| ; :: thesis: verum
end;
for r being ExtReal st r in NormVSets (X,Y,ww1) holds
||.(v + w).|| - ||.(vv1 + y1).|| <= r
proof
let r be ExtReal; :: thesis: ( r in NormVSets (X,Y,ww1) implies ||.(v + w).|| - ||.(vv1 + y1).|| <= r )
assume r in NormVSets (X,Y,ww1) ; :: thesis: ||.(v + w).|| - ||.(vv1 + y1).|| <= r
then consider x being VECTOR of X such that
A55: ( r = ||.x.|| & x in ww1 + Y ) ;
consider y2 being VECTOR of X such that
A56: ( x = ww1 + y2 & y2 in Y ) by A55;
thus ||.(v + w).|| - ||.(vv1 + y1).|| <= r by A54, A55, A56; :: thesis: verum
end;
then ||.(v + w).|| - ||.(vv1 + y1).|| is LowerBound of NormVSets (X,Y,ww1) by XXREAL_2:def 2;
then (||.(v + w).|| - ||.(vv1 + y1).||) + ||.(vv1 + y1).|| <= ||.w.|| + ||.(vv1 + y1).|| by A47, XREAL_1:6, XXREAL_2:def 4;
then ||.(v + w).|| - ||.w.|| <= (||.w.|| + ||.(vv1 + y1).||) - ||.w.|| by XREAL_1:9;
hence ||.(v + w).|| - ||.w.|| <= ||.(vv1 + y1).|| ; :: thesis: verum
end;
for r being ExtReal st r in NormVSets (X,Y,vv1) holds
||.(v + w).|| - ||.w.|| <= r
proof
let r be ExtReal; :: thesis: ( r in NormVSets (X,Y,vv1) implies ||.(v + w).|| - ||.w.|| <= r )
assume r in NormVSets (X,Y,vv1) ; :: thesis: ||.(v + w).|| - ||.w.|| <= r
then consider x being VECTOR of X such that
A58: ( r = ||.x.|| & x in vv1 + Y ) ;
consider y1 being VECTOR of X such that
A59: ( x = vv1 + y1 & y1 in Y ) by A58;
thus ||.(v + w).|| - ||.w.|| <= r by A52, A58, A59; :: thesis: verum
end;
then ||.(v + w).|| - ||.w.|| is LowerBound of NormVSets (X,Y,vv1) by XXREAL_2:def 2;
then (||.(v + w).|| - ||.w.||) + ||.w.|| <= ||.v.|| + ||.w.|| by A45, XREAL_1:6, XXREAL_2:def 4;
hence ||.(v + w).|| <= ||.v.|| + ||.w.|| ; :: thesis: verum
end;
end;
then T is RealNormSpace-like ;
then reconsider T = T as strict RealNormSpace by A4, A5, A6, A7, A8, A9, A10, A11, A15, A22;
take T ; :: thesis: ( RLSStruct(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T #) = VectQuot (X,Y) & the normF of T = NormCoset (X,Y) )
thus ( RLSStruct(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T #) = VectQuot (X,Y) & the normF of T = NormCoset (X,Y) ) ; :: thesis: verum