:: CSSPACE semantic presentation 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 ) proof defpred S1[ set ] means $1 is Complex_Sequence; consider IT being set such that A1: for x being set holds ( x in IT iff ( x in Funcs (NAT,COMPLEX) & S1[x] ) ) from XBOOLE_0:sch_1(); not IT is empty proof set zeroseq = the Complex_Sequence; the Complex_Sequence in Funcs (NAT,COMPLEX) by FUNCT_2:8; hence not IT is empty by A1; ::_thesis: verum end; then reconsider IT = IT as non empty set ; take IT ; ::_thesis: for x being set holds ( x in IT iff x is Complex_Sequence ) for x being set st x is Complex_Sequence holds x in IT proof let x be set ; ::_thesis: ( x is Complex_Sequence implies x in IT ) assume A2: x is Complex_Sequence ; ::_thesis: x in IT then x in Funcs (NAT,COMPLEX) by FUNCT_2:8; hence x in IT by A1, A2; ::_thesis: verum end; hence for x being set holds ( x in IT iff x is Complex_Sequence ) by A1; ::_thesis: verum end; 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 proof let X1, X2 be non empty set ; ::_thesis: ( ( for x being set holds ( x in X1 iff x is Complex_Sequence ) ) & ( for x being set holds ( x in X2 iff x is Complex_Sequence ) ) implies X1 = X2 ) assume that A3: for x being set holds ( x in X1 iff x is Complex_Sequence ) and A4: for x being set holds ( x in X2 iff x is Complex_Sequence ) ; ::_thesis: X1 = X2 A5: X2 c= X1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X2 or x in X1 ) assume x in X2 ; ::_thesis: x in X1 then x is Complex_Sequence by A4; hence x in X1 by A3; ::_thesis: verum end; X1 c= X2 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X1 or x in X2 ) assume x in X1 ; ::_thesis: x in X2 then x is Complex_Sequence by A3; hence x in X2 by A4; ::_thesis: verum end; hence X1 = X2 by A5, XBOOLE_0:def_10; ::_thesis: verum end; 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) proof defpred S1[ Element of the_set_of_ComplexSequences , Element of the_set_of_ComplexSequences , Element of the_set_of_ComplexSequences ] means $3 = (seq_id $1) + (seq_id $2); A1: for x, y being Element of the_set_of_ComplexSequences ex z being Element of the_set_of_ComplexSequences st S1[x,y,z] proof let x, y be Element of the_set_of_ComplexSequences ; ::_thesis: ex z being Element of the_set_of_ComplexSequences st S1[x,y,z] (seq_id x) + (seq_id y) is Element of the_set_of_ComplexSequences by Def1; hence ex z being Element of the_set_of_ComplexSequences st S1[x,y,z] ; ::_thesis: verum end; ex ADD being BinOp of the_set_of_ComplexSequences st for a, b being Element of the_set_of_ComplexSequences holds S1[a,b,ADD . (a,b)] from BINOP_1:sch_3(A1); then consider ADD being BinOp of the_set_of_ComplexSequences such that A2: for a, b being Element of the_set_of_ComplexSequences holds ADD . (a,b) = (seq_id a) + (seq_id b) ; thus 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) by A2; ::_thesis: verum end; 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 proof deffunc H1( Element of the_set_of_ComplexSequences , Element of the_set_of_ComplexSequences ) -> Element of bool [:NAT,COMPLEX:] = (seq_id $1) + (seq_id $2); for o1, o2 being BinOp of the_set_of_ComplexSequences st ( for a, b being Element of the_set_of_ComplexSequences holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of the_set_of_ComplexSequences holds o2 . (a,b) = H1(a,b) ) holds o1 = o2 from BINOP_2:sch_2(); hence 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 ; ::_thesis: verum end; 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) proof deffunc H1( set , set ) -> Element of bool [:NAT,COMPLEX:] = (C_id $1) (#) (seq_id $2); A1: for r, x being set st r in COMPLEX & x in the_set_of_ComplexSequences holds H1(r,x) in the_set_of_ComplexSequences by Def1; consider f being Function of [:COMPLEX,the_set_of_ComplexSequences:],the_set_of_ComplexSequences such that A2: for r, x being set st r in COMPLEX & x in the_set_of_ComplexSequences holds f . (r,x) = H1(r,x) from BINOP_1:sch_2(A1); take f ; ::_thesis: for z, x being set st z is Complex & x in the_set_of_ComplexSequences holds f . (z,x) = (C_id z) (#) (seq_id x) let r, x be set ; ::_thesis: ( r is Complex & x in the_set_of_ComplexSequences implies f . (r,x) = (C_id r) (#) (seq_id x) ) assume r is Complex ; ::_thesis: ( not x in the_set_of_ComplexSequences or f . (r,x) = (C_id r) (#) (seq_id x) ) then r in COMPLEX by XCMPLX_0:def_2; hence ( not x in the_set_of_ComplexSequences or f . (r,x) = (C_id r) (#) (seq_id x) ) by A2; ::_thesis: verum end; 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 proof let mult1, mult2 be Function of [:COMPLEX,the_set_of_ComplexSequences:],the_set_of_ComplexSequences; ::_thesis: ( ( for z, x being set st z is Complex & x in the_set_of_ComplexSequences holds mult1 . (z,x) = (C_id z) (#) (seq_id x) ) & ( for z, x being set st z is Complex & x in the_set_of_ComplexSequences holds mult2 . (z,x) = (C_id z) (#) (seq_id x) ) implies mult1 = mult2 ) assume that A3: for z, x being set st z is Complex & x in the_set_of_ComplexSequences holds mult1 . (z,x) = (C_id z) (#) (seq_id x) and A4: for z, x being set st z is Complex & x in the_set_of_ComplexSequences holds mult2 . (z,x) = (C_id z) (#) (seq_id x) ; ::_thesis: mult1 = mult2 for z being Element of COMPLEX for x being Element of the_set_of_ComplexSequences holds mult1 . (z,x) = mult2 . (z,x) proof let z be Element of COMPLEX ; ::_thesis: for x being Element of the_set_of_ComplexSequences holds mult1 . (z,x) = mult2 . (z,x) let x be Element of the_set_of_ComplexSequences ; ::_thesis: mult1 . (z,x) = mult2 . (z,x) thus mult1 . (z,x) = (C_id z) (#) (seq_id x) by A3 .= mult2 . (z,x) by A4 ; ::_thesis: verum end; hence mult1 = mult2 by BINOP_1:2; ::_thesis: verum end; 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 proof reconsider zeroseq = NAT --> 0c as Complex_Sequence ; A1: for n being Element of NAT holds zeroseq . n = 0c by FUNCOP_1:7; A2: zeroseq in the_set_of_ComplexSequences by Def1; then seq_id zeroseq = zeroseq by Def2; hence ex b1 being Element of the_set_of_ComplexSequences st for n being Element of NAT holds (seq_id b1) . n = 0c by A1, A2; ::_thesis: verum end; 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 proof let x, y be Element of the_set_of_ComplexSequences ; ::_thesis: ( ( for n being Element of NAT holds (seq_id x) . n = 0c ) & ( for n being Element of NAT holds (seq_id y) . n = 0c ) implies x = y ) assume that A3: for n being Element of NAT holds (seq_id x) . n = 0c and A4: for n being Element of NAT holds (seq_id y) . n = 0c ; ::_thesis: x = y A5: for s being Element of NAT holds (seq_id x) . s = (seq_id y) . s proof let s be Element of NAT ; ::_thesis: (seq_id x) . s = (seq_id y) . s (seq_id y) . s = 0c by A4; hence (seq_id x) . s = (seq_id y) . s by A3; ::_thesis: verum end; x = seq_id x by Def2 .= seq_id y by A5, FUNCT_2:63 ; hence x = y by Def2; ::_thesis: verum end; 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 proof let x be Complex_Sequence; ::_thesis: seq_id x = x x in the_set_of_ComplexSequences by Def1; hence seq_id x = x by Def2; ::_thesis: verum end; 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) proof let z be Complex; ::_thesis: for v being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) holds z * v = z (#) (seq_id v) let v be VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #); ::_thesis: z * v = z (#) (seq_id v) thus z * v = l_mult . (z,v) .= (C_id z) (#) (seq_id v) by Def5 .= z (#) (seq_id v) by Def3 ; ::_thesis: verum end; 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 proof let v, w be VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #); :: according to RLVECT_1:def_2 ::_thesis: v + w = w + v v + w = (seq_id v) + (seq_id w) by Def4; hence v + w = w + v by Def4; ::_thesis: verum end; 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) proof let u, v, w be VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #); ::_thesis: (u + v) + w = u + (v + w) (u + v) + w = (seq_id (u + v)) + (seq_id w) by Def4 .= (seq_id ((seq_id u) + (seq_id v))) + (seq_id w) by Def4 .= ((seq_id u) + (seq_id v)) + (seq_id w) by Th1 .= (seq_id u) + ((seq_id v) + (seq_id w)) by COMSEQ_1:7 .= (seq_id u) + (seq_id ((seq_id v) + (seq_id w))) by Th1 .= (seq_id u) + (seq_id (v + w)) by Def4 ; hence (u + v) + w = u + (v + w) by Def4; ::_thesis: verum end; 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 proof set V = CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #); let v be VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #); ::_thesis: v + (0. CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #)) = v A1: for s being Element of NAT holds ((seq_id v) + (seq_id CZeroseq)) . s = (seq_id v) . s proof let s be Element of NAT ; ::_thesis: ((seq_id v) + (seq_id CZeroseq)) . s = (seq_id v) . s ((seq_id v) + (seq_id CZeroseq)) . s = ((seq_id v) . s) + ((seq_id CZeroseq) . s) by VALUED_1:1 .= ((seq_id v) . s) + 0c by Def6 ; hence ((seq_id v) + (seq_id CZeroseq)) . s = (seq_id v) . s ; ::_thesis: verum end; v + (0. CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #)) = (seq_id v) + (seq_id CZeroseq) by Def4; hence v + (0. CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #)) = seq_id v by A1, FUNCT_2:63 .= v by Def2 ; ::_thesis: verum end; 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 #) proof set V = CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #); let v be VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #); ::_thesis: 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 #) reconsider w = - (seq_id v) as VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) by Def1; for s being Element of NAT holds ((seq_id v) + (- (seq_id v))) . s = (seq_id CZeroseq) . s proof let s be Element of NAT ; ::_thesis: ((seq_id v) + (- (seq_id v))) . s = (seq_id CZeroseq) . s ((seq_id v) + (- (seq_id v))) . s = ((seq_id v) . s) + ((- (seq_id v)) . s) by VALUED_1:1 .= ((seq_id v) . s) + (- ((seq_id v) . s)) by VALUED_1:8 .= (seq_id CZeroseq) . s by Def6 ; hence ((seq_id v) + (- (seq_id v))) . s = (seq_id CZeroseq) . s ; ::_thesis: verum end; then A1: (seq_id v) + (- (seq_id v)) = seq_id CZeroseq by FUNCT_2:63 .= CZeroseq by Def2 ; v + w = (seq_id v) + (seq_id w) by Def4 .= (seq_id v) + (- (seq_id v)) by Th1 ; hence 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 #) by A1; ::_thesis: verum end; 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) proof let z be Complex; ::_thesis: for v, w being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) holds z * (v + w) = (z * v) + (z * w) let v, w be VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #); ::_thesis: z * (v + w) = (z * v) + (z * w) A1: z in COMPLEX by XCMPLX_0:def_2; A2: z * (v + w) = z (#) (seq_id (v + w)) by Th3 .= z (#) (seq_id ((seq_id v) + (seq_id w))) by Def4 .= z (#) ((seq_id v) + (seq_id w)) by Th1 .= (z (#) (seq_id v)) + (z (#) (seq_id w)) by A1, COMSEQ_1:16 ; (z * v) + (z * w) = (seq_id (z * v)) + (seq_id (z * w)) by Def4 .= (seq_id (z (#) (seq_id v))) + (seq_id (z * w)) by Th3 .= (seq_id (z (#) (seq_id v))) + (seq_id (z (#) (seq_id w))) by Th3 .= (z (#) (seq_id v)) + (seq_id (z (#) (seq_id w))) by Th1 .= (z (#) (seq_id v)) + (z (#) (seq_id w)) by Th1 ; hence z * (v + w) = (z * v) + (z * w) by A2; ::_thesis: verum end; 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) proof let z1, z2 be Complex; ::_thesis: for v being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) holds (z1 + z2) * v = (z1 * v) + (z2 * v) let v be VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #); ::_thesis: (z1 + z2) * v = (z1 * v) + (z2 * v) for s being Element of NAT holds ((z1 + z2) (#) (seq_id v)) . s = ((z1 (#) (seq_id v)) + (z2 (#) (seq_id v))) . s proof let s be Element of NAT ; ::_thesis: ((z1 + z2) (#) (seq_id v)) . s = ((z1 (#) (seq_id v)) + (z2 (#) (seq_id v))) . s ((z1 + z2) (#) (seq_id v)) . s = (z1 + z2) * ((seq_id v) . s) by VALUED_1:6 .= (z1 * ((seq_id v) . s)) + (z2 * ((seq_id v) . s)) .= ((z1 (#) (seq_id v)) . s) + (z2 * ((seq_id v) . s)) by VALUED_1:6 .= ((z1 (#) (seq_id v)) . s) + ((z2 (#) (seq_id v)) . s) by VALUED_1:6 ; hence ((z1 + z2) (#) (seq_id v)) . s = ((z1 (#) (seq_id v)) + (z2 (#) (seq_id v))) . s by VALUED_1:1; ::_thesis: verum end; then A1: (z1 + z2) (#) (seq_id v) = (z1 (#) (seq_id v)) + (z2 (#) (seq_id v)) by FUNCT_2:63; (z1 * v) + (z2 * v) = (seq_id (z1 * v)) + (seq_id (z2 * v)) by Def4 .= (seq_id (z1 (#) (seq_id v))) + (seq_id (z2 * v)) by Th3 .= (seq_id (z1 (#) (seq_id v))) + (seq_id (z2 (#) (seq_id v))) by Th3 .= (z1 (#) (seq_id v)) + (seq_id (z2 (#) (seq_id v))) by Th1 .= (z1 (#) (seq_id v)) + (z2 (#) (seq_id v)) by Th1 ; hence (z1 + z2) * v = (z1 * v) + (z2 * v) by A1, Th3; ::_thesis: verum end; 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) proof let z1, z2 be Complex; ::_thesis: for v being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) holds (z1 * z2) * v = z1 * (z2 * v) A1: ( z1 in COMPLEX & z2 in COMPLEX ) by XCMPLX_0:def_2; let v be VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #); ::_thesis: (z1 * z2) * v = z1 * (z2 * v) (z1 * z2) * v = (z1 * z2) (#) (seq_id v) by Th3 .= z1 (#) (z2 (#) (seq_id v)) by A1, COMSEQ_1:17 .= z1 (#) (seq_id (z2 (#) (seq_id v))) by Th1 .= z1 (#) (seq_id (z2 * v)) by Th3 ; hence (z1 * z2) * v = z1 * (z2 * v) by Th3; ::_thesis: verum end; theorem Th10: :: CSSPACE:10 for v being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) holds 1r * v = v proof let v be VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #); ::_thesis: 1r * v = v 1r * v = 1r (#) (seq_id v) by Th3 .= seq_id v by COMSEQ_1:21 ; hence 1r * v = v by Def2; ::_thesis: verum end; 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 ) proof set L = Linear_Space_of_ComplexSequences ; thus Linear_Space_of_ComplexSequences is Abelian ; ::_thesis: ( 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 ) thus Linear_Space_of_ComplexSequences is add-associative ::_thesis: ( 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 ) proof let x be Element of Linear_Space_of_ComplexSequences; :: according to RLVECT_1:def_3 ::_thesis: for b1, b2 being Element of the carrier of Linear_Space_of_ComplexSequences holds (x + b1) + b2 = x + (b1 + b2) thus for b1, b2 being Element of the carrier of Linear_Space_of_ComplexSequences holds (x + b1) + b2 = x + (b1 + b2) by Th4; ::_thesis: verum end; thus Linear_Space_of_ComplexSequences is right_zeroed ::_thesis: ( 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 ) proof let x be Element of Linear_Space_of_ComplexSequences; :: according to RLVECT_1:def_4 ::_thesis: x + (0. Linear_Space_of_ComplexSequences) = x thus x + (0. Linear_Space_of_ComplexSequences) = x by Th5; ::_thesis: verum end; thus Linear_Space_of_ComplexSequences is right_complementable ::_thesis: ( 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 ) proof let x be Element of Linear_Space_of_ComplexSequences; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable consider y being Element of Linear_Space_of_ComplexSequences such that A1: x + y = 0. Linear_Space_of_ComplexSequences by Th6; take y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. Linear_Space_of_ComplexSequences thus x + y = 0. Linear_Space_of_ComplexSequences by A1; ::_thesis: verum end; thus ( ( for z being Complex for v, w being VECTOR of Linear_Space_of_ComplexSequences holds z * (v + w) = (z * v) + (z * w) ) & ( for z1, z2 being Complex for v being VECTOR of Linear_Space_of_ComplexSequences holds (z1 + z2) * v = (z1 * v) + (z2 * v) ) & ( for z1, z2 being Complex for v being VECTOR of Linear_Space_of_ComplexSequences holds (z1 * z2) * v = z1 * (z2 * v) ) & ( for v being VECTOR of Linear_Space_of_ComplexSequences holds 1r * v = v ) ) by Th7, Th8, Th9, Th10; :: according to CLVECT_1:def_2,CLVECT_1:def_3,CLVECT_1:def_4,CLVECT_1:def_5 ::_thesis: verum end; 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; proof A1: dom the addF of X = [: the carrier of X, the carrier of X:] by FUNCT_2:def_1; A2: for z being set st z in [:X1,X1:] holds ( the addF of X || X1) . z in X1 proof let z be set ; ::_thesis: ( z in [:X1,X1:] implies ( the addF of X || X1) . z in X1 ) assume A3: z in [:X1,X1:] ; ::_thesis: ( the addF of X || X1) . z in X1 consider r, x being set such that A4: r in X1 and A5: x in X1 and A6: z = [r,x] by A3, ZFMISC_1:def_2; reconsider y = x, r1 = r as VECTOR of X by A4, A5; [r,x] in dom ( the addF of X || X1) by A1, A3, A6, RELAT_1:62, ZFMISC_1:96; then ( the addF of X || X1) . z = r1 + y by A6, FUNCT_1:47; hence ( the addF of X || X1) . z in X1 by B1, A4, A5, CLVECT_1:def_7; ::_thesis: verum end; dom ( the addF of X || X1) = [:X1,X1:] by A1, RELAT_1:62, ZFMISC_1:96; hence the addF of X || X1 is BinOp of X1 by A2, FUNCT_2:3; ::_thesis: verum end; 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; proof A1: dom the Mult of X = [:COMPLEX, the carrier of X:] by FUNCT_2:def_1; A2: [:COMPLEX,X1:] c= [:COMPLEX, the carrier of X:] by ZFMISC_1:95; A3: for z being set st z in [:COMPLEX,X1:] holds ( the Mult of X | [:COMPLEX,X1:]) . z in X1 proof let z be set ; ::_thesis: ( z in [:COMPLEX,X1:] implies ( the Mult of X | [:COMPLEX,X1:]) . z in X1 ) assume A4: z in [:COMPLEX,X1:] ; ::_thesis: ( the Mult of X | [:COMPLEX,X1:]) . z in X1 consider r, x being set such that A5: r in COMPLEX and A6: x in X1 and A7: z = [r,x] by A4, ZFMISC_1:def_2; reconsider r = r as Complex by A5; reconsider y = x as VECTOR of X by A6; [r,x] in dom ( the Mult of X | [:COMPLEX,X1:]) by A2, A1, A4, A7, RELAT_1:62; then ( the Mult of X | [:COMPLEX,X1:]) . z = r * y by A7, FUNCT_1:47; hence ( the Mult of X | [:COMPLEX,X1:]) . z in X1 by B1, A6, CLVECT_1:def_7; ::_thesis: verum end; dom ( the Mult of X | [:COMPLEX,X1:]) = [:COMPLEX,X1:] by A2, A1, RELAT_1:62; hence the Mult of X | [:COMPLEX,X1:] is Function of [:COMPLEX,X1:],X1 by A3, FUNCT_2:3; ::_thesis: verum end; 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; proof set v = the Element of X1; the Element of X1 in X1 by A2; then reconsider v = the Element of X1 as Element of X ; v - v = 0. X by RLVECT_1:15; hence 0. X is Element of X1 by A1, A2, CLVECT_1:22; ::_thesis: verum end; 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 proof let V be ComplexLinearSpace; ::_thesis: 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 let V1 be Subset of V; ::_thesis: ( V1 is linearly-closed & not V1 is empty implies CLSStruct(# V1,(Zero_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)) #) is Subspace of V ) assume that A1: V1 is linearly-closed and A2: not V1 is empty ; ::_thesis: CLSStruct(# V1,(Zero_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)) #) is Subspace of V A3: Add_ (V1,V) = the addF of V || V1 by A1, Def8; A4: Mult_ (V1,V) = the Mult of V | [:COMPLEX,V1:] by A1, Def9; Zero_ (V1,V) = 0. V by A1, A2, Def10; hence CLSStruct(# V1,(Zero_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)) #) is Subspace of V by A2, A3, A4, CLVECT_1:43; ::_thesis: verum end; 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 ) ) ) ) proof defpred S1[ set ] means |.(seq_id $1).| (#) |.(seq_id $1).| is summable ; consider IT being set such that A1: for x being set holds ( x in IT iff ( x in the_set_of_ComplexSequences & S1[x] ) ) from XBOOLE_0:sch_1(); for x being set st x in IT holds x in the_set_of_ComplexSequences by A1; then A2: IT is Subset of the_set_of_ComplexSequences by TARSKI:def_3; |.(seq_id CZeroseq).| (#) |.(seq_id CZeroseq).| is absolutely_summable proof reconsider rseq = |.(seq_id CZeroseq).| (#) |.(seq_id CZeroseq).| as Real_Sequence ; now__::_thesis:_for_n_being_Element_of_NAT_holds_rseq_._n_=_0 let n be Element of NAT ; ::_thesis: rseq . n = 0 thus rseq . n = (|.(seq_id CZeroseq).| . n) * (|.(seq_id CZeroseq).| . n) by SEQ_1:8 .= (|.(seq_id CZeroseq).| . n) * |.((seq_id CZeroseq) . n).| by VALUED_1:18 .= (|.(seq_id CZeroseq).| . n) * 0 by Def6, COMPLEX1:44 .= 0 ; ::_thesis: verum end; hence |.(seq_id CZeroseq).| (#) |.(seq_id CZeroseq).| is absolutely_summable by COMSEQ_3:3; ::_thesis: verum end; then not IT is empty by A1; hence 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 ) ) ) ) by A1, A2; ::_thesis: verum end; 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 proof let X1, X2 be Subset of Linear_Space_of_ComplexSequences; ::_thesis: ( not X1 is empty & ( for x being set holds ( x in X1 iff ( x in the_set_of_ComplexSequences & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) ) & not X2 is empty & ( for x being set holds ( x in X2 iff ( x in the_set_of_ComplexSequences & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) ) implies X1 = X2 ) assume that not X1 is empty and A3: for x being set holds ( x in X1 iff ( x in the_set_of_ComplexSequences & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) and not X2 is empty and A4: for x being set holds ( x in X2 iff ( x in the_set_of_ComplexSequences & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) ; ::_thesis: X1 = X2 A5: X2 c= X1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X2 or x in X1 ) assume A6: x in X2 ; ::_thesis: x in X1 then |.(seq_id x).| (#) |.(seq_id x).| is summable by A4; hence x in X1 by A3, A6; ::_thesis: verum end; X1 c= X2 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X1 or x in X2 ) assume A7: x in X1 ; ::_thesis: x in X2 then |.(seq_id x).| (#) |.(seq_id x).| is summable by A3; hence x in X2 by A4, A7; ::_thesis: verum end; hence X1 = X2 by A5, XBOOLE_0:def_10; ::_thesis: verum end; 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 ) proof set W = the_set_of_l2ComplexSequences ; A1: for v, u being VECTOR of Linear_Space_of_ComplexSequences st v in the_set_of_l2ComplexSequences & u in the_set_of_l2ComplexSequences holds v + u in the_set_of_l2ComplexSequences proof let v, u be VECTOR of Linear_Space_of_ComplexSequences; ::_thesis: ( v in the_set_of_l2ComplexSequences & u in the_set_of_l2ComplexSequences implies v + u in the_set_of_l2ComplexSequences ) assume that A2: v in the_set_of_l2ComplexSequences and A3: u in the_set_of_l2ComplexSequences ; ::_thesis: v + u in the_set_of_l2ComplexSequences |.(seq_id (v + u)).| (#) |.(seq_id (v + u)).| is summable proof set r = |.(seq_id (v + u)).| (#) |.(seq_id (v + u)).|; set q = |.(seq_id u).| (#) |.(seq_id u).|; set p = |.(seq_id v).| (#) |.(seq_id v).|; A4: for n being Element of NAT holds 0 <= (|.(seq_id (v + u)).| (#) |.(seq_id (v + u)).|) . n proof let n be Element of NAT ; ::_thesis: 0 <= (|.(seq_id (v + u)).| (#) |.(seq_id (v + u)).|) . n (|.(seq_id (v + u)).| (#) |.(seq_id (v + u)).|) . n = (|.(seq_id (v + u)).| . n) * (|.(seq_id (v + u)).| . n) by SEQ_1:8; hence 0 <= (|.(seq_id (v + u)).| (#) |.(seq_id (v + u)).|) . n by XREAL_1:63; ::_thesis: verum end; A5: for n being Element of NAT holds (|.(seq_id (v + u)).| (#) |.(seq_id (v + u)).|) . n <= ((2 (#) (|.(seq_id v).| (#) |.(seq_id v).|)) + (2 (#) (|.(seq_id u).| (#) |.(seq_id u).|))) . n proof set t = |.(seq_id u).|; set s = |.(seq_id v).|; let n be Element of NAT ; ::_thesis: (|.(seq_id (v + u)).| (#) |.(seq_id (v + u)).|) . n <= ((2 (#) (|.(seq_id v).| (#) |.(seq_id v).|)) + (2 (#) (|.(seq_id u).| (#) |.(seq_id u).|))) . n reconsider sn = |.(seq_id v).| . n, tn = |.(seq_id u).| . n as Real ; A6: (|.(seq_id (v + u)).| (#) |.(seq_id (v + u)).|) . n = (|.(seq_id (v + u)).| . n) ^2 by SEQ_1:8; ((2 (#) (|.(seq_id v).| (#) |.(seq_id v).|)) + (2 (#) (|.(seq_id u).| (#) |.(seq_id u).|))) . n = ((2 (#) (|.(seq_id v).| (#) |.(seq_id v).|)) . n) + ((2 (#) (|.(seq_id u).| (#) |.(seq_id u).|)) . n) by SEQ_1:7 .= (2 * ((|.(seq_id v).| (#) |.(seq_id v).|) . n)) + ((2 (#) (|.(seq_id u).| (#) |.(seq_id u).|)) . n) by SEQ_1:9 .= (2 * ((|.(seq_id v).| (#) |.(seq_id v).|) . n)) + (2 * ((|.(seq_id u).| (#) |.(seq_id u).|) . n)) by SEQ_1:9 .= (2 * ((|.(seq_id v).| . n) * (|.(seq_id v).| . n))) + (2 * ((|.(seq_id u).| (#) |.(seq_id u).|) . n)) by SEQ_1:8 .= (2 * (sn ^2)) + (2 * (tn ^2)) by SEQ_1:8 ; then A7: (((2 (#) (|.(seq_id v).| (#) |.(seq_id v).|)) + (2 (#) (|.(seq_id u).| (#) |.(seq_id u).|))) . n) - (((sn ^2) + ((2 * sn) * tn)) + (tn ^2)) = (sn - tn) ^2 ; A8: seq_id (v + u) = seq_id ((seq_id v) + (seq_id u)) by Def4 .= (seq_id v) + (seq_id u) by Th1 ; |.(seq_id (v + u)).| . n = |.((seq_id (v + u)) . n).| by VALUED_1:18 .= |.(((seq_id v) . n) + ((seq_id u) . n)).| by A8, VALUED_1:1 ; then |.(seq_id (v + u)).| . n <= |.((seq_id v) . n).| + |.((seq_id u) . n).| by COMPLEX1:56; then |.(seq_id (v + u)).| . n <= (|.(seq_id v).| . n) + |.((seq_id u) . n).| by VALUED_1:18; then A9: |.(seq_id (v + u)).| . n <= (|.(seq_id v).| . n) + (|.(seq_id u).| . n) by VALUED_1:18; 0 <= (sn - tn) ^2 by XREAL_1:63; then A10: 0 + (((sn ^2) + ((2 * sn) * tn)) + (tn ^2)) <= ((2 (#) (|.(seq_id v).| (#) |.(seq_id v).|)) + (2 (#) (|.(seq_id u).| (#) |.(seq_id u).|))) . n by A7, XREAL_1:19; 0 <= |.((seq_id (v + u)) . n).| by COMPLEX1:46; then 0 <= |.(seq_id (v + u)).| . n by VALUED_1:18; then (|.(seq_id (v + u)).| . n) ^2 <= ((|.(seq_id v).| . n) + (|.(seq_id u).| . n)) ^2 by A9, SQUARE_1:15; hence (|.(seq_id (v + u)).| (#) |.(seq_id (v + u)).|) . n <= ((2 (#) (|.(seq_id v).| (#) |.(seq_id v).|)) + (2 (#) (|.(seq_id u).| (#) |.(seq_id u).|))) . n by A6, A10, XXREAL_0:2; ::_thesis: verum end; |.(seq_id u).| (#) |.(seq_id u).| is summable by A3, Def11; then A11: 2 (#) (|.(seq_id u).| (#) |.(seq_id u).|) is summable by SERIES_1:10; |.(seq_id v).| (#) |.(seq_id v).| is summable by A2, Def11; then 2 (#) (|.(seq_id v).| (#) |.(seq_id v).|) is summable by SERIES_1:10; then (2 (#) (|.(seq_id v).| (#) |.(seq_id v).|)) + (2 (#) (|.(seq_id u).| (#) |.(seq_id u).|)) is summable by A11, SERIES_1:7; hence |.(seq_id (v + u)).| (#) |.(seq_id (v + u)).| is summable by A4, A5, SERIES_1:20; ::_thesis: verum end; hence v + u in the_set_of_l2ComplexSequences by Def11; ::_thesis: verum end; for z being Complex for v being VECTOR of Linear_Space_of_ComplexSequences st v in the_set_of_l2ComplexSequences holds z * v in the_set_of_l2ComplexSequences proof let z be Complex; ::_thesis: for v being VECTOR of Linear_Space_of_ComplexSequences st v in the_set_of_l2ComplexSequences holds z * v in the_set_of_l2ComplexSequences let v be VECTOR of Linear_Space_of_ComplexSequences; ::_thesis: ( v in the_set_of_l2ComplexSequences implies z * v in the_set_of_l2ComplexSequences ) assume v in the_set_of_l2ComplexSequences ; ::_thesis: z * v in the_set_of_l2ComplexSequences then A12: |.(seq_id v).| (#) |.(seq_id v).| is summable by Def11; A13: z in COMPLEX by XCMPLX_0:def_2; seq_id (z * v) = seq_id (z (#) (seq_id v)) by Th3 .= z (#) (seq_id v) by Th1 ; then |.(seq_id (z * v)).| = |.z.| (#) |.(seq_id v).| by A13, COMSEQ_1:50; then |.(seq_id (z * v)).| (#) |.(seq_id (z * v)).| = |.z.| (#) ((|.z.| (#) |.(seq_id v).|) (#) |.(seq_id v).|) by SEQ_1:18 .= |.z.| (#) (|.z.| (#) (|.(seq_id v).| (#) |.(seq_id v).|)) by SEQ_1:18 .= (|.z.| * |.z.|) (#) (|.(seq_id v).| (#) |.(seq_id v).|) by SEQ_1:23 ; then |.(seq_id (z * v)).| (#) |.(seq_id (z * v)).| is summable by A12, SERIES_1:10; hence z * v in the_set_of_l2ComplexSequences by Def11; ::_thesis: verum end; hence ( the_set_of_l2ComplexSequences is linearly-closed & not the_set_of_l2ComplexSequences is empty ) by A1, Def11, CLVECT_1:def_7; ::_thesis: verum end; 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 ) proof set D = the non empty set ; set Z = the Element of the non empty set ; set a = the BinOp of the non empty set ; set m = the Function of [:COMPLEX, the non empty set :], the non empty set ; set s = the Function of [: the non empty set , the non empty set :],COMPLEX; take CUNITSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:COMPLEX, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :],COMPLEX #) ; ::_thesis: ( not CUNITSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:COMPLEX, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :],COMPLEX #) is empty & CUNITSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:COMPLEX, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :],COMPLEX #) is strict ) thus not the carrier of CUNITSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:COMPLEX, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :],COMPLEX #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: CUNITSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:COMPLEX, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :],COMPLEX #) is strict thus CUNITSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:COMPLEX, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :],COMPLEX #) is strict ; ::_thesis: verum end; 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]) *' proof let u, v be VECTOR of ((0). the ComplexLinearSpace); ::_thesis: nilfunc . [u,v] = (nilfunc . [v,u]) *' A1: v = 0. the ComplexLinearSpace by Lm1, TARSKI:def_1; u = 0. the ComplexLinearSpace by Lm1, TARSKI:def_1; hence nilfunc . [u,v] = (nilfunc . [v,u]) *' by A1, Lm3, COMPLEX1:28; ::_thesis: verum end; Lm6: for u, v, w being VECTOR of ((0). the ComplexLinearSpace) holds nilfunc . [(u + v),w] = (nilfunc . [u,w]) + (nilfunc . [v,w]) proof let u, v, w be VECTOR of ((0). the ComplexLinearSpace); ::_thesis: nilfunc . [(u + v),w] = (nilfunc . [u,w]) + (nilfunc . [v,w]) A1: v = 0. the ComplexLinearSpace by Lm1, TARSKI:def_1; A2: w = 0. the ComplexLinearSpace by Lm1, TARSKI:def_1; u = 0. the ComplexLinearSpace by Lm1, TARSKI:def_1; hence nilfunc . [(u + v),w] = (nilfunc . [u,w]) + (nilfunc . [v,w]) by A1, A2, Lm1, Lm3, TARSKI:def_1; ::_thesis: verum end; Lm7: for u, v being VECTOR of ((0). the ComplexLinearSpace) for a being Complex holds nilfunc . [(a * u),v] = a * (nilfunc . [u,v]) proof let u, v be VECTOR of ((0). the ComplexLinearSpace); ::_thesis: for a being Complex holds nilfunc . [(a * u),v] = a * (nilfunc . [u,v]) let a be Complex; ::_thesis: nilfunc . [(a * u),v] = a * (nilfunc . [u,v]) A1: v = 0. the ComplexLinearSpace by Lm1, TARSKI:def_1; u = 0. the ComplexLinearSpace by Lm1, TARSKI:def_1; hence nilfunc . [(a * u),v] = a * (nilfunc . [u,v]) by A1, Lm1, Lm3, TARSKI:def_1; ::_thesis: verum end; 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 ) proof take 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: ( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is ComplexUnitarySpace-like & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is vector-distributive & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-distributive & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-associative & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-unital & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is Abelian & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is add-associative & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_zeroed & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_complementable & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is strict ) thus CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is ComplexUnitarySpace-like by Def13, Lm8; ::_thesis: ( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is vector-distributive & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-distributive & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-associative & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-unital & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is Abelian & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is add-associative & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_zeroed & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_complementable & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is strict ) thus ( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is vector-distributive & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-distributive & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-associative & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-unital ) ::_thesis: ( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is Abelian & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is add-associative & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_zeroed & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_complementable & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is strict ) proof thus for a being Complex for v, w being VECTOR 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 #) holds a * (v + w) = (a * v) + (a * w) :: according to CLVECT_1:def_2 ::_thesis: ( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-distributive & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-associative & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-unital ) proof let a be Complex; ::_thesis: for v, w being VECTOR 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 #) holds a * (v + w) = (a * v) + (a * w) let v, w be VECTOR 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: a * (v + w) = (a * v) + (a * w) reconsider v9 = v, w9 = w as VECTOR of ((0). the ComplexLinearSpace) ; thus a * (v + w) = a * (v9 + w9) .= (a * v9) + (a * w9) by CLVECT_1:def_2 .= (a * v) + (a * w) ; ::_thesis: verum end; thus for a, b being Complex for v being VECTOR 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 #) holds (a + b) * v = (a * v) + (b * v) :: according to CLVECT_1:def_3 ::_thesis: ( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-associative & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-unital ) proof let a, b be Complex; ::_thesis: for v being VECTOR 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 #) holds (a + b) * v = (a * v) + (b * v) let v be VECTOR 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: (a + b) * v = (a * v) + (b * v) reconsider v9 = v as VECTOR of ((0). the ComplexLinearSpace) ; thus (a + b) * v = (a + b) * v9 .= (a * v9) + (b * v9) by CLVECT_1:def_3 .= (a * v) + (b * v) ; ::_thesis: verum end; thus for a, b being Complex for v being VECTOR 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 #) holds (a * b) * v = a * (b * v) :: according to CLVECT_1:def_4 ::_thesis: CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-unital proof let a, b be Complex; ::_thesis: for v being VECTOR 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 #) holds (a * b) * v = a * (b * v) let v be VECTOR 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: (a * b) * v = a * (b * v) reconsider v9 = v as VECTOR of ((0). the ComplexLinearSpace) ; thus (a * b) * v = (a * b) * v9 .= a * (b * v9) by CLVECT_1:def_4 .= a * (b * v) ; ::_thesis: verum end; let v be VECTOR 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 #); :: according to CLVECT_1:def_5 ::_thesis: 1r * v = v reconsider v9 = v as VECTOR of ((0). the ComplexLinearSpace) ; thus 1r * v = 1r * v9 .= v by CLVECT_1:def_5 ; ::_thesis: verum end; A1: for x, y being VECTOR 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 x9, y9 being VECTOR of ((0). the ComplexLinearSpace) st x = x9 & y = y9 holds ( x + y = x9 + y9 & ( for a being Complex holds a * x = a * x9 ) ) ; thus for v, w being VECTOR 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 #) holds v + w = w + v :: according to RLVECT_1:def_2 ::_thesis: ( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is add-associative & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_zeroed & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_complementable & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is strict ) proof let v, w be VECTOR 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: v + w = w + v reconsider v9 = v, w9 = w as VECTOR of ((0). the ComplexLinearSpace) ; thus v + w = w9 + v9 by A1 .= w + v ; ::_thesis: verum end; thus for u, v, w being VECTOR 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 #) holds (u + v) + w = u + (v + w) :: according to RLVECT_1:def_3 ::_thesis: ( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_zeroed & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_complementable & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is strict ) proof let u, v, w be VECTOR 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: (u + v) + w = u + (v + w) reconsider u9 = u, v9 = v, w9 = w as VECTOR of ((0). the ComplexLinearSpace) ; thus (u + v) + w = (u9 + v9) + w9 .= u9 + (v9 + w9) by RLVECT_1:def_3 .= u + (v + w) ; ::_thesis: verum end; thus for v being VECTOR 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 #) holds v + (0. CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)) = v :: according to RLVECT_1:def_4 ::_thesis: ( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_complementable & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is strict ) proof let v be VECTOR 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: v + (0. CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)) = v reconsider v9 = v as VECTOR of ((0). the ComplexLinearSpace) ; thus v + (0. CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)) = v9 + (0. ((0). the ComplexLinearSpace)) .= v by RLVECT_1:4 ; ::_thesis: verum end; thus CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_complementable ::_thesis: CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is strict proof let v be VECTOR 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 #); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable reconsider v9 = v as VECTOR of ((0). the ComplexLinearSpace) ; consider w9 being VECTOR of ((0). the ComplexLinearSpace) such that A2: v9 + w9 = 0. ((0). the ComplexLinearSpace) by ALGSTR_0:def_11; reconsider w = w9 as VECTOR 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 #) ; take w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) thus v + w = 0. 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 A2; ::_thesis: verum end; thus CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is strict ; ::_thesis: verum end; 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) proof let X be ComplexUnitarySpace; ::_thesis: for x, y, z being Point of X holds x .|. (y + z) = (x .|. y) + (x .|. z) let x, y, z be Point of X; ::_thesis: x .|. (y + z) = (x .|. y) + (x .|. z) thus x .|. (y + z) = ((y + z) .|. x) *' by Def13 .= ((y .|. x) + (z .|. x)) *' by Def13 .= ((y .|. x) *') + ((z .|. x) *') by COMPLEX1:32 .= (x .|. y) + ((z .|. x) *') by Def13 .= (x .|. y) + (x .|. z) by Def13 ; ::_thesis: verum end; 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) proof let a be Complex; ::_thesis: for X being ComplexUnitarySpace for x, y being Point of X holds x .|. (a * y) = (a *') * (x .|. y) let X be ComplexUnitarySpace; ::_thesis: for x, y being Point of X holds x .|. (a * y) = (a *') * (x .|. y) let x, y be Point of X; ::_thesis: x .|. (a * y) = (a *') * (x .|. y) thus x .|. (a * y) = ((a * y) .|. x) *' by Def13 .= (a * (y .|. x)) *' by Def13 .= (a *') * ((y .|. x) *') by COMPLEX1:35 .= (a *') * (x .|. y) by Def13 ; ::_thesis: verum end; 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) proof let a be Complex; ::_thesis: for X being ComplexUnitarySpace for x, y being Point of X holds (a * x) .|. y = x .|. ((a *') * y) let X be ComplexUnitarySpace; ::_thesis: for x, y being Point of X holds (a * x) .|. y = x .|. ((a *') * y) let x, y be Point of X; ::_thesis: (a * x) .|. y = x .|. ((a *') * y) (a * x) .|. y = a * (x .|. y) by Def13 .= ((a *') *') * ((y .|. x) *') by Def13 .= ((a *') * (y .|. x)) *' by COMPLEX1:35 .= (((a *') * y) .|. x) *' by Def13 ; hence (a * x) .|. y = x .|. ((a *') * y) by Def13; ::_thesis: verum end; 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)) proof let a, b be Complex; ::_thesis: for X being ComplexUnitarySpace for x, y, z being Point of X holds ((a * x) + (b * y)) .|. z = (a * (x .|. z)) + (b * (y .|. z)) let X be ComplexUnitarySpace; ::_thesis: for x, y, z being Point of X holds ((a * x) + (b * y)) .|. z = (a * (x .|. z)) + (b * (y .|. z)) let x, y, z be Point of X; ::_thesis: ((a * x) + (b * y)) .|. z = (a * (x .|. z)) + (b * (y .|. z)) ((a * x) + (b * y)) .|. z = ((a * x) .|. z) + ((b * y) .|. z) by Def13 .= (a * (x .|. z)) + ((b * y) .|. z) by Def13 ; hence ((a * x) + (b * y)) .|. z = (a * (x .|. z)) + (b * (y .|. z)) by Def13; ::_thesis: verum end; 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)) proof let a, b be Complex; ::_thesis: for X being ComplexUnitarySpace for x, y, z being Point of X holds x .|. ((a * y) + (b * z)) = ((a *') * (x .|. y)) + ((b *') * (x .|. z)) let X be ComplexUnitarySpace; ::_thesis: for x, y, z being Point of X holds x .|. ((a * y) + (b * z)) = ((a *') * (x .|. y)) + ((b *') * (x .|. z)) let x, y, z be Point of X; ::_thesis: x .|. ((a * y) + (b * z)) = ((a *') * (x .|. y)) + ((b *') * (x .|. z)) x .|. ((a * y) + (b * z)) = (((a * y) + (b * z)) .|. x) *' by Def13 .= ((a * (y .|. x)) + (b * (z .|. x))) *' by Th20 .= ((a * (y .|. x)) *') + ((b * (z .|. x)) *') by COMPLEX1:32 .= ((a *') * ((y .|. x) *')) + ((b * (z .|. x)) *') by COMPLEX1:35 .= ((a *') * ((y .|. x) *')) + ((b *') * ((z .|. x) *')) by COMPLEX1:35 .= ((a *') * (x .|. y)) + ((b *') * ((z .|. x) *')) by Def13 ; hence x .|. ((a * y) + (b * z)) = ((a *') * (x .|. y)) + ((b *') * (x .|. z)) by Def13; ::_thesis: verum end; theorem Th22: :: CSSPACE:22 for X being ComplexUnitarySpace for x, y being Point of X holds (- x) .|. y = x .|. (- y) proof let X be ComplexUnitarySpace; ::_thesis: for x, y being Point of X holds (- x) .|. y = x .|. (- y) let x, y be Point of X; ::_thesis: (- x) .|. y = x .|. (- y) (- x) .|. y = ((- 1r) * x) .|. y by CLVECT_1:3 .= x .|. (((- 1r) *') * y) by Th19 .= x .|. ((- 1r) * y) by COMPLEX1:30, COMPLEX1:33 ; hence (- x) .|. y = x .|. (- y) by CLVECT_1:3; ::_thesis: verum end; theorem Th23: :: CSSPACE:23 for X being ComplexUnitarySpace for x, y being Point of X holds (- x) .|. y = - (x .|. y) proof let X be ComplexUnitarySpace; ::_thesis: for x, y being Point of X holds (- x) .|. y = - (x .|. y) let x, y be Point of X; ::_thesis: (- x) .|. y = - (x .|. y) (- x) .|. y = ((- 1r) * x) .|. y by CLVECT_1:3 .= (- 1) * (x .|. y) by Def13, COMPLEX1:def_4 ; hence (- x) .|. y = - (x .|. y) ; ::_thesis: verum end; theorem Th24: :: CSSPACE:24 for X being ComplexUnitarySpace for x, y being Point of X holds x .|. (- y) = - (x .|. y) proof let X be ComplexUnitarySpace; ::_thesis: for x, y being Point of X holds x .|. (- y) = - (x .|. y) let x, y be Point of X; ::_thesis: x .|. (- y) = - (x .|. y) x .|. (- y) = (- x) .|. y by Th22; hence x .|. (- y) = - (x .|. y) by Th23; ::_thesis: verum end; theorem Th25: :: CSSPACE:25 for X being ComplexUnitarySpace for x, y being Point of X holds (- x) .|. (- y) = x .|. y proof let X be ComplexUnitarySpace; ::_thesis: for x, y being Point of X holds (- x) .|. (- y) = x .|. y let x, y be Point of X; ::_thesis: (- x) .|. (- y) = x .|. y (- x) .|. (- y) = - (x .|. (- y)) by Th23 .= - (- (x .|. y)) by Th24 ; hence (- x) .|. (- y) = x .|. y ; ::_thesis: verum end; theorem Th26: :: CSSPACE:26 for X being ComplexUnitarySpace for x, y, z being Point of X holds (x - y) .|. z = (x .|. z) - (y .|. z) proof let X be ComplexUnitarySpace; ::_thesis: for x, y, z being Point of X holds (x - y) .|. z = (x .|. z) - (y .|. z) let x, y, z be Point of X; ::_thesis: (x - y) .|. z = (x .|. z) - (y .|. z) (x - y) .|. z = (x .|. z) + ((- y) .|. z) by Def13 .= (x .|. z) + (- (y .|. z)) by Th23 ; hence (x - y) .|. z = (x .|. z) - (y .|. z) ; ::_thesis: verum end; theorem Th27: :: CSSPACE:27 for X being ComplexUnitarySpace for x, y, z being Point of X holds x .|. (y - z) = (x .|. y) - (x .|. z) proof let X be ComplexUnitarySpace; ::_thesis: for x, y, z being Point of X holds x .|. (y - z) = (x .|. y) - (x .|. z) let x, y, z be Point of X; ::_thesis: x .|. (y - z) = (x .|. y) - (x .|. z) x .|. (y - z) = (x .|. y) + (x .|. (- z)) by Th17 .= (x .|. y) + (- (x .|. z)) by Th24 ; hence x .|. (y - z) = (x .|. y) - (x .|. z) ; ::_thesis: verum end; 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) proof let X be ComplexUnitarySpace; ::_thesis: for x, y, u, v being Point of X holds (x - y) .|. (u - v) = (((x .|. u) - (x .|. v)) - (y .|. u)) + (y .|. v) let x, y, u, v be Point of X; ::_thesis: (x - y) .|. (u - v) = (((x .|. u) - (x .|. v)) - (y .|. u)) + (y .|. v) (x - y) .|. (u - v) = (x .|. (u - v)) - (y .|. (u - v)) by Th26 .= ((x .|. u) - (x .|. v)) - (y .|. (u - v)) by Th27 .= ((x .|. u) - (x .|. v)) - ((y .|. u) - (y .|. v)) by Th27 ; hence (x - y) .|. (u - v) = (((x .|. u) - (x .|. v)) - (y .|. u)) + (y .|. v) ; ::_thesis: verum end; theorem Th29: :: CSSPACE:29 for X being ComplexUnitarySpace for x being Point of X holds (0. X) .|. x = 0 proof let X be ComplexUnitarySpace; ::_thesis: for x being Point of X holds (0. X) .|. x = 0 let x be Point of X; ::_thesis: (0. X) .|. x = 0 H1(X) .|. x = (x + (- x)) .|. x by RLVECT_1:5 .= (x .|. x) + ((- x) .|. x) by Def13 .= (x .|. x) + (- (x .|. x)) by Th23 ; hence (0. X) .|. x = 0 ; ::_thesis: verum end; theorem Th30: :: CSSPACE:30 for X being ComplexUnitarySpace for x being Point of X holds x .|. (0. X) = 0 proof let X be ComplexUnitarySpace; ::_thesis: for x being Point of X holds x .|. (0. X) = 0 let x be Point of X; ::_thesis: x .|. (0. X) = 0 x .|. (0. X) = ((0. X) .|. x) *' by Def13 .= 0c by Th29, COMPLEX1:28 ; hence x .|. (0. X) = 0 ; ::_thesis: verum end; 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) proof let X be ComplexUnitarySpace; ::_thesis: for x, y being Point of X holds (x + y) .|. (x + y) = (((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y) let x, y be Point of X; ::_thesis: (x + y) .|. (x + y) = (((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y) (x + y) .|. (x + y) = (x .|. (x + y)) + (y .|. (x + y)) by Def13 .= ((x .|. x) + (x .|. y)) + (y .|. (x + y)) by Th17 .= ((x .|. x) + (x .|. y)) + ((y .|. x) + (y .|. y)) by Th17 ; hence (x + y) .|. (x + y) = (((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y) ; ::_thesis: verum end; 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) proof let X be ComplexUnitarySpace; ::_thesis: for x, y being Point of X holds (x + y) .|. (x - y) = (((x .|. x) - (x .|. y)) + (y .|. x)) - (y .|. y) let x, y be Point of X; ::_thesis: (x + y) .|. (x - y) = (((x .|. x) - (x .|. y)) + (y .|. x)) - (y .|. y) (x + y) .|. (x - y) = (x .|. (x - y)) + (y .|. (x - y)) by Def13 .= ((x .|. x) - (x .|. y)) + (y .|. (x - y)) by Th27 .= ((x .|. x) - (x .|. y)) + ((y .|. x) - (y .|. y)) by Th27 .= (((x .|. x) - (x .|. y)) + (y .|. x)) + (- (y .|. y)) ; hence (x + y) .|. (x - y) = (((x .|. x) - (x .|. y)) + (y .|. x)) - (y .|. y) ; ::_thesis: verum end; 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) proof let X be ComplexUnitarySpace; ::_thesis: for x, y being Point of X holds (x - y) .|. (x - y) = (((x .|. x) - (x .|. y)) - (y .|. x)) + (y .|. y) let x, y be Point of X; ::_thesis: (x - y) .|. (x - y) = (((x .|. x) - (x .|. y)) - (y .|. x)) + (y .|. y) (x - y) .|. (x - y) = (x .|. (x - y)) - (y .|. (x - y)) by Th26 .= ((x .|. x) - (x .|. y)) - (y .|. (x - y)) by Th27 .= ((x .|. x) - (x .|. y)) - ((y .|. x) - (y .|. y)) by Th27 ; hence (x - y) .|. (x - y) = (((x .|. x) - (x .|. y)) - (y .|. x)) + (y .|. y) ; ::_thesis: verum end; 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)) proof let X be ComplexUnitarySpace; ::_thesis: 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)) let p, q be Complex; ::_thesis: 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)) let x, y be Point of X; ::_thesis: ((p * x) + (q * y)) .|. ((p * x) + (q * y)) = ((((p * (p *')) * (x .|. x)) + ((p * (q *')) * (x .|. y))) + (((p *') * q) * (y .|. x))) + ((q * (q *')) * (y .|. y)) ((p * x) + (q * y)) .|. ((p * x) + (q * y)) = (p * (x .|. ((p * x) + (q * y)))) + (q * (y .|. ((p * x) + (q * y)))) by Th20 .= (p * (((p *') * (x .|. x)) + ((q *') * (x .|. y)))) + (q * (y .|. ((p * x) + (q * y)))) by Th21 .= (((p * (p *')) * (x .|. x)) + ((p * (q *')) * (x .|. y))) + (q * (((p *') * (y .|. x)) + ((q *') * (y .|. y)))) by Th21 .= (((p * (p *')) * (x .|. x)) + ((p * (q *')) * (x .|. y))) + (((q * (p *')) * (y .|. x)) + ((q * (q *')) * (y .|. y))) ; hence ((p * x) + (q * y)) .|. ((p * x) + (q * y)) = ((((p * (p *')) * (x .|. x)) + ((p * (q *')) * (x .|. y))) + (((p *') * q) * (y .|. x))) + ((q * (q *')) * (y .|. y)) ; ::_thesis: verum end; theorem Th34: :: CSSPACE:34 for X being ComplexUnitarySpace for x being Point of X holds |.(x .|. x).| = Re (x .|. x) proof let X be ComplexUnitarySpace; ::_thesis: for x being Point of X holds |.(x .|. x).| = Re (x .|. x) let x be Point of X; ::_thesis: |.(x .|. x).| = Re (x .|. x) A1: Im (x .|. x) = 0 by Def13; Re (x .|. x) >= 0 by Def13; then |.((Re (x .|. x)) + ((Im (x .|. x)) * )).| = Re (x .|. x) by A1, ABSVALUE:def_1; hence |.(x .|. x).| = Re (x .|. x) by COMPLEX1:13; ::_thesis: verum end; theorem Th35: :: CSSPACE:35 for X being ComplexUnitarySpace for x, y being Point of X holds |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) proof let X be ComplexUnitarySpace; ::_thesis: for x, y being Point of X holds |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) let x, y be Point of X; ::_thesis: |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) A1: ( y <> H1(X) implies |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) ) proof assume y <> H1(X) ; ::_thesis: |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) then y .|. y <> 0c by Def13; then A2: |.(y .|. y).| <> 0 by COMPLEX1:45; A3: (Re (x .|. y)) ^2 >= 0 by XREAL_1:63; set c2 = - (x .|. y); reconsider c1 = |.(y .|. y).| + (0 * ) as Element of COMPLEX by XCMPLX_0:def_2; A4: Re (c1 * ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x)))) = ((Re c1) * (Re ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))))) - ((Im c1) * (Im ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))))) by COMPLEX1:9 .= ((Re c1) * (Re ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))))) - (0 * (Im ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))))) by COMPLEX1:12 .= (Re c1) * (Re ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x)))) ; A5: Re ((- (x .|. y)) * (y .|. x)) = Re (- ((x .|. y) * (y .|. x))) .= - (Re ((x .|. y) * (y .|. x))) by COMPLEX1:17 .= - (Re ((x .|. y) * ((x .|. y) *'))) by Def13 ; A6: Im ((x .|. y) * ((x .|. y) *')) = 0 by COMPLEX1:40; A7: Im (y .|. y) = 0 by Def13; A8: Re (y .|. y) >= 0 by Def13; then |.((Re (y .|. y)) + ((Im (y .|. y)) * )).| = Re (y .|. y) by A7, ABSVALUE:def_1; then A9: |.(y .|. y).| = Re (y .|. y) by COMPLEX1:13; then A10: y .|. y = c1 by A7, COMPLEX1:13; ((c1 * x) + ((- (x .|. y)) * y)) .|. ((c1 * x) + ((- (x .|. y)) * y)) = ((((c1 * (c1 *')) * (x .|. x)) + ((c1 * ((- (x .|. y)) *')) * (x .|. y))) + (((c1 *') * (- (x .|. y))) * (y .|. x))) + (((- (x .|. y)) * ((- (x .|. y)) *')) * (y .|. y)) by Lm9 .= (((c1 * ((c1 *') * (x .|. x))) + (c1 * (((- (x .|. y)) *') * (x .|. y)))) + ((c1 *') * ((- (x .|. y)) * (y .|. x)))) + (c1 * ((- (x .|. y)) * ((- (x .|. y)) *'))) by A7, A9, COMPLEX1:13 .= ((c1 * (((c1 *') * (x .|. x)) + (((- (x .|. y)) *') * (x .|. y)))) + (c1 * ((- (x .|. y)) * (y .|. x)))) + (c1 * ((- (x .|. y)) * ((- (x .|. y)) *'))) by A10, Def13 .= c1 * (((((c1 *') * (x .|. x)) + (((- (x .|. y)) *') * (x .|. y))) + ((- (x .|. y)) * (y .|. x))) + ((- (x .|. y)) * ((- (x .|. y)) *'))) .= c1 * ((((c1 * (x .|. x)) + ((x .|. y) * ((- (x .|. y)) *'))) + ((- (x .|. y)) * (y .|. x))) + ((- (x .|. y)) * ((- (x .|. y)) *'))) by A10, Def13 .= c1 * ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))) ; then Re (c1 * ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x)))) >= 0 by Def13; then ( ( Re c1 >= 0 & Re ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))) >= 0 ) or ( Re c1 <= 0 & Re ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))) <= 0 ) ) by A4, XREAL_1:132; then (Re (c1 * (x .|. x))) + (Re ((- (x .|. y)) * (y .|. x))) >= 0 by A8, A7, A9, A2, COMPLEX1:8, COMPLEX1:13; then (Re (c1 * (x .|. x))) - (Re ((x .|. y) * ((x .|. y) *'))) >= 0 by A5; then A11: Re (c1 * (x .|. x)) >= (Re ((x .|. y) * ((x .|. y) *'))) + 0 by XREAL_1:19; A12: Im (x .|. x) = 0 by Def13; A13: (Im (x .|. y)) ^2 >= 0 by XREAL_1:63; Im c1 = 0 by A7, A9, COMPLEX1:13; then Im (c1 * (x .|. x)) = ((Re c1) * 0) + ((Re (x .|. x)) * 0) by A12, COMPLEX1:9; then A14: |.(c1 * (x .|. x)).| = abs (Re (c1 * (x .|. x))) by COMPLEX1:50; Re ((x .|. y) * ((x .|. y) *')) = ((Re (x .|. y)) ^2) + ((Im (x .|. y)) ^2) by COMPLEX1:40; then A15: Re ((x .|. y) * ((x .|. y) *')) >= 0 + 0 by A3, A13, XREAL_1:7; then abs (Re ((x .|. y) * ((x .|. y) *'))) = Re ((x .|. y) * ((x .|. y) *')) by ABSVALUE:def_1; then abs (Re (c1 * (x .|. x))) >= abs (Re ((x .|. y) * ((x .|. y) *'))) by A11, A15, ABSVALUE:def_1; then |.(c1 * (x .|. x)).| >= |.((x .|. y) * ((x .|. y) *')).| by A6, A14, COMPLEX1:50; then |.(x .|. x).| * |.(y .|. y).| >= |.((x .|. y) * ((x .|. y) *')).| by A10, COMPLEX1:65; then |.(x .|. x).| * |.(y .|. y).| >= |.(x .|. y).| * |.((x .|. y) *').| by COMPLEX1:65; then A16: |.(x .|. x).| * |.(y .|. y).| >= |.(x .|. y).| * |.(x .|. y).| by COMPLEX1:53; |.(x .|. y).| ^2 >= 0 by XREAL_1:63; then A17: sqrt (|.(x .|. x).| * |.(y .|. y).|) >= sqrt (|.(x .|. y).| ^2) by A16, SQUARE_1:26; A18: |.(y .|. y).| >= 0 by COMPLEX1:46; |.(x .|. x).| >= 0 by COMPLEX1:46; then (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) >= sqrt (|.(x .|. y).| ^2) by A17, A18, SQUARE_1:29; hence |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) by COMPLEX1:46, SQUARE_1:22; ::_thesis: verum end; ( y = H1(X) implies |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) ) proof assume A19: y = H1(X) ; ::_thesis: |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) then y .|. y = 0c by Def13; hence |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) by A19, Th30, COMPLEX1:44, SQUARE_1:17; ::_thesis: verum end; hence |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) by A1; ::_thesis: verum end; 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 proof let X be ComplexUnitarySpace; ::_thesis: for x, y being Point of X st x,y are_orthogonal holds x, - y are_orthogonal let x, y be Point of X; ::_thesis: ( x,y are_orthogonal implies x, - y are_orthogonal ) assume x,y are_orthogonal ; ::_thesis: x, - y are_orthogonal then - (x .|. y) = - 0 by Def14; then x .|. (- y) = 0 by Th24; hence x, - y are_orthogonal by Def14; ::_thesis: verum end; theorem :: CSSPACE:37 for X being ComplexUnitarySpace for x, y being Point of X st x,y are_orthogonal holds - x,y are_orthogonal proof let X be ComplexUnitarySpace; ::_thesis: for x, y being Point of X st x,y are_orthogonal holds - x,y are_orthogonal let x, y be Point of X; ::_thesis: ( x,y are_orthogonal implies - x,y are_orthogonal ) assume x,y are_orthogonal ; ::_thesis: - x,y are_orthogonal then - (x .|. y) = - 0 by Def14; then (- x) .|. y = 0 by Th23; hence - x,y are_orthogonal by Def14; ::_thesis: verum end; theorem :: CSSPACE:38 for X being ComplexUnitarySpace for x, y being Point of X st x,y are_orthogonal holds - x, - y are_orthogonal proof let X be ComplexUnitarySpace; ::_thesis: for x, y being Point of X st x,y are_orthogonal holds - x, - y are_orthogonal let x, y be Point of X; ::_thesis: ( x,y are_orthogonal implies - x, - y are_orthogonal ) assume x,y are_orthogonal ; ::_thesis: - x, - y are_orthogonal then x .|. y = 0 by Def14; then (- x) .|. (- y) = 0 by Th25; hence - x, - y are_orthogonal by Def14; ::_thesis: verum end; theorem :: CSSPACE:39 for X being ComplexUnitarySpace for x being Point of X holds x, 0. X are_orthogonal proof let X be ComplexUnitarySpace; ::_thesis: for x being Point of X holds x, 0. X are_orthogonal let x be Point of X; ::_thesis: x, 0. X are_orthogonal (0. X) .|. x = 0 by Th29; hence x, 0. X are_orthogonal by Def14; ::_thesis: verum end; 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) proof let X be ComplexUnitarySpace; ::_thesis: for x, y being Point of X st x,y are_orthogonal holds (x + y) .|. (x + y) = (x .|. x) + (y .|. y) let x, y be Point of X; ::_thesis: ( x,y are_orthogonal implies (x + y) .|. (x + y) = (x .|. x) + (y .|. y) ) assume A1: x,y are_orthogonal ; ::_thesis: (x + y) .|. (x + y) = (x .|. x) + (y .|. y) then A2: y .|. x = 0c by Def14; x .|. y = 0c by A1, Def14; then (x + y) .|. (x + y) = ((x .|. x) + 0c) + (y .|. y) by A2, Th31; hence (x + y) .|. (x + y) = (x .|. x) + (y .|. y) ; ::_thesis: verum end; 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) proof let X be ComplexUnitarySpace; ::_thesis: for x, y being Point of X st x,y are_orthogonal holds (x - y) .|. (x - y) = (x .|. x) + (y .|. y) let x, y be Point of X; ::_thesis: ( x,y are_orthogonal implies (x - y) .|. (x - y) = (x .|. x) + (y .|. y) ) assume A1: x,y are_orthogonal ; ::_thesis: (x - y) .|. (x - y) = (x .|. x) + (y .|. y) then A2: x .|. y = 0 by Def14; (x - y) .|. (x - y) = (((x .|. x) - (x .|. y)) - (y .|. x)) + (y .|. y) by Th33 .= ((x .|. x) + (y .|. y)) - 0 by A1, A2, Def14 ; hence (x - y) .|. (x - y) = (x .|. x) + (y .|. y) ; ::_thesis: verum end; 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 ) proof let X be ComplexUnitarySpace; ::_thesis: for x being Point of X holds ( ||.x.|| = 0 iff x = 0. X ) let x be Point of X; ::_thesis: ( ||.x.|| = 0 iff x = 0. X ) thus ( ||.x.|| = 0 implies x = H1(X) ) ::_thesis: ( x = 0. X implies ||.x.|| = 0 ) proof 0 <= Re (x .|. x) by Def13; then A1: 0 <= |.(x .|. x).| by Th34; assume ||.x.|| = 0 ; ::_thesis: x = H1(X) then |.(x .|. x).| = 0 by A1, SQUARE_1:24; then x .|. x = 0c by COMPLEX1:45; hence x = H1(X) by Def13; ::_thesis: verum end; assume x = H1(X) ; ::_thesis: ||.x.|| = 0 hence ||.x.|| = 0 by Def13, COMPLEX1:44, SQUARE_1:17; ::_thesis: verum end; theorem Th43: :: CSSPACE:43 for a being Complex for X being ComplexUnitarySpace for x being Point of X holds ||.(a * x).|| = |.a.| * ||.x.|| proof let a be Complex; ::_thesis: for X being ComplexUnitarySpace for x being Point of X holds ||.(a * x).|| = |.a.| * ||.x.|| let X be ComplexUnitarySpace; ::_thesis: for x being Point of X holds ||.(a * x).|| = |.a.| * ||.x.|| let x be Point of X; ::_thesis: ||.(a * x).|| = |.a.| * ||.x.|| A1: 0 <= |.(a * a).| by COMPLEX1:46; 0 <= Re (x .|. x) by Def13; then A2: 0 <= |.(x .|. x).| by Th34; ||.(a * x).|| = sqrt |.(a * (x .|. (a * x))).| by Def13 .= sqrt |.(a * ((a *') * (x .|. x))).| by Th18 .= sqrt |.((a * (a *')) * (x .|. x)).| .= sqrt (|.(a * (a *')).| * |.(x .|. x).|) by COMPLEX1:65 .= sqrt (|.(a * a).| * |.(x .|. x).|) by COMPLEX1:69 .= (sqrt |.(a * a).|) * (sqrt |.(x .|. x).|) by A1, A2, SQUARE_1:29 .= (sqrt (|.a.| ^2)) * (sqrt |.(x .|. x).|) by COMPLEX1:65 .= |.a.| * (sqrt |.(x .|. x).|) by COMPLEX1:46, SQUARE_1:22 ; hence ||.(a * x).|| = |.a.| * ||.x.|| ; ::_thesis: verum end; theorem Th44: :: CSSPACE:44 for X being ComplexUnitarySpace for x being Point of X holds 0 <= ||.x.|| proof let X be ComplexUnitarySpace; ::_thesis: for x being Point of X holds 0 <= ||.x.|| let x be Point of X; ::_thesis: 0 <= ||.x.|| 0 <= Re (x .|. x) by Def13; then 0 <= |.(x .|. x).| by Th34; hence 0 <= ||.x.|| by SQUARE_1:def_2; ::_thesis: verum end; 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.|| proof let X be ComplexUnitarySpace; ::_thesis: for x, y being Point of X holds ||.(x + y).|| <= ||.x.|| + ||.y.|| let x, y be Point of X; ::_thesis: ||.(x + y).|| <= ||.x.|| + ||.y.|| A1: ||.(x + y).|| ^2 >= 0 by XREAL_1:63; Re ((x + y) .|. (x + y)) >= 0 by Def13; then A2: |.((x + y) .|. (x + y)).| >= 0 by Th34; sqrt (||.(x + y).|| ^2) = sqrt |.((x + y) .|. (x + y)).| by Th44, SQUARE_1:22; then A3: ||.(x + y).|| ^2 = |.((x + y) .|. (x + y)).| by A2, A1, SQUARE_1:28; |.(y .|. y).| >= 0 by COMPLEX1:46; then A4: |.(y .|. y).| = ||.y.|| ^2 by SQUARE_1:def_2; A5: - (Im (x .|. y)) = Im ((x .|. y) *') by COMPLEX1:27 .= Im (y .|. x) by Def13 ; Im ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y)) = (Im (((x .|. x) + (x .|. y)) + (y .|. x))) + (Im (y .|. y)) by COMPLEX1:8 .= ((Im ((x .|. x) + (x .|. y))) + (Im (y .|. x))) + (Im (y .|. y)) by COMPLEX1:8 .= (((Im (x .|. x)) + (Im (x .|. y))) + (Im (y .|. x))) + (Im (y .|. y)) by COMPLEX1:8 .= ((0 + (Im (x .|. y))) + (Im (y .|. x))) + (Im (y .|. y)) by Def13 .= ((Im (x .|. y)) + (Im (y .|. x))) + 0 by Def13 ; then A6: (((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y) = (Re ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y))) + (0 * ) by A5, COMPLEX1:13; A7: Re (x .|. y) = Re ((x .|. y) *') by COMPLEX1:27 .= Re (y .|. x) by Def13 ; A8: Re (x .|. y) <= |.(x .|. y).| by COMPLEX1:54; |.(x .|. y).| <= ||.x.|| * ||.y.|| by Th35; then Re (x .|. y) <= ||.x.|| * ||.y.|| by A8, XXREAL_0:2; then A9: 2 * (Re (x .|. y)) <= 2 * (||.x.|| * ||.y.||) by XREAL_1:64; Re ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y)) = Re ((x + y) .|. (x + y)) by Th31; then A10: Re ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y)) >= 0 by Def13; Re ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y)) = (Re (((x .|. x) + (x .|. y)) + (y .|. x))) + (Re (y .|. y)) by COMPLEX1:8 .= ((Re ((x .|. x) + (x .|. y))) + (Re (y .|. x))) + (Re (y .|. y)) by COMPLEX1:8 .= (((Re (x .|. x)) + (Re (x .|. y))) + (Re (y .|. x))) + (Re (y .|. y)) by COMPLEX1:8 .= ((|.(x .|. x).| + (Re (x .|. y))) + (Re (y .|. x))) + (Re (y .|. y)) by Th34 .= ((|.(x .|. x).| + (Re (x .|. y))) + (Re (y .|. x))) + |.(y .|. y).| by Th34 ; then |.((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y)).| = (|.(x .|. x).| + (2 * (Re (x .|. y)))) + |.(y .|. y).| by A7, A10, A6, ABSVALUE:def_1; then A11: ||.(x + y).|| ^2 = (2 * (Re (x .|. y))) + (|.(x .|. x).| + |.(y .|. y).|) by A3, Th31; A12: ||.y.|| >= 0 by Th44; |.(x .|. x).| >= 0 by COMPLEX1:46; then (sqrt |.(x .|. x).|) ^2 = |.(x .|. x).| by SQUARE_1:def_2; then ||.(x + y).|| ^2 <= (2 * (||.x.|| * ||.y.||)) + ((||.x.|| ^2) + |.(y .|. y).|) by A11, A9, XREAL_1:6; then A13: ||.(x + y).|| ^2 <= (||.x.|| + ||.y.||) ^2 by A4; ||.x.|| >= 0 by Th44; then ||.x.|| + ||.y.|| >= 0 + 0 by A12, XREAL_1:7; hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by A13, SQUARE_1:16; ::_thesis: verum end; theorem Th47: :: CSSPACE:47 for X being ComplexUnitarySpace for x being Point of X holds ||.(- x).|| = ||.x.|| proof let X be ComplexUnitarySpace; ::_thesis: for x being Point of X holds ||.(- x).|| = ||.x.|| let x be Point of X; ::_thesis: ||.(- x).|| = ||.x.|| ||.(- x).|| = ||.((- 1r) * x).|| by CLVECT_1:3 .= |.(- 1r).| * ||.x.|| by Th43 .= |.1r.| * ||.x.|| by COMPLEX1:52 ; hence ||.(- x).|| = ||.x.|| by COMPLEX1:48; ::_thesis: verum end; theorem Th48: :: CSSPACE:48 for X being ComplexUnitarySpace for x, y being Point of X holds ||.x.|| - ||.y.|| <= ||.(x - y).|| proof let X be ComplexUnitarySpace; ::_thesis: for x, y being Point of X holds ||.x.|| - ||.y.|| <= ||.(x - y).|| let x, y be Point of X; ::_thesis: ||.x.|| - ||.y.|| <= ||.(x - y).|| (x - y) + y = x - (y - y) by RLVECT_1:29 .= x - H1(X) by RLVECT_1:15 .= x by RLVECT_1:13 ; then ||.x.|| <= ||.(x - y).|| + ||.y.|| by Th46; hence ||.x.|| - ||.y.|| <= ||.(x - y).|| by XREAL_1:20; ::_thesis: verum end; theorem :: CSSPACE:49 for X being ComplexUnitarySpace for x, y being Point of X holds abs (||.x.|| - ||.y.||) <= ||.(x - y).|| proof let X be ComplexUnitarySpace; ::_thesis: for x, y being Point of X holds abs (||.x.|| - ||.y.||) <= ||.(x - y).|| let x, y be Point of X; ::_thesis: abs (||.x.|| - ||.y.||) <= ||.(x - y).|| (y - x) + x = y - (x - x) by RLVECT_1:29 .= y - H1(X) by RLVECT_1:15 .= y by RLVECT_1:13 ; then ||.y.|| <= ||.(y - x).|| + ||.x.|| by Th46; then ||.y.|| - ||.x.|| <= ||.(y - x).|| by XREAL_1:20; then ||.y.|| - ||.x.|| <= ||.(- (x - y)).|| by RLVECT_1:33; then ||.y.|| - ||.x.|| <= ||.(x - y).|| by Th47; then A1: - ||.(x - y).|| <= - (||.y.|| - ||.x.||) by XREAL_1:24; ||.x.|| - ||.y.|| <= ||.(x - y).|| by Th48; hence abs (||.x.|| - ||.y.||) <= ||.(x - y).|| by A1, ABSVALUE:5; ::_thesis: verum end; 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) proof let x, y be Point of X; ::_thesis: dist (x,y) = dist (y,x) thus dist (x,y) = ||.(- (y - x)).|| by RLVECT_1:33 .= dist (y,x) by Th47 ; ::_thesis: verum end; end; theorem Th50: :: CSSPACE:50 for X being ComplexUnitarySpace for x being Point of X holds dist (x,x) = 0 proof let X be ComplexUnitarySpace; ::_thesis: for x being Point of X holds dist (x,x) = 0 let x be Point of X; ::_thesis: dist (x,x) = 0 thus dist (x,x) = ||.H1(X).|| by RLVECT_1:15 .= 0 by Th42 ; ::_thesis: verum end; 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)) proof let X be ComplexUnitarySpace; ::_thesis: for x, z, y being Point of X holds dist (x,z) <= (dist (x,y)) + (dist (y,z)) let x, z, y be Point of X; ::_thesis: dist (x,z) <= (dist (x,y)) + (dist (y,z)) dist (x,z) = ||.((x - z) + H1(X)).|| by RLVECT_1:4 .= ||.((x - z) + (y - y)).|| by RLVECT_1:15 .= ||.(x - (z - (y - y))).|| by RLVECT_1:29 .= ||.(x - (y + (z - y))).|| by RLVECT_1:29 .= ||.((x - y) - (z - y)).|| by RLVECT_1:27 .= ||.((x - y) + (y - z)).|| by RLVECT_1:33 ; hence dist (x,z) <= (dist (x,y)) + (dist (y,z)) by Th46; ::_thesis: verum end; theorem Th52: :: CSSPACE:52 for X being ComplexUnitarySpace for x, y being Point of X holds ( x <> y iff dist (x,y) <> 0 ) proof let X be ComplexUnitarySpace; ::_thesis: for x, y being Point of X holds ( x <> y iff dist (x,y) <> 0 ) let x, y be Point of X; ::_thesis: ( x <> y iff dist (x,y) <> 0 ) thus ( x <> y implies dist (x,y) <> 0 ) ::_thesis: ( dist (x,y) <> 0 implies x <> y ) proof assume that A1: x <> y and A2: dist (x,y) = 0 ; ::_thesis: contradiction x - y = H1(X) by A2, Th42; hence contradiction by A1, RLVECT_1:21; ::_thesis: verum end; thus ( dist (x,y) <> 0 implies x <> y ) by Th50; ::_thesis: verum end; 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 ) proof let X be ComplexUnitarySpace; ::_thesis: for x, y being Point of X holds ( x <> y iff dist (x,y) > 0 ) let x, y be Point of X; ::_thesis: ( x <> y iff dist (x,y) > 0 ) thus ( x <> y implies dist (x,y) > 0 ) ::_thesis: ( dist (x,y) > 0 implies x <> y ) proof assume x <> y ; ::_thesis: dist (x,y) > 0 then dist (x,y) <> 0 by Th52; hence dist (x,y) > 0 by Th44; ::_thesis: verum end; thus ( dist (x,y) > 0 implies x <> y ) by Th50; ::_thesis: verum end; 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)) proof let X be ComplexUnitarySpace; ::_thesis: for x, y, u, v being Point of X holds dist ((x + y),(u + v)) <= (dist (x,u)) + (dist (y,v)) let x, y, u, v be Point of X; ::_thesis: dist ((x + y),(u + v)) <= (dist (x,u)) + (dist (y,v)) dist ((x + y),(u + v)) = ||.(((- u) + (- v)) + (x + y)).|| by RLVECT_1:31 .= ||.((x + ((- u) + (- v))) + y).|| by RLVECT_1:def_3 .= ||.(((x - u) + (- v)) + y).|| by RLVECT_1:def_3 .= ||.((x - u) + (y - v)).|| by RLVECT_1:def_3 ; hence dist ((x + y),(u + v)) <= (dist (x,u)) + (dist (y,v)) by Th46; ::_thesis: verum end; 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)) proof let X be ComplexUnitarySpace; ::_thesis: for x, y, u, v being Point of X holds dist ((x - y),(u - v)) <= (dist (x,u)) + (dist (y,v)) let x, y, u, v be Point of X; ::_thesis: dist ((x - y),(u - v)) <= (dist (x,u)) + (dist (y,v)) dist ((x - y),(u - v)) = ||.(((x - y) - u) + v).|| by RLVECT_1:29 .= ||.((x - (u + y)) + v).|| by RLVECT_1:27 .= ||.(((x - u) - y) + v).|| by RLVECT_1:27 .= ||.((x - u) - (y - v)).|| by RLVECT_1:29 .= ||.((x - u) + (- (y - v))).|| ; then dist ((x - y),(u - v)) <= ||.(x - u).|| + ||.(- (y - v)).|| by Th46; hence dist ((x - y),(u - v)) <= (dist (x,u)) + (dist (y,v)) by Th47; ::_thesis: verum end; theorem :: CSSPACE:58 for X being ComplexUnitarySpace for x, z, y being Point of X holds dist ((x - z),(y - z)) = dist (x,y) proof let X be ComplexUnitarySpace; ::_thesis: for x, z, y being Point of X holds dist ((x - z),(y - z)) = dist (x,y) let x, z, y be Point of X; ::_thesis: dist ((x - z),(y - z)) = dist (x,y) thus dist ((x - z),(y - z)) = ||.(((x - z) - y) + z).|| by RLVECT_1:29 .= ||.((x - (y + z)) + z).|| by RLVECT_1:27 .= ||.(((x - y) - z) + z).|| by RLVECT_1:27 .= ||.((x - y) - (z - z)).|| by RLVECT_1:29 .= ||.((x - y) - H1(X)).|| by RLVECT_1:15 .= dist (x,y) by RLVECT_1:13 ; ::_thesis: verum end; 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)) proof let X be ComplexUnitarySpace; ::_thesis: for x, z, y being Point of X holds dist ((x - z),(y - z)) <= (dist (z,x)) + (dist (z,y)) let x, z, y be Point of X; ::_thesis: dist ((x - z),(y - z)) <= (dist (z,x)) + (dist (z,y)) dist ((x - z),(y - z)) = ||.((x - z) + (z - y)).|| by RLVECT_1:33 .= ||.((- (z - x)) + (z - y)).|| by RLVECT_1:33 ; then dist ((x - z),(y - z)) <= ||.(- (z - x)).|| + ||.(z - y).|| by Th46; hence dist ((x - z),(y - z)) <= (dist (z,x)) + (dist (z,y)) by Th47; ::_thesis: verum end; 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 proof let seq1, seq2 be sequence of X; ::_thesis: seq1 + seq2 = seq2 + seq1 now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq1_+_seq2)_._n_=_(seq2_+_seq1)_._n let n be Element of NAT ; ::_thesis: (seq1 + seq2) . n = (seq2 + seq1) . n thus (seq1 + seq2) . n = (seq2 . n) + (seq1 . n) by NORMSP_1:def_2 .= (seq2 + seq1) . n by NORMSP_1:def_2 ; ::_thesis: verum end; hence seq1 + seq2 = seq2 + seq1 by FUNCT_2:63; ::_thesis: verum end; end; theorem :: CSSPACE:60 for X being ComplexUnitarySpace for seq1, seq2, seq3 being sequence of X holds seq1 + (seq2 + seq3) = (seq1 + seq2) + seq3 proof let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2, seq3 being sequence of X holds seq1 + (seq2 + seq3) = (seq1 + seq2) + seq3 let seq1, seq2, seq3 be sequence of X; ::_thesis: seq1 + (seq2 + seq3) = (seq1 + seq2) + seq3 now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq1_+_(seq2_+_seq3))_._n_=_((seq1_+_seq2)_+_seq3)_._n let n be Element of NAT ; ::_thesis: (seq1 + (seq2 + seq3)) . n = ((seq1 + seq2) + seq3) . n thus (seq1 + (seq2 + seq3)) . n = (seq1 . n) + ((seq2 + seq3) . n) by NORMSP_1:def_2 .= (seq1 . n) + ((seq2 . n) + (seq3 . n)) by NORMSP_1:def_2 .= ((seq1 . n) + (seq2 . n)) + (seq3 . n) by RLVECT_1:def_3 .= ((seq1 + seq2) . n) + (seq3 . n) by NORMSP_1:def_2 .= ((seq1 + seq2) + seq3) . n by NORMSP_1:def_2 ; ::_thesis: verum end; hence seq1 + (seq2 + seq3) = (seq1 + seq2) + seq3 by FUNCT_2:63; ::_thesis: verum end; 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 proof let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2, seq being sequence of X st seq1 is constant & seq2 is constant & seq = seq1 + seq2 holds seq is constant let seq1, seq2, seq be sequence of X; ::_thesis: ( seq1 is constant & seq2 is constant & seq = seq1 + seq2 implies seq is constant ) assume that A1: seq1 is constant and A2: seq2 is constant and A3: seq = seq1 + seq2 ; ::_thesis: seq is constant consider x being Point of X such that A4: for n being Nat holds seq1 . n = x by A1, VALUED_0:def_18; consider y being Point of X such that A5: for n being Nat holds seq2 . n = y by A2, VALUED_0:def_18; take z = x + y; :: according to VALUED_0:def_20 ::_thesis: for b1 being set holds seq . b1 = z let n be Nat; ::_thesis: seq . n = z n in NAT by ORDINAL1:def_12; hence seq . n = (seq1 . n) + (seq2 . n) by A3, NORMSP_1:def_2 .= x + (seq2 . n) by A4 .= z by A5 ; ::_thesis: verum end; 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 proof let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2, seq being sequence of X st seq1 is constant & seq2 is constant & seq = seq1 - seq2 holds seq is constant let seq1, seq2, seq be sequence of X; ::_thesis: ( seq1 is constant & seq2 is constant & seq = seq1 - seq2 implies seq is constant ) assume that A1: seq1 is constant and A2: seq2 is constant and A3: seq = seq1 - seq2 ; ::_thesis: seq is constant consider x being Point of X such that A4: for n being Nat holds seq1 . n = x by A1, VALUED_0:def_18; consider y being Point of X such that A5: for n being Nat holds seq2 . n = y by A2, VALUED_0:def_18; take z = x - y; :: according to VALUED_0:def_20 ::_thesis: for b1 being set holds seq . b1 = z let n be Nat; ::_thesis: seq . n = z n in NAT by ORDINAL1:def_12; hence seq . n = (seq1 . n) - (seq2 . n) by A3, NORMSP_1:def_3 .= x - (seq2 . n) by A4 .= z by A5 ; ::_thesis: verum end; 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 proof let a be Complex; ::_thesis: for X being ComplexUnitarySpace for seq1, seq being sequence of X st seq1 is constant & seq = a * seq1 holds seq is constant let X be ComplexUnitarySpace; ::_thesis: for seq1, seq being sequence of X st seq1 is constant & seq = a * seq1 holds seq is constant let seq1, seq be sequence of X; ::_thesis: ( seq1 is constant & seq = a * seq1 implies seq is constant ) assume that A1: seq1 is constant and A2: seq = a * seq1 ; ::_thesis: seq is constant consider x being Point of X such that A3: for n being Nat holds seq1 . n = x by A1, VALUED_0:def_18; take z = a * x; :: according to VALUED_0:def_20 ::_thesis: for b1 being set holds seq . b1 = z let n be Nat; ::_thesis: seq . n = z n in NAT by ORDINAL1:def_12; hence seq . n = a * (seq1 . n) by A2, CLVECT_1:def_14 .= z by A3 ; ::_thesis: verum end; theorem :: CSSPACE:64 for X being ComplexUnitarySpace for seq1, seq2 being sequence of X holds seq1 - seq2 = seq1 + (- seq2) proof let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X holds seq1 - seq2 = seq1 + (- seq2) let seq1, seq2 be sequence of X; ::_thesis: seq1 - seq2 = seq1 + (- seq2) now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq1_-_seq2)_._n_=_(seq1_+_(-_seq2))_._n let n be Element of NAT ; ::_thesis: (seq1 - seq2) . n = (seq1 + (- seq2)) . n thus (seq1 - seq2) . n = (seq1 . n) - (seq2 . n) by NORMSP_1:def_3 .= (seq1 . n) + ((- seq2) . n) by BHSP_1:44 .= (seq1 + (- seq2)) . n by NORMSP_1:def_2 ; ::_thesis: verum end; hence seq1 - seq2 = seq1 + (- seq2) by FUNCT_2:63; ::_thesis: verum end; theorem :: CSSPACE:65 for X being ComplexUnitarySpace for seq being sequence of X holds seq = seq + (0. X) proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X holds seq = seq + (0. X) let seq be sequence of X; ::_thesis: seq = seq + (0. X) now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq_+_H1(X))_._n_=_seq_._n let n be Element of NAT ; ::_thesis: (seq + H1(X)) . n = seq . n thus (seq + H1(X)) . n = (seq . n) + H1(X) by BHSP_1:def_6 .= seq . n by RLVECT_1:4 ; ::_thesis: verum end; hence seq = seq + (0. X) by FUNCT_2:63; ::_thesis: verum end; 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) proof let a be Complex; ::_thesis: for X being ComplexUnitarySpace for seq1, seq2 being sequence of X holds a * (seq1 + seq2) = (a * seq1) + (a * seq2) let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X holds a * (seq1 + seq2) = (a * seq1) + (a * seq2) let seq1, seq2 be sequence of X; ::_thesis: a * (seq1 + seq2) = (a * seq1) + (a * seq2) now__::_thesis:_for_n_being_Element_of_NAT_holds_(a_*_(seq1_+_seq2))_._n_=_((a_*_seq1)_+_(a_*_seq2))_._n let n be Element of NAT ; ::_thesis: (a * (seq1 + seq2)) . n = ((a * seq1) + (a * seq2)) . n thus (a * (seq1 + seq2)) . n = a * ((seq1 + seq2) . n) by CLVECT_1:def_14 .= a * ((seq1 . n) + (seq2 . n)) by NORMSP_1:def_2 .= (a * (seq1 . n)) + (a * (seq2 . n)) by CLVECT_1:def_2 .= ((a * seq1) . n) + (a * (seq2 . n)) by CLVECT_1:def_14 .= ((a * seq1) . n) + ((a * seq2) . n) by CLVECT_1:def_14 .= ((a * seq1) + (a * seq2)) . n by NORMSP_1:def_2 ; ::_thesis: verum end; hence a * (seq1 + seq2) = (a * seq1) + (a * seq2) by FUNCT_2:63; ::_thesis: verum end; 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) proof let a, b be Complex; ::_thesis: for X being ComplexUnitarySpace for seq being sequence of X holds (a + b) * seq = (a * seq) + (b * seq) let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X holds (a + b) * seq = (a * seq) + (b * seq) let seq be sequence of X; ::_thesis: (a + b) * seq = (a * seq) + (b * seq) now__::_thesis:_for_n_being_Element_of_NAT_holds_((a_+_b)_*_seq)_._n_=_((a_*_seq)_+_(b_*_seq))_._n let n be Element of NAT ; ::_thesis: ((a + b) * seq) . n = ((a * seq) + (b * seq)) . n thus ((a + b) * seq) . n = (a + b) * (seq . n) by CLVECT_1:def_14 .= (a * (seq . n)) + (b * (seq . n)) by CLVECT_1:def_3 .= ((a * seq) . n) + (b * (seq . n)) by CLVECT_1:def_14 .= ((a * seq) . n) + ((b * seq) . n) by CLVECT_1:def_14 .= ((a * seq) + (b * seq)) . n by NORMSP_1:def_2 ; ::_thesis: verum end; hence (a + b) * seq = (a * seq) + (b * seq) by FUNCT_2:63; ::_thesis: verum end; 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) proof let a, b be Complex; ::_thesis: for X being ComplexUnitarySpace for seq being sequence of X holds (a * b) * seq = a * (b * seq) let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X holds (a * b) * seq = a * (b * seq) let seq be sequence of X; ::_thesis: (a * b) * seq = a * (b * seq) now__::_thesis:_for_n_being_Element_of_NAT_holds_((a_*_b)_*_seq)_._n_=_(a_*_(b_*_seq))_._n let n be Element of NAT ; ::_thesis: ((a * b) * seq) . n = (a * (b * seq)) . n thus ((a * b) * seq) . n = (a * b) * (seq . n) by CLVECT_1:def_14 .= a * (b * (seq . n)) by CLVECT_1:def_4 .= a * ((b * seq) . n) by CLVECT_1:def_14 .= (a * (b * seq)) . n by CLVECT_1:def_14 ; ::_thesis: verum end; hence (a * b) * seq = a * (b * seq) by FUNCT_2:63; ::_thesis: verum end; theorem :: CSSPACE:69 for X being ComplexUnitarySpace for seq being sequence of X holds 1r * seq = seq proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X holds 1r * seq = seq let seq be sequence of X; ::_thesis: 1r * seq = seq now__::_thesis:_for_n_being_Element_of_NAT_holds_(1r_*_seq)_._n_=_seq_._n let n be Element of NAT ; ::_thesis: (1r * seq) . n = seq . n thus (1r * seq) . n = 1r * (seq . n) by CLVECT_1:def_14 .= seq . n by CLVECT_1:def_5 ; ::_thesis: verum end; hence 1r * seq = seq by FUNCT_2:63; ::_thesis: verum end; theorem :: CSSPACE:70 for X being ComplexUnitarySpace for seq being sequence of X holds (- 1r) * seq = - seq proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X holds (- 1r) * seq = - seq let seq be sequence of X; ::_thesis: (- 1r) * seq = - seq now__::_thesis:_for_n_being_Element_of_NAT_holds_((-_1r)_*_seq)_._n_=_(-_seq)_._n let n be Element of NAT ; ::_thesis: ((- 1r) * seq) . n = (- seq) . n thus ((- 1r) * seq) . n = (- 1r) * (seq . n) by CLVECT_1:def_14 .= - (seq . n) by CLVECT_1:3 .= (- seq) . n by BHSP_1:44 ; ::_thesis: verum end; hence (- 1r) * seq = - seq by FUNCT_2:63; ::_thesis: verum end; theorem :: CSSPACE:71 for X being ComplexUnitarySpace for x being Point of X for seq being sequence of X holds seq - x = seq + (- x) proof let X be ComplexUnitarySpace; ::_thesis: for x being Point of X for seq being sequence of X holds seq - x = seq + (- x) let x be Point of X; ::_thesis: for seq being sequence of X holds seq - x = seq + (- x) let seq be sequence of X; ::_thesis: seq - x = seq + (- x) now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq_-_x)_._n_=_(seq_+_(-_x))_._n let n be Element of NAT ; ::_thesis: (seq - x) . n = (seq + (- x)) . n thus (seq - x) . n = (seq . n) - x by NORMSP_1:def_4 .= (seq + (- x)) . n by BHSP_1:def_6 ; ::_thesis: verum end; hence seq - x = seq + (- x) by FUNCT_2:63; ::_thesis: verum end; theorem :: CSSPACE:72 for X being ComplexUnitarySpace for seq1, seq2 being sequence of X holds seq1 - seq2 = - (seq2 - seq1) proof let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X holds seq1 - seq2 = - (seq2 - seq1) let seq1, seq2 be sequence of X; ::_thesis: seq1 - seq2 = - (seq2 - seq1) now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq1_-_seq2)_._n_=_(-_(seq2_-_seq1))_._n let n be Element of NAT ; ::_thesis: (seq1 - seq2) . n = (- (seq2 - seq1)) . n thus (seq1 - seq2) . n = (seq1 . n) - (seq2 . n) by NORMSP_1:def_3 .= - ((seq2 . n) - (seq1 . n)) by RLVECT_1:33 .= - ((seq2 - seq1) . n) by NORMSP_1:def_3 .= (- (seq2 - seq1)) . n by BHSP_1:44 ; ::_thesis: verum end; hence seq1 - seq2 = - (seq2 - seq1) by FUNCT_2:63; ::_thesis: verum end; theorem :: CSSPACE:73 for X being ComplexUnitarySpace for seq being sequence of X holds seq = seq - (0. X) proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X holds seq = seq - (0. X) let seq be sequence of X; ::_thesis: seq = seq - (0. X) now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq_-_H1(X))_._n_=_seq_._n let n be Element of NAT ; ::_thesis: (seq - H1(X)) . n = seq . n thus (seq - H1(X)) . n = (seq . n) - H1(X) by NORMSP_1:def_4 .= seq . n by RLVECT_1:13 ; ::_thesis: verum end; hence seq = seq - (0. X) by FUNCT_2:63; ::_thesis: verum end; theorem :: CSSPACE:74 for X being ComplexUnitarySpace for seq being sequence of X holds seq = - (- seq) proof let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X holds seq = - (- seq) let seq be sequence of X; ::_thesis: seq = - (- seq) now__::_thesis:_for_n_being_Element_of_NAT_holds_(-_(-_seq))_._n_=_seq_._n let n be Element of NAT ; ::_thesis: (- (- seq)) . n = seq . n thus (- (- seq)) . n = - ((- seq) . n) by BHSP_1:44 .= - (- (seq . n)) by BHSP_1:44 .= seq . n by RLVECT_1:17 ; ::_thesis: verum end; hence seq = - (- seq) by FUNCT_2:63; ::_thesis: verum end; theorem :: CSSPACE:75 for X being ComplexUnitarySpace for seq1, seq2, seq3 being sequence of X holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3 proof let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2, seq3 being sequence of X holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3 let seq1, seq2, seq3 be sequence of X; ::_thesis: seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3 now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq1_-_(seq2_+_seq3))_._n_=_((seq1_-_seq2)_-_seq3)_._n let n be Element of NAT ; ::_thesis: (seq1 - (seq2 + seq3)) . n = ((seq1 - seq2) - seq3) . n thus (seq1 - (seq2 + seq3)) . n = (seq1 . n) - ((seq2 + seq3) . n) by NORMSP_1:def_3 .= (seq1 . n) - ((seq2 . n) + (seq3 . n)) by NORMSP_1:def_2 .= ((seq1 . n) - (seq2 . n)) - (seq3 . n) by RLVECT_1:27 .= ((seq1 - seq2) . n) - (seq3 . n) by NORMSP_1:def_3 .= ((seq1 - seq2) - seq3) . n by NORMSP_1:def_3 ; ::_thesis: verum end; hence seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3 by FUNCT_2:63; ::_thesis: verum end; theorem :: CSSPACE:76 for X being ComplexUnitarySpace for seq1, seq2, seq3 being sequence of X holds (seq1 + seq2) - seq3 = seq1 + (seq2 - seq3) proof let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2, seq3 being sequence of X holds (seq1 + seq2) - seq3 = seq1 + (seq2 - seq3) let seq1, seq2, seq3 be sequence of X; ::_thesis: (seq1 + seq2) - seq3 = seq1 + (seq2 - seq3) now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_+_seq2)_-_seq3)_._n_=_(seq1_+_(seq2_-_seq3))_._n let n be Element of NAT ; ::_thesis: ((seq1 + seq2) - seq3) . n = (seq1 + (seq2 - seq3)) . n thus ((seq1 + seq2) - seq3) . n = ((seq1 + seq2) . n) - (seq3 . n) by NORMSP_1:def_3 .= ((seq1 . n) + (seq2 . n)) - (seq3 . n) by NORMSP_1:def_2 .= (seq1 . n) + ((seq2 . n) - (seq3 . n)) by RLVECT_1:def_3 .= (seq1 . n) + ((seq2 - seq3) . n) by NORMSP_1:def_3 .= (seq1 + (seq2 - seq3)) . n by NORMSP_1:def_2 ; ::_thesis: verum end; hence (seq1 + seq2) - seq3 = seq1 + (seq2 - seq3) by FUNCT_2:63; ::_thesis: verum end; theorem :: CSSPACE:77 for X being ComplexUnitarySpace for seq1, seq2, seq3 being sequence of X holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3 proof let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2, seq3 being sequence of X holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3 let seq1, seq2, seq3 be sequence of X; ::_thesis: seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3 now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq1_-_(seq2_-_seq3))_._n_=_((seq1_-_seq2)_+_seq3)_._n let n be Element of NAT ; ::_thesis: (seq1 - (seq2 - seq3)) . n = ((seq1 - seq2) + seq3) . n thus (seq1 - (seq2 - seq3)) . n = (seq1 . n) - ((seq2 - seq3) . n) by NORMSP_1:def_3 .= (seq1 . n) - ((seq2 . n) - (seq3 . n)) by NORMSP_1:def_3 .= ((seq1 . n) - (seq2 . n)) + (seq3 . n) by RLVECT_1:29 .= ((seq1 - seq2) . n) + (seq3 . n) by NORMSP_1:def_3 .= ((seq1 - seq2) + seq3) . n by NORMSP_1:def_2 ; ::_thesis: verum end; hence seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3 by FUNCT_2:63; ::_thesis: verum end; 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) proof let a be Complex; ::_thesis: for X being ComplexUnitarySpace for seq1, seq2 being sequence of X holds a * (seq1 - seq2) = (a * seq1) - (a * seq2) let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X holds a * (seq1 - seq2) = (a * seq1) - (a * seq2) let seq1, seq2 be sequence of X; ::_thesis: a * (seq1 - seq2) = (a * seq1) - (a * seq2) now__::_thesis:_for_n_being_Element_of_NAT_holds_(a_*_(seq1_-_seq2))_._n_=_((a_*_seq1)_-_(a_*_seq2))_._n let n be Element of NAT ; ::_thesis: (a * (seq1 - seq2)) . n = ((a * seq1) - (a * seq2)) . n thus (a * (seq1 - seq2)) . n = a * ((seq1 - seq2) . n) by CLVECT_1:def_14 .= a * ((seq1 . n) - (seq2 . n)) by NORMSP_1:def_3 .= (a * (seq1 . n)) - (a * (seq2 . n)) by CLVECT_1:9 .= ((a * seq1) . n) - (a * (seq2 . n)) by CLVECT_1:def_14 .= ((a * seq1) . n) - ((a * seq2) . n) by CLVECT_1:def_14 .= ((a * seq1) - (a * seq2)) . n by NORMSP_1:def_3 ; ::_thesis: verum end; hence a * (seq1 - seq2) = (a * seq1) - (a * seq2) by FUNCT_2:63; ::_thesis: verum end; 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) *')) proof deffunc H2( set , set ) -> Element of COMPLEX = Sum ((seq_id $1) (#) ((seq_id $2) *')); set X = the_set_of_l2ComplexSequences ; A1: for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds H2(x,y) in COMPLEX ; ex f 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 f . (x,y) = H2(x,y) from BINOP_1:sch_2(A1); hence 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) *')) ; ::_thesis: verum end; 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 proof set X = the_set_of_l2ComplexSequences ; let scalar1, scalar2 be Function of [:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:],COMPLEX; ::_thesis: ( ( for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds scalar1 . (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 scalar2 . (x,y) = Sum ((seq_id x) (#) ((seq_id y) *')) ) implies scalar1 = scalar2 ) assume that A2: for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds scalar1 . (x,y) = Sum ((seq_id x) (#) ((seq_id y) *')) and A3: for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds scalar2 . (x,y) = Sum ((seq_id x) (#) ((seq_id y) *')) ; ::_thesis: scalar1 = scalar2 for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds scalar1 . (x,y) = scalar2 . (x,y) proof let x, y be set ; ::_thesis: ( x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences implies scalar1 . (x,y) = scalar2 . (x,y) ) assume that A4: x in the_set_of_l2ComplexSequences and A5: y in the_set_of_l2ComplexSequences ; ::_thesis: scalar1 . (x,y) = scalar2 . (x,y) thus scalar1 . (x,y) = Sum ((seq_id x) (#) ((seq_id y) *')) by A2, A4, A5 .= scalar2 . (x,y) by A3, A4, A5 ; ::_thesis: verum end; hence scalar1 = scalar2 by BINOP_1:1; ::_thesis: verum end; 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 proof let l be CLSStruct ; ::_thesis: ( CLSStruct(# the carrier of l, the ZeroF of l, the addF of l, the Mult of l #) is ComplexLinearSpace implies l is ComplexLinearSpace ) assume A1: CLSStruct(# the carrier of l, the ZeroF of l, the addF of l, the Mult of l #) is ComplexLinearSpace ; ::_thesis: l is ComplexLinearSpace reconsider l = l as non empty CLSStruct by A1; reconsider l0 = CLSStruct(# the carrier of l,(0. l), the addF of l, the Mult of l #) as ComplexLinearSpace by A1; A2: l is Abelian proof let v, w be VECTOR of l; :: according to RLVECT_1:def_2 ::_thesis: v + w = w + v reconsider v1 = v as VECTOR of l0 ; reconsider w1 = w as VECTOR of l0 ; thus v + w = v1 + w1 .= w1 + v1 .= w + v ; ::_thesis: verum end; A3: l is add-associative proof let u, v, w be VECTOR of l; :: according to RLVECT_1:def_3 ::_thesis: (u + v) + w = u + (v + w) reconsider u1 = u as VECTOR of l0 ; reconsider v1 = v as VECTOR of l0 ; reconsider w1 = w as VECTOR of l0 ; thus (u + v) + w = (u1 + v1) + w1 .= u1 + (v1 + w1) by RLVECT_1:def_3 .= u + (v + w) ; ::_thesis: verum end; A4: ( l is vector-distributive & l is scalar-distributive & l is scalar-associative & l is scalar-unital ) proof thus for z being Complex for v, w being VECTOR of l holds z * (v + w) = (z * v) + (z * w) :: according to CLVECT_1:def_2 ::_thesis: ( l is scalar-distributive & l is scalar-associative & l is scalar-unital ) proof let z be Complex; ::_thesis: for v, w being VECTOR of l holds z * (v + w) = (z * v) + (z * w) let v, w be VECTOR of l; ::_thesis: z * (v + w) = (z * v) + (z * w) reconsider v1 = v, w1 = w as VECTOR of l0 ; thus z * (v + w) = z * (v1 + w1) .= (z * v1) + (z * w1) by CLVECT_1:def_2 .= (z * v) + (z * w) ; ::_thesis: verum end; thus for z1, z2 being Complex for v being VECTOR of l holds (z1 + z2) * v = (z1 * v) + (z2 * v) :: according to CLVECT_1:def_3 ::_thesis: ( l is scalar-associative & l is scalar-unital ) proof let z1, z2 be Complex; ::_thesis: for v being VECTOR of l holds (z1 + z2) * v = (z1 * v) + (z2 * v) let v be VECTOR of l; ::_thesis: (z1 + z2) * v = (z1 * v) + (z2 * v) reconsider v1 = v as VECTOR of l0 ; thus (z1 + z2) * v = (z1 + z2) * v1 .= (z1 * v1) + (z2 * v1) by CLVECT_1:def_3 .= (z1 * v) + (z2 * v) ; ::_thesis: verum end; thus for z1, z2 being Complex for v being VECTOR of l holds (z1 * z2) * v = z1 * (z2 * v) :: according to CLVECT_1:def_4 ::_thesis: l is scalar-unital proof let z1, z2 be Complex; ::_thesis: for v being VECTOR of l holds (z1 * z2) * v = z1 * (z2 * v) let v be VECTOR of l; ::_thesis: (z1 * z2) * v = z1 * (z2 * v) reconsider v1 = v as VECTOR of l0 ; thus (z1 * z2) * v = (z1 * z2) * v1 .= z1 * (z2 * v1) by CLVECT_1:def_4 .= z1 * (z2 * v) ; ::_thesis: verum end; let v be VECTOR of l; :: according to CLVECT_1:def_5 ::_thesis: 1r * v = v reconsider v1 = v as VECTOR of l0 ; thus 1r * v = 1r * v1 .= v by CLVECT_1:def_5 ; ::_thesis: verum end; A5: l is right_complementable proof let v be VECTOR of l; :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable reconsider v1 = v as VECTOR of l0 ; consider w1 being VECTOR of l0 such that A6: v1 + w1 = 0. l0 by ALGSTR_0:def_11; reconsider w = w1 as VECTOR of l ; take w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. l thus v + w = 0. l by A6; ::_thesis: verum end; l is right_zeroed proof let v be VECTOR of l; :: according to RLVECT_1:def_4 ::_thesis: v + (0. l) = v reconsider v1 = v as VECTOR of l0 ; thus v + (0. l) = v1 + (0. l0) .= v by RLVECT_1:def_4 ; ::_thesis: verum end; hence l is ComplexLinearSpace by A2, A3, A5, A4; ::_thesis: verum end; 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 ) proof let seq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq . n = 0c ) implies ( seq is summable & Sum seq = 0c ) ) assume A1: for n being Element of NAT holds seq . n = 0c ; ::_thesis: ( seq is summable & Sum seq = 0c ) A2: for m being Element of NAT holds (Partial_Sums seq) . m = 0c proof defpred S1[ Element of NAT ] means seq . $1 = (Partial_Sums seq) . $1; let m be Element of NAT ; ::_thesis: (Partial_Sums seq) . m = 0c A3: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: seq . k = (Partial_Sums seq) . k ; ::_thesis: S1[k + 1] thus seq . (k + 1) = 0c + (seq . (k + 1)) .= (seq . k) + (seq . (k + 1)) by A1 .= (Partial_Sums seq) . (k + 1) by A4, SERIES_1:def_1 ; ::_thesis: verum end; A5: S1[ 0 ] by SERIES_1:def_1; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A3); hence (Partial_Sums seq) . m = seq . m .= 0c by A1 ; ::_thesis: verum end; A6: for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((Partial_Sums seq) . m) - 0c).| < p proof let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((Partial_Sums seq) . m) - 0c).| < p ) assume A7: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((Partial_Sums seq) . m) - 0c).| < p take 0 ; ::_thesis: for m being Element of NAT st 0 <= m holds |.(((Partial_Sums seq) . m) - 0c).| < p let m be Element of NAT ; ::_thesis: ( 0 <= m implies |.(((Partial_Sums seq) . m) - 0c).| < p ) assume 0 <= m ; ::_thesis: |.(((Partial_Sums seq) . m) - 0c).| < p thus |.(((Partial_Sums seq) . m) - 0c).| < p by A2, A7, COMPLEX1:44; ::_thesis: verum end; then A8: Partial_Sums seq is convergent by COMSEQ_2:def_5; then lim (Partial_Sums seq) = 0c by A6, COMSEQ_2:def_6; hence ( seq is summable & Sum seq = 0c ) by A8, COMSEQ_3:def_7, COMSEQ_3:def_8; ::_thesis: verum end; 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;