:: LOPBAN_2 semantic presentation

definition

let c₁ be non empty set ;
let c₂, c₃ be Element of Funcs c₁,c₁;
redefine func * as c₃ * c₂ -> Element of Funcs a₁,a₁;
coherence

proof end;

end;

theorem Th1: :: LOPBAN_2:1

for b₁, b₂, b₃ being RealLinearSpace
for b₄ being LinearOperator of b₁,b₂
for b₅ being LinearOperator of b₂,b₃ holds b₅ * b₄ is LinearOperator of b₁,b₃

proof end;

theorem Th2: :: LOPBAN_2:2

for b₁, b₂, b₃ being RealNormSpace
for b₄ being bounded LinearOperator of b₁,b₂
for b₅ being bounded LinearOperator of b₂,b₃ holds
( b₅ * b₄ is bounded LinearOperator of b₁,b₃ & ( for b₆ being VECTOR of b₁ holds
( ||.((b₅ * b₄) . b₆).|| <= (((BoundedLinearOperatorsNorm b₂,b₃) . b₅) * ((BoundedLinearOperatorsNorm b₁,b₂) . b₄)) * ||.b₆.|| & (BoundedLinearOperatorsNorm b₁,b₃) . (b₅ * b₄) <= ((BoundedLinearOperatorsNorm b₂,b₃) . b₅) * ((BoundedLinearOperatorsNorm b₁,b₂) . b₄) ) ) )

proof end;

definition

let c₁ be RealNormSpace;
let c₂, c₃ be bounded LinearOperator of c₁,c₁;
redefine func * as c₃ * c₂ -> bounded LinearOperator of a₁,a₁;
correctness by Th2;

end;

definition

let c₁ be RealNormSpace;
let c₂, c₃ be Element of BoundedLinearOperators c₁,c₁;
func c₂ + c₃ -> Element of BoundedLinearOperators a₁,a₁ equals :: LOPBAN_2:def 1
(Add_ (BoundedLinearOperators a₁,a₁),(R_VectorSpace_of_LinearOperators a₁,a₁)) . a₂,a₃;
correctness ;

end;

:: deftheorem Def1 defines + LOPBAN_2:def 1 :

definition

let c₁ be RealNormSpace;
let c₂, c₃ be Element of BoundedLinearOperators c₁,c₁;
func c₃ * c₂ -> Element of BoundedLinearOperators a₁,a₁ equals :: LOPBAN_2:def 2
(modetrans a₃,a₁,a₁) * (modetrans a₂,a₁,a₁);
correctness by LOPBAN_1:def 10;

end;

:: deftheorem Def2 defines * LOPBAN_2:def 2 :

definition

let c₁ be RealNormSpace;
let c₂ be Element of BoundedLinearOperators c₁,c₁;
let c₃ be Real;
func c₃ * c₂ -> Element of BoundedLinearOperators a₁,a₁ equals :: LOPBAN_2:def 3
(Mult_ (BoundedLinearOperators a₁,a₁),(R_VectorSpace_of_LinearOperators a₁,a₁)) . a₃,a₂;
correctness ;

end;

:: deftheorem Def3 defines * LOPBAN_2:def 3 :

definition

let c₁ be RealNormSpace;
func FuncMult c₁ -> BinOp of BoundedLinearOperators a₁,a₁ means :Def4: :: LOPBAN_2:def 4
for b₁, b₂ being Element of BoundedLinearOperators a₁,a₁ holds a₂ . b₁,b₂ = b₁ * b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines FuncMult LOPBAN_2:def 4 :

theorem Th3: :: LOPBAN_2:3

for b₁ being RealNormSpace holds id the carrier of b₁ is bounded LinearOperator of b₁,b₁

proof end;

definition

let c₁ be RealNormSpace;
func FuncUnit c₁ -> Element of BoundedLinearOperators a₁,a₁ equals :: LOPBAN_2:def 5
id the carrier of a₁;
coherence

proof end;

end;

:: deftheorem Def5 defines FuncUnit LOPBAN_2:def 5 :

theorem Th4: :: LOPBAN_2:4

for b₁ being RealNormSpace
for b₂, b₃, b₄ being bounded LinearOperator of b₁,b₁ holds
( b₄ = b₂ * b₃ iff for b₅ being VECTOR of b₁ holds b₄ . b₅ = b₂ . (b₃ . b₅) )

proof end;

theorem Th5: :: LOPBAN_2:5

for b₁ being RealNormSpace
for b₂, b₃, b₄ being bounded LinearOperator of b₁,b₁ holds b₂ * (b₃ * b₄) = (b₂ * b₃) * b₄

proof end;

theorem Th6: :: LOPBAN_2:6

for b₁ being RealNormSpace
for b₂ being bounded LinearOperator of b₁,b₁ holds
( b₂ * (id the carrier of b₁) = b₂ & (id the carrier of b₁) * b₂ = b₂ )

proof end;

theorem Th7: :: LOPBAN_2:7

for b₁ being RealNormSpace
for b₂, b₃, b₄ being Element of BoundedLinearOperators b₁,b₁ holds b₂ * (b₃ * b₄) = (b₂ * b₃) * b₄

proof end;

theorem Th8: :: LOPBAN_2:8

for b₁ being RealNormSpace
for b₂ being Element of BoundedLinearOperators b₁,b₁ holds
( b₂ * (FuncUnit b₁) = b₂ & (FuncUnit b₁) * b₂ = b₂ )

proof end;

theorem Th9: :: LOPBAN_2:9

for b₁ being RealNormSpace
for b₂, b₃, b₄ being Element of BoundedLinearOperators b₁,b₁ holds b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄)

proof end;

theorem Th10: :: LOPBAN_2:10

for b₁ being RealNormSpace
for b₂, b₃, b₄ being Element of BoundedLinearOperators b₁,b₁ holds (b₃ + b₄) * b₂ = (b₃ * b₂) + (b₄ * b₂)

proof end;

theorem Th11: :: LOPBAN_2:11

for b₁ being RealNormSpace
for b₂, b₃ being Element of BoundedLinearOperators b₁,b₁
for b₄, b₅ being Real holds (b₄ * b₅) * (b₂ * b₃) = (b₄ * b₂) * (b₅ * b₃)

proof end;

theorem Th12: :: LOPBAN_2:12

for b₁ being RealNormSpace
for b₂, b₃ being Element of BoundedLinearOperators b₁,b₁
for b₄ being Real holds b₄ * (b₂ * b₃) = (b₄ * b₂) * b₃

proof end;

definition

let c₁ be RealNormSpace;
func Ring_of_BoundedLinearOperators c₁ -> doubleLoopStr equals :: LOPBAN_2:def 6
doubleLoopStr(# (BoundedLinearOperators a₁,a₁),(Add_ (BoundedLinearOperators a₁,a₁),(R_VectorSpace_of_LinearOperators a₁,a₁)),(FuncMult a₁),(FuncUnit a₁),(Zero_ (BoundedLinearOperators a₁,a₁),(R_VectorSpace_of_LinearOperators a₁,a₁)) #);
correctness ;

end;

:: deftheorem Def6 defines Ring_of_BoundedLinearOperators LOPBAN_2:def 6 :

registration

let c₁ be RealNormSpace;
cluster Ring_of_BoundedLinearOperators a₁ -> non empty strict ;
coherence

proof end;

end;

E14: now

let c₁ be RealNormSpace;
set c₂ = Ring_of_BoundedLinearOperators c₁;
let c₃, c₄ be Element of (Ring_of_BoundedLinearOperators c₁);
assume E15: c₄ = FuncUnit c₁ ;
reconsider c₅ = c₃ as Element of BoundedLinearOperators c₁,c₁ ;
thus c₃ * c₄ = the mult of (Ring_of_BoundedLinearOperators c₁) . c₃,c₄
.= (FuncMult c₁) . c₅,(FuncUnit c₁) by E15
.= c₅ * (FuncUnit c₁) by Def4
.= c₃ by Th8 ;
thus c₄ * c₃ = the mult of (Ring_of_BoundedLinearOperators c₁) . c₄,c₃
.= (FuncMult c₁) . (FuncUnit c₁),c₅ by E15
.= (FuncUnit c₁) * c₅ by Def4
.= c₃ by Th8 ;

end;

registration

let c₁ be RealNormSpace;
cluster Ring_of_BoundedLinearOperators a₁ -> non empty unital strict ;
coherence

proof end;

end;

E15: now

let c₁ be RealNormSpace;
set c₂ = Ring_of_BoundedLinearOperators c₁;
reconsider c₃ = FuncUnit c₁ as Element of (Ring_of_BoundedLinearOperators c₁) ;
for b₁ being Element of (Ring_of_BoundedLinearOperators c₁) holds
( b₁ * c₃ = b₁ & c₃ * b₁ = b₁ ) by Lemma14;
hence 1. (Ring_of_BoundedLinearOperators c₁) = FuncUnit c₁ by GROUP_1:def 5;

end;

theorem Th13: :: LOPBAN_2:13

for b₁ being RealNormSpace
for b₂, b₃, b₄ being Element of (Ring_of_BoundedLinearOperators b₁) holds
( b₂ + b₃ = b₃ + b₂ & (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄) & b₂ + (0. (Ring_of_BoundedLinearOperators b₁)) = b₂ & ex b₅ being Element of (Ring_of_BoundedLinearOperators b₁) st b₂ + b₅ = 0. (Ring_of_BoundedLinearOperators b₁) & (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) & b₂ * (1. (Ring_of_BoundedLinearOperators b₁)) = b₂ & (1. (Ring_of_BoundedLinearOperators b₁)) * b₂ = b₂ & b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄) & (b₃ + b₄) * b₂ = (b₃ * b₂) + (b₄ * b₂) )

proof end;

theorem Th14: :: LOPBAN_2:14

for b₁ being RealNormSpace holds Ring_of_BoundedLinearOperators b₁ is Ring

proof end;

registration

let c₁ be RealNormSpace;
cluster Ring_of_BoundedLinearOperators a₁ -> non empty Abelian add-associative right_zeroed right_complementable unital associative strict right_unital distributive left_unital ;
coherence by Th14;

end;

definition

let c₁ be RealNormSpace;
func R_Algebra_of_BoundedLinearOperators c₁ -> AlgebraStr equals :: LOPBAN_2:def 7
AlgebraStr(# (BoundedLinearOperators a₁,a₁),(FuncMult a₁),(Add_ (BoundedLinearOperators a₁,a₁),(R_VectorSpace_of_LinearOperators a₁,a₁)),(Mult_ (BoundedLinearOperators a₁,a₁),(R_VectorSpace_of_LinearOperators a₁,a₁)),(FuncUnit a₁),(Zero_ (BoundedLinearOperators a₁,a₁),(R_VectorSpace_of_LinearOperators a₁,a₁)) #);
correctness ;

end;

:: deftheorem Def7 defines R_Algebra_of_BoundedLinearOperators LOPBAN_2:def 7 :

registration

let c₁ be RealNormSpace;
cluster R_Algebra_of_BoundedLinearOperators a₁ -> non empty strict ;
coherence

proof end;

end;

E18: now

let c₁ be RealNormSpace;
set c₂ = R_Algebra_of_BoundedLinearOperators c₁;
let c₃, c₄ be Element of (R_Algebra_of_BoundedLinearOperators c₁);
assume E19: c₄ = FuncUnit c₁ ;
reconsider c₅ = c₃ as Element of BoundedLinearOperators c₁,c₁ ;
thus c₃ * c₄ = the mult of (R_Algebra_of_BoundedLinearOperators c₁) . c₃,c₄
.= (FuncMult c₁) . c₅,(FuncUnit c₁) by E19
.= c₅ * (FuncUnit c₁) by Def4
.= c₃ by Th8 ;
thus c₄ * c₃ = the mult of (R_Algebra_of_BoundedLinearOperators c₁) . c₄,c₃
.= (FuncMult c₁) . (FuncUnit c₁),c₅ by E19
.= (FuncUnit c₁) * c₅ by Def4
.= c₃ by Th8 ;

end;

registration

let c₁ be RealNormSpace;
cluster R_Algebra_of_BoundedLinearOperators a₁ -> non empty unital strict ;
coherence

proof end;

end;

E19: now

let c₁ be RealNormSpace;
set c₂ = R_Algebra_of_BoundedLinearOperators c₁;
reconsider c₃ = FuncUnit c₁ as Element of (R_Algebra_of_BoundedLinearOperators c₁) ;
for b₁ being Element of (R_Algebra_of_BoundedLinearOperators c₁) holds
( b₁ * c₃ = b₁ & c₃ * b₁ = b₁ ) by Lemma18;
hence 1. (R_Algebra_of_BoundedLinearOperators c₁) = FuncUnit c₁ by GROUP_1:def 5;

end;

theorem Th15: :: LOPBAN_2:15

for b₁ being RealNormSpace
for b₂, b₃, b₄ being Element of (R_Algebra_of_BoundedLinearOperators b₁)
for b₅, b₆ being Real holds
( b₂ + b₃ = b₃ + b₂ & (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄) & b₂ + (0. (R_Algebra_of_BoundedLinearOperators b₁)) = b₂ & ex b₇ being Element of (R_Algebra_of_BoundedLinearOperators b₁) st b₂ + b₇ = 0. (R_Algebra_of_BoundedLinearOperators b₁) & (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) & b₂ * (1. (R_Algebra_of_BoundedLinearOperators b₁)) = b₂ & (1. (R_Algebra_of_BoundedLinearOperators b₁)) * b₂ = b₂ & b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄) & (b₃ + b₄) * b₂ = (b₃ * b₂) + (b₄ * b₂) & b₅ * (b₂ * b₃) = (b₅ * b₂) * b₃ & b₅ * (b₂ + b₃) = (b₅ * b₂) + (b₅ * b₃) & (b₅ + b₆) * b₂ = (b₅ * b₂) + (b₆ * b₂) & (b₅ * b₆) * b₂ = b₅ * (b₆ * b₂) & (b₅ * b₆) * (b₂ * b₃) = (b₅ * b₂) * (b₆ * b₃) )

proof end;

definition

mode BLAlgebra is non empty Abelian add-associative right_zeroed right_complementable associative Algebra-like AlgebraStr ;

end;

theorem Th16: :: LOPBAN_2:16

for b₁ being RealNormSpace holds R_Algebra_of_BoundedLinearOperators b₁ is BLAlgebra

proof end;

registration

cluster l1_Space -> complete ;
coherence

proof end;

end;

registration

cluster l1_Space -> non trivial complete ;
coherence

proof end;

end;

registration

cluster non trivial NORMSTR ;
existence

proof end;

end;

theorem Th17: :: LOPBAN_2:17

for b₁ being non trivial RealNormSpace ex b₂ being VECTOR of b₁ st ||.b₂.|| = 1

proof end;

theorem Th18: :: LOPBAN_2:18

for b₁ being non trivial RealNormSpace holds (BoundedLinearOperatorsNorm b₁,b₁) . (id the carrier of b₁) = 1

proof end;

definition

attr a₁ is strict;
struct Normed_AlgebraStr -> AlgebraStr , NORMSTR ;
aggr Normed_AlgebraStr(# carrier, mult, add, Mult, unity, Zero, norm #) -> Normed_AlgebraStr ;

end;

registration

cluster non empty Normed_AlgebraStr ;
existence

proof end;

end;

definition

let c₁ be RealNormSpace;
func R_Normed_Algebra_of_BoundedLinearOperators c₁ -> Normed_AlgebraStr equals :: LOPBAN_2:def 8
Normed_AlgebraStr(# (BoundedLinearOperators a₁,a₁),(FuncMult a₁),(Add_ (BoundedLinearOperators a₁,a₁),(R_VectorSpace_of_LinearOperators a₁,a₁)),(Mult_ (BoundedLinearOperators a₁,a₁),(R_VectorSpace_of_LinearOperators a₁,a₁)),(FuncUnit a₁),(Zero_ (BoundedLinearOperators a₁,a₁),(R_VectorSpace_of_LinearOperators a₁,a₁)),(BoundedLinearOperatorsNorm a₁,a₁) #);
correctness ;

end;

:: deftheorem Def8 defines R_Normed_Algebra_of_BoundedLinearOperators LOPBAN_2:def 8 :

registration

let c₁ be RealNormSpace;
cluster R_Normed_Algebra_of_BoundedLinearOperators a₁ -> non empty strict ;
coherence

proof end;

end;

E23: now

let c₁ be RealNormSpace;
set c₂ = R_Normed_Algebra_of_BoundedLinearOperators c₁;
let c₃, c₄ be Element of (R_Normed_Algebra_of_BoundedLinearOperators c₁);
assume E24: c₄ = FuncUnit c₁ ;
reconsider c₅ = c₃ as Element of BoundedLinearOperators c₁,c₁ ;
thus c₃ * c₄ = the mult of (R_Normed_Algebra_of_BoundedLinearOperators c₁) . c₃,c₄
.= (FuncMult c₁) . c₅,(FuncUnit c₁) by E24
.= c₅ * (FuncUnit c₁) by Def4
.= c₃ by Th8 ;
thus c₄ * c₃ = the mult of (R_Normed_Algebra_of_BoundedLinearOperators c₁) . c₄,c₃
.= (FuncMult c₁) . (FuncUnit c₁),c₅ by E24
.= (FuncUnit c₁) * c₅ by Def4
.= c₃ by Th8 ;

end;

registration

let c₁ be RealNormSpace;
cluster R_Normed_Algebra_of_BoundedLinearOperators a₁ -> non empty unital strict ;
coherence

proof end;

end;

E24: now

let c₁ be RealNormSpace;
set c₂ = R_Normed_Algebra_of_BoundedLinearOperators c₁;
reconsider c₃ = FuncUnit c₁ as Element of (R_Normed_Algebra_of_BoundedLinearOperators c₁) ;
for b₁ being Element of (R_Normed_Algebra_of_BoundedLinearOperators c₁) holds
( b₁ * c₃ = b₁ & c₃ * b₁ = b₁ ) by Lemma23;
hence 1. (R_Normed_Algebra_of_BoundedLinearOperators c₁) = FuncUnit c₁ by GROUP_1:def 5;

end;

theorem Th19: :: LOPBAN_2:19

for b₁ being RealNormSpace
for b₂, b₃, b₄ being Element of (R_Normed_Algebra_of_BoundedLinearOperators b₁)
for b₅, b₆ being Real holds
( b₂ + b₃ = b₃ + b₂ & (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄) & b₂ + (0. (R_Normed_Algebra_of_BoundedLinearOperators b₁)) = b₂ & ex b₇ being Element of (R_Normed_Algebra_of_BoundedLinearOperators b₁) st b₂ + b₇ = 0. (R_Normed_Algebra_of_BoundedLinearOperators b₁) & (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) & b₂ * (1. (R_Normed_Algebra_of_BoundedLinearOperators b₁)) = b₂ & (1. (R_Normed_Algebra_of_BoundedLinearOperators b₁)) * b₂ = b₂ & b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄) & (b₃ + b₄) * b₂ = (b₃ * b₂) + (b₄ * b₂) & b₅ * (b₂ * b₃) = (b₅ * b₂) * b₃ & (b₅ * b₆) * (b₂ * b₃) = (b₅ * b₂) * (b₆ * b₃) & b₅ * (b₂ + b₃) = (b₅ * b₂) + (b₅ * b₃) & (b₅ + b₆) * b₂ = (b₅ * b₂) + (b₆ * b₂) & (b₅ * b₆) * b₂ = b₅ * (b₆ * b₂) & 1 * b₂ = b₂ )

proof end;

theorem Th20: :: LOPBAN_2:20

proof end;

registration

cluster non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like associative Algebra-like RealNormSpace-like strict Normed_AlgebraStr ;
existence

proof end;

end;

definition

mode Normed_Algebra is non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like associative Algebra-like RealNormSpace-like Normed_AlgebraStr ;

end;

registration end;

definition

let c₁ be non empty Normed_AlgebraStr ;
attr a₁ is Banach_Algebra-like_1 means :: LOPBAN_2:def 9
for b₁, b₂ being Element of a₁ holds ||.(b₁ * b₂).|| <= ||.b₁.|| * ||.b₂.||;
attr a₁ is Banach_Algebra-like_2 means :: LOPBAN_2:def 10
||.(1. a₁).|| = 1;
attr a₁ is Banach_Algebra-like_3 means :: LOPBAN_2:def 11
for b₁ being Real
for b₂, b₃ being Element of a₁ holds b₁ * (b₂ * b₃) = b₂ * (b₁ * b₃);

end;

:: deftheorem Def9 defines Banach_Algebra-like_1 LOPBAN_2:def 9 :

:: deftheorem Def10 defines Banach_Algebra-like_2 LOPBAN_2:def 10 :

:: deftheorem Def11 defines Banach_Algebra-like_3 LOPBAN_2:def 11 :

definition

let c₁ be Normed_Algebra;
attr a₁ is Banach_Algebra-like means :Def12: :: LOPBAN_2:def 12
( a₁ is Banach_Algebra-like_1 & a₁ is Banach_Algebra-like_2 & a₁ is Banach_Algebra-like_3 & a₁ is left_unital & a₁ is left-distributive & a₁ is complete );

end;

:: deftheorem Def12 defines Banach_Algebra-like LOPBAN_2:def 12 :

registration

cluster Banach_Algebra-like -> left-distributive left_unital complete Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Normed_AlgebraStr ;
coherence by Def12;
cluster left-distributive left_unital complete Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 -> Banach_Algebra-like Normed_AlgebraStr ;
coherence by Def12;

end;

registration end;

registration

cluster left-distributive left_unital complete Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_AlgebraStr ;
existence

proof end;

end;

definition

mode Banach_Algebra is Banach_Algebra-like Normed_Algebra;

end;

theorem Th21: :: LOPBAN_2:21

for b₁ being RealNormSpace holds 1. (Ring_of_BoundedLinearOperators b₁) = FuncUnit b₁ by Lemma15;

theorem Th22: :: LOPBAN_2:22

for b₁ being RealNormSpace holds 1. (R_Algebra_of_BoundedLinearOperators b₁) = FuncUnit b₁ by Lemma19;

theorem Th23: :: LOPBAN_2:23

for b₁ being RealNormSpace holds 1. (R_Normed_Algebra_of_BoundedLinearOperators b₁) = FuncUnit b₁ by Lemma24;