:: Hahn Banach Theorem in the Vector Space over the Field ofComplex Numbers
:: by Anna Justyna Milewska
::
:: Received May 23, 2000
:: Copyright (c) 2000 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)
theorem :: HAHNBAN1:1
theorem :: HAHNBAN1:2
theorem :: HAHNBAN1:3
canceled;
theorem :: HAHNBAN1:4
canceled;
theorem Th5: :: HAHNBAN1:5
:: deftheorem defines [** HAHNBAN1:def 1 :
:: deftheorem defines i_FC HAHNBAN1:def 2 :
theorem :: HAHNBAN1:6
canceled;
theorem :: HAHNBAN1:7
canceled;
theorem Th8: :: HAHNBAN1:8
theorem Th9: :: HAHNBAN1:9
theorem :: HAHNBAN1:10
theorem :: HAHNBAN1:11
theorem :: HAHNBAN1:12
theorem :: HAHNBAN1:13
theorem :: HAHNBAN1:14
canceled;
theorem :: HAHNBAN1:15
canceled;
theorem :: HAHNBAN1:16
theorem :: HAHNBAN1:17
:: deftheorem HAHNBAN1:def 3 :
canceled;
:: deftheorem HAHNBAN1:def 4 :
canceled;
:: deftheorem HAHNBAN1:def 5 :
canceled;
:: deftheorem Def6 defines + HAHNBAN1:def 6 :
:: deftheorem Def7 defines - HAHNBAN1:def 7 :
:: deftheorem defines - HAHNBAN1:def 8 :
:: deftheorem Def9 defines * HAHNBAN1:def 9 :
:: deftheorem defines 0Functional HAHNBAN1:def 10 :
:: deftheorem Def11 defines additive HAHNBAN1:def 11 :
:: deftheorem Def12 defines homogeneous HAHNBAN1:def 12 :
:: deftheorem defines 0-preserving HAHNBAN1:def 13 :
theorem :: HAHNBAN1:18
canceled;
theorem :: HAHNBAN1:19
canceled;
theorem Th20: :: HAHNBAN1:20
theorem Th21: :: HAHNBAN1:21
theorem :: HAHNBAN1:22
theorem Th23: :: HAHNBAN1:23
theorem Th24: :: HAHNBAN1:24
theorem Th25: :: HAHNBAN1:25
theorem Th26: :: HAHNBAN1:26
theorem Th27: :: HAHNBAN1:27
theorem Th28: :: HAHNBAN1:28
definition
let K be non
empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive doubleLoopStr ;
let V be non
empty VectSpStr of
K;
func V *' -> non
empty strict VectSpStr of
K means :
Def14:
:: HAHNBAN1:def 14
( ( 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 b1 being non empty strict VectSpStr of K st
( ( for x being set holds
( x in the carrier of b1 iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of b1 . f,g = f + g ) & 0. b1 = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of b1 . x,f = x * f ) )
uniqueness
for b1, b2 being non empty strict VectSpStr of K st ( for x being set holds
( x in the carrier of b1 iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of b1 . f,g = f + g ) & 0. b1 = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of b1 . x,f = x * f ) & ( for x being set holds
( x in the carrier of b2 iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of b2 . f,g = f + g ) & 0. b2 = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of b2 . x,f = x * f ) holds
b1 = b2
end;
:: deftheorem Def14 defines *' HAHNBAN1:def 14 :
:: deftheorem HAHNBAN1:def 15 :
canceled;
:: deftheorem Def16 defines subadditive HAHNBAN1:def 16 :
:: deftheorem Def17 defines additive HAHNBAN1:def 17 :
:: deftheorem Def18 defines Real_homogeneous HAHNBAN1:def 18 :
theorem Th29: :: HAHNBAN1:29
:: deftheorem Def19 defines homogeneous HAHNBAN1:def 19 :
:: deftheorem defines 0-preserving HAHNBAN1:def 20 :
:: deftheorem defines 0RFunctional HAHNBAN1:def 21 :
definition
let V be non
empty VectSpStr of
F_Complex ;
func RealVS V -> strict RLSStruct means :
Def22:
:: HAHNBAN1:def 22
(
addLoopStr(# the
carrier of
it,the
addF of
it,the
U2 of
it #)
= addLoopStr(# the
carrier of
V,the
addF of
V,the
U2 of
V #) & ( for
r being
Real for
v being
Vector of
V holds the
Mult of
it . r,
v = [**r,0 **] * v ) );
existence
ex b1 being strict RLSStruct st
( addLoopStr(# the carrier of b1,the addF of b1,the U2 of b1 #) = addLoopStr(# the carrier of V,the addF of V,the U2 of V #) & ( for r being Real
for v being Vector of V holds the Mult of b1 . r,v = [**r,0 **] * v ) )
uniqueness
for b1, b2 being strict RLSStruct st addLoopStr(# the carrier of b1,the addF of b1,the U2 of b1 #) = addLoopStr(# the carrier of V,the addF of V,the U2 of V #) & ( for r being Real
for v being Vector of V holds the Mult of b1 . r,v = [**r,0 **] * v ) & addLoopStr(# the carrier of b2,the addF of b2,the U2 of b2 #) = addLoopStr(# the carrier of V,the addF of V,the U2 of V #) & ( for r being Real
for v being Vector of V holds the Mult of b2 . r,v = [**r,0 **] * v ) holds
b1 = b2
end;
:: deftheorem Def22 defines RealVS HAHNBAN1:def 22 :
theorem Th30: :: HAHNBAN1:30
theorem Th31: :: HAHNBAN1:31
theorem Th32: :: HAHNBAN1:32
:: deftheorem Def23 defines projRe HAHNBAN1:def 23 :
:: deftheorem Def24 defines projIm HAHNBAN1:def 24 :
:: deftheorem defines RtoC HAHNBAN1:def 25 :
:: deftheorem defines CtoR HAHNBAN1:def 26 :
:: deftheorem Def27 defines i-shift HAHNBAN1:def 27 :
:: deftheorem Def28 defines prodReIm HAHNBAN1:def 28 :
theorem Th33: :: HAHNBAN1:33
theorem :: HAHNBAN1:34
theorem Th35: :: HAHNBAN1:35
theorem :: HAHNBAN1:36
theorem :: HAHNBAN1:37