LOPBAN

:: LOPBAN_2 semantic presentation

begin

theorem :: LOPBAN_2:2

definition

end;

definition

end;

definition

func g * f -> ( ( ) ( ) Element of BoundedLinearOperators (X : ( ( ) ( ) AlgebraStr ) ,X : ( ( ) ( ) AlgebraStr ) ) : ( ( ) ( ) Element of bool the carrier of (R_VectorSpace_of_LinearOperators (X : ( ( ) ( ) AlgebraStr ) ,X : ( ( ) ( ) AlgebraStr ) )) : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RLSStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) equals :: LOPBAN_2:def 2
(modetrans (g : ( ( Function-like V29([:X : ( ( ) ( ) AlgebraStr ) ,X : ( ( ) ( ) AlgebraStr ) :] : ( ( ) ( V15() ) set ) ,X : ( ( ) ( ) AlgebraStr ) ) ) ( V15() Function-like V29([:X : ( ( ) ( ) AlgebraStr ) ,X : ( ( ) ( ) AlgebraStr ) :] : ( ( ) ( V15() ) set ) ,X : ( ( ) ( ) AlgebraStr ) ) ) Element of bool [:[:X : ( ( ) ( ) AlgebraStr ) ,X : ( ( ) ( ) AlgebraStr ) :] : ( ( ) ( V15() ) set ) ,X : ( ( ) ( ) AlgebraStr ) :] : ( ( ) ( V15() ) set ) : ( ( ) ( ) set ) ) ,X : ( ( ) ( ) AlgebraStr ) ,X : ( ( ) ( ) AlgebraStr ) )) : ( ( Function-like V29( the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) , the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) ) V165(X : ( ( ) ( ) AlgebraStr ) ,X : ( ( ) ( ) AlgebraStr ) ) V166(X : ( ( ) ( ) AlgebraStr ) ,X : ( ( ) ( ) AlgebraStr ) ) Lipschitzian ) ( non empty V15() Function-like V25( the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) ) V29( the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) , the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) ) V165(X : ( ( ) ( ) AlgebraStr ) ,X : ( ( ) ( ) AlgebraStr ) ) V166(X : ( ( ) ( ) AlgebraStr ) ,X : ( ( ) ( ) AlgebraStr ) ) Lipschitzian ) Element of bool [: the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) , the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( V15() ) set ) : ( ( ) ( ) set ) ) * (modetrans (f : ( ( ) ( ) VectSpStr over X : ( ( ) ( ) AlgebraStr ) ) ,X : ( ( ) ( ) AlgebraStr ) ,X : ( ( ) ( ) AlgebraStr ) )) : ( ( Function-like V29( the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) , the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) ) V165(X : ( ( ) ( ) AlgebraStr ) ,X : ( ( ) ( ) AlgebraStr ) ) V166(X : ( ( ) ( ) AlgebraStr ) ,X : ( ( ) ( ) AlgebraStr ) ) Lipschitzian ) ( non empty V15() Function-like V25( the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) ) V29( the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) , the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) ) V165(X : ( ( ) ( ) AlgebraStr ) ,X : ( ( ) ( ) AlgebraStr ) ) V166(X : ( ( ) ( ) AlgebraStr ) ,X : ( ( ) ( ) AlgebraStr ) ) Lipschitzian ) Element of bool [: the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) , the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( V15() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like V29( the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) , the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) ) V165(X : ( ( ) ( ) AlgebraStr ) ,X : ( ( ) ( ) AlgebraStr ) ) V166(X : ( ( ) ( ) AlgebraStr ) ,X : ( ( ) ( ) AlgebraStr ) ) Lipschitzian ) ( non empty V15() Function-like V25( the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) ) V29( the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) , the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) ) V165(X : ( ( ) ( ) AlgebraStr ) ,X : ( ( ) ( ) AlgebraStr ) ) V166(X : ( ( ) ( ) AlgebraStr ) ,X : ( ( ) ( ) AlgebraStr ) ) Lipschitzian ) LinearOperator of X : ( ( ) ( ) AlgebraStr ) ,X : ( ( ) ( ) AlgebraStr ) ) ;

end;

definition

end;

definition

end;

theorem :: LOPBAN_2:3

definition

func FuncUnit X -> ( ( ) ( ) Element of BoundedLinearOperators (X : ( ( ) ( ) AlgebraStr ) ,X : ( ( ) ( ) AlgebraStr ) ) : ( ( ) ( ) Element of bool the carrier of (R_VectorSpace_of_LinearOperators (X : ( ( ) ( ) AlgebraStr ) ,X : ( ( ) ( ) AlgebraStr ) )) : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RLSStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) equals :: LOPBAN_2:def 5
id the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) : ( ( V25( the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) ) ) ( V15() V18( the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) ) V19( the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) ) Function-like one-to-one V25( the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) ) V29( the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) , the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) ) ) Element of bool [: the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) , the carrier of X : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) :] : ( ( ) ( V15() ) set ) : ( ( ) ( ) set ) ) ;

end;

theorem :: LOPBAN_2:4

theorem :: LOPBAN_2:5

theorem :: LOPBAN_2:6

theorem :: LOPBAN_2:7

theorem :: LOPBAN_2:8

theorem :: LOPBAN_2:9

theorem :: LOPBAN_2:10

theorem :: LOPBAN_2:11

theorem :: LOPBAN_2:12

definition

end;

registration

cluster Ring_of_BoundedLinearOperators X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like ) NORMSTR ) : ( ( ) ( ) doubleLoopStr ) -> non empty strict ;

end;

registration

end;

theorem :: LOPBAN_2:13

theorem :: LOPBAN_2:14

registration

end;

definition

end;

registration

cluster R_Algebra_of_BoundedLinearOperators X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like ) NORMSTR ) : ( ( ) ( ) AlgebraStr ) -> non empty strict ;

end;

registration

end;

theorem :: LOPBAN_2:15

definition end;

registration

end;

theorem :: LOPBAN_2:16

registration end;

registration

cluster non empty non trivial left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like complete for ( ( ) ( ) NORMSTR ) ;

end;

theorem :: LOPBAN_2:17

theorem :: LOPBAN_2:18

definition

attr c₁ is strict ;
struct Normed_AlgebraStr -> ( ( ) ( ) AlgebraStr ) , ( ( ) ( ) NORMSTR ) ;
aggr Normed_AlgebraStr(# carrier, multF, addF, Mult, OneF, ZeroF, normF #) -> ( ( strict ) ( strict ) Normed_AlgebraStr ) ;

end;

registration

cluster non empty for ( ( ) ( ) Normed_AlgebraStr ) ;

end;

definition

end;

registration

end;

registration

end;

theorem :: LOPBAN_2:19

theorem :: LOPBAN_2:20

registration

end;

definition end;

registration

cluster R_Normed_Algebra_of_BoundedLinearOperators X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty unital strict ) Normed_AlgebraStr ) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative discerning reflexive RealNormSpace-like associative right-distributive right_unital ;

end;

definition

let X be ( ( non empty ) ( non empty ) Normed_AlgebraStr ) ;

attr X is Banach_Algebra-like_1 means :: LOPBAN_2:def 9
for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds ||.(x : ( ( ) ( V11() real ext-real ) Real) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V46() V51() V52() V53() V57() ) set ) ) <= ||.x : ( ( ) ( V11() real ext-real ) Real) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V46() V51() V52() V53() V57() ) set ) ) * ||.y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V46() V51() V52() V53() V57() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V46() V51() V52() V53() V57() ) set ) ) ;

attr X is Banach_Algebra-like_2 means :: LOPBAN_2:def 10
||.(1. X : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V46() V51() V52() V53() V57() ) set ) ) = 1 : ( ( ) ( non empty natural V11() real V13() V32() ext-real positive non negative V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V51() V52() V53() V54() V55() V56() V57() ) Element of bool REAL : ( ( ) ( non empty V46() V51() V52() V53() V57() ) set ) : ( ( ) ( ) set ) ) ) ;

attr X is Banach_Algebra-like_3 means :: LOPBAN_2:def 11
for a being ( ( ) ( V11() real ext-real ) Real)
for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( V11() real ext-real ) Real) * (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * (a : ( ( ) ( V11() real ext-real ) Real) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

end;

definition