:: Hahn Banach Theorem
:: by Bogdan Nowak and Andrzej Trybulec
::
:: Received July 8, 1993
:: Copyright (c) 1993-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, SUBSET_1, PARTFUN1, FUNCT_1, TARSKI, RELAT_1,
SUPINF_1, XXREAL_0, ORDINAL1, ARYTM_3, ORDINAL2, XXREAL_2, RLVECT_1,
RLSUB_1, STRUCT_0, SUPINF_2, RLSUB_2, FINSEQ_4, MCART_1, RLVECT_3,
REAL_1, CARD_1, MSSUBFAM, UNIALG_1, COMPLEX1, FUNCOP_1, ARYTM_1,
ALGSTR_0, REALSET1, ZFMISC_1, NORMSP_1, HAHNBAN, NORMSP_0, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, COMPLEX1, STRUCT_0, ALGSTR_0, REAL_1, RELAT_1,
REALSET1, FUNCT_1, FUNCT_2, RLVECT_1, RLSUB_1, RLSUB_2, NORMSP_0,
NORMSP_1, SUPINF_1, PARTFUN1, FUNCOP_1, RLVECT_3, DOMAIN_1, XXREAL_2;
constructors BINOP_1, REAL_1, COMPLEX1, SUPINF_1, REALSET1, RFUNCT_3, RLSUB_2,
RLVECT_2, RLVECT_3, NORMSP_1, XXREAL_2, RELSET_1, XXREAL_1;
registrations SUBSET_1, RELSET_1, PARTFUN1, NUMBERS, XXREAL_0, XREAL_0,
MEMBERED, STRUCT_0, RLVECT_1, RLSUB_1, FUNCT_2, FUNCT_1, RELAT_1,
ORDINAL1, XTUPLE_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, RLSUB_1, RLSUB_2, ORDINAL1, XBOOLE_0, XXREAL_2;
equalities RLVECT_1, XBOOLE_0, STRUCT_0, ALGSTR_0, RLSUB_1;
expansions TARSKI, XBOOLE_0, STRUCT_0;
theorems PARTFUN1, RLSUB_1, FUNCT_2, ZFMISC_1, FUNCOP_1, TREES_2, TARSKI,
FUNCT_1, GRFUNC_1, RLVECT_1, RLSUB_2, RLVECT_4, MCART_1, RLVECT_3,
ABSVALUE, NORMSP_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_0,
XCMPLX_1, XREAL_1, XXREAL_0, NUMBERS, XXREAL_2, NORMSP_0, XREAL_0;
schemes ORDERS_1, DOMAIN_1, FUNCT_2;
begin :: Some Facts on Real Vector Spaces
reserve V for RealLinearSpace;
theorem Th1:
for W1,W2 being Subspace of V holds the carrier of W1 c= the
carrier of W1 + W2
proof
let W1,W2 be Subspace of V;
let x be object;
assume
A1: x in the carrier of W1;
the carrier of W1 c= the carrier of V by RLSUB_1:def 2;
then reconsider w = x as VECTOR of V by A1;
A2: w + 0.V = w & 0.V in W2 by RLSUB_1:17;
x in W1 by A1;
then x in {v + u where u,v is VECTOR of V : v in W1 & u in W2} by A2;
hence thesis by RLSUB_2:def 1;
end;
theorem Th2:
for W1,W2 being Subspace of V st V is_the_direct_sum_of W1,W2
for v,v1,v2 being VECTOR of V st v1 in W1 & v2 in W2 & v = v1 + v2 holds v |--
(W1,W2) = [v1,v2]
proof
let W1,W2 be Subspace of V;
assume
A1: V is_the_direct_sum_of W1,W2;
let v,v1,v2 be VECTOR of V;
[v1,v2]`1 = v1 & [v1,v2]`2 = v2;
hence thesis by A1,RLSUB_2:def 6;
end;
theorem Th3:
for W1,W2 being Subspace of V st V is_the_direct_sum_of W1,W2
for v,v1,v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds v = v1 + v2
proof
let W1,W2 be Subspace of V such that
A1: V is_the_direct_sum_of W1,W2;
let v,v1,v2 be VECTOR of V;
assume v |-- (W1,W2) = [v1,v2];
then (v |-- (W1,W2))`1 = v1 & (v |-- (W1,W2))`2 = v2;
hence thesis by A1,RLSUB_2:def 6;
end;
theorem Th4:
for W1,W2 being Subspace of V st V is_the_direct_sum_of W1,W2
for v,v1,v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds v1 in W1 & v2 in
W2
proof
let W1,W2 be Subspace of V such that
A1: V is_the_direct_sum_of W1,W2;
let v,v1,v2 be VECTOR of V;
assume v |-- (W1,W2) = [v1,v2];
then (v |-- (W1,W2))`1 = v1 & (v |-- (W1,W2))`2 = v2;
hence thesis by A1,RLSUB_2:def 6;
end;
theorem Th5:
for W1,W2 being Subspace of V st V is_the_direct_sum_of W1,W2
for v,v1,v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds v |-- (W2,W1) =
[v2,v1]
proof
let W1,W2 be Subspace of V;
assume
A1: V is_the_direct_sum_of W1,W2;
let v,v1,v2 be VECTOR of V;
assume
A2: v |-- (W1,W2) = [v1,v2];
then
A3: (v |-- (W1,W2))`1 = v1;
then
A4: v1 in W1 by A1,RLSUB_2:def 6;
A5: (v |-- (W1,W2))`2 = v2 by A2;
then
A6: v2 in W2 by A1,RLSUB_2:def 6;
v = v2 + v1 by A1,A3,A5,RLSUB_2:def 6;
hence thesis by A1,A4,A6,Th2,RLSUB_2:38;
end;
theorem Th6:
for W1,W2 being Subspace of V st V is_the_direct_sum_of W1,W2
for v being VECTOR of V st v in W1 holds v |-- (W1,W2) = [v,0.V]
proof
let W1,W2 be Subspace of V such that
A1: V is_the_direct_sum_of W1,W2;
let v be VECTOR of V such that
A2: v in W1;
0.V in W2 & v + 0.V = v by RLSUB_1:17;
hence thesis by A1,A2,Th2;
end;
theorem Th7:
for W1,W2 being Subspace of V st V is_the_direct_sum_of W1,W2
for v being VECTOR of V st v in W2 holds v |-- (W1,W2) = [0.V,v]
proof
let W1,W2 be Subspace of V;
assume
A1: V is_the_direct_sum_of W1,W2;
let v be VECTOR of V;
assume v in W2;
then v |-- (W2,W1) = [v,0.V] by A1,Th6,RLSUB_2:38;
hence thesis by A1,Th5,RLSUB_2:38;
end;
theorem Th8:
for V1 being Subspace of V, W1 being Subspace of V1, v being
VECTOR of V st v in W1 holds v is VECTOR of V1
proof
let V1 be Subspace of V, W1 be Subspace of V1, v be VECTOR of V;
assume v in W1;
then the carrier of W1 c= the carrier of V1 & v in the carrier of W1 by
RLSUB_1:def 2;
hence thesis;
end;
theorem Th9:
for V1,V2,W being Subspace of V, W1,W2 being Subspace of W st W1
= V1 & W2 = V2 holds W1 + W2 = V1 + V2
proof
let V1,V2,W be Subspace of V, W1,W2 be Subspace of W such that
A1: W1 = V1 & W2 = V2;
reconsider W3 = W1 + W2 as Subspace of V by RLSUB_1:27;
now
let v be VECTOR of V;
A2: the carrier of W1 c= the carrier of W & the carrier of W2 c= the
carrier of W by RLSUB_1:def 2;
hereby
assume
A3: v in W3;
then reconsider w = v as VECTOR of W by Th8;
consider w1,w2 being VECTOR of W such that
A4: w1 in W1 & w2 in W2 and
A5: w = w1 + w2 by A3,RLSUB_2:1;
reconsider v1 = w1, v2 = w2 as VECTOR of V by RLSUB_1:10;
v = v1 + v2 by A5,RLSUB_1:13;
hence v in V1 + V2 by A1,A4,RLSUB_2:1;
end;
assume v in V1 + V2;
then consider v1,v2 being VECTOR of V such that
A6: v1 in V1 & v2 in V2 and
A7: v = v1 + v2 by RLSUB_2:1;
v1 in the carrier of W1 & v2 in the carrier of W2 by A1,A6;
then reconsider w1 = v1, w2 = v2 as VECTOR of W by A2;
v = w1 + w2 by A7,RLSUB_1:13;
hence v in W3 by A1,A6,RLSUB_2:1;
end;
hence thesis by RLSUB_1:31;
end;
theorem Th10:
for W being Subspace of V for v being VECTOR of V, w being
VECTOR of W st v = w holds Lin{w} = Lin{v}
proof
let W be Subspace of V;
let v be VECTOR of V, w be VECTOR of W such that
A1: v = w;
reconsider W1 = Lin{w} as Subspace of V by RLSUB_1:27;
now
let u be VECTOR of V;
hereby
assume u in W1;
then consider a being Real such that
A2: u = a * w by RLVECT_4:8;
u = a * v by A1,A2,RLSUB_1:14;
hence u in Lin{v} by RLVECT_4:8;
end;
assume u in Lin{v};
then consider a being Real such that
A3: u = a * v by RLVECT_4:8;
u = a * w by A1,A3,RLSUB_1:14;
hence u in W1 by RLVECT_4:8;
end;
hence thesis by RLSUB_1:31;
end;
theorem Th11:
for v being VECTOR of V, X being Subspace of V st not v in X for
y being VECTOR of X + Lin{v}, W being Subspace of X + Lin{v} st v = y & W = X
holds X + Lin{v} is_the_direct_sum_of W,Lin{y}
proof
let v be VECTOR of V, X be Subspace of V such that
A1: not v in X;
let y be VECTOR of X + Lin{v}, W be Subspace of X + Lin{v};
assume that
A2: v = y and
A3: W = X;
Lin{v} = Lin{y} by A2,Th10;
hence the RLSStruct of X + Lin{v} = W + Lin{y} by A3,Th9;
assume W /\ Lin{y} <> (0).(X + Lin{v});
then consider z being VECTOR of X + Lin{v} such that
A4: not(z in W /\ Lin{y} iff z in (0).(X + Lin{v})) by RLSUB_1:31;
per cases by A4;
suppose that
A5: z in W /\ Lin{y} and
A6: not z in (0).(X + Lin{v});
z in Lin{y} by A5,RLSUB_2:3;
then consider a being Real such that
A7: z = a * y by RLVECT_4:8;
A8: z in W by A5,RLSUB_2:3;
now
per cases;
suppose
a = 0;
then z = 0.(X + Lin{v}) by A7,RLVECT_1:10;
hence contradiction by A6,RLSUB_1:17;
end;
suppose
A9: a <> 0;
y = 1*y by RLVECT_1:def 8
.= a"*a*y by A9,XCMPLX_0:def 7
.= a"*(a*y) by RLVECT_1:def 7;
hence contradiction by A1,A2,A3,A8,A7,RLSUB_1:21;
end;
end;
hence contradiction;
end;
suppose that
A10: not z in W /\ Lin{y} and
A11: z in (0).(X + Lin{v});
z = 0.(X + Lin{v}) by A11,RLVECT_3:29;
hence contradiction by A10,RLSUB_1:17;
end;
end;
theorem Th12:
for v being VECTOR of V, X being Subspace of V, y being VECTOR
of X + Lin{v}, W being Subspace of X + Lin{v} st v = y & X = W & not v in X
holds y |-- (W,Lin{y}) = [0.W,y]
proof
let v be VECTOR of V, X be Subspace of V, y be VECTOR of X + Lin{v}, W be
Subspace of X + Lin{v};
assume v = y & X = W & not v in X;
then X + Lin{v} is_the_direct_sum_of W,Lin{y} by Th11;
then y |-- (W,Lin{y}) = [0.(X + Lin{v}),y] by Th7,RLVECT_4:9;
hence thesis by RLSUB_1:11;
end;
theorem Th13:
for v being VECTOR of V, X being Subspace of V, y being VECTOR
of X + Lin{v}, W being Subspace of X + Lin{v} st v = y & X = W & not v in X for
w being VECTOR of X + Lin{v} st w in X holds w |-- (W,Lin{y}) = [w,0.V]
proof
let v be VECTOR of V, X be Subspace of V, y be VECTOR of X + Lin{v}, W be
Subspace of X + Lin{v} such that
A1: v = y and
A2: X = W and
A3: not v in X;
A4: X + Lin{v} is_the_direct_sum_of W,Lin{y} by A1,A2,A3,Th11;
let w be VECTOR of X + Lin{v};
assume w in X;
then w |-- (W,Lin{y}) = [w,0.(X + Lin{v})] by A2,A4,Th6;
hence thesis by RLSUB_1:11;
end;
theorem Th14:
for v being VECTOR of V, W1,W2 being Subspace of V ex v1,v2
being VECTOR of V st v |-- (W1,W2) = [v1,v2]
proof
let v be VECTOR of V, W1,W2 be Subspace of V;
take (v |-- (W1,W2))`1,(v |-- (W1,W2))`2;
thus thesis by MCART_1:21;
end;
theorem Th15:
for v being VECTOR of V, X being Subspace of V, y being VECTOR
of X + Lin{v}, W being Subspace of X + Lin{v} st v = y & X = W & not v in X for
w being VECTOR of X + Lin{v} ex x being VECTOR of X, r being Real
st w |-- (W,
Lin{y}) = [x,r*v]
proof
let v be VECTOR of V, X be Subspace of V, y be VECTOR of X + Lin{v}, W be
Subspace of X + Lin{v} such that
A1: v = y and
A2: X = W and
A3: not v in X;
let w be VECTOR of X + Lin{v};
consider v1,v2 being VECTOR of X + Lin{v} such that
A4: w |-- (W,Lin{y}) = [v1,v2] by Th14;
A5: X + Lin{v} is_the_direct_sum_of W,Lin{y} by A1,A2,A3,Th11;
then v1 in W by A4,Th4;
then reconsider x = v1 as VECTOR of X by A2;
v2 in Lin{y} by A5,A4,Th4;
then consider r being Real such that
A6: v2 = r * y by RLVECT_4:8;
take x,r;
thus thesis by A1,A4,A6,RLSUB_1:14;
end;
theorem Th16:
for v being VECTOR of V, X being Subspace of V, y being VECTOR
of X + Lin{v}, W being Subspace of X + Lin{v} st v = y & X = W & not v in X for
w1,w2 being VECTOR of X + Lin{v}, x1,x2 being VECTOR of X,
r1,r2 being Real st
w1 |-- (W,Lin{y}) = [x1,r1*v] & w2 |-- (W,Lin{y}) = [x2,r2*v] holds w1 + w2 |--
(W,Lin{y}) = [x1 + x2, (r1+r2)*v]
proof
let v be VECTOR of V, X be Subspace of V, y be VECTOR of X + Lin{v}, W be
Subspace of X + Lin{v};
assume that
A1: v = y and
A2: X = W and
A3: not v in X;
A4: X + Lin{v} is_the_direct_sum_of W,Lin{y} by A1,A2,A3,Th11;
let w1,w2 be VECTOR of X + Lin{v}, x1,x2 be VECTOR of X,
r1,r2 be Real such
that
A5: w1 |-- (W,Lin{y}) = [x1,r1*v] and
A6: w2 |-- (W,Lin{y}) = [x2,r2*v];
reconsider y1 = x1, y2 = x2 as VECTOR of X + Lin{v} by A2,RLSUB_1:10;
A7: r2*v = r2*y by A1,RLSUB_1:14;
then
A8: y2 in W by A4,A6,Th4;
(r1+r2)*v = (r1+r2)*y by A1,RLSUB_1:14;
then
A9: (r1+r2)*v in Lin{y} by RLVECT_4:8;
reconsider z1 = x1, z2 = x2 as VECTOR of V by RLSUB_1:10;
A10: y1 + y2 = z1 + z2 by RLSUB_1:13
.= x1 + x2 by RLSUB_1:13;
A11: r1*v = r1*y by A1,RLSUB_1:14;
then y1 in W by A4,A5,Th4;
then
A12: y1 + y2 in W by A8,RLSUB_1:20;
A13: w2 = y2 + r2*y by A4,A6,A7,Th3;
w1 = y1 + r1*y by A4,A5,A11,Th3;
then
A14: w1 + w2 = y1 + r1*y + y2 + r2*y by A13,RLVECT_1:def 3
.= y1 + y2 + r1*y + r2*y by RLVECT_1:def 3
.= y1 + y2 + (r1*y + r2*y) by RLVECT_1:def 3
.= y1 + y2 + (r1+r2)*y by RLVECT_1:def 6;
(r1+r2)*y = (r1+r2)*v by A1,RLSUB_1:14;
hence thesis by A4,A12,A9,A14,A10,Th2;
end;
theorem Th17:
for v being VECTOR of V, X being Subspace of V, y being VECTOR
of X + Lin{v}, W being Subspace of X + Lin{v} st v = y & X = W & not v in X for
w being VECTOR of X + Lin{v}, x being VECTOR of X,
t,r being Real st w |-- (W,
Lin{y}) = [x,r*v] holds t*w |-- (W,Lin{y}) = [t*x, t*r*v]
proof
let v be VECTOR of V, X be Subspace of V, y be VECTOR of X + Lin{v}, W be
Subspace of X + Lin{v};
assume that
A1: v = y and
A2: X = W and
A3: not v in X;
A4: X + Lin{v} is_the_direct_sum_of W,Lin{y} by A1,A2,A3,Th11;
let w be VECTOR of X + Lin{v}, x be VECTOR of X,
t,r be Real such that
A5: w |-- (W,Lin{y}) = [x,r*v];
reconsider z = x as VECTOR of X + Lin{v} by A2,RLSUB_1:10;
r*y = r*v by A1,RLSUB_1:14;
then
A6: t*w = t*(z + r*y) by A4,A5,Th3
.= t*z + t*(r*y) by RLVECT_1:def 5
.= t*z + t*r*y by RLVECT_1:def 7;
reconsider u = x as VECTOR of V by RLSUB_1:10;
A7: t*r*y in Lin{y} by RLVECT_4:8;
A8: t*r*y = t*r*v by A1,RLSUB_1:14;
A9: t*z = t*u by RLSUB_1:14
.= t*x by RLSUB_1:14;
then t*z in W by A2;
hence thesis by A4,A9,A8,A7,A6,Th2;
end;
begin :: Functionals in Real Linear Space
definition
let V be RLSStruct;
mode Functional of V is Function of the carrier of V,REAL;
end;
definition
let V;
let IT be Functional of V;
attr IT is subadditive means
:Def1:
for x,y being VECTOR of V holds IT.(x+y) <= IT.x+IT.y;
attr IT is additive means
:Def2:
for x,y being VECTOR of V holds IT.(x+y) = IT.x+IT.y;
attr IT is homogeneous means
:Def3:
for x being VECTOR of V, r being Real holds IT.(r*x) = r*IT.x;
attr IT is positively_homogeneous means
:Def4:
for x being VECTOR of V, r being Real st r > 0
holds IT.(r*x) = r*IT.x;
attr IT is semi-homogeneous means
for x being VECTOR of V, r being Real st r >= 0
holds IT.(r*x) = r*IT.x;
attr IT is absolutely_homogeneous means
for x being VECTOR of V, r being Real holds IT.(r*x) = |.r.|*IT.x;
attr IT is 0-preserving means
IT.(0.V) = 0;
end;
registration
let V;
cluster additive -> subadditive for Functional of V;
coherence;
cluster homogeneous -> positively_homogeneous for Functional of V;
coherence;
cluster semi-homogeneous -> positively_homogeneous for Functional of V;
coherence;
cluster semi-homogeneous -> 0-preserving for Functional of V;
coherence
proof
let f be Functional of V;
assume
A1: f is semi-homogeneous;
thus f.(0.V) = f.(0*0.V)
.= 0*f.(0.V) by A1
.= 0;
end;
cluster absolutely_homogeneous -> semi-homogeneous for Functional of V;
coherence
proof
let f be Functional of V;
assume
A2: f is absolutely_homogeneous;
let x be VECTOR of V, r be Real;
assume r >= 0;
then |.r.| = r by ABSVALUE:def 1;
hence thesis by A2;
end;
cluster 0-preserving positively_homogeneous -> semi-homogeneous for
Functional
of V;
coherence
proof
let f be Functional of V such that
A3: f is 0-preserving and
A4: f is positively_homogeneous;
let x be VECTOR of V, r be Real such that
A5: r >= 0;
per cases by A5;
suppose
A6: r = 0;
hence f.(r*x) = f.(0.V) by RLVECT_1:10
.= r*f.x by A3,A6;
end;
suppose
r > 0;
hence thesis by A4;
end;
end;
end;
registration
let V;
cluster additive absolutely_homogeneous homogeneous for Functional of V;
existence
proof
reconsider f = (the carrier of V) --> In(0,REAL) as Functional of V;
take f;
hereby
let x,y be VECTOR of V;
thus f.(x+y) = 0+0 by FUNCOP_1:7
.= f.x+0 by FUNCOP_1:7
.= f.x+f.y by FUNCOP_1:7;
end;
hereby
let x be VECTOR of V, r be Real;
thus f.(r*x) = |.r.|*0 by FUNCOP_1:7
.= |.r.|*f.x by FUNCOP_1:7;
end;
let x be VECTOR of V, r be Real;
thus f.(r*x) = r*0 by FUNCOP_1:7
.= r*f.x by FUNCOP_1:7;
end;
end;
definition
let V;
mode Banach-Functional of V is subadditive positively_homogeneous Functional
of V;
mode linear-Functional of V is additive homogeneous Functional of V;
end;
theorem Th18:
for L being homogeneous Functional of V, v being VECTOR of V
holds L.(-v) = - L.v
proof
let L be homogeneous Functional of V, v be VECTOR of V;
thus L.(-v) = L.((-1)*v) by RLVECT_1:16
.= (-1)*L.v by Def3
.= - L.v;
end;
theorem Th19:
for L being linear-Functional of V, v1,v2 being VECTOR of V
holds L.(v1 - v2) = L.v1 - L.v2
proof
let L be linear-Functional of V, v1,v2 be VECTOR of V;
thus L.(v1 - v2) = L.(v1) + L.(-v2) by Def2
.= L.v1 + - L.v2 by Th18
.= L.v1 - L.v2;
end;
theorem Th20:
for L being additive Functional of V holds L.(0.V) = 0
proof
let L be additive Functional of V;
L.(0.V) + 0 = L.(0.V + 0.V)
.= L.(0.V) + L.(0.V) by Def2;
hence thesis;
end;
theorem Th21:
for X being Subspace of V, fi being linear-Functional of X, v
being VECTOR of V, y being VECTOR of X + Lin{v} st v = y & not v in X for r
being Real ex psi being linear-Functional of X + Lin{v} st psi|the carrier of X
=fi & psi.y = r
proof
let X be Subspace of V, fi be linear-Functional of X, v be VECTOR of V, y be
VECTOR of X + Lin{v} such that
A1: v = y and
A2: not v in X;
reconsider W1 = X as Subspace of X + Lin{v} by RLSUB_2:7;
let r be Real;
defpred P[VECTOR of X + Lin{v},Real] means for x being VECTOR of X,
s being Real st
($1 |-- (W1,Lin{y}))`1 = x & ($1 |-- (W1,Lin{y}))`2 = s*v
holds $2 = fi.x + s*r;
A3: now
let e be Element of X + Lin{v};
consider x being VECTOR of X, s being Real such that
A4: e |-- (W1,Lin{y}) = [x,s*v] by A1,A2,Th15;
reconsider u = fi.x + s*r as Element of REAL by XREAL_0:def 1;
take u;
thus P[e,u]
proof
let x9 be VECTOR of X, t be Real such that
A5: (e |-- (W1,Lin{y}))`1 = x9 and
A6: (e |-- (W1,Lin{y}))`2 = t*v;
v <> 0.V by A2,RLSUB_1:17;
then t = s by A4,A6,RLVECT_1:37;
hence thesis by A4,A5;
end;
end;
consider f being Function of the carrier of X + Lin{v},REAL such that
A7: for e being VECTOR of X + Lin{v} holds P[e,f.e] from FUNCT_2:sch 3(
A3);
A8: now
let a be object;
assume a in dom fi;
then reconsider x = a as VECTOR of X by FUNCT_2:def 1;
the carrier of X c= the carrier of X + Lin{v} by Th1;
then reconsider v1 = x as VECTOR of X + Lin{v};
v1 in X;
then (v1 |-- (W1,Lin{y})) = [v1,0.V] by A1,A2,Th13
.= [v1,0*v] by RLVECT_1:10;
then
A9: (v1 |-- (W1,Lin{y}))`1 = x & (v1 |-- (W1,Lin{y}))`2 = 0*v;
thus fi.a = fi.x + 0*r .= f.a by A7,A9;
end;
reconsider f as Functional of X + Lin{v};
A10: y |-- (W1,Lin{y}) = [0.W1,y] by A1,A2,Th12;
then
A11: (y |-- (W1,Lin{y}))`1 = 0.X;
A12: f is additive
proof
let v1,v2 be VECTOR of X + Lin{v};
consider x1 being VECTOR of X, s1 being Real such that
A13: v1 |-- (W1,Lin{y}) = [x1,s1*v] by A1,A2,Th15;
A14: (v1 |-- (W1,Lin{y}))`1 = x1 & (v1 |-- (W1,Lin{y}))`2 = s1*v by A13;
consider x2 being VECTOR of X, s2 being Real such that
A15: v2 |-- (W1,Lin{y}) = [x2,s2*v] by A1,A2,Th15;
A16: (v2 |-- (W1,Lin{y}))`1 = x2 & (v2 |-- (W1,Lin{y}))`2 = s2*v by A15;
v1 + v2 |-- (W1,Lin{y}) = [x1 +x2,(s1+s2)*v] by A1,A2,A13,A15,Th16;
then
(v1 + v2 |-- (W1,Lin{y}))`1 = x1 + x2 & (v1 + v2 |-- (W1,Lin{y}))`2 =
(s1+ s2)*v;
hence f.(v1+v2) = fi.(x1 + x2) + (s1 + s2)*r by A7
.= fi.(x1) + fi.(x2) + (s1*r + s2*r) by Def2
.= fi.(x1) + s1*r + (fi.(x2) + s2*r)
.= f.v1 + (fi.(x2) + s2*r) by A7,A14
.= f.v1+f.v2 by A7,A16;
end;
f is homogeneous
proof
let v0 be VECTOR of X + Lin{v}, t be Real;
consider x0 being VECTOR of X, s0 being Real such that
A17: v0 |-- (W1,Lin{y}) = [x0,s0*v] by A1,A2,Th15;
A18: (v0 |-- (W1,Lin{y}))`1 = x0 & (v0 |-- (W1,Lin{y}))`2 = s0*v by A17;
t*v0 |-- (W1,Lin{y}) = [t*x0,t*s0*v] by A1,A2,A17,Th17;
then (t*v0 |-- (W1,Lin{y}))`1 = t*x0 & (t*v0 |-- (W1,Lin{y}))`2 = t*s0*v;
hence f.(t*v0) = fi.(t*x0) + t*s0*r by A7
.= t*(fi.x0) + t*(s0*r) by Def3
.= t*(fi.x0 + s0*r)
.= t*f.v0 by A7,A18;
end;
then reconsider f as linear-Functional of X + Lin{v} by A12;
take f;
dom fi = the carrier of X & dom f = the carrier of X + Lin{v} by
FUNCT_2:def 1;
then dom fi = dom f /\ the carrier of X by Th1,XBOOLE_1:28;
hence f|the carrier of X=fi by A8,FUNCT_1:46;
(y |-- (W1,Lin{y}))`2 = y by A10
.= 1*v by A1,RLVECT_1:def 8;
hence f.y = fi.(0.X) + 1*r by A7,A11
.= 0 + 1*r by Th20
.= r;
end;
begin :: Hahn Banach Theorem
Lm1: for X being Subspace of V, v being VECTOR of V st not v in the carrier of
X for q being Banach-Functional of V, fi being linear-Functional of X st for x
being VECTOR of X, v being VECTOR of V st x=v holds fi.x <= q.v ex psi being
linear-Functional of X + Lin{v} st psi|the carrier of X=fi & for x being VECTOR
of X + Lin{v}, v being VECTOR of V st x = v holds psi.x <= q.v
proof
let X be Subspace of V, v be VECTOR of V;
assume not v in the carrier of X;
then
A1: not v in X;
v in Lin{v} by RLVECT_4:9;
then
A2: v in the carrier of Lin{v};
the carrier of Lin{v} c= the carrier of Lin{v} + X by Th1;
then reconsider x0 = v as VECTOR of X + Lin{v} by A2,RLSUB_2:5;
set x1 = the VECTOR of X;
let q be Banach-Functional of V, fi be linear-Functional of X such that
A3: for x being VECTOR of X, v being VECTOR of V st x=v holds fi.x <= q. v;
set A = { fi.x - q.(y - v) where x is VECTOR of X, y is VECTOR of V : x = y
}, B = { fi.x + q.(v - y) where x is VECTOR of X, y is VECTOR of V : x = y };
A4: now
let x1,x2 be VECTOR of X, y1,y2 be VECTOR of V;
assume x1 = y1 & x2 = y2;
then fi.(x1 - x2) <= q.(y1 - y2) by A3,RLSUB_1:16;
then
A5: fi.x1 - fi.x2 <= q.(y1 - y2) by Th19;
y1 - y2 = y1 + 0.V + -y2
.= y1 + (-v + v) + -y2 by RLVECT_1:5
.= y1 - v + v + -y2 by RLVECT_1:def 3
.= y1 - v + (v - y2) by RLVECT_1:def 3;
then q.(y1 - y2) <= q.(y1 - v) + q.(v - y2) by Def1;
then fi.x1 - fi.x2 <= q.(v - y2) + q.(y1 - v) by A5,XXREAL_0:2;
then fi.x1 <= fi.x2 + (q.(v - y2) + q.(y1 - v)) by XREAL_1:20;
then fi.x1 <= fi.x2 + q.(v - y2) + q.(y1 - v);
hence fi.x1 - q.(y1 - v) <= fi.x2 + q.(v - y2) by XREAL_1:20;
end;
A6: now
let a,b be ExtReal;
assume a in A;
then
A7: ex x1 being VECTOR of X, y1 being VECTOR of V st a = fi.x1 - q.(y1 - v
) & x1 = y1;
assume b in B;
then
ex x2 being VECTOR of X, y2 being VECTOR of V st b = fi.x2 + q.(v - y2
) & x2 = y2;
hence a <= b by A4,A7;
end;
reconsider v1 = x1 as VECTOR of V by RLSUB_1:10;
A8: A c= REAL
proof
let a be object;
assume a in A;
then
ex x being VECTOR of X, y being VECTOR of V st a = fi.x - q.(y - v) &
x = y;
hence thesis;
end;
A9: B c= REAL
proof
let b be object;
assume b in B;
then
ex x being VECTOR of X, y being VECTOR of V st b = fi.x + q.(v - y) &
x = y;
hence thesis;
end;
fi.x1 - q.(v1 - v) in A & fi.x1 + q.(v - v1) in B;
then reconsider A, B as non empty Subset of ExtREAL by A8,A9,NUMBERS:31
,XBOOLE_1:1;
A10: sup A <= inf B by A6,XXREAL_2:96;
A11: A is bounded_above
proof
set b = the Element of B;
reconsider b as Real by A9;
take b;
let x be ExtReal;
thus thesis by A6;
end;
A <> {-infty}
proof
set x = the Element of A;
assume A = {-infty};
then x = -infty by TARSKI:def 1;
hence contradiction by A8;
end;
then reconsider r = sup A as Element of REAL by A11,XXREAL_2:57;
consider psi being linear-Functional of X + Lin{v} such that
A12: psi|the carrier of X=fi and
A13: psi.x0 = r by A1,Th21;
take psi;
thus psi|the carrier of X=fi by A12;
let y be VECTOR of X + Lin{v}, u be VECTOR of V such that
A14: y = u;
y in X + Lin{v};
then consider y1,y29 being VECTOR of V such that
A15: y1 in X and
A16: y29 in Lin{v} and
A17: y = y1 + y29 by RLSUB_2:1;
y1 in X + Lin{v} by A15,RLSUB_2:2;
then reconsider x = y1 as VECTOR of X + Lin{v};
reconsider x1 = x as VECTOR of X by A15;
consider t being Real such that
A18: y29 = t * v by A16,RLVECT_4:8;
per cases;
suppose
t = 0;
then y29 = 0.V by A18,RLVECT_1:10;
then
A19: y = x1 by A17;
then fi.x1 <= q.u by A3,A14;
hence thesis by A12,A19,FUNCT_1:49;
end;
suppose
A20: t > 0;
reconsider b = psi.((-t)"*x) + q.(v - (-t)"*y1) as R_eal by XBOOLE_0:def 3
,XXREAL_0:def 4;
A21: v - (-t)"*y1 = v - (-t")*y1 by XCMPLX_1:222
.= v + - -t"*y1 by RLVECT_4:3
.= v + t"*y1;
A22: (-t)"*x1 = (-t)"*y1 by RLSUB_1:14;
then (-t)"*x1 = (-t)"*x by RLSUB_1:14;
then fi.((-t)"*x1) = psi.((-t)"*x) by A12,FUNCT_1:49;
then psi.((-t)"*x) + q.(v - (-t)"*y1) in B by A22;
then inf B <= b by XXREAL_2:3;
then sup A <= b by A10,XXREAL_0:2;
then psi.((-t)"*x) >= r - q.(v - (-t)"*y1) by XREAL_1:20;
then
A23: - psi.((-t)"*x) <= - (r - q.(v - (-t)"*y1)) by XREAL_1:24;
- psi.((-t)"*x) = (-1)*psi.((-t)"*x) .= psi.((-1)*((-t)"*x)) by Def3
.= psi.((-1)*(-t)"*x) by RLVECT_1:def 7
.= psi.((-1)*(-t")*x) by XCMPLX_1:222
.= psi.(t"*x);
then
A24: psi.(t"*x) <= q.(v + t"*y1) - r by A23,A21;
t"*u = t"*y1 + t"*y29 by A14,A17,RLVECT_1:def 5
.= t"*y1 + t"*t*v by A18,RLVECT_1:def 7
.= t"*y1 + 1*v by A20,XCMPLX_0:def 7
.= v + t"*y1 by RLVECT_1:def 8;
then psi.(t"*x) + r <= q.(t"*u) by A24,XREAL_1:19;
then
A25: psi.(t"*x) + r <= t"*(q.u) by A20,Def4;
y29 in X + Lin{v} by A16,RLSUB_2:2;
then reconsider y2 = y29 as VECTOR of X + Lin{v};
y2 = t*x0 by A18,RLSUB_1:14;
then
A26: y = x + t*x0 by A17,RLSUB_1:13;
A27: t*(t"*(q.u)) = t*t"*(q.u) .= 1*(q.u) by A20,XCMPLX_0:def 7
.= q.u;
psi.(x + t*x0) = psi.x + psi.(t*x0) by Def2
.= 1*(psi.x + t*psi.x0) by Def3
.= t*t"*(psi.x + t*psi.x0) by A20,XCMPLX_0:def 7
.= t*(t"*(psi.x) + t"*t*psi.x0)
.= t*(t"*(psi.x) + 1*psi.x0) by A20,XCMPLX_0:def 7
.= t*(psi.(t"*x) + r) by A13,Def3;
hence thesis by A20,A26,A27,A25,XREAL_1:64;
end;
suppose
A28: t < 0;
-y29 in Lin{v} by A16,RLSUB_1:22;
then -y29 in X + Lin{v} by RLSUB_2:2;
then reconsider y2 = -y29 as VECTOR of X + Lin{v};
reconsider a = psi.((-t)"*x) - q.((-t)"*y1 - v) as R_eal by XBOOLE_0:def 3
,XXREAL_0:def 4;
A29: y = y1 - -y29 by A17;
A30: -y29 = (-t)*v by A18,RLVECT_4:3;
then y2 = (-t)*x0 by RLSUB_1:14;
then
A31: y = x - (-t)*x0 by A29,RLSUB_1:16;
A32: (-t)"*x1 = (-t)"*y1 by RLSUB_1:14;
then (-t)"*x1 = (-t)"*x by RLSUB_1:14;
then fi.((-t)"*x1) = psi.((-t)"*x) by A12,FUNCT_1:49;
then psi.((-t)"*x) - q.((-t)"*y1 - v) in A by A32;
then a <= sup A by XXREAL_2:4;
then
A33: psi.((-t)"*x) <= r + q.((-t)"*y1 - v) by XREAL_1:20;
A34: -t > 0 by A28,XREAL_1:58;
(-t)"*u = (-t)"*y1 - (-t)"*-y29 by A14,A29,RLVECT_1:34
.= (-t)"*y1 - (-t)"*(-t)*v by A30,RLVECT_1:def 7
.= (-t)"*y1 - 1*v by A34,XCMPLX_0:def 7
.= (-t)"*y1 - v by RLVECT_1:def 8;
then psi.((-t)"*x) - r <= q.((-t)"*u) by A33,XREAL_1:20;
then
A35: psi.((-t)"*x) - r <= (-t)"*(q.u) by A34,Def4;
A36: (-t)*((-t)"*(q.u)) = (-t)*(-t)"*(q.u) .= 1*(q.u) by A34,XCMPLX_0:def 7
.= q.u;
psi.(x - (-t)*x0) = psi.x - psi.((-t)*x0) by Th19
.= 1*(psi.x - (-t)*psi.x0) by Def3
.= (-t)*(-t)"*(psi.x - (-t)*psi.x0) by A34,XCMPLX_0:def 7
.= (-t)*((-t)"*(psi.x) - (-t)"*(-t)*psi.x0)
.= (-t)*((-t)"*(psi.x) - 1*psi.x0) by A34,XCMPLX_0:def 7
.= (-t)*(psi.((-t)"*x) - r) by A13,Def3;
hence thesis by A28,A31,A36,A35,XREAL_1:64;
end;
end;
Lm2: the RLSStruct of V is RealLinearSpace
proof
(Omega).V is RealLinearSpace;
hence thesis;
end;
Lm3: for V9,W9 being RealLinearSpace st V9 = the RLSStruct of V for W being
Subspace of V st W9 = the RLSStruct of W holds W9 is Subspace of V9
proof
let V9,W9 be RealLinearSpace such that
A1: V9 = the RLSStruct of V;
let W be Subspace of V;
assume
A2: W9 = the RLSStruct of W;
hence the carrier of W9 c= the carrier of V9 by A1,RLSUB_1:def 2;
thus 0.W9 = 0.W by A2
.= 0.V by RLSUB_1:def 2
.= 0.V9 by A1;
thus the addF of W9 = (the addF of V9)||the carrier of W9 by A1,A2,
RLSUB_1:def 2;
thus the Mult of W9 = (the Mult of V9)|[:REAL, the carrier of W9:] by A1,A2,
RLSUB_1:def 2;
end;
Lm4: for V9 being RealLinearSpace st V9 = the RLSStruct of V for f being
linear-Functional of V9 holds f is linear-Functional of V
proof
let V9 be RealLinearSpace such that
A1: V9 = the RLSStruct of V;
let f be linear-Functional of V9;
reconsider f9 = f as Functional of V by A1;
A2: f9 is homogeneous
proof
let x be VECTOR of V, r be Real;
reconsider x9 = x as VECTOR of V9 by A1;
thus f9.(r*x) = f9.(r*x9) by A1
.= r*f9.x by Def3;
end;
f9 is additive
proof
let x,y be VECTOR of V;
reconsider x9 = x, y9 = y as VECTOR of V9 by A1;
thus f9.(x+y) = f.(x9+y9) by A1
.= f9.x+f9.y by Def2;
end;
hence thesis by A2;
end;
Lm5: for V9 being RealLinearSpace st V9 = the RLSStruct of V for f being
linear-Functional of V holds f is linear-Functional of V9
proof
let V9 be RealLinearSpace such that
A1: V9 = the RLSStruct of V;
let f be linear-Functional of V;
reconsider f9 = f as Functional of V9 by A1;
A2: f9 is homogeneous
proof
let x be VECTOR of V9, r be Real;
reconsider x9 = x as VECTOR of V by A1;
thus f9.(r*x) = f9.(r*x9) by A1
.= r*f9.x by Def3;
end;
f9 is additive
proof
let x,y be VECTOR of V9;
reconsider x9 = x, y9 = y as VECTOR of V by A1;
thus f9.(x+y) = f.(x9+y9) by A1
.= f9.x+f9.y by Def2;
end;
hence thesis by A2;
end;
theorem Th22:
for V being RealLinearSpace, X being Subspace of V, q being
Banach-Functional of V, fi being linear-Functional of X st for x being VECTOR
of X, 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
proof
let V be RealLinearSpace, X be Subspace of V, q be Banach-Functional of V,
fi be linear-Functional of 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,50;
then reconsider fi9 = fi as Element of PFuncs(the carrier of V,REAL);
reconsider RLS = the RLSStruct of V as RealLinearSpace by Lm2;
defpred P[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, 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): P[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, v being VECTOR of V st x=v holds fi.x <= q. v;
then fi in A by A1;
then reconsider A as non empty Subset of PFuncs(the carrier of V,REAL);
defpred P[set, set] means $1 c= $2;
A2: for x,y being Element of A st P[x,y] & P[y,x] holds x = y;
A3: for x,y,z being Element of A st P[x,y] & P[y,z] holds P[x,z] by XBOOLE_1:1;
A4: now
let B be set such that
A5: B c= A and
A6: for x,y being Element of A st x in B & y in B holds P[x,y] or P[y ,x];
per cases;
suppose
A7: B = {};
set u = the Element of A;
take u;
let x be Element of A;
assume x in B;
hence P[x,u] by A7;
end;
suppose
A8: B <> {};
A9: B is c=-linear
proof
let x,y be set;
assume x in B & y in B;
hence x c= y or y c= x by A5,A6;
end;
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 non empty functional set by A5,A8;
set t = the Element of B;
set K = the set of all dom g where g is Element of E;
A10: dom u = union K by FUNCT_1:110;
A11: now
let t be set;
assume t in A;
then consider
f being Element of PFuncs(the carrier of V,REAL) such that
A12: t = f and
A13: 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, v being VECTOR of V st y = v holds f9.y <= q.v;
consider Y being Subspace of V such that
A14: the carrier of X c= the carrier of Y and
A15: f|the carrier of X = fi and
A16: ex f9 being linear-Functional of Y st f = f9 & for y being
VECTOR of Y, v being VECTOR of V st y = v holds f9.y <= q.v by A13;
take Y;
consider f9 being linear-Functional of Y such that
A17: f = f9 and
A18: for y being VECTOR of Y, v being VECTOR of V st y = v holds
f9.y <= q.v by A16;
reconsider f = f9 as linear-Functional of Y;
take f;
thus t = f by A12,A17;
thus the carrier of X c= the carrier of Y by A14;
thus f|the carrier of X = fi by A15,A17;
thus for y being VECTOR of Y, v being VECTOR of V st y = v holds f.y
<= q.v by A18;
end;
A19: now
let x be set;
assume x in the set of all dom g where g is Element of E;
then consider g being Element of E such that
A20: dom g = x;
g in A by A5;
then consider
Y being Subspace of V, f9 being linear-Functional of Y such
that
A21: 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, v being VECTOR of V st y = v holds f9.y
<= q.v by A11;
dom g = the carrier of Y by A21,FUNCT_2:def 1;
hence x c= the carrier of V by A20,RLSUB_1:def 2;
end;
t in A by A5,A8;
then ex Y being Subspace of V, f9 being linear-Functional of Y st t = f9
& the carrier of X c= the carrier of Y & f9|the carrier of X = fi & for y being
VECTOR of Y, 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
let v,u be Element of V;
assume that
A22: v in D and
A23: u in D;
consider D1 being set such that
A24: v in D1 and
A25: D1 in K 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 K 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, 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 K;
hence v + u in D by A10,A35,TARSKI:def 4;
end;
let a be Real, v be Element of V;
assume v in D;
then consider D1 being set such that
A36: v in D1 and
A37: D1 in K 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, 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 K;
hence thesis by A10,A41,TARSKI:def 4;
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
t in XX and
A43: XX in K 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 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;
consider XXx being set such that
A46: x in XXx and
A47: XXx in K 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 K 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, 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;
end;
f9 is homogeneous
proof
let x be VECTOR of Y, r be Real;
consider XX being set such that
A57: x in XX and
A58: XX in K 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, 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;
end;
then reconsider f9 as linear-Functional of Y by A45;
A63: now
let y be VECTOR of Y, v be VECTOR of V such that
A64: y = v;
consider XX being set such that
A65: y in XX and
A66: XX in K 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, 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;
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, 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 as Element of A;
take u;
let x be Element of A;
assume x in B;
hence P[x,u] by ZFMISC_1:74;
end;
end;
A76: for x being Element of A holds P[x,x];
consider psi being Element of A such that
A77: for chi being Element of A st psi <> chi holds not P[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, 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, v being VECTOR of V st y = v holds f9.y <= q.v by A79;
reconsider RLSY = the RLSStruct 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, 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
assume the RLSStruct of Y <> the RLSStruct of V;
then
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 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}, 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 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 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;
end;
reconsider ggh = f9 as linear-Functional of RLSY by Lm5;
f = ggh by A83;
then reconsider psi as linear-Functional of V by A78,A86,Lm4;
take psi;
thus psi|the carrier of X = fi by A78,A81;
let x be VECTOR of V;
thus thesis by A78,A82,A86;
end;
theorem Th23:
for V being RealNormSpace holds the normF of V is
absolutely_homogeneous subadditive Functional of V
proof
let V be RealNormSpace;
reconsider N = the normF of V as Functional of V;
A1: N is subadditive
proof
let x,y be VECTOR of V;
A2: N.(x+y) = ||.x+y.|| by NORMSP_0:def 1;
N.(x) = ||.x.|| & N.(y) = ||.y.|| by NORMSP_0:def 1;
hence thesis by A2,NORMSP_1:def 1;
end;
N is absolutely_homogeneous
proof
let x be VECTOR of V, r be Real;
thus N.(r*x) = ||.r*x.|| by NORMSP_0:def 1
.= |.r.|*||.x.|| by NORMSP_1:def 1
.= |.r.|*N.x by NORMSP_0:def 1;
end;
hence thesis by A1;
end;
::$N Hahn-Banach Theorem (real spaces)
theorem
for V being RealNormSpace, X being Subspace of V, fi being
linear-Functional of X st for x being VECTOR of X, v being VECTOR of V st x=v
holds fi.x <= ||.v.|| ex psi being linear-Functional of V st psi|the carrier of
X=fi & for x being VECTOR of V holds psi.x <= ||.x.||
proof
let V be RealNormSpace, X be Subspace of V, fi be linear-Functional of X
such that
A1: for x being VECTOR of X, v being VECTOR of V st x=v holds fi.x <= ||.v.||;
reconsider q = the normF of V as Banach-Functional of V by Th23;
now
let x be VECTOR of X, v be VECTOR of V such that
A2: x=v;
q.v = ||.v.|| by NORMSP_0:def 1;
hence fi.x <= q.v by A1,A2;
end;
then consider psi being linear-Functional of V such that
A3: psi|the carrier of X=fi and
A4: for x being VECTOR of V holds psi.x <= q.x by Th22;
take psi;
thus psi|the carrier of X=fi by A3;
let x be VECTOR of V;
q.x = ||.x.|| by NORMSP_0:def 1;
hence thesis by A4;
end;