:: Real Functions Spaces
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Copyright (c) 1990-2021 Association of Mizar Users

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 func F . (f,g) -> Element of Funcs (A,B);
coherence
F . (f,g) is Element of Funcs (A,B)
proof end;
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 func F . cd -> Element of Funcs (A,B);
coherence
F . cd is Element of Funcs (A,B)
proof end;
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 func F .: (f,g) -> Element of Funcs (Z,X);
coherence
F .: (f,g) is Element of Funcs (Z,X)
proof end;
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 func F [;] (a,f) -> Element of Funcs (Z,X);
coherence
F [;] (a,f) is Element of Funcs (Z,X)
proof end;
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)
proof end;
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
proof end;
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) );

registration
let A be set ;
coherence
proof end;
end;

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)
proof end;
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
proof end;
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) );

registration
let A be set ;
coherence
proof end;
end;

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)
proof end;
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
proof end;
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) );

registration
let A be set ;
coherence
proof end;
end;

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

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)
proof end;
func RealFuncUnit A -> Element of Funcs (A,REAL) equals :: FUNCSDOM:def 5
A --> 1;
coherence
A --> 1 is Element of Funcs (A,REAL)
proof end;
end;

:: deftheorem defines RealFuncZero FUNCSDOM:def 4 :
for A being set holds RealFuncZero A = A --> 0;

:: deftheorem defines RealFuncUnit FUNCSDOM:def 5 :
for A being set holds RealFuncUnit A = A --> 1;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

proof end;

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

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

theorem Th17: :: FUNCSDOM:17
for x1 being set
for A being non empty set st x1 in A holds
( () +* (x1 .--> 1) in Funcs (A,REAL) & () +* (x1 .--> 0) in Funcs (A,REAL) )
proof end;

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 & x2 in A & x1 <> x2 & f = () +* (x1 .--> 1) & g = () +* (x1 .--> 0) holds
for a, b being Real st () . ((() . [a,f]),(() . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 )
proof end;

theorem :: FUNCSDOM:19
canceled;

::$CT 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} & x1 <> x2 & f = () +* (x1 .--> 1) & g = () +* (x1 .--> 0) holds for h being Element of Funcs (A,REAL) ex a, b being Real st h = () . ((() . [a,f]),(() . [b,g])) proof end; theorem :: FUNCSDOM:21 canceled; ::$CT
theorem Th22: :: FUNCSDOM:22
for x1, x2 being set
for A being non empty set st A = {x1,x2} & x1 <> x2 holds
ex f, g being Element of Funcs (A,REAL) st
( ( for a, b being Real st () . ((() . [a,f]),(() . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,REAL) ex a, b being Real st h = () . ((() . [a,f]),(() . [b,g])) ) )
proof end;

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

:: deftheorem defines RealVectSpace FUNCSDOM:def 6 :
for A being set holds RealVectSpace A = RLSStruct(# (Funcs (A,REAL)),(),(),() #);

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 & b = 0 ) ) & ( for w being Element of V ex a, b being Real st w = (a * u) + (b * v) ) )
proof end;

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

:: deftheorem defines RRing FUNCSDOM:def 7 :
for A being non empty set holds RRing A = doubleLoopStr(# (Funcs (A,REAL)),(),(),(),() #);

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 () st a = RealFuncUnit A holds
( h * a = h & a * h = h )
let A be non empty set ; :: thesis: for h, a being Element of () st a = RealFuncUnit A holds
( h * a = h & a * h = h )

set FR = RRing A;
let h, a be Element of (); :: thesis: ( a = RealFuncUnit A implies ( h * a = h & a * h = h ) )
reconsider g = h as Element of Funcs (A,REAL) ;
assume A1: a = RealFuncUnit A ; :: thesis: ( h * a = h & a * h = h )
hence h * a = () . ((),g) by Th7
.= h by Th9 ;
:: thesis: a * h = h
thus a * h = h by ; :: thesis: verum
end;

registration
let A be non empty set ;
coherence
RRing A is unital
proof end;
end;

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

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

registration
existence
ex b1 being 1 -element doubleLoopStr st
( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is associative & b1 is commutative & b1 is right_unital & b1 is right-distributive )
proof end;
end;

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

definition end;

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

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

:: deftheorem defines RAlgebra FUNCSDOM:def 8 :
for A being set holds RAlgebra A = AlgebraStr(# (Funcs (A,REAL)),(),(),(),(),() #);

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 () st e = RealFuncUnit A holds
( x * e = x & e * x = x )
let A be non empty set ; :: thesis: for x, e being Element of () st e = RealFuncUnit A holds
( x * e = x & e * x = x )

set F = RAlgebra A;
let x, e be Element of (); :: thesis: ( e = RealFuncUnit A implies ( x * e = x & e * x = x ) )
reconsider f = x as Element of Funcs (A,REAL) ;
assume A1: e = RealFuncUnit A ; :: thesis: ( x * e = x & e * x = x )
hence x * e = () . ((),f) by Th7
.= x by Th9 ;
:: thesis: e * x = x
thus e * x = x by ; :: thesis: verum
end;

registration
let A be non empty set ;
coherence
proof end;
end;

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

definition
let IT be non empty AlgebraStr ;
attr IT 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 ;
coherence
proof end;
end;

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

definition end;

theorem :: FUNCSDOM:28
for A being non empty set
for f, g being Element of Funcs (A,REAL) holds () . (f,g) = f + g
proof end;

theorem :: FUNCSDOM:29
for A being non empty set
for f, g being Element of Funcs (A,REAL) holds () . (f,g) = f (#) g
proof end;

theorem :: FUNCSDOM:30
for A being non empty set
for f being Element of Funcs (A,REAL)
for a being Real holds () . (a,f) = a (#) f
proof end;