:: C0SP1 semantic presentation

definition

let V be non empty addLoopStr ;
let V1 be Subset of V;
attr V1 is having-inverse means :Rdef210b: :: C0SP1:def 1
for v being Element of V st v in V1 holds
- v in V1;

end;

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

definition

let V be non empty addLoopStr ;
let V1 be Subset of V;
attr V1 is additively-closed means :Rdef210: :: C0SP1:def 2
( V1 is add-closed & V1 is having-inverse );

end;

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

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

proof end;

Cor2: for V being non empty addLoopStr holds [#] V is having-inverse

proof end;

registration

let V be non empty addLoopStr ;
cluster [#] V -> add-closed having-inverse ;
correctness by Cor1, Cor2;

end;

registration

let V be non empty doubleLoopStr ;
cluster additively-closed -> add-closed having-inverse Element of bool the carrier of V;
coherence by Rdef210;
cluster add-closed having-inverse -> additively-closed Element of bool the carrier of V;
coherence by Rdef210;

end;

registration

let V be non empty addLoopStr ;
cluster non empty add-closed having-inverse Element of bool the carrier of V;
correctness

proof end;

end;

definition

let V be Ring;
mode Subring of V -> Ring means :DefSubRing: :: 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

proof end;

end;

:: deftheorem DefSubRing defines Subring C0SP1:def 3 :

theorem Th01: :: 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

proof end;

registration

let V be Ring;
cluster strict Subring of V;
existence

proof end;

end;

definition

let V be non empty multLoopStr_0 ;
let V1 be Subset of V;
attr V1 is multiplicatively-closed means :Rdef200: :: 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 ) );

end;

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

definition

let V be non empty addLoopStr ;
let V1 be Subset of V;
assume A1: ( V1 is add-closed & not V1 is empty ) ;
func Add_ V1,V -> BinOp of V1 equals :Rdef211: :: C0SP1:def 5
the addF of V || V1;
correctness

proof end;

end;

:: deftheorem Rdef211 defines Add_ C0SP1:def 5 :

definition

let V be non empty multLoopStr_0 ;
let V1 be Subset of V;
assume A1: ( V1 is multiplicatively-closed & not V1 is empty ) ;
func mult_ V1,V -> BinOp of V1 equals :Rdef220: :: C0SP1:def 6
the multF of V || V1;
correctness

proof end;

end;

:: deftheorem Rdef220 defines mult_ C0SP1:def 6 :

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 ) ;
func Zero_ V1,V -> Element of V1 equals :Rdef213: :: C0SP1:def 7
0. V;
correctness

proof end;

end;

:: deftheorem Rdef213 defines Zero_ C0SP1:def 7 :

definition

let V be non empty multLoopStr_0 ;
let V1 be Subset of V;
assume A1: ( V1 is multiplicatively-closed & not V1 is empty ) ;
func One_ V1,V -> Element of V1 equals :Rdef214: :: C0SP1:def 8
1. V;
correctness by A1, Rdef200;

end;

:: deftheorem Rdef214 defines One_ C0SP1:def 8 :

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

proof end;

definition

let V be Algebra;
mode Subalgebra of V -> Algebra means :DefSubAlg: :: 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

proof end;

end;

:: deftheorem DefSubAlg defines Subalgebra C0SP1:def 9 :

theorem Th02: :: 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

proof end;

registration

let V be Algebra;
cluster strict Subalgebra of V;
existence

proof end;

end;

definition

let V be Algebra;
let V1 be Subset of V;
attr V1 is additively-linearly-closed means :def210: :: 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 ) );

end;

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

registration

let V be Algebra;
cluster additively-linearly-closed -> additively-closed Element of bool the carrier of V;
coherence

proof end;

end;

definition

let V be Algebra;
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 :def212: :: C0SP1:def 11
the Mult of V | [:REAL ,V1:];
correctness

proof end;

end;

:: deftheorem def212 defines Mult_ C0SP1:def 11 :

definition

let V be non empty RLSStruct ;
attr V is scalar-mult-cancelable means :DefSMC: :: C0SP1:def 12
for a being Real
for v being Element of V holds
( not a * v = 0. V or a = 0 or v = 0. V );

end;

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

theorem RLVECT123: :: C0SP1:4

for V being non empty right_complementable add-associative right_zeroed Algebra-like AlgebraStr
for a being Real holds a * (0. V) = 0. V

proof end;

theorem :: C0SP1:5

for V being non empty right_complementable Abelian add-associative right_zeroed Algebra-like AlgebraStr st V is scalar-mult-cancelable holds
V is RealLinearSpace

proof end;

LmAlgebra: for V being non empty right_complementable Abelian add-associative right_zeroed Algebra-like AlgebraStr st ( for v being VECTOR of V holds 1 * v = v ) holds
V is RealLinearSpace

proof end;

theorem Th03: :: 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

proof end;

registration

let X be non empty set ;
cluster RAlgebra X -> right_complementable Abelian add-associative right_zeroed Algebra-like associative commutative right-distributive right_unital ;
correctness by FUNCSDOM:50;

end;

theorem LmAlgebra2: :: C0SP1:7

for X being non empty set holds RAlgebra X is RealLinearSpace

proof end;

theorem RLSUB121: :: 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 )

proof end;

definition

let X be non empty set ;
func BoundedFunctions X -> non empty Subset of (RAlgebra X) equals :: C0SP1:def 13
{ f where f is Function of X, REAL : f is_bounded_on X } ;
correctness

proof end;

end;

:: deftheorem defines BoundedFunctions C0SP1:def 13 :

theorem ThB7: :: C0SP1:9

for X being non empty set holds
( BoundedFunctions X is additively-linearly-closed & BoundedFunctions X is multiplicatively-closed )

proof end;

registration

let X be non empty set ;
cluster BoundedFunctions X -> non empty multiplicatively-closed additively-linearly-closed ;
coherence by ThB7;

end;

theorem :: C0SP1:10

for X being non empty set holds 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 Subalgebra of RAlgebra X by Th03;

definition

let X be non empty set ;
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 by Th03;

end;

:: deftheorem defines R_Algebra_of_BoundedFunctions C0SP1:def 14 :

theorem :: C0SP1:11

for X being non empty set holds R_Algebra_of_BoundedFunctions X is RealLinearSpace

proof end;

theorem ThB10: :: 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) )

proof end;

theorem ThB11: :: 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) )

proof end;

theorem ThB12: :: 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) )

proof end;

theorem ThB12Zero: :: C0SP1:15

for X being non empty set holds 0. (R_Algebra_of_BoundedFunctions X) = X --> 0

proof end;

theorem ThB12One: :: C0SP1:16

for X being non empty set holds 1_ (R_Algebra_of_BoundedFunctions X) = X --> 1

proof end;

definition

let X be non empty set ;
let F be set ;
assume A1: F in BoundedFunctions X ;
func modetrans F,X -> Function of X, REAL means :DefB7: :: C0SP1:def 15
( it = F & it is_bounded_on X );
correctness by A1;

end;

:: deftheorem DefB7 defines modetrans C0SP1:def 15 :

definition

let X be non empty set ;
let f be Function of X, REAL ;
func PreNorms f -> non empty Subset of REAL equals :: C0SP1:def 16
{ (abs (f . x)) where x is Element of X : verum } ;
coherence

proof end;

end;

:: deftheorem defines PreNorms C0SP1:def 16 :

theorem ThB13: :: C0SP1:17

for X being non empty set
for f being Function of X, REAL st f is_bounded_on X holds
( not PreNorms f is empty & 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 is_bounded_on X iff PreNorms f is bounded_above )

proof end;

theorem ThB15: :: C0SP1:19

for X being non empty set ex NORM being Function of BoundedFunctions X, REAL st
for F being set st F in BoundedFunctions X holds
NORM . F = sup (PreNorms (modetrans F,X))

proof end;

definition

let X be non empty set ;
func BoundedFunctionsNorm X -> Function of BoundedFunctions X, REAL means :DefB9: :: C0SP1:def 17
for x being set st x in BoundedFunctions X holds
it . x = sup (PreNorms (modetrans x,X));
existence by ThB15;
uniqueness

proof end;

end;

:: deftheorem DefB9 defines BoundedFunctionsNorm C0SP1:def 17 :

theorem ThB16: :: C0SP1:20

for X being non empty set
for f being Function of X, REAL st f is_bounded_on X holds
modetrans f,X = f

proof end;

theorem ThB17: :: C0SP1:21

for X being non empty