:: HAHNBAN1 semantic presentation
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
let F be non empty right_complementable Abelian add-associative right_zeroed right-distributive doubleLoopStr ; ::_thesis: for x, y being Element of F holds x * (- y) = - (x * y)
let x, y be Element of F; ::_thesis: x * (- y) = - (x * y)
(x * y) + (x * (- y)) = x * (y + (- y)) by VECTSP_1:def_2
.= x * (0. F) by RLVECT_1:def_10
.= 0. F by VECTSP_1:6 ;
hence x * (- y) = - (x * y) by RLVECT_1:def_10; ::_thesis: verum
end;
theorem :: HAHNBAN1:1
canceled;
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 Th3: :: HAHNBAN1:3
for z being Element of COMPLEX holds |.z.| + (0 * **) = ((z *') / (|.z.| + (0 * **))) * z
proof
let z be Element of COMPLEX ; ::_thesis: |.z.| + (0 * **) = ((z *') / (|.z.| + (0 * **))) * z
percases ( |.z.| = 0 or |.z.| <> 0 ) ;
supposeA1: |.z.| = 0 ; ::_thesis: |.z.| + (0 * **) = ((z *') / (|.z.| + (0 * **))) * z
then z = 0 by COMPLEX1:45;
hence |.z.| + (0 * **) = ((z *') / (|.z.| + (0 * **))) * z by A1; ::_thesis: verum
end;
supposeA2: |.z.| <> 0 ; ::_thesis: |.z.| + (0 * **) = ((z *') / (|.z.| + (0 * **))) * z
A3: Im (z * (z *')) = 0 by COMPLEX1:40;
|.z.| = |.z.| + (0 * **) ;
then A4: ( Re |.z.| = |.z.| & Im |.z.| = 0 ) by COMPLEX1:12;
A5: ( ((z *') / |.z.|) * z = (z * (z *')) / |.z.| & Re (z * (z *')) = ((Re z) ^2) + ((Im z) ^2) ) by COMPLEX1:40, XCMPLX_1:74;
then A6: Im (((z *') / |.z.|) * z) = ((|.z.| * 0) - ((((Re z) ^2) + ((Im z) ^2)) * 0)) / ((|.z.| ^2) + (0 ^2)) by A3, A4, COMPLEX1:24;
Re (((z *') / |.z.|) * z) = (((((Re z) ^2) + ((Im z) ^2)) * |.z.|) + (0 * 0)) / ((|.z.| ^2) + (0 ^2)) by A5, A3, A4, COMPLEX1:24
.= (|.(z * z).| * |.z.|) / (|.z.| * |.z.|) by COMPLEX1:68
.= |.(z * z).| / |.z.| by A2, XCMPLX_1:91
.= (|.z.| * |.z.|) / |.z.| by COMPLEX1:65
.= |.z.| by A2, XCMPLX_1:89 ;
hence |.z.| + (0 * **) = ((z *') / (|.z.| + (0 * **))) * z by A6, COMPLEX1:13; ::_thesis: verum
end;
end;
end;
begin
definition
let x, y be real number ;
func[**x,y**] -> Element of F_Complex equals :: HAHNBAN1:def 1
x + (y * **);
coherence
x + (y * **) is Element of F_Complex
proof
x + (y * **) in COMPLEX by XCMPLX_0:def_2;
hence x + (y * **) is Element of F_Complex by COMPLFLD:def_1; ::_thesis: verum
end;
end;
:: deftheorem defines [** HAHNBAN1:def_1_:_
for x, y being real number holds [**x,y**] = x + (y * **);
definition
func i_FC -> Element of F_Complex equals :: HAHNBAN1:def 2
** ;
coherence
** is Element of F_Complex
proof
0 + (1 * **) = [**0,1**] ;
hence ** is Element of F_Complex ; ::_thesis: verum
end;
end;
:: deftheorem defines i_FC HAHNBAN1:def_2_:_
i_FC = ** ;
theorem Th4: :: HAHNBAN1:4
i_FC * i_FC = - (1_ F_Complex)
proof
thus i_FC * i_FC = - 1r
.= - (1_ F_Complex) by COMPLFLD:2, COMPLFLD:8 ; ::_thesis: verum
end;
theorem Th5: :: HAHNBAN1:5
(- (1_ F_Complex)) * (- (1_ F_Complex)) = 1_ F_Complex
proof
- 1r = - (1_ F_Complex) by COMPLFLD:2, COMPLFLD:8;
hence (- (1_ F_Complex)) * (- (1_ F_Complex)) = 1_ F_Complex by COMPLFLD:8; ::_thesis: verum
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 number holds [**x1,y1**] * [**x2,y2**] = [**((x1 * x2) - (y1 * y2)),((x1 * y2) + (x2 * y1))**] ;
theorem :: HAHNBAN1:8
canceled;
theorem :: HAHNBAN1:9
for r being Real holds |.[**r,0**].| = abs 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;
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;
definition
let K be non empty addLoopStr ;
let V be non empty VectSpStr over K;
let f, g be Functional of V;
funcf + g -> Functional of V means :Def3: :: HAHNBAN1:def 3
for x being Element of V holds it . x = (f . x) + (g . x);
existence
ex b1 being Functional of V st
for x being Element of V holds b1 . x = (f . x) + (g . x)
proof
deffunc H1( Element of V) -> Element of the carrier of K = (f . $1) + (g . $1);
consider F being Function of the carrier of V, the carrier of K such that
A1: for x being Element of V holds F . x = H1(x) from FUNCT_2:sch_4();
reconsider F = F as Functional of V ;
take F ; ::_thesis: for x being Element of V holds F . x = (f . x) + (g . x)
thus for x being Element of V holds F . x = (f . x) + (g . x) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Functional of V st ( for x being Element of V holds b1 . x = (f . x) + (g . x) ) & ( for x being Element of V holds b2 . x = (f . x) + (g . x) ) holds
b1 = b2
proof
let a, b be Functional of V; ::_thesis: ( ( for x being Element of V holds a . x = (f . x) + (g . x) ) & ( for x being Element of V holds b . x = (f . x) + (g . x) ) implies a = b )
assume that
A2: for x being Element of V holds a . x = (f . x) + (g . x) and
A3: for x being Element of V holds b . x = (f . x) + (g . x) ; ::_thesis: a = b
now__::_thesis:_for_x_being_Element_of_V_holds_a_._x_=_b_._x
let x be Element of V; ::_thesis: a . x = b . x
thus a . x = (f . x) + (g . x) by A2
.= b . x by A3 ; ::_thesis: verum
end;
hence a = b by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines + HAHNBAN1:def_3_:_
for K being non empty addLoopStr
for V being non empty VectSpStr over K
for f, g, b5 being Functional of V holds
( b5 = f + g iff for x being Element of V holds b5 . x = (f . x) + (g . x) );
definition
let K be non empty addLoopStr ;
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
ex b1 being Functional of V st
for x being Element of V holds b1 . x = - (f . x)
proof
deffunc H1( Element of V) -> Element of the carrier of K = - (f . $1);
consider F being Function of the carrier of V, the carrier of K such that
A1: for x being Element of V holds F . x = H1(x) from FUNCT_2:sch_4();
reconsider F = F as Functional of V ;
take F ; ::_thesis: for x being Element of V holds F . x = - (f . x)
thus for x being Element of V holds F . x = - (f . x) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Functional of V st ( for x being Element of V holds b1 . x = - (f . x) ) & ( for x being Element of V holds b2 . x = - (f . x) ) holds
b1 = b2
proof
let a, b be Functional of V; ::_thesis: ( ( for x being Element of V holds a . x = - (f . x) ) & ( for x being Element of V holds b . x = - (f . x) ) implies a = b )
assume that
A2: for x being Element of V holds a . x = - (f . x) and
A3: for x being Element of V holds b . x = - (f . x) ; ::_thesis: a = b
now__::_thesis:_for_x_being_Element_of_V_holds_a_._x_=_b_._x
let x be Element of V; ::_thesis: a . x = b . x
thus a . x = - (f . x) by A2
.= b . x by A3 ; ::_thesis: verum
end;
hence a = b by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines - HAHNBAN1:def_4_:_
for K being non empty addLoopStr
for V being non empty VectSpStr over K
for f, b4 being Functional of V holds
( b4 = - f iff for x being Element of V holds b4 . x = - (f . x) );
definition
let K be non empty addLoopStr ;
let V be non empty VectSpStr over K;
let f, g be Functional of V;
funcf - 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 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;
funcv * f -> Functional of V means :Def6: :: HAHNBAN1:def 6
for x being Element of V holds it . x = v * (f . x);
existence
ex b1 being Functional of V st
for x being Element of V holds b1 . x = v * (f . x)
proof
deffunc H1( Element of V) -> Element of the carrier of K = v * (f . $1);
consider F being Function of the carrier of V, the carrier of K such that
A1: for x being Element of V holds F . x = H1(x) from FUNCT_2:sch_4();
reconsider F = F as Functional of V ;
take F ; ::_thesis: for x being Element of V holds F . x = v * (f . x)
thus for x being Element of V holds F . x = v * (f . x) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Functional of V st ( for x being Element of V holds b1 . x = v * (f . x) ) & ( for x being Element of V holds b2 . x = v * (f . x) ) holds
b1 = b2
proof
let a, b be Functional of V; ::_thesis: ( ( for x being Element of V holds a . x = v * (f . x) ) & ( for x being Element of V holds b . x = v * (f . x) ) implies a = b )
assume that
A2: for x being Element of V holds a . x = v * (f . x) and
A3: for x being Element of V holds b . x = v * (f . x) ; ::_thesis: a = b
now__::_thesis:_for_x_being_Element_of_V_holds_a_._x_=_b_._x
let x be Element of V; ::_thesis: a . x = b . x
thus a . x = v * (f . x) by A2
.= b . x by A3 ; ::_thesis: verum
end;
hence a = b by FUNCT_2:63; ::_thesis: verum
end;
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, b5 being Functional of V holds
( b5 = v * f iff for x being Element of V holds b5 . x = v * (f . x) );
definition
let K be non empty ZeroStr ;
let V be VectSpStr 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 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;
attrF 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 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
let K be non empty ZeroStr ;
let V be non empty VectSpStr over K;
let F be Functional of V;
attrF 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 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;
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 b1 being Functional of V st b1 is homogeneous holds
b1 is 0-preserving
proof
let F be Functional of V; ::_thesis: ( F is homogeneous implies F is 0-preserving )
assume A1: F is homogeneous ; ::_thesis: F is 0-preserving
thus F . (0. V) = F . ((0. K) * (0. V)) by VECTSP_1:14
.= (0. K) * (F . (0. V)) by A1, Def8
.= 0. K by VECTSP_1:7 ; :: according to HAHNBAN1:def_9 ::_thesis: verum
end;
end;
registration
let K be non empty right_zeroed addLoopStr ;
let V be non empty VectSpStr over K;
cluster 0Functional V -> additive ;
coherence
0Functional V is additive
proof
let x, y be Vector of V; :: according to VECTSP_1:def_20 ::_thesis: (0Functional V) . (x + y) = ((0Functional V) . x) + ((0Functional V) . y)
A1: ( (0Functional V) . x = 0. K & (0Functional V) . y = 0. K ) by FUNCOP_1:7;
thus (0Functional V) . (x + y) = 0. K by FUNCOP_1:7
.= ((0Functional V) . x) + ((0Functional V) . y) by A1, RLVECT_1:def_4 ; ::_thesis: verum
end;
end;
registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty VectSpStr over K;
cluster 0Functional V -> homogeneous ;
coherence
0Functional V is homogeneous
proof
let x be Vector of V; :: according to HAHNBAN1:def_8 ::_thesis: for r being Scalar of holds (0Functional V) . (r * x) = r * ((0Functional V) . x)
let r be Scalar of ; ::_thesis: (0Functional V) . (r * x) = r * ((0Functional V) . x)
A1: (0Functional V) . x = 0. K by FUNCOP_1:7;
thus (0Functional V) . (r * x) = 0. K by FUNCOP_1:7
.= r * ((0Functional V) . x) by A1, VECTSP_1:6 ; ::_thesis: verum
end;
end;
registration
let K be non empty ZeroStr ;
let V be non empty VectSpStr over K;
cluster 0Functional V -> 0-preserving ;
coherence
0Functional V is 0-preserving
proof
thus (0Functional V) . (0. V) = 0. K by FUNCOP_1:7; :: according to HAHNBAN1:def_9 ::_thesis: verum
end;
end;
registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty VectSpStr over K;
clusterV16() 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 b1 being Functional of V st
( b1 is additive & b1 is homogeneous & b1 is 0-preserving )
proof
take 0Functional V ; ::_thesis: ( 0Functional V is additive & 0Functional V is homogeneous & 0Functional V is 0-preserving )
thus ( 0Functional V is additive & 0Functional V is homogeneous & 0Functional V is 0-preserving ) ; ::_thesis: verum
end;
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
proof
let K be non empty Abelian addLoopStr ; ::_thesis: for V being non empty VectSpStr over K
for f, g being Functional of V holds f + g = g + f
let V be non empty VectSpStr over K; ::_thesis: for f, g being Functional of V holds f + g = g + f
let f, g be Functional of V; ::_thesis: f + g = g + f
now__::_thesis:_for_x_being_Element_of_V_holds_(f_+_g)_._x_=_(g_+_f)_._x
let x be Element of V; ::_thesis: (f + g) . x = (g + f) . x
thus (f + g) . x = (f . x) + (g . x) by Def3
.= (g + f) . x by Def3 ; ::_thesis: verum
end;
hence f + g = g + f by FUNCT_2:63; ::_thesis: verum
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)
proof
let K be non empty add-associative addLoopStr ; ::_thesis: for V being non empty VectSpStr over K
for f, g, h being Functional of V holds (f + g) + h = f + (g + h)
let V be non empty VectSpStr over K; ::_thesis: for f, g, h being Functional of V holds (f + g) + h = f + (g + h)
let f, g, h be Functional of V; ::_thesis: (f + g) + h = f + (g + h)
now__::_thesis:_for_x_being_Element_of_V_holds_((f_+_g)_+_h)_._x_=_(f_+_(g_+_h))_._x
let x be Element of V; ::_thesis: ((f + g) + h) . x = (f + (g + h)) . x
thus ((f + g) + h) . x = ((f + g) . x) + (h . x) by Def3
.= ((f . x) + (g . x)) + (h . x) by Def3
.= (f . x) + ((g . x) + (h . x)) by RLVECT_1:def_3
.= (f . x) + ((g + h) . x) by Def3
.= (f + (g + h)) . x by Def3 ; ::_thesis: verum
end;
hence (f + g) + h = f + (g + h) by FUNCT_2:63; ::_thesis: verum
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;
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
proof
let K be non empty right_zeroed addLoopStr ; ::_thesis: for V being non empty VectSpStr over K
for f being Functional of V holds f + (0Functional V) = f
let V be non empty VectSpStr over K; ::_thesis: for f being Functional of V holds f + (0Functional V) = f
let f be Functional of V; ::_thesis: f + (0Functional V) = f
now__::_thesis:_for_x_being_Element_of_V_holds_(f_+_(0Functional_V))_._x_=_f_._x
let x be Element of V; ::_thesis: (f + (0Functional V)) . x = f . x
thus (f + (0Functional V)) . x = (f . x) + ((0Functional V) . x) by Def3
.= (f . x) + (0. K) by FUNCOP_1:7
.= f . x by RLVECT_1:def_4 ; ::_thesis: verum
end;
hence f + (0Functional V) = f by FUNCT_2:63; ::_thesis: verum
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
proof
let K be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for V being non empty VectSpStr over K
for f being Functional of V holds f - f = 0Functional V
let V be non empty VectSpStr over K; ::_thesis: for f being Functional of V holds f - f = 0Functional V
let f be Functional of V; ::_thesis: f - f = 0Functional V
now__::_thesis:_for_x_being_Element_of_V_holds_(f_-_f)_._x_=_(0Functional_V)_._x
let x be Element of V; ::_thesis: (f - f) . x = (0Functional V) . x
thus (f - f) . x = (f . x) + ((- f) . x) by Def3
.= (f . x) + (- (f . x)) by Def4
.= 0. K by RLVECT_1:5
.= (0Functional V) . x by FUNCOP_1:7 ; ::_thesis: verum
end;
hence f - f = 0Functional V by FUNCT_2:63; ::_thesis: verum
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)
proof
let K be non empty right-distributive doubleLoopStr ; ::_thesis: 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)
let V be non empty VectSpStr over K; ::_thesis: for r being Element of K
for f, g being Functional of V holds r * (f + g) = (r * f) + (r * g)
let r be Element of K; ::_thesis: for f, g being Functional of V holds r * (f + g) = (r * f) + (r * g)
let f, g be Functional of V; ::_thesis: r * (f + g) = (r * f) + (r * g)
now__::_thesis:_for_x_being_Element_of_V_holds_(r_*_(f_+_g))_._x_=_((r_*_f)_+_(r_*_g))_._x
let x be Element of V; ::_thesis: (r * (f + g)) . x = ((r * f) + (r * g)) . x
thus (r * (f + g)) . x = r * ((f + g) . x) by Def6
.= r * ((f . x) + (g . x)) by Def3
.= (r * (f . x)) + (r * (g . x)) by VECTSP_1:def_2
.= ((r * f) . x) + (r * (g . x)) by Def6
.= ((r * f) . x) + ((r * g) . x) by Def6
.= ((r * f) + (r * g)) . x by Def3 ; ::_thesis: verum
end;
hence r * (f + g) = (r * f) + (r * g) by FUNCT_2:63; ::_thesis: verum
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)
proof
let K be non empty left-distributive doubleLoopStr ; ::_thesis: 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)
let V be non empty VectSpStr over K; ::_thesis: for r, s being Element of K
for f being Functional of V holds (r + s) * f = (r * f) + (s * f)
let r, s be Element of K; ::_thesis: for f being Functional of V holds (r + s) * f = (r * f) + (s * f)
let f be Functional of V; ::_thesis: (r + s) * f = (r * f) + (s * f)
now__::_thesis:_for_x_being_Element_of_V_holds_((r_+_s)_*_f)_._x_=_((r_*_f)_+_(s_*_f))_._x
let x be Element of V; ::_thesis: ((r + s) * f) . x = ((r * f) + (s * f)) . x
thus ((r + s) * f) . x = (r + s) * (f . x) by Def6
.= (r * (f . x)) + (s * (f . x)) by VECTSP_1:def_3
.= ((r * f) . x) + (s * (f . x)) by Def6
.= ((r * f) . x) + ((s * f) . x) by Def6
.= ((r * f) + (s * f)) . x by Def3 ; ::_thesis: verum
end;
hence (r + s) * f = (r * f) + (s * f) by FUNCT_2:63; ::_thesis: verum
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)
proof
let K be non empty associative multMagma ; ::_thesis: 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)
let V be non empty VectSpStr over K; ::_thesis: for r, s being Element of K
for f being Functional of V holds (r * s) * f = r * (s * f)
let r, s be Element of K; ::_thesis: for f being Functional of V holds (r * s) * f = r * (s * f)
let f be Functional of V; ::_thesis: (r * s) * f = r * (s * f)
now__::_thesis:_for_x_being_Element_of_V_holds_((r_*_s)_*_f)_._x_=_(r_*_(s_*_f))_._x
let x be Element of V; ::_thesis: ((r * s) * f) . x = (r * (s * f)) . x
thus ((r * s) * f) . x = (r * s) * (f . x) by Def6
.= r * (s * (f . x)) by GROUP_1:def_3
.= r * ((s * f) . x) by Def6
.= (r * (s * f)) . x by Def6 ; ::_thesis: verum
end;
hence (r * s) * f = r * (s * f) by FUNCT_2:63; ::_thesis: verum
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
proof
let K be non empty left_unital doubleLoopStr ; ::_thesis: for V being non empty VectSpStr over K
for f being Functional of V holds (1. K) * f = f
let V be non empty VectSpStr over K; ::_thesis: for f being Functional of V holds (1. K) * f = f
let f be Functional of V; ::_thesis: (1. K) * f = f
now__::_thesis:_for_x_being_Element_of_V_holds_((1._K)_*_f)_._x_=_f_._x
let x be Element of V; ::_thesis: ((1. K) * f) . x = f . x
thus ((1. K) * f) . x = (1. K) * (f . x) by Def6
.= f . x by VECTSP_1:def_8 ; ::_thesis: verum
end;
hence (1. K) * f = f by FUNCT_2:63; ::_thesis: verum
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;
clusterf + g -> additive ;
coherence
f + g is additive
proof
let x, y be Vector of V; :: according to VECTSP_1:def_20 ::_thesis: (f + g) . (x + y) = ((f + g) . x) + ((f + g) . y)
thus (f + g) . (x + y) = (f . (x + y)) + (g . (x + y)) by Def3
.= ((f . x) + (f . y)) + (g . (x + y)) by VECTSP_1:def_20
.= ((f . x) + (f . y)) + ((g . x) + (g . y)) by VECTSP_1:def_20
.= (f . x) + ((f . y) + ((g . x) + (g . y))) by RLVECT_1:def_3
.= (f . x) + ((g . x) + ((f . y) + (g . y))) by RLVECT_1:def_3
.= ((f . x) + (g . x)) + ((f . y) + (g . y)) by RLVECT_1:def_3
.= ((f + g) . x) + ((f . y) + (g . y)) by Def3
.= ((f + g) . x) + ((f + g) . y) by Def3 ; ::_thesis: verum
end;
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;
cluster - f -> additive ;
coherence
- f is additive
proof
let x, y be Vector of V; :: according to VECTSP_1:def_20 ::_thesis: (- f) . (x + y) = ((- f) . x) + ((- f) . y)
thus (- f) . (x + y) = - (f . (x + y)) by Def4
.= - ((f . x) + (f . y)) by VECTSP_1:def_20
.= (- (f . x)) + (- (f . y)) by RLVECT_1:31
.= ((- f) . x) + (- (f . y)) by Def4
.= ((- f) . x) + ((- f) . y) by Def4 ; ::_thesis: verum
end;
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;
clusterv * f -> additive ;
coherence
v * f is additive
proof
let x, y be Vector of V; :: according to VECTSP_1:def_20 ::_thesis: (v * f) . (x + y) = ((v * f) . x) + ((v * f) . y)
thus (v * f) . (x + y) = v * (f . (x + y)) by Def6
.= v * ((f . x) + (f . y)) by VECTSP_1:def_20
.= (v * (f . x)) + (v * (f . y)) by VECTSP_1:def_2
.= ((v * f) . x) + (v * (f . y)) by Def6
.= ((v * f) . x) + ((v * f) . y) by Def6 ; ::_thesis: verum
end;
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;
clusterf + g -> homogeneous ;
coherence
f + g is homogeneous
proof
let x be Vector of V; :: according to HAHNBAN1:def_8 ::_thesis: for r being Scalar of holds (f + g) . (r * x) = r * ((f + g) . x)
let r be Scalar of ; ::_thesis: (f + g) . (r * x) = r * ((f + g) . x)
thus (f + g) . (r * x) = (f . (r * x)) + (g . (r * x)) by Def3
.= (r * (f . x)) + (g . (r * x)) by Def8
.= (r * (f . x)) + (r * (g . x)) by Def8
.= r * ((f . x) + (g . x)) by VECTSP_1:def_2
.= r * ((f + g) . x) by Def3 ; ::_thesis: verum
end;
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;
cluster - f -> homogeneous ;
coherence
- f is homogeneous
proof
let x be Vector of V; :: according to HAHNBAN1:def_8 ::_thesis: for r being Scalar of holds (- f) . (r * x) = r * ((- f) . x)
let r be Scalar of ; ::_thesis: (- f) . (r * x) = r * ((- f) . x)
thus (- f) . (r * x) = - (f . (r * x)) by Def4
.= - (r * (f . x)) by Def8
.= r * (- (f . x)) by Lm1
.= r * ((- f) . x) by Def4 ; ::_thesis: verum
end;
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;
clusterv * f -> homogeneous ;
coherence
v * f is homogeneous
proof
let x be Vector of V; :: according to HAHNBAN1:def_8 ::_thesis: for r being Scalar of holds (v * f) . (r * x) = r * ((v * f) . x)
let r be Scalar of ; ::_thesis: (v * f) . (r * x) = r * ((v * f) . x)
thus (v * f) . (r * x) = v * (f . (r * x)) by Def6
.= v * (r * (f . x)) by Def8
.= r * (v * (f . x)) by GROUP_1:def_3
.= r * ((v * f) . x) by Def6 ; ::_thesis: verum
end;
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;
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;
funcV *' -> 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
ex b1 being non empty strict VectSpStr over 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 ) )
proof
defpred S1[ set , set , set ] means ex f, g being Functional of V st
( $1 = f & $2 = g & $3 = f + g );
0Functional V in { x where x is linear-Functional of V : verum } ;
then reconsider ca = { x where x is linear-Functional of V : verum } as non empty set ;
A1: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_ca_implies_x_is_linear-Functional_of_V_)_&_(_x_is_linear-Functional_of_V_implies_x_in_ca_)_)
let x be set ; ::_thesis: ( ( x in ca implies x is linear-Functional of V ) & ( x is linear-Functional of V implies x in ca ) )
thus ( x in ca implies x is linear-Functional of V ) ::_thesis: ( x is linear-Functional of V implies x in ca )
proof
assume x in ca ; ::_thesis: x is linear-Functional of V
then ex y being linear-Functional of V st x = y ;
hence x is linear-Functional of V ; ::_thesis: verum
end;
thus ( x is linear-Functional of V implies x in ca ) ; ::_thesis: verum
end;
then reconsider 0F = 0Functional V as Element of ca ;
A2: for x, y being Element of ca ex u being Element of ca st S1[x,y,u]
proof
let x, y be Element of ca; ::_thesis: ex u being Element of ca st S1[x,y,u]
reconsider f = x, g = y as linear-Functional of V by A1;
reconsider u = f + g as Element of ca by A1;
take u ; ::_thesis: S1[x,y,u]
take f ; ::_thesis: ex g being Functional of V st
( x = f & y = g & u = f + g )
take g ; ::_thesis: ( x = f & y = g & u = f + g )
thus ( x = f & y = g & u = f + g ) ; ::_thesis: verum
end;
consider ad being Function of [:ca,ca:],ca such that
A3: for x, y being Element of ca holds S1[x,y,ad . (x,y)] from BINOP_1:sch_3(A2);
defpred S2[ Element of K, set , set ] means ex f being Functional of V st
( $2 = f & $3 = $1 * f );
A4: for x being Element of K
for y being Element of ca ex u being Element of ca st S2[x,y,u]
proof
let x be Element of K; ::_thesis: for y being Element of ca ex u being Element of ca st S2[x,y,u]
let y be Element of ca; ::_thesis: ex u being Element of ca st S2[x,y,u]
reconsider f = y as linear-Functional of V by A1;
reconsider u = x * f as Element of ca by A1;
take u ; ::_thesis: S2[x,y,u]
take f ; ::_thesis: ( y = f & u = x * f )
thus ( y = f & u = x * f ) ; ::_thesis: verum
end;
consider lm being Function of [: the carrier of K,ca:],ca such that
A5: for x being Element of K
for y being Element of ca holds S2[x,y,lm . (x,y)] from BINOP_1:sch_3(A4);
A6: now__::_thesis:_for_f_being_linear-Functional_of_V
for_x_being_Element_of_K_holds_lm_._(x,f)_=_x_*_f
let f be linear-Functional of V; ::_thesis: for x being Element of K holds lm . (x,f) = x * f
reconsider y = f as Element of ca by A1;
let x be Element of K; ::_thesis: lm . (x,f) = x * f
ex f1 being Functional of V st
( y = f1 & lm . (x,y) = x * f1 ) by A5;
hence lm . (x,f) = x * f ; ::_thesis: verum
end;
reconsider V1 = VectSpStr(# ca,ad,0F,lm #) as non empty strict VectSpStr over K ;
take V1 ; ::_thesis: ( ( for x being set holds
( x in the carrier of V1 iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of V1 . (f,g) = f + g ) & 0. V1 = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of V1 . (x,f) = x * f ) )
now__::_thesis:_for_f,_g_being_linear-Functional_of_V_holds_ad_._(f,g)_=_f_+_g
let f, g be linear-Functional of V; ::_thesis: ad . (f,g) = f + g
reconsider x = f, y = g as Element of ca by A1;
ex f1, g1 being Functional of V st
( x = f1 & y = g1 & ad . (x,y) = f1 + g1 ) by A3;
hence ad . (f,g) = f + g ; ::_thesis: verum
end;
hence ( ( for x being set holds
( x in the carrier of V1 iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of V1 . (f,g) = f + g ) & 0. V1 = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of V1 . (x,f) = x * f ) ) by A1, A6; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty strict VectSpStr over 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
proof
let V1, V2 be non empty strict VectSpStr over K; ::_thesis: ( ( for x being set holds
( x in the carrier of V1 iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of V1 . (f,g) = f + g ) & 0. V1 = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of V1 . (x,f) = x * f ) & ( for x being set holds
( x in the carrier of V2 iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of V2 . (f,g) = f + g ) & 0. V2 = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of V2 . (x,f) = x * f ) implies V1 = V2 )
assume that
A7: for x being set holds
( x in the carrier of V1 iff x is linear-Functional of V ) and
A8: for f, g being linear-Functional of V holds the addF of V1 . (f,g) = f + g and
A9: 0. V1 = 0Functional V and
A10: for f being linear-Functional of V
for x being Element of K holds the lmult of V1 . (x,f) = x * f and
A11: for x being set holds
( x in the carrier of V2 iff x is linear-Functional of V ) and
A12: for f, g being linear-Functional of V holds the addF of V2 . (f,g) = f + g and
A13: 0. V2 = 0Functional V and
A14: for f being linear-Functional of V
for x being Element of K holds the lmult of V2 . (x,f) = x * f ; ::_thesis: V1 = V2
A15: now__::_thesis:_for_r_being_Element_of_K
for_x_being_Element_of_V1_holds_the_lmult_of_V1_._(r,x)_=_the_lmult_of_V2_._(r,x)
let r be Element of K; ::_thesis: for x being Element of V1 holds the lmult of V1 . (r,x) = the lmult of V2 . (r,x)
let x be Element of V1; ::_thesis: the lmult of V1 . (r,x) = the lmult of V2 . (r,x)
reconsider f = x as linear-Functional of V by A7;
thus the lmult of V1 . (r,x) = r * f by A10
.= the lmult of V2 . (r,x) by A14 ; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_the_carrier_of_V1_implies_x_in_the_carrier_of_V2_)_&_(_x_in_the_carrier_of_V2_implies_x_in_the_carrier_of_V1_)_)
let x be set ; ::_thesis: ( ( x in the carrier of V1 implies x in the carrier of V2 ) & ( x in the carrier of V2 implies x in the carrier of V1 ) )
thus ( x in the carrier of V1 implies x in the carrier of V2 ) ::_thesis: ( x in the carrier of V2 implies x in the carrier of V1 )
proof
assume x in the carrier of V1 ; ::_thesis: x in the carrier of V2
then x is linear-Functional of V by A7;
hence x in the carrier of V2 by A11; ::_thesis: verum
end;
assume x in the carrier of V2 ; ::_thesis: x in the carrier of V1
then x is linear-Functional of V by A11;
hence x in the carrier of V1 by A7; ::_thesis: verum
end;
then A16: the carrier of V1 = the carrier of V2 by TARSKI:1;
now__::_thesis:_for_x,_y_being_Element_of_V1_holds_the_addF_of_V1_._(x,y)_=_the_addF_of_V2_._(x,y)
let x, y be Element of V1; ::_thesis: the addF of V1 . (x,y) = the addF of V2 . (x,y)
reconsider f = x, g = y as linear-Functional of V by A7;
thus the addF of V1 . (x,y) = f + g by A8
.= the addF of V2 . (x,y) by A12 ; ::_thesis: verum
end;
then the addF of V1 = the addF of V2 by A16, BINOP_1:2;
hence V1 = V2 by A9, A13, A16, A15, BINOP_1:2; ::_thesis: verum
end;
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 b3 being non empty strict VectSpStr over K holds
( b3 = V *' iff ( ( for x being set holds
( x in the carrier of b3 iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of b3 . (f,g) = f + g ) & 0. b3 = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of b3 . (x,f) = x * f ) ) );
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;
clusterV *' -> non empty Abelian strict ;
coherence
V *' is Abelian
proof
let v, w be Element of (V *'); :: according to RLVECT_1:def_2 ::_thesis: v + w = w + v
reconsider f = v, g = w as linear-Functional of V by Def10;
thus v + w = f + g by Def10
.= g + f by Th12
.= w + v by Def10 ; ::_thesis: verum
end;
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;
clusterV *' -> non empty add-associative strict ;
coherence
V *' is add-associative
proof
let u, v, w be Element of (V *'); :: according to RLVECT_1:def_3 ::_thesis: (u + v) + w = u + (v + w)
reconsider f = u, g = v, h = w as linear-Functional of V by Def10;
thus (u + v) + w = the addF of (V *') . ((f + g),w) by Def10
.= (f + g) + h by Def10
.= f + (g + h) by Th13
.= the addF of (V *') . (u,(g + h)) by Def10
.= u + (v + w) by Def10 ; ::_thesis: verum
end;
clusterV *' -> non empty right_zeroed strict ;
coherence
V *' is right_zeroed
proof
let x be Element of (V *'); :: according to RLVECT_1:def_4 ::_thesis: x + (0. (V *')) = x
reconsider f = x as linear-Functional of V by Def10;
thus x + (0. (V *')) = the addF of (V *') . (x,(0Functional V)) by Def10
.= f + (0Functional V) by Def10
.= x by Th15 ; ::_thesis: verum
end;
clusterV *' -> non empty right_complementable strict ;
coherence
V *' is right_complementable
proof
let x be Element of (V *'); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider f = x as linear-Functional of V by Def10;
reconsider b = - f as Element of (V *') by Def10;
take b ; :: according to ALGSTR_0:def_11 ::_thesis: x + b = 0. (V *')
thus x + b = f - f by Def10
.= 0Functional V by Th16
.= 0. (V *') by Def10 ; ::_thesis: verum
end;
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;
clusterV *' -> 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
now__::_thesis:_for_x,_y_being_Element_of_K
for_v,_w_being_Element_of_(V_*')_holds_
(_x_*_(v_+_w)_=_(x_*_v)_+_(x_*_w)_&_(x_+_y)_*_v_=_(x_*_v)_+_(y_*_v)_&_(x_*_y)_*_v_=_x_*_(y_*_v)_&_(1._K)_*_v_=_v_)
let x, y be Element of K; ::_thesis: for v, w being Element of (V *') holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. K) * v = v )
let v, w be Element of (V *'); ::_thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. K) * v = v )
reconsider f = v, g = w as linear-Functional of V by Def10;
thus x * (v + w) = the lmult of (V *') . (x,(f + g)) by Def10
.= x * (f + g) by Def10
.= (x * f) + (x * g) by Th17
.= the addF of (V *') . ((x * f),(x * g)) by Def10
.= the addF of (V *') . (( the lmult of (V *') . (x,f)),(x * g)) by Def10
.= (x * v) + (x * w) by Def10 ; ::_thesis: ( (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. K) * v = v )
thus (x + y) * v = (x + y) * f by Def10
.= (x * f) + (y * f) by Th18
.= the addF of (V *') . ((x * f),(y * f)) by Def10
.= the addF of (V *') . (( the lmult of (V *') . (x,f)),(y * f)) by Def10
.= (x * v) + (y * v) by Def10 ; ::_thesis: ( (x * y) * v = x * (y * v) & (1. K) * v = v )
thus (x * y) * v = (x * y) * f by Def10
.= x * (y * f) by Th19
.= the lmult of (V *') . (x,(y * f)) by Def10
.= x * (y * v) by Def10 ; ::_thesis: (1. K) * v = v
thus (1. K) * v = (1. K) * f by Def10
.= v by Th20 ; ::_thesis: verum
end;
hence ( V *' is vector-distributive & V *' is scalar-distributive & V *' is scalar-associative & V *' is scalar-unital ) by VECTSP_1:def_14, VECTSP_1:def_15, VECTSP_1:def_16, VECTSP_1:def_17; ::_thesis: verum
end;
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;
definition
let K be 1-sorted ;
let V be non empty VectSpStr over K;
let F be RFunctional of V;
attrF 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 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) );
definition
let K be 1-sorted ;
let V be non empty VectSpStr over K;
let F be RFunctional of V;
attrF 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 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) );
definition
let V be non empty VectSpStr over F_Complex ;
let F be RFunctional of V;
attrF 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 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))
proof
let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F_Complex ; ::_thesis: 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))
let F be RFunctional of V; ::_thesis: ( F is Real_homogeneous implies for v being Vector of V
for r being Real holds F . ([**0,r**] * v) = r * (F . (i_FC * v)) )
assume A1: F is Real_homogeneous ; ::_thesis: for v being Vector of V
for r being Real holds F . ([**0,r**] * v) = r * (F . (i_FC * v))
let v be Vector of V; ::_thesis: for r being Real holds F . ([**0,r**] * v) = r * (F . (i_FC * v))
let r be Real; ::_thesis: F . ([**0,r**] * v) = r * (F . (i_FC * v))
thus F . ([**0,r**] * v) = F . (([**r,0**] * i_FC) * v)
.= F . ([**r,0**] * (i_FC * v)) by VECTSP_1:def_16
.= r * (F . (i_FC * v)) by A1, Def13 ; ::_thesis: verum
end;
definition
let V be non empty VectSpStr over F_Complex ;
let F be RFunctional of V;
attrF 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 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) );
definition
let K be 1-sorted ;
let V be VectSpStr over K;
let F be RFunctional of V;
attrF 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 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;
cluster Function-like V30( the carrier of V, REAL ) additive -> subadditive for Element of bool [: the carrier of V,REAL:];
coherence
for b1 being RFunctional of V st b1 is additive holds
b1 is subadditive
proof
let F be RFunctional of V; ::_thesis: ( F is additive implies F is subadditive )
assume A1: F is additive ; ::_thesis: F is subadditive
let x, y be Vector of V; :: according to HAHNBAN1:def_11 ::_thesis: F . (x + y) <= (F . x) + (F . y)
thus F . (x + y) <= (F . x) + (F . y) by A1, Def12; ::_thesis: verum
end;
end;
registration
let V be VectSp of F_Complex ;
cluster Function-like V30( the carrier of V, REAL ) Real_homogeneous -> 0-preserving for Element of bool [: the carrier of V,REAL:];
coherence
for b1 being RFunctional of V st b1 is Real_homogeneous holds
b1 is 0-preserving
proof
let F be RFunctional of V; ::_thesis: ( F is Real_homogeneous implies F is 0-preserving )
assume A1: F is Real_homogeneous ; ::_thesis: F is 0-preserving
A2: 0. F_Complex = [**0,0**] by COMPLFLD:7;
thus F . (0. V) = F . ((0. F_Complex) * (0. V)) by VECTSP_1:14
.= 0 * (F . (0. V)) by A1, A2, Def13
.= 0 ; :: according to HAHNBAN1:def_15 ::_thesis: verum
end;
end;
definition
let K be 1-sorted ;
let V be VectSpStr over K;
func 0RFunctional V -> RFunctional of V equals :: HAHNBAN1:def 16
([#] V) --> 0;
coherence
([#] V) --> 0 is RFunctional of V ;
end;
:: deftheorem defines 0RFunctional HAHNBAN1:def_16_:_
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;
cluster 0RFunctional V -> additive ;
coherence
0RFunctional V is additive
proof
let x, y be Vector of V; :: according to HAHNBAN1:def_12 ::_thesis: (0RFunctional V) . (x + y) = ((0RFunctional V) . x) + ((0RFunctional V) . y)
( (0RFunctional V) . x = 0 & (0RFunctional V) . y = 0 ) by FUNCOP_1:7;
hence (0RFunctional V) . (x + y) = ((0RFunctional V) . x) + ((0RFunctional V) . y) by FUNCOP_1:7; ::_thesis: verum
end;
cluster 0RFunctional V -> 0-preserving ;
coherence
0RFunctional V is 0-preserving
proof
thus (0RFunctional V) . (0. V) = 0 by FUNCOP_1:7; :: according to HAHNBAN1:def_15 ::_thesis: verum
end;
end;
registration
let V be non empty VectSpStr over F_Complex ;
cluster 0RFunctional V -> Real_homogeneous ;
coherence
0RFunctional V is Real_homogeneous
proof
let x be Vector of V; :: according to HAHNBAN1:def_13 ::_thesis: for r being Real holds (0RFunctional V) . ([**r,0**] * x) = r * ((0RFunctional V) . x)
let r be Real; ::_thesis: (0RFunctional V) . ([**r,0**] * x) = r * ((0RFunctional V) . x)
(0RFunctional V) . x = 0 by FUNCOP_1:7;
hence (0RFunctional V) . ([**r,0**] * x) = r * ((0RFunctional V) . x) by FUNCOP_1:7; ::_thesis: verum
end;
cluster 0RFunctional V -> homogeneous ;
coherence
0RFunctional V is homogeneous
proof
let x be Vector of V; :: according to HAHNBAN1:def_14 ::_thesis: for r being Scalar of holds (0RFunctional V) . (r * x) = |.r.| * ((0RFunctional V) . x)
let r be Scalar of ; ::_thesis: (0RFunctional V) . (r * x) = |.r.| * ((0RFunctional V) . x)
(0RFunctional V) . x = 0 by FUNCOP_1:7;
hence (0RFunctional V) . (r * x) = |.r.| * ((0RFunctional V) . x) by FUNCOP_1:7; ::_thesis: verum
end;
end;
registration
let K be 1-sorted ;
let V be non empty VectSpStr over K;
clusterV16() 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 b1 being RFunctional of V st
( b1 is additive & b1 is 0-preserving )
proof
take 0RFunctional V ; ::_thesis: ( 0RFunctional V is additive & 0RFunctional V is 0-preserving )
thus ( 0RFunctional V is additive & 0RFunctional V is 0-preserving ) ; ::_thesis: verum
end;
end;
registration
let V be non empty VectSpStr over F_Complex ;
clusterV16() 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 b1 being RFunctional of V st
( b1 is additive & b1 is Real_homogeneous & b1 is homogeneous )
proof
take 0RFunctional V ; ::_thesis: ( 0RFunctional V is additive & 0RFunctional V is Real_homogeneous & 0RFunctional V is homogeneous )
thus ( 0RFunctional V is additive & 0RFunctional V is Real_homogeneous & 0RFunctional V is homogeneous ) ; ::_thesis: verum
end;
end;
definition
let V be non empty VectSpStr over F_Complex ;
mode Semi-Norm of V is subadditive homogeneous RFunctional of V;
end;
begin
definition
let V be non empty VectSpStr 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 b1 being strict RLSStruct st
( addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = 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 b1 . (r,v) = [**r,0**] * v ) )
proof
deffunc H1( Element of REAL , Element of V) -> Element of the carrier of V = [**$1,0**] * $2;
consider f being Function of [:REAL, the carrier of V:], the carrier of V such that
A1: for r being Real
for v being Vector of V holds f . (r,v) = H1(r,v) from BINOP_1:sch_4();
take R = RLSStruct(# the carrier of V,(0. V), the addF of V,f #); ::_thesis: ( addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) = 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 R . (r,v) = [**r,0**] * v ) )
thus addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) = addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) ; ::_thesis: for r being Real
for v being Vector of V holds the Mult of R . (r,v) = [**r,0**] * v
let r be Real; ::_thesis: for v being Vector of V holds the Mult of R . (r,v) = [**r,0**] * v
let v be Vector of V; ::_thesis: the Mult of R . (r,v) = [**r,0**] * v
thus the Mult of R . (r,v) = [**r,0**] * v by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict RLSStruct st addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = 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 b1 . (r,v) = [**r,0**] * v ) & addLoopStr(# the carrier of b2, the addF of b2, the ZeroF of b2 #) = 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 b2 . (r,v) = [**r,0**] * v ) holds
b1 = b2
proof
let a, b be strict RLSStruct ; ::_thesis: ( addLoopStr(# the carrier of a, the addF of a, the ZeroF of a #) = 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 a . (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 ) implies a = b )
assume that
A2: addLoopStr(# the carrier of a, the addF of a, the ZeroF of a #) = addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) and
A3: for r being Real
for v being Vector of V holds the Mult of a . (r,v) = [**r,0**] * v and
A4: 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 #) and
A5: for r being Real
for v being Vector of V holds the Mult of b . (r,v) = [**r,0**] * v ; ::_thesis: a = b
now__::_thesis:_for_r_being_Real
for_v_being_Vector_of_V_holds_the_Mult_of_a_._(r,v)_=_the_Mult_of_b_._(r,v)
let r be Real; ::_thesis: for v being Vector of V holds the Mult of a . (r,v) = the Mult of b . (r,v)
let v be Vector of V; ::_thesis: the Mult of a . (r,v) = the Mult of b . (r,v)
thus the Mult of a . (r,v) = [**r,0**] * v by A3
.= the Mult of b . (r,v) by A5 ; ::_thesis: verum
end;
hence a = b by A2, A4, BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def17 defines RealVS HAHNBAN1:def_17_:_
for V being non empty VectSpStr over F_Complex
for b2 being strict RLSStruct holds
( b2 = RealVS V iff ( addLoopStr(# the carrier of b2, the addF of b2, the ZeroF of b2 #) = 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 b2 . (r,v) = [**r,0**] * v ) ) );
registration
let V be non empty VectSpStr over F_Complex ;
cluster RealVS V -> non empty strict ;
coherence
not RealVS V is empty
proof
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
hence not RealVS V is empty ; ::_thesis: verum
end;
end;
registration
let V be non empty Abelian VectSpStr over F_Complex ;
cluster RealVS V -> strict Abelian ;
coherence
RealVS V is Abelian
proof
let v, w be Element of (RealVS V); :: according to RLVECT_1:def_2 ::_thesis: v + w = w + v
A1: addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider v1 = v, w1 = w as Element of V ;
thus v + w = v1 + w1 by A1
.= w1 + v1
.= w + v by A1 ; ::_thesis: verum
end;
end;
registration
let V be non empty add-associative VectSpStr over F_Complex ;
cluster RealVS V -> strict add-associative ;
coherence
RealVS V is add-associative
proof
let u, v, w be Element of (RealVS V); :: according to RLVECT_1:def_3 ::_thesis: (u + v) + w = u + (v + w)
A1: addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider u1 = u, v1 = v, w1 = w as Element of V ;
thus (u + v) + w = (u1 + v1) + w1 by A1
.= u1 + (v1 + w1) by RLVECT_1:def_3
.= u + (v + w) by A1 ; ::_thesis: verum
end;
end;
registration
let V be non empty right_zeroed VectSpStr over F_Complex ;
cluster RealVS V -> strict right_zeroed ;
coherence
RealVS V is right_zeroed
proof
let v be Element of (RealVS V); :: according to RLVECT_1:def_4 ::_thesis: v + (0. (RealVS V)) = v
A1: addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider v1 = v as Element of V ;
thus v + (0. (RealVS V)) = v1 + (0. V) by A1
.= v by RLVECT_1:def_4 ; ::_thesis: verum
end;
end;
registration
let V be non empty right_complementable VectSpStr over F_Complex ;
cluster RealVS V -> right_complementable strict ;
coherence
RealVS V is right_complementable
proof
let v be Element of (RealVS V); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
A1: addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider v1 = v as Element of V ;
consider w1 being Element of V such that
A2: v1 + w1 = 0. V by ALGSTR_0:def_11;
reconsider w = w1 as Element of (RealVS V) by A1;
take w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. (RealVS V)
thus v + w = 0. (RealVS V) by A1, A2; ::_thesis: verum
end;
end;
registration
let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr 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
thus for a being real number
for v, w being Element of (RealVS V) holds a * (v + w) = (a * v) + (a * w) :: according to RLVECT_1:def_5 ::_thesis: ( RealVS V is scalar-distributive & RealVS V is scalar-associative & RealVS V is scalar-unital )
proof
let a be real number ; ::_thesis: for v, w being Element of (RealVS V) holds a * (v + w) = (a * v) + (a * w)
reconsider a = a as Real by XREAL_0:def_1;
let v, w be Element of (RealVS V); ::_thesis: a * (v + w) = (a * v) + (a * w)
set a1 = [**a,0**];
A1: addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider v1 = v, w1 = w as Element of V ;
a * (v + w) = [**a,0**] * (v1 + w1) by A1, Def17
.= ([**a,0**] * v1) + ([**a,0**] * w1) by VECTSP_1:def_14
.= the addF of V . [( the Mult of (RealVS V) . (a,v1)),([**a,0**] * w1)] by Def17
.= (a * v) + (a * w) by A1, Def17 ;
hence a * (v + w) = (a * v) + (a * w) ; ::_thesis: verum
end;
thus for a, b being real number
for v being Element of (RealVS V) holds (a + b) * v = (a * v) + (b * v) :: according to RLVECT_1:def_6 ::_thesis: ( RealVS V is scalar-associative & RealVS V is scalar-unital )
proof
let a, b be real number ; ::_thesis: for v being Element of (RealVS V) holds (a + b) * v = (a * v) + (b * v)
reconsider a = a, b = b as Real by XREAL_0:def_1;
let v be Element of (RealVS V); ::_thesis: (a + b) * v = (a * v) + (b * v)
set a1 = [**a,0**];
set b1 = [**b,0**];
A2: addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider v1 = v as Element of V ;
[**a,0**] + [**b,0**] = [**(a + b),0**] ;
then (a + b) * v = ([**a,0**] + [**b,0**]) * v1 by Def17
.= ([**a,0**] * v1) + ([**b,0**] * v1) by VECTSP_1:def_15
.= the addF of (RealVS V) . [( the Mult of (RealVS V) . (a,v)),([**b,0**] * v1)] by A2, Def17
.= (a * v) + (b * v) by Def17 ;
hence (a + b) * v = (a * v) + (b * v) ; ::_thesis: verum
end;
thus for a, b being real number
for v being Element of (RealVS V) holds (a * b) * v = a * (b * v) :: according to RLVECT_1:def_7 ::_thesis: RealVS V is scalar-unital
proof
let a, b be real number ; ::_thesis: for v being Element of (RealVS V) holds (a * b) * v = a * (b * v)
reconsider a = a, b = b as Real by XREAL_0:def_1;
let v be Element of (RealVS V); ::_thesis: (a * b) * v = a * (b * v)
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider v1 = v as Element of V ;
[**(a * b),0**] = [**a,0**] * [**b,0**] ;
then (a * b) * v = ([**a,0**] * [**b,0**]) * v1 by Def17
.= [**a,0**] * ([**b,0**] * v1) by VECTSP_1:def_16
.= the Mult of (RealVS V) . (a,([**b,0**] * v1)) by Def17
.= a * (b * v) by Def17 ;
hence (a * b) * v = a * (b * v) ; ::_thesis: verum
end;
let v be Element of (RealVS V); :: according to RLVECT_1:def_8 ::_thesis: 1 * v = v
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider v1 = v as Element of V ;
thus 1 * v = [**1,0**] * v1 by Def17
.= v by COMPLFLD:8, VECTSP_1:def_17 ; ::_thesis: verum
end;
end;
theorem Th22: :: HAHNBAN1:22
for V being VectSp of F_Complex
for M being Subspace of V holds RealVS M is Subspace of RealVS V
proof
let V be VectSp of F_Complex ; ::_thesis: for M being Subspace of V holds RealVS M is Subspace of RealVS V
let M be Subspace of V; ::_thesis: RealVS M is Subspace of RealVS V
A1: the carrier of M c= the carrier of V by VECTSP_4:def_2;
A2: the lmult of M = the lmult of V | [: the carrier of F_Complex, the carrier of M:] by VECTSP_4:def_2;
A3: addLoopStr(# the carrier of M, the addF of M, the ZeroF of M #) = addLoopStr(# the carrier of (RealVS M), the addF of (RealVS M), the ZeroF of (RealVS M) #) by Def17;
A4: addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
hence A5: the carrier of (RealVS M) c= the carrier of (RealVS V) by A3, VECTSP_4:def_2; :: according to RLSUB_1:def_2 ::_thesis: ( 0. (RealVS M) = 0. (RealVS V) & the addF of (RealVS M) = the addF of (RealVS V) || the carrier of (RealVS M) & the Mult of (RealVS M) = K69( the Mult of (RealVS V),[:REAL, the carrier of (RealVS M):]) )
then [:REAL, the carrier of (RealVS M):] c= [:REAL, the carrier of (RealVS V):] by ZFMISC_1:95;
then [:REAL, the carrier of (RealVS M):] c= dom the Mult of (RealVS V) by FUNCT_2:def_1;
then A6: dom ( the Mult of (RealVS V) | [:REAL, the carrier of (RealVS M):]) = [:REAL, the carrier of (RealVS M):] by RELAT_1:62;
rng ( the Mult of (RealVS V) | [:REAL, the carrier of (RealVS M):]) c= the carrier of (RealVS M)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ( the Mult of (RealVS V) | [:REAL, the carrier of (RealVS M):]) or y in the carrier of (RealVS M) )
assume y in rng ( the Mult of (RealVS V) | [:REAL, the carrier of (RealVS M):]) ; ::_thesis: y in the carrier of (RealVS M)
then consider x being set such that
A7: x in dom ( the Mult of (RealVS V) | [:REAL, the carrier of (RealVS M):]) and
A8: y = ( the Mult of (RealVS V) | [:REAL, the carrier of (RealVS M):]) . x by FUNCT_1:def_3;
consider a, b being set such that
A9: x = [a,b] by A7, RELAT_1:def_1;
reconsider a = a as Real by A7, A9, ZFMISC_1:87;
reconsider b = b as Element of (RealVS M) by A6, A7, A9, ZFMISC_1:87;
reconsider b1 = b as Element of M by A3;
reconsider b2 = b1 as Element of V by A1, TARSKI:def_3;
[[**a,0**],b2] in [: the carrier of F_Complex, the carrier of V:] by ZFMISC_1:87;
then ( [[**a,0**],b1] in [: the carrier of F_Complex, the carrier of M:] & [[**a,0**],b2] in dom the lmult of V ) by FUNCT_2:def_1, ZFMISC_1:87;
then [[**a,0**],b2] in (dom the lmult of V) /\ [: the carrier of F_Complex, the carrier of M:] by XBOOLE_0:def_4;
then A10: [[**a,0**],b2] in dom ( the lmult of V | [: the carrier of F_Complex, the carrier of M:]) by RELAT_1:61;
y = the Mult of (RealVS V) . (a,b) by A7, A8, A9, FUNCT_1:47
.= [**a,0**] * b2 by Def17
.= [**a,0**] * b1 by A2, A10, FUNCT_1:47
.= the Mult of (RealVS M) . (a,b) by Def17 ;
hence y in the carrier of (RealVS M) ; ::_thesis: verum
end;
then reconsider RM = the Mult of (RealVS V) | [:REAL, the carrier of (RealVS M):] as Function of [:REAL, the carrier of (RealVS M):], the carrier of (RealVS M) by A6, FUNCT_2:2;
thus 0. (RealVS M) = 0. M by A3
.= 0. V by VECTSP_4:def_2
.= 0. (RealVS V) by A4 ; ::_thesis: ( the addF of (RealVS M) = the addF of (RealVS V) || the carrier of (RealVS M) & the Mult of (RealVS M) = K69( the Mult of (RealVS V),[:REAL, the carrier of (RealVS M):]) )
thus the addF of (RealVS M) = the addF of (RealVS V) || the carrier of (RealVS M) by A3, A4, VECTSP_4:def_2; ::_thesis: the Mult of (RealVS M) = K69( the Mult of (RealVS V),[:REAL, the carrier of (RealVS M):])
now__::_thesis:_for_a_being_Real
for_b_being_Element_of_(RealVS_M)_holds_the_Mult_of_(RealVS_M)_._(a,b)_=_RM_._(a,b)
let a be Real; ::_thesis: for b being Element of (RealVS M) holds the Mult of (RealVS M) . (a,b) = RM . (a,b)
let b be Element of (RealVS M); ::_thesis: the Mult of (RealVS M) . (a,b) = RM . (a,b)
reconsider b1 = b as Element of M by A3;
reconsider b2 = b1 as Element of V by A1, TARSKI:def_3;
[[**a,0**],b2] in [: the carrier of F_Complex, the carrier of V:] by ZFMISC_1:87;
then ( [[**a,0**],b1] in [: the carrier of F_Complex, the carrier of M:] & [[**a,0**],b2] in dom the lmult of V ) by FUNCT_2:def_1, ZFMISC_1:87;
then [[**a,0**],b2] in (dom the lmult of V) /\ [: the carrier of F_Complex, the carrier of M:] by XBOOLE_0:def_4;
then A11: [[**a,0**],b2] in dom ( the lmult of V | [: the carrier of F_Complex, the carrier of M:]) by RELAT_1:61;
b in the carrier of (RealVS V) by A5, TARSKI:def_3;
then [a,b] in [:REAL, the carrier of (RealVS V):] by ZFMISC_1:87;
then ( [a,b] in [:REAL, the carrier of (RealVS M):] & [a,b] in dom the Mult of (RealVS V) ) by FUNCT_2:def_1, ZFMISC_1:87;
then [a,b] in (dom the Mult of (RealVS V)) /\ [:REAL, the carrier of (RealVS M):] by XBOOLE_0:def_4;
then A12: [a,b] in dom RM by RELAT_1:61;
thus the Mult of (RealVS M) . (a,b) = [**a,0**] * b1 by Def17
.= [**a,0**] * b2 by A2, A11, FUNCT_1:47
.= the Mult of (RealVS V) . (a,b) by Def17
.= RM . (a,b) by A12, FUNCT_1:47 ; ::_thesis: verum
end;
hence the Mult of (RealVS M) = the Mult of (RealVS V) | [:REAL, the carrier of (RealVS M):] by BINOP_1:2; ::_thesis: verum
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)
proof
let V be non empty VectSpStr over F_Complex ; ::_thesis: for p being RFunctional of V holds p is Functional of (RealVS V)
let p be RFunctional of V; ::_thesis: p is Functional of (RealVS V)
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
hence p is Functional of (RealVS V) ; ::_thesis: verum
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)
proof
let V be VectSp of F_Complex ; ::_thesis: for p being Semi-Norm of V holds p is Banach-Functional of (RealVS V)
let p be Semi-Norm of V; ::_thesis: p is Banach-Functional of (RealVS V)
reconsider p1 = p as Functional of (RealVS V) by Th23;
A1: p1 is positively_homogeneous
proof
let x be VECTOR of (RealVS V); :: according to HAHNBAN:def_4 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or p1 . (b1 * x) = b1 * (p1 . x) )
let r be Real; ::_thesis: ( r <= 0 or p1 . (r * x) = r * (p1 . x) )
assume A2: r > 0 ; ::_thesis: p1 . (r * x) = r * (p1 . x)
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider x1 = x as Vector of V ;
r * x = [**r,0**] * x1 by Def17;
hence p1 . (r * x) = (abs r) * (p1 . x) by Def14
.= r * (p1 . x) by A2, ABSVALUE:def_1 ;
::_thesis: verum
end;
p1 is subadditive
proof
let x, y be VECTOR of (RealVS V); :: according to HAHNBAN:def_1 ::_thesis: p1 . (x + y) <= (p1 . x) + (p1 . y)
A3: addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider x1 = x, y1 = y as Vector of V ;
x + y = x1 + y1 by A3;
hence p1 . (x + y) <= (p1 . x) + (p1 . y) by Def11; ::_thesis: verum
end;
hence p is Banach-Functional of (RealVS V) by A1; ::_thesis: verum
end;
definition
let V be non empty VectSpStr 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 b1 being Functional of (RealVS V) st
for i being Element of V holds b1 . i = Re (l . i)
proof
deffunc H1( Element of V) -> Element of REAL = Re (l . $1);
consider f being Function of the carrier of V,REAL such that
A1: for i being Element of V holds f . i = H1(i) from FUNCT_2:sch_4();
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider f = f as Functional of (RealVS V) ;
take f ; ::_thesis: for i being Element of V holds f . i = Re (l . i)
thus for i being Element of V holds f . i = Re (l . i) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Functional of (RealVS V) st ( for i being Element of V holds b1 . i = Re (l . i) ) & ( for i being Element of V holds b2 . i = Re (l . i) ) holds
b1 = b2
proof
let a, b be Functional of (RealVS V); ::_thesis: ( ( for i being Element of V holds a . i = Re (l . i) ) & ( for i being Element of V holds b . i = Re (l . i) ) implies a = b )
assume A2: for i being Element of V holds a . i = Re (l . i) ; ::_thesis: ( ex i being Element of V st not b . i = Re (l . i) or a = b )
assume A3: for i being Element of V holds b . i = Re (l . i) ; ::_thesis: a = b
now__::_thesis:_for_i_being_Element_of_(RealVS_V)_holds_a_._i_=_b_._i
let i be Element of (RealVS V); ::_thesis: a . i = b . i
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider j = i as Element of V ;
thus a . i = Re (l . j) by A2
.= b . i by A3 ; ::_thesis: verum
end;
hence a = b by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def18 defines projRe HAHNBAN1:def_18_:_
for V being non empty VectSpStr over F_Complex
for l being Functional of V
for b3 being Functional of (RealVS V) holds
( b3 = projRe l iff for i being Element of V holds b3 . i = Re (l . i) );
definition
let V be non empty VectSpStr 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 b1 being Functional of (RealVS V) st
for i being Element of V holds b1 . i = Im (l . i)
proof
deffunc H1( Element of V) -> Element of REAL = Im (l . $1);
consider f being Function of the carrier of V,REAL such that
A1: for i being Element of V holds f . i = H1(i) from FUNCT_2:sch_4();
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider f = f as Functional of (RealVS V) ;
take f ; ::_thesis: for i being Element of V holds f . i = Im (l . i)
thus for i being Element of V holds f . i = Im (l . i) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Functional of (RealVS V) st ( for i being Element of V holds b1 . i = Im (l . i) ) & ( for i being Element of V holds b2 . i = Im (l . i) ) holds
b1 = b2
proof
let a, b be Functional of (RealVS V); ::_thesis: ( ( for i being Element of V holds a . i = Im (l . i) ) & ( for i being Element of V holds b . i = Im (l . i) ) implies a = b )
assume A2: for i being Element of V holds a . i = Im (l . i) ; ::_thesis: ( ex i being Element of V st not b . i = Im (l . i) or a = b )
assume A3: for i being Element of V holds b . i = Im (l . i) ; ::_thesis: a = b
now__::_thesis:_for_i_being_Element_of_(RealVS_V)_holds_a_._i_=_b_._i
let i be Element of (RealVS V); ::_thesis: a . i = b . i
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider j = i as Element of V ;
thus a . i = Im (l . j) by A2
.= b . i by A3 ; ::_thesis: verum
end;
hence a = b by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def19 defines projIm HAHNBAN1:def_19_:_
for V being non empty VectSpStr over F_Complex
for l being Functional of V
for b3 being Functional of (RealVS V) holds
( b3 = projIm l iff for i being Element of V holds b3 . i = Im (l . i) );
definition
let V be non empty VectSpStr 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
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
hence l is RFunctional of V ; ::_thesis: verum
end;
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;
definition
let V be non empty VectSpStr 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
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
hence l is Functional of (RealVS V) ; ::_thesis: verum
end;
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;
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
let x, y be Vector of V; :: according to HAHNBAN1:def_12 ::_thesis: (RtoC l) . (x + y) = ((RtoC l) . x) + ((RtoC l) . y)
A1: addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider x1 = x, y1 = y as VECTOR of (RealVS V) ;
x + y = x1 + y1 by A1;
hence (RtoC l) . (x + y) = ((RtoC l) . x) + ((RtoC l) . y) by HAHNBAN:def_2; ::_thesis: verum
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
let x, y be VECTOR of (RealVS V); :: according to HAHNBAN:def_2 ::_thesis: (CtoR l) . (x + y) = ((CtoR l) . x) + ((CtoR l) . y)
A1: addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider x1 = x, y1 = y as Vector of V ;
x + y = x1 + y1 by A1;
hence (CtoR l) . (x + y) = ((CtoR l) . x) + ((CtoR l) . y) by Def12; ::_thesis: verum
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
let x be Vector of V; :: according to HAHNBAN1:def_13 ::_thesis: for r being Real holds (RtoC l) . ([**r,0**] * x) = r * ((RtoC l) . x)
let r be Real; ::_thesis: (RtoC l) . ([**r,0**] * x) = r * ((RtoC l) . x)
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider x1 = x as VECTOR of (RealVS V) ;
[**r,0**] * x = r * x1 by Def17;
hence (RtoC l) . ([**r,0**] * x) = r * ((RtoC l) . x) by HAHNBAN:def_3; ::_thesis: verum
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
let x be VECTOR of (RealVS V); :: according to HAHNBAN:def_3 ::_thesis: for b1 being Element of REAL holds (CtoR l) . (b1 * x) = b1 * ((CtoR l) . x)
let r be Real; ::_thesis: (CtoR l) . (r * x) = r * ((CtoR l) . x)
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider x1 = x as Vector of V ;
[**r,0**] * x1 = r * x by Def17;
hence (CtoR l) . (r * x) = r * ((CtoR l) . x) by Def13; ::_thesis: verum
end;
end;
definition
let V be non empty VectSpStr 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 b1 being RFunctional of V st
for v being Element of V holds b1 . v = l . (i_FC * v)
proof
deffunc H1( Element of V) -> Element of REAL = l . (i_FC * $1);
consider f being Function of the carrier of V,REAL such that
A1: for v being Element of V holds f . v = H1(v) from FUNCT_2:sch_4();
reconsider f = f as RFunctional of V ;
take f ; ::_thesis: for v being Element of V holds f . v = l . (i_FC * v)
thus for v being Element of V holds f . v = l . (i_FC * v) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being RFunctional of V st ( for v being Element of V holds b1 . v = l . (i_FC * v) ) & ( for v being Element of V holds b2 . v = l . (i_FC * v) ) holds
b1 = b2
proof
let F1, F2 be RFunctional of V; ::_thesis: ( ( for v being Element of V holds F1 . v = l . (i_FC * v) ) & ( for v being Element of V holds F2 . v = l . (i_FC * v) ) implies F1 = F2 )
assume that
A2: for v being Element of V holds F1 . v = l . (i_FC * v) and
A3: for v being Element of V holds F2 . v = l . (i_FC * v) ; ::_thesis: F1 = F2
now__::_thesis:_for_v_being_Element_of_V_holds_F1_._v_=_F2_._v
let v be Element of V; ::_thesis: F1 . v = F2 . v
thus F1 . v = l . (i_FC * v) by A2
.= F2 . v by A3 ; ::_thesis: verum
end;
hence F1 = F2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def22 defines i-shift HAHNBAN1:def_22_:_
for V being non empty VectSpStr over F_Complex
for l, b3 being RFunctional of V holds
( b3 = i-shift l iff for v being Element of V holds b3 . v = l . (i_FC * v) );
definition
let V be non empty VectSpStr 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 b1 being Functional of V st
for v being Element of V holds b1 . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**]
proof
deffunc H1( Element of V) -> Element of F_Complex = [**((RtoC l) . $1),(- ((i-shift (RtoC l)) . $1))**];
consider f being Function of the carrier of V, the carrier of F_Complex such that
A1: for v being Element of V holds f . v = H1(v) from FUNCT_2:sch_4();
reconsider f = f as Functional of V ;
take f ; ::_thesis: for v being Element of V holds f . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**]
thus for v being Element of V holds f . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Functional of V st ( for v being Element of V holds b1 . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] ) & ( for v being Element of V holds b2 . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] ) holds
b1 = b2
proof
let a, b be Functional of V; ::_thesis: ( ( for v being Element of V holds a . 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))**] ) implies a = b )
assume A2: for v being Element of V holds a . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] ; ::_thesis: ( ex v being Element of V st not b . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] or a = b )
assume A3: for v being Element of V holds b . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] ; ::_thesis: a = b
now__::_thesis:_for_v_being_Element_of_V_holds_a_._v_=_b_._v
let v be Element of V; ::_thesis: a . v = b . v
thus a . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] by A2
.= b . v by A3 ; ::_thesis: verum
end;
hence a = b by FUNCT_2:63; ::_thesis: verum
end;
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 b3 being Functional of V holds
( b3 = prodReIm l iff for v being Element of V holds b3 . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] );
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)
proof
let V be VectSp of F_Complex ; ::_thesis: for l being linear-Functional of V holds projRe l is linear-Functional of (RealVS V)
let l be linear-Functional of V; ::_thesis: projRe l is linear-Functional of (RealVS V)
A1: projRe l is homogeneous
proof
let x be VECTOR of (RealVS V); :: according to HAHNBAN:def_3 ::_thesis: for b1 being Element of REAL holds (projRe l) . (b1 * x) = b1 * ((projRe l) . x)
let r be Real; ::_thesis: (projRe l) . (r * x) = r * ((projRe l) . x)
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider x1 = x as Vector of V ;
r * x = [**r,0**] * x1 by Def17;
hence (projRe l) . (r * x) = Re (l . ([**r,0**] * x1)) by Def18
.= Re ([**r,0**] * (l . x1)) by Def8
.= ((Re [**r,0**]) * (Re (l . x1))) - ((Im [**r,0**]) * (Im (l . x1))) by COMPLEX1:9
.= ((Re [**r,0**]) * (Re (l . x1))) - (0 * (Im (l . x1))) by COMPLEX1:12
.= r * (Re (l . x1)) by COMPLEX1:12
.= r * ((projRe l) . x) by Def18 ;
::_thesis: verum
end;
projRe l is additive
proof
let x, y be VECTOR of (RealVS V); :: according to HAHNBAN:def_2 ::_thesis: (projRe l) . (x + y) = ((projRe l) . x) + ((projRe l) . y)
A2: addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider x1 = x, y1 = y as Vector of V ;
thus (projRe l) . (x + y) = Re (l . (x1 + y1)) by A2, Def18
.= Re ((l . x1) + (l . y1)) by VECTSP_1:def_20
.= (Re (l . x1)) + (Re (l . y1)) by COMPLEX1:8
.= (Re (l . x1)) + ((projRe l) . y) by Def18
.= ((projRe l) . x) + ((projRe l) . y) by Def18 ; ::_thesis: verum
end;
hence projRe l is linear-Functional of (RealVS V) by A1; ::_thesis: verum
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
let V be VectSp of F_Complex ; ::_thesis: for l being linear-Functional of V holds projIm l is linear-Functional of (RealVS V)
let l be linear-Functional of V; ::_thesis: projIm l is linear-Functional of (RealVS V)
A1: projIm l is homogeneous
proof
let x be VECTOR of (RealVS V); :: according to HAHNBAN:def_3 ::_thesis: for b1 being Element of REAL holds (projIm l) . (b1 * x) = b1 * ((projIm l) . x)
let r be Real; ::_thesis: (projIm l) . (r * x) = r * ((projIm l) . x)
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider x1 = x as Vector of V ;
r * x = [**r,0**] * x1 by Def17;
hence (projIm l) . (r * x) = Im (l . ([**r,0**] * x1)) by Def19
.= Im ([**r,0**] * (l . x1)) by Def8
.= ((Re [**r,0**]) * (Im (l . x1))) + ((Re (l . x1)) * (Im [**r,0**])) by COMPLEX1:9
.= ((Re [**r,0**]) * (Im (l . x1))) + ((Re (l . x1)) * 0) by COMPLEX1:12
.= r * (Im (l . x1)) by COMPLEX1:12
.= r * ((projIm l) . x) by Def19 ;
::_thesis: verum
end;
projIm l is additive
proof
let x, y be VECTOR of (RealVS V); :: according to HAHNBAN:def_2 ::_thesis: (projIm l) . (x + y) = ((projIm l) . x) + ((projIm l) . y)
A2: addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider x1 = x, y1 = y as Vector of V ;
thus (projIm l) . (x + y) = Im (l . (x1 + y1)) by A2, Def19
.= Im ((l . x1) + (l . y1)) by VECTSP_1:def_20
.= (Im (l . x1)) + (Im (l . y1)) by COMPLEX1:8
.= (Im (l . x1)) + ((projIm l) . y) by Def19
.= ((projIm l) . x) + ((projIm l) . y) by Def19 ; ::_thesis: verum
end;
hence projIm l is linear-Functional of (RealVS V) by A1; ::_thesis: verum
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
proof
let V be VectSp of F_Complex ; ::_thesis: for l being linear-Functional of (RealVS V) holds prodReIm l is linear-Functional of V
let l be linear-Functional of (RealVS V); ::_thesis: prodReIm l is linear-Functional of V
A1: prodReIm l is homogeneous
proof
let x be Vector of V; :: according to HAHNBAN1:def_8 ::_thesis: for r being Scalar of holds (prodReIm l) . (r * x) = r * ((prodReIm l) . x)
let r be Scalar of ; ::_thesis: (prodReIm l) . (r * x) = r * ((prodReIm l) . x)
reconsider r1 = r as Element of COMPLEX by COMPLFLD:def_1;
set a = Re r1;
set b = Im r1;
A2: r1 = (Re r1) + ((Im r1) * **) by COMPLEX1:13;
A3: - (1_ F_Complex) = [**(- 1),0**] by COMPLFLD:2, COMPLFLD:8;
x = (i_FC * (i_FC * (- (1_ F_Complex)))) * x by Th4, Th5, VECTSP_1:def_17
.= i_FC * (((- (1_ F_Complex)) * i_FC) * x) by VECTSP_1:def_16 ;
then A4: ((Re r1) * (- ((RtoC l) . (i_FC * x)))) + (((RtoC l) . x) * (Im r1)) = (- ((Re r1) * ((RtoC l) . (i_FC * x)))) + ((Im r1) * ((RtoC l) . (i_FC * (((- (1_ F_Complex)) * i_FC) * x))))
.= (- ((RtoC l) . ([**(Re r1),0**] * (i_FC * x)))) + (- ((- (Im r1)) * ((RtoC l) . (i_FC * (((- (1_ F_Complex)) * i_FC) * x))))) by Def13
.= (- ((RtoC l) . ([**(Re r1),0**] * (i_FC * x)))) + (- ((RtoC l) . ([**0,(- (Im r1))**] * (((- (1_ F_Complex)) * i_FC) * x)))) by Th21
.= (- ((RtoC l) . ([**(Re r1),0**] * (i_FC * x)))) + (- ((RtoC l) . ([**0,(- (Im r1))**] * ((- (1_ F_Complex)) * (i_FC * x))))) by VECTSP_1:def_16
.= (- ((RtoC l) . ([**(Re r1),0**] * (i_FC * x)))) + (- ((RtoC l) . (([**0,(- (Im r1))**] * (- (1_ F_Complex))) * (i_FC * x)))) by VECTSP_1:def_16
.= - (((RtoC l) . ([**(Re r1),0**] * (i_FC * x))) + ((RtoC l) . ([**0,(Im r1)**] * (i_FC * x)))) by A3
.= - ((RtoC l) . (([**(Re r1),0**] * (i_FC * x)) + ([**0,(Im r1)**] * (i_FC * x)))) by Def12
.= - ((RtoC l) . (([**(Re r1),0**] + [**0,(Im r1)**]) * (i_FC * x))) by VECTSP_1:def_15
.= - ((RtoC l) . ((i_FC * r) * x)) by A2, VECTSP_1:def_16 ;
A5: ((Re r1) * ((RtoC l) . x)) - ((Im r1) * (- ((RtoC l) . (i_FC * x)))) = ((Re r1) * ((RtoC l) . x)) + ((Im r1) * ((RtoC l) . (i_FC * x)))
.= ((RtoC l) . ([**(Re r1),0**] * x)) + ((Im r1) * ((RtoC l) . (i_FC * x))) by Def13
.= ((RtoC l) . ([**(Re r1),0**] * x)) + ((RtoC l) . ([**0,(Im r1)**] * x)) by Th21
.= (RtoC l) . (([**(Re r1),0**] * x) + ([**0,(Im r1)**] * x)) by Def12
.= (RtoC l) . (([**(Re r1),0**] + [**0,(Im r1)**]) * x) by VECTSP_1:def_15
.= (RtoC l) . (r * x) by COMPLEX1:13 ;
thus (prodReIm l) . (r * x) = [**((RtoC l) . (r * x)),(- ((i-shift (RtoC l)) . (r * x)))**] by Def23
.= [**((RtoC l) . (r * x)),(- ((RtoC l) . (i_FC * (r * x))))**] by Def22
.= ((RtoC l) . (r * x)) + ((((Re r1) * (- ((RtoC l) . (i_FC * x)))) + (((RtoC l) . x) * (Im r1))) * **) by A4, VECTSP_1:def_16
.= r * [**((RtoC l) . x),(- ((RtoC l) . (i_FC * x)))**] by A2, A5
.= r * [**((RtoC l) . x),(- ((i-shift (RtoC l)) . x))**] by Def22
.= r * ((prodReIm l) . x) by Def23 ; ::_thesis: verum
end;
prodReIm l is additive
proof
let x, y be Vector of V; :: according to VECTSP_1:def_20 ::_thesis: (prodReIm l) . (x + y) = ((prodReIm l) . x) + ((prodReIm l) . y)
thus (prodReIm l) . (x + y) = [**((RtoC l) . (x + y)),(- ((i-shift (RtoC l)) . (x + y)))**] by Def23
.= [**((RtoC l) . (x + y)),(- ((RtoC l) . (i_FC * (x + y))))**] by Def22
.= [**(((RtoC l) . x) + ((RtoC l) . y)),(- ((RtoC l) . (i_FC * (x + y))))**] by Def12
.= [**(((RtoC l) . x) + ((RtoC l) . y)),(- ((RtoC l) . ((i_FC * x) + (i_FC * y))))**] by VECTSP_1:def_14
.= [**(((RtoC l) . x) + ((RtoC l) . y)),(- (((RtoC l) . (i_FC * x)) + ((RtoC l) . (i_FC * y))))**] by Def12
.= [**((RtoC l) . x),(- ((RtoC l) . (i_FC * x)))**] + [**((RtoC l) . y),(- ((RtoC l) . (i_FC * y)))**]
.= [**((RtoC l) . x),(- ((i-shift (RtoC l)) . x))**] + [**((RtoC l) . y),(- ((RtoC l) . (i_FC * y)))**] by Def22
.= [**((RtoC l) . x),(- ((i-shift (RtoC l)) . x))**] + [**((RtoC l) . y),(- ((i-shift (RtoC l)) . y))**] by Def22
.= ((prodReIm l) . x) + [**((RtoC l) . y),(- ((i-shift (RtoC l)) . y))**] by Def23
.= ((prodReIm l) . x) + ((prodReIm l) . y) by Def23 ; ::_thesis: verum
end;
hence prodReIm l is linear-Functional of V by A1; ::_thesis: verum
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 ) )
proof
let V be VectSp of F_Complex ; ::_thesis: 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 ) )
let p be Semi-Norm of V; ::_thesis: 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 ) )
reconsider p1 = p as Banach-Functional of (RealVS V) by Th24;
let M be Subspace of V; ::_thesis: 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 ) )
reconsider tcM = the carrier of M as Subset of V by VECTSP_4:def_2;
reconsider RVSM = RealVS M as Subspace of RealVS V by Th22;
let l be linear-Functional of M; ::_thesis: ( ( for e being Vector of M
for v being Vector of V st v = e holds
|.(l . e).| <= p . v ) implies 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 ) ) )
reconsider prRl = projRe l as linear-Functional of RVSM by Th25;
A1: addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
A2: addLoopStr(# the carrier of M, the addF of M, the ZeroF of M #) = addLoopStr(# the carrier of (RealVS M), the addF of (RealVS M), the ZeroF of (RealVS M) #) by Def17;
assume A3: for e being Vector of M
for v being Vector of V st v = e holds
|.(l . e).| <= p . v ; ::_thesis: 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 x being VECTOR of RVSM
for v being VECTOR of (RealVS V) st x = v holds
prRl . x <= p1 . v
proof
let x be VECTOR of RVSM; ::_thesis: for v being VECTOR of (RealVS V) st x = v holds
prRl . x <= p1 . v
reconsider x1 = x as Vector of M by A2;
let v be VECTOR of (RealVS V); ::_thesis: ( x = v implies prRl . x <= p1 . v )
reconsider v1 = v as Vector of V by A1;
prRl . x = Re (l . x1) by Def18;
then A4: prRl . x <= |.(l . x1).| by COMPLEX1:54;
assume x = v ; ::_thesis: prRl . x <= p1 . v
then |.(l . x1).| <= p . v1 by A3;
hence prRl . x <= p1 . v by A4, XXREAL_0:2; ::_thesis: verum
end;
then consider L1 being linear-Functional of (RealVS V) such that
A5: L1 | the carrier of RVSM = prRl and
A6: for e being VECTOR of (RealVS V) holds L1 . e <= p1 . e by HAHNBAN:22;
reconsider L = prodReIm L1 as linear-Functional of V by Th27;
take L ; ::_thesis: ( L | the carrier of M = l & ( for e being Vector of V holds |.(L . e).| <= p . e ) )
now__::_thesis:_for_x_being_Element_of_M_holds_(L_|_tcM)_._x_=_l_._x
let x be Element of M; ::_thesis: (L | tcM) . x = l . x
the carrier of M c= the carrier of V by VECTSP_4:def_2;
then reconsider x2 = x as Element of V by TARSKI:def_3;
reconsider x1 = x2, ix1 = i_FC * x2 as Element of (RealVS V) by A1;
reconsider lx = l . x as Element of COMPLEX by COMPLFLD:def_1;
lx = (Re lx) + ((Im lx) * **) by COMPLEX1:13;
then A7: i_FC * (l . x) = ((0 * (Re lx)) - (1 * (Im lx))) + (((0 * (Im lx)) + (1 * (Re lx))) * **) ;
A8: i_FC * x = i_FC * x2 by VECTSP_4:14;
then A9: L1 . ix1 = (projRe l) . ix1 by A2, A5, FUNCT_1:49
.= Re (l . (i_FC * x)) by A8, Def18
.= Re ((- (Im lx)) + ((Re lx) * **)) by A7, Def8
.= - (Im (l . x)) by COMPLEX1:12 ;
A10: L1 . x1 = (projRe l) . x1 by A2, A5, FUNCT_1:49
.= Re (l . x) by Def18 ;
thus (L | tcM) . x = L . x by FUNCT_1:49
.= [**((RtoC L1) . x2),(- ((i-shift (RtoC L1)) . x2))**] by Def23
.= [**(Re (l . x)),(- ((RtoC L1) . (i_FC * x2)))**] by A10, Def22
.= l . x by A9, COMPLEX1:13 ; ::_thesis: verum
end;
hence L | the carrier of M = l by FUNCT_2:63; ::_thesis: for e being Vector of V holds |.(L . e).| <= p . e
let e be Vector of V; ::_thesis: |.(L . e).| <= p . e
reconsider Le = L . e as Element of COMPLEX by COMPLFLD:def_1;
reconsider Ledz = (Le *') / |.Le.| as Element of F_Complex by COMPLFLD:def_1;
reconsider e1 = e, Ledze = Ledz * e as VECTOR of (RealVS V) by A1;
percases ( |.Le.| <> 0 or |.Le.| = 0 ) ;
supposeA11: |.Le.| <> 0 ; ::_thesis: |.(L . e).| <= p . e
A12: |.Ledz.| = |.(Le *').| / |.|.Le.|.| by COMPLEX1:67
.= |.Le.| / |.Le.| by COMPLEX1:53
.= 1 by A11, XCMPLX_1:60 ;
|.Le.| + (0 * **) = Ledz * (L . e) by Th3
.= L . (Ledz * e) by Def8
.= [**((RtoC L1) . (Ledz * e)),(- ((i-shift (RtoC L1)) . (Ledz * e)))**] by Def23
.= (L1 . Ledze) + ((- ((i-shift (RtoC L1)) . (Ledz * e))) * **) ;
then A13: L1 . Ledze = |.(L . e).| by COMPLEX1:77;
p1 . Ledze = |.Ledz.| * (p . e) by Def14
.= p . e by A12 ;
hence |.(L . e).| <= p . e by A6, A13; ::_thesis: verum
end;
supposeA14: |.Le.| = 0 ; ::_thesis: |.(L . e).| <= p . e
|.(L . e).| = |.[**((RtoC L1) . e),(- ((i-shift (RtoC L1)) . e))**].| by Def23
.= |.(((RtoC L1) . e) + ((- ((i-shift (RtoC L1)) . e)) * **)).| ;
then ((RtoC L1) . e) + ((- ((i-shift (RtoC L1)) . e)) * **) = 0 + (0 * **) by A14, COMPLEX1:45;
then L1 . e1 = 0 by COMPLEX1:77;
hence |.(L . e).| <= p . e by A6, A14; ::_thesis: verum
end;
end;
end;
begin
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**]
proof
let x be Real; ::_thesis: ( x > 0 implies for n being Element of NAT holds (power F_Complex) . ([**x,0**],n) = [**(x to_power n),0**] )
defpred S1[ Element of NAT ] means (power F_Complex) . ([**x,0**],$1) = [**(x to_power $1),0**];
assume A1: x > 0 ; ::_thesis: for n being Element of NAT holds (power F_Complex) . ([**x,0**],n) = [**(x to_power n),0**]
A2: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume S1[n] ; ::_thesis: S1[n + 1]
then (power F_Complex) . ([**x,0**],(n + 1)) = [**(x to_power n),0**] * [**x,0**] by GROUP_1:def_7
.= [**((x to_power n) * (x to_power 1)),0**] by POWER:25
.= [**(x to_power (n + 1)),0**] by A1, POWER:27 ;
hence S1[n + 1] ; ::_thesis: verum
end;
(power F_Complex) . ([**x,0**],0) = 1r + (0 * **) by COMPLFLD:8, GROUP_1:def_7
.= [**(x to_power 0),0**] by POWER:24 ;
then A3: S1[ 0 ] ;
thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2); ::_thesis: verum
end;
*