let V be non empty VectSp of F_Complex ; :: thesis: for p being Semi-Norm of V
for M being Subspace of V
for l being linear-Functional of M st ( for e being Vector of M
for v being Vector of V st v = e holds
|.(l . e).| <= p . v ) holds
ex L being linear-Functional of V st
( L | the carrier of M = l & ( for e being Vector of V holds |.(L . e).| <= p . e ) )
let p be Semi-Norm of V; :: thesis: for M being Subspace of V
for l being linear-Functional of M st ( for e being Vector of M
for v being Vector of V st v = e holds
|.(l . e).| <= p . v ) holds
ex L being linear-Functional of V st
( L | the carrier of M = l & ( for e being Vector of V holds |.(L . e).| <= p . e ) )
let M be Subspace of V; :: thesis: for l being linear-Functional of M st ( for e being Vector of M
for v being Vector of V st v = e holds
|.(l . e).| <= p . v ) holds
ex L being linear-Functional of V st
( L | the carrier of M = l & ( for e being Vector of V holds |.(L . e).| <= p . e ) )
let l be linear-Functional of M; :: thesis: ( ( for e being Vector of M
for v being Vector of V st v = e holds
|.(l . e).| <= p . v ) implies ex L being linear-Functional of V st
( L | the carrier of M = l & ( for e being Vector of V holds |.(L . e).| <= p . e ) ) )
assume A1:
for e being Vector of M
for v being Vector of V st v = e holds
|.(l . e).| <= p . v
; :: thesis: ex L being linear-Functional of V st
( L | the carrier of M = l & ( for e being Vector of V holds |.(L . e).| <= p . e ) )
reconsider RVSM = RealVS M as Subspace of RealVS V by Th30;
reconsider p1 = p as Banach-Functional of (RealVS V) by Th32;
reconsider prRl = projRe l as linear-Functional of RVSM by Th33;
A2:
addLoopStr(# the carrier of V,the addF of V,the U2 of V #) = addLoopStr(# the carrier of (RealVS V),the addF of (RealVS V),the U2 of (RealVS V) #)
by Def22;
A3:
addLoopStr(# the carrier of M,the addF of M,the U2 of M #) = addLoopStr(# the carrier of (RealVS M),the addF of (RealVS M),the U2 of (RealVS M) #)
by Def22;
for x being VECTOR of RVSM
for v being VECTOR of (RealVS V) st x = v holds
prRl . x <= p1 . v
then consider L1 being linear-Functional of (RealVS V) such that
A5:
L1 | the carrier of RVSM = prRl
and
A6:
for e being VECTOR of (RealVS V) holds L1 . e <= p1 . e
by HAHNBAN:35;
reconsider L = prodReIm L1 as linear-Functional of V by Th35;
take
L
; :: thesis: ( L | the carrier of M = l & ( for e being Vector of V holds |.(L . e).| <= p . e ) )
reconsider tcM = the carrier of M as Subset of V by VECTSP_4:def 2;
now let x be
Element of
M;
:: thesis: (L | tcM) . x = l . x
the
carrier of
M c= the
carrier of
V
by VECTSP_4:def 2;
then reconsider x2 =
x as
Element of
V by TARSKI:def 3;
reconsider x1 =
x2,
ix1 =
i_FC * x2 as
Element of
(RealVS V) by A2;
A7:
L1 . x1 =
(projRe l) . x1
by A3, A5, FUNCT_1:72
.=
Re (l . x)
by Def23
;
reconsider lx =
l . x as
Element of
COMPLEX by COMPLFLD:def 1;
lx = (Re lx) + ((Im lx) * <i> )
by COMPLEX1:29;
then A9:
i_FC * (l . x) = ((0 * (Re lx)) - (1 * (Im lx))) + (((0 * (Im lx)) + (1 * (Re lx))) * <i> )
;
A11:
i_FC * x = i_FC * x2
by VECTSP_4:22;
then A12:
L1 . ix1 =
(projRe l) . ix1
by A3, A5, FUNCT_1:72
.=
Re (l . (i_FC * x))
by A11, Def23
.=
Re ((- (Im lx)) + ((Re lx) * <i> ))
by A9, Def12
.=
- (Im (l . x))
by COMPLEX1:28
;
thus (L | tcM) . x =
L . x
by FUNCT_1:72
.=
[**((RtoC L1) . x2),(- ((i-shift (RtoC L1)) . x2))**]
by Def28
.=
[**(Re (l . x)),(- ((RtoC L1) . (i_FC * x2)))**]
by A7, Def27
.=
l . x
by A12, COMPLEX1:29
;
:: thesis: verum end;
hence
L | the carrier of M = l
by FUNCT_2:113; :: thesis: for e being Vector of V holds |.(L . e).| <= p . e
let e be Vector of V; :: thesis: |.(L . e).| <= p . e
reconsider Le = L . e as Element of COMPLEX by COMPLFLD:def 1;
reconsider Ledz = (Le *' ) / |.Le.| as Element of F_Complex by COMPLFLD:def 1;
reconsider e1 = e, Ledze = Ledz * e as VECTOR of (RealVS V) by A2;