:: Hahn Banach Theorem
:: by Bogdan Nowak and Andrzej Trybulec
::
:: Received July 8, 1993
:: Copyright (c) 1993-2012 Association of Mizar Users


begin

theorem Th1: :: HAHNBAN:1
for V being RealLinearSpace
for W1, W2 being Subspace of V holds the carrier of W1 c= the carrier of (W1 + W2)
proofend;

theorem Th2: :: HAHNBAN:2
for V being RealLinearSpace
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being VECTOR of V st v1 in W1 & v2 in W2 & v = v1 + v2 holds
v |-- (W1,W2) = [v1,v2]
proofend;

theorem Th3: :: HAHNBAN:3
for V being RealLinearSpace
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds
v = v1 + v2
proofend;

theorem Th4: :: HAHNBAN:4
for V being RealLinearSpace
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds
( v1 in W1 & v2 in W2 )
proofend;

theorem Th5: :: HAHNBAN:5
for V being RealLinearSpace
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds
v |-- (W2,W1) = [v2,v1]
proofend;

theorem Th6: :: HAHNBAN:6
for V being RealLinearSpace
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v being VECTOR of V st v in W1 holds
v |-- (W1,W2) = [v,(0. V)]
proofend;

theorem Th7: :: HAHNBAN:7
for V being RealLinearSpace
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v being VECTOR of V st v in W2 holds
v |-- (W1,W2) = [(0. V),v]
proofend;

theorem Th8: :: HAHNBAN:8
for V being RealLinearSpace
for V1 being Subspace of V
for W1 being Subspace of V1
for v being VECTOR of V st v in W1 holds
v is VECTOR of V1
proofend;

theorem Th9: :: HAHNBAN:9
for V being RealLinearSpace
for V1, V2, W being Subspace of V
for W1, W2 being Subspace of W st W1 = V1 & W2 = V2 holds
W1 + W2 = V1 + V2
proofend;

theorem Th10: :: HAHNBAN:10
for V being RealLinearSpace
for W being Subspace of V
for v being VECTOR of V
for w being VECTOR of W st v = w holds
Lin {w} = Lin {v}
proofend;

theorem Th11: :: HAHNBAN:11
for V being RealLinearSpace
for v being VECTOR of V
for X being Subspace of V st not v in X holds
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
proofend;

theorem Th12: :: HAHNBAN:12
for V being RealLinearSpace
for v being VECTOR of V
for X being Subspace of V
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
y |-- (W,(Lin {y})) = [(0. W),y]
proofend;

theorem Th13: :: HAHNBAN:13
for V being RealLinearSpace
for v being VECTOR of V
for X being Subspace of V
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being VECTOR of (X + (Lin {v})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. V)]
proofend;

theorem Th14: :: HAHNBAN:14
for V being RealLinearSpace
for v being VECTOR of V
for W1, W2 being Subspace of V ex v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2]
proofend;

theorem Th15: :: HAHNBAN:15
for V being RealLinearSpace
for v being VECTOR of V
for X being Subspace of V
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being VECTOR of (X + (Lin {v})) ex x being VECTOR of X ex r being Real st w |-- (W,(Lin {y})) = [x,(r * v)]
proofend;

theorem Th16: :: HAHNBAN:16
for V being RealLinearSpace
for v being VECTOR of V
for X being Subspace of V
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w1, w2 being VECTOR of (X + (Lin {v}))
for x1, x2 being VECTOR of X
for 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)]
proofend;

theorem Th17: :: HAHNBAN:17
for V being RealLinearSpace
for v being VECTOR of V
for X being Subspace of V
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being VECTOR of (X + (Lin {v}))
for x being VECTOR of X
for t, r being Real st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
proofend;

begin

definition
let V be RLSStruct ;
mode Functional of V is Function of the carrier of V,REAL;
end;

definition
let V be RealLinearSpace;
let IT be Functional of V;
attrIT is subadditive  means :Def1: :: HAHNBAN:def 1
 for x, y being VECTOR of V holds IT . (x + y) <= (IT . x) + (IT . y);
attrIT is additive  means :Def2: :: HAHNBAN:def 2
 for x, y being VECTOR of V holds IT . (x + y) = (IT . x) + (IT . y);
attrIT is homogeneous  means :Def3: :: HAHNBAN:def 3
 for x being VECTOR of V
for r being Real holds IT . (r * x) = r * (IT . x);
attrIT is positively_homogeneous  means :Def4: :: HAHNBAN:def 4
 for x being VECTOR of V
for r being Real st r > 0 holds
IT . (r * x) = r * (IT . x);
attrIT is semi-homogeneous  means :Def5: :: HAHNBAN:def 5
 for x being VECTOR of V
for r being Real st r >= 0 holds
IT . (r * x) = r * (IT . x);
attrIT is absolutely_homogeneous  means :Def6: :: HAHNBAN:def 6
 for x being VECTOR of V
for r being Real holds IT . (r * x) = (abs r) * (IT . x);
attrIT is 0-preserving  means :Def7: :: HAHNBAN:def 7
IT . (0. V) = 0 ;
end;

:: deftheorem Def1 defines subadditive HAHNBAN:def_1_:_
 for V being RealLinearSpace
for IT being Functional of V holds
( IT is subadditive iff for x, y being VECTOR of V holds IT . (x + y) <= (IT . x) + (IT . y) );

:: deftheorem Def2 defines additive HAHNBAN:def_2_:_
 for V being RealLinearSpace
for IT being Functional of V holds
( IT is additive iff for x, y being VECTOR of V holds IT . (x + y) = (IT . x) + (IT . y) );

:: deftheorem Def3 defines homogeneous HAHNBAN:def_3_:_
 for V being RealLinearSpace
for IT being Functional of V holds
( IT is homogeneous iff for x being VECTOR of V
for r being Real holds IT . (r * x) = r * (IT . x) );

:: deftheorem Def4 defines positively_homogeneous HAHNBAN:def_4_:_
 for V being RealLinearSpace
for IT being Functional of V holds
( IT is positively_homogeneous iff for x being VECTOR of V
for r being Real st r > 0 holds
IT . (r * x) = r * (IT . x) );

:: deftheorem Def5 defines semi-homogeneous HAHNBAN:def_5_:_
 for V being RealLinearSpace
for IT being Functional of V holds
( IT is semi-homogeneous iff for x being VECTOR of V
for r being Real st r >= 0 holds
IT . (r * x) = r * (IT . x) );

:: deftheorem Def6 defines absolutely_homogeneous HAHNBAN:def_6_:_
 for V being RealLinearSpace
for IT being Functional of V holds
( IT is absolutely_homogeneous iff for x being VECTOR of V
for r being Real holds IT . (r * x) = (abs r) * (IT . x) );

:: deftheorem Def7 defines 0-preserving HAHNBAN:def_7_:_
 for V being RealLinearSpace
for IT being Functional of V holds
( IT is 0-preserving iff IT . (0. V) = 0 );

registration
let V be RealLinearSpace;
cluster Function-like V18( the carrier of V, REAL ) additive  ->  subadditive for Element of bool [: the carrier of V,REAL:];
coherence
 for b1 being Functional of V st b1 is additive holds
b1 is subadditive
proofend;
cluster Function-like V18( the carrier of V, REAL ) homogeneous  ->  positively_homogeneous for Element of bool [: the carrier of V,REAL:];
coherence
 for b1 being Functional of V st b1 is homogeneous holds
b1 is positively_homogeneous
proofend;
cluster Function-like V18( the carrier of V, REAL ) semi-homogeneous  ->  positively_homogeneous for Element of bool [: the carrier of V,REAL:];
coherence
 for b1 being Functional of V st b1 is semi-homogeneous holds
b1 is positively_homogeneous
proofend;
cluster Function-like V18( the carrier of V, REAL ) semi-homogeneous  ->  0-preserving for Element of bool [: the carrier of V,REAL:];
coherence
 for b1 being Functional of V st b1 is semi-homogeneous holds
b1 is 0-preserving
proofend;
cluster Function-like V18( the carrier of V, REAL ) absolutely_homogeneous  ->  semi-homogeneous for Element of bool [: the carrier of V,REAL:];
coherence
 for b1 being Functional of V st b1 is absolutely_homogeneous holds
b1 is semi-homogeneous
proofend;
cluster Function-like V18( the carrier of V, REAL ) positively_homogeneous 0-preserving  ->  semi-homogeneous for Element of bool [: the carrier of V,REAL:];
coherence
 for b1 being Functional of V st b1 is 0-preserving &amp; b1 is positively_homogeneous holds
b1 is semi-homogeneous
proofend;
end;

registration
let V be RealLinearSpace;
cluster Relation-like the carrier of V -defined REAL -valued Function-like non empty total V18( the carrier of V, REAL ) additive homogeneous absolutely_homogeneous for Element of bool [: the carrier of V,REAL:];
existence
 ex b1 being Functional of V st
( b1 is additive &amp; b1 is absolutely_homogeneous &amp; b1 is homogeneous )
proofend;
end;

definition
let V be RealLinearSpace;
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: :: HAHNBAN:18
for V being RealLinearSpace
for L being homogeneous Functional of V
for v being VECTOR of V holds L . (- v) = - (L . v)
proofend;

theorem Th19: :: HAHNBAN:19
for V being RealLinearSpace
for L being linear-Functional of V
for v1, v2 being VECTOR of V holds L . (v1 - v2) = (L . v1) - (L . v2)
proofend;

theorem Th20: :: HAHNBAN:20
for V being RealLinearSpace
for L being additive Functional of V holds L . (0. V) = 0
proofend;

theorem Th21: :: HAHNBAN:21
for V being RealLinearSpace
for X being Subspace of V
for fi being linear-Functional of X
for v being VECTOR of V
for y being VECTOR of (X + (Lin {v})) st v = y &amp; not v in X holds
for r being Real ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi &amp; psi . y = r )
proofend;

begin

Lm1:  for V being RealLinearSpace
for X being Subspace of V
for v being VECTOR of V st not v in the carrier of X holds
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 (X + (Lin {v})) st
( psi | the carrier of X = fi &amp; ( for x being VECTOR of (X + (Lin {v}))
for v being VECTOR of V st x = v holds
psi . x <= q . v ) )
proofend;

Lm2:  for V being RealLinearSpace holds RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is RealLinearSpace
proofend;

Lm3:  for V, V9, W9 being RealLinearSpace st V9 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds
for W being Subspace of V st W9 = RLSStruct(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W #) holds
W9 is Subspace of V9
proofend;

Lm4:  for V, V9 being RealLinearSpace st V9 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds
for f being linear-Functional of V9 holds f is linear-Functional of V
proofend;

Lm5:  for V, V9 being RealLinearSpace st V9 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds
for f being linear-Functional of V holds f is linear-Functional of V9
proofend;

theorem Th22: :: HAHNBAN:22
for V being 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 &amp; ( for x being VECTOR of V holds psi . x <= q . x ) )
proofend;

theorem Th23: :: HAHNBAN:23
for V being RealNormSpace holds the normF of V is subadditive absolutely_homogeneous Functional of V
proofend;

:: [WP: ] Hahn-Banach_Theorem_(real_spaces)
theorem :: HAHNBAN:24
for V being RealNormSpace
for X being Subspace 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 <= ||.v.|| ) holds
ex psi being linear-Functional of V st
( psi | the carrier of X = fi &amp; ( for x being VECTOR of V holds psi . x <= ||.x.|| ) )
proofend;