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