:: Real Functions Spaces
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received March 23, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, BINOP_1, FUNCT_2, SUBSET_1, FUNCT_1, ZFMISC_1, NUMBERS,
RELAT_1, FUNCOP_1, BINOP_2, REAL_1, CARD_1, ARYTM_3, RLVECT_1, ARYTM_1,
STRUCT_0, ALGSTR_0, SUPINF_2, GROUP_1, MESFUNC1, VECTSP_1, LATTICES,
TARSKI, FUNCSDOM, VALUED_1, VALUED_2, VALUED_0, FUNCT_7, FUNCT_4;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1,
MEMBERED, FUNCT_1, FUNCT_2, BINOP_1, FUNCT_4, DOMAIN_1, FUNCOP_1,
BINOP_2, XCMPLX_0, XREAL_0, VALUED_0, VALUED_1, VALUED_2, STRUCT_0,
ALGSTR_0, RLVECT_1, REAL_1, GROUP_1, VECTSP_1, PARTFUN3;
constructors BINOP_1, DOMAIN_1, FUNCOP_1, REAL_1, BINOP_2, VECTSP_1, RLVECT_1,
FUNCT_3, RELSET_1, VALUED_2, VALUED_0, VALUED_1, NUMBERS, GROUP_1,
PARTFUN3, FUNCT_4;
registrations XBOOLE_0, SUBSET_1, RELSET_1, NUMBERS, RLVECT_1, VECTSP_1,
ALGSTR_0, BINOP_2, FUNCOP_1, FUNCT_3, XREAL_0, RELAT_1, VALUED_0,
STRUCT_0, MEMBERED;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
definitions RLVECT_1, STRUCT_0, GROUP_1, VECTSP_1, ALGSTR_0, FUNCT_2,
VALUED_2;
equalities RLVECT_1, STRUCT_0, BINOP_1, ALGSTR_0, FUNCOP_1;
expansions RLVECT_1, GROUP_1, BINOP_1, VECTSP_1, FUNCT_2;
theorems FUNCT_2, FUNCOP_1, TARSKI, BINOP_2, STRUCT_0, XREAL_0, PARTFUN1,
FUNCT_1, VALUED_1, ZFMISC_1, FUNCT_4, XBOOLE_1, RELAT_1;
schemes BINOP_1;
begin
reserve x1,x2,z for set;
reserve A,B for non empty set;
definition
let A be set, B be non empty set;
let F be BinOp of Funcs(A,B);
let f,g be Element of Funcs(A,B);
redefine func F.(f,g) -> Element of Funcs(A,B); :: redefines . (BINOP_1, definition)
coherence
proof
reconsider f,g as Element of Funcs(A,B) qua non empty set;
F.(f,g) is Element of Funcs(A,B);
hence thesis;
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:];
redefine func F.cd -> Element of Funcs(A,B); :: redefines . (FUNCT_1, definition)
coherence
proof
F.cd is Element of Funcs(A,B);
hence thesis;
end;
end;
reserve f,g,h for Element of Funcs(A,REAL);
definition
let X be non empty set, Z be set;
let F be (BinOp of X), f,g be Function of Z,X;
redefine func F.:(f,g) -> Element of Funcs(Z,X); :: redefines .: (FUNCOP_1, definition)
coherence
proof
F.:(f,g) in Funcs(Z,X) by FUNCT_2:8;
hence thesis;
end;
end;
definition
let X be non empty set, Z be set;
let F be (BinOp of X),a be Element of X,f be Function of Z,X;
redefine func F[;](a,f) -> Element of Funcs(Z,X); :: redefines [;] (FUNCOP_1, definition)
coherence
proof
F[;](a,f) in Funcs(Z,X) by FUNCT_2:8;
hence thesis;
end;
end;
definition let A be set;
func RealFuncAdd(A) -> BinOp of Funcs(A,REAL) means :Def1:
for f,g being Element of Funcs(A,REAL) holds it.(f,g) = addreal.:(f,g);
existence
proof
deffunc F(Element of Funcs(A,REAL),Element of Funcs(A,REAL)) = addreal.:(
$1,$2);
consider F being BinOp of Funcs(A,REAL) such that
A1: for x,y being Element of Funcs(A,REAL) holds F.(x,y) = F(x,y) from
BINOP_1:sch 4;
take F;
let f,g be Element of Funcs(A,REAL);
thus thesis by A1;
end;
uniqueness
proof
let it1,it2 be BinOp of Funcs(A,REAL) such that
A2: for f,g being Element of Funcs(A,REAL) holds it1.(f,g) = addreal.:
(f,g) and
A3: for f,g being Element of Funcs(A,REAL) holds it2.(f,g) = addreal.: (f,g);
now
let f,g be Element of Funcs(A,REAL);
thus it1.(f,g) = addreal.:(f,g) by A2
.= it2.(f,g) by A3;
end;
hence thesis;
end;
end;
registration let A be set;
cluster RealFuncAdd A -> real-functions-valued;
coherence
proof let x be object;
set IT = RealFuncAdd A;
assume x in dom IT;
then IT.x is Function of A,REAL by FUNCT_2:66,PARTFUN1:4;
hence IT.x is real-valued Function;
end;
end;
definition let A be set;
func RealFuncMult(A) -> BinOp of Funcs(A,REAL) means :Def2:
for f,g being Element of Funcs(A,REAL) holds it.(f,g) = multreal.:(f,g);
existence
proof
deffunc F(Element of Funcs(A,REAL),Element of Funcs(A,REAL)) = multreal.:(
$1,$2);
consider F being BinOp of Funcs(A,REAL) such that
A1: for x,y being Element of Funcs(A,REAL) holds F.(x,y) = F(x,y) from
BINOP_1:sch 4;
take F;
let f,g be Element of Funcs(A,REAL);
thus thesis by A1;
end;
uniqueness
proof
let it1,it2 be BinOp of Funcs(A,REAL) such that
A2: for f,g being Element of Funcs(A,REAL) holds it1.(f,g) = multreal
.:(f,g) and
A3: for f,g being Element of Funcs(A,REAL) holds it2.(f,g) = multreal .:(f,g);
now
let f,g be Element of Funcs(A,REAL);
thus it1.(f,g) = multreal.:(f,g) by A2
.=it2.(f,g) by A3;
end;
hence thesis;
end;
end;
registration let A be set;
cluster RealFuncMult A -> real-functions-valued;
coherence
proof let x be object;
set IT = RealFuncMult A;
assume x in dom IT;
then IT.x is Function of A,REAL by FUNCT_2:66,PARTFUN1:4;
hence IT.x is real-valued Function;
end;
end;
definition let A be set;
func RealFuncExtMult(A) -> Function of [:REAL,Funcs(A,REAL):],Funcs(A,REAL)
means :Def3:
for a being Real, f being Element of Funcs(A,REAL) holds
it.(a,f) = multreal[;](a,f);
existence
proof
deffunc F(Element of REAL,Element of Funcs(A,REAL)) = (multreal[;]($1,$2));
consider F being Function of [:REAL,Funcs(A,REAL):],Funcs(A,REAL) such
that
A1: for a being Element of REAL, f being Element of Funcs(A,REAL)
holds F.(a,f) = F(a,f) from BINOP_1:sch 4;
take F;
let a be Real, f be Element of Funcs(A,REAL);
a in REAL by XREAL_0:def 1;
hence thesis by A1;
end;
uniqueness
proof
let it1,it2 be Function of [:REAL,Funcs(A,REAL):],Funcs(A,REAL) such that
A2: for a being Real, f being Element of Funcs(A,REAL) holds it1.(a,f)
= multreal[;](a,f) and
A3: for a being Real, f being Element of Funcs(A,REAL) holds it2.(a,f)
= multreal[;](a,f);
now
let a be Element of REAL, f be Element of Funcs(A,REAL);
thus it1.(a,f) = multreal[;](a,f) by A2
.= it2.(a,f) by A3;
end;
hence thesis;
end;
end;
registration let A be set;
cluster RealFuncExtMult A -> real-functions-valued;
coherence
proof let x be object;
set IT = RealFuncExtMult A;
assume x in dom IT;
then IT.x is Function of A,REAL by FUNCT_2:66,PARTFUN1:4;
hence IT.x is real-valued Function;
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
A --> 0;
coherence
proof
A --> In(0,REAL) is Function of A,REAL;
hence thesis by FUNCT_2:8;
end;
func RealFuncUnit A -> Element of Funcs(A,REAL) equals
A --> 1;
coherence
proof
A --> jj is Function of A,REAL;
hence thesis by FUNCT_2:8;
end;
end;
theorem Th1:
h = (RealFuncAdd A).(f,g) iff for x being Element of A holds h.x = f.x + g.x
proof
A1: now
assume
A2: for x being Element of A holds h.x=f.x + g.x;
now
let x be Element of A;
A3: dom (addreal.:(f,g)) = A by FUNCT_2:def 1;
thus ((RealFuncAdd A).(f,g)).x = (addreal.:(f,g)).x by Def1
.= addreal.(f.x,g.x) by A3,FUNCOP_1:22
.= f.x + g.x by BINOP_2:def 9
.= h.x by A2;
end;
hence h = (RealFuncAdd A).(f,g);
end;
now
assume
A4: h = (RealFuncAdd A).(f,g);
let x be Element of A;
A5: dom (addreal.:(f,g)) = A by FUNCT_2:def 1;
thus h.x = (addreal.:(f,g)).x by A4,Def1
.= addreal.(f.x,g.x) by A5,FUNCOP_1:22
.= f.x + g.x by BINOP_2:def 9;
end;
hence thesis by A1;
end;
theorem Th2:
h = (RealFuncMult(A)).(f,g) iff for x being Element of A holds
h.x = f.x * g.x
proof
A1: now
assume
A2: for x being Element of A holds h.x=f.x * g.x;
now
let x be Element of A;
A3: dom (multreal.:(f,g)) = A by FUNCT_2:def 1;
thus ((RealFuncMult(A)).(f,g)).x = (multreal.:(f,g)).x by Def2
.= multreal.(f.x,g.x) by A3,FUNCOP_1:22
.= f.x * g.x by BINOP_2:def 11
.= h.x by A2;
end;
hence h = (RealFuncMult(A)).(f,g);
end;
now
assume
A4: h = (RealFuncMult(A)).(f,g);
let x be Element of A;
A5: dom (multreal.:(f,g)) = A by FUNCT_2:def 1;
thus h.x = (multreal.:(f,g)).x by A4,Def2
.= multreal.(f.x,g.x) by A5,FUNCOP_1:22
.= f.x * g.x by BINOP_2:def 11;
end;
hence thesis by A1;
end;
theorem
RealFuncZero(A) <> RealFuncUnit(A)
proof
set a = the Element of A;
(RealFuncZero(A)).a=0;
hence thesis by FUNCOP_1:7;
end;
reserve a,b for Real;
theorem Th4:
h = (RealFuncExtMult A).[a,f] iff
for x being Element of A holds h.x = a*(f.x)
proof
reconsider aa=a as Element of REAL by XREAL_0:def 1;
thus h = (RealFuncExtMult A).[a,f] implies for x being Element of A holds h.
x = a*(f.x)
proof
assume
A1: h = (RealFuncExtMult A).[a,f];
let x be Element of A;
h = (RealFuncExtMult A).(a,f) by A1;
hence h.x = (multreal[;](aa,f)).x by Def3
.= multreal.(aa,f.x) by FUNCOP_1:53
.= a*(f.x) by BINOP_2:def 11;
end;
now
assume
A2: for x being Element of A holds h.x = a*(f.x);
for x being Element of A holds h.x = ((RealFuncExtMult A).[aa,f]).x
proof
let x be Element of A;
A3: multreal[;](a,f) = (RealFuncExtMult A).(a,f) by Def3;
thus h.x = a*(f.x) by A2
.= multreal.(a,f.x) by BINOP_2:def 11
.= ((RealFuncExtMult A).[aa,f]).x by A3,FUNCOP_1:53;
end;
hence h = (RealFuncExtMult A).(a,f) by FUNCT_2:63;
end;
hence thesis;
end;
theorem Th5:
for A being set, f,g being Element of Funcs(A,REAL) holds
(RealFuncAdd A).(f,g) = (RealFuncAdd A).(g,f)
proof
let A be set, f,g be Element of Funcs(A,REAL);
thus (RealFuncAdd A).(f,g) = addreal.:(f,g) by Def1
.= addreal.:(g,f) by FUNCOP_1:65
.= (RealFuncAdd A).(g,f) by Def1;
end;
theorem Th6:
for A being set, f,g,h being Element of Funcs(A,REAL) holds
(RealFuncAdd A).(f,(RealFuncAdd A).(g,h)) =
(RealFuncAdd A).((RealFuncAdd A).(f,g),h)
proof
let A be set, f,g,h be Element of Funcs(A,REAL);
thus (RealFuncAdd A).(f,(RealFuncAdd A).(g,h))
= (RealFuncAdd A).(f,addreal.:(g,h)) by Def1
.= addreal.:(f,addreal.:(g,h)) by Def1
.= addreal.:(addreal.:(f,g),h) by FUNCOP_1:61
.= (RealFuncAdd A).(addreal.:(f,g),h) by Def1
.= (RealFuncAdd A).((RealFuncAdd A).(f,g),h) by Def1;
end;
theorem Th7:
for A be set, f,g be Element of Funcs(A,REAL) holds
(RealFuncMult A).(f,g) = (RealFuncMult A).(g,f)
proof let A be set, f,g be Element of Funcs(A,REAL);
thus (RealFuncMult A).(f,g) = multreal.:(f,g) by Def2
.= multreal.:(g,f) by FUNCOP_1:65
.= (RealFuncMult A).(g,f) by Def2;
end;
theorem Th8:
for A be set, f,g,h be Element of Funcs(A,REAL) holds
(RealFuncMult(A)).(f,(RealFuncMult(A)).(g,h)) =
(RealFuncMult(A)).((RealFuncMult(A)).(f,g),h)
proof
let A be set, f,g,h be Element of Funcs(A,REAL);
thus (RealFuncMult A).(f,(RealFuncMult A).(g,h))
= (RealFuncMult A).(f,multreal.:(g,h)) by Def2
.= multreal.:(f,multreal.:(g,h)) by Def2
.= multreal.:(multreal.:(f,g),h) by FUNCOP_1:61
.= (RealFuncMult A).(multreal.:(f,g),h) by Def2
.= (RealFuncMult A).((RealFuncMult A).(f,g),h) by Def2;
end;
theorem Th9:
for A being set, f being Element of Funcs(A,REAL) holds
(RealFuncMult(A)).(RealFuncUnit(A),f) = f
proof
let A be set, f being Element of Funcs(A,REAL);
per cases;
suppose A = {}; then
A1: f = {};
thus (RealFuncMult A).(RealFuncUnit(A),f)
= multreal.:(RealFuncUnit(A),f) by Def2
.= f by A1;
end;
suppose
A <> {};
then reconsider A as non empty set;
reconsider f as Element of Funcs(A,REAL);
now
let x be Element of A;
thus ((RealFuncMult A).(RealFuncUnit(A),f)).x
= (RealFuncUnit(A)).x * f.x by Th2
.= 1 * f.x
.= f.x;
end;
hence thesis;
end;
end;
theorem Th10:
for A being set, f being Element of Funcs(A,REAL) holds
(RealFuncAdd A).(RealFuncZero(A),f) = f
proof
let A be set, f be Element of Funcs(A,REAL);
per cases;
suppose A = {}; then
A1: f = {};
thus (RealFuncAdd A).(RealFuncZero(A),f) = addreal.:(RealFuncZero(A),f) by
Def1
.= f by A1;
end;
suppose
A <> {};
then reconsider A as non empty set;
reconsider f as Element of Funcs(A,REAL);
now
let x be Element of A;
thus ((RealFuncAdd A).(RealFuncZero(A),f)).x = (RealFuncZero(A)).x + f.x
by Th1
.= 0 + f.x
.= f.x;
end;
hence thesis;
end;
end;
theorem Th11:
for A being set, f be Element of Funcs(A,REAL) holds
(RealFuncAdd A).(f,(RealFuncExtMult A).[-1,f]) = RealFuncZero(A)
proof
let A be set, f be Element of Funcs(A,REAL);
per cases;
suppose
A1: A = {};
then (RealFuncAdd A).(f,(RealFuncExtMult A).[-jj,f]) = {}
.= RealFuncZero(A) by A1;
hence thesis;
end;
suppose
A <> {};
then reconsider A as non empty set;
reconsider f as Element of Funcs(A,REAL);
now
let x be Element of A;
set y=f.x;
thus ((RealFuncAdd A).(f,(RealFuncExtMult A).[-jj,f])).x = f.x + ((
RealFuncExtMult A).[-jj,f]).x by Th1
.= f.x + ((-1)*y) by Th4
.= (RealFuncZero(A)).x;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem Th12:
for A being set, f being Element of Funcs(A,REAL) holds
(RealFuncExtMult A).(1,f) = f
proof
let A be set, f be Element of Funcs(A,REAL);
per cases;
suppose A = {}; then
A1: f = {};
thus (RealFuncExtMult A).(1,f) = multreal[;](jj,f) by Def3
.= f by A1;
end;
suppose A <> {};
then reconsider A as non empty set;
reconsider f as Element of Funcs(A,REAL);
reconsider g = (RealFuncExtMult A).(jj,f) as Element of Funcs(A,REAL);
now
let x be Element of A;
thus g.x = jj*(f.x) by Th4
.= f.x;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem Th13:
for A being set, f being Element of Funcs(A,REAL) holds
(RealFuncExtMult A).(a,(RealFuncExtMult A).(b,f)) =
(RealFuncExtMult A).(a*b,f)
proof
let A be set, f be Element of Funcs(A,REAL);
reconsider aa=a, bb=b as Element of REAL by XREAL_0:def 1;
per cases;
suppose
A1: A = {};
(RealFuncExtMult A).(b,f) = multreal[;](b,f) by Def3;
hence (RealFuncExtMult A).(a,(RealFuncExtMult A).(b,f))
= multreal[;](aa,multreal[;](bb,f)) by Def3
.= multreal[;](a*b,f) by A1
.= (RealFuncExtMult A).(a*b,f) by Def3;
end;
suppose
A <> {};
then reconsider A as non empty set;
reconsider f as Element of Funcs(A,REAL);
now
let x be Element of A;
thus ((RealFuncExtMult A).[aa,(RealFuncExtMult A).[bb,f]]).x
= aa*(((RealFuncExtMult A).[bb,f]).x) by Th4
.= aa*(bb*(f.x)) by Th4
.= (aa*bb)*(f.x)
.= ((RealFuncExtMult A).[aa*bb,f]).x by Th4;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem Th14:
for A being set, f being Element of Funcs(A,REAL) holds
(RealFuncAdd A).((RealFuncExtMult A).(a,f),(RealFuncExtMult A).(b,f)) =
(RealFuncExtMult A).(a+b,f)
proof
let A be set, f be Element of Funcs(A,REAL);
reconsider aa=a, bb=b as Element of REAL by XREAL_0:def 1;
per cases;
suppose
A1: A = {};
thus
(RealFuncAdd A).((RealFuncExtMult A).(a,f),(RealFuncExtMult A).(b,f)) =
(RealFuncAdd A).((RealFuncExtMult A).(aa,f),(RealFuncExtMult A).(bb,f))
.= {} by A1
.= multreal[;](a+b,f) by A1
.= (RealFuncExtMult A).(a+b,f) by Def3;
end;
suppose
A <> {};
then reconsider A as non empty set;
reconsider f as Element of Funcs(A,REAL);
now
let x be Element of A;
thus ((RealFuncAdd A). ((RealFuncExtMult A).[aa,f],
(RealFuncExtMult A).[bb,f])).x =
((RealFuncExtMult A).[aa,f]).x + ((RealFuncExtMult A).[bb,f]).x
by Th1
.= a*(f.x) + ((RealFuncExtMult A).[bb,f]).x by Th4
.= a*(f.x) + b*(f.x) by Th4
.= (a+b)*(f.x)
.= ((RealFuncExtMult A).[aa+bb,f]).x by Th4;
end;
hence thesis by FUNCT_2:63;
end;
end;
Lm2: for A being set, 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))
proof
let A be set, f,g be Element of Funcs(A,REAL);
reconsider aa=a as Element of REAL by XREAL_0:def 1;
per cases;
suppose
A1: A = {};
thus
(RealFuncAdd A).((RealFuncExtMult A).(a,f),(RealFuncExtMult A).(a,g)) =
(RealFuncAdd A).((RealFuncExtMult A).(aa,f),(RealFuncExtMult A).(aa,g))
.= {} by A1
.= multreal[;](a,(RealFuncAdd A).(f,g)) by A1
.= (RealFuncExtMult A).(a,(RealFuncAdd A).(f,g)) by Def3;
end;
suppose
A <> {};
then reconsider A as non empty set;
reconsider f,g as Element of Funcs(A,REAL);
now
let x be Element of A;
thus ((RealFuncAdd A). ((RealFuncExtMult A).[aa,f],
(RealFuncExtMult A).[aa,g])).x =
((RealFuncExtMult A).[aa,f]).x + ((RealFuncExtMult A).[aa,g]).x
by Th1
.= a*(f.x) + ((RealFuncExtMult A).[aa,g]).x by Th4
.= a*(f.x) + a*(g.x) by Th4
.= a*(f.x + g.x)
.= a*(((RealFuncAdd A).(f,g)).x) by Th1
.= ((RealFuncExtMult A).[aa,(RealFuncAdd A).(f,g)]).x by Th4;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem Th15:
for A be set, f,g,h be Element of Funcs(A,REAL) holds
(RealFuncMult(A)).(f,(RealFuncAdd A).(g,h)) =
(RealFuncAdd A).((RealFuncMult(A)).(f,g),(RealFuncMult(A)).(f,h))
proof
let A be set, f,g,h be Element of Funcs(A,REAL);
A1: multreal.:(f,addreal.:(g,h)) = addreal.:(multreal.:(f,g),multreal.:(f,h))
proof let a be Element of A;
per cases;
suppose A = {};
hence (multreal.:(f,addreal.:(g,h))).a
= (addreal.:(multreal.:(f,g),multreal.:(f,h))).a;
end;
suppose A <> {};
then reconsider B=A as non empty set;
reconsider ff=f, gg=g, hh=h as Element of Funcs(B,REAL);
reconsider b = a as Element of B;
thus (multreal.:(f,addreal.:(g,h))).a
= multreal.(f.b,addreal.:(g,h).b) by FUNCOP_1:37
.= multreal.(f.b,addreal.(g.b,h.b)) by FUNCOP_1:37
.= ff.b * addreal.(gg.b,hh.b) by BINOP_2:def 11
.= ff.b * (gg.b + hh.b) by BINOP_2:def 9
.= (ff.b * gg.b) + (ff.b * hh.b)
.= (ff.b * gg.b) + multreal.(ff.b,hh.b) by BINOP_2:def 11
.= multreal.(ff.b,gg.b) + multreal.(ff.b,hh.b) by BINOP_2:def 11
.= addreal.(multreal.(f.a,g.a),multreal.(f.a,h.a)) by BINOP_2:def 9
.= addreal.(multreal.(f.a,g.a),multreal.:(ff,h).a) by FUNCOP_1:37
.= addreal.(multreal.:(ff,g).a,multreal.:(ff,h).a) by FUNCOP_1:37
.= (addreal.:(multreal.:(f,g),multreal.:(f,h))).a by FUNCOP_1:37;
end;
end;
thus (RealFuncMult(A)).(f,(RealFuncAdd A).(g,h))
= (RealFuncMult(A)).(f,addreal.:(g,h)) by Def1
.= addreal.:(multreal.:(f,g),multreal.:(f,h)) by A1,Def2
.= (RealFuncAdd A).(multreal.:(f,g),multreal.:(f,h)) by Def1
.= (RealFuncAdd A).((RealFuncMult(A)).(f,g),multreal.:(f,h)) by Def2
.= (RealFuncAdd A).((RealFuncMult A).(f,g),(RealFuncMult A).(f,h)) by Def2;
end;
theorem Th16:
for A being set, f,g,h be Element of Funcs(A,REAL), a being Real holds
(RealFuncMult A).((RealFuncExtMult A).(a,f),g)
= (RealFuncExtMult A).(a,(RealFuncMult A).(f,g))
proof
let A be set, f,g,h be Element of Funcs(A,REAL), a be Real;
reconsider aa=a as Element of REAL by XREAL_0:def 1;
thus (RealFuncMult A).((RealFuncExtMult A).(a,f),g)
= (RealFuncMult A).(multreal[;](a,f),g) by Def3
.= multreal.:(multreal[;](aa,f),g) by Def2
.= multreal[;](aa,multreal.:(f,g)) by FUNCOP_1:85
.= (RealFuncExtMult A).(a,multreal.:(f,g)) by Def3
.= (RealFuncExtMult A).(a,(RealFuncMult A).(f,g)) by Def2;
end;
theorem Th17:
x1 in A implies
(RealFuncZero A) +* (x1 .--> 1) in Funcs (A,REAL) &
(RealFuncUnit A) +* (x1 .--> 0) in Funcs (A,REAL)
proof
assume a0: x1 in A;
A2: dom ((RealFuncZero A) +* (x1 .--> 1)) =
dom RealFuncZero A \/ dom (x1 .--> 1) by FUNCT_4:def 1
.= dom RealFuncZero A \/ {x1}
.= A \/ {x1}
.= A by a0,XBOOLE_1:12,ZFMISC_1:31;
a2: dom ((RealFuncUnit A) +* (x1 .--> 0)) =
dom RealFuncUnit A \/ dom (x1 .--> 0) by FUNCT_4:def 1
.= dom RealFuncUnit A \/ {x1}
.= A \/ {x1}
.= A by a0,XBOOLE_1:12,ZFMISC_1:31;
H2: rng ((RealFuncZero A) +* (x1 .--> 1)) c= rng RealFuncZero A \/
rng (x1 .--> 1) by FUNCT_4:17;
B1: rng RealFuncZero A c= REAL by RELAT_1:def 19;
rng (x1 .--> 1) = {1} by FUNCOP_1:8; then
rng (x1 .--> 1) c= REAL by XREAL_0:def 1,ZFMISC_1:31; then
rng RealFuncZero A \/ rng (x1 .--> 1) c= REAL \/ REAL by B1,XBOOLE_1:13;
then
S1: (RealFuncZero A) +* (x1 .--> 1) is Function of A, REAL by A2,FUNCT_2:2,
H2,XBOOLE_1:1;
H2: rng ((RealFuncUnit A) +* (x1 .--> 0)) c= rng RealFuncUnit A \/
rng (x1 .--> 0) by FUNCT_4:17;
B1: rng RealFuncUnit A c= REAL by RELAT_1:def 19;
rng (x1 .--> 0) = {0} by FUNCOP_1:8; then
rng (x1 .--> 0) c= REAL by XREAL_0:def 1,ZFMISC_1:31; then
rng RealFuncUnit A \/ rng (x1 .--> 0) c= REAL \/ REAL by B1,XBOOLE_1:13;
then
(RealFuncUnit A) +* (x1 .--> 0) is Function of A, REAL
by a2,FUNCT_2:2,H2,XBOOLE_1:1;
hence thesis by S1,FUNCT_2:8;
end;
theorem Th18:
x1 in A & x2 in A & x1<>x2 &
f = (RealFuncZero A) +* (x1 .--> 1) &
g = (RealFuncUnit A) +* (x1 .--> 0) implies
for a,b st
(RealFuncAdd A).((RealFuncExtMult A).[a,f],(RealFuncExtMult A).[b,g])
= RealFuncZero(A) holds a=0 & b=0
proof
assume that
A1: x1 in A and
A2: x2 in A and
A3: x1<>x2 and
A4: f = (RealFuncZero A) +* (x1 .--> 1) &
g = (RealFuncUnit A) +* (x1 .--> 0);
a5: f.x2 = (RealFuncZero A).x2 by A3,A4,FUNCT_4:83
.= 0 by A2,FUNCOP_1:7;
A5: g.x2 = (RealFuncUnit A).x2 by A3,A4,FUNCT_4:83
.= 1 by A2,FUNCOP_1:7;
a6: f.x1 = 1 by A4,FUNCT_4:113;
A6: g.x1=0 by A4,FUNCT_4:113;
let a,b;
reconsider x1,x2 as Element of A by A1,A2;
reconsider aa=a, bb=b as Element of REAL by XREAL_0:def 1;
assume
A7: (RealFuncAdd A). ((RealFuncExtMult A).[a,f],(RealFuncExtMult A).[b,
g]) = RealFuncZero(A);
then
A8: 0 = ((RealFuncAdd A). ((RealFuncExtMult A).[aa,f],
(RealFuncExtMult A).[bb,g])).x2
.= (((RealFuncExtMult A).[aa,f]).x2) + (((RealFuncExtMult A).[bb,g]).x2)
by Th1
.= a*(f.x2) + (((RealFuncExtMult A).[bb,g]).x2) by Th4
.=0 + b*1 by A5,Th4,a5
.= b;
0 = ((RealFuncAdd A). ((RealFuncExtMult A).[aa,f],(RealFuncExtMult A).[bb
,g])).x1 by A7
.= (((RealFuncExtMult A).[aa,f]).x1) + (((RealFuncExtMult A).[bb,g]).x1)
by Th1
.= a*(f.x1) + (((RealFuncExtMult A).[bb,g]).x1) by Th4
.= a + b*0 by A6,Th4,a6
.= a;
hence thesis by A8;
end;
::$CT
theorem Th20:
A = {x1,x2} & x1<>x2 &
f = (RealFuncZero A) +* (x1 .--> 1) &
g = (RealFuncUnit A) +* (x1 .--> 0) implies
for h holds ex a,b st h = (RealFuncAdd A).
((RealFuncExtMult A).[a,f],(RealFuncExtMult A).[b,g])
proof
assume that
A1: A = {x1,x2} and
A2: x1<>x2 and
A3: f = (RealFuncZero A) +* (x1 .--> 1) &
g = (RealFuncUnit A) +* (x1 .--> 0);
a4: x2 in A by A1,TARSKI:def 2;
A4: f.x2 = (RealFuncZero A).x2 by A2,A3,FUNCT_4:83
.= 0 by FUNCOP_1:7,a4;
A5: g.x2 = (RealFuncUnit A).x2 by A2,A3,FUNCT_4:83
.= 1 by FUNCOP_1:7,a4;
a6: f.x1 = 1 by A3,FUNCT_4:113;
B6: g.x1=0 by A3,FUNCT_4:113;
let h;
reconsider x1,x2 as Element of A by A1,TARSKI:def 2;
take a = h.x1, b = h.x2;
now
let x be Element of A;
A6: x = x1 or x = x2 by A1,TARSKI:def 2;
A7: ((RealFuncAdd A). ((RealFuncExtMult A).[a,f],(RealFuncExtMult A).[b,g
])).x2 = (((RealFuncExtMult A).[a,f]).x2) + (((RealFuncExtMult A).[b,g]).x2)
by Th1
.= a*(f.x2) + (((RealFuncExtMult A).[b,g]).x2) by Th4
.= 0 + b*1 by A5,A4,Th4
.= h.x2;
((RealFuncAdd A). ((RealFuncExtMult A).[a,f],(RealFuncExtMult A).[b,g
])).x1 = (((RealFuncExtMult A).[a,f]).x1) + (((RealFuncExtMult A).[b,g]).x1)
by Th1
.= a*1 + (((RealFuncExtMult A).[b,g]).x1) by a6,Th4
.= a + b*0 by Th4,B6
.= h.x1;
hence
h.x = ((RealFuncAdd A). ((RealFuncExtMult A).[a,f],(RealFuncExtMult A
).[b,g])).x by A6,A7;
end;
hence thesis by FUNCT_2:63;
end;
::$CT
theorem Th22:
A = {x1,x2} & x1<>x2 implies ex f,g st (for a,b st (RealFuncAdd
A).((RealFuncExtMult A).[a,f], (RealFuncExtMult A).[b,g]) = RealFuncZero(A)
holds a=0 & b=0) & for h holds ex a,b st h = (RealFuncAdd A). ((RealFuncExtMult
A).[a,f],(RealFuncExtMult A).[b,g])
proof
assume that
A1: A = {x1,x2} and
A2: x1<>x2;
x1 in A by TARSKI:def 2,A1; then
reconsider f = (RealFuncZero A) +* (x1 .--> 1),
g = (RealFuncUnit A) +* (x1 .--> 0) as Element of Funcs (A,REAL) by Th17;
take f,g;
x1 in A & x2 in A by A1,TARSKI:def 2;
hence thesis by A1,A2,Th18,Th20;
end;
definition let A be set;
func RealVectSpace(A) -> strict RealLinearSpace equals
RLSStruct(#Funcs(A,REAL),
RealFuncZero(A),RealFuncAdd(A),RealFuncExtMult(A)#);
coherence
proof
set S = RLSStruct(#Funcs(A,REAL), (RealFuncZero(A)),RealFuncAdd(A),
RealFuncExtMult(A)#);
A1: S is add-associative by Th6;
A2: S is right_complementable
proof
let u be Element of S;
reconsider u9 = u as Element of Funcs(A,REAL);
reconsider w = (RealFuncExtMult A).[-jj,u9] as VECTOR of S;
take w;
thus thesis by Th11;
end;
A3: S is vector-distributive scalar-distributive scalar-associative
scalar-unital by Lm2,Th14,Th13,Th12;
A4: S is right_zeroed
proof
let u be Element of S;
reconsider u9=u as Element of Funcs(A,REAL);
thus u+0.S = (RealFuncAdd A).(RealFuncZero(A),u9) by Th5
.= u by Th10;
end;
S is Abelian by Th5;
hence thesis by A1,A4,A2,A3;
end;
end;
theorem
ex V being strict RealLinearSpace st ex u,v being Element of V st
(for a,b st a*u + b*v = 0.V holds a=0 & b=0) &
for w being Element of V ex a,b st w = a*u + b*v
proof
set A ={0,1};
take V = RealVectSpace(A);
consider f,g being Element of Funcs(A,REAL) such that
A1: for a,b st (RealFuncAdd A).((RealFuncExtMult A).[a,f], (
RealFuncExtMult A).[b,g]) = RealFuncZero(A) holds a=0 & b=0 and
A2: for h being Element of Funcs(A,REAL) holds ex a,b st h = (
RealFuncAdd A). ((RealFuncExtMult A).[a,f],(RealFuncExtMult A).[b,g]) by Th22;
reconsider u=f, v=g as Element of V;
take u,v;
thus for a,b st a*u + b*v = 0.V holds a=0 & b=0 by A1;
thus for w being Element of V ex a,b st w = a*u + b*v
proof
let w be Element of V;
reconsider h=w as Element of Funcs(A,REAL);
consider a,b such that
A3: h = (RealFuncAdd A).((RealFuncExtMult A).[a,f], (RealFuncExtMult A
).[b,g]) by A2;
h = a*u + b*v by A3;
hence thesis;
end;
end;
definition let A be set;
func RRing A -> strict doubleLoopStr equals
doubleLoopStr(#Funcs(A,REAL),
RealFuncAdd A,RealFuncMult A, RealFuncUnit A,RealFuncZero A#);
correctness;
end;
registration let A be set;
cluster RRing A -> non empty;
coherence;
end;
Lm3: now
let A;
set FR = RRing(A);
let h, a be Element of FR;
reconsider g = h as Element of Funcs(A,REAL);
assume
A1: a = RealFuncUnit(A);
hence h * a = (RealFuncMult(A)).(RealFuncUnit(A),g) by Th7
.= h by Th9;
thus a * h = h by A1,Th9;
end;
registration let A;
cluster RRing A -> unital;
coherence
proof
reconsider e = RealFuncUnit(A) as Element of RRing(A);
take e;
thus thesis by Lm3;
end;
end;
theorem
1.RRing(A) = RealFuncUnit(A);
theorem Th25:
for x,y,z being Element of RRing(A) holds x+y = y+x & (x+y)+z =
x+(y+z) & x+(0.RRing(A)) = x & (ex t being Element of RRing(A) st x+t=(0.RRing(
A))) & x*y = y*x & (x*y)*z = x*(y*z) & x*(1.RRing(A)) = x & (1.RRing(A))*x = x
& x*(y+z) = x*y + x*z & (y+z)*x = y*x + z*x
proof
let x,y,z be Element of RRing(A);
set IT = RRing(A);
reconsider f=x as Element of Funcs(A,REAL);
thus x+y = y+x by Th5;
thus (x+y)+z = x+(y+z) by Th6;
thus x+(0.RRing(A)) = (RealFuncAdd A).(RealFuncZero(A),f) by Th5
.= x by Th10;
thus ex t being Element of RRing(A) st x+t=(0.RRing(A))
proof
set h = (RealFuncExtMult A).[-jj,f];
reconsider t=h as Element of IT;
take t;
thus thesis by Th11;
end;
thus x*y = y*x by Th7;
thus (x*y)*z = x*(y*z) by Th8;
thus x*(1.RRing(A)) = (RealFuncMult(A)).(RealFuncUnit(A),f) by Th7
.= x by Th9;
hence (1.RRing(A))*x = x by Th7;
thus x*(y+z) = x*y + x*z by Th15;
hence (y+z)*x = x*y + x*z by Th7
.= y*x + x*z by Th7
.= y*x + z*x by Th7;
end;
registration
cluster strict Abelian add-associative right_zeroed right_complementable
associative commutative right_unital right-distributive for 1-element
doubleLoopStr;
existence
proof
take L = Trivial-doubleLoopStr;
thus L is strict;
thus L is Abelian by STRUCT_0:def 10;
thus L is add-associative by STRUCT_0:def 10;
thus L is right_zeroed by STRUCT_0:def 10;
thus L is right_complementable
proof
let x be Element of L;
take x;
thus thesis by STRUCT_0:def 10;
end;
thus L is associative by STRUCT_0:def 10;
thus L is commutative by STRUCT_0:def 10;
thus L is right_unital by STRUCT_0:def 10;
let x be Element of L;
thus thesis by STRUCT_0:def 10;
end;
end;
theorem
RRing(A) is commutative Ring
proof
A1: RRing A is Abelian by Th25;
A2: RRing A is add-associative by Th25;
A3: RRing A is right_complementable
proof
let x be Element of RRing A;
consider t being Element of RRing A such that
A4: x+t = 0.RRing(A) by Th25;
take t;
thus thesis by A4;
end;
A5: RRing A is right_zeroed by Th25;
A6: RRing A is distributive by Th25;
A7: RRing A is well-unital by Th25;
A8: RRing A is associative by Th25;
RRing A is commutative by Th25;
hence thesis by A1,A2,A5,A3,A8,A7,A6;
end;
definition
struct (doubleLoopStr,RLSStruct)
AlgebraStr
(# carrier -> set,
multF,addF -> (BinOp of the carrier),
Mult -> (Function of [:REAL,the carrier:],the carrier),
OneF,ZeroF -> Element of the carrier #);
end;
registration
cluster non empty for AlgebraStr;
existence
proof
set X = the non empty set,m = the BinOp of X,
M = the Function of [:REAL,X:],X,u = the Element of X;
take AlgebraStr(#X,m,m,M,u,u#);
thus the carrier of AlgebraStr(#X,m,m,M,u,u#) is non empty;
end;
end;
definition
let A be set;
func RAlgebra A -> strict AlgebraStr equals
AlgebraStr(#Funcs(A,REAL),
RealFuncMult(A),RealFuncAdd(A), RealFuncExtMult(A),(RealFuncUnit(A)),(
RealFuncZero(A))#);
correctness;
end;
registration let A be set;
cluster RAlgebra A -> non empty;
coherence;
end;
Lm4: now
let A;
set F = RAlgebra A;
let x, e be Element of F;
reconsider f = x as Element of Funcs(A,REAL);
assume
A1: e = RealFuncUnit(A);
hence x * e = (RealFuncMult(A)).(RealFuncUnit(A),f) by Th7
.= x by Th9;
thus e * x = x by A1,Th9;
end;
registration let A;
cluster RAlgebra A -> unital;
coherence
proof
reconsider e = RealFuncUnit(A) as Element of RAlgebra(A);
take e;
thus thesis by Lm4;
end;
end;
theorem
1.RAlgebra(A) = RealFuncUnit(A);
definition
let IT be non empty AlgebraStr;
attr IT is vector-associative means
for x,y being Element of IT for a holds a*(x*y) = (a*x)*y;
end;
registration let A be set;
cluster RAlgebra A -> strict Abelian add-associative right_zeroed
right_complementable commutative associative right_unital
right-distributive vector-associative scalar-associative
vector-distributive scalar-distributive;
coherence
proof
thus RAlgebra A is strict;
thus RAlgebra A is Abelian by Th5;
thus RAlgebra A is add-associative by Th6;
thus RAlgebra A is right_zeroed proof let x be Element of RAlgebra A;
thus x+0.RAlgebra A = (RealFuncAdd A).(RealFuncZero A,x) by Th5
.= x by Th10;
end;
thus RAlgebra A is right_complementable
proof
let x be Element of RAlgebra A;
reconsider f=x as Element of Funcs(A,REAL);
reconsider t=(RealFuncExtMult A).[-jj,f] as Element of RAlgebra A;
take t;
thus thesis by Th11;
end;
thus RAlgebra A is commutative by Th7;
thus RAlgebra A is associative by Th8;
thus RAlgebra A is right_unital proof let x be Element of RAlgebra A;
thus x*(1.RAlgebra A) = (RealFuncMult A).(RealFuncUnit A,x) by Th7
.= x by Th9;
end;
thus RAlgebra A is right-distributive by Th15;
thus RAlgebra A is vector-associative by Th16;
thus RAlgebra A is scalar-associative by Th13;
thus RAlgebra A is vector-distributive by Lm2;
let a,b be Real, v be Element of RAlgebra A;
thus thesis by Th14;
end;
end;
registration
cluster strict Abelian add-associative right_zeroed right_complementable
commutative associative right_unital right-distributive vector-associative
scalar-associative vector-distributive scalar-distributive for non empty
AlgebraStr;
existence
proof
take RAlgebra {};
thus thesis;
end;
end;
definition
mode Algebra is Abelian add-associative right_zeroed right_complementable
commutative associative right_unital right-distributive
vector-associative scalar-associative vector-distributive
scalar-distributive non empty AlgebraStr;
end;
theorem
(RealFuncAdd A).(f,g) = f + g
proof
A1: dom ((RealFuncAdd A).(f,g)) = A by FUNCT_2:def 1;
a1: dom (f + g) = dom f /\ dom g by VALUED_1:def 1
.= A /\ dom g by FUNCT_2:def 1
.= A /\ A by FUNCT_2:def 1
.= A;
now
let x be object;
assume
a0: x in dom (f+g);
A3: dom (addreal.:(f,g)) = A by FUNCT_2:def 1;
thus ((RealFuncAdd A).(f,g)).x = (addreal.:(f,g)).x by Def1
.= addreal.(f.x,g.x) by a1,a0,A3,FUNCOP_1:22
.= f.x + g.x by BINOP_2:def 9
.= (f+g).x by VALUED_1:1,a1,a0;
end;
hence thesis by a1,A1,FUNCT_1:2;
end;
theorem
(RealFuncMult(A)).(f,g) = f (#) g
proof
A1: dom ((RealFuncMult A).(f,g)) = A by FUNCT_2:def 1;
a1: dom (f (#) g) = dom f /\ dom g by VALUED_1:def 4
.= A /\ dom g by FUNCT_2:def 1
.= A /\ A by FUNCT_2:def 1
.= A;
now
let x be object;
assume
a0: x in dom (f (#) g);
A3: dom (multreal.:(f,g)) = A by FUNCT_2:def 1;
thus ((RealFuncMult(A)).(f,g)).x = (multreal.:(f,g)).x by Def2
.= multreal.(f.x,g.x) by a1,a0,A3,FUNCOP_1:22
.= f.x * g.x by BINOP_2:def 11
.= (f (#) g).x by VALUED_1:5;
end;
hence thesis by A1,a1,FUNCT_1:2;
end;
theorem
(RealFuncExtMult A).(a,f) = a (#) f
proof
reconsider aa=a as Element of REAL by XREAL_0:def 1;
set h = (RealFuncExtMult A).(a,f);
b1:dom (a (#) f) = dom f by VALUED_1:def 5 .= A by FUNCT_2:def 1;
A2:now let x be Element of A;
thus h.x = (multreal[;](aa,f)).x by Def3
.= multreal.(aa,f.x) by FUNCOP_1:53
.= a*(f.x) by BINOP_2:def 11
.= (a (#) f).x by VALUED_1:def 5,b1;
end;
a in REAL & f in Funcs(A,REAL) by XREAL_0:def 1; then
[a,f] in [:REAL,Funcs(A,REAL):] by ZFMISC_1:87; then
(RealFuncExtMult A).(a,f) is Function of A, REAL by FUNCT_2:66,5; then
B1:dom ((RealFuncExtMult A).(a,f)) = A by FUNCT_2:def 1;
for x being object st x in dom (a (#) f) holds
((RealFuncExtMult A).(a,f)).x = (a (#) f).x by A2,b1;
hence thesis by FUNCT_1:2,B1,b1;
end;