:: HAHNBAN1 semantic presentation

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

proof end;

theorem :: HAHNBAN1:1

for z being complex number holds abs |.z.| = |.z.| ;

theorem :: HAHNBAN1:2

for x1, y1, x2, y2 being real number holds (x1 + (y1 * )) * (x2 + (y2 * )) = ((x1 * x2) - (y1 * y2)) + (((x1 * y2) + (x2 * y1)) * ) ;

theorem :: HAHNBAN1:3

for r being Real holds [*r,0*] * = [*0,r*]

proof end;

theorem Th4: :: HAHNBAN1:4

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

proof end;

theorem Th5: :: HAHNBAN1:5

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

proof end;

definition

let x, y be Real;
func [**x,y**] -> Element of F_Complex equals :: HAHNBAN1:def 1
x + (y * );
coherence

proof end;

end;

:: deftheorem defines [** HAHNBAN1:def 1 :

definition

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

proof end;

end;

:: deftheorem defines i_FC HAHNBAN1:def 2 :

theorem :: HAHNBAN1:6

( i_FC = [*0,1*] & i_FC = [**0,1**] ) by COMPLEX1:def 8;

theorem :: HAHNBAN1:7

|.i_FC .| = 1 by COMPLEX1:135;

theorem Th8: :: HAHNBAN1:8

i_FC * i_FC = - (1. F_Complex )

proof end;

theorem Th9: :: HAHNBAN1:9

(- (1. F_Complex )) * (- (1. F_Complex )) = 1. F_Complex

proof end;

theorem Th10: :: HAHNBAN1:10

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

proof end;

theorem Th11: :: HAHNBAN1:11

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

proof end;

theorem :: HAHNBAN1:12

for z being complex number holds abs |.z.| = |.z.| ;

theorem :: HAHNBAN1:13

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

theorem Th14: :: HAHNBAN1:14

for r being Real holds [**r,0**] * i_FC = [**0,r**] by COMPLFLD:6;

theorem Th15: :: HAHNBAN1:15

for x, y being Real holds
( Re [**x,y**] = x & Im [**x,y**] = y ) by COMPLEX1:28;

theorem Th16: :: HAHNBAN1:16

for x, y being Element of F_Complex holds
( Re (x + y) = (Re x) + (Re y) & Im (x + y) = (Im x) + (Im y) )

proof end;

theorem Th17: :: HAHNBAN1:17

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)) )

proof end;

definition

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

end;

definition

let K be non empty LoopStr ;
let V be non empty VectSpStr of K;
let f, g be Functional of V;
canceled;
canceled;
canceled;
func f + g -> Functional of V means :Def6: :: HAHNBAN1:def 6
for x being Element of V holds it . x = (f . x) + (g . x);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem HAHNBAN1:def 3 :

:: deftheorem HAHNBAN1:def 4 :

:: deftheorem HAHNBAN1:def 5 :

:: deftheorem Def6 defines + HAHNBAN1:def 6 :

definition

let K be non empty LoopStr ;
let V be non empty VectSpStr of K;
let f be Functional of V;
func - f -> Functional of V means :Def7: :: HAHNBAN1:def 7
for x being Element of V holds it . x = - (f . x);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines - HAHNBAN1:def 7 :

definition

let K be non empty LoopStr ;
let V be non empty VectSpStr of K;
let f, g be Functional of V;
func f - g -> Functional of V equals :: HAHNBAN1:def 8
f + (- g);
coherence ;

end;

:: deftheorem defines - HAHNBAN1:def 8 :

definition

let K be non empty HGrStr ;
let V be non empty VectSpStr of K;
let v be Element of K;
let f be Functional of V;
func v * f -> Functional of V means :Def9: :: HAHNBAN1:def 9
for x being Element of V holds it . x = v * (f . x);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines * HAHNBAN1:def 9 :

definition

let K be non empty ZeroStr ;
let V be VectSpStr of K;
func 0Functional V -> Functional of V equals :: HAHNBAN1:def 10
([#] V) --> (0. K);
coherence

proof end;

end;

:: deftheorem defines 0Functional HAHNBAN1:def 10 :

definition

let K be non empty LoopStr ;
let V be non empty VectSpStr of K;
let F be Functional of V;
attr F is additive means :Def11: :: HAHNBAN1:def 11
for x, y being Vector of V holds F . (x + y) = (F . x) + (F . y);

end;

:: deftheorem Def11 defines additive HAHNBAN1:def 11 :

definition

let K be non empty HGrStr ;
let V be non empty VectSpStr of K;
let F be Functional of V;
attr F is homogeneous means :Def12: :: HAHNBAN1:def 12
for x being Vector of V
for r being Scalar of holds F . (r * x) = r * (F . x);

end;

:: deftheorem Def12 defines homogeneous HAHNBAN1:def 12 :

definition

let K be non empty ZeroStr ;
let V be non empty VectSpStr of K;
let F be Functional of V;
attr F is 0-preserving means :: HAHNBAN1:def 13
F . (0. V) = 0. K;

end;

:: deftheorem defines 0-preserving HAHNBAN1:def 13 :

registration

let K be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let V be VectSp of K;
cluster homogeneous -> 0-preserving Relation of the carrier of V,the carrier of K;
coherence

proof end;

end;

registration

let K be non empty right_zeroed LoopStr ;
let V be non empty VectSpStr of K;
cluster 0Functional V -> additive ;
coherence

proof end;

end;

registration

let K be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let V be non empty VectSpStr of K;
cluster 0Functional V -> additive homogeneous ;
coherence

proof end;

end;

registration

let K be non empty ZeroStr ;
let V be non empty VectSpStr of K;
cluster 0Functional V -> 0-preserving ;
coherence

proof end;

end;

registration

let K be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let V be non empty VectSpStr of K;
cluster additive homogeneous 0-preserving Relation of the carrier of V,the carrier of K;
existence

proof end;

end;

theorem :: HAHNBAN1:18

canceled;

theorem :: HAHNBAN1:19

canceled;

theorem Th20: :: HAHNBAN1:20

for K being non empty Abelian LoopStr
for V being non empty VectSpStr of K
for f, g being Functional of V holds f + g = g + f

proof end;

theorem Th21: :: HAHNBAN1:21

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

proof end;

theorem Th22: :: HAHNBAN1:22

for K being non empty ZeroStr
for V being non empty VectSpStr of K
for x being Element of V holds (0Functional V) . x = 0. K

proof end;

theorem Th23: :: HAHNBAN1:23

for K being non empty right_zeroed LoopStr
for V being non empty VectSpStr of K
for f being Functional of V holds f + (0Functional V) = f

proof end;

theorem Th24: :: HAHNBAN1:24

for K being non empty add-associative right_zeroed right_complementable LoopStr
for V being non empty VectSpStr of K
for f being Functional of V holds f - f = 0Functional V

proof end;

theorem Th25: :: HAHNBAN1:25

for K being non empty right-distributive doubleLoopStr
for V being non empty VectSpStr of 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 Th26: :: HAHNBAN1:26

for K being non empty left-distributive doubleLoopStr
for V being non empty VectSpStr of 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 Th27: :: HAHNBAN1:27

for K being non empty associative HGrStr
for V being non empty VectSpStr of K
for r, s being Element of K
for f being Functional of V holds (r * s) * f = r * (s * f)

proof end;

theorem Th28: :: HAHNBAN1:28

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

proof end;

registration

let K be non empty Abelian add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let V be non empty VectSpStr of K;
let f, g be additive Functional of V;
cluster f + g -> additive ;
coherence

proof end;

end;

registration

let K be non empty Abelian add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let V be non empty VectSpStr of K;
let f be additive Functional of V;
cluster - f -> additive ;
coherence

proof end;

end;

registration

let K be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let V be non empty VectSpStr of K;
let v be Element of K;
let f be additive Functional of V;
cluster v * f -> additive ;
coherence

proof end;

end;

registration

let K be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let V be non empty VectSpStr of K;
let f, g be homogeneous Functional of V;
cluster f + g -> homogeneous ;
coherence

proof end;

end;

registration

let K be non empty Abelian add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let V be non empty VectSpStr of K;
let f be homogeneous Functional of V;
cluster - f -> homogeneous ;
coherence

proof end;

end;

registration

let K be non empty add-associative right_zeroed right_complementable associative commutative right-distributive doubleLoopStr ;
let V be non empty VectSpStr of K;
let v be Element of K;
let f be homogeneous Functional of V;
cluster v * f -> homogeneous ;
coherence

proof end;

end;

definition

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

end;

definition

let K be non empty Abelian add-associative right_zeroed right_complementable 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 add of it . f,g = f + g ) & the Zero of 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines *' HAHNBAN1:def 14 :

registration

proof end;

end;

registration

proof end;

cluster V *' -> non empty Abelian right_zeroed strict ;
coherence

proof end;

cluster V *' -> non empty Abelian right_complementable strict ;
coherence

proof end;

end;

registration

let K be non empty Abelian add-associative right_zeroed right_complementable associative commutative distributive left_unital doubleLoopStr ;
let V be non empty VectSpStr of K;
cluster V *' -> non empty Abelian add-associative right_zeroed right_complementable strict VectSp-like ;
coherence

proof end;

end;

definition

let K be 1-sorted ;
let V be VectSpStr of 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 VectSpStr of K;
let F be RFunctional of V;
canceled;
attr F is subadditive means :Def16: :: HAHNBAN1:def 16
for x, y being Vector of V holds F . (x + y) <= (F . x) + (F . y);

end;

:: deftheorem HAHNBAN1:def 15 :

:: deftheorem Def16 defines subadditive HAHNBAN1:def 16 :

definition

let K be 1-sorted ;
let V be non empty VectSpStr of K;
let F be RFunctional of V;
attr F is additive means :Def17: :: HAHNBAN1:def 17
for x, y being Vector of V holds F . (x + y) = (F . x) + (F . y);

end;

:: deftheorem Def17 defines additive HAHNBAN1:def 17 :

definition

let V be non empty VectSpStr of F_Complex ;
let F be RFunctional of V;
attr F is Real_homogeneous means :Def18: :: HAHNBAN1:def 18
for v being Vector of V
for r being Real holds F . ([**r,0**] * v) = r * (F . v);

end;

:: deftheorem Def18 defines Real_homogeneous HAHNBAN1:def 18 :

theorem Th29: :: HAHNBAN1:29

for V being non empty VectSp-like VectSpStr of 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 VectSpStr of F_Complex ;
let F be RFunctional of V;
attr F is homogeneous means :Def19: :: HAHNBAN1:def 19
for v being Vector of V
for r being Scalar of holds F . (r * v) = |.r.| * (F . v);

end;

:: deftheorem Def19 defines homogeneous HAHNBAN1:def 19 :

definition

let K be 1-sorted ;
let V be VectSpStr of K;
let F be RFunctional of V;
attr F is 0-preserving means :: HAHNBAN1:def 20
F . (0. V) = 0;

end;

:: deftheorem defines 0-preserving HAHNBAN1:def 20 :

registration

let K be 1-sorted ;
let V be non empty VectSpStr of K;
cluster additive -> subadditive Relation of the carrier of V, REAL ;
coherence

proof end;

end;

Lm2: 0c = [*0,0*]
by ARYTM_0:def 7, COMPLEX1:def 6;

Lm3: 1r = [*1,0*]
by ARYTM_0:def 7, COMPLEX1:def 7;

registration

let V be VectSp of F_Complex ;
cluster Real_homogeneous -> 0-preserving Relation of the carrier of V, REAL ;
coherence

proof end;

end;

definition

let K be 1-sorted ;
let V be VectSpStr of K;
func 0RFunctional V -> RFunctional of V equals :: HAHNBAN1:def 21
([#] V) --> 0;
coherence

proof end;

end;

:: deftheorem defines 0RFunctional HAHNBAN1:def 21 :

registration

let K be 1-sorted ;
let V be non empty VectSpStr of K;
cluster 0RFunctional V -> subadditive additive ;
coherence

proof end;

cluster 0RFunctional V -> 0-preserving ;
coherence

proof end;

end;

registration

let V be non empty VectSpStr of F_Complex ;
cluster 0RFunctional V -> subadditive additive Real_homogeneous 0-preserving ;
coherence

proof end;

cluster 0RFunctional V -> subadditive additive homogeneous 0-preserving ;
coherence

proof end;

end;

registration

let K be 1-sorted ;
let V be non empty VectSpStr of K;
cluster subadditive additive 0-preserving Relation of the carrier of V, REAL ;
existence

proof end;

end;

registration

let V be non empty VectSpStr of F_Complex ;
cluster subadditive additive Real_homogeneous homogeneous Relation of the carrier of V, REAL ;
existence

proof end;

end;

definition

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

end;

definition

let V be non empty VectSpStr of F_Complex ;
func RealVS V -> strict RLSStruct means :Def22: :: HAHNBAN1:def 22
( LoopStr(# the carrier of it,the add of it,the Zero of it #) = LoopStr(# the carrier of V,the add of V,the Zero of V #) & ( for r being Real
for v being Vector of V holds the Mult of it . r,v = [**r,0**] * v ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def22 defines RealVS HAHNBAN1:def 22 :

registration

let V be non empty VectSpStr of F_Complex ;
cluster RealVS V -> non empty strict ;
coherence

proof end;

end;

registration

let V be non empty Abelian VectSpStr of F_Complex ;
cluster RealVS V -> non empty strict Abelian ;
coherence

proof end;

end;

registration

let V be non empty add-associative VectSpStr of F_Complex ;
cluster RealVS V -> non empty strict add-associative ;
coherence

proof end;

end;

registration

let V be non empty right_zeroed VectSpStr of F_Complex ;
cluster RealVS V -> non empty strict right_zeroed ;
coherence

proof end;

end;

registration

let V be non empty right_complementable VectSpStr of F_Complex ;
cluster RealVS V -> non empty strict right_complementable ;
coherence

proof end;

end;

registration

let V be non empty VectSp-like VectSpStr of F_Complex ;
cluster RealVS V -> non empty strict RealLinearSpace-like ;
coherence

proof end;

end;

theorem Th30: :: HAHNBAN1:30

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

proof end;

theorem Th31: :: HAHNBAN1:31

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

proof end;

theorem Th32: :: HAHNBAN1:32

for V being non empty 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 VectSpStr of F_Complex ;
let l be Functional of V;
func projRe l -> Functional of (RealVS V) means :Def23: :: HAHNBAN1:def 23
for i being Element of V holds it . i = Re (l . i);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def23 defines projRe HAHNBAN1:def 23 :

definition

let V be non empty VectSpStr of F_Complex ;
let l be Functional of V;
func projIm l -> Functional of (RealVS V) means :Def24: :: HAHNBAN1:def 24
for i being Element of V holds it . i = Im (l . i);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def24 defines projIm HAHNBAN1:def 24 :

definition

let V be non empty VectSpStr of F_Complex ;
let l be Functional of (RealVS V);
func RtoC l -> RFunctional of V equals :: HAHNBAN1:def 25
l;
coherence

proof end;

end;

:: deftheorem defines RtoC HAHNBAN1:def 25 :

definition

let V be non empty VectSpStr of F_Complex ;
let l be RFunctional of V;
func CtoR l -> Functional of (RealVS V) equals :: HAHNBAN1:def 26
l;
coherence

proof end;

end;

:: deftheorem defines CtoR HAHNBAN1:def 26 :

registration

let V be non empty VectSp of F_Complex ;
let l be additive Functional of (RealVS V);
cluster RtoC l -> subadditive additive ;
coherence

proof end;

end;

registration

let V be non empty VectSp of F_Complex ;
let l be additive RFunctional of V;
cluster CtoR l -> additive ;
coherence

proof end;

end;

registration

let V be non empty VectSp of F_Complex ;
let l be homogeneous Functional of (RealVS V);
cluster RtoC l -> Real_homogeneous 0-preserving ;
coherence

proof end;

end;

registration

let V be non empty VectSp of F_Complex ;
let l be Real_homogeneous RFunctional of V;
cluster CtoR l -> homogeneous ;
coherence

proof end;

end;

definition

let V be non empty VectSpStr of F_Complex ;
let l be RFunctional of V;
func i-shift l -> RFunctional of V means :Def27: :: HAHNBAN1:def 27
for v being Element of V holds it . v = l . (i_FC * v);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def27 defines i-shift HAHNBAN1:def 27 :

definition

let V be non empty VectSpStr of F_Complex ;
let l be Functional of (RealVS V);
func prodReIm l -> Functional of V means :Def28: :: HAHNBAN1:def 28
for v being Element of V holds it . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def28 defines prodReIm HAHNBAN1:def 28 :

theorem Th33: :: HAHNBAN1:33

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

proof end;

theorem :: HAHNBAN1:34

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

proof end;

theorem Th35: :: HAHNBAN1:35

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

proof end;

theorem :: HAHNBAN1:36

for V being non empty 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;