let V be RealLinearSpace; 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; 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; 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; ( ( 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 ) ) )
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:45, PARTFUN1:50;
then reconsider fi9 = fi as Element of PFuncs ( the carrier of V,REAL) ;
reconsider RLS = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) as RealLinearSpace by Lm2;
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 f9 being linear-Functional of Y st
( $1 = f9 & ( for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f9 . 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();
A1:
fi9 | the carrier of X = fi
;
assume
for x being VECTOR of X
for v being VECTOR of V st x = v holds
fi . x <= q . v
; 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 ) )
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, y being Element of A st S2[x,y] & S2[y,x] holds
x = y
;
A3:
for x, y, z being Element of A st S2[x,y] & S2[y,z] holds
S2[x,z]
by XBOOLE_1:1;
A4:
now for B being set st 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] ) holds
ex u being Element of A st
for x being Element of A st x in B holds
S2[x,u]let B be
set ;
( 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 A5:
B c= A
and A6:
for
x,
y being
Element of
A st
x in B &
y in B & not
S2[
x,
y] holds
S2[
y,
x]
;
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 A8:
B <> {}
;
ex u being Element of A st
for x being Element of A st b3 in u holds
S2[b3,x]A9:
B is
c=-linear
B is
Subset of
(PFuncs ( the carrier of V,REAL))
by A5, XBOOLE_1:1;
then reconsider u =
union B as
Element of
PFuncs ( the
carrier of
V,
REAL)
by A9, TREES_2:40;
reconsider E =
B as
functional non
empty set by A5, A8;
set t = the
Element of
B;
set K =
{ (dom g) where g is Element of E : verum } ;
A10:
dom u = union { (dom g) where g is Element of E : verum }
by FUNCT_1:110;
the
Element of
B in A
by A5, A8;
then
ex
Y being
Subspace of
V ex
f9 being
linear-Functional of
Y st
( the
Element of
B = f9 & the
carrier of
X c= the
carrier of
Y &
f9 | the
carrier of
X = fi & ( for
y being
VECTOR of
Y for
v being
VECTOR of
V st
y = v holds
f9 . y <= q . v ) )
by A11;
then
u <> {}
by A8, XBOOLE_1:3, ZFMISC_1:74;
then reconsider D =
dom u as non
empty Subset of
V by A10, A19, ZFMISC_1:76;
D is
linearly-closed
proof
hereby RLSUB_1:def 1 for b1 being object
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;
( v in D & u in D implies v + u in D )assume that A22:
v in D
and A23:
u in D
;
v + u in Dconsider D1 being
set such that A24:
v in D1
and A25:
D1 in { (dom g) where g is Element of E : verum }
by A10, A22, 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
and A28:
D2 in { (dom g) where g is Element of E : verum }
by A10, A23, TARSKI:def 4;
consider g2 being
Element of
E such that A29:
D2 = dom g2
by A28;
(
g1 in A &
g2 in A )
by A5;
then
(
g1 c= g2 or
g2 c= g1 )
by A6;
then consider g being
Element of
E such that A30:
g1 c= g
and A31:
g2 c= g
;
g in A
by A5;
then consider Y being
Subspace of
V,
f9 being
linear-Functional of
Y such that A32:
g = f9
and
the
carrier of
X c= the
carrier of
Y
and
f9 | the
carrier of
X = fi
and
for
y being
VECTOR of
Y for
v being
VECTOR of
V st
y = v holds
f9 . y <= q . v
by A11;
A33:
dom g = the
carrier of
Y
by A32, FUNCT_2:def 1;
D2 c= dom g
by A29, A31, RELAT_1:11;
then A34:
u in Y
by A27, A33;
D1 c= dom g
by A26, A30, RELAT_1:11;
then
v in Y
by A24, A33;
then
v + u in Y
by A34, RLSUB_1:20;
then A35:
v + u in dom g
by A33;
dom g in { (dom g) where g is Element of E : verum }
;
hence
v + u in D
by A10, A35, TARSKI:def 4;
verum
end;
let a be
Real;
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;
( not v in D or a * v in D )
assume
v in D
;
a * v in D
then consider D1 being
set such that A36:
v in D1
and A37:
D1 in { (dom g) where g is Element of E : verum }
by A10, TARSKI:def 4;
consider g being
Element of
E such that A38:
D1 = dom g
by A37;
g in A
by A5;
then consider Y being
Subspace of
V,
f9 being
linear-Functional of
Y such that A39:
g = f9
and
the
carrier of
X c= the
carrier of
Y
and
f9 | the
carrier of
X = fi
and
for
y being
VECTOR of
Y for
v being
VECTOR of
V st
y = v holds
f9 . y <= q . v
by A11;
A40:
dom g = the
carrier of
Y
by A39, FUNCT_2:def 1;
then
v in Y
by A36, A38;
then
a * v in Y
by RLSUB_1:21;
then A41:
a * v in dom g
by A40;
dom g in { (dom g) where g is Element of E : verum }
;
hence
a * v in D
by A10, A41, TARSKI:def 4;
verum
end; then consider Y being
strict Subspace of
V such that A42:
the
carrier of
Y = dom u
by RLSUB_1:35;
set t = the
Element of
dom u;
consider XX being
set such that
the
Element of
dom u in XX
and A43:
XX in { (dom g) where g is Element of E : verum }
by A10, A42, TARSKI:def 4;
ex
f being
Function st
(
u = f &
dom f c= the
carrier of
V &
rng f c= REAL )
by PARTFUN1:def 3;
then reconsider f9 =
u as
Function of the
carrier of
Y,
REAL by A42, FUNCT_2:def 1, RELSET_1:4;
reconsider f9 =
f9 as
Functional of
Y ;
consider gg being
Element of
E such that A44:
XX = dom gg
by A43;
A45:
f9 is
additive
proof
let x,
y be
VECTOR of
Y;
HAHNBAN:def 2 f9 . (x + y) = (f9 . x) + (f9 . y)
consider XXx being
set such that A46:
x in XXx
and A47:
XXx in { (dom g) where g is Element of E : verum }
by A10, A42, TARSKI:def 4;
consider ggx being
Element of
E such that A48:
XXx = dom ggx
by A47;
consider XXy being
set such that A49:
y in XXy
and A50:
XXy in { (dom g) where g is Element of E : verum }
by A10, A42, TARSKI:def 4;
consider ggy being
Element of
E such that A51:
XXy = dom ggy
by A50;
(
ggx in A &
ggy in A )
by A5;
then
(
ggx c= ggy or
ggy c= ggx )
by A6;
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 A5;
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
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;
(
dom ggx c= dom gg &
dom ggy c= dom gg )
by A53, RELAT_1:11;
then reconsider x9 =
x,
y9 =
y as
VECTOR of
YY by A46, A48, A49, A51, A54, FUNCT_2:def 1;
A55:
ff c= f9
by A54, ZFMISC_1:74;
A56:
dom ff = the
carrier of
YY
by FUNCT_2:def 1;
then
YY is
Subspace of
Y
by A10, A42, A47, A48, A50, A51, A52, A54, RLSUB_1:28, ZFMISC_1:74;
then
x + y = x9 + y9
by RLSUB_1:13;
hence f9 . (x + y) =
ff . (x9 + y9)
by A56, A55, GRFUNC_1:2
.=
(ff . x9) + (ff . y9)
by Def2
.=
(f9 . x) + (ff . y9)
by A56, A55, GRFUNC_1:2
.=
(f9 . x) + (f9 . y)
by A56, A55, GRFUNC_1:2
;
verum
end;
f9 is
homogeneous
proof
let x be
VECTOR of
Y;
HAHNBAN:def 3 for r being Real holds f9 . (r * x) = r * (f9 . x)let r be
Real;
f9 . (r * x) = r * (f9 . x)
consider XX being
set such that A57:
x in XX
and A58:
XX in { (dom g) where g is Element of E : verum }
by A10, A42, TARSKI:def 4;
consider gg being
Element of
E such that A59:
XX = dom gg
by A58;
gg in A
by A5;
then consider YY being
Subspace of
V,
ff being
linear-Functional of
YY such that A60:
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;
reconsider x9 =
x as
VECTOR of
YY by A57, A59, A60, FUNCT_2:def 1;
A61:
ff c= f9
by A60, ZFMISC_1:74;
A62:
dom ff = the
carrier of
YY
by FUNCT_2:def 1;
then
YY is
Subspace of
Y
by A10, A42, A58, A59, A60, RLSUB_1:28, ZFMISC_1:74;
then
r * x = r * x9
by RLSUB_1:14;
hence f9 . (r * x) =
ff . (r * x9)
by A62, A61, GRFUNC_1:2
.=
r * (ff . x9)
by Def3
.=
r * (f9 . x)
by A62, A61, GRFUNC_1:2
;
verum
end; then reconsider f9 =
f9 as
linear-Functional of
Y by A45;
A63:
now for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f9 . y <= q . vlet y be
VECTOR of
Y;
for v being VECTOR of V st y = v holds
f9 . y <= q . vlet v be
VECTOR of
V;
( y = v implies f9 . y <= q . v )assume A64:
y = v
;
f9 . y <= q . vconsider XX being
set such that A65:
y in XX
and A66:
XX in { (dom g) where g is Element of E : verum }
by A10, A42, TARSKI:def 4;
consider gg being
Element of
E such that A67:
XX = dom gg
by A66;
gg in A
by A5;
then consider YY being
Subspace of
V,
ff being
linear-Functional of
YY such that A68:
gg = ff
and
the
carrier of
X c= the
carrier of
YY
and
ff | the
carrier of
X = fi
and A69:
for
y being
VECTOR of
YY for
v being
VECTOR of
V st
y = v holds
ff . y <= q . v
by A11;
reconsider y9 =
y as
VECTOR of
YY by A65, A67, A68, FUNCT_2:def 1;
A70:
(
dom ff = the
carrier of
YY &
ff c= f9 )
by A68, FUNCT_2:def 1, ZFMISC_1:74;
ff . y9 <= q . v
by A64, A69;
hence
f9 . y <= q . v
by A70, GRFUNC_1:2;
verum end;
gg in A
by A5;
then consider YY being
Subspace of
V,
ff being
linear-Functional of
YY such that A71:
gg = ff
and A72:
the
carrier of
X c= the
carrier of
YY
and A73:
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;
the
carrier of
X c= dom ff
by A72, FUNCT_2:def 1;
then A74:
u | the
carrier of
X = fi
by A71, A73, GRFUNC_1:27, ZFMISC_1:74;
A75:
XX c= dom u
by A10, A43, ZFMISC_1:74;
XX = the
carrier of
YY
by A44, A71, FUNCT_2:def 1;
then
the
carrier of
X c= the
carrier of
Y
by A42, A72, A75;
then
u in A
by A74, A63;
then reconsider u =
u as
Element of
A ;
take u =
u;
for x being Element of A st x in B holds
S2[x,u]let x be
Element of
A;
( x in B implies S2[x,u] )assume
x in B
;
S2[x,u]hence
S2[
x,
u]
by ZFMISC_1:74;
verum end; end;
A76:
for x being Element of A holds S2[x,x]
;
consider psi being Element of A such that
A77:
for chi being Element of A st psi <> chi holds
not S2[psi,chi]
from ORDERS_1:sch 1(A76, A2, A3, A4);
psi in A
;
then consider f being Element of PFuncs ( the carrier of V,REAL) such that
A78:
f = psi
and
A79:
ex Y being Subspace of V st
( the carrier of X c= the carrier of Y & f | the carrier of X = fi & ex f9 being linear-Functional of Y st
( f = f9 & ( for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f9 . y <= q . v ) ) )
;
consider Y being Subspace of V such that
A80:
the carrier of X c= the carrier of Y
and
A81:
f | the carrier of X = fi
and
A82:
ex f9 being linear-Functional of Y st
( f = f9 & ( for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f9 . y <= q . v ) )
by A79;
reconsider RLSY = RLSStruct(# the carrier of Y, the ZeroF of Y, the addF of Y, the Mult of Y #) as RealLinearSpace by Lm2;
consider f9 being linear-Functional of Y such that
A83:
f = f9
and
A84:
for y being VECTOR of Y
for v being VECTOR of V st y = v holds
f9 . y <= q . v
by A82;
A85:
RLSY is Subspace of RLS
by Lm3;
A86:
now not RLSStruct(# the carrier of Y, the ZeroF of Y, the addF of Y, the Mult of Y #) <> RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)assume
RLSStruct(# the
carrier of
Y, the
ZeroF of
Y, the
addF of
Y, the
Mult of
Y #)
<> RLSStruct(# the
carrier of
V, the
ZeroF of
V, the
addF of
V, the
Mult of
V #)
;
contradictionthen A87:
the
carrier of
Y <> the
carrier of
V
by A85, RLSUB_1:32;
the
carrier of
Y c= the
carrier of
V
by RLSUB_1:def 2;
then
the
carrier of
Y c< the
carrier of
V
by A87;
then consider v being
object such that A88:
v in the
carrier of
V
and A89:
not
v in the
carrier of
Y
by XBOOLE_0:6;
reconsider v =
v as
VECTOR of
V by A88;
consider phi being
linear-Functional of
(Y + (Lin {v})) such that A90:
phi | the
carrier of
Y = f9
and A91:
for
x being
VECTOR of
(Y + (Lin {v})) for
v being
VECTOR of
V st
x = v holds
phi . x <= q . v
by A84, A89, Lm1;
A92:
rng phi c= REAL
by RELAT_1:def 19;
the
carrier of
Y c= the
carrier of
(Y + (Lin {v}))
by Th1;
then A93:
the
carrier of
X c= the
carrier of
(Y + (Lin {v}))
by A80;
A94:
dom phi = the
carrier of
(Y + (Lin {v}))
by FUNCT_2:def 1;
then
dom phi c= the
carrier of
V
by RLSUB_1:def 2;
then reconsider phi =
phi as
Element of
PFuncs ( the
carrier of
V,
REAL)
by A92, PARTFUN1:def 3;
the
carrier of
Y /\ the
carrier of
X = the
carrier of
X
by A80, XBOOLE_1:28;
then
phi | the
carrier of
X = fi
by A81, A83, A90, RELAT_1:71;
then A95:
phi in A
by A91, A93;
v in Lin {v}
by RLVECT_4:9;
then A96:
v in the
carrier of
(Lin {v})
;
reconsider phi =
phi as
Element of
A by A95;
the
carrier of
(Lin {v}) c= the
carrier of
((Lin {v}) + Y)
by Th1;
then
(
dom f9 = the
carrier of
Y &
v in the
carrier of
((Lin {v}) + Y) )
by A96, FUNCT_2:def 1;
then
phi <> psi
by A78, A83, A89, A94, RLSUB_2:5;
hence
contradiction
by A77, A78, A83, A90, RELAT_1:59;
verum end;
reconsider ggh = f9 as linear-Functional of RLSY by Lm5;
f = ggh
by A83;
then reconsider psi = psi as linear-Functional of V by A78, A86, Lm4;
take
psi
; ( 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 A78, A81; for x being VECTOR of V holds psi . x <= q . x
let x be VECTOR of V; psi . x <= q . x
thus
psi . x <= q . x
by A78, A82, A86; verum