:: Complex Valued Function's Space
:: by Noboru Endou
::
:: Copyright (c) 2004-2019 Association of Mizar Users

definition
let A be 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)
proof end;
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
proof end;
end;

:: deftheorem Def1 defines ComplexFuncAdd CFUNCDOM:def 1 :
for A being 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) );

registration
let A be set ;
coherence ;
end;

definition
let A be 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)
proof end;
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
proof end;
end;

:: deftheorem Def2 defines ComplexFuncMult CFUNCDOM:def 2 :
for A being 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) );

registration
let A be set ;
coherence ;
end;

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 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 Complex
for f being Element of Funcs (A,COMPLEX)
for x being Element of A holds (b1 . [z,f]) . x = z * (f . x)
proof end;
uniqueness
for b1, b2 being Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)) st ( for z being 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 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
proof end;
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 Complex
for f being Element of Funcs (A,COMPLEX)
for x being Element of A holds (b2 . [z,f]) . x = z * (f . x) );

registration
let A be non empty set ;
coherence ;
end;

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)
proof end;
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

proof end;

theorem Th1: :: CFUNCDOM:1
for A being non empty set
for f, g, h being Element of Funcs (A,COMPLEX) holds
( h = () . (f,g) iff for x being Element of A holds h . x = (f . x) + (g . x) )
proof end;

theorem Th2: :: CFUNCDOM:2
for A being non empty set
for f, g, h being Element of Funcs (A,COMPLEX) holds
( h = () . (f,g) iff for x being Element of A holds h . x = (f . x) * (g . x) )
proof end;

theorem :: CFUNCDOM:3
for A being non empty set holds ComplexFuncZero A <> ComplexFuncUnit A
proof end;

theorem Th4: :: CFUNCDOM:4
for A being non empty set
for f, h being Element of Funcs (A,COMPLEX)
for a being Complex holds
( h = . [a,f] iff for x being Element of A holds h . x = a * (f . x) )
proof end;

theorem Th5: :: CFUNCDOM:5
for A being non empty set
for f, g being Element of Funcs (A,COMPLEX) holds () . (f,g) = () . (g,f)
proof end;

theorem Th6: :: CFUNCDOM:6
for A being non empty set
for f, g, h being Element of Funcs (A,COMPLEX) holds () . (f,(() . (g,h))) = () . ((() . (f,g)),h)
proof end;

theorem Th7: :: CFUNCDOM:7
for A being non empty set
for f, g being Element of Funcs (A,COMPLEX) holds () . (f,g) = () . (g,f)
proof end;

theorem Th8: :: CFUNCDOM:8
for A being non empty set
for f, g, h being Element of Funcs (A,COMPLEX) holds () . (f,(() . (g,h))) = () . ((() . (f,g)),h)
proof end;

theorem Th9: :: CFUNCDOM:9
for A being non empty set
for f being Element of Funcs (A,COMPLEX) holds () . ((),f) = f
proof end;

theorem Th10: :: CFUNCDOM:10
for A being non empty set
for f being Element of Funcs (A,COMPLEX) holds () . ((),f) = f
proof end;

theorem Th11: :: CFUNCDOM:11
for A being non empty set
for f being Element of Funcs (A,COMPLEX) holds () . (f,( . [(),f])) = ComplexFuncZero A
proof end;

theorem Th12: :: CFUNCDOM:12
for A being non empty set
for f being Element of Funcs (A,COMPLEX) holds . [1r,f] = f
proof end;

theorem Th13: :: CFUNCDOM:13
for A being non empty set
for f being Element of Funcs (A,COMPLEX)
for a, b being Complex holds . [a,( . [b,f])] = . [(a * b),f]
proof end;

theorem Th14: :: CFUNCDOM:14
for A being non empty set
for f being Element of Funcs (A,COMPLEX)
for a, b being Complex holds () . (( . [a,f]),( . [b,f])) = . [(a + b),f]
proof end;

Lm2: for A being non empty set
for f, g being Element of Funcs (A,COMPLEX)
for a being Complex holds () . (( . [a,f]),( . [a,g])) = . [a,(() . (f,g))]

proof end;

theorem Th15: :: CFUNCDOM:15
for A being non empty set
for f, g, h being Element of Funcs (A,COMPLEX) holds () . (f,(() . (g,h))) = () . ((() . (f,g)),(() . (f,h)))
proof end;

theorem Th16: :: CFUNCDOM:16
for A being non empty set
for f, g being Element of Funcs (A,COMPLEX)
for a being Complex holds () . (( . [a,f]),g) = . [a,(() . (f,g))]
proof end;

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 ) ) ) )
proof end;

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 Complex st () . (( . [a,f]),( . [b,g])) = ComplexFuncZero A holds
( a = 0c & b = 0c )
proof end;

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 Complex st () . (( . [a,f]),( . [b,g])) = ComplexFuncZero A holds
( a = 0 & b = 0 )
proof end;

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 Complex st h = () . (( . [a,f]),( . [b,g]))
proof end;

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 Complex st h = () . (( . [a,f]),( . [b,g]))
proof end;

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 Complex st () . (( . [a,f]),( . [b,g])) = ComplexFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,COMPLEX) ex a, b being Complex st h = () . (( . [a,f]),( . [b,g])) ) )
proof end;

definition
let A be non empty set ;
func ComplexVectSpace A -> non empty strict CLSStruct equals :: CFUNCDOM:def 6
CLSStruct(# (Funcs (A,COMPLEX)),(),(), #);
coherence
CLSStruct(# (Funcs (A,COMPLEX)),(),(), #) 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)),(),(), #);

registration
let A be non empty set ;
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 )
proof end;
end;

Lm3: ex A being non empty set ex x1, x2 being set st
( A = {x1,x2} & x1 <> x2 )

proof end;

theorem :: CFUNCDOM:23
ex V being strict ComplexLinearSpace ex u, v being VECTOR of V st
( ( for a, b being Complex st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Complex st w = (a * u) + (b * v) ) )
proof end;

definition
let A be non empty set ;
func CRing A -> doubleLoopStr equals :: CFUNCDOM:def 7
doubleLoopStr(# (Funcs (A,COMPLEX)),(),(),(),() #);
correctness
coherence
doubleLoopStr(# (Funcs (A,COMPLEX)),(),(),(),() #) is doubleLoopStr
;
;
end;

:: deftheorem defines CRing CFUNCDOM:def 7 :
for A being non empty set holds CRing A = doubleLoopStr(# (Funcs (A,COMPLEX)),(),(),(),() #);

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 () st e = ComplexFuncUnit A holds
( e * x = x & x * e = x )
let A be non empty set ; :: thesis: for x, e being Element of () st e = ComplexFuncUnit A holds
( e * x = x & x * e = x )

let x, e be Element of (); :: 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 ;
coherence
CRing A is unital
proof end;
end;

theorem Th24: :: CFUNCDOM:24
for A being non empty set
for x, y, z being Element of () holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. ()) = x & x is right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. ()) = x & (1. ()) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
proof end;

theorem :: CFUNCDOM:25
for A being non empty set holds CRing A is commutative Ring
proof end;

definition end;

registration
existence
not for b1 being ComplexAlgebraStr holds b1 is empty
proof end;
end;

definition
let A be non empty set ;
func CAlgebra A -> strict ComplexAlgebraStr equals :: CFUNCDOM:def 8
ComplexAlgebraStr(# (Funcs (A,COMPLEX)),(),(),,(),() #);
correctness
coherence
ComplexAlgebraStr(# (Funcs (A,COMPLEX)),(),(),,(),() #) is strict ComplexAlgebraStr
;
;
end;

:: deftheorem defines CAlgebra CFUNCDOM:def 8 :
for A being non empty set holds CAlgebra A = ComplexAlgebraStr(# (Funcs (A,COMPLEX)),(),(),,(),() #);

registration
let A be non empty set ;
cluster CAlgebra A -> non empty strict ;
coherence
not CAlgebra A is empty
;
end;

Lm5: now :: thesis: for A being non empty set
for x, e being Element of () st e = ComplexFuncUnit A holds
( e * x = x & x * e = x )
let A be non empty set ; :: thesis: for x, e being Element of () st e = ComplexFuncUnit A holds
( e * x = x & x * e = x )

let x, e be Element of (); :: 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 ;
coherence
proof end;
end;

theorem :: CFUNCDOM:26
for A being non empty set
for x, y, z being Element of ()
for a, b being Complex holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. ()) = x & x is right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. ()) = 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) )
proof end;

definition
let IT be non empty ComplexAlgebraStr ;
attr IT is vector-associative means :: CFUNCDOM:def 9
for x, y being Element of IT
for a being 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 Complex holds a * (x * y) = (a * x) * y );

registration
let A be non empty set ;
coherence
proof end;
end;

registration
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 )
proof end;
end;

definition 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. () = ComplexFuncUnit A ;

theorem :: CFUNCDOM:29
for A being non empty set holds 1. () = ComplexFuncUnit A ;