let X, Y be RealNormSpace; :: thesis: for L being Lipschitzian LinearOperator of X,Y
for y being Lipschitzian linear-Functional of Y holds y * L is Lipschitzian linear-Functional of X
let L be Lipschitzian LinearOperator of X,Y; :: thesis: for y being Lipschitzian linear-Functional of Y holds y * L is Lipschitzian linear-Functional of X
let y be Lipschitzian linear-Functional of Y; :: thesis: y * L is Lipschitzian linear-Functional of X
consider M being Real such that
AS1: ( 0 <= M & ( for x being VECTOR of X holds ||.(L . x).|| <= M * ||.x.|| ) ) by LOPBAN_1:def 8;
D1: dom L = the carrier of X by FUNCT_2:def 1;
set x = y * L;
P6: for v, w being VECTOR of X holds (y * L) . (v + w) = ((y * L) . v) + ((y * L) . w)
proof
let v, w be VECTOR of X; :: thesis: (y * L) . (v + w) = ((y * L) . v) + ((y * L) . w)
thus (y * L) . (v + w) = y . (L . (v + w)) by D1, FUNCT_1:13
.= y . ((L . v) + (L . w)) by VECTSP_1:def 20
.= (y . (L . v)) + (y . (L . w)) by HAHNBAN:def 2
.= ((y * L) . v) + (y . (L . w)) by D1, FUNCT_1:13
.= ((y * L) . v) + ((y * L) . w) by D1, FUNCT_1:13 ; :: thesis: verum
end;
for v being VECTOR of X
for r being Real holds (y * L) . (r * v) = r * ((y * L) . v)
proof
let v be VECTOR of X; :: thesis: for r being Real holds (y * L) . (r * v) = r * ((y * L) . v)
let r be Real; :: thesis: (y * L) . (r * v) = r * ((y * L) . v)
thus (y * L) . (r * v) = y . (L . (r * v)) by D1, FUNCT_1:13
.= y . (r * (L . v)) by LOPBAN_1:def 5
.= r * (y . (L . v)) by HAHNBAN:def 3
.= r * ((y * L) . v) by D1, FUNCT_1:13 ; :: thesis: verum
end;
then reconsider x = y * L as linear-Functional of X by P6, HAHNBAN:def 2, HAHNBAN:def 3;
consider N being Real such that
P7: ( 0 <= N & ( for v being VECTOR of Y holds |.(y . v).| <= N * ||.v.|| ) ) by DUALSP01:def 9;
for v being VECTOR of X holds |.(x . v).| <= (M * N) * ||.v.||
proof
let v be VECTOR of X; :: thesis: |.(x . v).| <= (M * N) * ||.v.||
P8: |.(x . v).| = |.(y . (L . v)).| by D1, FUNCT_1:13;
P9: |.(y . (L . v)).| <= N * ||.(L . v).|| by P7;
N * ||.(L . v).|| <= N * (M * ||.v.||) by AS1, P7, XREAL_1:64;
hence |.(x . v).| <= (M * N) * ||.v.|| by P8, P9, XXREAL_0:2; :: thesis: verum
end;
hence y * L is Lipschitzian linear-Functional of X by DUALSP01:def 9, AS1, P7; :: thesis: verum