:: Algebra of Vector Functions
:: by Hiroshi Yamazaki and Yasunari Shidama
::
:: Received October 27, 1992
:: Copyright (c) 1992-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, SUBSET_1, NORMSP_1, PARTFUN1, REAL_1, ARYTM_3, ARYTM_1,
RELAT_1, NUMBERS, FUNCT_1, VALUED_1, SUPINF_2, CARD_1, TARSKI, COMPLEX1,
XXREAL_0, XXREAL_2, RLVECT_1, VFUNCT_1, ALGSTR_0, BINOP_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, XCMPLX_0,
COMPLEX1, REAL_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, PARTFUN2,
VALUED_1, COMSEQ_2, SEQ_2, XXREAL_0, STRUCT_0, ALGSTR_0, RLVECT_1,
NORMSP_0, NORMSP_1;
constructors PARTFUN1, XXREAL_0, REAL_1, COMPLEX1, PARTFUN2, RFUNCT_1,
NORMSP_1, VALUED_1, SEQ_2, RELSET_1, COMSEQ_2;
registrations RELSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, VALUED_0,
RFUNCT_1, NORMSP_1, RLVECT_1, NORMSP_0, FUNCT_2, ORDINAL1;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, PARTFUN1, XBOOLE_0;
equalities XBOOLE_0, RLVECT_1, NORMSP_0;
expansions PARTFUN1, XBOOLE_0;
theorems TARSKI, SUBSET_1, FUNCT_1, ABSVALUE, PARTFUN1, PARTFUN2, RFUNCT_1,
RLVECT_1, NORMSP_1, RELAT_1, XBOOLE_0, XBOOLE_1, XREAL_1, COMPLEX1,
XXREAL_0, VALUED_1, NORMSP_0, FUNCT_2;
schemes PARTFUN2;
begin
reserve x,X,Y for set;
reserve C for non empty set;
reserve c for Element of C;
reserve V for RealNormSpace;
reserve f,f1,f2,f3 for PartFunc of C,V;
reserve r,r1,r2,p for Real;
::
::OPERATIONS ON PARTIAL FUNCTIONS FROM A DOMAIN TO THE SET OF REAL NUMBERS
::
definition
let C;
let V be non empty addLoopStr;
let f1,f2 be PartFunc of C,V;
deffunc F(set) = (f1/.$1) + (f2/.$1);
deffunc G(set) = (f1/.$1) - (f2/.$1);
defpred P[set] means $1 in dom f1 /\ dom f2;
set X = dom f1 /\ dom f2;
func f1+f2 -> PartFunc of C,V means
:Def1:
dom it = dom f1 /\ dom f2 &
for c st c in dom it holds it/.c = (f1/.c) + (f2/.c);
existence
proof
consider F be PartFunc of C,V such that
A1: for c holds c in dom F iff P[c] and
A2: for c st c in dom F holds F/.c = F(c) from PARTFUN2:sch 2;
take F;
thus thesis by A1,A2,SUBSET_1:3;
end;
uniqueness
proof
thus for f,g being PartFunc of C,V st (dom f=X &
for c st c in dom f holds f/.c = F(c)) & (dom g=X &
for c st c in dom g holds g/.c = F(c)) holds f = g from PARTFUN2:sch 3;
end;
func f1-f2 -> PartFunc of C,V means
:Def2:
dom it = dom f1 /\ dom f2 &
for c st c in dom it holds it/.c = (f1/.c) - (f2/.c);
existence
proof
consider F be PartFunc of C,V such that
A3: for c holds c in dom F iff P[c] and
A4: for c st c in dom F holds F/.c = G(c) from PARTFUN2:sch 2;
take F;
thus thesis by A3,A4,SUBSET_1:3;
end;
uniqueness
proof
thus for f,g being PartFunc of C,V st (dom f=X & for c be
Element of C st c in dom f holds f/.c = G(c)) & (dom g=X & for c be Element of
C st c in dom g holds g/.c = G(c)) holds f = g from PARTFUN2:sch 3;
end;
end;
registration
let C;
let V be non empty addLoopStr;
let f1,f2 be Function of C,V;
cluster f1+f2 -> total;
coherence
proof
thus dom (f1+f2) = dom f1 /\ dom f2 by Def1
.= C /\ dom f2 by FUNCT_2:def 1
.= C /\ C by FUNCT_2:def 1
.= C;
end;
cluster f1-f2 -> total;
coherence
proof
thus dom (f1-f2) = dom f1 /\ dom f2 by Def2
.= C /\ dom f2 by FUNCT_2:def 1
.= C /\ C by FUNCT_2:def 1
.= C;
end;
end;
definition
let C;
let V be non empty RLSStruct;
let f1 be PartFunc of C,REAL;
let f2 be PartFunc of C,V;
deffunc F(Element of C) = (f1.$1) * (f2/.$1);
defpred P[set] means $1 in dom f1 /\ dom f2;
set X = dom f1 /\ dom f2;
func f1(#)f2 -> PartFunc of C,V means
:Def3:
dom it = dom f1 /\ dom f2 &
for c st c in dom it holds it/.c = f1.c * (f2/.c);
existence
proof
consider F be PartFunc of C,V such that
A1: for c holds c in dom F iff P[c] and
A2: for c st c in dom F holds F/.c = F(c) from PARTFUN2:sch 2;
take F;
thus thesis by A1,A2,SUBSET_1:3;
end;
uniqueness
proof
thus for f,g being PartFunc of C,V st (dom f=X & for c be
Element of C st c in dom f holds f/.c = F(c)) & (dom g=X & for c be Element of
C st c in dom g holds g/.c = F(c)) holds f = g from PARTFUN2:sch 3;
end;
end;
registration
let C;
let V be non empty RLSStruct;
let f1 be Function of C,REAL;
let f2 be Function of C,V;
cluster f1(#)f2 -> total;
coherence
proof
thus dom (f1(#)f2) = dom f1 /\ dom f2 by Def3
.= C /\ dom f2 by FUNCT_2:def 1
.= C /\ C by FUNCT_2:def 1
.= C;
end;
end;
definition
let C;
let V be non empty RLSStruct;
let f be PartFunc of C,V;
let r be Real;
deffunc F(Element of C) = r * (f/.$1);
defpred P[set] means $1 in dom f;
func r(#)f -> PartFunc of C,V means
:Def4:
dom it = dom f & for c st c in dom it holds it/.c = r * (f/.c);
existence
proof
consider F be PartFunc of C,V such that
A1: for c holds c in dom F iff P[c] and
A2: for c st c in dom F holds F/.c = F(c) from PARTFUN2:sch 2;
take F;
thus thesis by A1,A2,SUBSET_1:3;
end;
uniqueness
proof
set X = dom f;
thus for f,g being PartFunc of C,V st (dom f=X & for c be
Element of C st c in dom f holds f/.c = F(c)) & (dom g=X & for c be Element of
C st c in dom g holds g/.c = F(c)) holds f = g from PARTFUN2:sch 3;
end;
end;
registration
let C;
let V be non empty RLSStruct;
let f be Function of C,V;
let r;
cluster r(#)f -> total;
coherence
proof
thus dom (r(#)f) = dom f by Def4
.= C by FUNCT_2:def 1;
end;
end;
definition
let C;
let V be non empty addLoopStr;
let f be PartFunc of C,V;
deffunc G(Element of C) = - f/.$1;
defpred P[set] means $1 in dom f;
func -f -> PartFunc of C,V means
:Def5:
dom it = dom f & for c st c in dom it holds it/.c = -(f/.c);
existence
proof
consider F being PartFunc of C,V such that
A1: for c holds c in dom F iff P[c] and
A2: for c st c in dom F holds F/.c = G(c) from PARTFUN2:sch 2;
take F;
thus thesis by A1,A2,SUBSET_1:3;
end;
uniqueness
proof
set X = dom f;
thus for f,g being PartFunc of C,V st (dom f=X & for c be
Element of C st c in dom f holds f/.c = G(c)) & (dom g=X & for c be Element of
C st c in dom g holds g/.c = G(c)) holds f = g from PARTFUN2:sch 3;
end;
end;
registration
let C;
let V be non empty addLoopStr;
let f be Function of C,V;
cluster -f -> total;
coherence
proof
thus dom -f = dom f by Def5
.= C by FUNCT_2:def 1;
end;
end;
theorem
for f1 be PartFunc of C,REAL holds
dom (f1(#)f2) \ (f1(#)f2)"{0.V} =
(dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0.V})
proof
let f1 be PartFunc of C,REAL;
thus dom (f1(#)f2) \ (f1(#) f2)"{0.V} c= (dom f1 \ (f1)"{0}) /\ (dom f2 \ (
f2)"{0.V})
proof
let x be object;
assume
A1: x in dom (f1(#)f2) \ (f1(#)f2)"{0.V};
then
A2: x in dom (f1(#)f2) by XBOOLE_0:def 5;
reconsider x1=x as Element of C by A1;
not x in (f1(#)f2)"{0.V} by A1,XBOOLE_0:def 5;
then not (f1(#)f2)/.x1 in {0.V} by A2,PARTFUN2:26;
then (f1(#)f2)/.x1 <> 0.V by TARSKI:def 1;
then
A3: f1.x1 * (f2/.x1) <> 0.V by A2,Def3;
then (f2/.x1) <> 0.V;
then not (f2/.x1) in {0.V } by TARSKI:def 1;
then
A4: not x1 in (f2)"{0.V} by PARTFUN2:26;
A5: x1 in dom f1 /\ dom f2 by A2,Def3;
then x1 in dom f2 by XBOOLE_0:def 4;
then
A6: x in dom f2 \ (f2)"{0.V} by A4,XBOOLE_0:def 5;
f1.x1 <> 0 by A3,RLVECT_1:10;
then not f1.x1 in {0} by TARSKI:def 1;
then
A7: not x1 in (f1)"{0} by FUNCT_1:def 7;
x1 in dom f1 by A5,XBOOLE_0:def 4;
then x in dom f1 \ (f1)"{0} by A7,XBOOLE_0:def 5;
hence thesis by A6,XBOOLE_0:def 4;
end;
thus (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0.V}) c= dom (f1(#)f2) \ (f1(#)
f2)"{0.V}
proof
let x be object;
assume
A8: x in (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0.V});
then reconsider x1=x as Element of C;
A9: x in dom f2 \ (f2)"{0.V} by A8,XBOOLE_0:def 4;
then
A10: x in dom f2 by XBOOLE_0:def 5;
not x in (f2)"{0.V } by A9,XBOOLE_0:def 5;
then not (f2/.x1) in {0.V} by A10,PARTFUN2:26;
then
A11: (f2/.x1) <> 0.V by TARSKI:def 1;
A12: x in dom f1 \ (f1)"{0} by A8,XBOOLE_0:def 4;
then
A13: x in dom f1 by XBOOLE_0:def 5;
then x1 in dom f1 /\ dom f2 by A10,XBOOLE_0:def 4;
then
A14: x1 in dom (f1(#)f2) by Def3;
not x in (f1)"{0} by A12,XBOOLE_0:def 5;
then not f1.x1 in {0} by A13,FUNCT_1:def 7;
then f1.x1 <> 0 by TARSKI:def 1;
then f1.x1 * (f2/.x1) <>0.V by A11,RLVECT_1:11;
then (f1(#)f2)/.x1 <> 0.V by A14,Def3;
then not (f1(#)f2)/.x1 in {0.V} by TARSKI:def 1;
then not x in (f1(#)f2)"{0.V} by PARTFUN2:26;
hence thesis by A14,XBOOLE_0:def 5;
end;
end;
theorem
(||.f.||)"{0} = f"{0.V} & (-f)"{0.V} = f"{0.V}
proof
now
let c;
thus c in (||.f.||)"{0} implies c in f"{0.V}
proof
assume
A1: c in (||.f.||)"{0};
then
A2: c in dom (||.f.||) by FUNCT_1:def 7;
(||.f.||).c in {0} by A1,FUNCT_1:def 7;
then (||.f.||).c = 0 by TARSKI:def 1;
then ||.f/.c.|| = 0 by A2,NORMSP_0:def 3;
then f/.c = 0.V by NORMSP_0:def 5;
then
A3: f/.c in {0.V} by TARSKI:def 1;
c in dom f by A2,NORMSP_0:def 3;
hence thesis by A3,PARTFUN2:26;
end;
assume
A4: c in (f)"{0.V};
then c in dom f by PARTFUN2:26;
then
A5: c in dom (||.f.||) by NORMSP_0:def 3;
f/.c in {0.V} by A4,PARTFUN2:26;
then f/.c = 0.V by TARSKI:def 1;
then ||.f/.c.|| = 0;
then (||.f.||).c = 0 by A5,NORMSP_0:def 3;
then (||.f.||).c in {0} by TARSKI:def 1;
hence c in (||.f.||)"{0} by A5,FUNCT_1:def 7;
end;
hence (||.f.||)"{0} = f"{0.V} by SUBSET_1:3;
now
let c;
thus c in (-f)"{0.V} implies c in f"{0.V}
proof
assume
A6: c in (-f)"{0.V};
then
A7: c in dom (-f) by PARTFUN2:26;
(-f)/.c in {0.V} by A6,PARTFUN2:26;
then (-f)/.c = 0.V by TARSKI:def 1;
then --(f/.c) = -0.V by A7,Def5;
then f/.c = 0.V;
then
A8: f/.c in {0.V} by TARSKI:def 1;
c in dom f by A7,Def5;
hence thesis by A8,PARTFUN2:26;
end;
assume
A9: c in (f)"{0.V};
then c in dom f by PARTFUN2:26;
then
A10: c in dom (-f) by Def5;
f/.c in {0.V} by A9,PARTFUN2:26;
then f/.c = 0.V by TARSKI:def 1;
then (-f)/.c = -0.V by A10,Def5;
then (-f)/.c in {0.V} by TARSKI:def 1;
hence c in (-f)"{0.V} by A10,PARTFUN2:26;
end;
hence thesis by SUBSET_1:3;
end;
theorem
r<>0 implies (r(#)f)"{0.V} = f"{0.V}
proof
assume
A1: r<>0;
now
let c;
thus c in (r(#)f)"{0.V} implies c in f"{0.V}
proof
assume
A2: c in (r(#)f)"{0.V};
then
A3: c in dom (r(#)f) by PARTFUN2:26;
(r(#)f)/.c in {0.V} by A2,PARTFUN2:26;
then (r(#)f)/.c = 0.V by TARSKI:def 1;
then r*f/.c = r*0.V by A3,Def4;
then f/.c = 0.V by A1,RLVECT_1:36;
then
A4: f/.c in {0.V} by TARSKI:def 1;
c in dom f by A3,Def4;
hence thesis by A4,PARTFUN2:26;
end;
assume
A5: c in (f)"{0.V};
then c in dom f by PARTFUN2:26;
then
A6: c in dom (r(#)f) by Def4;
f/.c in {0.V} by A5,PARTFUN2:26;
then r*f/.c = r*0.V by TARSKI:def 1;
then (r(#)f)/.c = 0.V by A6,Def4;
then (r(#)f)/.c in {0.V} by TARSKI:def 1;
hence c in (r(#)f)"{0.V} by A6,PARTFUN2:26;
end;
hence thesis by SUBSET_1:3;
end;
::
:: BASIC PROPERTIES OF OPERATIONS
::
theorem Th4:
for V being Abelian non empty addLoopStr
for f1,f2 being PartFunc of C,V holds
f1 + f2 = f2 + f1
proof
let V be Abelian non empty addLoopStr;
let f1,f2 be PartFunc of C,V;
A1: dom (f1 + f2) = dom f2 /\ dom f1 by Def1
.= dom (f2 + f1) by Def1;
now
let c;
assume
A2: c in dom (f1+f2);
hence (f1 + f2)/.c = (f2/.c) + (f1/.c) by Def1
.= (f2 + f1)/.c by A1,A2,Def1;
end;
hence thesis by A1,PARTFUN2:1;
end;
definition
let C;
let V be Abelian non empty addLoopStr;
let f1,f2 be PartFunc of C,V;
redefine func f1+f2; :: redefines + (VFUNCT_1, definition)
commutativity by Th4;
end;
theorem
for V being add-associative non empty addLoopStr
for f1,f2,f3 being PartFunc of C,V holds
(f1 + f2) + f3 = f1 + (f2 + f3)
proof
let V be add-associative non empty addLoopStr;
let f1,f2,f3 be PartFunc of C,V;
A1: dom (f1 + f2 + f3) = dom (f1 + f2) /\ dom f3 by Def1
.= dom f1 /\ dom f2 /\ dom f3 by Def1
.= dom f1 /\ (dom f2 /\ dom f3) by XBOOLE_1:16
.= dom f1 /\ dom (f2 + f3) by Def1
.= dom (f1 + (f2 + f3)) by Def1;
now
let c;
assume
A2: c in dom (f1 + f2 + f3);
then c in dom (f1 + f2) /\ dom f3 by Def1;
then
A3: c in dom (f1 + f2) by XBOOLE_0:def 4;
c in dom f1 /\ dom (f2 + f3) by A1,A2,Def1;
then
A4: c in dom (f2 + f3) by XBOOLE_0:def 4;
thus (f1 + f2 + f3)/.c = ((f1 + f2)/.c) + (f3/.c) by A2,Def1
.= (f1/.c) + (f2/.c) + (f3/.c) by A3,Def1
.= (f1/.c) + ((f2/.c) + (f3/.c)) by RLVECT_1:def 3
.= (f1/.c) + ((f2 + f3)/.c) by A4,Def1
.= (f1 + (f2 + f3))/.c by A1,A2,Def1;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for V being scalar-associative non empty RLSStruct
for f1,f2 being PartFunc of C,REAL, f3 being PartFunc of C,V
holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
proof
let V be scalar-associative non empty RLSStruct;
let f1,f2 be PartFunc of C,REAL;
let f3 be PartFunc of C,V;
A1: dom (f1 (#) f2 (#) f3) = dom (f1 (#) f2) /\ dom f3 by Def3
.= dom f1 /\ dom f2 /\ dom f3 by VALUED_1:def 4
.= dom f1 /\ (dom f2 /\ dom f3) by XBOOLE_1:16
.= dom f1 /\ dom (f2 (#) f3) by Def3
.= dom (f1 (#) (f2 (#) f3)) by Def3;
now
let c;
assume
A2: c in dom (f1(#)f2(#)f3);
then c in dom f1 /\ dom (f2(#)f3) by A1,Def3;
then
A3: c in dom (f2 (#) f3) by XBOOLE_0:def 4;
thus (f1 (#) f2 (#) f3)/.c = (f1 (#) f2).c * (f3/.c) by A2,Def3
.= f1.c * f2.c * (f3/.c) by VALUED_1:5
.= f1.c * (f2.c * (f3/.c)) by RLVECT_1:def 7
.= f1.c * ((f2 (#) f3)/.c) by A3,Def3
.= (f1 (#) (f2 (#) f3))/.c by A1,A2,Def3;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for V being scalar-distributive non empty RLSStruct
for f1,f2 being PartFunc of C,REAL
for f3 being Function of C,V holds
(f1 + f2) (#) f3 = f1 (#) f3 + f2 (#) f3
proof
let V be scalar-distributive non empty RLSStruct;
let f1,f2 be PartFunc of C,REAL;
let f3 be Function of C,V;
A1: dom ((f1 + f2) (#) f3) = dom (f1 + f2) /\ dom f3 by Def3
.= dom f1 /\ dom f2 /\ (dom f3 /\ dom f3) by VALUED_1:def 1
.= dom f1 /\ dom f2 /\ dom f3 /\ dom f3 by XBOOLE_1:16
.= dom f1 /\ dom f3 /\ dom f2 /\ dom f3 by XBOOLE_1:16
.= dom f1 /\ dom f3 /\ (dom f2 /\ dom f3) by XBOOLE_1:16
.= dom (f1 (#) f3) /\ (dom f2 /\ dom f3) by Def3
.= dom (f1 (#) f3) /\ dom (f2 (#) f3) by Def3
.= dom (f1 (#) f3 + f2 (#) f3) by Def1;
now
let c;
assume
A2: c in dom ((f1 + f2)(#)f3);
then c in dom (f1 + f2) /\ dom f3 by Def3;
then
A3: c in dom (f1 + f2) by XBOOLE_0:def 4;
A4: c in dom (f1(#)f3) /\ dom (f2(#)f3) by A1,A2,Def1;
then
A5: c in dom (f1(#)f3) by XBOOLE_0:def 4;
A6: c in dom (f2 (#) f3) by A4,XBOOLE_0:def 4;
thus ((f1 + f2) (#) f3)/.c = (f1 + f2).c * (f3/.c) by A2,Def3
.= (f1.c + f2.c) * (f3/.c) by A3,VALUED_1:def 1
.= f1.c * (f3/.c) + f2.c * (f3/.c) by RLVECT_1:def 6
.= ((f1 (#) f3)/.c) + f2.c* (f3/.c) by A5,Def3
.= ((f1 (#) f3)/.c) + ((f2 (#) f3)/.c) by A6,Def3
.= ((f1 (#) f3) + (f2 (#) f3))/.c by A1,A2,Def1;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for V being vector-distributive non empty RLSStruct
for f1,f2 being PartFunc of C,V
for f3 being Function of C,REAL holds
f3 (#) (f1 + f2) = f3(#)f1 + f3(#)f2
proof
let V be vector-distributive non empty RLSStruct;
let f1,f2 be PartFunc of C,V;
let f3 be Function of C,REAL;
A1: dom (f3 (#) (f1 + f2)) = dom f3 /\ dom (f1 + f2) by Def3
.= dom f3 /\ (dom f1 /\ dom f2) by Def1
.= dom f3 /\ dom f3 /\ dom f1 /\ dom f2 by XBOOLE_1:16
.= dom f3 /\ dom f1 /\ dom f3 /\ dom f2 by XBOOLE_1:16
.= dom f3 /\ dom f1 /\ (dom f3 /\ dom f2) by XBOOLE_1:16
.= dom (f3 (#) f1) /\ (dom f3 /\ dom f2) by Def3
.= dom (f3 (#) f1) /\ dom (f3 (#) f2) by Def3
.= dom (f3 (#) f1 + f3 (#) f2) by Def1;
now
let c;
assume
A2: c in dom (f3(#)(f1 + f2));
then c in dom f3 /\ dom (f1 + f2) by Def3;
then
A3: c in dom (f1 + f2) by XBOOLE_0:def 4;
A4: c in dom (f3(#)f1) /\ dom (f3(#)f2) by A1,A2,Def1;
then
A5: c in dom (f3(#)f1) by XBOOLE_0:def 4;
A6: c in dom (f3 (#) f2) by A4,XBOOLE_0:def 4;
thus (f3 (#) (f1 + f2))/.c = f3.c * ((f1 + f2)/.c) by A2,Def3
.= f3.c * ((f1/.c) + (f2/.c)) by A3,Def1
.= f3.c * (f1/.c) + f3.c * (f2/.c) by RLVECT_1:def 5
.= ((f3 (#) f1)/.c) + f3.c* (f2/.c) by A5,Def3
.= ((f3 (#) f1)/.c) + ((f3 (#) f2)/.c) by A6,Def3
.= ((f3 (#) f1) + (f3 (#) f2))/.c by A1,A2,Def1;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for V being scalar-associative non empty RLSStruct
for f1 being PartFunc of C,REAL
for f2 being PartFunc of C,V holds
r(#)(f1(#)f2) = r(#)f1(#)f2
proof
let V be scalar-associative non empty RLSStruct;
let f1 be PartFunc of C,REAL;
let f2 be PartFunc of C,V;
A1: dom (r(#)(f1 (#) f2)) = dom (f1 (#) f2) by Def4
.= dom f1 /\ dom f2 by Def3
.= dom (r(#)f1) /\ dom f2 by VALUED_1:def 5
.= dom (r(#)f1(#)f2) by Def3;
now
let c;
assume
A2: c in dom (r(#)(f1(#)f2));
then
A3: c in dom (f1(#)f2) by Def4;
c in dom (r(#)f1) /\ dom f2 by A1,A2,Def3;
then
A4: c in dom (r(#)f1) by XBOOLE_0:def 4;
thus (r(#)(f1(#)f2))/.c = r * ((f1(#)f2)/.c) by A2,Def4
.= r*(f1.c * (f2/.c)) by A3,Def3
.= (r*f1.c) * (f2/.c) by RLVECT_1:def 7
.= (r(#)f1).c * (f2/.c) by A4,VALUED_1:def 5
.= (r(#)f1 (#) f2)/.c by A1,A2,Def3;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for V being scalar-associative non empty RLSStruct
for f1 being PartFunc of C,REAL
for f2 being PartFunc of C,V holds
r(#)(f1(#)f2) = f1(#)(r(#)f2)
proof
let V be scalar-associative non empty RLSStruct;
let f1 be PartFunc of C,REAL;
let f2 be PartFunc of C,V;
A1: dom (r(#)(f1 (#) f2)) = dom (f1 (#) f2) by Def4
.= dom f1 /\ dom f2 by Def3
.= dom f1 /\ dom (r(#)f2) by Def4
.= dom (f1(#)(r(#)f2)) by Def3;
now
let c;
assume
A2: c in dom (r(#)(f1(#)f2));
then
A3: c in dom (f1(#)f2) by Def4;
c in dom f1 /\ dom (r(#)f2) by A1,A2,Def3;
then
A4: c in dom (r(#)f2) by XBOOLE_0:def 4;
thus (r(#)(f1(#)f2))/.c = r * (f1(#)f2)/.c by A2,Def4
.= r * (f1.c * (f2/.c)) by A3,Def3
.= f1.c * r * (f2/.c) by RLVECT_1:def 7
.= f1.c * (r * (f2/.c)) by RLVECT_1:def 7
.= f1.c * ((r(#)f2)/.c) by A4,Def4
.= (f1(#)(r(#)f2))/.c by A1,A2,Def3;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for V being add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct
for f1,f2 being PartFunc of C,REAL
for f3 being Function of C,V holds
(f1 - f2)(#)f3 = f1(#)f3 - f2(#)f3
proof
let V be add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct;
let f1,f2 be PartFunc of C,REAL;
let f3 be Function of C,V;
A1: dom ((f1 - f2) (#) f3) = dom (f1 - f2) /\ dom f3 by Def3
.= dom f1 /\ dom f2 /\ (dom f3 /\ dom f3) by VALUED_1:12
.= dom f1 /\ dom f2 /\ dom f3 /\ dom f3 by XBOOLE_1:16
.= dom f1 /\ dom f3 /\ dom f2 /\ dom f3 by XBOOLE_1:16
.= dom f1 /\ dom f3 /\ (dom f2 /\ dom f3) by XBOOLE_1:16
.= dom (f1 (#) f3) /\ (dom f2 /\ dom f3) by Def3
.= dom (f1 (#) f3) /\ dom (f2 (#) f3) by Def3
.= dom (f1 (#) f3 - f2 (#) f3) by Def2;
now
let c;
assume
A2: c in dom ((f1 - f2)(#)f3);
then c in dom (f1 - f2) /\ dom f3 by Def3;
then
A3: c in dom (f1 - f2) by XBOOLE_0:def 4;
A4: c in dom (f1(#)f3) /\ dom (f2(#)f3) by A1,A2,Def2;
then
A5: c in dom (f1(#)f3) by XBOOLE_0:def 4;
A6: c in dom (f2 (#) f3) by A4,XBOOLE_0:def 4;
thus ((f1 - f2) (#) f3)/.c = (f1 - f2).c * (f3/.c) by A2,Def3
.= (f1.c - f2.c) * (f3/.c) by A3,VALUED_1:13
.= f1.c * (f3/.c) - f2.c * (f3/.c) by RLVECT_1:35
.= ((f1 (#) f3)/.c) - f2.c * (f3/.c) by A5,Def3
.= ((f1 (#) f3)/.c) - ((f2 (#) f3)/.c) by A6,Def3
.= ((f1 (#) f3) - (f2 (#) f3))/.c by A1,A2,Def2;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for V being add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct
for f1,f2 being PartFunc of C,V
for f3 be PartFunc of C,REAL holds
f3(#)f1 - f3(#)f2 = f3(#)(f1 - f2)
proof
let V be add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct;
let f1,f2 be PartFunc of C,V;
let f3 be PartFunc of C,REAL;
A1: dom (f3 (#) f1 - f3 (#) f2) = dom (f3 (#) f1) /\ dom (f3 (#) f2) by Def2
.= dom (f3 (#) f1) /\ (dom f3 /\ dom f2) by Def3
.= dom f3 /\ dom f1 /\ (dom f3 /\ dom f2) by Def3
.= dom f3 /\ (dom f3 /\ dom f1) /\ dom f2 by XBOOLE_1:16
.= dom f3 /\ dom f3 /\ dom f1 /\ dom f2 by XBOOLE_1:16
.= dom f3 /\ (dom f1 /\ dom f2) by XBOOLE_1:16
.= dom f3 /\ dom (f1 - f2) by Def2
.= dom (f3(#)(f1 - f2)) by Def3;
now
let c;
assume
A2: c in dom (f3(#)(f1 - f2));
then c in dom f3 /\ dom (f1 - f2) by Def3;
then
A3: c in dom (f1 - f2) by XBOOLE_0:def 4;
A4: c in dom (f3(#)f1) /\ dom (f3(#)f2) by A1,A2,Def2;
then
A5: c in dom (f3(#)f1) by XBOOLE_0:def 4;
A6: c in dom (f3 (#) f2) by A4,XBOOLE_0:def 4;
thus (f3 (#) (f1 - f2))/.c = f3.c * ((f1 - f2)/.c) by A2,Def3
.= f3.c * ((f1/.c) - (f2/.c)) by A3,Def2
.= f3.c * (f1/.c) - f3.c * (f2/.c) by RLVECT_1:34
.= ((f3 (#) f1)/.c) - f3.c * (f2/.c) by A5,Def3
.= ((f3 (#) f1)/.c) - ((f3 (#) f2)/.c) by A6,Def3
.= ((f3 (#) f1) - (f3 (#) f2))/.c by A1,A2,Def2;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for V being vector-distributive non empty RLSStruct
for f1,f2 being PartFunc of C,V holds
r(#)(f1 + f2) = r(#)f1 + r(#)f2
proof
let V be vector-distributive non empty RLSStruct;
let f1,f2 be PartFunc of C,V;
A1: dom (r(#)(f1 + f2)) = dom (f1 + f2) by Def4
.= dom f1 /\ dom f2 by Def1
.= dom f1 /\ dom (r(#)f2) by Def4
.= dom (r(#)f1) /\ dom (r(#)f2) by Def4
.= dom (r(#)f1 + r(#)f2) by Def1;
now
let c;
assume
A2: c in dom (r(#)(f1 + f2));
then
A3: c in dom (f1 + f2) by Def4;
A4: c in dom (r(#)f1) /\ dom (r(#)f2) by A1,A2,Def1;
then
A5: c in dom (r(#)f1) by XBOOLE_0:def 4;
A6: c in dom (r(#)f2) by A4,XBOOLE_0:def 4;
thus (r(#)(f1 + f2))/.c = r * ((f1 + f2)/.c) by A2,Def4
.= r * ((f1/.c) + (f2/.c)) by A3,Def1
.= r * (f1/.c) + r * (f2/.c) by RLVECT_1:def 5
.= ((r(#)f1)/.c) + r * (f2/.c) by A5,Def4
.= ((r(#)f1)/.c) + ((r(#)f2)/.c) by A6,Def4
.= (r(#)f1 + r(#)f2)/.c by A1,A2,Def1;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for V being scalar-associative non empty RLSStruct
for f being PartFunc of C,V holds
(r*p)(#)f = r(#)(p(#)f)
proof
let V be scalar-associative non empty RLSStruct;
let f be PartFunc of C,V;
A1: dom ((r*p) (#) f) = dom f by Def4
.= dom (p(#)f) by Def4
.= dom (r(#)(p(#)f)) by Def4;
now
let c;
assume
A2: c in dom ((r*p)(#)f);
then
A3: c in dom (p(#)f) by A1,Def4;
thus ((r*p)(#)f)/.c = r*p * f/.c by A2,Def4
.= r*(p * f/.c) by RLVECT_1:def 7
.= r * ((p(#)f)/.c) by A3,Def4
.= (r(#)(p(#)f))/.c by A1,A2,Def4;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for V being add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct
for f1,f2 being PartFunc of C,V holds
r(#)(f1 - f2) = r(#)f1 - r(#)f2
proof
let V be add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct;
let f1,f2 be PartFunc of C,V;
A1: dom (r(#)(f1 - f2)) = dom (f1 - f2) by Def4
.= dom f1 /\ dom f2 by Def2
.= dom f1 /\ dom (r(#)f2) by Def4
.= dom (r(#)f1) /\ dom (r(#)f2) by Def4
.= dom (r(#)f1 - r(#)f2) by Def2;
now
let c;
assume
A2: c in dom (r(#)(f1 - f2));
then
A3: c in dom (f1 - f2) by Def4;
A4: c in dom (r(#)f1) /\ dom (r(#)f2) by A1,A2,Def2;
then
A5: c in dom (r(#)f1) by XBOOLE_0:def 4;
A6: c in dom (r(#)f2) by A4,XBOOLE_0:def 4;
thus (r(#)(f1 - f2))/.c = r * ((f1 - f2)/.c) by A2,Def4
.= r * ((f1/.c) - (f2/.c)) by A3,Def2
.= r * (f1/.c) - r * (f2/.c) by RLVECT_1:34
.= ((r(#)f1)/.c) - r * (f2/.c) by A5,Def4
.= ((r(#)f1)/.c) - ((r(#)f2)/.c) by A6,Def4
.= (r(#)f1 - r(#)f2)/.c by A1,A2,Def2;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for V being add-associative right_zeroed right_complementable
Abelian scalar-distributive scalar-unital vector-distributive
non empty RLSStruct
for f1,f2 being PartFunc of C,V holds
f1-f2 = (-1)(#)(f2-f1)
proof
let V be add-associative right_zeroed right_complementable
Abelian scalar-distributive scalar-unital vector-distributive
non empty RLSStruct;
let f1,f2 be PartFunc of C,V;
A1: dom (f1 - f2) = dom f2 /\ dom f1 by Def2
.= dom (f2 - f1) by Def2
.= dom ((-1)(#)(f2 - f1)) by Def4;
now
A2: dom (f1 - f2) = dom f2 /\ dom f1 by Def2
.= dom (f2 - f1) by Def2;
let c such that
A3: c in dom (f1-f2);
thus (f1 - f2)/.c = (f1/.c) - (f2/.c) by A3,Def2
.= -((f2/.c) - (f1/.c)) by RLVECT_1:33
.= (-1)*((f2/.c) - (f1/.c)) by RLVECT_1:16
.= (-1)*((f2 - f1)/.c) by A3,A2,Def2
.= ((-1)(#)(f2 - f1))/.c by A1,A3,Def4;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for V being add-associative right_zeroed right_complementable Abelian
non empty addLoopStr
for f1,f2,f3 being PartFunc of C,V holds
f1 - (f2 + f3) = f1 - f2 - f3
proof
let V be add-associative right_zeroed right_complementable Abelian
non empty addLoopStr;
let f1,f2,f3 be PartFunc of C,V;
A1: dom (f1 - (f2 + f3)) = dom f1 /\ dom (f2 + f3) by Def2
.= dom f1 /\ (dom f2 /\ dom f3) by Def1
.= dom f1 /\ dom f2 /\ dom f3 by XBOOLE_1:16
.= dom (f1 - f2) /\ dom f3 by Def2
.= dom (f1 - f2 - f3) by Def2;
now
let c;
assume
A2: c in dom (f1 - (f2 + f3));
then c in dom f1 /\ dom (f2 + f3) by Def2;
then
A3: c in dom (f2 + f3) by XBOOLE_0:def 4;
c in dom (f1 - f2) /\ dom f3 by A1,A2,Def2;
then
A4: c in dom (f1 - f2) by XBOOLE_0:def 4;
thus (f1 - (f2 + f3))/.c = (f1/.c) - ((f2 + f3)/.c) by A2,Def2
.= (f1/.c) - ((f2/.c) + (f3/.c)) by A3,Def1
.= (f1/.c) - (f2/.c) - (f3/.c) by RLVECT_1:27
.= ((f1 - f2)/.c) - (f3/.c) by A4,Def2
.= (f1 - f2 - f3)/.c by A1,A2,Def2;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for V being scalar-unital non empty RLSStruct
for f being PartFunc of C,V holds
1(#)f = f
proof
let V be scalar-unital non empty RLSStruct;
let f be PartFunc of C,V;
A1: now
let c;
assume c in dom (1(#)f);
hence (1(#)f)/.c = 1 * f/.c by Def4
.= f/.c by RLVECT_1:def 8;
end;
dom (1(#)f) = dom f by Def4;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr
for f1,f2,f3 being PartFunc of C,V holds
f1 - (f2 - f3) = f1 - f2 + f3
proof
let V be Abelian add-associative right_zeroed right_complementable
non empty addLoopStr;
let f1,f2,f3 be PartFunc of C,V;
A1: dom (f1 - (f2 - f3)) = dom f1 /\ dom (f2 - f3) by Def2
.= dom f1 /\ (dom f2 /\ dom f3) by Def2
.= dom f1 /\ dom f2 /\ dom f3 by XBOOLE_1:16
.= dom (f1 - f2) /\ dom f3 by Def2
.= dom (f1 - f2 + f3) by Def1;
now
let c;
assume
A2: c in dom (f1 - (f2 - f3));
then c in dom f1 /\ dom (f2 - f3) by Def2;
then
A3: c in dom (f2 - f3) by XBOOLE_0:def 4;
c in dom (f1 - f2) /\ dom f3 by A1,A2,Def1;
then
A4: c in dom (f1 - f2) by XBOOLE_0:def 4;
thus (f1 - (f2 - f3))/.c = (f1/.c) - ((f2 - f3)/.c) by A2,Def2
.= (f1/.c) - ((f2/.c) - (f3/.c)) by A3,Def2
.= (f1/.c) - (f2/.c) + (f3/.c) by RLVECT_1:29
.= ((f1 - f2)/.c) + (f3/.c) by A4,Def2
.= (f1 - f2 + f3)/.c by A1,A2,Def1;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for V being add-associative non empty addLoopStr
for f1,f2,f3 being PartFunc of C,V holds
f1 + (f2 - f3) = f1 + f2 - f3
proof
let V be add-associative non empty addLoopStr;
let f1,f2,f3 be PartFunc of C,V;
A1: dom (f1 + (f2 - f3)) = dom f1 /\ dom (f2 - f3) by Def1
.= dom f1 /\ (dom f2 /\ dom f3) by Def2
.= dom f1 /\ dom f2 /\ dom f3 by XBOOLE_1:16
.= dom (f1 + f2) /\ dom f3 by Def1
.= dom (f1 + f2 - f3) by Def2;
now
let c;
assume
A2: c in dom (f1 + (f2 - f3));
then c in dom f1 /\ dom (f2 - f3) by Def1;
then
A3: c in dom (f2 - f3) by XBOOLE_0:def 4;
c in dom (f1 + f2) /\ dom f3 by A1,A2,Def2;
then
A4: c in dom (f1 + f2) by XBOOLE_0:def 4;
thus (f1 + (f2 - f3))/.c = (f1/.c) + ((f2 - f3)/.c) by A2,Def1
.= (f1/.c) + ((f2/.c) - (f3/.c)) by A3,Def2
.= (f1/.c) + (f2/.c) - (f3/.c) by RLVECT_1:def 3
.= ((f1 + f2)/.c) - (f3/.c) by A4,Def1
.= (f1 + f2 - f3)/.c by A1,A2,Def2;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for V being RealNormSpace-like non empty NORMSTR
for f1 being PartFunc of C,REAL
for f2 being PartFunc of C,V holds
||.f1(#)f2.|| = abs(f1)(#)||.f2.||
proof
let V be RealNormSpace-like non empty NORMSTR;
let f1 be PartFunc of C,REAL;
let f2 be PartFunc of C,V;
A1: dom (||.f1 (#) f2.||) = dom (f1 (#) f2) by NORMSP_0:def 3
.= dom f1 /\ dom f2 by Def3
.= dom f1 /\ dom (||.f2.||) by NORMSP_0:def 3
.= dom (abs(f1)) /\ dom (||.f2.||) by VALUED_1:def 11
.= dom (abs(f1)(#)||.f2.||) by VALUED_1:def 4;
now
let c;
assume
A2: c in dom (||.f1 (#) f2.||);
then
A3: c in dom (f1 (#) f2) by NORMSP_0:def 3;
c in dom (abs(f1)) /\ dom (||.f2.||) by A1,A2,VALUED_1:def 4;
then
A4: c in dom (||.f2.||) by XBOOLE_0:def 4;
thus (||.f1(#)f2.||).c = ||.(f1(#)f2)/.c.|| by A2,NORMSP_0:def 3
.= ||.f1.c * (f2/.c).|| by A3,Def3
.= |.f1.c.| * ||.(f2/.c).|| by NORMSP_1:def 1
.= ((abs(f1)).c) * ||.(f2/.c).|| by VALUED_1:18
.= ((abs(f1)).c) * (||.f2.||).c by A4,NORMSP_0:def 3
.= (abs(f1)(#)||.f2.||).c by VALUED_1:5;
end;
hence thesis by A1,PARTFUN1:5;
end;
theorem
for V being RealNormSpace-like non empty NORMSTR
for f being PartFunc of C,V holds
||.r(#)f.|| = |.r.|(#)||.f.||
proof
let V be RealNormSpace-like non empty NORMSTR;
let f be PartFunc of C,V;
A1: dom (||.r(#)f.||) = dom (r(#)f) by NORMSP_0:def 3
.= dom f by Def4
.= dom (||.f.||) by NORMSP_0:def 3
.= dom (|.r.|(#)||.f.||) by VALUED_1:def 5;
now
let c;
assume
A2: c in dom (||.r(#)f.||);
then
A3: c in dom (||.f.||) by A1,VALUED_1:def 5;
A4: c in dom (r(#)f) by A2,NORMSP_0:def 3;
thus (||.r(#)f.||).c = ||.(r(#)f)/.c.|| by A2,NORMSP_0:def 3
.=||.r*(f/.c).|| by A4,Def4
.=|.r.|*||.f/.c.|| by NORMSP_1:def 1
.=|.r.|*(||.f.||.c) by A3,NORMSP_0:def 3
.=(|.r.|(#)||.f.||).c by A1,A2,VALUED_1:def 5;
end;
hence thesis by A1,PARTFUN1:5;
end;
theorem Th23:
for V being add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-unital vector-distributive
non empty RLSStruct
for f being PartFunc of C,V holds
-f = (-1)(#)f
proof
let V be add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-unital vector-distributive
non empty RLSStruct;
let f be PartFunc of C,V;
A1: dom (-f) = dom f by Def5
.= dom ((-1)(#)f) by Def4;
now
let c;
assume
A2: c in dom ((-1)(#)f);
hence (-f)/.c = -(f/.c) by A1,Def5
.= (-1) * f/.c by RLVECT_1:16
.= ((-1)(#)f)/.c by A2,Def4;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem Th24:
for V being add-associative right_zeroed right_complementable
non empty addLoopStr
for f being PartFunc of C,V holds
-(-f) = f
proof
let V be add-associative right_zeroed right_complementable
non empty addLoopStr;
let f be PartFunc of C,V;
A1: dom(--f) = dom(-f) by Def5;
A2: dom(-f) = dom(f) by Def5;
now
let c;
assume
A3: c in dom(f);
hence (--f)/.c = -((-f)/.c) by A1,A2,Def5
.= --(f/.c) by A2,A3,Def5
.= f/.c;
end;
hence thesis by A1,A2,PARTFUN2:1;
end;
theorem Th25:
for V being non empty addLoopStr
for f1,f2 being PartFunc of C,V holds
f1 - f2 = f1 + -f2
proof
let V be non empty addLoopStr;
let f1,f2 be PartFunc of C,V;
A1: dom (f1 - f2) = dom f1 /\ dom f2 by Def2
.= dom f1 /\ dom (-f2) by Def5
.= dom (f1 + -f2) by Def1;
now
let c;
assume
A2: c in dom (f1+-f2);
then c in dom f1 /\ dom (-f2) by Def1;
then
A3: c in dom (-f2) by XBOOLE_0:def 4;
thus (f1 + -f2)/.c = (f1/.c) + ((-f2)/.c) by A2,Def1
.= (f1/.c) - (f2/.c) by A3,Def5
.= (f1-f2)/.c by A1,A2,Def2;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for V being add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-unital scalar-associative vector-distributive
non empty RLSStruct
for f1,f2 being PartFunc of C,V holds
f1 - (-f2) = f1 + f2
proof
let V be add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-unital scalar-associative vector-distributive
non empty RLSStruct;
let f1,f2 be PartFunc of C,V;
thus f1 - (-f2) = f1 + (-(-f2)) by Th25
.= f1 + f2 by Th24;
end;
theorem Th27:
(f1+f2)|X = f1|X + f2|X & (f1+f2)|X = f1|X + f2 & (f1+f2)|X = f1 + f2|X
proof
A1: now
let c;
assume
A2: c in dom ((f1+f2)|X);
then
A3: c in dom (f1+f2) /\ X by RELAT_1:61;
then
A4: c in X by XBOOLE_0:def 4;
A5: c in dom (f1+f2) by A3,XBOOLE_0:def 4;
then
A6: c in dom f1 /\ dom f2 by Def1;
then c in dom f2 by XBOOLE_0:def 4;
then c in dom f2 /\ X by A4,XBOOLE_0:def 4;
then
A7: c in dom (f2|X) by RELAT_1:61;
c in dom f1 by A6,XBOOLE_0:def 4;
then c in dom f1 /\ X by A4,XBOOLE_0:def 4;
then
A8: c in dom (f1|X) by RELAT_1:61;
then c in dom (f1|X) /\ dom (f2|X) by A7,XBOOLE_0:def 4;
then
A9: c in dom ((f1|X) + (f2|X)) by Def1;
thus ((f1+f2)|X)/.c = (f1+f2)/.c by A2,PARTFUN2:15
.= (f1/.c) + (f2/.c) by A5,Def1
.= ((f1|X)/.c) + (f2/.c) by A8,PARTFUN2:15
.= ((f1|X)/.c) + ((f2|X)/.c) by A7,PARTFUN2:15
.= ((f1|X)+(f2|X))/.c by A9,Def1;
end;
dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ (X /\ X) by Def1
.= dom f1 /\ (dom f2 /\ (X /\ X)) by XBOOLE_1:16
.= dom f1 /\ (dom f2 /\ X /\ X) by XBOOLE_1:16
.= dom f1 /\ (X /\ dom (f2|X)) by RELAT_1:61
.= dom f1 /\ X /\ dom (f2|X) by XBOOLE_1:16
.= dom (f1|X) /\ dom (f2|X) by RELAT_1:61
.= dom ((f1|X)+(f2|X)) by Def1;
hence (f1+f2)|X = f1|X + f2|X by A1,PARTFUN2:1;
A10: now
let c;
assume
A11: c in dom ((f1+f2)|X);
then
A12: c in dom (f1+f2) /\ X by RELAT_1:61;
then
A13: c in X by XBOOLE_0:def 4;
A14: c in dom (f1+f2) by A12,XBOOLE_0:def 4;
then
A15: c in dom f1 /\ dom f2 by Def1;
then c in dom f1 by XBOOLE_0:def 4;
then c in dom f1 /\ X by A13,XBOOLE_0:def 4;
then
A16: c in dom (f1|X) by RELAT_1:61;
c in dom f2 by A15,XBOOLE_0:def 4;
then c in dom (f1|X) /\ dom f2 by A16,XBOOLE_0:def 4;
then
A17: c in dom ((f1|X) + f2) by Def1;
thus ((f1+f2)|X)/.c = (f1+f2)/.c by A11,PARTFUN2:15
.= (f1/.c) + (f2/.c) by A14,Def1
.= ((f1|X)/.c) +(f2/.c) by A16,PARTFUN2:15
.= ((f1|X)+f2)/.c by A17,Def1;
end;
dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ X by Def1
.= dom f1 /\ X /\ dom f2 by XBOOLE_1:16
.= dom (f1|X) /\ dom f2 by RELAT_1:61
.= dom ((f1|X)+ f2) by Def1;
hence (f1+f2)|X = f1|X + f2 by A10,PARTFUN2:1;
A18: now
let c;
assume
A19: c in dom ((f1+f2)|X);
then
A20: c in dom (f1+f2) /\ X by RELAT_1:61;
then
A21: c in X by XBOOLE_0:def 4;
A22: c in dom (f1+f2) by A20,XBOOLE_0:def 4;
then
A23: c in dom f1 /\ dom f2 by Def1;
then c in dom f2 by XBOOLE_0:def 4;
then c in dom f2 /\ X by A21,XBOOLE_0:def 4;
then
A24: c in dom (f2|X) by RELAT_1:61;
c in dom f1 by A23,XBOOLE_0:def 4;
then c in dom f1 /\ dom (f2|X) by A24,XBOOLE_0:def 4;
then
A25: c in dom (f1 + (f2|X)) by Def1;
thus ((f1+f2)|X)/.c = (f1+f2)/.c by A19,PARTFUN2:15
.= (f1/.c) +(f2/.c) by A22,Def1
.= (f1/.c) + ((f2|X)/.c) by A24,PARTFUN2:15
.= (f1+(f2|X))/.c by A25,Def1;
end;
dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ X by Def1
.= dom f1 /\ (dom f2 /\ X) by XBOOLE_1:16
.= dom f1 /\ dom (f2|X) by RELAT_1:61
.= dom (f1 + (f2|X)) by Def1;
hence thesis by A18,PARTFUN2:1;
end;
theorem
for f1 be PartFunc of C,REAL holds
(f1(#)f2)|X = f1|X (#) f2|X & (f1(#)f2)|X = f1|X (#) f2 &
(f1(#)f2)|X = f1 (#) f2|X
proof
let f1 be PartFunc of C,REAL;
A1: now
let c;
assume
A2: c in dom ((f1(#)f2)|X);
then
A3: c in dom (f1(#)f2) /\ X by RELAT_1:61;
then
A4: c in X by XBOOLE_0:def 4;
A5: c in dom (f1(#)f2) by A3,XBOOLE_0:def 4;
then
A6: c in dom f1 /\ dom f2 by Def3;
then c in dom f2 by XBOOLE_0:def 4;
then c in dom f2 /\ X by A4,XBOOLE_0:def 4;
then
A7: c in dom (f2|X) by RELAT_1:61;
c in dom f1 by A6,XBOOLE_0:def 4;
then c in dom f1 /\ X by A4,XBOOLE_0:def 4;
then
A8: c in dom (f1|X) by RELAT_1:61;
then c in dom (f1|X) /\ dom (f2|X) by A7,XBOOLE_0:def 4;
then
A9: c in dom ((f1|X) (#) (f2|X)) by Def3;
thus ((f1(#)f2)|X)/.c = (f1(#)f2)/.c by A2,PARTFUN2:15
.= (f1.c) * (f2/.c) by A5,Def3
.= ((f1|X).c) * (f2/.c) by A8,FUNCT_1:47
.= ((f1|X).c) * ((f2|X)/.c) by A7,PARTFUN2:15
.= ((f1|X)(#)(f2|X))/.c by A9,Def3;
end;
dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ (X /\ X) by Def3
.= dom f1 /\ (dom f2 /\ (X /\ X)) by XBOOLE_1:16
.= dom f1 /\ (dom f2 /\ X /\ X) by XBOOLE_1:16
.= dom f1 /\ (X /\ dom (f2|X)) by RELAT_1:61
.= dom f1 /\ X /\ dom (f2|X) by XBOOLE_1:16
.= dom (f1|X) /\ dom (f2|X) by RELAT_1:61
.= dom ((f1|X)(#)(f2|X)) by Def3;
hence (f1(#)f2)|X = f1|X (#) f2|X by A1,PARTFUN2:1;
A10: now
let c;
assume
A11: c in dom ((f1(#)f2)|X);
then
A12: c in dom (f1(#)f2) /\ X by RELAT_1:61;
then
A13: c in X by XBOOLE_0:def 4;
A14: c in dom (f1(#)f2) by A12,XBOOLE_0:def 4;
then
A15: c in dom f1 /\ dom f2 by Def3;
then c in dom f1 by XBOOLE_0:def 4;
then c in dom f1 /\ X by A13,XBOOLE_0:def 4;
then
A16: c in dom (f1|X) by RELAT_1:61;
c in dom f2 by A15,XBOOLE_0:def 4;
then c in dom (f1|X) /\ dom f2 by A16,XBOOLE_0:def 4;
then
A17: c in dom ((f1|X) (#) f2) by Def3;
thus ((f1(#)f2)|X)/.c = (f1(#)f2)/.c by A11,PARTFUN2:15
.= (f1.c) * (f2/.c) by A14,Def3
.= ((f1|X).c) * (f2/.c) by A16,FUNCT_1:47
.= ((f1|X)(#)f2)/.c by A17,Def3;
end;
dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ X by Def3
.= dom f1 /\ X /\ dom f2 by XBOOLE_1:16
.= dom (f1|X) /\ dom f2 by RELAT_1:61
.= dom ((f1|X)(#) f2) by Def3;
hence (f1(#)f2)|X = f1|X (#) f2 by A10,PARTFUN2:1;
A18: now
let c;
assume
A19: c in dom ((f1(#)f2)|X);
then
A20: c in dom (f1(#)f2) /\ X by RELAT_1:61;
then
A21: c in X by XBOOLE_0:def 4;
A22: c in dom (f1(#)f2) by A20,XBOOLE_0:def 4;
then
A23: c in dom f1 /\ dom f2 by Def3;
then c in dom f2 by XBOOLE_0:def 4;
then c in dom f2 /\ X by A21,XBOOLE_0:def 4;
then
A24: c in dom (f2|X) by RELAT_1:61;
c in dom f1 by A23,XBOOLE_0:def 4;
then c in dom f1 /\ dom (f2|X) by A24,XBOOLE_0:def 4;
then
A25: c in dom (f1 (#) (f2|X)) by Def3;
thus ((f1(#)f2)|X)/.c = (f1(#)f2)/.c by A19,PARTFUN2:15
.= (f1.c) * (f2/.c) by A22,Def3
.= (f1.c) * ((f2|X)/.c) by A24,PARTFUN2:15
.= (f1(#)(f2|X))/.c by A25,Def3;
end;
dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ X by Def3
.= dom f1 /\ (dom f2 /\ X) by XBOOLE_1:16
.= dom f1 /\ dom (f2|X) by RELAT_1:61
.= dom (f1 (#) (f2|X)) by Def3;
hence thesis by A18,PARTFUN2:1;
end;
theorem Th29:
(-f)|X = -(f|X) & (||.f.||)|X = ||.(f|X).||
proof
A1: now
let c;
assume
A2: c in dom ((-f)|X);
then
A3: c in dom (-f) /\ X by RELAT_1:61;
then
A4: c in X by XBOOLE_0:def 4;
A5: c in dom (-f) by A3,XBOOLE_0:def 4;
then c in dom f by Def5;
then c in dom f /\ X by A4,XBOOLE_0:def 4;
then
A6: c in dom (f|X) by RELAT_1:61;
then
A7: c in dom (-(f|X)) by Def5;
thus ((-f)|X)/.c = (-f)/.c by A2,PARTFUN2:15
.= -(f/.c) by A5,Def5
.= -((f|X)/.c) by A6,PARTFUN2:15
.= (-(f|X))/.c by A7,Def5;
end;
dom ((-f)|X) = dom (-f) /\ X by RELAT_1:61
.= dom f /\ X by Def5
.= dom (f|X) by RELAT_1:61
.= dom (-(f|X)) by Def5;
hence (-f)|X = -(f|X) by A1,PARTFUN2:1;
A8: dom ((||.f.||)|X) = dom (||.f.||) /\ X by RELAT_1:61
.= dom f /\ X by NORMSP_0:def 3
.= dom (f|X) by RELAT_1:61
.= dom (||.(f|X).||) by NORMSP_0:def 3;
now
let c;
assume
A9: c in dom ((||.f.||)|X);
then
A10: c in dom (f|X) by A8,NORMSP_0:def 3;
c in dom (||.f.||) /\ X by A9,RELAT_1:61;
then
A11: c in dom (||.f.||) by XBOOLE_0:def 4;
thus ((||.f.||)|X).c = (||.f.||).c by A9,FUNCT_1:47
.= ||.f/.c.|| by A11,NORMSP_0:def 3
.= ||.(f|X)/.c.|| by A10,PARTFUN2:15
.= (||.(f|X).||).c by A8,A9,NORMSP_0:def 3;
end;
hence thesis by A8,PARTFUN1:5;
end;
theorem
(f1-f2)|X = f1|X - f2|X & (f1-f2)|X = f1|X - f2 &(f1-f2)|X = f1 - f2|X
proof
thus (f1-f2)|X = (f1+-f2)|X by Th25
.= (f1|X)+ (-f2)|X by Th27
.= (f1|X)+ -(f2|X) by Th29
.= (f1|X) - (f2|X) by Th25;
thus (f1-f2)|X = (f1+-f2)|X by Th25
.= (f1|X)+ -f2 by Th27
.= (f1|X) - f2 by Th25;
thus (f1-f2)|X = (f1+-f2)|X by Th25
.= f1+ (-f2)|X by Th27
.= f1 +- (f2|X) by Th29
.= f1 - (f2|X) by Th25;
end;
theorem
(r(#)f)|X = r(#)(f|X)
proof
A1: now
let c;
assume
A2: c in dom ((r(#)f)|X);
then
A3: c in dom (r(#)f) /\ X by RELAT_1:61;
then
A4: c in X by XBOOLE_0:def 4;
A5: c in dom (r(#)f) by A3,XBOOLE_0:def 4;
then c in dom f by Def4;
then c in dom f /\ X by A4,XBOOLE_0:def 4;
then
A6: c in dom (f|X) by RELAT_1:61;
then
A7: c in dom (r(#)(f|X)) by Def4;
thus ((r(#)f)|X)/.c = (r(#)f)/.c by A2,PARTFUN2:15
.= r*(f/.c) by A5,Def4
.= r*((f|X)/.c) by A6,PARTFUN2:15
.= (r(#)(f|X))/.c by A7,Def4;
end;
dom ((r(#)f)|X) = dom (r(#)f) /\ X by RELAT_1:61
.= dom f /\ X by Def4
.= dom (f|X) by RELAT_1:61
.= dom (r(#)(f|X)) by Def4;
hence thesis by A1,PARTFUN2:1;
end;
::
:: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN TO REAL
::
theorem
(f1 is total & f2 is total iff f1+f2 is total) & (f1 is total &
f2 is total iff f1-f2 is total)
proof
thus f1 is total & f2 is total iff f1+f2 is total
proof
thus f1 is total & f2 is total implies f1+f2 is total;
assume f1+f2 is total;
then dom f1 /\ dom f2 = C by Def1;
hence dom f1 = C & dom f2 = C by XBOOLE_1:17;
end;
thus f1 is total & f2 is total iff f1-f2 is total
proof
thus f1 is total & f2 is total implies f1-f2 is total;
assume f1-f2 is total;
then dom f1 /\ dom f2 = C by Def2;
hence dom f1 = C & dom f2 = C by XBOOLE_1:17;
end;
end;
theorem
for f1 be PartFunc of C,REAL holds (f1 is total & f2 is total
iff f1(#)f2 is total)
proof
let f1 be PartFunc of C,REAL;
thus f1 is total & f2 is total implies f1(#)f2 is total;
assume f1(#)f2 is total;
then dom f1 /\ dom f2 = C by Def3;
hence dom f1 = C & dom f2 = C by XBOOLE_1:17;
end;
theorem
f is total iff r(#)f is total by Def4;
theorem
f is total iff -f is total
proof
thus f is total implies -f is total;
assume
A1: -f is total;
-f = (-1)(#)f by Th23;
hence thesis by A1,Def4;
end;
theorem
f is total iff ||.f.|| is total by NORMSP_0:def 3;
theorem
f1 is total & f2 is total implies (f1+f2)/.c = (f1/.c) + (f2/.c) &
(f1-f2)/.c = (f1/.c) - (f2/.c)
proof
assume
A1: f1 is total & f2 is total;
then dom (f1+f2) = C by PARTFUN1:def 2;
hence (f1+f2)/.c = (f1/.c) + (f2/.c) by Def1;
dom (f1-f2) = C by A1,PARTFUN1:def 2;
hence thesis by Def2;
end;
theorem
for f1 be PartFunc of C,REAL holds f1 is total & f2 is total implies
(f1(#)f2)/.c = f1.c * (f2/.c)
proof
let f1 be PartFunc of C,REAL;
assume f1 is total & f2 is total;
then dom (f1(#)f2) = C by PARTFUN1:def 2;
hence thesis by Def3;
end;
theorem
f is total implies (r(#)f)/.c = r * (f/.c)
proof
assume f is total;
then dom (r(#)f) = C by PARTFUN1:def 2;
hence thesis by Def4;
end;
theorem
f is total implies (-f)/.c = - f/.c & (||.f.||).c = ||. f/.c .||
proof
assume
A1: f is total;
then dom (-f) = C by PARTFUN1:def 2;
hence (-f)/.c = - f/.c by Def5;
||.f.|| is total by A1,NORMSP_0:def 3;
hence thesis by NORMSP_0:def 3;
end;
::
:: BOUNDED AND CONSTANT PARTIAL FUNCTIONS FROM A DOMAIN TO A NORMED REAL SPACE
::
definition
let C;
let V be non empty NORMSTR;
let f be PartFunc of C,V;
let Y;
pred f is_bounded_on Y means
ex r st for c st c in Y /\ dom f holds ||.f/.c.|| <= r;
end;
theorem
Y c= X & f is_bounded_on X implies f is_bounded_on Y
proof
assume that
A1: Y c= X and
A2: f is_bounded_on X;
consider r such that
A3: for c st c in X /\ dom f holds ||.f/.c.|| <= r by A2;
take r;
let c;
assume c in Y /\ dom f;
then c in Y & c in dom f by XBOOLE_0:def 4;
then c in X /\ dom f by A1,XBOOLE_0:def 4;
hence thesis by A3;
end;
theorem
X misses dom f implies f is_bounded_on X
proof
assume X /\ dom f = {};
then for c holds c in X /\ dom f implies ||.f/.c.|| <= 0;
hence thesis;
end;
theorem
0(#)f is_bounded_on Y
proof
now
take p=0;
let c;
0*||.f/.c.|| = 0;
then |.0 .|*||.f/.c.|| <= 0 by ABSVALUE:2;
then
A1: ||.0*(f/.c).|| <= 0 by NORMSP_1:def 1;
assume c in Y /\ dom (0(#)f);
then c in dom (0(#)f) by XBOOLE_0:def 4;
hence ||.(0(#)f)/.c.|| <= p by A1,Def4;
end;
hence thesis;
end;
theorem Th44:
f is_bounded_on Y implies r(#)f is_bounded_on Y
proof
assume f is_bounded_on Y;
then consider r1 such that
A1: for c st c in Y /\ dom f holds ||.f/.c.|| <= r1;
take p = |.r.|*|.r1.|;
let c;
assume
A2: c in Y /\ dom (r(#)f);
then
A3: c in Y by XBOOLE_0:def 4;
A4: c in dom (r(#)f) by A2,XBOOLE_0:def 4;
then c in dom f by Def4;
then c in Y /\ dom f by A3,XBOOLE_0:def 4;
then
A5: ||.f/.c.|| <= r1 by A1;
r1 <= |.r1.| by ABSVALUE:4;
then |.r.| >= 0 & ||.f/.c.|| <= |.r1.| by A5,COMPLEX1:46,XXREAL_0:2;
then |.r.| * ||.(f/.c).|| <= |.r.|*|.r1.| by XREAL_1:64;
then ||.r * (f/.c).|| <= p by NORMSP_1:def 1;
hence thesis by A4,Def4;
end;
theorem Th45:
f is_bounded_on Y implies ||.f.|||Y is bounded & -f is_bounded_on Y
proof
assume
A1: f is_bounded_on Y;
then consider r1 such that
A2: for c st c in Y /\ dom f holds ||.f/.c.|| <= r1;
now
let c be object;
assume
A3: c in Y /\ dom (||.f.||);
then
A4: c in Y by XBOOLE_0:def 4;
A5: c in dom (||.f.||) by A3,XBOOLE_0:def 4;
then c in dom f by NORMSP_0:def 3;
then c in Y /\ dom f by A4,XBOOLE_0:def 4;
then ||.f/.c.|| >= 0 & ||.f/.c.|| <= r1 by A2,NORMSP_1:4;
then |.||.f/.c.||.| <= r1 by ABSVALUE:def 1;
hence |.(||.f.||).c.| <= r1 by A5,NORMSP_0:def 3;
end;
hence ||.f.|||Y is bounded by RFUNCT_1:73;
(-1)(#)f is_bounded_on Y by A1,Th44;
hence thesis by Th23;
end;
theorem Th46:
f1 is_bounded_on X & f2 is_bounded_on Y implies f1+f2 is_bounded_on (X /\ Y)
proof
assume that
A1: f1 is_bounded_on X and
A2: f2 is_bounded_on Y;
consider r1 such that
A3: for c st c in X /\ dom f1 holds ||.(f1/.c).|| <= r1 by A1;
consider r2 such that
A4: for c st c in Y /\ dom f2 holds ||.(f2/.c).|| <= r2 by A2;
take r=r1+r2;
let c;
assume
A5: c in X /\ Y /\ dom (f1+f2);
then
A6: c in X /\ Y by XBOOLE_0:def 4;
then
A7: c in Y by XBOOLE_0:def 4;
A8: c in dom (f1+f2) by A5,XBOOLE_0:def 4;
then
A9: c in dom f1 /\ dom f2 by Def1;
then c in dom f2 by XBOOLE_0:def 4;
then c in Y /\ dom f2 by A7,XBOOLE_0:def 4;
then
A10: ||.(f2/.c).|| <= r2 by A4;
A11: c in X by A6,XBOOLE_0:def 4;
c in dom f1 by A9,XBOOLE_0:def 4;
then c in X /\ dom f1 by A11,XBOOLE_0:def 4;
then ||.(f1/.c).|| <= r1 by A3;
then ||.(f1/.c) + (f2/.c).|| <= ||.(f1/.c).|| + ||.f2/.c.|| & ||.(f1/.c).||
+ ||. (f2/.c).|| <= r by A10,NORMSP_1:def 1,XREAL_1:7;
then ||.(f1/.c) + (f2/.c).|| <= r by XXREAL_0:2;
hence thesis by A8,Def1;
end;
theorem
for f1 be PartFunc of C,REAL holds f1|X is bounded & f2 is_bounded_on
Y implies f1(#)f2 is_bounded_on (X /\ Y)
proof
let f1 be PartFunc of C,REAL;
assume that
A1: f1|X is bounded and
A2: f2 is_bounded_on Y;
consider r1 be Real such that
A3: for c being object st c in X /\ dom f1 holds |.f1.c.| <= r1
by A1,RFUNCT_1:73;
consider r2 such that
A4: for c st c in Y /\ dom f2 holds ||.(f2/.c).|| <= r2 by A2;
reconsider r1 as Real;
now
take r=r1*r2;
let c;
assume
A5: c in X /\ Y /\ dom (f1(#)f2);
then
A6: c in X /\ Y by XBOOLE_0:def 4;
then
A7: c in X by XBOOLE_0:def 4;
A8: c in dom (f1(#)f2) by A5,XBOOLE_0:def 4;
then
A9: c in dom f1 /\ dom f2 by Def3;
then c in dom f1 by XBOOLE_0:def 4;
then c in X /\ dom f1 by A7,XBOOLE_0:def 4;
then
A10: |.f1.c.| <= r1 by A3;
A11: c in Y by A6,XBOOLE_0:def 4;
c in dom f2 by A9,XBOOLE_0:def 4;
then c in Y /\ dom f2 by A11,XBOOLE_0:def 4;
then
A12: ||.(f2/.c).|| <= r2 by A4;
0<=|.f1.c.| & 0<=||.(f2/.c).|| by COMPLEX1:46,NORMSP_1:4;
then |.f1.c.|*||.(f2/.c).|| <= r by A10,A12,XREAL_1:66;
then ||.f1.c * (f2/.c).|| <= r by NORMSP_1:def 1;
hence ||.(f1(#)f2)/.c.|| <= r by A8,Def3;
end;
hence thesis;
end;
theorem
f1 is_bounded_on X & f2 is_bounded_on Y implies f1-f2 is_bounded_on X /\ Y
proof
assume that
A1: f1 is_bounded_on X and
A2: f2 is_bounded_on Y;
-f2 is_bounded_on Y by A2,Th45;
then f1+-f2 is_bounded_on (X /\ Y) by A1,Th46;
hence thesis by Th25;
end;
theorem
f is_bounded_on X & f is_bounded_on Y implies f is_bounded_on X \/ Y
proof
assume that
A1: f is_bounded_on X and
A2: f is_bounded_on Y;
consider r1 such that
A3: for c st c in X /\ dom f holds ||.f/.c.|| <= r1 by A1;
consider r2 such that
A4: for c st c in Y /\ dom f holds ||.f/.c.|| <= r2 by A2;
take r = |.r1.| + |.r2.|;
let c;
assume
A5: c in (X \/ Y) /\ dom f;
then
A6: c in dom f by XBOOLE_0:def 4;
A7: c in X \/ Y by A5,XBOOLE_0:def 4;
now
per cases by A7,XBOOLE_0:def 3;
suppose
c in X;
then c in X /\ dom f by A6,XBOOLE_0:def 4;
then
A8: ||.f/.c.|| <= r1 by A3;
A9: 0 <= |.r2.| by COMPLEX1:46;
r1 <= |.r1.| by ABSVALUE:4;
then ||.f/.c.|| <= |.r1.| by A8,XXREAL_0:2;
then ||.f/.c.|| + 0 <= r by A9,XREAL_1:7;
hence thesis;
end;
suppose
c in Y;
then c in Y /\ dom f by A6,XBOOLE_0:def 4;
then
A10: ||.f/.c.|| <= r2 by A4;
A11: 0 <= |.r1.| by COMPLEX1:46;
r2 <= |.r2.| by ABSVALUE:4;
then ||.f/.c.|| <= |.r2.| by A10,XXREAL_0:2;
then 0 + ||.f/.c.|| <= r by A11,XREAL_1:7;
hence thesis;
end;
end;
hence thesis;
end;
theorem
f1|X is constant & f2|Y is constant implies (f1+f2)|(X /\ Y) is
constant & (f1-f2)|(X /\ Y) is constant
proof
assume that
A1: f1|X is constant and
A2: f2|Y is constant;
consider r1 being VECTOR of V such that
A3: for c st c in X /\ dom f1 holds (f1/.c) = r1 by A1,PARTFUN2:35;
consider r2 being VECTOR of V such that
A4: for c st c in Y /\ dom f2 holds (f2/.c) = r2 by A2,PARTFUN2:35;
now
let c;
assume
A5: c in X /\ Y /\ dom (f1+f2);
then
A6: c in X /\ Y by XBOOLE_0:def 4;
then
A7: c in X by XBOOLE_0:def 4;
A8: c in dom (f1+f2) by A5,XBOOLE_0:def 4;
then
A9: c in (dom f1 /\ dom f2) by Def1;
then c in dom f1 by XBOOLE_0:def 4;
then
A10: c in X /\ dom f1 by A7,XBOOLE_0:def 4;
A11: c in Y by A6,XBOOLE_0:def 4;
c in dom f2 by A9,XBOOLE_0:def 4;
then
A12: c in Y /\ dom f2 by A11,XBOOLE_0:def 4;
thus (f1+f2)/.c = (f1/.c) + (f2/.c) by A8,Def1
.= r1 + (f2/.c) by A3,A10
.= r1 + r2 by A4,A12;
end;
hence (f1+f2)|(X /\ Y) is constant by PARTFUN2:35;
now
let c;
assume
A13: c in X /\ Y /\ dom (f1-f2);
then
A14: c in X /\ Y by XBOOLE_0:def 4;
then
A15: c in X by XBOOLE_0:def 4;
A16: c in dom (f1-f2) by A13,XBOOLE_0:def 4;
then
A17: c in (dom f1 /\ dom f2) by Def2;
then c in dom f1 by XBOOLE_0:def 4;
then
A18: c in X /\ dom f1 by A15,XBOOLE_0:def 4;
A19: c in Y by A14,XBOOLE_0:def 4;
c in dom f2 by A17,XBOOLE_0:def 4;
then
A20: c in Y /\ dom f2 by A19,XBOOLE_0:def 4;
thus (f1-f2)/.c = (f1/.c) - (f2/.c) by A16,Def2
.= r1 - (f2/.c) by A3,A18
.= r1 - r2 by A4,A20;
end;
hence thesis by PARTFUN2:35;
end;
theorem
for f1 be PartFunc of C,REAL holds f1|X is constant & f2|Y is constant
implies (f1(#)f2)|(X /\ Y) is constant
proof
let f1 be PartFunc of C,REAL;
assume that
A1: f1|X is constant and
A2: f2|Y is constant;
consider r1 being Element of REAL such that
A3: for c st c in X /\ dom f1 holds f1.c = r1 by A1,PARTFUN2:57;
consider r2 being VECTOR of V such that
A4: for c st c in Y /\ dom f2 holds (f2/.c) = r2 by A2,PARTFUN2:35;
now
let c;
assume
A5: c in X /\ Y /\ dom (f1(#)f2);
then
A6: c in X /\ Y by XBOOLE_0:def 4;
then
A7: c in X by XBOOLE_0:def 4;
A8: c in dom (f1(#)f2) by A5,XBOOLE_0:def 4;
then
A9: c in (dom f1 /\ dom f2) by Def3;
then c in dom f1 by XBOOLE_0:def 4;
then
A10: c in X /\ dom f1 by A7,XBOOLE_0:def 4;
A11: c in Y by A6,XBOOLE_0:def 4;
c in dom f2 by A9,XBOOLE_0:def 4;
then
A12: c in Y /\ dom f2 by A11,XBOOLE_0:def 4;
thus (f1(#)f2)/.c = f1.c * (f2/.c) by A8,Def3
.= r1 * (f2/.c) by A3,A10
.= r1 * r2 by A4,A12;
end;
hence thesis by PARTFUN2:35;
end;
theorem Th52:
f|Y is constant implies (p(#)f)|Y is constant
proof
assume f|Y is constant;
then consider r being VECTOR of V such that
A1: for c st c in Y /\ dom f holds f/.c = r by PARTFUN2:35;
now
let c;
assume
A2: c in Y /\ dom (p(#)f);
then
A3: c in Y by XBOOLE_0:def 4;
A4: c in dom (p(#)f) by A2,XBOOLE_0:def 4;
then c in dom f by Def4;
then
A5: c in Y /\ dom f by A3,XBOOLE_0:def 4;
thus (p(#)f)/.c = p * f/.c by A4,Def4
.= p*r by A1,A5;
end;
hence thesis by PARTFUN2:35;
end;
theorem Th53:
f|Y is constant implies ||.f.|||Y is constant & (-f)|Y is constant
proof
assume f|Y is constant;
then consider r being VECTOR of V such that
A1: for c st c in Y /\ dom f holds f/.c = r by PARTFUN2:35;
now
let c;
assume
A2: c in Y /\ dom (||.f.||);
then
A3: c in Y by XBOOLE_0:def 4;
A4: c in dom (||.f.||) by A2,XBOOLE_0:def 4;
then c in dom f by NORMSP_0:def 3;
then
A5: c in Y /\ dom f by A3,XBOOLE_0:def 4;
thus (||.f.||).c = ||.f/.c.|| by A4,NORMSP_0:def 3
.= ||.r.|| by A1,A5;
end;
hence ||.f.|||Y is constant by PARTFUN2:57;
now
take p=-r;
let c;
assume
A6: c in Y /\ dom (-f);
then c in Y /\ dom f by Def5;
then
A7: -f/.c = p by A1;
c in dom (-f) by A6,XBOOLE_0:def 4;
hence (-f)/.c = p by A7,Def5;
end;
hence thesis by PARTFUN2:35;
end;
theorem Th54:
f|Y is constant implies f is_bounded_on Y
proof
assume f|Y is constant;
then consider r being VECTOR of V such that
A1: for c st c in Y /\ dom f holds f/.c = r by PARTFUN2:35;
now
take p=||.r.||;
let c;
assume c in Y /\ dom f;
hence ||.f/.c.|| <= p by A1;
end;
hence thesis;
end;
theorem
f|Y is constant implies (for r holds r(#)f is_bounded_on Y) & -f
is_bounded_on Y & ||.f.|||Y is bounded
proof
assume
A1: f|Y is constant;
hereby
let r;
(r(#)f)|Y is constant by A1,Th52;
hence r(#)f is_bounded_on Y by Th54;
end;
(-f)|Y is constant by A1,Th53;
hence -f is_bounded_on Y by Th54;
||.f.|||Y is constant by A1,Th53;
hence thesis;
end;
theorem
f1 is_bounded_on X & f2|Y is constant implies f1+f2 is_bounded_on (X /\ Y)
proof
assume that
A1: f1 is_bounded_on X and
A2: f2|Y is constant;
f2 is_bounded_on Y by A2,Th54;
hence thesis by A1,Th46;
end;
theorem
f1 is_bounded_on X & f2|Y is constant implies f1-f2 is_bounded_on X /\
Y & f2-f1 is_bounded_on X /\ Y
proof
assume that
A1: f1 is_bounded_on X and
A2: f2|Y is constant;
A3: f2 is_bounded_on Y by A2,Th54;
then -f2 is_bounded_on Y by Th45;
then
A4: f1+-f2 is_bounded_on X /\ Y by A1,Th46;
-f1 is_bounded_on X by A1,Th45;
then f2+-f1 is_bounded_on Y /\ X by A3,Th46;
hence thesis by A4,Th25;
end;