:: CLOPBAN1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let X be set ;
let Y be non empty set ;
let F be Function of [:COMPLEX ,Y:],Y;
let c be complex number ;
let f be Function of X,Y;
:: original: [;]
redefine func F [;] c,f -> Element of Funcs X,Y;
coherence
F [;] c,f is Element of Funcs X,Y
proof end;
end;

theorem Th1: :: CLOPBAN1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexLinearSpace ex MULT being Function of [:COMPLEX ,(Funcs X,the carrier of Y):], Funcs X,the carrier of Y st
for c being Complex
for f being Element of Funcs X,the carrier of Y
for s being Element of X holds (MULT . [c,f]) . s = c * (f . s)
proof end;

definition
let X be non empty set ;
let Y be ComplexLinearSpace;
func FuncExtMult X,Y -> Function of [:COMPLEX ,(Funcs X,the carrier of Y):], Funcs X,the carrier of Y means :Def1: :: CLOPBAN1:def 1
for c being Complex
for f being Element of Funcs X,the carrier of Y
for x being Element of X holds (it . [c,f]) . x = c * (f . x);
existence
ex b1 being Function of [:COMPLEX ,(Funcs X,the carrier of Y):], Funcs X,the carrier of Y st
for c being Complex
for f being Element of Funcs X,the carrier of Y
for x being Element of X holds (b1 . [c,f]) . x = c * (f . x)
by Th1;
uniqueness
for b1, b2 being Function of [:COMPLEX ,(Funcs X,the carrier of Y):], Funcs X,the carrier of Y st ( for c being Complex
for f being Element of Funcs X,the carrier of Y
for x being Element of X holds (b1 . [c,f]) . x = c * (f . x) ) & ( for c being Complex
for f being Element of Funcs X,the carrier of Y
for x being Element of X holds (b2 . [c,f]) . x = c * (f . x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines FuncExtMult CLOPBAN1:def 1 :
for X being non empty set
for Y being ComplexLinearSpace
for b3 being Function of [:COMPLEX ,(Funcs X,the carrier of Y):], Funcs X,the carrier of Y holds
( b3 = FuncExtMult X,Y iff for c being Complex
for f being Element of Funcs X,the carrier of Y
for x being Element of X holds (b3 . [c,f]) . x = c * (f . x) );

theorem Th2: :: CLOPBAN1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexLinearSpace
for x being Element of X holds (FuncZero X,Y) . x = 0. Y
proof end;

theorem Th3: :: CLOPBAN1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexLinearSpace
for h, f being Element of Funcs X,the carrier of Y
for a being Complex holds
( h = (FuncExtMult X,Y) . [a,f] iff for x being Element of X holds h . x = a * (f . x) )
proof end;

theorem Th4: :: CLOPBAN1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexLinearSpace
for f, g being Element of Funcs X,the carrier of Y holds (FuncAdd X,Y) . f,g = (FuncAdd X,Y) . g,f
proof end;

theorem Th5: :: CLOPBAN1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexLinearSpace
for f, g, h being Element of Funcs X,the carrier of Y holds (FuncAdd X,Y) . f,((FuncAdd X,Y) . g,h) = (FuncAdd X,Y) . ((FuncAdd X,Y) . f,g),h
proof end;

theorem Th6: :: CLOPBAN1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexLinearSpace
for f being Element of Funcs X,the carrier of Y holds (FuncAdd X,Y) . (FuncZero X,Y),f = f
proof end;

theorem Th7: :: CLOPBAN1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexLinearSpace
for f being Element of Funcs X,the carrier of Y holds (FuncAdd X,Y) . f,((FuncExtMult X,Y) . [(- 1r ),f]) = FuncZero X,Y
proof end;

theorem Th8: :: CLOPBAN1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexLinearSpace
for f being Element of Funcs X,the carrier of Y holds (FuncExtMult X,Y) . [1r ,f] = f
proof end;

theorem Th9: :: CLOPBAN1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexLinearSpace
for f being Element of Funcs X,the carrier of Y
for a, b being Complex holds (FuncExtMult X,Y) . [a,((FuncExtMult X,Y) . [b,f])] = (FuncExtMult X,Y) . [(a * b),f]
proof end;

theorem Th10: :: CLOPBAN1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexLinearSpace
for f being Element of Funcs X,the carrier of Y
for a, b being Complex holds (FuncAdd X,Y) . ((FuncExtMult X,Y) . [a,f]),((FuncExtMult X,Y) . [b,f]) = (FuncExtMult X,Y) . [(a + b),f]
proof end;

Lm1: for X being non empty set
for Y being ComplexLinearSpace
for f, g being Element of Funcs X,the carrier of Y
for a being Complex holds (FuncAdd X,Y) . ((FuncExtMult X,Y) . [a,f]),((FuncExtMult X,Y) . [a,g]) = (FuncExtMult X,Y) . [a,((FuncAdd X,Y) . f,g)]
proof end;

theorem Th11: :: CLOPBAN1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexLinearSpace holds CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is ComplexLinearSpace
proof end;

definition
let X be non empty set ;
let Y be ComplexLinearSpace;
func ComplexVectSpace X,Y -> ComplexLinearSpace equals :: CLOPBAN1:def 2
CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #);
coherence
CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is ComplexLinearSpace
by Th11;
end;

:: deftheorem defines ComplexVectSpace CLOPBAN1:def 2 :
for X being non empty set
for Y being ComplexLinearSpace holds ComplexVectSpace X,Y = CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #);

registration
let X be non empty set ;
let Y be ComplexLinearSpace;
cluster ComplexVectSpace X,Y -> strict ;
coherence
ComplexVectSpace X,Y is strict
;
end;

registration
let X be non empty set ;
let Y be ComplexLinearSpace;
cluster ComplexVectSpace X,Y -> strict constituted-Functions ;
coherence
ComplexVectSpace X,Y is constituted-Functions
by MONOID_0:89;
end;

definition
let X be non empty set ;
let Y be ComplexLinearSpace;
let f be VECTOR of (ComplexVectSpace X,Y);
let x be Element of X;
:: original: .
redefine func f . x -> VECTOR of Y;
coherence
f . x is VECTOR of Y
proof end;
end;

theorem Th12: :: CLOPBAN1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexLinearSpace
for f, g, h being VECTOR of (ComplexVectSpace X,Y) holds
( h = f + g iff for x being Element of X holds h . x = (f . x) + (g . x) )
proof end;

theorem Th13: :: CLOPBAN1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexLinearSpace
for f, h being VECTOR of (ComplexVectSpace X,Y)
for c being Complex holds
( h = c * f iff for x being Element of X holds h . x = c * (f . x) )
proof end;

theorem Th14: :: CLOPBAN1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being ComplexLinearSpace holds 0. (ComplexVectSpace X,Y) = X --> (0. Y) by LOPBAN_1:def 3;

definition
let X be non empty CLSStruct ;
let Y be non empty LoopStr ;
let IT be Function of X,Y;
attr IT is additive means :Def3: :: CLOPBAN1:def 3
for x, y being VECTOR of X holds IT . (x + y) = (IT . x) + (IT . y);
end;

:: deftheorem Def3 defines additive CLOPBAN1:def 3 :
for X being non empty CLSStruct
for Y being non empty LoopStr
for IT being Function of X,Y holds
( IT is additive iff for x, y being VECTOR of X holds IT . (x + y) = (IT . x) + (IT . y) );

definition
let X, Y be non empty CLSStruct ;
let IT be Function of X,Y;
attr IT is homogeneous means :Def4: :: CLOPBAN1:def 4
for x being VECTOR of X
for r being Complex holds IT . (r * x) = r * (IT . x);
end;

:: deftheorem Def4 defines homogeneous CLOPBAN1:def 4 :
for X, Y being non empty CLSStruct
for IT being Function of X,Y holds
( IT is homogeneous iff for x being VECTOR of X
for r being Complex holds IT . (r * x) = r * (IT . x) );

registration
let X be non empty CLSStruct ;
let Y be ComplexLinearSpace;
cluster additive homogeneous M4(the carrier of X,the carrier of Y);
existence
ex b1 being Function of X,Y st
( b1 is additive & b1 is homogeneous )
proof end;
end;

definition
let X, Y be ComplexLinearSpace;
mode LinearOperator of X,Y is additive homogeneous Function of X,Y;
end;

definition
let X, Y be ComplexLinearSpace;
func LinearOperators X,Y -> Subset of (ComplexVectSpace the carrier of X,Y) means :Def5: :: CLOPBAN1:def 5
for x being set holds
( x in it iff x is LinearOperator of X,Y );
existence
ex b1 being Subset of (ComplexVectSpace the carrier of X,Y) st
for x being set holds
( x in b1 iff x is LinearOperator of X,Y )
proof end;
uniqueness
for b1, b2 being Subset of (ComplexVectSpace the carrier of X,Y) st ( for x being set holds
( x in b1 iff x is LinearOperator of X,Y ) ) & ( for x being set holds
( x in b2 iff x is LinearOperator of X,Y ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines LinearOperators CLOPBAN1:def 5 :
for X, Y being ComplexLinearSpace
for b3 being Subset of (ComplexVectSpace the carrier of X,Y) holds
( b3 = LinearOperators X,Y iff for x being set holds
( x in b3 iff x is LinearOperator of X,Y ) );

registration
let X, Y be ComplexLinearSpace;
cluster LinearOperators X,Y -> non empty functional ;
coherence
( not LinearOperators X,Y is empty & LinearOperators X,Y is functional )
proof end;
end;

theorem Th15: :: CLOPBAN1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexLinearSpace holds LinearOperators X,Y is lineary-closed
proof end;

theorem Th16: :: CLOPBAN1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexLinearSpace holds CLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)) #) is Subspace of ComplexVectSpace the carrier of X,Y
proof end;

registration
let X, Y be ComplexLinearSpace;
cluster CLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)) #) -> Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ;
coherence
( CLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)) #) is Abelian & CLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)) #) is add-associative & CLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)) #) is right_zeroed & CLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)) #) is right_complementable & CLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)) #) is ComplexLinearSpace-like )
by Th16;
end;

definition
let X, Y be ComplexLinearSpace;
func C_VectorSpace_of_LinearOperators X,Y -> ComplexLinearSpace equals :: CLOPBAN1:def 6
CLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)) #);
coherence
CLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)) #) is ComplexLinearSpace
;
end;

:: deftheorem defines C_VectorSpace_of_LinearOperators CLOPBAN1:def 6 :
for X, Y being ComplexLinearSpace holds C_VectorSpace_of_LinearOperators X,Y = CLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(ComplexVectSpace the carrier of X,Y)) #);

registration
let X, Y be ComplexLinearSpace;
cluster C_VectorSpace_of_LinearOperators X,Y -> strict ;
coherence
C_VectorSpace_of_LinearOperators X,Y is strict
;
end;

registration
let X, Y be ComplexLinearSpace;
cluster C_VectorSpace_of_LinearOperators X,Y -> strict constituted-Functions ;
coherence
C_VectorSpace_of_LinearOperators X,Y is constituted-Functions
by MONOID_0:89;
end;

definition
let X, Y be ComplexLinearSpace;
let f be Element of (C_VectorSpace_of_LinearOperators X,Y);
let v be VECTOR of X;
:: original: .
redefine func f . v -> VECTOR of Y;
coherence
f . v is VECTOR of Y
proof end;
end;

theorem :: CLOPBAN1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th18: :: CLOPBAN1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexLinearSpace
for f, g, h being VECTOR of (C_VectorSpace_of_LinearOperators X,Y) holds
( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )
proof end;

theorem Th19: :: CLOPBAN1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexLinearSpace
for f, h being VECTOR of (C_VectorSpace_of_LinearOperators X,Y)
for c being Complex holds
( h = c * f iff for x being VECTOR of X holds h . x = c * (f . x) )
proof end;

theorem Th20: :: CLOPBAN1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexLinearSpace holds 0. (C_VectorSpace_of_LinearOperators X,Y) = the carrier of X --> (0. Y)
proof end;

theorem Th21: :: CLOPBAN1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexLinearSpace holds the carrier of X --> (0. Y) is LinearOperator of X,Y
proof end;

theorem Th22: :: CLOPBAN1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexNormSpace
for seq being sequence of X
for g being Point of X st seq is convergent & lim seq = g holds
( ||.seq.|| is convergent & lim ||.seq.|| = ||.g.|| )
proof end;

definition
let X, Y be ComplexNormSpace;
let IT be LinearOperator of X,Y;
attr IT is bounded means :Def7: :: CLOPBAN1:def 7
ex K being Real st
( 0 <= K & ( for x being VECTOR of X holds ||.(IT . x).|| <= K * ||.x.|| ) );
end;

:: deftheorem Def7 defines bounded CLOPBAN1:def 7 :
for X, Y being ComplexNormSpace
for IT being LinearOperator of X,Y holds
( IT is bounded iff ex K being Real st
( 0 <= K & ( for x being VECTOR of X holds ||.(IT . x).|| <= K * ||.x.|| ) ) );

theorem Th23: :: CLOPBAN1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexNormSpace
for f being LinearOperator of X,Y st ( for x being VECTOR of X holds f . x = 0. Y ) holds
f is bounded
proof end;

registration
let X, Y be ComplexNormSpace;
cluster bounded M4(the carrier of X,the carrier of Y);
existence
ex b1 being LinearOperator of X,Y st b1 is bounded
proof end;
end;

definition
let X, Y be ComplexNormSpace;
func BoundedLinearOperators X,Y -> Subset of (C_VectorSpace_of_LinearOperators X,Y) means :Def8: :: CLOPBAN1:def 8
for x being set holds
( x in it iff x is bounded LinearOperator of X,Y );
existence
ex b1 being Subset of (C_VectorSpace_of_LinearOperators X,Y) st
for x being set holds
( x in b1 iff x is bounded LinearOperator of X,Y )
proof end;
uniqueness
for b1, b2 being Subset of (C_VectorSpace_of_LinearOperators X,Y) st ( for x being set holds
( x in b1 iff x is bounded LinearOperator of X,Y ) ) & ( for x being set holds
( x in b2 iff x is bounded LinearOperator of X,Y ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines BoundedLinearOperators CLOPBAN1:def 8 :
for X, Y being ComplexNormSpace
for b3 being Subset of (C_VectorSpace_of_LinearOperators X,Y) holds
( b3 = BoundedLinearOperators X,Y iff for x being set holds
( x in b3 iff x is bounded LinearOperator of X,Y ) );

registration
let X, Y be ComplexNormSpace;
cluster BoundedLinearOperators X,Y -> non empty ;
coherence
not BoundedLinearOperators X,Y is empty
proof end;
end;

theorem Th24: :: CLOPBAN1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexNormSpace holds BoundedLinearOperators X,Y is lineary-closed
proof end;

theorem Th25: :: CLOPBAN1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexNormSpace holds CLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)) #) is Subspace of C_VectorSpace_of_LinearOperators X,Y
proof end;

registration
let X, Y be ComplexNormSpace;
cluster CLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)) #) -> Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ;
coherence
( CLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)) #) is Abelian & CLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)) #) is add-associative & CLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)) #) is right_zeroed & CLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)) #) is right_complementable & CLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)) #) is ComplexLinearSpace-like )
by Th25;
end;

definition
let X, Y be ComplexNormSpace;
func C_VectorSpace_of_BoundedLinearOperators X,Y -> ComplexLinearSpace equals :: CLOPBAN1:def 9
CLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)) #);
coherence
CLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)) #) is ComplexLinearSpace
;
end;

:: deftheorem defines C_VectorSpace_of_BoundedLinearOperators CLOPBAN1:def 9 :
for X, Y being ComplexNormSpace holds C_VectorSpace_of_BoundedLinearOperators X,Y = CLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)) #);

registration
let X, Y be ComplexNormSpace;
cluster C_VectorSpace_of_BoundedLinearOperators X,Y -> strict ;
coherence
C_VectorSpace_of_BoundedLinearOperators X,Y is strict
;
end;

registration
let X, Y be ComplexNormSpace;
cluster -> Relation-like Function-like Element of the carrier of (C_VectorSpace_of_BoundedLinearOperators X,Y);
coherence
for b1 being Element of (C_VectorSpace_of_BoundedLinearOperators X,Y) holds
( b1 is Function-like & b1 is Relation-like )
by Def8;
end;

definition
let X, Y be ComplexNormSpace;
let f be Element of (C_VectorSpace_of_BoundedLinearOperators X,Y);
let v be VECTOR of X;
:: original: .
redefine func f . v -> VECTOR of Y;
coherence
f . v is VECTOR of Y
proof end;
end;

theorem :: CLOPBAN1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th27: :: CLOPBAN1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexNormSpace
for f, g, h being VECTOR of (C_VectorSpace_of_BoundedLinearOperators X,Y) holds
( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )
proof end;

theorem Th28: :: CLOPBAN1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexNormSpace
for f, h being VECTOR of (C_VectorSpace_of_BoundedLinearOperators X,Y)
for c being Complex holds
( h = c * f iff for x being VECTOR of X holds h . x = c * (f . x) )
proof end;

theorem Th29: :: CLOPBAN1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexNormSpace holds 0. (C_VectorSpace_of_BoundedLinearOperators X,Y) = the carrier of X --> (0. Y)
proof end;

definition
let X, Y be ComplexNormSpace;
let f be set ;
assume A1: f in BoundedLinearOperators X,Y ;
func modetrans f,X,Y -> bounded LinearOperator of X,Y equals :Def10: :: CLOPBAN1:def 10
f;
coherence
f is bounded LinearOperator of X,Y
by A1, Def8;
end;

:: deftheorem Def10 defines modetrans CLOPBAN1:def 10 :
for X, Y being ComplexNormSpace
for f being set st f in BoundedLinearOperators X,Y holds
modetrans f,X,Y = f;

definition
let X, Y be ComplexNormSpace;
let u be LinearOperator of X,Y;
func PreNorms u -> non empty Subset of REAL equals :: CLOPBAN1:def 11
{ ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } ;
coherence
{ ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } is non empty Subset of REAL
proof end;
end;

:: deftheorem defines PreNorms CLOPBAN1:def 11 :
for X, Y being ComplexNormSpace
for u being LinearOperator of X,Y holds PreNorms u = { ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } ;

theorem Th30: :: CLOPBAN1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexNormSpace
for g being bounded LinearOperator of X,Y holds
( not PreNorms g is empty & PreNorms g is bounded_above )
proof end;

theorem :: CLOPBAN1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexNormSpace
for g being LinearOperator of X,Y holds
( g is bounded iff PreNorms g is bounded_above )
proof end;

theorem Th32: :: CLOPBAN1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexNormSpace ex NORM being Function of BoundedLinearOperators X,Y, REAL st
for f being set st f in BoundedLinearOperators X,Y holds
NORM . f = sup (PreNorms (modetrans f,X,Y))
proof end;

definition
let X, Y be ComplexNormSpace;
func BoundedLinearOperatorsNorm X,Y -> Function of BoundedLinearOperators X,Y, REAL means :Def12: :: CLOPBAN1:def 12
for x being set st x in BoundedLinearOperators X,Y holds
it . x = sup (PreNorms (modetrans x,X,Y));
existence
ex b1 being Function of BoundedLinearOperators X,Y, REAL st
for x being set st x in BoundedLinearOperators X,Y holds
b1 . x = sup (PreNorms (modetrans x,X,Y))
by Th32;
uniqueness
for b1, b2 being Function of BoundedLinearOperators X,Y, REAL st ( for x being set st x in BoundedLinearOperators X,Y holds
b1 . x = sup (PreNorms (modetrans x,X,Y)) ) & ( for x being set st x in BoundedLinearOperators X,Y holds
b2 . x = sup (PreNorms (modetrans x,X,Y)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines BoundedLinearOperatorsNorm CLOPBAN1:def 12 :
for X, Y being ComplexNormSpace
for b3 being Function of BoundedLinearOperators X,Y, REAL holds
( b3 = BoundedLinearOperatorsNorm X,Y iff for x being set st x in BoundedLinearOperators X,Y holds
b3 . x = sup (PreNorms (modetrans x,X,Y)) );

theorem Th33: :: CLOPBAN1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexNormSpace
for f being bounded LinearOperator of X,Y holds modetrans f,X,Y = f
proof end;

theorem Th34: :: CLOPBAN1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexNormSpace
for f being bounded LinearOperator of X,Y holds (BoundedLinearOperatorsNorm X,Y) . f = sup (PreNorms f)
proof end;

definition
let X, Y be ComplexNormSpace;
func C_NormSpace_of_BoundedLinearOperators X,Y -> non empty CNORMSTR equals :: CLOPBAN1:def 13
CNORMSTR(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(BoundedLinearOperatorsNorm X,Y) #);
coherence
CNORMSTR(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(BoundedLinearOperatorsNorm X,Y) #) is non empty CNORMSTR
;
end;

:: deftheorem defines C_NormSpace_of_BoundedLinearOperators CLOPBAN1:def 13 :
for X, Y being ComplexNormSpace holds C_NormSpace_of_BoundedLinearOperators X,Y = CNORMSTR(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(C_VectorSpace_of_LinearOperators X,Y)),(BoundedLinearOperatorsNorm X,Y) #);

theorem Th35: :: CLOPBAN1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexNormSpace holds the carrier of X --> (0. Y) = 0. (C_NormSpace_of_BoundedLinearOperators X,Y)
proof end;

theorem Th36: :: CLOPBAN1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexNormSpace
for f being Point of (C_NormSpace_of_BoundedLinearOperators X,Y)
for g being bounded LinearOperator of X,Y st g = f holds
for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.||
proof end;

theorem Th37: :: CLOPBAN1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexNormSpace
for f being Point of (C_NormSpace_of_BoundedLinearOperators X,Y) holds 0 <= ||.f.||
proof end;

theorem Th38: :: CLOPBAN1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexNormSpace
for f being Point of (C_NormSpace_of_BoundedLinearOperators X,Y) st f = 0. (C_NormSpace_of_BoundedLinearOperators X,Y) holds
0 = ||.f.||
proof end;

registration
let X, Y be ComplexNormSpace;
cluster -> Relation-like Function-like Element of the carrier of (C_NormSpace_of_BoundedLinearOperators X,Y);
coherence
for b1 being Element of (C_NormSpace_of_BoundedLinearOperators X,Y) holds
( b1 is Function-like & b1 is Relation-like )
by Def8;
end;

definition
let X, Y be ComplexNormSpace;
let f be Element of (C_NormSpace_of_BoundedLinearOperators X,Y);
let v be VECTOR of X;
:: original: .
redefine func f . v -> VECTOR of Y;
coherence
f . v is VECTOR of Y
proof end;
end;

theorem Th39: :: CLOPBAN1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexNormSpace
for f, g, h being Point of (C_NormSpace_of_BoundedLinearOperators X,Y) holds
( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )
proof end;

theorem Th40: :: CLOPBAN1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexNormSpace
for f, h being Point of (C_NormSpace_of_BoundedLinearOperators X,Y)
for c being Complex holds
( h = c * f iff for x being VECTOR of X holds h . x = c * (f . x) )
proof end;

theorem Th41: :: CLOPBAN1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexNormSpace
for f, g being Point of (C_NormSpace_of_BoundedLinearOperators X,Y)
for c being Complex holds
( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedLinearOperators X,Y) ) & ( f = 0. (C_NormSpace_of_BoundedLinearOperators X,Y) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
proof end;

theorem Th42: :: CLOPBAN1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexNormSpace holds C_NormSpace_of_BoundedLinearOperators X,Y is ComplexNormSpace-like
proof end;

theorem Th43: :: CLOPBAN1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexNormSpace holds C_NormSpace_of_BoundedLinearOperators X,Y is ComplexNormSpace
proof end;

registration
let X, Y be ComplexNormSpace;
cluster C_NormSpace_of_BoundedLinearOperators X,Y -> non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ComplexNormSpace-like ;
coherence
( C_NormSpace_of_BoundedLinearOperators X,Y is ComplexNormSpace-like & C_NormSpace_of_BoundedLinearOperators X,Y is ComplexLinearSpace-like & C_NormSpace_of_BoundedLinearOperators X,Y is Abelian & C_NormSpace_of_BoundedLinearOperators X,Y is add-associative & C_NormSpace_of_BoundedLinearOperators X,Y is right_zeroed & C_NormSpace_of_BoundedLinearOperators X,Y is right_complementable )
by Th43;
end;

theorem Th44: :: CLOPBAN1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexNormSpace
for f, g, h being Point of (C_NormSpace_of_BoundedLinearOperators X,Y) holds
( h = f - g iff for x being VECTOR of X holds h . x = (f . x) - (g . x) )
proof end;

definition
let X be ComplexNormSpace;
attr X is complete means :Def14: :: CLOPBAN1:def 14
for seq being sequence of X st seq is CCauchy holds
seq is convergent;
end;

:: deftheorem Def14 defines complete CLOPBAN1:def 14 :
for X being ComplexNormSpace holds
( X is complete iff for seq being sequence of X st seq is CCauchy holds
seq is convergent );

registration
cluster complete CNORMSTR ;
existence
ex b1 being ComplexNormSpace st b1 is complete
proof end;
end;

definition
mode ComplexBanachSpace is complete ComplexNormSpace;
end;

Lm2: for e being Real
for seq being Real_Sequence st seq is convergent & ex k being Nat st
for i being Nat st k <= i holds
seq . i <= e holds
lim seq <= e
proof end;

theorem Th45: :: CLOPBAN1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexNormSpace
for seq being sequence of X st seq is convergent holds
( ||.seq.|| is convergent & lim ||.seq.|| = ||.(lim seq).|| )
proof end;

theorem Th46: :: CLOPBAN1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being ComplexNormSpace st Y is complete holds
for seq being sequence of (C_NormSpace_of_BoundedLinearOperators X,Y) st seq is CCauchy holds
seq is convergent
proof end;

theorem Th47: :: CLOPBAN1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexNormSpace
for Y being ComplexBanachSpace holds C_NormSpace_of_BoundedLinearOperators X,Y is ComplexBanachSpace
proof end;

registration
let X be ComplexNormSpace;
let Y be ComplexBanachSpace;
cluster C_NormSpace_of_BoundedLinearOperators X,Y -> non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ComplexNormSpace-like complete ;
coherence
C_NormSpace_of_BoundedLinearOperators X,Y is complete
by Th47;
end;