let V be RealLinearSpace; :: thesis: for X being Subspace of V
for q being Banach-Functional of V
for fi being linear-Functional of X st ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
fi . x <= q . v ) holds
ex psi being linear-Functional of V st
( psi | the carrier of X = fi & ( for x being VECTOR of V holds psi . x <= q . x ) )
let X be Subspace of V; :: thesis: for q being Banach-Functional of V
for fi being linear-Functional of X st ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
fi . x <= q . v ) holds
ex psi being linear-Functional of V st
( psi | the carrier of X = fi & ( for x being VECTOR of V holds psi . x <= q . x ) )
let q be Banach-Functional of V; :: thesis: for fi being linear-Functional of X st ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
fi . x <= q . v ) holds
ex psi being linear-Functional of V st
( psi | the carrier of X = fi & ( for x being VECTOR of V holds psi . x <= q . x ) )
let fi be linear-Functional of X; :: thesis: ( ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
fi . x <= q . v ) implies ex psi being linear-Functional of V st
( psi | the carrier of X = fi & ( for x being VECTOR of V holds psi . x <= q . x ) ) )
assume A1:
for x being VECTOR of X
for v being VECTOR of V st x = v holds
fi . x <= q . v
; :: thesis: ex psi being linear-Functional of V st
( psi | the carrier of X = fi & ( for x being VECTOR of V holds psi . x <= q . x ) )
defpred S1[ Element of PFuncs the carrier of V,REAL ] means ex Y being Subspace of V st
( the carrier of X c= the carrier of Y & $1 | the carrier of X = fi & ex f' being linear-Functional of Y st
( $1 = f' & ( for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f' . y <= q . v ) ) );
reconsider A = { f where f is Element of PFuncs the carrier of V,REAL : S1[f] } as Subset of (PFuncs the carrier of V,REAL ) from DOMAIN_1:sch 7();
the carrier of X c= the carrier of V
by RLSUB_1:def 2;
then
( fi in PFuncs the carrier of X,REAL & PFuncs the carrier of X,REAL c= PFuncs the carrier of V,REAL )
by PARTFUN1:119, PARTFUN1:128;
then reconsider fi' = fi as Element of PFuncs the carrier of V,REAL ;
fi' | the carrier of X = fi
by RELSET_1:34;
then
fi in A
by A1;
then reconsider A = A as non empty Subset of (PFuncs the carrier of V,REAL ) ;
defpred S2[ set , set ] means $1 c= $2;
A2:
for x being Element of A holds S2[x,x]
;
A3:
for x, y being Element of A st S2[x,y] & S2[y,x] holds
x = y
by XBOOLE_0:def 10;
A4:
for x, y, z being Element of A st S2[x,y] & S2[y,z] holds
S2[x,z]
by XBOOLE_1:1;
A5:
now let B be
set ;
:: thesis: ( B c= A & ( for x, y being Element of A st x in B & y in B & not S2[x,y] holds
S2[y,x] ) implies ex u being Element of A st
for x being Element of A st b3 in u holds
S2[b3,x] )assume that A6:
B c= A
and A7:
for
x,
y being
Element of
A st
x in B &
y in B & not
S2[
x,
y] holds
S2[
y,
x]
;
:: thesis: ex u being Element of A st
for x being Element of A st b3 in u holds
S2[b3,x]per cases
( B = {} or B <> {} )
;
suppose A9:
B <> {}
;
:: thesis: ex u being Element of A st
for x being Element of A st b3 in u holds
S2[b3,x]A10:
B is
Subset of
(PFuncs the carrier of V,REAL )
by A6, XBOOLE_1:1;
then reconsider E =
B as
functional non
empty set by A9;
B is
c=-linear
then reconsider u =
union B as
Element of
PFuncs the
carrier of
V,
REAL by A10, Th13;
consider t being
Element of
B;
t in A
by A6, A9, TARSKI:def 3;
then consider Y being
Subspace of
V,
f' being
linear-Functional of
Y such that A19:
t = f'
and
( the
carrier of
X c= the
carrier of
Y &
f' | the
carrier of
X = fi & ( for
y being
VECTOR of
Y for
v being
VECTOR of
V st
y = v holds
f' . y <= q . v ) )
by A11;
A20:
u <> {}
by A9, A19, XBOOLE_1:3, ZFMISC_1:92;
set K =
{ (dom g) where g is Element of E : verum } ;
A21:
dom u = union { (dom g) where g is Element of E : verum }
by Th5;
then reconsider D =
dom u as non
empty Subset of
V by A20, A21, RELAT_1:64, ZFMISC_1:94;
D is
linearly-closed
proof
hereby :: according to RLSUB_1:def 1 :: thesis: for b1 being Element of REAL
for b2 being Element of the carrier of V holds
( not b2 in D or b1 * b2 in D )
let v,
u be
Element of
V;
:: thesis: ( v in D & u in D implies v + u in D )assume A24:
(
v in D &
u in D )
;
:: thesis: v + u in Dthen consider D1 being
set such that A25:
(
v in D1 &
D1 in { (dom g) where g is Element of E : verum } )
by A21, TARSKI:def 4;
consider g1 being
Element of
E such that A26:
D1 = dom g1
by A25;
consider D2 being
set such that A27:
(
u in D2 &
D2 in { (dom g) where g is Element of E : verum } )
by A21, A24, TARSKI:def 4;
consider g2 being
Element of
E such that A28:
D2 = dom g2
by A27;
(
g1 in A &
g2 in A )
by A6, TARSKI:def 3;
then
(
g1 c= g2 or
g2 c= g1 )
by A7;
then consider g being
Element of
E such that A29:
(
g1 c= g &
g2 c= g )
;
A30:
(
D1 c= dom g &
D2 c= dom g )
by A26, A28, A29, RELAT_1:25;
g in A
by A6, TARSKI:def 3;
then consider Y being
Subspace of
V,
f' being
linear-Functional of
Y such that A31:
g = f'
and
( the
carrier of
X c= the
carrier of
Y &
f' | the
carrier of
X = fi & ( for
y being
VECTOR of
Y for
v being
VECTOR of
V st
y = v holds
f' . y <= q . v ) )
by A11;
A32:
dom g = the
carrier of
Y
by A31, FUNCT_2:def 1;
then
(
v in Y &
u in Y )
by A25, A27, A30, STRUCT_0:def 5;
then
v + u in Y
by RLSUB_1:28;
then
(
v + u in dom g &
dom g in { (dom g) where g is Element of E : verum } )
by A32, STRUCT_0:def 5;
hence
v + u in D
by A21, TARSKI:def 4;
:: thesis: verum
end;
let a be
Real;
:: thesis: for b1 being Element of the carrier of V holds
( not b1 in D or a * b1 in D )let v be
Element of
V;
:: thesis: ( not v in D or a * v in D )
assume
v in D
;
:: thesis: a * v in D
then consider D1 being
set such that A33:
(
v in D1 &
D1 in { (dom g) where g is Element of E : verum } )
by A21, TARSKI:def 4;
consider g being
Element of
E such that A34:
D1 = dom g
by A33;
g in A
by A6, TARSKI:def 3;
then consider Y being
Subspace of
V,
f' being
linear-Functional of
Y such that A35:
g = f'
and
( the
carrier of
X c= the
carrier of
Y &
f' | the
carrier of
X = fi & ( for
y being
VECTOR of
Y for
v being
VECTOR of
V st
y = v holds
f' . y <= q . v ) )
by A11;
A36:
dom g = the
carrier of
Y
by A35, FUNCT_2:def 1;
then
v in Y
by A33, A34, STRUCT_0:def 5;
then
a * v in Y
by RLSUB_1:29;
then
(
a * v in dom g &
dom g in { (dom g) where g is Element of E : verum } )
by A36, STRUCT_0:def 5;
hence
a * v in D
by A21, TARSKI:def 4;
:: thesis: verum
end; then consider Y being
strict Subspace of
V such that A37:
the
carrier of
Y = dom u
by RLSUB_1:43;
consider t being
Element of
dom u;
consider XX being
set such that A38:
(
t in XX &
XX in { (dom g) where g is Element of E : verum } )
by A21, A37, TARSKI:def 4;
consider gg being
Element of
E such that A39:
XX = dom gg
by A38;
gg in A
by A6, TARSKI:def 3;
then consider YY being
Subspace of
V,
ff being
linear-Functional of
YY such that A40:
gg = ff
and A41:
the
carrier of
X c= the
carrier of
YY
and A42:
ff | the
carrier of
X = fi
and
for
y being
VECTOR of
YY for
v being
VECTOR of
V st
y = v holds
ff . y <= q . v
by A11;
A43:
XX = the
carrier of
YY
by A39, A40, FUNCT_2:def 1;
XX c= dom u
by A21, A38, ZFMISC_1:92;
then A44:
the
carrier of
X c= the
carrier of
Y
by A37, A41, A43, XBOOLE_1:1;
the
carrier of
X c= dom ff
by A41, FUNCT_2:def 1;
then A45:
u | the
carrier of
X = fi
by A40, A42, GRFUNC_1:88, ZFMISC_1:92;
ex
f being
Function st
(
u = f &
dom f c= the
carrier of
V &
rng f c= REAL )
by PARTFUN1:def 5;
then reconsider f' =
u as
Function of the
carrier of
Y,
REAL by A37, FUNCT_2:def 1, RELSET_1:11;
reconsider f' =
f' as
Functional of
Y ;
A46:
f' is
additive
proof
let x,
y be
VECTOR of
Y;
:: according to HAHNBAN:def 4 :: thesis: f' . (x + y) = (f' . x) + (f' . y)
consider XXx being
set such that A47:
(
x in XXx &
XXx in { (dom g) where g is Element of E : verum } )
by A21, A37, TARSKI:def 4;
consider ggx being
Element of
E such that A48:
XXx = dom ggx
by A47;
A49:
ggx in A
by A6, TARSKI:def 3;
consider XXy being
set such that A50:
(
y in XXy &
XXy in { (dom g) where g is Element of E : verum } )
by A21, A37, TARSKI:def 4;
consider ggy being
Element of
E such that A51:
XXy = dom ggy
by A50;
ggy in A
by A6, TARSKI:def 3;
then
(
ggx c= ggy or
ggy c= ggx )
by A7, A49;
then consider gg being
Element of
E such that A52:
(
gg = ggx or
gg = ggy )
and A53:
(
ggx c= gg &
ggy c= gg )
;
gg in A
by A6, TARSKI:def 3;
then consider YY being
Subspace of
V,
ff being
linear-Functional of
YY such that A54:
gg = ff
and
( the
carrier of
X c= the
carrier of
YY &
ff | the
carrier of
X = fi & ( for
y being
VECTOR of
YY for
v being
VECTOR of
V st
y = v holds
ff . y <= q . v ) )
by A11;
A55:
dom ff = the
carrier of
YY
by FUNCT_2:def 1;
(
dom ggx c= dom gg &
dom ggy c= dom gg )
by A53, RELAT_1:25;
then reconsider x' =
x,
y' =
y as
VECTOR of
YY by A47, A48, A50, A51, A54, FUNCT_2:def 1;
A56:
ff c= f'
by A54, ZFMISC_1:92;
YY is
Subspace of
Y
by A21, A37, A47, A48, A50, A51, A52, A54, A55, RLSUB_1:36, ZFMISC_1:92;
then
x + y = x' + y'
by RLSUB_1:21;
hence f' . (x + y) =
ff . (x' + y')
by A55, A56, GRFUNC_1:8
.=
(ff . x') + (ff . y')
by Def4
.=
(f' . x) + (ff . y')
by A55, A56, GRFUNC_1:8
.=
(f' . x) + (f' . y)
by A55, A56, GRFUNC_1:8
;
:: thesis: verum
end;
f' is
homogeneous
proof
let x be
VECTOR of
Y;
:: according to HAHNBAN:def 5 :: thesis: for r being Real holds f' . (r * x) = r * (f' . x)let r be
Real;
:: thesis: f' . (r * x) = r * (f' . x)
consider XX being
set such that A57:
(
x in XX &
XX in { (dom g) where g is Element of E : verum } )
by A21, A37, TARSKI:def 4;
consider gg being
Element of
E such that A58:
XX = dom gg
by A57;
gg in A
by A6, TARSKI:def 3;
then consider YY being
Subspace of
V,
ff being
linear-Functional of
YY such that A59:
gg = ff
and
the
carrier of
X c= the
carrier of
YY
and
ff | the
carrier of
X = fi
and
for
y being
VECTOR of
YY for
v being
VECTOR of
V st
y = v holds
ff . y <= q . v
by A11;
A60:
dom ff = the
carrier of
YY
by FUNCT_2:def 1;
reconsider x' =
x as
VECTOR of
YY by A57, A58, A59, FUNCT_2:def 1;
A61:
ff c= f'
by A59, ZFMISC_1:92;
YY is
Subspace of
Y
by A21, A37, A57, A58, A59, A60, RLSUB_1:36, ZFMISC_1:92;
then
r * x = r * x'
by RLSUB_1:22;
hence f' . (r * x) =
ff . (r * x')
by A60, A61, GRFUNC_1:8
.=
r * (ff . x')
by Def5
.=
r * (f' . x)
by A60, A61, GRFUNC_1:8
;
:: thesis: verum
end; then reconsider f' =
f' as
linear-Functional of
Y by A46;
now let y be
VECTOR of
Y;
:: thesis: for v being VECTOR of V st y = v holds
f' . y <= q . vlet v be
VECTOR of
V;
:: thesis: ( y = v implies f' . y <= q . v )assume A62:
y = v
;
:: thesis: f' . y <= q . vconsider XX being
set such that A63:
(
y in XX &
XX in { (dom g) where g is Element of E : verum } )
by A21, A37, TARSKI:def 4;
consider gg being
Element of
E such that A64:
XX = dom gg
by A63;
gg in A
by A6, TARSKI:def 3;
then consider YY being
Subspace of
V,
ff being
linear-Functional of
YY such that A65:
gg = ff
and
the
carrier of
X c= the
carrier of
YY
and
ff | the
carrier of
X = fi
and A66:
for
y being
VECTOR of
YY for
v being
VECTOR of
V st
y = v holds
ff . y <= q . v
by A11;
A67:
dom ff = the
carrier of
YY
by FUNCT_2:def 1;
reconsider y' =
y as
VECTOR of
YY by A63, A64, A65, FUNCT_2:def 1;
A68:
ff c= f'
by A65, ZFMISC_1:92;
ff . y' <= q . v
by A62, A66;
hence
f' . y <= q . v
by A67, A68, GRFUNC_1:8;
:: thesis: verum end; then
u in A
by A44, A45;
then reconsider u =
u as
Element of
A ;
take u =
u;
:: thesis: for x being Element of A st x in B holds
S2[x,u]let x be
Element of
A;
:: thesis: ( x in B implies S2[x,u] )assume
x in B
;
:: thesis: S2[x,u]hence
S2[
x,
u]
by ZFMISC_1:92;
:: thesis: verum end; end;
consider psi being Element of A such that
A69:
for chi being Element of A st psi <> chi holds
not S2[psi,chi]
from ORDERS_1:sch 1(A2, A3, A4, A5);
psi in A
;
then consider f being Element of PFuncs the carrier of V,REAL such that
A70:
f = psi
and
A71:
ex Y being Subspace of V st
( the carrier of X c= the carrier of Y & f | the carrier of X = fi & ex f' being linear-Functional of Y st
( f = f' & ( for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f' . y <= q . v ) ) )
;
consider Y being Subspace of V such that
A72:
the carrier of X c= the carrier of Y
and
A73:
f | the carrier of X = fi
and
A74:
ex f' being linear-Functional of Y st
( f = f' & ( for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f' . y <= q . v ) )
by A71;
consider f' being linear-Functional of Y such that
A75:
f = f'
and
A76:
for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f' . y <= q . v
by A74;
reconsider RLSY = RLSStruct(# the carrier of Y,the U2 of Y,the addF of Y,the Mult of Y #) as RealLinearSpace by Lm2;
reconsider ggh = f' as linear-Functional of RLSY by Lm5;
A77:
f = ggh
by A75;
reconsider RLS = RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) as RealLinearSpace by Lm2;
A78:
RLSY is Subspace of RLS
by Lm3;
A79:
now assume
RLSStruct(# the
carrier of
Y,the
U2 of
Y,the
addF of
Y,the
Mult of
Y #)
<> RLSStruct(# the
carrier of
V,the
U2 of
V,the
addF of
V,the
Mult of
V #)
;
:: thesis: contradictionthen
( the
carrier of
Y <> the
carrier of
V & the
carrier of
Y c= the
carrier of
V )
by A78, RLSUB_1:40, RLSUB_1:def 2;
then
the
carrier of
Y c< the
carrier of
V
by XBOOLE_0:def 8;
then consider v being
set such that A80:
(
v in the
carrier of
V & not
v in the
carrier of
Y )
by XBOOLE_0:6;
reconsider v =
v as
VECTOR of
V by A80;
consider phi being
linear-Functional of
(Y + (Lin {v})) such that A81:
phi | the
carrier of
Y = f'
and A82:
for
x being
VECTOR of
(Y + (Lin {v})) for
v being
VECTOR of
V st
x = v holds
phi . x <= q . v
by A76, A80, Lm1;
A83:
dom phi = the
carrier of
(Y + (Lin {v}))
by FUNCT_2:def 1;
the
carrier of
Y c= the
carrier of
(Y + (Lin {v}))
by Th14;
then A84:
the
carrier of
X c= the
carrier of
(Y + (Lin {v}))
by A72, XBOOLE_1:1;
A85:
dom phi c= the
carrier of
V
by A83, RLSUB_1:def 2;
rng phi c= REAL
by RELAT_1:def 19;
then reconsider phi =
phi as
Element of
PFuncs the
carrier of
V,
REAL by A85, PARTFUN1:def 5;
the
carrier of
Y /\ the
carrier of
X = the
carrier of
X
by A72, XBOOLE_1:28;
then
phi | the
carrier of
X = fi
by A73, A75, A81, RELAT_1:100;
then
phi in A
by A82, A84;
then reconsider phi =
phi as
Element of
A ;
A86:
dom f' = the
carrier of
Y
by FUNCT_2:def 1;
A87:
the
carrier of
(Lin {v}) c= the
carrier of
((Lin {v}) + Y)
by Th14;
v in Lin {v}
by RLVECT_4:12;
then
v in the
carrier of
(Lin {v})
by STRUCT_0:def 5;
then
v in the
carrier of
((Lin {v}) + Y)
by A87;
then
phi <> psi
by A70, A75, A80, A83, A86, RLSUB_2:9;
hence
contradiction
by A69, A70, A75, A81, RELAT_1:88;
:: thesis: verum end;
then reconsider psi = psi as linear-Functional of V by A70, A77, Lm4;
take
psi
; :: thesis: ( psi | the carrier of X = fi & ( for x being VECTOR of V holds psi . x <= q . x ) )
thus
psi | the carrier of X = fi
by A70, A73; :: thesis: for x being VECTOR of V holds psi . x <= q . x
let x be VECTOR of V; :: thesis: psi . x <= q . x
thus
psi . x <= q . x
by A70, A74, A79; :: thesis: verum