:: Complex Linear Space of Complex Sequences :: by Noboru Endou :: :: Received January 26, 2004 :: Copyright (c) 2004-2012 Association of Mizar Users begin definition func the_set_of_ComplexSequences -> non empty set means :Def1: :: CSSPACE:def 1 for x being set holds ( x in it iff x is Complex_Sequence ); existence ex b1 being non empty set st for x being set holds ( x in b1 iff x is Complex_Sequence ) proofend; uniqueness for b1, b2 being non empty set st ( for x being set holds ( x in b1 iff x is Complex_Sequence ) ) & ( for x being set holds ( x in b2 iff x is Complex_Sequence ) ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines the_set_of_ComplexSequences CSSPACE:def_1_:_ for b1 being non empty set holds ( b1 = the_set_of_ComplexSequences iff for x being set holds ( x in b1 iff x is Complex_Sequence ) ); definition let z be set ; assume A1: z in the_set_of_ComplexSequences ; func seq_id z -> Complex_Sequence equals :Def2: :: CSSPACE:def 2 z; coherence z is Complex_Sequence by A1, Def1; end; :: deftheorem Def2 defines seq_id CSSPACE:def_2_:_ for z being set st z in the_set_of_ComplexSequences holds seq_id z = z; definition let z be set ; assume A1: z is Complex ; func C_id z -> Complex equals :Def3: :: CSSPACE:def 3 z; coherence z is Complex by A1; end; :: deftheorem Def3 defines C_id CSSPACE:def_3_:_ for z being set st z is Complex holds C_id z = z; definition func l_add -> BinOp of the_set_of_ComplexSequences means :Def4: :: CSSPACE:def 4 for a, b being Element of the_set_of_ComplexSequences holds it . (a,b) = (seq_id a) + (seq_id b); existence ex b1 being BinOp of the_set_of_ComplexSequences st for a, b being Element of the_set_of_ComplexSequences holds b1 . (a,b) = (seq_id a) + (seq_id b) proofend; uniqueness for b1, b2 being BinOp of the_set_of_ComplexSequences st ( for a, b being Element of the_set_of_ComplexSequences holds b1 . (a,b) = (seq_id a) + (seq_id b) ) & ( for a, b being Element of the_set_of_ComplexSequences holds b2 . (a,b) = (seq_id a) + (seq_id b) ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines l_add CSSPACE:def_4_:_ for b1 being BinOp of the_set_of_ComplexSequences holds ( b1 = l_add iff for a, b being Element of the_set_of_ComplexSequences holds b1 . (a,b) = (seq_id a) + (seq_id b) ); definition func l_mult -> Function of [:COMPLEX,the_set_of_ComplexSequences:],the_set_of_ComplexSequences means :Def5: :: CSSPACE:def 5 for z, x being set st z is Complex & x in the_set_of_ComplexSequences holds it . (z,x) = (C_id z) (#) (seq_id x); existence ex b1 being Function of [:COMPLEX,the_set_of_ComplexSequences:],the_set_of_ComplexSequences st for z, x being set st z is Complex & x in the_set_of_ComplexSequences holds b1 . (z,x) = (C_id z) (#) (seq_id x) proofend; uniqueness for b1, b2 being Function of [:COMPLEX,the_set_of_ComplexSequences:],the_set_of_ComplexSequences st ( for z, x being set st z is Complex & x in the_set_of_ComplexSequences holds b1 . (z,x) = (C_id z) (#) (seq_id x) ) & ( for z, x being set st z is Complex & x in the_set_of_ComplexSequences holds b2 . (z,x) = (C_id z) (#) (seq_id x) ) holds b1 = b2 proofend; end; :: deftheorem Def5 defines l_mult CSSPACE:def_5_:_ for b1 being Function of [:COMPLEX,the_set_of_ComplexSequences:],the_set_of_ComplexSequences holds ( b1 = l_mult iff for z, x being set st z is Complex & x in the_set_of_ComplexSequences holds b1 . (z,x) = (C_id z) (#) (seq_id x) ); definition func CZeroseq -> Element of the_set_of_ComplexSequences means :Def6: :: CSSPACE:def 6 for n being Element of NAT holds (seq_id it) . n = 0c ; existence ex b1 being Element of the_set_of_ComplexSequences st for n being Element of NAT holds (seq_id b1) . n = 0c proofend; uniqueness for b1, b2 being Element of the_set_of_ComplexSequences st ( for n being Element of NAT holds (seq_id b1) . n = 0c ) & ( for n being Element of NAT holds (seq_id b2) . n = 0c ) holds b1 = b2 proofend; end; :: deftheorem Def6 defines CZeroseq CSSPACE:def_6_:_ for b1 being Element of the_set_of_ComplexSequences holds ( b1 = CZeroseq iff for n being Element of NAT holds (seq_id b1) . n = 0c ); theorem Th1: :: CSSPACE:1 for x being Complex_Sequence holds seq_id x = x proofend; theorem :: CSSPACE:2 for v, w being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) holds v + w = (seq_id v) + (seq_id w) by Def4; theorem Th3: :: CSSPACE:3 for z being Complex for v being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) holds z * v = z (#) (seq_id v) proofend; registration cluster CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) -> Abelian ; coherence CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) is Abelian proofend; end; theorem Th4: :: CSSPACE:4 for u, v, w being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) holds (u + v) + w = u + (v + w) proofend; theorem Th5: :: CSSPACE:5 for v being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) holds v + (0. CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #)) = v proofend; theorem Th6: :: CSSPACE:6 for v being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) ex w being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) st v + w = 0. CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) proofend; theorem Th7: :: CSSPACE:7 for z being Complex for v, w being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) holds z * (v + w) = (z * v) + (z * w) proofend; theorem Th8: :: CSSPACE:8 for z1, z2 being Complex for v being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) holds (z1 + z2) * v = (z1 * v) + (z2 * v) proofend; theorem Th9: :: CSSPACE:9 for z1, z2 being Complex for v being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) holds (z1 * z2) * v = z1 * (z2 * v) proofend; theorem Th10: :: CSSPACE:10 for v being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) holds 1r * v = v proofend; definition func Linear_Space_of_ComplexSequences -> non empty strict CLSStruct equals :: CSSPACE:def 7 CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #); coherence CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) is non empty strict CLSStruct ; end; :: deftheorem defines Linear_Space_of_ComplexSequences CSSPACE:def_7_:_ Linear_Space_of_ComplexSequences = CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #); registration cluster Linear_Space_of_ComplexSequences -> non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ; coherence ( Linear_Space_of_ComplexSequences is Abelian & Linear_Space_of_ComplexSequences is add-associative & Linear_Space_of_ComplexSequences is right_zeroed & Linear_Space_of_ComplexSequences is right_complementable & Linear_Space_of_ComplexSequences is vector-distributive & Linear_Space_of_ComplexSequences is scalar-distributive & Linear_Space_of_ComplexSequences is scalar-associative & Linear_Space_of_ComplexSequences is scalar-unital ) proofend; end; definition let X be ComplexLinearSpace; let X1 be Subset of X; assume B1: X1 is linearly-closed ; func Add_ (X1,X) -> BinOp of X1 equals :Def8: :: CSSPACE:def 8 the addF of X || X1; correctness coherence the addF of X || X1 is BinOp of X1; proofend; end; :: deftheorem Def8 defines Add_ CSSPACE:def_8_:_ for X being ComplexLinearSpace for X1 being Subset of X st X1 is linearly-closed holds Add_ (X1,X) = the addF of X || X1; definition let X be ComplexLinearSpace; let X1 be Subset of X; assume B1: X1 is linearly-closed ; func Mult_ (X1,X) -> Function of [:COMPLEX,X1:],X1 equals :Def9: :: CSSPACE:def 9 the Mult of X | [:COMPLEX,X1:]; correctness coherence the Mult of X | [:COMPLEX,X1:] is Function of [:COMPLEX,X1:],X1; proofend; end; :: deftheorem Def9 defines Mult_ CSSPACE:def_9_:_ for X being ComplexLinearSpace for X1 being Subset of X st X1 is linearly-closed holds Mult_ (X1,X) = the Mult of X | [:COMPLEX,X1:]; definition let X be ComplexLinearSpace; let X1 be Subset of X; assume that A1: X1 is linearly-closed and A2: not X1 is empty ; func Zero_ (X1,X) -> Element of X1 equals :Def10: :: CSSPACE:def 10 0. X; correctness coherence 0. X is Element of X1; proofend; end; :: deftheorem Def10 defines Zero_ CSSPACE:def_10_:_ for X being ComplexLinearSpace for X1 being Subset of X st X1 is linearly-closed & not X1 is empty holds Zero_ (X1,X) = 0. X; theorem Th11: :: CSSPACE:11 for V being ComplexLinearSpace for V1 being Subset of V st V1 is linearly-closed & not V1 is empty holds CLSStruct(# V1,(Zero_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)) #) is Subspace of V proofend; definition func the_set_of_l2ComplexSequences -> Subset of Linear_Space_of_ComplexSequences means :Def11: :: CSSPACE:def 11 ( not it is empty & ( for x being set holds ( x in it iff ( x in the_set_of_ComplexSequences & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) ) ); existence ex b1 being Subset of Linear_Space_of_ComplexSequences st ( not b1 is empty & ( for x being set holds ( x in b1 iff ( x in the_set_of_ComplexSequences & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) ) ) proofend; uniqueness for b1, b2 being Subset of Linear_Space_of_ComplexSequences st not b1 is empty & ( for x being set holds ( x in b1 iff ( x in the_set_of_ComplexSequences & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) ) & not b2 is empty & ( for x being set holds ( x in b2 iff ( x in the_set_of_ComplexSequences & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def11 defines the_set_of_l2ComplexSequences CSSPACE:def_11_:_ for b1 being Subset of Linear_Space_of_ComplexSequences holds ( b1 = the_set_of_l2ComplexSequences iff ( not b1 is empty & ( for x being set holds ( x in b1 iff ( x in the_set_of_ComplexSequences & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) ) ) ); theorem Th12: :: CSSPACE:12 ( the_set_of_l2ComplexSequences is linearly-closed & not the_set_of_l2ComplexSequences is empty ) proofend; theorem :: CSSPACE:13 CLSStruct(# the_set_of_l2ComplexSequences,(Zero_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)) #) is Subspace of Linear_Space_of_ComplexSequences by Th11, Th12; theorem Th14: :: CSSPACE:14 CLSStruct(# the_set_of_l2ComplexSequences,(Zero_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)) #) is ComplexLinearSpace by Th11, Th12; theorem :: CSSPACE:15 ( the carrier of Linear_Space_of_ComplexSequences = the_set_of_ComplexSequences & ( for x being set holds ( x is Element of Linear_Space_of_ComplexSequences iff x is Complex_Sequence ) ) & ( for x being set holds ( x is VECTOR of Linear_Space_of_ComplexSequences iff x is Complex_Sequence ) ) & ( for u being VECTOR of Linear_Space_of_ComplexSequences holds u = seq_id u ) & ( for u, v being VECTOR of Linear_Space_of_ComplexSequences holds u + v = (seq_id u) + (seq_id v) ) & ( for z being Complex for u being VECTOR of Linear_Space_of_ComplexSequences holds z * u = z (#) (seq_id u) ) ) by Def1, Def2, Def4, Th3; begin definition attrc1 is strict ; struct CUNITSTR -> CLSStruct ; aggrCUNITSTR(# carrier, ZeroF, addF, Mult, scalar #) -> CUNITSTR ; sel scalar c1 -> Function of [: the carrier of c1, the carrier of c1:],COMPLEX; end; registration cluster non empty strict for CUNITSTR ; existence ex b1 being CUNITSTR st ( not b1 is empty & b1 is strict ) proofend; end; registration let D be non empty set ; let Z be Element of D; let a be BinOp of D; let m be Function of [:COMPLEX,D:],D; let s be Function of [:D,D:],COMPLEX; cluster CUNITSTR(# D,Z,a,m,s #) -> non empty ; coherence not CUNITSTR(# D,Z,a,m,s #) is empty ; end; deffunc H1( CUNITSTR ) -> Element of the carrier of $1 = 0. $1; definition let X be non empty CUNITSTR ; let x, y be Point of X; funcx .|. y -> Complex equals :: CSSPACE:def 12 the scalar of X . (x,y); correctness coherence the scalar of X . (x,y) is Complex; ; end; :: deftheorem defines .|. CSSPACE:def_12_:_ for X being non empty CUNITSTR for x, y being Point of X holds x .|. y = the scalar of X . (x,y); set V0 = the ComplexLinearSpace; Lm1: the carrier of ((0). the ComplexLinearSpace) = {(0. the ComplexLinearSpace)} by CLVECT_1:def_9; reconsider nilfunc = [: the carrier of ((0). the ComplexLinearSpace), the carrier of ((0). the ComplexLinearSpace):] --> 0c as Function of [: the carrier of ((0). the ComplexLinearSpace), the carrier of ((0). the ComplexLinearSpace):],COMPLEX ; Lm2: for x, y being VECTOR of ((0). the ComplexLinearSpace) holds nilfunc . [x,y] = 0c by FUNCOP_1:7; 0. the ComplexLinearSpace in the carrier of ((0). the ComplexLinearSpace) by Lm1, TARSKI:def_1; then Lm3: nilfunc . [(0. the ComplexLinearSpace),(0. the ComplexLinearSpace)] = 0c by Lm2; Lm4: for u being VECTOR of ((0). the ComplexLinearSpace) holds ( 0 <= Re (nilfunc . [u,u]) & Im (nilfunc . [u,u]) = 0 ) by COMPLEX1:4, FUNCOP_1:7; Lm5: for u, v being VECTOR of ((0). the ComplexLinearSpace) holds nilfunc . [u,v] = (nilfunc . [v,u]) *' proofend; Lm6: for u, v, w being VECTOR of ((0). the ComplexLinearSpace) holds nilfunc . [(u + v),w] = (nilfunc . [u,w]) + (nilfunc . [v,w]) proofend; Lm7: for u, v being VECTOR of ((0). the ComplexLinearSpace) for a being Complex holds nilfunc . [(a * u),v] = a * (nilfunc . [u,v]) proofend; set X0 = CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #); Lm8: now__::_thesis:_for_x,_y,_z_being_Point_of_CUNITSTR(#_the_carrier_of_((0)._the_ComplexLinearSpace),(0._((0)._the_ComplexLinearSpace)),_the_addF_of_((0)._the_ComplexLinearSpace),_the_Mult_of_((0)._the_ComplexLinearSpace),nilfunc_#) for_a_being_Complex_holds_ (_(_x_.|._x_=_0c_implies_x_=_H1(_CUNITSTR(#_the_carrier_of_((0)._the_ComplexLinearSpace),(0._((0)._the_ComplexLinearSpace)),_the_addF_of_((0)._the_ComplexLinearSpace),_the_Mult_of_((0)._the_ComplexLinearSpace),nilfunc_#))_)_&_(_x_=_H1(_CUNITSTR(#_the_carrier_of_((0)._the_ComplexLinearSpace),(0._((0)._the_ComplexLinearSpace)),_the_addF_of_((0)._the_ComplexLinearSpace),_the_Mult_of_((0)._the_ComplexLinearSpace),nilfunc_#))_implies_x_.|._x_=_0c_)_&_0_<=_Re_(x_.|._x)_&_0_=_Im_(x_.|._x)_&_x_.|._y_=_(y_.|._x)_*'_&_(x_+_y)_.|._z_=_(x_.|._z)_+_(y_.|._z)_&_(a_*_x)_.|._y_=_a_*_(x_.|._y)_) let x, y, z be Point of CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #); ::_thesis: for a being Complex holds ( ( x .|. x = 0c implies x = H1( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)) ) & ( x = H1( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)) implies x .|. x = 0c ) & 0 <= Re (x .|. x) & 0 = Im (x .|. x) & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) ) let a be Complex; ::_thesis: ( ( x .|. x = 0c implies x = H1( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)) ) & ( x = H1( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)) implies x .|. x = 0c ) & 0 <= Re (x .|. x) & 0 = Im (x .|. x) & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) ) H1( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)) = 0. the ComplexLinearSpace by CLVECT_1:30; hence ( x .|. x = 0c iff x = H1( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)) ) by Lm1, Lm2, TARSKI:def_1; ::_thesis: ( 0 <= Re (x .|. x) & 0 = Im (x .|. x) & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) ) thus ( 0 <= Re (x .|. x) & 0 = Im (x .|. x) ) by Lm4; ::_thesis: ( x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) ) thus x .|. y = (y .|. x) *' by Lm5; ::_thesis: ( (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) ) thus (x + y) .|. z = (x .|. z) + (y .|. z) ::_thesis: (a * x) .|. y = a * (x .|. y) proof reconsider u = x, v = y, w = z as VECTOR of ((0). the ComplexLinearSpace) ; (x + y) .|. z = nilfunc . [(u + v),w] ; hence (x + y) .|. z = (x .|. z) + (y .|. z) by Lm6; ::_thesis: verum end; thus (a * x) .|. y = a * (x .|. y) ::_thesis: verum proof reconsider u = x, v = y as VECTOR of ((0). the ComplexLinearSpace) ; (a * x) .|. y = nilfunc . [(a * u),v] ; hence (a * x) .|. y = a * (x .|. y) by Lm7; ::_thesis: verum end; end; definition let IT be non empty CUNITSTR ; attrIT is ComplexUnitarySpace-like means :Def13: :: CSSPACE:def 13 for x, y, w being Point of IT for a being Complex holds ( ( x .|. x = 0 implies x = 0. IT ) & ( x = 0. IT implies x .|. x = 0 ) & 0 <= Re (x .|. x) & 0 = Im (x .|. x) & x .|. y = (y .|. x) *' & (x + y) .|. w = (x .|. w) + (y .|. w) & (a * x) .|. y = a * (x .|. y) ); end; :: deftheorem Def13 defines ComplexUnitarySpace-like CSSPACE:def_13_:_ for IT being non empty CUNITSTR holds ( IT is ComplexUnitarySpace-like iff for x, y, w being Point of IT for a being Complex holds ( ( x .|. x = 0 implies x = 0. IT ) & ( x = 0. IT implies x .|. x = 0 ) & 0 <= Re (x .|. x) & 0 = Im (x .|. x) & x .|. y = (y .|. x) *' & (x + y) .|. w = (x .|. w) + (y .|. w) & (a * x) .|. y = a * (x .|. y) ) ); registration cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ComplexUnitarySpace-like for CUNITSTR ; existence ex b1 being non empty CUNITSTR st ( b1 is ComplexUnitarySpace-like & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is strict ) proofend; end; definition mode ComplexUnitarySpace is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ComplexUnitarySpace-like CUNITSTR ; end; theorem :: CSSPACE:16 for X being ComplexUnitarySpace holds (0. X) .|. (0. X) = 0 by Def13; theorem Th17: :: CSSPACE:17 for X being ComplexUnitarySpace for x, y, z being Point of X holds x .|. (y + z) = (x .|. y) + (x .|. z) proofend; theorem Th18: :: CSSPACE:18 for a being Complex for X being ComplexUnitarySpace for x, y being Point of X holds x .|. (a * y) = (a *') * (x .|. y) proofend; theorem Th19: :: CSSPACE:19 for a being Complex for X being ComplexUnitarySpace for x, y being Point of X holds (a * x) .|. y = x .|. ((a *') * y) proofend; theorem Th20: :: CSSPACE:20 for a, b being Complex for X being ComplexUnitarySpace for x, y, z being Point of X holds ((a * x) + (b * y)) .|. z = (a * (x .|. z)) + (b * (y .|. z)) proofend; theorem Th21: :: CSSPACE:21 for a, b being Complex for X being ComplexUnitarySpace for x, y, z being Point of X holds x .|. ((a * y) + (b * z)) = ((a *') * (x .|. y)) + ((b *') * (x .|. z)) proofend; theorem Th22: :: CSSPACE:22 for X being ComplexUnitarySpace for x, y being Point of X holds (- x) .|. y = x .|. (- y) proofend; theorem Th23: :: CSSPACE:23 for X being ComplexUnitarySpace for x, y being Point of X holds (- x) .|. y = - (x .|. y) proofend; theorem Th24: :: CSSPACE:24 for X being ComplexUnitarySpace for x, y being Point of X holds x .|. (- y) = - (x .|. y) proofend; theorem Th25: :: CSSPACE:25 for X being ComplexUnitarySpace for x, y being Point of X holds (- x) .|. (- y) = x .|. y proofend; theorem Th26: :: CSSPACE:26 for X being ComplexUnitarySpace for x, y, z being Point of X holds (x - y) .|. z = (x .|. z) - (y .|. z) proofend; theorem Th27: :: CSSPACE:27 for X being ComplexUnitarySpace for x, y, z being Point of X holds x .|. (y - z) = (x .|. y) - (x .|. z) proofend; theorem :: CSSPACE:28 for X being ComplexUnitarySpace for x, y, u, v being Point of X holds (x - y) .|. (u - v) = (((x .|. u) - (x .|. v)) - (y .|. u)) + (y .|. v) proofend; theorem Th29: :: CSSPACE:29 for X being ComplexUnitarySpace for x being Point of X holds (0. X) .|. x = 0 proofend; theorem Th30: :: CSSPACE:30 for X being ComplexUnitarySpace for x being Point of X holds x .|. (0. X) = 0 proofend; theorem Th31: :: CSSPACE:31 for X being ComplexUnitarySpace for x, y being Point of X holds (x + y) .|. (x + y) = (((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y) proofend; theorem :: CSSPACE:32 for X being ComplexUnitarySpace for x, y being Point of X holds (x + y) .|. (x - y) = (((x .|. x) - (x .|. y)) + (y .|. x)) - (y .|. y) proofend; theorem Th33: :: CSSPACE:33 for X being ComplexUnitarySpace for x, y being Point of X holds (x - y) .|. (x - y) = (((x .|. x) - (x .|. y)) - (y .|. x)) + (y .|. y) proofend; Lm9: for X being ComplexUnitarySpace for p, q being Complex for x, y being Point of X holds ((p * x) + (q * y)) .|. ((p * x) + (q * y)) = ((((p * (p *')) * (x .|. x)) + ((p * (q *')) * (x .|. y))) + (((p *') * q) * (y .|. x))) + ((q * (q *')) * (y .|. y)) proofend; theorem Th34: :: CSSPACE:34 for X being ComplexUnitarySpace for x being Point of X holds |.(x .|. x).| = Re (x .|. x) proofend; theorem Th35: :: CSSPACE:35 for X being ComplexUnitarySpace for x, y being Point of X holds |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) proofend; definition let X be ComplexUnitarySpace; let x, y be Point of X; predx,y are_orthogonal means :Def14: :: CSSPACE:def 14 x .|. y = 0 ; symmetry for x, y being Point of X st x .|. y = 0 holds y .|. x = 0 by Def13, COMPLEX1:28; end; :: deftheorem Def14 defines are_orthogonal CSSPACE:def_14_:_ for X being ComplexUnitarySpace for x, y being Point of X holds ( x,y are_orthogonal iff x .|. y = 0 ); theorem :: CSSPACE:36 for X being ComplexUnitarySpace for x, y being Point of X st x,y are_orthogonal holds x, - y are_orthogonal proofend; theorem :: CSSPACE:37 for X being ComplexUnitarySpace for x, y being Point of X st x,y are_orthogonal holds - x,y are_orthogonal proofend; theorem :: CSSPACE:38 for X being ComplexUnitarySpace for x, y being Point of X st x,y are_orthogonal holds - x, - y are_orthogonal proofend; theorem :: CSSPACE:39 for X being ComplexUnitarySpace for x being Point of X holds x, 0. X are_orthogonal proofend; theorem :: CSSPACE:40 for X being ComplexUnitarySpace for x, y being Point of X st x,y are_orthogonal holds (x + y) .|. (x + y) = (x .|. x) + (y .|. y) proofend; theorem :: CSSPACE:41 for X being ComplexUnitarySpace for x, y being Point of X st x,y are_orthogonal holds (x - y) .|. (x - y) = (x .|. x) + (y .|. y) proofend; definition let X be ComplexUnitarySpace; let x be Point of X; func||.x.|| -> Real equals :: CSSPACE:def 15 sqrt |.(x .|. x).|; correctness coherence sqrt |.(x .|. x).| is Real; ; end; :: deftheorem defines ||. CSSPACE:def_15_:_ for X being ComplexUnitarySpace for x being Point of X holds ||.x.|| = sqrt |.(x .|. x).|; theorem Th42: :: CSSPACE:42 for X being ComplexUnitarySpace for x being Point of X holds ( ||.x.|| = 0 iff x = 0. X ) proofend; theorem Th43: :: CSSPACE:43 for a being Complex for X being ComplexUnitarySpace for x being Point of X holds ||.(a * x).|| = |.a.| * ||.x.|| proofend; theorem Th44: :: CSSPACE:44 for X being ComplexUnitarySpace for x being Point of X holds 0 <= ||.x.|| proofend; theorem :: CSSPACE:45 for X being ComplexUnitarySpace for x, y being Point of X holds |.(x .|. y).| <= ||.x.|| * ||.y.|| by Th35; theorem Th46: :: CSSPACE:46 for X being ComplexUnitarySpace for x, y being Point of X holds ||.(x + y).|| <= ||.x.|| + ||.y.|| proofend; theorem Th47: :: CSSPACE:47 for X being ComplexUnitarySpace for x being Point of X holds ||.(- x).|| = ||.x.|| proofend; theorem Th48: :: CSSPACE:48 for X being ComplexUnitarySpace for x, y being Point of X holds ||.x.|| - ||.y.|| <= ||.(x - y).|| proofend; theorem :: CSSPACE:49 for X being ComplexUnitarySpace for x, y being Point of X holds abs (||.x.|| - ||.y.||) <= ||.(x - y).|| proofend; definition let X be ComplexUnitarySpace; let x, y be Point of X; func dist (x,y) -> Real equals :: CSSPACE:def 16 ||.(x - y).||; correctness coherence ||.(x - y).|| is Real; ; end; :: deftheorem defines dist CSSPACE:def_16_:_ for X being ComplexUnitarySpace for x, y being Point of X holds dist (x,y) = ||.(x - y).||; definition let X be ComplexUnitarySpace; let x, y be Point of X; :: original:dist redefine func dist (x,y) -> Real; commutativity for x, y being Point of X holds dist (x,y) = dist (y,x) proofend; end; theorem Th50: :: CSSPACE:50 for X being ComplexUnitarySpace for x being Point of X holds dist (x,x) = 0 proofend; theorem :: CSSPACE:51 for X being ComplexUnitarySpace for x, z, y being Point of X holds dist (x,z) <= (dist (x,y)) + (dist (y,z)) proofend; theorem Th52: :: CSSPACE:52 for X being ComplexUnitarySpace for x, y being Point of X holds ( x <> y iff dist (x,y) <> 0 ) proofend; theorem :: CSSPACE:53 for X being ComplexUnitarySpace for x, y being Point of X holds dist (x,y) >= 0 by Th44; theorem :: CSSPACE:54 for X being ComplexUnitarySpace for x, y being Point of X holds ( x <> y iff dist (x,y) > 0 ) proofend; theorem :: CSSPACE:55 for X being ComplexUnitarySpace for x, y being Point of X holds dist (x,y) = sqrt |.((x - y) .|. (x - y)).| ; theorem :: CSSPACE:56 for X being ComplexUnitarySpace for x, y, u, v being Point of X holds dist ((x + y),(u + v)) <= (dist (x,u)) + (dist (y,v)) proofend; theorem :: CSSPACE:57 for X being ComplexUnitarySpace for x, y, u, v being Point of X holds dist ((x - y),(u - v)) <= (dist (x,u)) + (dist (y,v)) proofend; theorem :: CSSPACE:58 for X being ComplexUnitarySpace for x, z, y being Point of X holds dist ((x - z),(y - z)) = dist (x,y) proofend; theorem :: CSSPACE:59 for X being ComplexUnitarySpace for x, z, y being Point of X holds dist ((x - z),(y - z)) <= (dist (z,x)) + (dist (z,y)) proofend; definition let X be ComplexUnitarySpace; let seq1, seq2 be sequence of X; :: original:+ redefine funcseq1 + seq2 -> Element of bool [:NAT, the carrier of X:]; commutativity for seq1, seq2 being sequence of X holds seq1 + seq2 = seq2 + seq1 proofend; end; theorem :: CSSPACE:60 for X being ComplexUnitarySpace for seq1, seq2, seq3 being sequence of X holds seq1 + (seq2 + seq3) = (seq1 + seq2) + seq3 proofend; theorem :: CSSPACE:61 for X being ComplexUnitarySpace for seq1, seq2, seq being sequence of X st seq1 is constant & seq2 is constant & seq = seq1 + seq2 holds seq is constant proofend; theorem :: CSSPACE:62 for X being ComplexUnitarySpace for seq1, seq2, seq being sequence of X st seq1 is constant & seq2 is constant & seq = seq1 - seq2 holds seq is constant proofend; theorem :: CSSPACE:63 for a being Complex for X being ComplexUnitarySpace for seq1, seq being sequence of X st seq1 is constant & seq = a * seq1 holds seq is constant proofend; theorem :: CSSPACE:64 for X being ComplexUnitarySpace for seq1, seq2 being sequence of X holds seq1 - seq2 = seq1 + (- seq2) proofend; theorem :: CSSPACE:65 for X being ComplexUnitarySpace for seq being sequence of X holds seq = seq + (0. X) proofend; theorem :: CSSPACE:66 for a being Complex for X being ComplexUnitarySpace for seq1, seq2 being sequence of X holds a * (seq1 + seq2) = (a * seq1) + (a * seq2) proofend; theorem :: CSSPACE:67 for a, b being Complex for X being ComplexUnitarySpace for seq being sequence of X holds (a + b) * seq = (a * seq) + (b * seq) proofend; theorem :: CSSPACE:68 for a, b being Complex for X being ComplexUnitarySpace for seq being sequence of X holds (a * b) * seq = a * (b * seq) proofend; theorem :: CSSPACE:69 for X being ComplexUnitarySpace for seq being sequence of X holds 1r * seq = seq proofend; theorem :: CSSPACE:70 for X being ComplexUnitarySpace for seq being sequence of X holds (- 1r) * seq = - seq proofend; theorem :: CSSPACE:71 for X being ComplexUnitarySpace for x being Point of X for seq being sequence of X holds seq - x = seq + (- x) proofend; theorem :: CSSPACE:72 for X being ComplexUnitarySpace for seq1, seq2 being sequence of X holds seq1 - seq2 = - (seq2 - seq1) proofend; theorem :: CSSPACE:73 for X being ComplexUnitarySpace for seq being sequence of X holds seq = seq - (0. X) proofend; theorem :: CSSPACE:74 for X being ComplexUnitarySpace for seq being sequence of X holds seq = - (- seq) proofend; theorem :: CSSPACE:75 for X being ComplexUnitarySpace for seq1, seq2, seq3 being sequence of X holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3 proofend; theorem :: CSSPACE:76 for X being ComplexUnitarySpace for seq1, seq2, seq3 being sequence of X holds (seq1 + seq2) - seq3 = seq1 + (seq2 - seq3) proofend; theorem :: CSSPACE:77 for X being ComplexUnitarySpace for seq1, seq2, seq3 being sequence of X holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3 proofend; theorem :: CSSPACE:78 for a being Complex for X being ComplexUnitarySpace for seq1, seq2 being sequence of X holds a * (seq1 - seq2) = (a * seq1) - (a * seq2) proofend; begin definition func cl_scalar -> Function of [:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:],COMPLEX means :: CSSPACE:def 17 for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds it . (x,y) = Sum ((seq_id x) (#) ((seq_id y) *')); existence ex b1 being Function of [:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:],COMPLEX st for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds b1 . (x,y) = Sum ((seq_id x) (#) ((seq_id y) *')) proofend; uniqueness for b1, b2 being Function of [:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:],COMPLEX st ( for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds b1 . (x,y) = Sum ((seq_id x) (#) ((seq_id y) *')) ) & ( for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds b2 . (x,y) = Sum ((seq_id x) (#) ((seq_id y) *')) ) holds b1 = b2 proofend; end; :: deftheorem defines cl_scalar CSSPACE:def_17_:_ for b1 being Function of [:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:],COMPLEX holds ( b1 = cl_scalar iff for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds b1 . (x,y) = Sum ((seq_id x) (#) ((seq_id y) *')) ); registration cluster CUNITSTR(# the_set_of_l2ComplexSequences,(Zero_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),cl_scalar #) -> non empty ; coherence not CUNITSTR(# the_set_of_l2ComplexSequences,(Zero_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),cl_scalar #) is empty by Def11; end; definition func Complex_l2_Space -> non empty CUNITSTR equals :: CSSPACE:def 18 CUNITSTR(# the_set_of_l2ComplexSequences,(Zero_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),cl_scalar #); correctness coherence CUNITSTR(# the_set_of_l2ComplexSequences,(Zero_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),cl_scalar #) is non empty CUNITSTR ; ; end; :: deftheorem defines Complex_l2_Space CSSPACE:def_18_:_ Complex_l2_Space = CUNITSTR(# the_set_of_l2ComplexSequences,(Zero_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),cl_scalar #); theorem Th79: :: CSSPACE:79 for l being CLSStruct st CLSStruct(# the carrier of l, the ZeroF of l, the addF of l, the Mult of l #) is ComplexLinearSpace holds l is ComplexLinearSpace proofend; theorem :: CSSPACE:80 for seq being Complex_Sequence st ( for n being Element of NAT holds seq . n = 0c ) holds ( seq is summable & Sum seq = 0c ) proofend; registration cluster Complex_l2_Space -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ; coherence ( Complex_l2_Space is Abelian & Complex_l2_Space is add-associative & Complex_l2_Space is right_zeroed & Complex_l2_Space is right_complementable & Complex_l2_Space is vector-distributive & Complex_l2_Space is scalar-distributive & Complex_l2_Space is scalar-associative & Complex_l2_Space is scalar-unital ) by Th14, Th79; end;