:: by Anna Justyna Milewska

::

:: Received May 23, 2000

:: Copyright (c) 2000-2012 Association of Mizar Users

begin

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:2

begin

definition
end;

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

for x, y being real number holds [**x,y**] = x + (y * <i>);

for x, y being real number holds [**x,y**] = x + (y * <i>);

theorem :: HAHNBAN1:6

theorem :: HAHNBAN1:7

theorem :: HAHNBAN1:10

theorem :: HAHNBAN1:11

begin

definition

let K be 1-sorted ;

let V be VectSpStr over K;

mode Functional of V is Function of the carrier of V, the carrier of K;

end;
let V be VectSpStr over K;

mode Functional of V is Function of the carrier of V, the carrier of K;

definition

let K be non empty addLoopStr ;

let V be non empty VectSpStr over K;

let f, g be Functional of V;

ex b_{1} being Functional of V st

for x being Element of V holds b_{1} . x = (f . x) + (g . x)

for b_{1}, b_{2} being Functional of V st ( for x being Element of V holds b_{1} . x = (f . x) + (g . x) ) & ( for x being Element of V holds b_{2} . x = (f . x) + (g . x) ) holds

b_{1} = b_{2}

end;
let V be non empty VectSpStr 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 for x being Element of V holds it . x = (f . x) + (g . x);

ex b

for x being Element of V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines + HAHNBAN1:def 3 :

for K being non empty addLoopStr

for V being non empty VectSpStr over K

for f, g, b_{5} being Functional of V holds

( b_{5} = f + g iff for x being Element of V holds b_{5} . x = (f . x) + (g . x) );

for K being non empty addLoopStr

for V being non empty VectSpStr over K

for f, g, b

( b

definition

let K be non empty addLoopStr ;

let V be non empty VectSpStr over K;

let f be Functional of V;

ex b_{1} being Functional of V st

for x being Element of V holds b_{1} . x = - (f . x)

for b_{1}, b_{2} being Functional of V st ( for x being Element of V holds b_{1} . x = - (f . x) ) & ( for x being Element of V holds b_{2} . x = - (f . x) ) holds

b_{1} = b_{2}

end;
let V be non empty VectSpStr 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 for x being Element of V holds it . x = - (f . x);

ex b

for x being Element of V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines - HAHNBAN1:def 4 :

for K being non empty addLoopStr

for V being non empty VectSpStr over K

for f, b_{4} being Functional of V holds

( b_{4} = - f iff for x being Element of V holds b_{4} . x = - (f . x) );

for K being non empty addLoopStr

for V being non empty VectSpStr over K

for f, b

( b

definition

let K be non empty addLoopStr ;

let V be non empty VectSpStr over K;

let f, g be Functional of V;

coherence

f + (- g) is Functional of V ;

end;
let V be non empty VectSpStr over K;

let f, g be Functional of V;

coherence

f + (- g) is Functional of V ;

:: deftheorem defines - HAHNBAN1:def 5 :

for K being non empty addLoopStr

for V being non empty VectSpStr over K

for f, g being Functional of V holds f - g = f + (- g);

for K being non empty addLoopStr

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

let v be Element of K;

let f be Functional of V;

ex b_{1} being Functional of V st

for x being Element of V holds b_{1} . x = v * (f . x)

for b_{1}, b_{2} being Functional of V st ( for x being Element of V holds b_{1} . x = v * (f . x) ) & ( for x being Element of V holds b_{2} . x = v * (f . x) ) holds

b_{1} = b_{2}

end;
let V be non empty VectSpStr 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 for x being Element of V holds it . x = v * (f . x);

ex b

for x being Element of V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines * HAHNBAN1:def 6 :

for K being non empty multMagma

for V being non empty VectSpStr over K

for v being Element of K

for f, b_{5} being Functional of V holds

( b_{5} = v * f iff for x being Element of V holds b_{5} . x = v * (f . x) );

for K being non empty multMagma

for V being non empty VectSpStr over K

for v being Element of K

for f, b

( b

definition

let K be non empty ZeroStr ;

let V be VectSpStr over K;

coherence

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

end;
let V be VectSpStr over K;

coherence

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

:: deftheorem defines 0Functional HAHNBAN1:def 7 :

for K being non empty ZeroStr

for V being VectSpStr over K holds 0Functional V = ([#] V) --> (0. K);

for K being non empty ZeroStr

for V being VectSpStr over K holds 0Functional V = ([#] V) --> (0. K);

definition

let K be non empty multMagma ;

let V be non empty VectSpStr over K;

let F be Functional of V;

end;
let V be non empty VectSpStr 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);

for x being Vector of V

for r being Scalar of holds F . (r * x) = r * (F . x);

:: deftheorem Def8 defines homogeneous HAHNBAN1:def 8 :

for K being non empty multMagma

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

for K being non empty multMagma

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

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

for K being non empty ZeroStr

for V being non empty VectSpStr over K

for F being Functional of V holds

( F is 0-preserving iff F . (0. V) = 0. K );

for K being non empty ZeroStr

for V being non empty VectSpStr 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 associative well-unital distributive doubleLoopStr ;

let V be VectSp of K;

for b_{1} being Functional of V st b_{1} is homogeneous holds

b_{1} is 0-preserving

end;
let V be VectSp of K;

cluster Function-like V30( 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

b

proof end;

registration

let K be non empty right_zeroed addLoopStr ;

let V be non empty VectSpStr over K;

coherence

0Functional V is additive

end;
let V be non empty VectSpStr over K;

coherence

0Functional V is additive

proof end;

registration

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

let V be non empty VectSpStr over K;

coherence

0Functional V is homogeneous

end;
let V be non empty VectSpStr over K;

coherence

0Functional V is homogeneous

proof end;

registration

let K be non empty ZeroStr ;

let V be non empty VectSpStr over K;

coherence

0Functional V is 0-preserving

end;
let V be non empty VectSpStr over K;

coherence

0Functional V is 0-preserving

proof end;

registration

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

let V be non empty VectSpStr over K;

ex b_{1} being Functional of V st

( b_{1} is additive & b_{1} is homogeneous & b_{1} is 0-preserving )

end;
let V be non empty VectSpStr over K;

cluster V16() V19( the carrier of V) V20( the carrier of K) Function-like V30( 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

( b

proof end;

theorem Th12: :: HAHNBAN1:12

for K being non empty Abelian addLoopStr

for V being non empty VectSpStr over K

for f, g being Functional of V holds f + g = g + f

for V being non empty VectSpStr over K

for f, g being Functional of V holds f + g = g + f

proof end;

theorem Th13: :: HAHNBAN1:13

for K being non empty add-associative addLoopStr

for V being non empty VectSpStr over K

for f, g, h being Functional of V holds (f + g) + h = f + (g + h)

for V being non empty VectSpStr 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 VectSpStr over K

for x being Element of V holds (0Functional V) . x = 0. K by FUNCOP_1:7;

for V being non empty VectSpStr over K

for x being Element of V holds (0Functional V) . x = 0. K by FUNCOP_1:7;

theorem Th15: :: HAHNBAN1:15

for K being non empty right_zeroed addLoopStr

for V being non empty VectSpStr over K

for f being Functional of V holds f + (0Functional V) = f

for V being non empty VectSpStr over K

for f being Functional of V holds f + (0Functional V) = f

proof end;

theorem Th16: :: HAHNBAN1:16

for K being non empty right_complementable add-associative right_zeroed addLoopStr

for V being non empty VectSpStr over K

for f being Functional of V holds f - f = 0Functional V

for V being non empty VectSpStr over K

for f being Functional of V holds f - f = 0Functional V

proof end;

theorem Th17: :: HAHNBAN1:17

for K being non empty right-distributive doubleLoopStr

for V being non empty VectSpStr over K

for r being Element of K

for f, g being Functional of V holds r * (f + g) = (r * f) + (r * g)

for V being non empty VectSpStr 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 Th18: :: HAHNBAN1:18

for K being non empty left-distributive doubleLoopStr

for V being non empty VectSpStr over K

for r, s being Element of K

for f being Functional of V holds (r + s) * f = (r * f) + (s * f)

for V being non empty VectSpStr 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 Th19: :: HAHNBAN1:19

for K being non empty associative multMagma

for V being non empty VectSpStr over K

for r, s being Element of K

for f being Functional of V holds (r * s) * f = r * (s * f)

for V being non empty VectSpStr 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 Th20: :: HAHNBAN1:20

for K being non empty left_unital doubleLoopStr

for V being non empty VectSpStr over K

for f being Functional of V holds (1. K) * f = f

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

let f, g be additive Functional of V;

coherence

f + g is additive

end;
let V be non empty VectSpStr over K;

let f, g be additive Functional of V;

coherence

f + g is additive

proof end;

registration

let K be non empty right_complementable Abelian add-associative right_zeroed right-distributive doubleLoopStr ;

let V be non empty VectSpStr over K;

let f be additive Functional of V;

coherence

- f is additive

end;
let V be non empty VectSpStr over K;

let f be additive Functional of V;

coherence

- f is additive

proof end;

registration

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

let V be non empty VectSpStr over K;

let v be Element of K;

let f be additive Functional of V;

coherence

v * f is additive

end;
let V be non empty VectSpStr over K;

let v be Element of K;

let f be additive Functional of V;

coherence

v * f is additive

proof end;

registration

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

let V be non empty VectSpStr over K;

let f, g be homogeneous Functional of V;

coherence

f + g is homogeneous

end;
let V be non empty VectSpStr over K;

let f, g be homogeneous Functional of V;

coherence

f + g is homogeneous

proof end;

registration

let K be non empty right_complementable Abelian add-associative right_zeroed right-distributive doubleLoopStr ;

let V be non empty VectSpStr over K;

let f be homogeneous Functional of V;

coherence

- f is homogeneous

end;
let V be non empty VectSpStr over K;

let f be homogeneous Functional of V;

coherence

- f is homogeneous

proof end;

registration

let K be non empty right_complementable add-associative right_zeroed associative commutative right-distributive doubleLoopStr ;

let V be non empty VectSpStr over K;

let v be Element of K;

let f be homogeneous Functional of V;

coherence

v * f is homogeneous

end;
let V be non empty VectSpStr over K;

let v be Element of K;

let f be homogeneous Functional of V;

coherence

v * f is homogeneous

proof end;

definition

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

let V be non empty VectSpStr over K;

mode linear-Functional of V is additive homogeneous Functional of V;

end;
let V be non empty VectSpStr over K;

mode linear-Functional of V is additive homogeneous Functional of V;

begin

definition

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

let V be non empty VectSpStr over K;

ex b_{1} being non empty strict VectSpStr over K st

( ( for x being set holds

( x in the carrier of b_{1} iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of b_{1} . (f,g) = f + g ) & 0. b_{1} = 0Functional V & ( for f being linear-Functional of V

for x being Element of K holds the lmult of b_{1} . (x,f) = x * f ) )

for b_{1}, b_{2} being non empty strict VectSpStr over K st ( for x being set holds

( x in the carrier of b_{1} iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of b_{1} . (f,g) = f + g ) & 0. b_{1} = 0Functional V & ( for f being linear-Functional of V

for x being Element of K holds the lmult of b_{1} . (x,f) = x * f ) & ( for x being set holds

( x in the carrier of b_{2} iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of b_{2} . (f,g) = f + g ) & 0. b_{2} = 0Functional V & ( for f being linear-Functional of V

for x being Element of K holds the lmult of b_{2} . (x,f) = x * f ) holds

b_{1} = b_{2}

end;
let V be non empty VectSpStr over K;

func V *' -> non empty strict VectSpStr 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 ( ( 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 ) );

ex b

( ( for x being set holds

( x in the carrier of b

for x being Element of K holds the lmult of b

proof end;

uniqueness for b

( x in the carrier of b

for x being Element of K holds the lmult of b

( x in the carrier of b

for x being Element of K holds the lmult of b

b

proof end;

:: deftheorem Def10 defines *' HAHNBAN1:def 10 :

for K being non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive doubleLoopStr

for V being non empty VectSpStr over K

for b_{3} being non empty strict VectSpStr over K holds

( b_{3} = V *' iff ( ( for x being set holds

( x in the carrier of b_{3} iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of b_{3} . (f,g) = f + g ) & 0. b_{3} = 0Functional V & ( for f being linear-Functional of V

for x being Element of K holds the lmult of b_{3} . (x,f) = x * f ) ) );

for K being non empty right_complementable Abelian add-associative right_zeroed associative commutative right-distributive doubleLoopStr

for V being non empty VectSpStr over K

for b

( b

( x in the carrier of b

for x being Element of K holds the lmult of b

registration

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

let V be non empty VectSpStr over K;

coherence

V *' is Abelian

end;
let V be non empty VectSpStr over K;

coherence

V *' is Abelian

proof end;

registration

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

let V be non empty VectSpStr over K;

coherence

V *' is add-associative

V *' is right_zeroed

V *' is right_complementable

end;
let V be non empty VectSpStr over K;

coherence

V *' is add-associative

proof end;

coherence V *' is right_zeroed

proof end;

coherence V *' is right_complementable

proof end;

registration

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

let V be non empty VectSpStr over K;

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

end;
let V be non empty VectSpStr 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;

begin

definition

let K be 1-sorted ;

let V be VectSpStr over K;

mode RFunctional of V is Function of the carrier of V,REAL;

end;
let V be VectSpStr over K;

mode RFunctional of V is Function of the carrier of V,REAL;

definition

let K be 1-sorted ;

let V be non empty VectSpStr over K;

let F be RFunctional of V;

end;
let V be non empty VectSpStr 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);

for x, y being Vector of V holds F . (x + y) <= (F . x) + (F . y);

:: deftheorem Def11 defines subadditive HAHNBAN1:def 11 :

for K being 1-sorted

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

for K being 1-sorted

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

:: deftheorem Def12 defines additive HAHNBAN1:def 12 :

for K being 1-sorted

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

for K being 1-sorted

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

:: deftheorem Def13 defines Real_homogeneous HAHNBAN1:def 13 :

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

for V being non empty VectSpStr 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 Th21: :: HAHNBAN1:21

for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr 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))

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;

:: deftheorem Def14 defines homogeneous HAHNBAN1:def 14 :

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

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

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

for K being 1-sorted

for V being VectSpStr over K

for F being RFunctional of V holds

( F is 0-preserving iff F . (0. V) = 0 );

for K being 1-sorted

for V being VectSpStr 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 VectSpStr over K;

for b_{1} being RFunctional of V st b_{1} is additive holds

b_{1} is subadditive

end;
let V be non empty VectSpStr over K;

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

coherence for b

b

proof end;

registration

let V be VectSp of F_Complex ;

for b_{1} being RFunctional of V st b_{1} is Real_homogeneous holds

b_{1} is 0-preserving

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

coherence for b

b

proof end;

definition
end;

:: deftheorem defines 0RFunctional HAHNBAN1:def 16 :

for K being 1-sorted

for V being VectSpStr over K holds 0RFunctional V = ([#] V) --> 0;

for K being 1-sorted

for V being VectSpStr over K holds 0RFunctional V = ([#] V) --> 0;

registration

let K be 1-sorted ;

let V be non empty VectSpStr over K;

coherence

0RFunctional V is additive

0RFunctional V is 0-preserving

end;
let V be non empty VectSpStr over K;

coherence

0RFunctional V is additive

proof end;

coherence 0RFunctional V is 0-preserving

proof end;

registration

let V be non empty VectSpStr over F_Complex ;

coherence

0RFunctional V is Real_homogeneous

0RFunctional V is homogeneous

end;
coherence

0RFunctional V is Real_homogeneous

proof end;

coherence 0RFunctional V is homogeneous

proof end;

registration

let K be 1-sorted ;

let V be non empty VectSpStr over K;

ex b_{1} being RFunctional of V st

( b_{1} is additive & b_{1} is 0-preserving )

end;
let V be non empty VectSpStr over K;

cluster V16() V19( the carrier of V) V20( REAL ) Function-like V30( the carrier of V, REAL ) additive 0-preserving for Element of bool [: the carrier of V,REAL:];

existence ex b

( b

proof end;

registration

let V be non empty VectSpStr over F_Complex ;

ex b_{1} being RFunctional of V st

( b_{1} is additive & b_{1} is Real_homogeneous & b_{1} is homogeneous )

end;
cluster V16() V19( the carrier of V) V20( REAL ) Function-like V30( the carrier of V, REAL ) additive Real_homogeneous homogeneous for Element of bool [: the carrier of V,REAL:];

existence ex b

( b

proof end;

definition

let V be non empty VectSpStr over F_Complex ;

mode Semi-Norm of V is subadditive homogeneous RFunctional of V;

end;
mode Semi-Norm of V is subadditive homogeneous RFunctional of V;

begin

definition

let V be non empty VectSpStr over F_Complex ;

ex b_{1} being strict RLSStruct st

( addLoopStr(# the carrier of b_{1}, the addF of b_{1}, the ZeroF of b_{1} #) = 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_{1} . (r,v) = [**r,0**] * v ) )

for b_{1}, b_{2} being strict RLSStruct st addLoopStr(# the carrier of b_{1}, the addF of b_{1}, the ZeroF of b_{1} #) = 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_{1} . (r,v) = [**r,0**] * v ) & addLoopStr(# the carrier of b_{2}, the addF of b_{2}, the ZeroF of b_{2} #) = 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_{2} . (r,v) = [**r,0**] * v ) holds

b_{1} = b_{2}

end;
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 ( 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 ) );

ex b

( addLoopStr(# the carrier of b

for v being Vector of V holds the Mult of b

proof end;

uniqueness for b

for v being Vector of V holds the Mult of b

for v being Vector of V holds the Mult of b

b

proof end;

:: deftheorem Def17 defines RealVS HAHNBAN1:def 17 :

for V being non empty VectSpStr over F_Complex

for b_{2} being strict RLSStruct holds

( b_{2} = RealVS V iff ( addLoopStr(# the carrier of b_{2}, the addF of b_{2}, the ZeroF of b_{2} #) = 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_{2} . (r,v) = [**r,0**] * v ) ) );

for V being non empty VectSpStr over F_Complex

for b

( b

for v being Vector of V holds the Mult of b

registration
end;

registration
end;

registration

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

coherence

RealVS V is add-associative

end;
coherence

RealVS V is add-associative

proof end;

registration

let V be non empty right_zeroed VectSpStr over F_Complex ;

coherence

RealVS V is right_zeroed

end;
coherence

RealVS V is right_zeroed

proof end;

registration

let V be non empty right_complementable VectSpStr over F_Complex ;

coherence

RealVS V is right_complementable

end;
coherence

RealVS V is right_complementable

proof end;

registration

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

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

end;
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;

theorem Th23: :: HAHNBAN1:23

for V being non empty VectSpStr over F_Complex

for p being RFunctional of V holds p is Functional of (RealVS V)

for p being RFunctional of V holds p is Functional of (RealVS V)

proof end;

theorem Th24: :: HAHNBAN1:24

for V being VectSp of F_Complex

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

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

proof end;

definition

let V be non empty VectSpStr over F_Complex ;

let l be Functional of V;

ex b_{1} being Functional of (RealVS V) st

for i being Element of V holds b_{1} . i = Re (l . i)

for b_{1}, b_{2} being Functional of (RealVS V) st ( for i being Element of V holds b_{1} . i = Re (l . i) ) & ( for i being Element of V holds b_{2} . i = Re (l . i) ) holds

b_{1} = b_{2}

end;
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 for i being Element of V holds it . i = Re (l . i);

ex b

for i being Element of V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def18 defines projRe HAHNBAN1:def 18 :

for V being non empty VectSpStr over F_Complex

for l being Functional of V

for b_{3} being Functional of (RealVS V) holds

( b_{3} = projRe l iff for i being Element of V holds b_{3} . i = Re (l . i) );

for V being non empty VectSpStr over F_Complex

for l being Functional of V

for b

( b

definition

let V be non empty VectSpStr over F_Complex ;

let l be Functional of V;

ex b_{1} being Functional of (RealVS V) st

for i being Element of V holds b_{1} . i = Im (l . i)

for b_{1}, b_{2} being Functional of (RealVS V) st ( for i being Element of V holds b_{1} . i = Im (l . i) ) & ( for i being Element of V holds b_{2} . i = Im (l . i) ) holds

b_{1} = b_{2}

end;
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 for i being Element of V holds it . i = Im (l . i);

ex b

for i being Element of V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def19 defines projIm HAHNBAN1:def 19 :

for V being non empty VectSpStr over F_Complex

for l being Functional of V

for b_{3} being Functional of (RealVS V) holds

( b_{3} = projIm l iff for i being Element of V holds b_{3} . i = Im (l . i) );

for V being non empty VectSpStr over F_Complex

for l being Functional of V

for b

( b

definition

let V be non empty VectSpStr over F_Complex ;

let l be Functional of (RealVS V);

coherence

l is RFunctional of V

end;
let l be Functional of (RealVS V);

coherence

l is RFunctional of V

proof end;

:: deftheorem defines RtoC HAHNBAN1:def 20 :

for V being non empty VectSpStr over F_Complex

for l being Functional of (RealVS V) holds RtoC l = l;

for V being non empty VectSpStr over F_Complex

for l being Functional of (RealVS V) holds RtoC l = l;

definition

let V be non empty VectSpStr over F_Complex ;

let l be RFunctional of V;

coherence

l is Functional of (RealVS V)

end;
let l be RFunctional of V;

coherence

l is Functional of (RealVS V)

proof end;

:: deftheorem defines CtoR HAHNBAN1:def 21 :

for V being non empty VectSpStr over F_Complex

for l being RFunctional of V holds CtoR l = l;

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

coherence

RtoC l is additive

end;
let l be additive Functional of (RealVS V);

coherence

RtoC l is additive

proof end;

registration

let V be VectSp of F_Complex ;

let l be additive RFunctional of V;

coherence

CtoR l is additive

end;
let l be additive RFunctional of V;

coherence

CtoR l is additive

proof end;

registration

let V be VectSp of F_Complex ;

let l be homogeneous Functional of (RealVS V);

coherence

RtoC l is Real_homogeneous

end;
let l be homogeneous Functional of (RealVS V);

coherence

RtoC l is Real_homogeneous

proof end;

registration

let V be VectSp of F_Complex ;

let l be Real_homogeneous RFunctional of V;

coherence

CtoR l is homogeneous

end;
let l be Real_homogeneous RFunctional of V;

coherence

CtoR l is homogeneous

proof end;

definition

let V be non empty VectSpStr over F_Complex ;

let l be RFunctional of V;

ex b_{1} being RFunctional of V st

for v being Element of V holds b_{1} . v = l . (i_FC * v)

for b_{1}, b_{2} being RFunctional of V st ( for v being Element of V holds b_{1} . v = l . (i_FC * v) ) & ( for v being Element of V holds b_{2} . v = l . (i_FC * v) ) holds

b_{1} = b_{2}

end;
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 for v being Element of V holds it . v = l . (i_FC * v);

ex b

for v being Element of V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def22 defines i-shift HAHNBAN1:def 22 :

for V being non empty VectSpStr over F_Complex

for l, b_{3} being RFunctional of V holds

( b_{3} = i-shift l iff for v being Element of V holds b_{3} . v = l . (i_FC * v) );

for V being non empty VectSpStr over F_Complex

for l, b

( b

definition

let V be non empty VectSpStr over F_Complex ;

let l be Functional of (RealVS V);

ex b_{1} being Functional of V st

for v being Element of V holds b_{1} . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**]

for b_{1}, b_{2} being Functional of V st ( for v being Element of V holds b_{1} . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] ) & ( for v being Element of V holds b_{2} . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] ) holds

b_{1} = b_{2}

end;
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 for v being Element of V holds it . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**];

ex b

for v being Element of V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def23 defines prodReIm HAHNBAN1:def 23 :

for V being non empty VectSpStr over F_Complex

for l being Functional of (RealVS V)

for b_{3} being Functional of V holds

( b_{3} = prodReIm l iff for v being Element of V holds b_{3} . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] );

for V being non empty VectSpStr over F_Complex

for l being Functional of (RealVS V)

for b

( b

theorem Th25: :: 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)

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)

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

proof end;

theorem Th27: :: 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

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

proof end;

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

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;

begin

:: from COMPTRIG, 2006.08.12, A.T.

theorem :: HAHNBAN1:29

for x being Real st x > 0 holds

for n being Element of NAT holds (power F_Complex) . ([**x,0**],n) = [**(x to_power n),0**]

for n being Element of NAT holds (power F_Complex) . ([**x,0**],n) = [**(x to_power n),0**]

proof end;

:: Hahn-Banach Theorem (complex spaces)