:: Hahn Banach Theorem in the Vector Space over the Field of Complex Numbers
:: by Anna Justyna Milewska
::
:: Received May 23, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users

Lm1: for F being non empty right_complementable Abelian add-associative right_zeroed right-distributive doubleLoopStr
for x, y being Element of F holds x * (- y) = - (x * y)

proof end;

theorem :: HAHNBAN1:1

canceled;

::$CT

theorem :: HAHNBAN1:2

for x1, y1, x2, y2 being Real holds (x1 + (y1 * <i>)) * (x2 + (y2 * <i>)) = ((x1 * x2) - (y1 * y2)) + (((x1 * y2) + (x2 * y1)) * <i>) ;

theorem Th2: :: HAHNBAN1:3

for z being Element of COMPLEX holds |.z.| + (0 * <i>) = ((z *') / (|.z.| + (0 * <i>))) * z

proof end;

definition

let x, y be Real;

func [**x,y**] -> Element of F_Complex equals :: HAHNBAN1:def 1
x + (y * <i>);

coherence
x + (y * <i>) is Element of F_Complex

proof end;

end;

:: deftheorem defines [** HAHNBAN1:def 1 :
for x, y being Real holds [**x,y**] = x + (y * <i>);

definition

func i_FC -> Element of F_Complex equals :: HAHNBAN1:def 2
<i> ;

coherence
<i> is Element of F_Complex

proof end;

end;

:: deftheorem defines i_FC HAHNBAN1:def 2 :
i_FC = <i> ;

theorem Th3: :: HAHNBAN1:4

i_FC * i_FC = - (1_ F_Complex)

proof end;

theorem Th4: :: HAHNBAN1:5

(- (1_ F_Complex)) * (- (1_ F_Complex)) = 1_ F_Complex

proof end;

theorem :: HAHNBAN1:6

for x1, y1, x2, y2 being Real holds [**x1,y1**] + [**x2,y2**] = [**(x1 + x2),(y1 + y2)**] ;

theorem :: HAHNBAN1:7

for x1, y1, x2, y2 being Real holds [**x1,y1**] * [**x2,y2**] = [**((x1 * x2) - (y1 * y2)),((x1 * y2) + (x2 * y1))**] ;

theorem :: HAHNBAN1:8

canceled;

::$CT

theorem :: HAHNBAN1:9

for r being Real holds |.[**r,0**].| = |.r.| ;

theorem :: HAHNBAN1:10

for x, y being Element of F_Complex holds
( Re (x + y) = (Re x) + (Re y) & Im (x + y) = (Im x) + (Im y) ) by COMPLEX1:8;

theorem :: HAHNBAN1:11

for x, y being Element of F_Complex holds
( Re (x * y) = ((Re x) * (Re y)) - ((Im x) * (Im y)) & Im (x * y) = ((Re x) * (Im y)) + ((Re y) * (Im x)) ) by COMPLEX1:9;

definition

let K be 1-sorted ;
let V be ModuleStr over K;
mode Functional of V is Function of the carrier of V, the carrier of K;

end;

definition

let K be non empty addLoopStr ;
let V be non empty ModuleStr over K;
let f, g be Functional of V;

func f + g -> Functional of V means :Def3: :: HAHNBAN1:def 3
for x being Element of V holds it . x = (f . x) + (g . x);

existence
ex b₁ being Functional of V st
for x being Element of V holds b₁ . x = (f . x) + (g . x)

proof end;

uniqueness
for b₁, b₂ being Functional of V st ( for x being Element of V holds b₁ . x = (f . x) + (g . x) ) & ( for x being Element of V holds b₂ . x = (f . x) + (g . x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines + HAHNBAN1:def 3 :
for K being non empty addLoopStr
for V being non empty ModuleStr over K
for f, g, b₅ being Functional of V holds
( b₅ = f + g iff for x being Element of V holds b₅ . x = (f . x) + (g . x) );

definition

let K be non empty addLoopStr ;
let V be non empty ModuleStr over K;
let f be Functional of V;

func - f -> Functional of V means :Def4: :: HAHNBAN1:def 4
for x being Element of V holds it . x = - (f . x);

existence
ex b₁ being Functional of V st
for x being Element of V holds b₁ . x = - (f . x)

proof end;

uniqueness
for b₁, b₂ being Functional of V st ( for x being Element of V holds b₁ . x = - (f . x) ) & ( for x being Element of V holds b₂ . x = - (f . x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines - HAHNBAN1:def 4 :
for K being non empty addLoopStr
for V being non empty ModuleStr over K
for f, b₄ being Functional of V holds
( b₄ = - f iff for x being Element of V holds b₄ . x = - (f . x) );

definition

let K be non empty addLoopStr ;
let V be non empty ModuleStr over K;
let f, g be Functional of V;

func f - g -> Functional of V equals :: HAHNBAN1:def 5
f + (- g);

coherence
f + (- g) is Functional of V ;

end;

:: deftheorem defines - HAHNBAN1:def 5 :
for K being non empty addLoopStr
for V being non empty ModuleStr over K
for f, g being Functional of V holds f - g = f + (- g);

definition

let K be non empty multMagma ;
let V be non empty ModuleStr over K;
let v be Element of K;
let f be Functional of V;

func v * f -> Functional of V means :Def6: :: HAHNBAN1:def 6
for x being Element of V holds it . x = v * (f . x);

existence
ex b₁ being Functional of V st
for x being Element of V holds b₁ . x = v * (f . x)

proof end;

uniqueness
for b₁, b₂ being Functional of V st ( for x being Element of V holds b₁ . x = v * (f . x) ) & ( for x being Element of V holds b₂ . x = v * (f . x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines * HAHNBAN1:def 6 :
for K being non empty multMagma
for V being non empty ModuleStr over K
for v being Element of K
for f, b₅ being Functional of V holds
( b₅ = v * f iff for x being Element of V holds b₅ . x = v * (f . x) );

definition

let K be non empty ZeroStr ;
let V be ModuleStr over K;

func 0Functional V -> Functional of V equals :: HAHNBAN1:def 7
([#] V) --> (0. K);

coherence
([#] V) --> (0. K) is Functional of V ;

end;

:: deftheorem defines 0Functional HAHNBAN1:def 7 :
for K being non empty ZeroStr
for V being ModuleStr over K holds 0Functional V = ([#] V) --> (0. K);

definition

let K be non empty multMagma ;
let V be non empty ModuleStr over K;
let F be Functional of V;

attr F is homogeneous means :Def8: :: HAHNBAN1:def 8
for x being Vector of V
for r being Scalar of holds F . (r * x) = r * (F . x);

end;

:: deftheorem Def8 defines homogeneous HAHNBAN1:def 8 :
for K being non empty multMagma
for V being non empty ModuleStr over K
for F being Functional of V holds
( F is homogeneous iff for x being Vector of V
for r being Scalar of holds F . (r * x) = r * (F . x) );

definition

let K be non empty ZeroStr ;
let V be non empty ModuleStr over K;
let F be Functional of V;

attr F is 0-preserving means :: HAHNBAN1:def 9
F . (0. V) = 0. K;

end;

:: deftheorem defines 0-preserving HAHNBAN1:def 9 :
for K being non empty ZeroStr
for V being non empty ModuleStr over K
for F being Functional of V holds
( F is 0-preserving iff F . (0. V) = 0. K );

registration

let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ;
let V be VectSp of K;

cluster Function-like V33( the carrier of V, the carrier of K) homogeneous -> 0-preserving for Element of bool [: the carrier of V, the carrier of K:];

coherence
for b₁ being Functional of V st b₁ is homogeneous holds
b₁ is 0-preserving

proof end;

end;

registration

let K be non empty right_zeroed addLoopStr ;
let V be non empty ModuleStr over K;

cluster 0Functional V -> additive ;

coherence
0Functional V is additive

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty ModuleStr over K;

cluster 0Functional V -> homogeneous ;

coherence
0Functional V is homogeneous

proof end;

end;

registration

let K be non empty ZeroStr ;
let V be non empty ModuleStr over K;

cluster 0Functional V -> 0-preserving ;

coherence
0Functional V is 0-preserving by FUNCOP_1:7;

end;

registration

let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty ModuleStr over K;

cluster V1() V4( the carrier of V) V5( the carrier of K) Function-like V33( the carrier of V, the carrier of K) additive homogeneous 0-preserving for Element of bool [: the carrier of V, the carrier of K:];

existence
ex b₁ being Functional of V st
( b₁ is additive & b₁ is homogeneous & b₁ is 0-preserving )

proof end;

end;

theorem Th10: :: HAHNBAN1:12

for K being non empty Abelian addLoopStr
for V being non empty ModuleStr over K
for f, g being Functional of V holds f + g = g + f

proof end;

theorem Th11: :: HAHNBAN1:13

for K being non empty add-associative addLoopStr
for V being non empty ModuleStr over K
for f, g, h being Functional of V holds (f + g) + h = f + (g + h)

proof end;

theorem :: HAHNBAN1:14

for K being non empty ZeroStr
for V being non empty ModuleStr over K
for x being Element of V holds (0Functional V) . x = 0. K by FUNCOP_1:7;

theorem Th13: :: HAHNBAN1:15

for K being non empty right_zeroed addLoopStr
for V being non empty ModuleStr over K
for f being Functional of V holds f + (0Functional V) = f

proof end;

theorem Th14: :: HAHNBAN1:16

for K being non empty right_complementable add-associative right_zeroed addLoopStr
for V being non empty ModuleStr over K
for f being Functional of V holds f - f = 0Functional V

proof end;

theorem Th15: :: HAHNBAN1:17

for K being non empty right-distributive doubleLoopStr
for V being non empty ModuleStr over K
for r being Element of K
for f, g being Functional of V holds r * (f + g) = (r * f) + (r * g)

proof end;

theorem Th16: :: HAHNBAN1:18

for K being non empty left-distributive doubleLoopStr
for V being non empty ModuleStr over K
for r, s being Element of K
for f being Functional of V holds (r + s) * f = (r * f) + (s * f)

proof end;

theorem Th17: :: HAHNBAN1:19

for K being non empty associative multMagma
for V being non empty ModuleStr over K
for r, s being Element of K
for f being Functional of V holds (r * s) * f = r * (s * f)

proof end;

theorem Th18: :: HAHNBAN1:20

for K being non empty left_unital doubleLoopStr
for V being non empty ModuleStr over K
for f being Functional of V holds (1. K) * f = f

proof end;

registration

let K be non empty right_complementable Abelian add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty ModuleStr over K;
let f, g be additive Functional of V;

cluster f + g -> additive ;

coherence
f + g is additive

proof end;

end;

registration

let K be non empty right_complementable Abelian add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty ModuleStr over K;
let f be additive Functional of V;

cluster - f -> additive ;

coherence
- f is additive

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty ModuleStr over K;
let v be Element of K;
let f be additive Functional of V;

cluster v * f -> additive ;

coherence
v * f is additive

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty ModuleStr over K;
let f, g be homogeneous Functional of V;

cluster f + g -> homogeneous ;

coherence
f + g is homogeneous

proof end;

end;

registration

let K be non empty right_complementable Abelian add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty ModuleStr over K;
let f be homogeneous Functional of V;

cluster - f -> homogeneous ;

coherence
- f is homogeneous

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed right-distributive associative commutative doubleLoopStr ;
let V be non empty ModuleStr over K;
let v be Element of K;
let f be homogeneous Functional of V;

cluster v * f -> homogeneous ;

coherence
v * f is homogeneous

proof end;

end;

definition

let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty ModuleStr over K;
mode linear-Functional of V is additive homogeneous Functional of V;

end;

definition

let K be non empty right_complementable Abelian add-associative right_zeroed right-distributive associative commutative doubleLoopStr ;
let V be non empty ModuleStr over K;

func V *' -> non empty strict ModuleStr over K means :Def10: :: HAHNBAN1:def 10
( ( for x being set holds
( x in the carrier of it iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of it . (f,g) = f + g ) & 0. it = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of it . (x,f) = x * f ) );

existence
ex b₁ being non empty strict ModuleStr over K st
( ( for x being set holds
( x in the carrier of b₁ iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of b₁ . (f,g) = f + g ) & 0. b₁ = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of b₁ . (x,f) = x * f ) )

proof end;

uniqueness
for b₁, b₂ being non empty strict ModuleStr over K st ( for x being set holds
( x in the carrier of b₁ iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of b₁ . (f,g) = f + g ) & 0. b₁ = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of b₁ . (x,f) = x * f ) & ( for x being set holds
( x in the carrier of b₂ iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of b₂ . (f,g) = f + g ) & 0. b₂ = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of b₂ . (x,f) = x * f ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines *' HAHNBAN1:def 10 :
for K being non empty right_complementable Abelian add-associative right_zeroed right-distributive associative commutative doubleLoopStr
for V being non empty ModuleStr over K
for b₃ being non empty strict ModuleStr over K holds
( b₃ = V *' iff ( ( for x being set holds
( x in the carrier of b₃ iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of b₃ . (f,g) = f + g ) & 0. b₃ = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of b₃ . (x,f) = x * f ) ) );

registration

let K be non empty right_complementable Abelian add-associative right_zeroed right-distributive associative commutative doubleLoopStr ;
let V be non empty ModuleStr over K;

cluster V *' -> non empty Abelian strict ;

coherence
V *' is Abelian

proof end;

end;

registration

let K be non empty right_complementable Abelian add-associative right_zeroed right-distributive associative commutative doubleLoopStr ;
let V be non empty ModuleStr over K;

cluster V *' -> non empty add-associative strict ;

coherence
V *' is add-associative

proof end;

cluster V *' -> non empty right_zeroed strict ;

coherence
V *' is right_zeroed

proof end;

cluster V *' -> non empty right_complementable strict ;

coherence
V *' is right_complementable

proof end;

end;

registration

let K be non empty right_complementable Abelian add-associative right_zeroed distributive left_unital associative commutative doubleLoopStr ;
let V be non empty ModuleStr over K;

cluster V *' -> non empty strict vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence
( V *' is vector-distributive & V *' is scalar-distributive & V *' is scalar-associative & V *' is scalar-unital )

proof end;

end;

definition

let K be 1-sorted ;
let V be ModuleStr over K;
mode RFunctional of V is Function of the carrier of V,REAL;

end;

definition

let K be 1-sorted ;
let V be non empty ModuleStr over K;
let F be RFunctional of V;

attr F is subadditive means :Def11: :: HAHNBAN1:def 11
for x, y being Vector of V holds F . (x + y) <= (F . x) + (F . y);

end;

:: deftheorem Def11 defines subadditive HAHNBAN1:def 11 :
for K being 1-sorted
for V being non empty ModuleStr over K
for F being RFunctional of V holds
( F is subadditive iff for x, y being Vector of V holds F . (x + y) <= (F . x) + (F . y) );

definition

let K be 1-sorted ;
let V be non empty ModuleStr over K;
let F be RFunctional of V;

attr F is additive means :Def12: :: HAHNBAN1:def 12
for x, y being Vector of V holds F . (x + y) = (F . x) + (F . y);

end;

:: deftheorem Def12 defines additive HAHNBAN1:def 12 :
for K being 1-sorted
for V being non empty ModuleStr over K
for F being RFunctional of V holds
( F is additive iff for x, y being Vector of V holds F . (x + y) = (F . x) + (F . y) );

definition

let V be non empty ModuleStr over F_Complex ;
let F be RFunctional of V;

attr F is Real_homogeneous means :Def13: :: HAHNBAN1:def 13
for v being Vector of V
for r being Real holds F . ([**r,0**] * v) = r * (F . v);

end;

:: deftheorem Def13 defines Real_homogeneous HAHNBAN1:def 13 :
for V being non empty ModuleStr over F_Complex
for F being RFunctional of V holds
( F is Real_homogeneous iff for v being Vector of V
for r being Real holds F . ([**r,0**] * v) = r * (F . v) );

theorem Th19: :: HAHNBAN1:21

for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F_Complex
for F being RFunctional of V st F is Real_homogeneous holds
for v being Vector of V
for r being Real holds F . ([**0,r**] * v) = r * (F . (i_FC * v))

proof end;

definition

let V be non empty ModuleStr over F_Complex ;
let F be RFunctional of V;

attr F is homogeneous means :Def14: :: HAHNBAN1:def 14
for v being Vector of V
for r being Scalar of holds F . (r * v) = |.r.| * (F . v);

end;

:: deftheorem Def14 defines homogeneous HAHNBAN1:def 14 :
for V being non empty ModuleStr over F_Complex
for F being RFunctional of V holds
( F is homogeneous iff for v being Vector of V
for r being Scalar of holds F . (r * v) = |.r.| * (F . v) );

definition

let K be 1-sorted ;
let V be ModuleStr over K;
let F be RFunctional of V;

attr F is 0-preserving means :: HAHNBAN1:def 15
F . (0. V) = 0 ;

end;

:: deftheorem defines 0-preserving HAHNBAN1:def 15 :
for K being 1-sorted
for V being ModuleStr over K
for F being RFunctional of V holds
( F is 0-preserving iff F . (0. V) = 0 );

registration

let K be 1-sorted ;
let V be non empty ModuleStr over K;

cluster Function-like V33( the carrier of V, REAL ) additive -> subadditive for Element of bool [: the carrier of V,REAL:];

coherence
for b₁ being RFunctional of V st b₁ is additive holds
b₁ is subadditive ;

end;

registration

let V be VectSp of F_Complex ;

cluster Function-like V33( the carrier of V, REAL ) Real_homogeneous -> 0-preserving for Element of bool [: the carrier of V,REAL:];

coherence
for b₁ being RFunctional of V st b₁ is Real_homogeneous holds
b₁ is 0-preserving

proof end;

end;

definition

let K be 1-sorted ;
let V be ModuleStr over K;

func 0RFunctional V -> RFunctional of V equals :: HAHNBAN1:def 16
([#] V) --> 0;

coherence
([#] V) --> 0 is RFunctional of V

proof end;

end;

:: deftheorem defines 0RFunctional HAHNBAN1:def 16 :
for K being 1-sorted
for V being ModuleStr over K holds 0RFunctional V = ([#] V) --> 0;

registration

let K be 1-sorted ;
let V be non empty ModuleStr over K;

cluster 0RFunctional V -> additive ;

coherence
0RFunctional V is additive

proof end;

cluster 0RFunctional V -> 0-preserving ;

coherence
0RFunctional V is 0-preserving by FUNCOP_1:7;

end;

registration

let V be non empty ModuleStr over F_Complex ;

cluster 0RFunctional V -> Real_homogeneous ;

coherence
0RFunctional V is Real_homogeneous

proof end;

cluster 0RFunctional V -> homogeneous ;

coherence
0RFunctional V is homogeneous

proof end;

end;

registration

let K be 1-sorted ;
let V be non empty ModuleStr over K;

cluster V1() V4( the carrier of V) V5( REAL ) Function-like V33( the carrier of V, REAL ) additive 0-preserving for Element of bool [: the carrier of V,REAL:];

existence
ex b₁ being RFunctional of V st
( b₁ is additive & b₁ is 0-preserving )

proof end;

end;

registration

let V be non empty ModuleStr over F_Complex ;

cluster V1() V4( the carrier of V) V5( REAL ) Function-like V33( the carrier of V, REAL ) additive Real_homogeneous homogeneous for Element of bool [: the carrier of V,REAL:];

existence
ex b₁ being RFunctional of V st
( b₁ is additive & b₁ is Real_homogeneous & b₁ is homogeneous )

proof end;

end;

definition

let V be non empty ModuleStr over F_Complex ;
mode Semi-Norm of V is subadditive homogeneous RFunctional of V;

end;

definition

let V be non empty ModuleStr over F_Complex ;

func RealVS V -> strict RLSStruct means :Def17: :: HAHNBAN1:def 17
( addLoopStr(# the carrier of it, the addF of it, the ZeroF of it #) = addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) & ( for r being Real
for v being Vector of V holds the Mult of it . (r,v) = [**r,0**] * v ) );

existence
ex b₁ being strict RLSStruct st
( addLoopStr(# the carrier of b₁, the addF of b₁, the ZeroF of b₁ #) = addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) & ( for r being Real
for v being Vector of V holds the Mult of b₁ . (r,v) = [**r,0**] * v ) )

proof end;

uniqueness
for b₁, b₂ being strict RLSStruct st addLoopStr(# the carrier of b₁, the addF of b₁, the ZeroF of b₁ #) = addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) & ( for r being Real
for v being Vector of V holds the Mult of b₁ . (r,v) = [**r,0**] * v ) & addLoopStr(# the carrier of b₂, the addF of b₂, the ZeroF of b₂ #) = addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) & ( for r being Real
for v being Vector of V holds the Mult of b₂ . (r,v) = [**r,0**] * v ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def17 defines RealVS HAHNBAN1:def 17 :
for V being non empty ModuleStr over F_Complex
for b₂ being strict RLSStruct holds
( b₂ = RealVS V iff ( addLoopStr(# the carrier of b₂, the addF of b₂, the ZeroF of b₂ #) = addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) & ( for r being Real
for v being Vector of V holds the Mult of b₂ . (r,v) = [**r,0**] * v ) ) );

registration

let V be non empty ModuleStr over F_Complex ;

cluster RealVS V -> non empty strict ;

coherence
not RealVS V is empty

proof end;

end;

registration

let V be non empty Abelian ModuleStr over F_Complex ;

cluster RealVS V -> strict Abelian ;

coherence
RealVS V is Abelian

proof end;

end;

registration

let V be non empty add-associative ModuleStr over F_Complex ;

cluster RealVS V -> strict add-associative ;

coherence
RealVS V is add-associative

proof end;

end;

registration

let V be non empty right_zeroed ModuleStr over F_Complex ;

cluster RealVS V -> strict right_zeroed ;

coherence
RealVS V is right_zeroed

proof end;

end;

registration

let V be non empty right_complementable ModuleStr over F_Complex ;

cluster RealVS V -> right_complementable strict ;

coherence
RealVS V is right_complementable

proof end;

end;

registration

let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F_Complex ;

cluster RealVS V -> strict vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence
( RealVS V is vector-distributive & RealVS V is scalar-distributive & RealVS V is scalar-associative & RealVS V is scalar-unital )

proof end;

end;

theorem Th20: :: HAHNBAN1:22

for V being VectSp of F_Complex
for M being Subspace of V holds RealVS M is Subspace of RealVS V

proof end;

theorem Th21: :: HAHNBAN1:23

for V being non empty ModuleStr over F_Complex
for p being RFunctional of V holds p is Functional of (RealVS V)

proof end;

theorem Th22: :: HAHNBAN1:24

for V being VectSp of F_Complex
for p being Semi-Norm of V holds p is Banach-Functional of (RealVS V)

proof end;

definition

let V be non empty ModuleStr over F_Complex ;
let l be Functional of V;

func projRe l -> Functional of (RealVS V) means :Def18: :: HAHNBAN1:def 18
for i being Element of V holds it . i = Re (l . i);

existence
ex b₁ being Functional of (RealVS V) st
for i being Element of V holds b₁ . i = Re (l . i)

proof end;

uniqueness
for b₁, b₂ being Functional of (RealVS V) st ( for i being Element of V holds b₁ . i = Re (l . i) ) & ( for i being Element of V holds b₂ . i = Re (l . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def18 defines projRe HAHNBAN1:def 18 :
for V being non empty ModuleStr over F_Complex
for l being Functional of V
for b₃ being Functional of (RealVS V) holds
( b₃ = projRe l iff for i being Element of V holds b₃ . i = Re (l . i) );

definition

let V be non empty ModuleStr over F_Complex ;
let l be Functional of V;

func projIm l -> Functional of (RealVS V) means :Def19: :: HAHNBAN1:def 19
for i being Element of V holds it . i = Im (l . i);

existence
ex b₁ being Functional of (RealVS V) st
for i being Element of V holds b₁ . i = Im (l . i)

proof end;

uniqueness
for b₁, b₂ being Functional of (RealVS V) st ( for i being Element of V holds b₁ . i = Im (l . i) ) & ( for i being Element of V holds b₂ . i = Im (l . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def19 defines projIm HAHNBAN1:def 19 :
for V being non empty ModuleStr over F_Complex
for l being Functional of V
for b₃ being Functional of (RealVS V) holds
( b₃ = projIm l iff for i being Element of V holds b₃ . i = Im (l . i) );

definition

let V be non empty ModuleStr over F_Complex ;
let l be Functional of (RealVS V);

func RtoC l -> RFunctional of V equals :: HAHNBAN1:def 20
l;

coherence
l is RFunctional of V

proof end;

end;

:: deftheorem defines RtoC HAHNBAN1:def 20 :
for V being non empty ModuleStr over F_Complex
for l being Functional of (RealVS V) holds RtoC l = l;

definition

let V be non empty ModuleStr over F_Complex ;
let l be RFunctional of V;

func CtoR l -> Functional of (RealVS V) equals :: HAHNBAN1:def 21
l;

coherence
l is Functional of (RealVS V)

proof end;

end;

:: deftheorem defines CtoR HAHNBAN1:def 21 :
for V being non empty ModuleStr over F_Complex
for l being RFunctional of V holds CtoR l = l;

registration

let V be VectSp of F_Complex ;
let l be additive Functional of (RealVS V);

cluster RtoC l -> additive ;

coherence
RtoC l is additive

proof end;

end;

registration

let V be VectSp of F_Complex ;
let l be additive RFunctional of V;

cluster CtoR l -> additive ;

coherence
CtoR l is additive

proof end;

end;

registration

let V be VectSp of F_Complex ;
let l be homogeneous Functional of (RealVS V);

cluster RtoC l -> Real_homogeneous ;

coherence
RtoC l is Real_homogeneous

proof end;

end;

registration

let V be VectSp of F_Complex ;
let l be Real_homogeneous RFunctional of V;

cluster CtoR l -> homogeneous ;

coherence
CtoR l is homogeneous

proof end;

end;

definition

let V be non empty ModuleStr over F_Complex ;
let l be RFunctional of V;

func i-shift l -> RFunctional of V means :Def22: :: HAHNBAN1:def 22
for v being Element of V holds it . v = l . (i_FC * v);

existence
ex b₁ being RFunctional of V st
for v being Element of V holds b₁ . v = l . (i_FC * v)

proof end;

uniqueness
for b₁, b₂ being RFunctional of V st ( for v being Element of V holds b₁ . v = l . (i_FC * v) ) & ( for v being Element of V holds b₂ . v = l . (i_FC * v) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def22 defines i-shift HAHNBAN1:def 22 :
for V being non empty ModuleStr over F_Complex
for l, b₃ being RFunctional of V holds
( b₃ = i-shift l iff for v being Element of V holds b₃ . v = l . (i_FC * v) );

definition

let V be non empty ModuleStr over F_Complex ;
let l be Functional of (RealVS V);

func prodReIm l -> Functional of V means :Def23: :: HAHNBAN1:def 23
for v being Element of V holds it . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**];

existence
ex b₁ being Functional of V st
for v being Element of V holds b₁ . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**]

proof end;

uniqueness
for b₁, b₂ being Functional of V st ( for v being Element of V holds b₁ . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] ) & ( for v being Element of V holds b₂ . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def23 defines prodReIm HAHNBAN1:def 23 :
for V being non empty ModuleStr over F_Complex
for l being Functional of (RealVS V)
for b₃ being Functional of V holds
( b₃ = prodReIm l iff for v being Element of V holds b₃ . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] );

theorem Th23: :: HAHNBAN1:25

for V being VectSp of F_Complex
for l being linear-Functional of V holds projRe l is linear-Functional of (RealVS V)

proof end;

theorem :: HAHNBAN1:26

for V being VectSp of F_Complex
for l being linear-Functional of V holds projIm l is linear-Functional of (RealVS V)

proof end;

theorem Th25: :: HAHNBAN1:27

for V being VectSp of F_Complex
for l being linear-Functional of (RealVS V) holds prodReIm l is linear-Functional of V

proof end;

:: Hahn Banach Theorem
:: Hahn-Banach Theorem (complex spaces)

theorem :: HAHNBAN1:28

for V being 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 ) )

proof end;

:: from COMPTRIG, 2006.08.12, A.T.

theorem :: HAHNBAN1:29

for x being Real st x > 0 holds
for n being Nat holds (power F_Complex) . ([**x,0**],n) = [**(x to_power n),0**]

proof end;