:: Real Functions Spaces
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received March 23, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
let A be set ;
let B be non empty set ;
let F be BinOp of (Funcs (A,B));
let f, g be Element of Funcs (A,B);
:: original:.
redefine funcF . (f,g) ->  Element of Funcs (A,B);
coherence
 F . (f,g) is Element of Funcs (A,B)
proofend;
end;

definition
let A, B, C, D be non empty set ;
let F be Function of [:C,D:],(Funcs (A,B));
let cd be Element of [:C,D:];
:: original:.
redefine funcF . cd ->  Element of Funcs (A,B);
coherence
 F . cd is Element of Funcs (A,B)
proofend;
end;

definition
let X be non empty set ;
let Z be set ;
let F be BinOp of X;
let f, g be Function of Z,X;
:: original:.:
redefine funcF .: (f,g) ->  Element of Funcs (Z,X);
coherence
 F .: (f,g) is Element of Funcs (Z,X)
proofend;
end;

definition
let X be non empty set ;
let Z be set ;
let F be BinOp of X;
let a be Element of X;
let f be Function of Z,X;
:: original:[;]
redefine funcF [;] (a,f) ->  Element of Funcs (Z,X);
coherence
 F [;] (a,f) is Element of Funcs (Z,X)
proofend;
end;

definition
let A be set ;
func RealFuncAdd A ->  BinOp of (Funcs (A,REAL)) means :Def1: :: FUNCSDOM:def 1
 for f, g being Element of Funcs (A,REAL) holds it . (f,g) = addreal .: (f,g);
existence
 ex b1 being BinOp of (Funcs (A,REAL)) st
for f, g being Element of Funcs (A,REAL) holds b1 . (f,g) = addreal .: (f,g)
proofend;
uniqueness
 for b1, b2 being BinOp of (Funcs (A,REAL)) st ( for f, g being Element of Funcs (A,REAL) holds b1 . (f,g) = addreal .: (f,g) ) & ( for f, g being Element of Funcs (A,REAL) holds b2 . (f,g) = addreal .: (f,g) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines RealFuncAdd FUNCSDOM:def_1_:_
 for A being set
for b2 being BinOp of (Funcs (A,REAL)) holds
( b2 = RealFuncAdd A iff for f, g being Element of Funcs (A,REAL) holds b2 . (f,g) = addreal .: (f,g) );

definition
let A be set ;
func RealFuncMult A ->  BinOp of (Funcs (A,REAL)) means :Def2: :: FUNCSDOM:def 2
 for f, g being Element of Funcs (A,REAL) holds it . (f,g) = multreal .: (f,g);
existence
 ex b1 being BinOp of (Funcs (A,REAL)) st
for f, g being Element of Funcs (A,REAL) holds b1 . (f,g) = multreal .: (f,g)
proofend;
uniqueness
 for b1, b2 being BinOp of (Funcs (A,REAL)) st ( for f, g being Element of Funcs (A,REAL) holds b1 . (f,g) = multreal .: (f,g) ) & ( for f, g being Element of Funcs (A,REAL) holds b2 . (f,g) = multreal .: (f,g) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines RealFuncMult FUNCSDOM:def_2_:_
 for A being set
for b2 being BinOp of (Funcs (A,REAL)) holds
( b2 = RealFuncMult A iff for f, g being Element of Funcs (A,REAL) holds b2 . (f,g) = multreal .: (f,g) );

definition
let A be set ;
func RealFuncExtMult A ->  Function of [:REAL,(Funcs (A,REAL)):],(Funcs (A,REAL)) means :Def3: :: FUNCSDOM:def 3
 for a being Real
for f being Element of Funcs (A,REAL) holds it . (a,f) = multreal [;] (a,f);
existence
 ex b1 being Function of [:REAL,(Funcs (A,REAL)):],(Funcs (A,REAL)) st
for a being Real
for f being Element of Funcs (A,REAL) holds b1 . (a,f) = multreal [;] (a,f)
proofend;
uniqueness
 for b1, b2 being Function of [:REAL,(Funcs (A,REAL)):],(Funcs (A,REAL)) st ( for a being Real
for f being Element of Funcs (A,REAL) holds b1 . (a,f) = multreal [;] (a,f) ) & ( for a being Real
for f being Element of Funcs (A,REAL) holds b2 . (a,f) = multreal [;] (a,f) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines RealFuncExtMult FUNCSDOM:def_3_:_
 for A being set
for b2 being Function of [:REAL,(Funcs (A,REAL)):],(Funcs (A,REAL)) holds
( b2 = RealFuncExtMult A iff for a being Real
for f being Element of Funcs (A,REAL) holds b2 . (a,f) = multreal [;] (a,f) );

definition
let A be set ;
func RealFuncZero A ->  Element of Funcs (A,REAL) equals :: FUNCSDOM:def 4
A --> 0;
coherence
 A --> 0 is Element of Funcs (A,REAL)
proofend;
end;

:: deftheorem  defines RealFuncZero FUNCSDOM:def_4_:_
 for A being set holds RealFuncZero A = A --> 0;

definition
let A be set ;
func RealFuncUnit A ->  Element of Funcs (A,REAL) equals :: FUNCSDOM:def 5
A --> 1;
coherence
 A --> 1 is Element of Funcs (A,REAL)
proofend;
end;

:: deftheorem  defines RealFuncUnit FUNCSDOM:def_5_:_
 for A being set holds RealFuncUnit A = A --> 1;

Lm1:  for A, B being non empty set
for x being Element of A
for f being Function of A,B holds x in dom f
proofend;

theorem Th1: :: FUNCSDOM:1
for A being non empty set
for h, f, g being Element of Funcs (A,REAL) holds
( h = (RealFuncAdd A) . (f,g) iff for x being Element of A holds h . x = (f . x) + (g . x) )
proofend;

theorem Th2: :: FUNCSDOM:2
for A being non empty set
for h, f, g being Element of Funcs (A,REAL) holds
( h = (RealFuncMult A) . (f,g) iff for x being Element of A holds h . x = (f . x) * (g . x) )
proofend;

theorem :: FUNCSDOM:3
for A being non empty set holds RealFuncZero A <> RealFuncUnit A
proofend;

theorem Th4: :: FUNCSDOM:4
for A being non empty set
for h, f being Element of Funcs (A,REAL)
for a being Real holds
( h = (RealFuncExtMult A) . [a,f] iff for x being Element of A holds h . x = a * (f . x) )
proofend;

theorem Th5: :: FUNCSDOM:5
for A being set
for f, g being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (f,g) = (RealFuncAdd A) . (g,f)
proofend;

theorem Th6: :: FUNCSDOM:6
for A being set
for f, g, h being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (f,((RealFuncAdd A) . (g,h))) = (RealFuncAdd A) . (((RealFuncAdd A) . (f,g)),h)
proofend;

theorem Th7: :: FUNCSDOM:7
for A being set
for f, g being Element of Funcs (A,REAL) holds (RealFuncMult A) . (f,g) = (RealFuncMult A) . (g,f)
proofend;

theorem Th8: :: FUNCSDOM:8
for A being set
for f, g, h being Element of Funcs (A,REAL) holds (RealFuncMult A) . (f,((RealFuncMult A) . (g,h))) = (RealFuncMult A) . (((RealFuncMult A) . (f,g)),h)
proofend;

theorem Th9: :: FUNCSDOM:9
for A being set
for f being Element of Funcs (A,REAL) holds (RealFuncMult A) . ((RealFuncUnit A),f) = f
proofend;

theorem Th10: :: FUNCSDOM:10
for A being set
for f being Element of Funcs (A,REAL) holds (RealFuncAdd A) . ((RealFuncZero A),f) = f
proofend;

theorem Th11: :: FUNCSDOM:11
for A being set
for f being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = RealFuncZero A
proofend;

theorem Th12: :: FUNCSDOM:12
for A being set
for f being Element of Funcs (A,REAL) holds (RealFuncExtMult A) . (1,f) = f
proofend;

theorem Th13: :: FUNCSDOM:13
for a, b being Real
for A being set
for f being Element of Funcs (A,REAL) holds (RealFuncExtMult A) . (a,((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a * b),f)
proofend;

theorem Th14: :: FUNCSDOM:14
for a, b being Real
for A being set
for f being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a + b),f)
proofend;

Lm2:  for a being Real
for A being set
for f, g being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (a,g))) = (RealFuncExtMult A) . (a,((RealFuncAdd A) . (f,g)))
proofend;

theorem Th15: :: FUNCSDOM:15
for A being set
for f, g, h being Element of Funcs (A,REAL) holds (RealFuncMult A) . (f,((RealFuncAdd A) . (g,h))) = (RealFuncAdd A) . (((RealFuncMult A) . (f,g)),((RealFuncMult A) . (f,h)))
proofend;

theorem Th16: :: FUNCSDOM:16
for A being set
for f, g, h being Element of Funcs (A,REAL)
for a being Real holds (RealFuncMult A) . (((RealFuncExtMult A) . (a,f)),g) = (RealFuncExtMult A) . (a,((RealFuncMult A) . (f,g)))
proofend;

theorem Th17: :: FUNCSDOM:17
for x1 being set
for A being non empty set ex f, g being Element of Funcs (A,REAL) st
( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) &amp; ( z <> x1 implies f . z = 0 ) ) ) &amp; ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) &amp; ( z <> x1 implies g . z = 1 ) ) ) )
proofend;

theorem Th18: :: FUNCSDOM:18
for x1, x2 being set
for A being non empty set
for f, g being Element of Funcs (A,REAL) st x1 in A &amp; x2 in A &amp; x1 <> x2 &amp; ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) &amp; ( z <> x1 implies f . z = 0 ) ) ) &amp; ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) &amp; ( z <> x1 implies g . z = 1 ) ) ) holds
for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 &amp; b = 0 )
proofend;

theorem :: FUNCSDOM:19
for x1, x2 being set
for A being non empty set st x1 in A &amp; x2 in A &amp; x1 <> x2 holds
ex f, g being Element of Funcs (A,REAL) st
for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 &amp; b = 0 )
proofend;

theorem Th20: :: FUNCSDOM:20
for x1, x2 being set
for A being non empty set
for f, g being Element of Funcs (A,REAL) st A = {x1,x2} &amp; x1 <> x2 &amp; ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) &amp; ( z <> x1 implies f . z = 0 ) ) ) &amp; ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) &amp; ( z <> x1 implies g . z = 1 ) ) ) holds
for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))
proofend;

theorem :: FUNCSDOM:21
for x1, x2 being set
for A being non empty set st A = {x1,x2} &amp; x1 <> x2 holds
ex f, g being Element of Funcs (A,REAL) st
for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))
proofend;

theorem Th22: :: FUNCSDOM:22
for x1, x2 being set
for A being non empty set st A = {x1,x2} &amp; x1 <> x2 holds
ex f, g being Element of Funcs (A,REAL) st
( ( for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 &amp; b = 0 ) ) &amp; ( for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) ) )
proofend;

definition
let A be set ;
func RealVectSpace A ->  strict RealLinearSpace equals :: FUNCSDOM:def 6
 RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #);
coherence
 RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is strict RealLinearSpace
proofend;
end;

:: deftheorem  defines RealVectSpace FUNCSDOM:def_6_:_
 for A being set holds RealVectSpace A = RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #);

theorem :: FUNCSDOM:23
ex V being strict RealLinearSpace ex u, v being Element of V st
( ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 &amp; b = 0 ) ) &amp; ( for w being Element of V ex a, b being Real st w = (a * u) + (b * v) ) )
proofend;

definition
let A be non empty set ;
func RRing A ->  strict doubleLoopStr  equals :: FUNCSDOM:def 7
 doubleLoopStr(# (Funcs (A,REAL)),(RealFuncAdd A),(RealFuncMult A),(RealFuncUnit A),(RealFuncZero A) #);
correctness
coherence
doubleLoopStr(# (Funcs (A,REAL)),(RealFuncAdd A),(RealFuncMult A),(RealFuncUnit A),(RealFuncZero A) #) is strict doubleLoopStr ;
;
end;

:: deftheorem  defines RRing FUNCSDOM:def_7_:_
 for A being non empty set holds RRing A = doubleLoopStr(# (Funcs (A,REAL)),(RealFuncAdd A),(RealFuncMult A),(RealFuncUnit A),(RealFuncZero A) #);

registration
let A be non empty set ;
cluster RRing A ->  non empty strict ;
coherence
 not RRing A is empty ;
end;

Lm3: now__::_thesis:_for_A_being_non_empty_set_
for_h,_a_being_Element_of_(RRing_A)_st_a_=_RealFuncUnit_A_holds_
(_h_*_a_=_h_&amp;_a_*_h_=_h_)
let A be non empty set ; ::_thesis: for h, a being Element of (RRing A) st a = RealFuncUnit A holds
( h * a = h &amp; a * h = h )
set FR = RRing A;
let h, a be Element of (RRing A); ::_thesis: ( a = RealFuncUnit A implies ( h * a = h &amp; a * h = h ) )
reconsider g = h as Element of Funcs (A,REAL) ;
assume A1: a = RealFuncUnit A ; ::_thesis: ( h * a = h &amp; a * h = h )
hence h * a = (RealFuncMult A) . ((RealFuncUnit A),g) by Th7
.= h by Th9 ;
::_thesis: a * h = h
thus  a * h = h by A1, Th9; ::_thesis: verum
end;

registration
let A be non empty set ;
cluster RRing A ->  strict unital ;
coherence
 RRing A is unital
proofend;
end;

theorem :: FUNCSDOM:24
for A being non empty set holds 1. (RRing A) = RealFuncUnit A ;

theorem Th25: :: FUNCSDOM:25
for A being non empty set
for x, y, z being Element of (RRing A) holds
( x + y = y + x &amp; (x + y) + z = x + (y + z) &amp; x + (0. (RRing A)) = x &amp; ex t being Element of (RRing A) st x + t = 0. (RRing A) &amp; x * y = y * x &amp; (x * y) * z = x * (y * z) &amp; x * (1. (RRing A)) = x &amp; (1. (RRing A)) * x = x &amp; x * (y + z) = (x * y) + (x * z) &amp; (y + z) * x = (y * x) + (z * x) )
proofend;

registration
cluster non empty trivial V52() 1 -element right_complementable strict associative commutative right-distributive right_unital Abelian add-associative right_zeroed for doubleLoopStr ;
existence
 ex b1 being 1 -element doubleLoopStr st
( b1 is strict &amp; b1 is Abelian &amp; b1 is add-associative &amp; b1 is right_zeroed &amp; b1 is right_complementable &amp; b1 is associative &amp; b1 is commutative &amp; b1 is right_unital &amp; b1 is right-distributive )
proofend;
end;

definition
mode Ring is non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
end;

theorem :: FUNCSDOM:26
for A being non empty set holds RRing A is commutative Ring
proofend;

definition
attrc1 is strict ;
struct AlgebraStr  ->  doubleLoopStr , RLSStruct ;
aggrAlgebraStr(# carrier, multF, addF, Mult, OneF, ZeroF #) ->  AlgebraStr ;
end;

registration
cluster non empty for AlgebraStr ;
existence
 not for b1 being AlgebraStr holds b1 is empty
proofend;
end;

definition
let A be set ;
func RAlgebra A ->  strict AlgebraStr  equals :: FUNCSDOM:def 8
 AlgebraStr(# (Funcs (A,REAL)),(RealFuncMult A),(RealFuncAdd A),(RealFuncExtMult A),(RealFuncUnit A),(RealFuncZero A) #);
correctness
coherence
AlgebraStr(# (Funcs (A,REAL)),(RealFuncMult A),(RealFuncAdd A),(RealFuncExtMult A),(RealFuncUnit A),(RealFuncZero A) #) is strict AlgebraStr ;
;
end;

:: deftheorem  defines RAlgebra FUNCSDOM:def_8_:_
 for A being set holds RAlgebra A = AlgebraStr(# (Funcs (A,REAL)),(RealFuncMult A),(RealFuncAdd A),(RealFuncExtMult A),(RealFuncUnit A),(RealFuncZero A) #);

registration
let A be non empty set ;
cluster RAlgebra A ->  non empty strict ;
coherence
 not RAlgebra A is empty ;
end;

Lm4: now__::_thesis:_for_A_being_non_empty_set_
for_x,_e_being_Element_of_(RAlgebra_A)_st_e_=_RealFuncUnit_A_holds_
(_x_*_e_=_x_&amp;_e_*_x_=_x_)
let A be non empty set ; ::_thesis: for x, e being Element of (RAlgebra A) st e = RealFuncUnit A holds
( x * e = x &amp; e * x = x )
set F = RAlgebra A;
let x, e be Element of (RAlgebra A); ::_thesis: ( e = RealFuncUnit A implies ( x * e = x &amp; e * x = x ) )
reconsider f = x as Element of Funcs (A,REAL) ;
assume A1: e = RealFuncUnit A ; ::_thesis: ( x * e = x &amp; e * x = x )
hence x * e = (RealFuncMult A) . ((RealFuncUnit A),f) by Th7
.= x by Th9 ;
::_thesis: e * x = x
thus  e * x = x by A1, Th9; ::_thesis: verum
end;

registration
let A be non empty set ;
cluster RAlgebra A ->  unital strict ;
coherence
 RAlgebra A is unital
proofend;
end;

theorem :: FUNCSDOM:27
for A being non empty set holds 1. (RAlgebra A) = RealFuncUnit A ;

definition
let IT be non empty AlgebraStr ;
attrIT is vector-associative  means :: FUNCSDOM:def 9
 for x, y being Element of IT
for a being Real holds a * (x * y) = (a * x) * y;
end;

:: deftheorem  defines vector-associative FUNCSDOM:def_9_:_
 for IT being non empty AlgebraStr holds
( IT is vector-associative iff for x, y being Element of IT
for a being Real holds a * (x * y) = (a * x) * y );

registration
let A be set ;
cluster RAlgebra A ->  non empty strict ;
coherence
 not RAlgebra A is empty ;
end;

registration
let A be set ;
cluster RAlgebra A ->  right_complementable associative commutative right-distributive right_unital Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative strict vector-associative ;
coherence
 ( RAlgebra A is strict &amp; RAlgebra A is Abelian &amp; RAlgebra A is add-associative &amp; RAlgebra A is right_zeroed &amp; RAlgebra A is right_complementable &amp; RAlgebra A is commutative &amp; RAlgebra A is associative &amp; RAlgebra A is right_unital &amp; RAlgebra A is right-distributive &amp; RAlgebra A is vector-associative &amp; RAlgebra A is scalar-associative &amp; RAlgebra A is vector-distributive &amp; RAlgebra A is scalar-distributive )
proofend;
end;

registration
cluster non empty right_complementable associative commutative right-distributive right_unital Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative strict vector-associative for AlgebraStr ;
existence
 ex b1 being non empty AlgebraStr st
( b1 is strict &amp; b1 is Abelian &amp; b1 is add-associative &amp; b1 is right_zeroed &amp; b1 is right_complementable &amp; b1 is commutative &amp; b1 is associative &amp; b1 is right_unital &amp; b1 is right-distributive &amp; b1 is vector-associative &amp; b1 is scalar-associative &amp; b1 is vector-distributive &amp; b1 is scalar-distributive )
proofend;
end;

definition
mode Algebra is non empty right_complementable associative commutative right-distributive right_unital Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr ;
end;