let V be VectSp of F_Complex ; 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; 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 ) )
reconsider p1 = p as Banach-Functional of (RealVS V) by Th22;
let M be 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 ) )
reconsider tcM = the carrier of M as Subset of V by VECTSP_4:def 2;
reconsider RVSM = RealVS M as Subspace of RealVS V by Th20;
let l be linear-Functional of M; ( ( 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 ) ) )
reconsider prRl = projRe l as linear-Functional of RVSM by Th23;
A1:
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #)
by Def17;
A2:
addLoopStr(# the carrier of M, the addF of M, the ZeroF of M #) = addLoopStr(# the carrier of (RealVS M), the addF of (RealVS M), the ZeroF of (RealVS M) #)
by Def17;
assume A3:
for e being Vector of M
for v being Vector of V st v = e holds
|.(l . e).| <= p . v
; 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 ) )
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:22;
reconsider L = prodReIm L1 as linear-Functional of V by Th25;
take
L
; ( L | the carrier of M = l & ( for e being Vector of V holds |.(L . e).| <= p . e ) )
now for x being Element of M holds (L | tcM) . x = l . xlet x be
Element of
M;
(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 ;
reconsider x1 =
x2,
ix1 =
i_FC * x2 as
Element of
(RealVS V) by A1;
reconsider lx =
l . x as
Element of
COMPLEX by COMPLFLD:def 1;
lx = (Re lx) + ((Im lx) * <i>)
by COMPLEX1:13;
then A7:
i_FC * (l . x) = ((0 * (Re lx)) - (1 * (Im lx))) + (((0 * (Im lx)) + (1 * (Re lx))) * <i>)
;
A8:
i_FC * x = i_FC * x2
by VECTSP_4:14;
then A9:
L1 . ix1 =
(projRe l) . ix1
by A2, A5, FUNCT_1:49
.=
Re (l . (i_FC * x))
by A8, Def18
.=
Re ((- (Im lx)) + ((Re lx) * <i>))
by A7, Def8
.=
- (Im (l . x))
by COMPLEX1:12
;
A10:
L1 . x1 =
(projRe l) . x1
by A2, A5, FUNCT_1:49
.=
Re (l . x)
by Def18
;
thus (L | tcM) . x =
L . x
by FUNCT_1:49
.=
[**((RtoC L1) . x2),(- ((i-shift (RtoC L1)) . x2))**]
by Def23
.=
[**(Re (l . x)),(- ((RtoC L1) . (i_FC * x2)))**]
by A10, Def22
.=
l . x
by A9, COMPLEX1:13
;
verum end;
hence
L | the carrier of M = l
by FUNCT_2:63; for e being Vector of V holds |.(L . e).| <= p . e
let e be Vector of V; |.(L . e).| <= p . e
reconsider Le = L . e as Element of COMPLEX by COMPLFLD:def 1;
(Le *') / |.Le.| in COMPLEX
by XCMPLX_0:def 2;
then 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 A1;