:: Complex Valued Function's Space :: by Noboru Endou :: :: Received March 18, 2004 :: Copyright (c) 2004-2012 Association of Mizar Users begin definition let A be non empty set ; func ComplexFuncAdd A -> BinOp of (Funcs (A,COMPLEX)) means :Def1: :: CFUNCDOM:def 1 for f, g being Element of Funcs (A,COMPLEX) holds it . (f,g) = addcomplex .: (f,g); existence ex b1 being BinOp of (Funcs (A,COMPLEX)) st for f, g being Element of Funcs (A,COMPLEX) holds b1 . (f,g) = addcomplex .: (f,g) proofend; uniqueness for b1, b2 being BinOp of (Funcs (A,COMPLEX)) st ( for f, g being Element of Funcs (A,COMPLEX) holds b1 . (f,g) = addcomplex .: (f,g) ) & ( for f, g being Element of Funcs (A,COMPLEX) holds b2 . (f,g) = addcomplex .: (f,g) ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines ComplexFuncAdd CFUNCDOM:def_1_:_ for A being non empty set for b2 being BinOp of (Funcs (A,COMPLEX)) holds ( b2 = ComplexFuncAdd A iff for f, g being Element of Funcs (A,COMPLEX) holds b2 . (f,g) = addcomplex .: (f,g) ); definition let A be non empty set ; func ComplexFuncMult A -> BinOp of (Funcs (A,COMPLEX)) means :Def2: :: CFUNCDOM:def 2 for f, g being Element of Funcs (A,COMPLEX) holds it . (f,g) = multcomplex .: (f,g); existence ex b1 being BinOp of (Funcs (A,COMPLEX)) st for f, g being Element of Funcs (A,COMPLEX) holds b1 . (f,g) = multcomplex .: (f,g) proofend; uniqueness for b1, b2 being BinOp of (Funcs (A,COMPLEX)) st ( for f, g being Element of Funcs (A,COMPLEX) holds b1 . (f,g) = multcomplex .: (f,g) ) & ( for f, g being Element of Funcs (A,COMPLEX) holds b2 . (f,g) = multcomplex .: (f,g) ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines ComplexFuncMult CFUNCDOM:def_2_:_ for A being non empty set for b2 being BinOp of (Funcs (A,COMPLEX)) holds ( b2 = ComplexFuncMult A iff for f, g being Element of Funcs (A,COMPLEX) holds b2 . (f,g) = multcomplex .: (f,g) ); definition let A be non empty set ; func ComplexFuncExtMult A -> Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)) means :Def3: :: CFUNCDOM:def 3 for z being Element of COMPLEX for f being Element of Funcs (A,COMPLEX) for x being Element of A holds (it . [z,f]) . x = z * (f . x); existence ex b1 being Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)) st for z being Element of COMPLEX for f being Element of Funcs (A,COMPLEX) for x being Element of A holds (b1 . [z,f]) . x = z * (f . x) proofend; uniqueness for b1, b2 being Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)) st ( for z being Element of COMPLEX for f being Element of Funcs (A,COMPLEX) for x being Element of A holds (b1 . [z,f]) . x = z * (f . x) ) & ( for z being Element of COMPLEX for f being Element of Funcs (A,COMPLEX) for x being Element of A holds (b2 . [z,f]) . x = z * (f . x) ) holds b1 = b2 proofend; end; :: deftheorem Def3 defines ComplexFuncExtMult CFUNCDOM:def_3_:_ for A being non empty set for b2 being Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)) holds ( b2 = ComplexFuncExtMult A iff for z being Element of COMPLEX for f being Element of Funcs (A,COMPLEX) for x being Element of A holds (b2 . [z,f]) . x = z * (f . x) ); definition let A be non empty set ; func ComplexFuncZero A -> Element of Funcs (A,COMPLEX) equals :: CFUNCDOM:def 4 A --> 0; coherence A --> 0 is Element of Funcs (A,COMPLEX) proofend; end; :: deftheorem defines ComplexFuncZero CFUNCDOM:def_4_:_ for A being non empty set holds ComplexFuncZero A = A --> 0; definition let A be non empty set ; func ComplexFuncUnit A -> Element of Funcs (A,COMPLEX) equals :: CFUNCDOM:def 5 A --> 1r; coherence A --> 1r is Element of Funcs (A,COMPLEX) by FUNCT_2:8; end; :: deftheorem defines ComplexFuncUnit CFUNCDOM:def_5_:_ for A being non empty set holds ComplexFuncUnit A = A --> 1r; Lm1: for A, B being non empty set for x being Element of A for f being Function of A,B holds x in dom f proofend; theorem Th1: :: CFUNCDOM:1 for A being non empty set for h, f, g being Element of Funcs (A,COMPLEX) holds ( h = (ComplexFuncAdd A) . (f,g) iff for x being Element of A holds h . x = (f . x) + (g . x) ) proofend; theorem Th2: :: CFUNCDOM:2 for A being non empty set for h, f, g being Element of Funcs (A,COMPLEX) holds ( h = (ComplexFuncMult A) . (f,g) iff for x being Element of A holds h . x = (f . x) * (g . x) ) proofend; theorem :: CFUNCDOM:3 for A being non empty set holds ComplexFuncZero A <> ComplexFuncUnit A proofend; theorem Th4: :: CFUNCDOM:4 for A being non empty set for h, f being Element of Funcs (A,COMPLEX) for a being Element of COMPLEX holds ( h = (ComplexFuncExtMult A) . [a,f] iff for x being Element of A holds h . x = a * (f . x) ) proofend; theorem Th5: :: CFUNCDOM:5 for A being non empty set for f, g being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . (f,g) = (ComplexFuncAdd A) . (g,f) proofend; theorem Th6: :: CFUNCDOM:6 for A being non empty set for f, g, h being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . (f,((ComplexFuncAdd A) . (g,h))) = (ComplexFuncAdd A) . (((ComplexFuncAdd A) . (f,g)),h) proofend; theorem Th7: :: CFUNCDOM:7 for A being non empty set for f, g being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . (f,g) = (ComplexFuncMult A) . (g,f) proofend; theorem Th8: :: CFUNCDOM:8 for A being non empty set for f, g, h being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . (f,((ComplexFuncMult A) . (g,h))) = (ComplexFuncMult A) . (((ComplexFuncMult A) . (f,g)),h) proofend; theorem Th9: :: CFUNCDOM:9 for A being non empty set for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . ((ComplexFuncUnit A),f) = f proofend; theorem Th10: :: CFUNCDOM:10 for A being non empty set for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . ((ComplexFuncZero A),f) = f proofend; theorem Th11: :: CFUNCDOM:11 for A being non empty set for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . (f,((ComplexFuncExtMult A) . [(- 1r),f])) = ComplexFuncZero A proofend; theorem Th12: :: CFUNCDOM:12 for A being non empty set for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncExtMult A) . [1r,f] = f proofend; theorem Th13: :: CFUNCDOM:13 for A being non empty set for f being Element of Funcs (A,COMPLEX) for a, b being Complex holds (ComplexFuncExtMult A) . [a,((ComplexFuncExtMult A) . [b,f])] = (ComplexFuncExtMult A) . [(a * b),f] proofend; theorem Th14: :: CFUNCDOM:14 for A being non empty set for f being Element of Funcs (A,COMPLEX) for a, b being Complex holds (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,f])) = (ComplexFuncExtMult A) . [(a + b),f] proofend; Lm2: for A being non empty set for f, g being Element of Funcs (A,COMPLEX) for a being Complex holds (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [a,g])) = (ComplexFuncExtMult A) . [a,((ComplexFuncAdd A) . (f,g))] proofend; theorem Th15: :: CFUNCDOM:15 for A being non empty set for f, g, h being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . (f,((ComplexFuncAdd A) . (g,h))) = (ComplexFuncAdd A) . (((ComplexFuncMult A) . (f,g)),((ComplexFuncMult A) . (f,h))) proofend; theorem Th16: :: CFUNCDOM:16 for A being non empty set for f, g being Element of Funcs (A,COMPLEX) for a being Element of COMPLEX holds (ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g) = (ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))] proofend; begin theorem Th17: :: CFUNCDOM:17 for x1 being set for A being non empty set ex f, g being Element of Funcs (A,COMPLEX) st ( ( for z being set st z in A holds ( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds ( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) ) proofend; theorem Th18: :: CFUNCDOM:18 for x1, x2 being set for A being non empty set for f, g being Element of Funcs (A,COMPLEX) st x1 in A & x2 in A & x1 <> x2 & ( for z being set st z in A holds ( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds ( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) holds for a, b being Element of COMPLEX st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds ( a = 0c & b = 0c ) proofend; theorem :: CFUNCDOM:19 for x1, x2 being set for A being non empty set st x1 in A & x2 in A & x1 <> x2 holds ex f, g being Element of Funcs (A,COMPLEX) st for a, b being Element of COMPLEX st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds ( a = 0 & b = 0 ) proofend; theorem Th20: :: CFUNCDOM:20 for x1, x2 being set for A being non empty set for f, g being Element of Funcs (A,COMPLEX) st A = {x1,x2} & x1 <> x2 & ( for z being set st z in A holds ( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds ( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) holds for h being Element of Funcs (A,COMPLEX) ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) proofend; theorem :: CFUNCDOM:21 for x1, x2 being set for A being non empty set st A = {x1,x2} & x1 <> x2 holds ex f, g being Element of Funcs (A,COMPLEX) st for h being Element of Funcs (A,COMPLEX) ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) proofend; theorem Th22: :: CFUNCDOM:22 for x1, x2 being set for A being non empty set st A = {x1,x2} & x1 <> x2 holds ex f, g being Element of Funcs (A,COMPLEX) st ( ( for a, b being Element of COMPLEX st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds ( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,COMPLEX) ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) ) ) proofend; definition let A be non empty set ; func ComplexVectSpace A -> non empty strict CLSStruct equals :: CFUNCDOM:def 6 CLSStruct(# (Funcs (A,COMPLEX)),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #); coherence CLSStruct(# (Funcs (A,COMPLEX)),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is non empty strict CLSStruct ; end; :: deftheorem defines ComplexVectSpace CFUNCDOM:def_6_:_ for A being non empty set holds ComplexVectSpace A = CLSStruct(# (Funcs (A,COMPLEX)),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #); registration let A be non empty set ; cluster ComplexVectSpace A -> non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital for non empty strict CLSStruct ; coherence for b1 being non empty strict CLSStruct st b1 = ComplexVectSpace A holds ( b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital ) proofend; end; Lm3: ex A being non empty set ex x1, x2 being set st ( A = {x1,x2} & x1 <> x2 ) proofend; theorem :: CFUNCDOM:23 ex V being strict ComplexLinearSpace ex u, v being VECTOR of V st ( ( for a, b being Element of COMPLEX st (a * u) + (b * v) = 0. V holds ( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Element of COMPLEX st w = (a * u) + (b * v) ) ) proofend; definition let A be non empty set ; func CRing A -> doubleLoopStr equals :: CFUNCDOM:def 7 doubleLoopStr(# (Funcs (A,COMPLEX)),(ComplexFuncAdd A),(ComplexFuncMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #); correctness coherence doubleLoopStr(# (Funcs (A,COMPLEX)),(ComplexFuncAdd A),(ComplexFuncMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #) is doubleLoopStr ; ; end; :: deftheorem defines CRing CFUNCDOM:def_7_:_ for A being non empty set holds CRing A = doubleLoopStr(# (Funcs (A,COMPLEX)),(ComplexFuncAdd A),(ComplexFuncMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #); registration let A be non empty set ; cluster CRing A -> non empty strict ; coherence ( not CRing A is empty & CRing A is strict ) ; end; Lm4: now__::_thesis:_for_A_being_non_empty_set_ for_x,_e_being_Element_of_(CRing_A)_st_e_=_ComplexFuncUnit_A_holds_ (_e_*_x_=_x_&_x_*_e_=_x_) let A be non empty set ; ::_thesis: for x, e being Element of (CRing A) st e = ComplexFuncUnit A holds ( e * x = x & x * e = x ) let x, e be Element of (CRing A); ::_thesis: ( e = ComplexFuncUnit A implies ( e * x = x & x * e = x ) ) assume e = ComplexFuncUnit A ; ::_thesis: ( e * x = x & x * e = x ) hence e * x = x by Th9; ::_thesis: x * e = x hence x * e = x by Th7; ::_thesis: verum end; registration let A be non empty set ; cluster CRing A -> unital ; coherence CRing A is unital proofend; end; theorem Th24: :: CFUNCDOM:24 for A being non empty set for x, y, z being Element of (CRing A) holds ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (CRing A)) = x & x is right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (CRing A)) = x & (1. (CRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) proofend; theorem :: CFUNCDOM:25 for A being non empty set holds CRing A is commutative Ring proofend; definition attrc1 is strict ; struct ComplexAlgebraStr -> doubleLoopStr , CLSStruct ; aggrComplexAlgebraStr(# carrier, multF, addF, Mult, OneF, ZeroF #) -> ComplexAlgebraStr ; end; registration cluster non empty for ComplexAlgebraStr ; existence not for b1 being ComplexAlgebraStr holds b1 is empty proofend; end; definition let A be non empty set ; func CAlgebra A -> strict ComplexAlgebraStr equals :: CFUNCDOM:def 8 ComplexAlgebraStr(# (Funcs (A,COMPLEX)),(ComplexFuncMult A),(ComplexFuncAdd A),(ComplexFuncExtMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #); correctness coherence ComplexAlgebraStr(# (Funcs (A,COMPLEX)),(ComplexFuncMult A),(ComplexFuncAdd A),(ComplexFuncExtMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #) is strict ComplexAlgebraStr ; ; end; :: deftheorem defines CAlgebra CFUNCDOM:def_8_:_ for A being non empty set holds CAlgebra A = ComplexAlgebraStr(# (Funcs (A,COMPLEX)),(ComplexFuncMult A),(ComplexFuncAdd A),(ComplexFuncExtMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #); registration let A be non empty set ; cluster CAlgebra A -> non empty strict ; coherence not CAlgebra A is empty proofend; end; Lm5: now__::_thesis:_for_A_being_non_empty_set_ for_x,_e_being_Element_of_(CAlgebra_A)_st_e_=_ComplexFuncUnit_A_holds_ (_e_*_x_=_x_&_x_*_e_=_x_) let A be non empty set ; ::_thesis: for x, e being Element of (CAlgebra A) st e = ComplexFuncUnit A holds ( e * x = x & x * e = x ) let x, e be Element of (CAlgebra A); ::_thesis: ( e = ComplexFuncUnit A implies ( e * x = x & x * e = x ) ) assume e = ComplexFuncUnit A ; ::_thesis: ( e * x = x & x * e = x ) hence e * x = x by Th9; ::_thesis: x * e = x hence x * e = x by Th7; ::_thesis: verum end; registration let A be non empty set ; cluster CAlgebra A -> unital strict ; coherence CAlgebra A is unital proofend; end; theorem :: CFUNCDOM:26 for A being non empty set for x, y, z being Element of (CAlgebra A) for a, b being Element of COMPLEX holds ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (CAlgebra A)) = x & x is right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (CAlgebra A)) = x & x * (y + z) = (x * y) + (x * z) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) ) proofend; definition let IT be non empty ComplexAlgebraStr ; attrIT is vector-associative means :: CFUNCDOM:def 9 for x, y being Element of IT for a being Element of COMPLEX holds a * (x * y) = (a * x) * y; end; :: deftheorem defines vector-associative CFUNCDOM:def_9_:_ for IT being non empty ComplexAlgebraStr holds ( IT is vector-associative iff for x, y being Element of IT for a being Element of COMPLEX holds a * (x * y) = (a * x) * y ); registration let A be non empty set ; cluster CAlgebra A -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative associative commutative right-distributive right_unital strict vector-associative ; coherence ( CAlgebra A is strict & CAlgebra A is Abelian & CAlgebra A is add-associative & CAlgebra A is right_zeroed & CAlgebra A is right_complementable & CAlgebra A is commutative & CAlgebra A is associative & CAlgebra A is right_unital & CAlgebra A is right-distributive & CAlgebra A is vector-distributive & CAlgebra A is scalar-distributive & CAlgebra A is scalar-associative & CAlgebra A is vector-associative ) proofend; end; registration cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative associative commutative right-distributive right_unital strict vector-associative for ComplexAlgebraStr ; existence ex b1 being non empty ComplexAlgebraStr st ( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is commutative & b1 is associative & b1 is right_unital & b1 is right-distributive & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is vector-associative ) proofend; end; definition mode ComplexAlgebra is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative associative commutative right-distributive right_unital vector-associative ComplexAlgebraStr ; end; theorem :: CFUNCDOM:27 for A being non empty set holds CAlgebra A is ComplexAlgebra ; theorem :: CFUNCDOM:28 for A being non empty set holds 1. (CRing A) = ComplexFuncUnit A ; theorem :: CFUNCDOM:29 for A being non empty set holds 1. (CAlgebra A) = ComplexFuncUnit A ;