:: by Yasunari Shidama , Hikofumi Suzuki and Noboru Endou

::

:: Received March 3, 2008

:: Copyright (c) 2008-2016 Association of Mizar Users

:: deftheorem defines having-inverse C0SP1:def 1 :

for V being non empty addLoopStr

for V1 being Subset of V holds

( V1 is having-inverse iff for v being Element of V st v in V1 holds

- v in V1 );

for V being non empty addLoopStr

for V1 being Subset of V holds

( V1 is having-inverse iff for v being Element of V st v in V1 holds

- v in V1 );

:: deftheorem defines additively-closed C0SP1:def 2 :

for V being non empty addLoopStr

for V1 being Subset of V holds

( V1 is additively-closed iff ( V1 is add-closed & V1 is having-inverse ) );

for V being non empty addLoopStr

for V1 being Subset of V holds

( V1 is additively-closed iff ( V1 is add-closed & V1 is having-inverse ) );

Lm1: for V being non empty addLoopStr holds [#] V is add-closed

proof end;

registration

let V be non empty addLoopStr ;

correctness

coherence

( [#] V is add-closed & [#] V is having-inverse );

by Lm1;

end;
correctness

coherence

( [#] V is add-closed & [#] V is having-inverse );

by Lm1;

registration

let V be non empty doubleLoopStr ;

coherence

for b_{1} being Subset of V st b_{1} is additively-closed holds

( b_{1} is add-closed & b_{1} is having-inverse )
;

coherence

for b_{1} being Subset of V st b_{1} is add-closed & b_{1} is having-inverse holds

b_{1} is additively-closed
;

end;
coherence

for b

( b

coherence

for b

b

registration

let V be non empty addLoopStr ;

correctness

existence

ex b_{1} being Subset of V st

( b_{1} is add-closed & b_{1} is having-inverse & not b_{1} is empty );

end;
correctness

existence

ex b

( b

proof end;

definition

let V be Ring;

ex b_{1} being Ring st

( the carrier of b_{1} c= the carrier of V & the addF of b_{1} = the addF of V || the carrier of b_{1} & the multF of b_{1} = the multF of V || the carrier of b_{1} & 1. b_{1} = 1. V & 0. b_{1} = 0. V )

end;
mode Subring of V -> Ring means :Def3: :: C0SP1:def 3

( the carrier of it c= the carrier of V & the addF of it = the addF of V || the carrier of it & the multF of it = the multF of V || the carrier of it & 1. it = 1. V & 0. it = 0. V );

existence ( the carrier of it c= the carrier of V & the addF of it = the addF of V || the carrier of it & the multF of it = the multF of V || the carrier of it & 1. it = 1. V & 0. it = 0. V );

ex b

( the carrier of b

proof end;

:: deftheorem Def3 defines Subring C0SP1:def 3 :

for V, b_{2} being Ring holds

( b_{2} is Subring of V iff ( the carrier of b_{2} c= the carrier of V & the addF of b_{2} = the addF of V || the carrier of b_{2} & the multF of b_{2} = the multF of V || the carrier of b_{2} & 1. b_{2} = 1. V & 0. b_{2} = 0. V ) );

for V, b

( b

theorem Th1: :: C0SP1:1

for X being non empty set

for d1, d2 being Element of X

for A being BinOp of X

for M being Function of [:X,X:],X

for V being Ring

for V1 being Subset of V st V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse holds

doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V

for d1, d2 being Element of X

for A being BinOp of X

for M being Function of [:X,X:],X

for V being Ring

for V1 being Subset of V st V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse holds

doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V

proof end;

registration

let V be Ring;

ex b_{1} being Subring of V st b_{1} is strict

end;
cluster non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed V103() right-distributive left-distributive right_unital well-unital distributive left_unital unital associative for Subring of V;

existence ex b

proof end;

definition

let V be non empty multLoopStr_0 ;

let V1 be Subset of V;

end;
let V1 be Subset of V;

attr V1 is multiplicatively-closed means :: C0SP1:def 4

( 1. V in V1 & ( for v, u being Element of V st v in V1 & u in V1 holds

v * u in V1 ) );

( 1. V in V1 & ( for v, u being Element of V st v in V1 & u in V1 holds

v * u in V1 ) );

:: deftheorem defines multiplicatively-closed C0SP1:def 4 :

for V being non empty multLoopStr_0

for V1 being Subset of V holds

( V1 is multiplicatively-closed iff ( 1. V in V1 & ( for v, u being Element of V st v in V1 & u in V1 holds

v * u in V1 ) ) );

for V being non empty multLoopStr_0

for V1 being Subset of V holds

( V1 is multiplicatively-closed iff ( 1. V in V1 & ( for v, u being Element of V st v in V1 & u in V1 holds

v * u in V1 ) ) );

definition

let V be non empty addLoopStr ;

let V1 be Subset of V;

assume A1: ( V1 is add-closed & not V1 is empty ) ;

correctness

coherence

the addF of V || V1 is BinOp of V1;

end;
let V1 be Subset of V;

assume A1: ( V1 is add-closed & not V1 is empty ) ;

correctness

coherence

the addF of V || V1 is BinOp of V1;

proof end;

:: deftheorem Def5 defines Add_ C0SP1:def 5 :

for V being non empty addLoopStr

for V1 being Subset of V st V1 is add-closed & not V1 is empty holds

Add_ (V1,V) = the addF of V || V1;

for V being non empty addLoopStr

for V1 being Subset of V st V1 is add-closed & not V1 is empty holds

Add_ (V1,V) = the addF of V || V1;

definition

let V be non empty multLoopStr_0 ;

let V1 be Subset of V;

assume A1: ( V1 is multiplicatively-closed & not V1 is empty ) ;

correctness

coherence

the multF of V || V1 is BinOp of V1;

end;
let V1 be Subset of V;

assume A1: ( V1 is multiplicatively-closed & not V1 is empty ) ;

correctness

coherence

the multF of V || V1 is BinOp of V1;

proof end;

:: deftheorem Def6 defines mult_ C0SP1:def 6 :

for V being non empty multLoopStr_0

for V1 being Subset of V st V1 is multiplicatively-closed & not V1 is empty holds

mult_ (V1,V) = the multF of V || V1;

for V being non empty multLoopStr_0

for V1 being Subset of V st V1 is multiplicatively-closed & not V1 is empty holds

mult_ (V1,V) = the multF of V || V1;

definition

let V be non empty right_complementable add-associative right_zeroed doubleLoopStr ;

let V1 be Subset of V;

assume A1: ( V1 is add-closed & V1 is having-inverse & not V1 is empty ) ;

correctness

coherence

0. V is Element of V1;

end;
let V1 be Subset of V;

assume A1: ( V1 is add-closed & V1 is having-inverse & not V1 is empty ) ;

correctness

coherence

0. V is Element of V1;

proof end;

:: deftheorem Def7 defines Zero_ C0SP1:def 7 :

for V being non empty right_complementable add-associative right_zeroed doubleLoopStr

for V1 being Subset of V st V1 is add-closed & V1 is having-inverse & not V1 is empty holds

Zero_ (V1,V) = 0. V;

for V being non empty right_complementable add-associative right_zeroed doubleLoopStr

for V1 being Subset of V st V1 is add-closed & V1 is having-inverse & not V1 is empty holds

Zero_ (V1,V) = 0. V;

definition

let V be non empty multLoopStr_0 ;

let V1 be Subset of V;

assume A1: ( V1 is multiplicatively-closed & not V1 is empty ) ;

correctness

coherence

1. V is Element of V1;

by A1;

end;
let V1 be Subset of V;

assume A1: ( V1 is multiplicatively-closed & not V1 is empty ) ;

correctness

coherence

1. V is Element of V1;

by A1;

:: deftheorem Def8 defines One_ C0SP1:def 8 :

for V being non empty multLoopStr_0

for V1 being Subset of V st V1 is multiplicatively-closed & not V1 is empty holds

One_ (V1,V) = 1. V;

for V being non empty multLoopStr_0

for V1 being Subset of V st V1 is multiplicatively-closed & not V1 is empty holds

One_ (V1,V) = 1. V;

theorem :: C0SP1:2

for V being Ring

for V1 being Subset of V st V1 is additively-closed & V1 is multiplicatively-closed & not V1 is empty holds

doubleLoopStr(# V1,(Add_ (V1,V)),(mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Ring

for V1 being Subset of V st V1 is additively-closed & V1 is multiplicatively-closed & not V1 is empty holds

doubleLoopStr(# V1,(Add_ (V1,V)),(mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Ring

proof end;

definition

let V be Algebra;

ex b_{1} being Algebra st

( the carrier of b_{1} c= the carrier of V & the addF of b_{1} = the addF of V || the carrier of b_{1} & the multF of b_{1} = the multF of V || the carrier of b_{1} & the Mult of b_{1} = the Mult of V | [:REAL, the carrier of b_{1}:] & 1. b_{1} = 1. V & 0. b_{1} = 0. V )

end;
mode Subalgebra of V -> Algebra means :Def9: :: C0SP1:def 9

( the carrier of it c= the carrier of V & the addF of it = the addF of V || the carrier of it & the multF of it = the multF of V || the carrier of it & the Mult of it = the Mult of V | [:REAL, the carrier of it:] & 1. it = 1. V & 0. it = 0. V );

existence ( the carrier of it c= the carrier of V & the addF of it = the addF of V || the carrier of it & the multF of it = the multF of V || the carrier of it & the Mult of it = the Mult of V | [:REAL, the carrier of it:] & 1. it = 1. V & 0. it = 0. V );

ex b

( the carrier of b

proof end;

:: deftheorem Def9 defines Subalgebra C0SP1:def 9 :

for V, b_{2} being Algebra holds

( b_{2} is Subalgebra of V iff ( the carrier of b_{2} c= the carrier of V & the addF of b_{2} = the addF of V || the carrier of b_{2} & the multF of b_{2} = the multF of V || the carrier of b_{2} & the Mult of b_{2} = the Mult of V | [:REAL, the carrier of b_{2}:] & 1. b_{2} = 1. V & 0. b_{2} = 0. V ) );

for V, b

( b

theorem Th3: :: C0SP1:3

for X being non empty set

for d1, d2 being Element of X

for A being BinOp of X

for M being Function of [:X,X:],X

for V being Algebra

for V1 being Subset of V

for MR being Function of [:REAL,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL,V1:] & V1 is having-inverse holds

AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V

for d1, d2 being Element of X

for A being BinOp of X

for M being Function of [:X,X:],X

for V being Algebra

for V1 being Subset of V

for MR being Function of [:REAL,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL,V1:] & V1 is having-inverse holds

AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V

proof end;

registration

let V be Algebra;

ex b_{1} being Subalgebra of V st b_{1} is strict

end;
cluster non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V103() strict vector-associative right-distributive right_unital well-unital left_unital unital associative commutative for Subalgebra of V;

existence ex b

proof end;

definition

let V be Algebra;

let V1 be Subset of V;

end;
let V1 be Subset of V;

attr V1 is additively-linearly-closed means :: C0SP1:def 10

( V1 is add-closed & V1 is having-inverse & ( for a being Real

for v being Element of V st v in V1 holds

a * v in V1 ) );

( V1 is add-closed & V1 is having-inverse & ( for a being Real

for v being Element of V st v in V1 holds

a * v in V1 ) );

:: deftheorem defines additively-linearly-closed C0SP1:def 10 :

for V being Algebra

for V1 being Subset of V holds

( V1 is additively-linearly-closed iff ( V1 is add-closed & V1 is having-inverse & ( for a being Real

for v being Element of V st v in V1 holds

a * v in V1 ) ) );

for V being Algebra

for V1 being Subset of V holds

( V1 is additively-linearly-closed iff ( V1 is add-closed & V1 is having-inverse & ( for a being Real

for v being Element of V st v in V1 holds

a * v in V1 ) ) );

registration

let V be Algebra;

coherence

for b_{1} being Subset of V st b_{1} is additively-linearly-closed holds

b_{1} is additively-closed
;

end;
coherence

for b

b

definition

let V be Algebra;

let V1 be Subset of V;

assume A1: ( V1 is additively-linearly-closed & not V1 is empty ) ;

coherence

the Mult of V | [:REAL,V1:] is Function of [:REAL,V1:],V1;

end;
let V1 be Subset of V;

assume A1: ( V1 is additively-linearly-closed & not V1 is empty ) ;

func Mult_ (V1,V) -> Function of [:REAL,V1:],V1 equals :Def11: :: C0SP1:def 11

the Mult of V | [:REAL,V1:];

correctness the Mult of V | [:REAL,V1:];

coherence

the Mult of V | [:REAL,V1:] is Function of [:REAL,V1:],V1;

proof end;

:: deftheorem Def11 defines Mult_ C0SP1:def 11 :

for V being Algebra

for V1 being Subset of V st V1 is additively-linearly-closed & not V1 is empty holds

Mult_ (V1,V) = the Mult of V | [:REAL,V1:];

for V being Algebra

for V1 being Subset of V st V1 is additively-linearly-closed & not V1 is empty holds

Mult_ (V1,V) = the Mult of V | [:REAL,V1:];

:: deftheorem defines scalar-mult-cancelable C0SP1:def 12 :

for V being non empty RLSStruct holds

( V is scalar-mult-cancelable iff for a being Real

for v being Element of V holds

( not a * v = 0. V or a = 0 or v = 0. V ) );

for V being non empty RLSStruct holds

( V is scalar-mult-cancelable iff for a being Real

for v being Element of V holds

( not a * v = 0. V or a = 0 or v = 0. V ) );

theorem Th4: :: C0SP1:4

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr

for a being Real holds a * (0. V) = 0. V

for a being Real holds a * (0. V) = 0. V

proof end;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

theorem :: C0SP1:5

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr st V is scalar-mult-cancelable holds

V is RealLinearSpace

V is RealLinearSpace

proof end;

Lm2: for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr st ( for v being VECTOR of V holds 1 * v = v ) holds

V is RealLinearSpace

by RLVECT_1:def 8;

theorem Th6: :: C0SP1:6

for V being Algebra

for V1 being Subset of V st V1 is additively-linearly-closed & V1 is multiplicatively-closed & not V1 is empty holds

AlgebraStr(# V1,(mult_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Subalgebra of V

for V1 being Subset of V st V1 is additively-linearly-closed & V1 is multiplicatively-closed & not V1 is empty holds

AlgebraStr(# V1,(mult_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Subalgebra of V

proof end;

registration

let X be non empty set ;

coherence

( RAlgebra X is Abelian & RAlgebra X is add-associative & RAlgebra X is right_zeroed & RAlgebra X is right_complementable & RAlgebra X is commutative & RAlgebra X is associative & RAlgebra X is right_unital & RAlgebra X is right-distributive & RAlgebra X is vector-distributive & RAlgebra X is scalar-distributive & RAlgebra X is scalar-associative & RAlgebra X is vector-associative );

;

end;
cluster RAlgebra X -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative right-distributive right_unital associative commutative ;

correctness coherence

( RAlgebra X is Abelian & RAlgebra X is add-associative & RAlgebra X is right_zeroed & RAlgebra X is right_complementable & RAlgebra X is commutative & RAlgebra X is associative & RAlgebra X is right_unital & RAlgebra X is right-distributive & RAlgebra X is vector-distributive & RAlgebra X is scalar-distributive & RAlgebra X is scalar-associative & RAlgebra X is vector-associative );

;

theorem Th8: :: C0SP1:8

for V being Algebra

for V1 being Subalgebra of V holds

( ( for v1, w1 being Element of V1

for v, w being Element of V st v1 = v & w1 = w holds

v1 + w1 = v + w ) & ( for v1, w1 being Element of V1

for v, w being Element of V st v1 = v & w1 = w holds

v1 * w1 = v * w ) & ( for v1 being Element of V1

for v being Element of V

for a being Real st v1 = v holds

a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )

for V1 being Subalgebra of V holds

( ( for v1, w1 being Element of V1

for v, w being Element of V st v1 = v & w1 = w holds

v1 + w1 = v + w ) & ( for v1, w1 being Element of V1

for v, w being Element of V st v1 = v & w1 = w holds

v1 * w1 = v * w ) & ( for v1 being Element of V1

for v being Element of V

for a being Real st v1 = v holds

a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )

proof end;

definition

let X be non empty set ;

coherence

{ f where f is Function of X,REAL : f | X is bounded } is non empty Subset of (RAlgebra X);

end;
func BoundedFunctions X -> non empty Subset of (RAlgebra X) equals :: C0SP1:def 13

{ f where f is Function of X,REAL : f | X is bounded } ;

correctness { f where f is Function of X,REAL : f | X is bounded } ;

coherence

{ f where f is Function of X,REAL : f | X is bounded } is non empty Subset of (RAlgebra X);

proof end;

:: deftheorem defines BoundedFunctions C0SP1:def 13 :

for X being non empty set holds BoundedFunctions X = { f where f is Function of X,REAL : f | X is bounded } ;

for X being non empty set holds BoundedFunctions X = { f where f is Function of X,REAL : f | X is bounded } ;

theorem Th9: :: C0SP1:9

for X being non empty set holds

( BoundedFunctions X is additively-linearly-closed & BoundedFunctions X is multiplicatively-closed )

( BoundedFunctions X is additively-linearly-closed & BoundedFunctions X is multiplicatively-closed )

proof end;

registration

let X be non empty set ;

coherence

( BoundedFunctions X is additively-linearly-closed & BoundedFunctions X is multiplicatively-closed ) by Th9;

end;
coherence

( BoundedFunctions X is additively-linearly-closed & BoundedFunctions X is multiplicatively-closed ) by Th9;

definition

let X be non empty set ;

AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))) #) is Algebra by Th6;

end;
func R_Algebra_of_BoundedFunctions X -> Algebra equals :: C0SP1:def 14

AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))) #);

coherence AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))) #);

AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))) #) is Algebra by Th6;

:: deftheorem defines R_Algebra_of_BoundedFunctions C0SP1:def 14 :

for X being non empty set holds R_Algebra_of_BoundedFunctions X = AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))) #);

for X being non empty set holds R_Algebra_of_BoundedFunctions X = AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))) #);

theorem :: C0SP1:10

theorem Th12: :: C0SP1:12

for X being non empty set

for F, G, H being VECTOR of (R_Algebra_of_BoundedFunctions X)

for f, g, h being Function of X,REAL st f = F & g = G & h = H holds

( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )

for F, G, H being VECTOR of (R_Algebra_of_BoundedFunctions X)

for f, g, h being Function of X,REAL st f = F & g = G & h = H holds

( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )

proof end;

theorem Th13: :: C0SP1:13

for X being non empty set

for a being Real

for F, G being VECTOR of (R_Algebra_of_BoundedFunctions X)

for f, g being Function of X,REAL st f = F & g = G holds

( G = a * F iff for x being Element of X holds g . x = a * (f . x) )

for a being Real

for F, G being VECTOR of (R_Algebra_of_BoundedFunctions X)

for f, g being Function of X,REAL st f = F & g = G holds

( G = a * F iff for x being Element of X holds g . x = a * (f . x) )

proof end;

theorem Th14: :: C0SP1:14

for X being non empty set

for F, G, H being VECTOR of (R_Algebra_of_BoundedFunctions X)

for f, g, h being Function of X,REAL st f = F & g = G & h = H holds

( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )

for F, G, H being VECTOR of (R_Algebra_of_BoundedFunctions X)

for f, g, h being Function of X,REAL st f = F & g = G & h = H holds

( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )

proof end;

definition

let X be non empty set ;

let F be object ;

assume A1: F in BoundedFunctions X ;

existence

ex b_{1} being Function of X,REAL st

( b_{1} = F & b_{1} | X is bounded );

uniqueness

for b_{1}, b_{2} being Function of X,REAL st b_{1} = F & b_{1} | X is bounded & b_{2} = F & b_{2} | X is bounded holds

b_{1} = b_{2};

by A1;

end;
let F be object ;

assume A1: F in BoundedFunctions X ;

func modetrans (F,X) -> Function of X,REAL means :Def15: :: C0SP1:def 15

( it = F & it | X is bounded );

correctness ( it = F & it | X is bounded );

existence

ex b

( b

uniqueness

for b

b

by A1;

:: deftheorem Def15 defines modetrans C0SP1:def 15 :

for X being non empty set

for F being object st F in BoundedFunctions X holds

for b_{3} being Function of X,REAL holds

( b_{3} = modetrans (F,X) iff ( b_{3} = F & b_{3} | X is bounded ) );

for X being non empty set

for F being object st F in BoundedFunctions X holds

for b

( b

definition

let X be non empty set ;

let f be Function of X,REAL;

{ |.(f . x).| where x is Element of X : verum } is non empty Subset of REAL

end;
let f be Function of X,REAL;

func PreNorms f -> non empty Subset of REAL equals :: C0SP1:def 16

{ |.(f . x).| where x is Element of X : verum } ;

coherence { |.(f . x).| where x is Element of X : verum } ;

{ |.(f . x).| where x is Element of X : verum } is non empty Subset of REAL

proof end;

:: deftheorem defines PreNorms C0SP1:def 16 :

for X being non empty set

for f being Function of X,REAL holds PreNorms f = { |.(f . x).| where x is Element of X : verum } ;

for X being non empty set

for f being Function of X,REAL holds PreNorms f = { |.(f . x).| where x is Element of X : verum } ;

theorem Th17: :: C0SP1:17

for X being non empty set

for f being Function of X,REAL st f | X is bounded holds

PreNorms f is bounded_above

for f being Function of X,REAL st f | X is bounded holds

PreNorms f is bounded_above

proof end;

theorem :: C0SP1:18

for X being non empty set

for f being Function of X,REAL holds

( f | X is bounded iff PreNorms f is bounded_above )

for f being Function of X,REAL holds

( f | X is bounded iff PreNorms f is bounded_above )

proof end;

definition

let X be non empty set ;

ex b_{1} being Function of (BoundedFunctions X),REAL st

for x being object st x in BoundedFunctions X holds

b_{1} . x = upper_bound (PreNorms (modetrans (x,X)))

for b_{1}, b_{2} being Function of (BoundedFunctions X),REAL st ( for x being object st x in BoundedFunctions X holds

b_{1} . x = upper_bound (PreNorms (modetrans (x,X))) ) & ( for x being object st x in BoundedFunctions X holds

b_{2} . x = upper_bound (PreNorms (modetrans (x,X))) ) holds

b_{1} = b_{2}

end;
func BoundedFunctionsNorm X -> Function of (BoundedFunctions X),REAL means :Def17: :: C0SP1:def 17

for x being object st x in BoundedFunctions X holds

it . x = upper_bound (PreNorms (modetrans (x,X)));

existence for x being object st x in BoundedFunctions X holds

it . x = upper_bound (PreNorms (modetrans (x,X)));

ex b

for x being object st x in BoundedFunctions X holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def17 defines BoundedFunctionsNorm C0SP1:def 17 :

for X being non empty set

for b_{2} being Function of (BoundedFunctions X),REAL holds

( b_{2} = BoundedFunctionsNorm X iff for x being object st x in BoundedFunctions X holds

b_{2} . x = upper_bound (PreNorms (modetrans (x,X))) );

for X being non empty set

for b

( b

b

theorem Th19: :: C0SP1:19

for X being non empty set

for f being Function of X,REAL st f | X is bounded holds

modetrans (f,X) = f

for f being Function of X,REAL st f | X is bounded holds

modetrans (f,X) = f

proof end;

theorem Th20: :: C0SP1:20

for X being non empty set

for f being Function of X,REAL st f | X is bounded holds

(BoundedFunctionsNorm X) . f = upper_bound (PreNorms f)

for f being Function of X,REAL st f | X is bounded holds

(BoundedFunctionsNorm X) . f = upper_bound (PreNorms f)

proof end;

definition

let X be non empty set ;

coherence

Normed_AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))),(BoundedFunctionsNorm X) #) is Normed_AlgebraStr ;

;

end;
func R_Normed_Algebra_of_BoundedFunctions X -> Normed_AlgebraStr equals :: C0SP1:def 18

Normed_AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))),(BoundedFunctionsNorm X) #);

correctness Normed_AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))),(BoundedFunctionsNorm X) #);

coherence

Normed_AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))),(BoundedFunctionsNorm X) #) is Normed_AlgebraStr ;

;

:: deftheorem defines R_Normed_Algebra_of_BoundedFunctions C0SP1:def 18 :

for X being non empty set holds R_Normed_Algebra_of_BoundedFunctions X = Normed_AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))),(BoundedFunctionsNorm X) #);

for X being non empty set holds R_Normed_Algebra_of_BoundedFunctions X = Normed_AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))),(BoundedFunctionsNorm X) #);

registration

let X be non empty set ;

correctness

coherence

not R_Normed_Algebra_of_BoundedFunctions X is empty ;

;

end;
correctness

coherence

not R_Normed_Algebra_of_BoundedFunctions X is empty ;

;

Lm3: now :: thesis: for X being non empty set

for x, e being Element of (R_Normed_Algebra_of_BoundedFunctions X) st e = One_ ((BoundedFunctions X),(RAlgebra X)) holds

( x * e = x & e * x = x )

for x, e being Element of (R_Normed_Algebra_of_BoundedFunctions X) st e = One_ ((BoundedFunctions X),(RAlgebra X)) holds

( x * e = x & e * x = x )

let X be non empty set ; :: thesis: for x, e being Element of (R_Normed_Algebra_of_BoundedFunctions X) st e = One_ ((BoundedFunctions X),(RAlgebra X)) holds

( x * e = x & e * x = x )

set F = R_Normed_Algebra_of_BoundedFunctions X;

let x, e be Element of (R_Normed_Algebra_of_BoundedFunctions X); :: thesis: ( e = One_ ((BoundedFunctions X),(RAlgebra X)) implies ( x * e = x & e * x = x ) )

set X1 = BoundedFunctions X;

reconsider f = x as Element of BoundedFunctions X ;

assume A1: e = One_ ((BoundedFunctions X),(RAlgebra X)) ; :: thesis: ( x * e = x & e * x = x )

then x * e = (mult_ ((BoundedFunctions X),(RAlgebra X))) . (f,(1_ (RAlgebra X))) by Def8;

then A2: x * e = ( the multF of (RAlgebra X) || (BoundedFunctions X)) . (f,(1_ (RAlgebra X))) by Def6;

e * x = (mult_ ((BoundedFunctions X),(RAlgebra X))) . ((1_ (RAlgebra X)),f) by A1, Def8;

then A3: e * x = ( the multF of (RAlgebra X) || (BoundedFunctions X)) . ((1_ (RAlgebra X)),f) by Def6;

A4: 1_ (RAlgebra X) = 1_ (R_Algebra_of_BoundedFunctions X) by Th16;

then [f,(1_ (RAlgebra X))] in [:(BoundedFunctions X),(BoundedFunctions X):] by ZFMISC_1:87;

then x * e = f * (1_ (RAlgebra X)) by A2, FUNCT_1:49;

hence x * e = x by VECTSP_1:def 4; :: thesis: e * x = x

[(1_ (RAlgebra X)),f] in [:(BoundedFunctions X),(BoundedFunctions X):] by A4, ZFMISC_1:87;

then e * x = (1_ (RAlgebra X)) * f by A3, FUNCT_1:49;

hence e * x = x by VECTSP_1:def 4; :: thesis: verum

end;
( x * e = x & e * x = x )

set F = R_Normed_Algebra_of_BoundedFunctions X;

let x, e be Element of (R_Normed_Algebra_of_BoundedFunctions X); :: thesis: ( e = One_ ((BoundedFunctions X),(RAlgebra X)) implies ( x * e = x & e * x = x ) )

set X1 = BoundedFunctions X;

reconsider f = x as Element of BoundedFunctions X ;

assume A1: e = One_ ((BoundedFunctions X),(RAlgebra X)) ; :: thesis: ( x * e = x & e * x = x )

then x * e = (mult_ ((BoundedFunctions X),(RAlgebra X))) . (f,(1_ (RAlgebra X))) by Def8;

then A2: x * e = ( the multF of (RAlgebra X) || (BoundedFunctions X)) . (f,(1_ (RAlgebra X))) by Def6;

e * x = (mult_ ((BoundedFunctions X),(RAlgebra X))) . ((1_ (RAlgebra X)),f) by A1, Def8;

then A3: e * x = ( the multF of (RAlgebra X) || (BoundedFunctions X)) . ((1_ (RAlgebra X)),f) by Def6;

A4: 1_ (RAlgebra X) = 1_ (R_Algebra_of_BoundedFunctions X) by Th16;

then [f,(1_ (RAlgebra X))] in [:(BoundedFunctions X),(BoundedFunctions X):] by ZFMISC_1:87;

then x * e = f * (1_ (RAlgebra X)) by A2, FUNCT_1:49;

hence x * e = x by VECTSP_1:def 4; :: thesis: e * x = x

[(1_ (RAlgebra X)),f] in [:(BoundedFunctions X),(BoundedFunctions X):] by A4, ZFMISC_1:87;

then e * x = (1_ (RAlgebra X)) * f by A3, FUNCT_1:49;

hence e * x = x by VECTSP_1:def 4; :: thesis: verum

registration

let X be non empty set ;

correctness

coherence

R_Normed_Algebra_of_BoundedFunctions X is unital ;

end;
correctness

coherence

R_Normed_Algebra_of_BoundedFunctions X is unital ;

proof end;

theorem Th21: :: C0SP1:21

for W being Normed_AlgebraStr

for V being Algebra st AlgebraStr(# the carrier of W, the multF of W, the addF of W, the Mult of W, the OneF of W, the ZeroF of W #) = V holds

W is Algebra

for V being Algebra st AlgebraStr(# the carrier of W, the multF of W, the addF of W, the Mult of W, the OneF of W, the ZeroF of W #) = V holds

W is Algebra

proof end;

theorem Th23: :: C0SP1:23

for X being non empty set

for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds (Mult_ ((BoundedFunctions X),(RAlgebra X))) . (1,F) = F

for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds (Mult_ ((BoundedFunctions X),(RAlgebra X))) . (1,F) = F

proof end;

theorem Th26: :: C0SP1:26

for X being non empty set

for x being Element of X

for f being Function of X,REAL

for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & f | X is bounded holds

|.(f . x).| <= ||.F.||

for x being Element of X

for f being Function of X,REAL

for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & f | X is bounded holds

|.(f . x).| <= ||.F.||

proof end;

theorem :: C0SP1:27

for X being non empty set

for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds 0 <= ||.F.||

for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds 0 <= ||.F.||

proof end;

theorem Th28: :: C0SP1:28

for X being non empty set

for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) st F = 0. (R_Normed_Algebra_of_BoundedFunctions X) holds

0 = ||.F.||

for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) st F = 0. (R_Normed_Algebra_of_BoundedFunctions X) holds

0 = ||.F.||

proof end;

theorem Th29: :: C0SP1:29

for X being non empty set

for f, g, h being Function of X,REAL

for F, G, H being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds

( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )

for f, g, h being Function of X,REAL

for F, G, H being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds

( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )

proof end;

theorem Th30: :: C0SP1:30

for X being non empty set

for a being Real

for f, g being Function of X,REAL

for F, G being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G holds

( G = a * F iff for x being Element of X holds g . x = a * (f . x) )

for a being Real

for f, g being Function of X,REAL

for F, G being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G holds

( G = a * F iff for x being Element of X holds g . x = a * (f . x) )

proof end;

theorem Th31: :: C0SP1:31

for X being non empty set

for f, g, h being Function of X,REAL

for F, G, H being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds

( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )

for f, g, h being Function of X,REAL

for F, G, H being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds

( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )

proof end;

theorem Th32: :: C0SP1:32

for X being non empty set

for a being Real

for F, G being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds

( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )

for a being Real

for F, G being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds

( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )

proof end;

theorem Th33: :: C0SP1:33

for X being non empty set holds

( R_Normed_Algebra_of_BoundedFunctions X is reflexive & R_Normed_Algebra_of_BoundedFunctions X is discerning & R_Normed_Algebra_of_BoundedFunctions X is RealNormSpace-like )

( R_Normed_Algebra_of_BoundedFunctions X is reflexive & R_Normed_Algebra_of_BoundedFunctions X is discerning & R_Normed_Algebra_of_BoundedFunctions X is RealNormSpace-like )

proof end;

registration

let X be non empty set ;

( R_Normed_Algebra_of_BoundedFunctions X is reflexive & R_Normed_Algebra_of_BoundedFunctions X is discerning & R_Normed_Algebra_of_BoundedFunctions X is RealNormSpace-like & R_Normed_Algebra_of_BoundedFunctions X is vector-distributive & R_Normed_Algebra_of_BoundedFunctions X is scalar-distributive & R_Normed_Algebra_of_BoundedFunctions X is scalar-associative & R_Normed_Algebra_of_BoundedFunctions X is scalar-unital & R_Normed_Algebra_of_BoundedFunctions X is Abelian & R_Normed_Algebra_of_BoundedFunctions X is add-associative & R_Normed_Algebra_of_BoundedFunctions X is right_zeroed & R_Normed_Algebra_of_BoundedFunctions X is right_complementable ) by Th24, Th33;

end;
cluster R_Normed_Algebra_of_BoundedFunctions X -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ;

coherence ( R_Normed_Algebra_of_BoundedFunctions X is reflexive & R_Normed_Algebra_of_BoundedFunctions X is discerning & R_Normed_Algebra_of_BoundedFunctions X is RealNormSpace-like & R_Normed_Algebra_of_BoundedFunctions X is vector-distributive & R_Normed_Algebra_of_BoundedFunctions X is scalar-distributive & R_Normed_Algebra_of_BoundedFunctions X is scalar-associative & R_Normed_Algebra_of_BoundedFunctions X is scalar-unital & R_Normed_Algebra_of_BoundedFunctions X is Abelian & R_Normed_Algebra_of_BoundedFunctions X is add-associative & R_Normed_Algebra_of_BoundedFunctions X is right_zeroed & R_Normed_Algebra_of_BoundedFunctions X is right_complementable ) by Th24, Th33;

theorem Th34: :: C0SP1:34

for X being non empty set

for f, g, h being Function of X,REAL

for F, G, H being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds

( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) )

for f, g, h being Function of X,REAL

for F, G, H being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds

( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) )

proof end;

theorem Th35: :: C0SP1:35

for X being non empty set

for seq being sequence of (R_Normed_Algebra_of_BoundedFunctions X) st seq is Cauchy_sequence_by_Norm holds

seq is convergent

for seq being sequence of (R_Normed_Algebra_of_BoundedFunctions X) st seq is Cauchy_sequence_by_Norm holds

seq is convergent

proof end;

registration
end;

registration

let X be non empty set ;

( R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra-like_1 & R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra-like_2 & R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra-like_3 & R_Normed_Algebra_of_BoundedFunctions X is left-distributive & R_Normed_Algebra_of_BoundedFunctions X is left_unital )

end;
cluster R_Normed_Algebra_of_BoundedFunctions X -> left-distributive left_unital Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 ;

coherence ( R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra-like_1 & R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra-like_2 & R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra-like_3 & R_Normed_Algebra_of_BoundedFunctions X is left-distributive & R_Normed_Algebra_of_BoundedFunctions X is left_unital )

proof end;

theorem :: C0SP1:37