:: RFUNCT_1 semantic presentation
begin
Lm1: (- 1) " = - 1
;
definition
let f1, f2 be complex-valued Function;
funcf1 / f2 -> Function means :Def1: :: RFUNCT_1:def 1
( dom it = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom it holds
it . c = (f1 . c) * ((f2 . c) ") ) );
existence
ex b1 being Function st
( dom b1 = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom b1 holds
b1 . c = (f1 . c) * ((f2 . c) ") ) )
proof
deffunc H1( set ) -> set = (f1 . $1) * ((f2 . $1) ");
ex f being Function st
( dom f = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for x being set st x in (dom f1) /\ ((dom f2) \ (f2 " {0})) holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
hence ex b1 being Function st
( dom b1 = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom b1 holds
b1 . c = (f1 . c) * ((f2 . c) ") ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function st dom b1 = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom b1 holds
b1 . c = (f1 . c) * ((f2 . c) ") ) & dom b2 = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom b2 holds
b2 . c = (f1 . c) * ((f2 . c) ") ) holds
b1 = b2
proof
let f, g be Function; ::_thesis: ( dom f = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom f holds
f . c = (f1 . c) * ((f2 . c) ") ) & dom g = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom g holds
g . c = (f1 . c) * ((f2 . c) ") ) implies f = g )
assume that
A1: dom f = (dom f1) /\ ((dom f2) \ (f2 " {0})) and
A2: for c being set st c in dom f holds
f . c = (f1 . c) * ((f2 . c) ") and
A3: dom g = (dom f1) /\ ((dom f2) \ (f2 " {0})) and
A4: for c being set st c in dom g holds
g . c = (f1 . c) * ((f2 . c) ") ; ::_thesis: f = g
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in dom f implies f . x = g . x )
assume A5: x in dom f ; ::_thesis: f . x = g . x
hence f . x = (f1 . x) * ((f2 . x) ") by A2
.= g . x by A1, A3, A4, A5 ;
::_thesis: verum
end;
hence f = g by A1, A3, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines / RFUNCT_1:def_1_:_
for f1, f2 being complex-valued Function
for b3 being Function holds
( b3 = f1 / f2 iff ( dom b3 = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom b3 holds
b3 . c = (f1 . c) * ((f2 . c) ") ) ) );
registration
let f1, f2 be complex-valued Function;
clusterf1 / f2 -> complex-valued ;
coherence
f1 / f2 is complex-valued
proof
let x be set ; :: according to VALUED_0:def_7 ::_thesis: ( not x in dom (f1 / f2) or (f1 / f2) . x is complex )
set F = f1 / f2;
assume x in dom (f1 / f2) ; ::_thesis: (f1 / f2) . x is complex
then (f1 / f2) . x = (f1 . x) * ((f2 . x) ") by Def1;
hence (f1 / f2) . x is complex ; ::_thesis: verum
end;
end;
registration
let f1, f2 be real-valued Function;
clusterf1 / f2 -> real-valued ;
coherence
f1 / f2 is real-valued
proof
let x be set ; :: according to VALUED_0:def_9 ::_thesis: ( not x in dom (f1 / f2) or (f1 / f2) . x is real )
set F = f1 / f2;
assume x in dom (f1 / f2) ; ::_thesis: (f1 / f2) . x is real
then (f1 / f2) . x = (f1 . x) * ((f2 . x) ") by Def1;
hence (f1 / f2) . x is real ; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be complex-membered set ;
let f1, f2 be PartFunc of C,D;
:: original: /
redefine funcf1 / f2 -> PartFunc of C,COMPLEX;
coherence
f1 / f2 is PartFunc of C,COMPLEX
proof
set F = f1 / f2;
A1: rng (f1 / f2) c= COMPLEX by VALUED_0:def_1;
dom (f1 / f2) = (dom f1) /\ ((dom f2) \ (f2 " {0})) by Def1;
hence f1 / f2 is PartFunc of C,COMPLEX by A1, RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be real-membered set ;
let f1, f2 be PartFunc of C,D;
:: original: /
redefine funcf1 / f2 -> PartFunc of C,REAL;
coherence
f1 / f2 is PartFunc of C,REAL
proof
set F = f1 / f2;
rng (f1 / f2) c= REAL by VALUED_0:def_3;
then f1 / f2 is PartFunc of (dom (f1 / f2)),REAL by RELSET_1:4;
hence f1 / f2 is PartFunc of C,REAL by RELSET_1:5; ::_thesis: verum
end;
end;
definition
let f be complex-valued Function;
funcf ^ -> Function means :Def2: :: RFUNCT_1:def 2
( dom it = (dom f) \ (f " {0}) & ( for c being set st c in dom it holds
it . c = (f . c) " ) );
existence
ex b1 being Function st
( dom b1 = (dom f) \ (f " {0}) & ( for c being set st c in dom b1 holds
b1 . c = (f . c) " ) )
proof
deffunc H1( set ) -> set = (f . $1) " ;
ex h being Function st
( dom h = (dom f) \ (f " {0}) & ( for x being set st x in (dom f) \ (f " {0}) holds
h . x = H1(x) ) ) from FUNCT_1:sch_3();
hence ex b1 being Function st
( dom b1 = (dom f) \ (f " {0}) & ( for c being set st c in dom b1 holds
b1 . c = (f . c) " ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function st dom b1 = (dom f) \ (f " {0}) & ( for c being set st c in dom b1 holds
b1 . c = (f . c) " ) & dom b2 = (dom f) \ (f " {0}) & ( for c being set st c in dom b2 holds
b2 . c = (f . c) " ) holds
b1 = b2
proof
let h, g be Function; ::_thesis: ( dom h = (dom f) \ (f " {0}) & ( for c being set st c in dom h holds
h . c = (f . c) " ) & dom g = (dom f) \ (f " {0}) & ( for c being set st c in dom g holds
g . c = (f . c) " ) implies h = g )
assume that
A1: dom h = (dom f) \ (f " {0}) and
A2: for c being set st c in dom h holds
h . c = (f . c) " and
A3: dom g = (dom f) \ (f " {0}) and
A4: for c being set st c in dom g holds
g . c = (f . c) " ; ::_thesis: h = g
now__::_thesis:_for_x_being_set_st_x_in_dom_h_holds_
h_._x_=_g_._x
let x be set ; ::_thesis: ( x in dom h implies h . x = g . x )
assume A5: x in dom h ; ::_thesis: h . x = g . x
hence h . x = (f . x) " by A2
.= g . x by A1, A3, A4, A5 ;
::_thesis: verum
end;
hence h = g by A1, A3, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines ^ RFUNCT_1:def_2_:_
for f being complex-valued Function
for b2 being Function holds
( b2 = f ^ iff ( dom b2 = (dom f) \ (f " {0}) & ( for c being set st c in dom b2 holds
b2 . c = (f . c) " ) ) );
registration
let f be complex-valued Function;
clusterf ^ -> complex-valued ;
coherence
f ^ is complex-valued
proof
let x be set ; :: according to VALUED_0:def_7 ::_thesis: ( not x in dom (f ^) or (f ^) . x is complex )
set F = f ^ ;
assume x in dom (f ^) ; ::_thesis: (f ^) . x is complex
then (f ^) . x = (f . x) " by Def2;
hence (f ^) . x is complex ; ::_thesis: verum
end;
end;
registration
let f be real-valued Function;
clusterf ^ -> real-valued ;
coherence
f ^ is real-valued
proof
let x be set ; :: according to VALUED_0:def_9 ::_thesis: ( not x in dom (f ^) or (f ^) . x is real )
set F = f ^ ;
assume x in dom (f ^) ; ::_thesis: (f ^) . x is real
then (f ^) . x = (f . x) " by Def2;
hence (f ^) . x is real ; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be complex-membered set ;
let f be PartFunc of C,D;
:: original: ^
redefine funcf ^ -> PartFunc of C,COMPLEX;
coherence
f ^ is PartFunc of C,COMPLEX
proof
set F = f ^ ;
A1: rng (f ^) c= COMPLEX by VALUED_0:def_1;
dom (f ^) = (dom f) \ (f " {0}) by Def2;
hence f ^ is PartFunc of C,COMPLEX by A1, RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be real-membered set ;
let f be PartFunc of C,D;
:: original: ^
redefine funcf ^ -> PartFunc of C,REAL;
coherence
f ^ is PartFunc of C,REAL
proof
set F = f ^ ;
rng (f ^) c= REAL by VALUED_0:def_3;
then f ^ is PartFunc of (dom (f ^)),REAL by RELSET_1:4;
hence f ^ is PartFunc of C,REAL by RELSET_1:5; ::_thesis: verum
end;
end;
theorem Th1: :: RFUNCT_1:1
for g being complex-valued Function holds
( dom (g ^) c= dom g & (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0}) )
proof
let g be complex-valued Function; ::_thesis: ( dom (g ^) c= dom g & (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0}) )
dom (g ^) = (dom g) \ (g " {0}) by Def2;
hence dom (g ^) c= dom g ; ::_thesis: (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0})
thus (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0}) by XBOOLE_1:28; ::_thesis: verum
end;
theorem Th2: :: RFUNCT_1:2
for f1, f2 being complex-valued Function holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0}))
proof
let f1, f2 be complex-valued Function; ::_thesis: (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0}))
thus (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) c= ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) :: according to XBOOLE_0:def_10 ::_thesis: ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) c= (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0})
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) or x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) )
assume A1: x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) ; ::_thesis: x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0}))
then not x in (f1 (#) f2) " {0} by XBOOLE_0:def_5;
then not (f1 (#) f2) . x in {0} by A1, FUNCT_1:def_7;
then (f1 (#) f2) . x <> 0 by TARSKI:def_1;
then A2: (f1 . x) * (f2 . x) <> 0 by VALUED_1:5;
then f2 . x <> 0 ;
then not f2 . x in {0} by TARSKI:def_1;
then A3: not x in f2 " {0} by FUNCT_1:def_7;
x in dom (f1 (#) f2) by A1;
then A4: x in (dom f1) /\ (dom f2) by VALUED_1:def_4;
then x in dom f2 by XBOOLE_0:def_4;
then A5: x in (dom f2) \ (f2 " {0}) by A3, XBOOLE_0:def_5;
f1 . x <> 0 by A2;
then not f1 . x in {0} by TARSKI:def_1;
then A6: not x in f1 " {0} by FUNCT_1:def_7;
x in dom f1 by A4, XBOOLE_0:def_4;
then x in (dom f1) \ (f1 " {0}) by A6, XBOOLE_0:def_5;
hence x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) by A5, XBOOLE_0:def_4; ::_thesis: verum
end;
thus ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) c= (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) or x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) )
assume A7: x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) ; ::_thesis: x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0})
then x in (dom f2) \ (f2 " {0}) by XBOOLE_0:def_4;
then not x in f2 " {0} by XBOOLE_0:def_5;
then not f2 . x in {0} by A7, FUNCT_1:def_7;
then A8: f2 . x <> 0 by TARSKI:def_1;
A9: x in (dom f1) \ (f1 " {0}) by A7, XBOOLE_0:def_4;
then not x in f1 " {0} by XBOOLE_0:def_5;
then not f1 . x in {0} by A9, FUNCT_1:def_7;
then f1 . x <> 0 by TARSKI:def_1;
then (f1 . x) * (f2 . x) <> 0 by A8;
then (f1 (#) f2) . x <> 0 by VALUED_1:5;
then not (f1 (#) f2) . x in {0} by TARSKI:def_1;
then A10: not x in (f1 (#) f2) " {0} by FUNCT_1:def_7;
x in (dom f1) /\ (dom f2) by A7, A9, XBOOLE_0:def_4;
then x in dom (f1 (#) f2) by VALUED_1:def_4;
hence x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) by A10, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
theorem Th3: :: RFUNCT_1:3
for C being non empty set
for c being Element of C
for f being complex-valued Function st c in dom (f ^) holds
f . c <> 0
proof
let C be non empty set ; ::_thesis: for c being Element of C
for f being complex-valued Function st c in dom (f ^) holds
f . c <> 0
let c be Element of C; ::_thesis: for f being complex-valued Function st c in dom (f ^) holds
f . c <> 0
let f be complex-valued Function; ::_thesis: ( c in dom (f ^) implies f . c <> 0 )
assume that
A1: c in dom (f ^) and
A2: f . c = 0 ; ::_thesis: contradiction
A3: c in (dom f) \ (f " {0}) by A1, Def2;
then A4: not c in f " {0} by XBOOLE_0:def_5;
now__::_thesis:_contradiction
percases ( not c in dom f or not f . c in {0} ) by A4, FUNCT_1:def_7;
suppose not c in dom f ; ::_thesis: contradiction
hence contradiction by A3; ::_thesis: verum
end;
suppose not f . c in {0} ; ::_thesis: contradiction
hence contradiction by A2, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
theorem Th4: :: RFUNCT_1:4
for f being complex-valued Function holds (f ^) " {0} = {}
proof
let f be complex-valued Function; ::_thesis: (f ^) " {0} = {}
set x = the Element of (f ^) " {0};
assume A1: (f ^) " {0} <> {} ; ::_thesis: contradiction
then A2: the Element of (f ^) " {0} in dom (f ^) by FUNCT_1:def_7;
then A3: the Element of (f ^) " {0} in (dom f) \ (f " {0}) by Def2;
then not the Element of (f ^) " {0} in f " {0} by XBOOLE_0:def_5;
then A4: not f . the Element of (f ^) " {0} in {0} by A3, FUNCT_1:def_7;
(f ^) . the Element of (f ^) " {0} in {0} by A1, FUNCT_1:def_7;
then (f ^) . the Element of (f ^) " {0} = 0 by TARSKI:def_1;
then (f . the Element of (f ^) " {0}) " = 0 by A2, Def2;
hence contradiction by A4, TARSKI:def_1, XCMPLX_1:202; ::_thesis: verum
end;
theorem Th5: :: RFUNCT_1:5
for f being complex-valued Function holds
( (abs f) " {0} = f " {0} & (- f) " {0} = f " {0} )
proof
let f be complex-valued Function; ::_thesis: ( (abs f) " {0} = f " {0} & (- f) " {0} = f " {0} )
now__::_thesis:_for_c_being_set_holds_
(_(_c_in_(abs_f)_"_{0}_implies_c_in_f_"_{0}_)_&_(_c_in_f_"_{0}_implies_c_in_(abs_f)_"_{0}_)_)
let c be set ; ::_thesis: ( ( c in (abs f) " {0} implies c in f " {0} ) & ( c in f " {0} implies c in (abs f) " {0} ) )
thus ( c in (abs f) " {0} implies c in f " {0} ) ::_thesis: ( c in f " {0} implies c in (abs f) " {0} )
proof
assume A1: c in (abs f) " {0} ; ::_thesis: c in f " {0}
then (abs f) . c in {0} by FUNCT_1:def_7;
then (abs f) . c = 0 by TARSKI:def_1;
then abs (f . c) = 0 by VALUED_1:18;
then f . c = 0 by COMPLEX1:45;
then A2: f . c in {0} by TARSKI:def_1;
c in dom (abs f) by A1, FUNCT_1:def_7;
then c in dom f by VALUED_1:def_11;
hence c in f " {0} by A2, FUNCT_1:def_7; ::_thesis: verum
end;
assume A3: c in f " {0} ; ::_thesis: c in (abs f) " {0}
then f . c in {0} by FUNCT_1:def_7;
then f . c = 0 by TARSKI:def_1;
then abs (f . c) = 0 by ABSVALUE:2;
then (abs f) . c = 0 by VALUED_1:18;
then A4: (abs f) . c in {0} by TARSKI:def_1;
c in dom f by A3, FUNCT_1:def_7;
then c in dom (abs f) by VALUED_1:def_11;
hence c in (abs f) " {0} by A4, FUNCT_1:def_7; ::_thesis: verum
end;
hence (abs f) " {0} = f " {0} by TARSKI:1; ::_thesis: (- f) " {0} = f " {0}
now__::_thesis:_for_c_being_set_holds_
(_(_c_in_(-_f)_"_{0}_implies_c_in_f_"_{0}_)_&_(_c_in_f_"_{0}_implies_c_in_(-_f)_"_{0}_)_)
let c be set ; ::_thesis: ( ( c in (- f) " {0} implies c in f " {0} ) & ( c in f " {0} implies c in (- f) " {0} ) )
thus ( c in (- f) " {0} implies c in f " {0} ) ::_thesis: ( c in f " {0} implies c in (- f) " {0} )
proof
assume A5: c in (- f) " {0} ; ::_thesis: c in f " {0}
then (- f) . c in {0} by FUNCT_1:def_7;
then (- f) . c = 0 by TARSKI:def_1;
then - (- (f . c)) = - 0 by VALUED_1:8;
then A6: f . c in {0} by TARSKI:def_1;
c in dom (- f) by A5, FUNCT_1:def_7;
then c in dom f by VALUED_1:8;
hence c in f " {0} by A6, FUNCT_1:def_7; ::_thesis: verum
end;
assume A7: c in f " {0} ; ::_thesis: c in (- f) " {0}
then f . c in {0} by FUNCT_1:def_7;
then f . c = 0 by TARSKI:def_1;
then (- f) . c = - 0 by VALUED_1:8;
then A8: (- f) . c in {0} by TARSKI:def_1;
c in dom f by A7, FUNCT_1:def_7;
then c in dom (- f) by VALUED_1:8;
hence c in (- f) " {0} by A8, FUNCT_1:def_7; ::_thesis: verum
end;
hence (- f) " {0} = f " {0} by TARSKI:1; ::_thesis: verum
end;
theorem Th6: :: RFUNCT_1:6
for f being complex-valued Function holds dom ((f ^) ^) = dom (f | (dom (f ^)))
proof
let f be complex-valued Function; ::_thesis: dom ((f ^) ^) = dom (f | (dom (f ^)))
A1: dom (f ^) = (dom f) \ (f " {0}) by Def2;
thus dom ((f ^) ^) = (dom (f ^)) \ ((f ^) " {0}) by Def2
.= (dom (f ^)) \ {} by Th4
.= (dom f) /\ (dom (f ^)) by A1, XBOOLE_1:28
.= dom (f | (dom (f ^))) by RELAT_1:61 ; ::_thesis: verum
end;
theorem Th7: :: RFUNCT_1:7
for f being complex-valued Function
for r being complex number st r <> 0 holds
(r (#) f) " {0} = f " {0}
proof
let f be complex-valued Function; ::_thesis: for r being complex number st r <> 0 holds
(r (#) f) " {0} = f " {0}
let r be complex number ; ::_thesis: ( r <> 0 implies (r (#) f) " {0} = f " {0} )
assume A1: r <> 0 ; ::_thesis: (r (#) f) " {0} = f " {0}
now__::_thesis:_for_c_being_set_holds_
(_(_c_in_(r_(#)_f)_"_{0}_implies_c_in_f_"_{0}_)_&_(_c_in_f_"_{0}_implies_c_in_(r_(#)_f)_"_{0}_)_)
let c be set ; ::_thesis: ( ( c in (r (#) f) " {0} implies c in f " {0} ) & ( c in f " {0} implies c in (r (#) f) " {0} ) )
thus ( c in (r (#) f) " {0} implies c in f " {0} ) ::_thesis: ( c in f " {0} implies c in (r (#) f) " {0} )
proof
assume A2: c in (r (#) f) " {0} ; ::_thesis: c in f " {0}
then A3: c in dom (r (#) f) by FUNCT_1:def_7;
(r (#) f) . c in {0} by A2, FUNCT_1:def_7;
then (r (#) f) . c = 0 by TARSKI:def_1;
then r * (f . c) = 0 by A3, VALUED_1:def_5;
then f . c = 0 by A1;
then A4: f . c in {0} by TARSKI:def_1;
c in dom f by A3, VALUED_1:def_5;
hence c in f " {0} by A4, FUNCT_1:def_7; ::_thesis: verum
end;
assume A5: c in f " {0} ; ::_thesis: c in (r (#) f) " {0}
then f . c in {0} by FUNCT_1:def_7;
then f . c = 0 by TARSKI:def_1;
then A6: r * (f . c) = 0 ;
A7: c in dom f by A5, FUNCT_1:def_7;
then c in dom (r (#) f) by VALUED_1:def_5;
then (r (#) f) . c = 0 by A6, VALUED_1:def_5;
then A8: (r (#) f) . c in {0} by TARSKI:def_1;
c in dom (r (#) f) by A7, VALUED_1:def_5;
hence c in (r (#) f) " {0} by A8, FUNCT_1:def_7; ::_thesis: verum
end;
hence (r (#) f) " {0} = f " {0} by TARSKI:1; ::_thesis: verum
end;
theorem :: RFUNCT_1:8
for f1, f2, f3 being complex-valued Function holds (f1 + f2) + f3 = f1 + (f2 + f3)
proof
let f1, f2, f3 be complex-valued Function; ::_thesis: (f1 + f2) + f3 = f1 + (f2 + f3)
A1: dom ((f1 + f2) + f3) = (dom (f1 + f2)) /\ (dom f3) by VALUED_1:def_1
.= ((dom f1) /\ (dom f2)) /\ (dom f3) by VALUED_1:def_1
.= (dom f1) /\ ((dom f2) /\ (dom f3)) by XBOOLE_1:16
.= (dom f1) /\ (dom (f2 + f3)) by VALUED_1:def_1
.= dom (f1 + (f2 + f3)) by VALUED_1:def_1 ;
now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_+_f2)_+_f3)_holds_
((f1_+_f2)_+_f3)_._c_=_(f1_+_(f2_+_f3))_._c
let c be set ; ::_thesis: ( c in dom ((f1 + f2) + f3) implies ((f1 + f2) + f3) . c = (f1 + (f2 + f3)) . c )
assume A2: c in dom ((f1 + f2) + f3) ; ::_thesis: ((f1 + f2) + f3) . c = (f1 + (f2 + f3)) . c
then c in (dom (f1 + f2)) /\ (dom f3) by VALUED_1:def_1;
then A3: c in dom (f1 + f2) by XBOOLE_0:def_4;
c in (dom f1) /\ (dom (f2 + f3)) by A1, A2, VALUED_1:def_1;
then A4: c in dom (f2 + f3) by XBOOLE_0:def_4;
thus ((f1 + f2) + f3) . c = ((f1 + f2) . c) + (f3 . c) by A2, VALUED_1:def_1
.= ((f1 . c) + (f2 . c)) + (f3 . c) by A3, VALUED_1:def_1
.= (f1 . c) + ((f2 . c) + (f3 . c))
.= (f1 . c) + ((f2 + f3) . c) by A4, VALUED_1:def_1
.= (f1 + (f2 + f3)) . c by A1, A2, VALUED_1:def_1 ; ::_thesis: verum
end;
hence (f1 + f2) + f3 = f1 + (f2 + f3) by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem Th9: :: RFUNCT_1:9
for f1, f2, f3 being complex-valued Function holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
proof
let f1, f2, f3 be complex-valued Function; ::_thesis: (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
A1: now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_(#)_f2)_(#)_f3)_holds_
((f1_(#)_f2)_(#)_f3)_._c_=_(f1_(#)_(f2_(#)_f3))_._c
let c be set ; ::_thesis: ( c in dom ((f1 (#) f2) (#) f3) implies ((f1 (#) f2) (#) f3) . c = (f1 (#) (f2 (#) f3)) . c )
assume c in dom ((f1 (#) f2) (#) f3) ; ::_thesis: ((f1 (#) f2) (#) f3) . c = (f1 (#) (f2 (#) f3)) . c
thus ((f1 (#) f2) (#) f3) . c = ((f1 (#) f2) . c) * (f3 . c) by VALUED_1:5
.= ((f1 . c) * (f2 . c)) * (f3 . c) by VALUED_1:5
.= (f1 . c) * ((f2 . c) * (f3 . c))
.= (f1 . c) * ((f2 (#) f3) . c) by VALUED_1:5
.= (f1 (#) (f2 (#) f3)) . c by VALUED_1:5 ; ::_thesis: verum
end;
dom ((f1 (#) f2) (#) f3) = (dom (f1 (#) f2)) /\ (dom f3) by VALUED_1:def_4
.= ((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 VALUED_1:def_4
.= dom (f1 (#) (f2 (#) f3)) by VALUED_1:def_4 ;
hence (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3) by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem Th10: :: RFUNCT_1:10
for f1, f2, f3 being complex-valued Function holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3)
proof
let f1, f2, f3 be complex-valued Function; ::_thesis: (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3)
A1: dom ((f1 + f2) (#) f3) = (dom (f1 + f2)) /\ (dom f3) by VALUED_1:def_4
.= ((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 VALUED_1:def_4
.= (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by VALUED_1:def_4
.= dom ((f1 (#) f3) + (f2 (#) f3)) by VALUED_1:def_1 ;
now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_+_f2)_(#)_f3)_holds_
((f1_+_f2)_(#)_f3)_._c_=_((f1_(#)_f3)_+_(f2_(#)_f3))_._c
let c be set ; ::_thesis: ( c in dom ((f1 + f2) (#) f3) implies ((f1 + f2) (#) f3) . c = ((f1 (#) f3) + (f2 (#) f3)) . c )
assume A2: c in dom ((f1 + f2) (#) f3) ; ::_thesis: ((f1 + f2) (#) f3) . c = ((f1 (#) f3) + (f2 (#) f3)) . c
then c in (dom (f1 + f2)) /\ (dom f3) by VALUED_1:def_4;
then A3: c in dom (f1 + f2) by XBOOLE_0:def_4;
thus ((f1 + f2) (#) f3) . c = ((f1 + f2) . c) * (f3 . c) by VALUED_1:5
.= ((f1 . c) + (f2 . c)) * (f3 . c) by A3, VALUED_1:def_1
.= ((f1 . c) * (f3 . c)) + ((f2 . c) * (f3 . c))
.= ((f1 (#) f3) . c) + ((f2 . c) * (f3 . c)) by VALUED_1:5
.= ((f1 (#) f3) . c) + ((f2 (#) f3) . c) by VALUED_1:5
.= ((f1 (#) f3) + (f2 (#) f3)) . c by A1, A2, VALUED_1:def_1 ; ::_thesis: verum
end;
hence (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3) by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem :: RFUNCT_1:11
for f3, f1, f2 being complex-valued Function holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2) by Th10;
theorem Th12: :: RFUNCT_1:12
for f1, f2 being complex-valued Function
for r being complex number holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2
proof
let f1, f2 be complex-valued Function; ::_thesis: for r being complex number holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2
let r be complex number ; ::_thesis: r (#) (f1 (#) f2) = (r (#) f1) (#) f2
A1: dom (r (#) (f1 (#) f2)) = dom (f1 (#) f2) by VALUED_1:def_5
.= (dom f1) /\ (dom f2) by VALUED_1:def_4
.= (dom (r (#) f1)) /\ (dom f2) by VALUED_1:def_5
.= dom ((r (#) f1) (#) f2) by VALUED_1:def_4 ;
now__::_thesis:_for_c_being_set_st_c_in_dom_(r_(#)_(f1_(#)_f2))_holds_
(r_(#)_(f1_(#)_f2))_._c_=_((r_(#)_f1)_(#)_f2)_._c
let c be set ; ::_thesis: ( c in dom (r (#) (f1 (#) f2)) implies (r (#) (f1 (#) f2)) . c = ((r (#) f1) (#) f2) . c )
assume A2: c in dom (r (#) (f1 (#) f2)) ; ::_thesis: (r (#) (f1 (#) f2)) . c = ((r (#) f1) (#) f2) . c
then c in (dom (r (#) f1)) /\ (dom f2) by A1, VALUED_1:def_4;
then A3: c in dom (r (#) f1) by XBOOLE_0:def_4;
thus (r (#) (f1 (#) f2)) . c = r * ((f1 (#) f2) . c) by A2, VALUED_1:def_5
.= r * ((f1 . c) * (f2 . c)) by VALUED_1:5
.= (r * (f1 . c)) * (f2 . c)
.= ((r (#) f1) . c) * (f2 . c) by A3, VALUED_1:def_5
.= ((r (#) f1) (#) f2) . c by VALUED_1:5 ; ::_thesis: verum
end;
hence r (#) (f1 (#) f2) = (r (#) f1) (#) f2 by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem Th13: :: RFUNCT_1:13
for f1, f2 being complex-valued Function
for r being complex number holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2)
proof
let f1, f2 be complex-valued Function; ::_thesis: for r being complex number holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2)
let r be complex number ; ::_thesis: r (#) (f1 (#) f2) = f1 (#) (r (#) f2)
A1: dom (r (#) (f1 (#) f2)) = dom (f1 (#) f2) by VALUED_1:def_5
.= (dom f1) /\ (dom f2) by VALUED_1:def_4
.= (dom f1) /\ (dom (r (#) f2)) by VALUED_1:def_5
.= dom (f1 (#) (r (#) f2)) by VALUED_1:def_4 ;
now__::_thesis:_for_c_being_set_st_c_in_dom_(r_(#)_(f1_(#)_f2))_holds_
(r_(#)_(f1_(#)_f2))_._c_=_(f1_(#)_(r_(#)_f2))_._c
let c be set ; ::_thesis: ( c in dom (r (#) (f1 (#) f2)) implies (r (#) (f1 (#) f2)) . c = (f1 (#) (r (#) f2)) . c )
assume A2: c in dom (r (#) (f1 (#) f2)) ; ::_thesis: (r (#) (f1 (#) f2)) . c = (f1 (#) (r (#) f2)) . c
then c in (dom f1) /\ (dom (r (#) f2)) by A1, VALUED_1:def_4;
then A3: c in dom (r (#) f2) by XBOOLE_0:def_4;
thus (r (#) (f1 (#) f2)) . c = r * ((f1 (#) f2) . c) by A2, VALUED_1:def_5
.= r * ((f1 . c) * (f2 . c)) by VALUED_1:5
.= (f1 . c) * (r * (f2 . c))
.= (f1 . c) * ((r (#) f2) . c) by A3, VALUED_1:def_5
.= (f1 (#) (r (#) f2)) . c by VALUED_1:5 ; ::_thesis: verum
end;
hence r (#) (f1 (#) f2) = f1 (#) (r (#) f2) by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem Th14: :: RFUNCT_1:14
for f1, f2, f3 being complex-valued Function holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)
proof
let f1, f2, f3 be complex-valued Function; ::_thesis: (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)
A1: dom ((f1 - f2) (#) f3) = (dom (f1 - f2)) /\ (dom f3) by VALUED_1:def_4
.= ((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 VALUED_1:def_4
.= (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by VALUED_1:def_4
.= dom ((f1 (#) f3) - (f2 (#) f3)) by VALUED_1:12 ;
now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_-_f2)_(#)_f3)_holds_
((f1_-_f2)_(#)_f3)_._c_=_((f1_(#)_f3)_-_(f2_(#)_f3))_._c
let c be set ; ::_thesis: ( c in dom ((f1 - f2) (#) f3) implies ((f1 - f2) (#) f3) . c = ((f1 (#) f3) - (f2 (#) f3)) . c )
assume A2: c in dom ((f1 - f2) (#) f3) ; ::_thesis: ((f1 - f2) (#) f3) . c = ((f1 (#) f3) - (f2 (#) f3)) . c
then c in (dom (f1 - f2)) /\ (dom f3) by VALUED_1:def_4;
then A3: c in dom (f1 - f2) by XBOOLE_0:def_4;
thus ((f1 - f2) (#) f3) . c = ((f1 - f2) . c) * (f3 . c) by VALUED_1:5
.= ((f1 . c) - (f2 . c)) * (f3 . c) by A3, VALUED_1:13
.= ((f1 . c) * (f3 . c)) - ((f2 . c) * (f3 . c))
.= ((f1 (#) f3) . c) - ((f2 . c) * (f3 . c)) by VALUED_1:5
.= ((f1 (#) f3) . c) - ((f2 (#) f3) . c) by VALUED_1:5
.= ((f1 (#) f3) - (f2 (#) f3)) . c by A1, A2, VALUED_1:13 ; ::_thesis: verum
end;
hence (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3) by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem :: RFUNCT_1:15
for f3, f1, f2 being complex-valued Function holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2) by Th14;
theorem :: RFUNCT_1:16
for f1, f2 being complex-valued Function
for r being complex number holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2)
proof
let f1, f2 be complex-valued Function; ::_thesis: for r being complex number holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2)
let r be complex number ; ::_thesis: r (#) (f1 + f2) = (r (#) f1) + (r (#) f2)
A1: dom (r (#) (f1 + f2)) = dom (f1 + f2) by VALUED_1:def_5
.= (dom f1) /\ (dom f2) by VALUED_1:def_1
.= (dom f1) /\ (dom (r (#) f2)) by VALUED_1:def_5
.= (dom (r (#) f1)) /\ (dom (r (#) f2)) by VALUED_1:def_5
.= dom ((r (#) f1) + (r (#) f2)) by VALUED_1:def_1 ;
now__::_thesis:_for_c_being_set_st_c_in_dom_(r_(#)_(f1_+_f2))_holds_
(r_(#)_(f1_+_f2))_._c_=_((r_(#)_f1)_+_(r_(#)_f2))_._c
let c be set ; ::_thesis: ( c in dom (r (#) (f1 + f2)) implies (r (#) (f1 + f2)) . c = ((r (#) f1) + (r (#) f2)) . c )
assume A2: c in dom (r (#) (f1 + f2)) ; ::_thesis: (r (#) (f1 + f2)) . c = ((r (#) f1) + (r (#) f2)) . c
then A3: c in dom (f1 + f2) by VALUED_1:def_5;
A4: c in (dom (r (#) f1)) /\ (dom (r (#) f2)) by A1, A2, VALUED_1:def_1;
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, VALUED_1:def_5
.= r * ((f1 . c) + (f2 . c)) by A3, VALUED_1:def_1
.= (r * (f1 . c)) + (r * (f2 . c))
.= ((r (#) f1) . c) + (r * (f2 . c)) by A5, VALUED_1:def_5
.= ((r (#) f1) . c) + ((r (#) f2) . c) by A6, VALUED_1:def_5
.= ((r (#) f1) + (r (#) f2)) . c by A1, A2, VALUED_1:def_1 ; ::_thesis: verum
end;
hence r (#) (f1 + f2) = (r (#) f1) + (r (#) f2) by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem :: RFUNCT_1:17
for f being complex-valued Function
for r, p being complex number holds (r * p) (#) f = r (#) (p (#) f)
proof
let f be complex-valued Function; ::_thesis: for r, p being complex number holds (r * p) (#) f = r (#) (p (#) f)
let r, p be complex number ; ::_thesis: (r * p) (#) f = r (#) (p (#) f)
A1: dom ((r * p) (#) f) = dom f by VALUED_1:def_5
.= dom (p (#) f) by VALUED_1:def_5
.= dom (r (#) (p (#) f)) by VALUED_1:def_5 ;
now__::_thesis:_for_c_being_set_st_c_in_dom_((r_*_p)_(#)_f)_holds_
((r_*_p)_(#)_f)_._c_=_(r_(#)_(p_(#)_f))_._c
let c be set ; ::_thesis: ( c in dom ((r * p) (#) f) implies ((r * p) (#) f) . c = (r (#) (p (#) f)) . c )
assume A2: c in dom ((r * p) (#) f) ; ::_thesis: ((r * p) (#) f) . c = (r (#) (p (#) f)) . c
then A3: c in dom (p (#) f) by A1, VALUED_1:def_5;
thus ((r * p) (#) f) . c = (r * p) * (f . c) by A2, VALUED_1:def_5
.= r * (p * (f . c))
.= r * ((p (#) f) . c) by A3, VALUED_1:def_5
.= (r (#) (p (#) f)) . c by A1, A2, VALUED_1:def_5 ; ::_thesis: verum
end;
hence (r * p) (#) f = r (#) (p (#) f) by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem :: RFUNCT_1:18
for f1, f2 being complex-valued Function
for r being complex number holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2)
proof
let f1, f2 be complex-valued Function; ::_thesis: for r being complex number holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2)
let r be complex number ; ::_thesis: r (#) (f1 - f2) = (r (#) f1) - (r (#) f2)
A1: dom (r (#) (f1 - f2)) = dom (f1 - f2) by VALUED_1:def_5
.= (dom f1) /\ (dom f2) by VALUED_1:12
.= (dom f1) /\ (dom (r (#) f2)) by VALUED_1:def_5
.= (dom (r (#) f1)) /\ (dom (r (#) f2)) by VALUED_1:def_5
.= dom ((r (#) f1) - (r (#) f2)) by VALUED_1:12 ;
now__::_thesis:_for_c_being_set_st_c_in_dom_(r_(#)_(f1_-_f2))_holds_
(r_(#)_(f1_-_f2))_._c_=_((r_(#)_f1)_-_(r_(#)_f2))_._c
let c be set ; ::_thesis: ( c in dom (r (#) (f1 - f2)) implies (r (#) (f1 - f2)) . c = ((r (#) f1) - (r (#) f2)) . c )
assume A2: c in dom (r (#) (f1 - f2)) ; ::_thesis: (r (#) (f1 - f2)) . c = ((r (#) f1) - (r (#) f2)) . c
then A3: c in dom (f1 - f2) by VALUED_1:def_5;
A4: c in (dom (r (#) f1)) /\ (dom (r (#) f2)) by A1, A2, VALUED_1:12;
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, VALUED_1:def_5
.= r * ((f1 . c) - (f2 . c)) by A3, VALUED_1:13
.= (r * (f1 . c)) - (r * (f2 . c))
.= ((r (#) f1) . c) - (r * (f2 . c)) by A5, VALUED_1:def_5
.= ((r (#) f1) . c) - ((r (#) f2) . c) by A6, VALUED_1:def_5
.= ((r (#) f1) - (r (#) f2)) . c by A1, A2, VALUED_1:13 ; ::_thesis: verum
end;
hence r (#) (f1 - f2) = (r (#) f1) - (r (#) f2) by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem :: RFUNCT_1:19
for f1, f2 being complex-valued Function holds f1 - f2 = (- 1) (#) (f2 - f1)
proof
let f1, f2 be complex-valued Function; ::_thesis: f1 - f2 = (- 1) (#) (f2 - f1)
A1: dom (f1 - f2) = (dom f2) /\ (dom f1) by VALUED_1:12
.= dom (f2 - f1) by VALUED_1:12
.= dom ((- 1) (#) (f2 - f1)) by VALUED_1:def_5 ;
now__::_thesis:_for_c_being_set_st_c_in_dom_(f1_-_f2)_holds_
(f1_-_f2)_._c_=_((-_1)_(#)_(f2_-_f1))_._c
A2: dom (f1 - f2) = (dom f2) /\ (dom f1) by VALUED_1:12
.= dom (f2 - f1) by VALUED_1:12 ;
let c be set ; ::_thesis: ( c in dom (f1 - f2) implies (f1 - f2) . c = ((- 1) (#) (f2 - f1)) . c )
assume A3: c in dom (f1 - f2) ; ::_thesis: (f1 - f2) . c = ((- 1) (#) (f2 - f1)) . c
thus (f1 - f2) . c = (f1 . c) - (f2 . c) by A3, VALUED_1:13
.= (- 1) * ((f2 . c) - (f1 . c))
.= (- 1) * ((f2 - f1) . c) by A3, A2, VALUED_1:13
.= ((- 1) (#) (f2 - f1)) . c by A1, A3, VALUED_1:def_5 ; ::_thesis: verum
end;
hence f1 - f2 = (- 1) (#) (f2 - f1) by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem :: RFUNCT_1:20
for f1, f2, f3 being complex-valued Function holds f1 - (f2 + f3) = (f1 - f2) - f3
proof
let f1, f2, f3 be complex-valued Function; ::_thesis: f1 - (f2 + f3) = (f1 - f2) - f3
A1: dom (f1 - (f2 + f3)) = (dom f1) /\ (dom (f2 + f3)) by VALUED_1:12
.= (dom f1) /\ ((dom f2) /\ (dom f3)) by VALUED_1:def_1
.= ((dom f1) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16
.= (dom (f1 - f2)) /\ (dom f3) by VALUED_1:12
.= dom ((f1 - f2) - f3) by VALUED_1:12 ;
now__::_thesis:_for_c_being_set_st_c_in_dom_(f1_-_(f2_+_f3))_holds_
(f1_-_(f2_+_f3))_._c_=_((f1_-_f2)_-_f3)_._c
let c be set ; ::_thesis: ( c in dom (f1 - (f2 + f3)) implies (f1 - (f2 + f3)) . c = ((f1 - f2) - f3) . c )
assume A2: c in dom (f1 - (f2 + f3)) ; ::_thesis: (f1 - (f2 + f3)) . c = ((f1 - f2) - f3) . c
then c in (dom f1) /\ (dom (f2 + f3)) by VALUED_1:12;
then A3: c in dom (f2 + f3) by XBOOLE_0:def_4;
c in (dom (f1 - f2)) /\ (dom f3) by A1, A2, VALUED_1:12;
then A4: c in dom (f1 - f2) by XBOOLE_0:def_4;
thus (f1 - (f2 + f3)) . c = (f1 . c) - ((f2 + f3) . c) by A2, VALUED_1:13
.= (f1 . c) - ((f2 . c) + (f3 . c)) by A3, VALUED_1:def_1
.= ((f1 . c) - (f2 . c)) - (f3 . c)
.= ((f1 - f2) . c) - (f3 . c) by A4, VALUED_1:13
.= ((f1 - f2) - f3) . c by A1, A2, VALUED_1:13 ; ::_thesis: verum
end;
hence f1 - (f2 + f3) = (f1 - f2) - f3 by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem :: RFUNCT_1:21
for f being complex-valued Function holds 1 (#) f = f
proof
let f be complex-valued Function; ::_thesis: 1 (#) f = f
A1: now__::_thesis:_for_c_being_set_st_c_in_dom_(1_(#)_f)_holds_
(1_(#)_f)_._c_=_f_._c
let c be set ; ::_thesis: ( c in dom (1 (#) f) implies (1 (#) f) . c = f . c )
assume c in dom (1 (#) f) ; ::_thesis: (1 (#) f) . c = f . c
hence (1 (#) f) . c = 1 * (f . c) by VALUED_1:def_5
.= f . c ;
::_thesis: verum
end;
dom (1 (#) f) = dom f by VALUED_1:def_5;
hence 1 (#) f = f by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem :: RFUNCT_1:22
for f1, f2, f3 being complex-valued Function holds f1 - (f2 - f3) = (f1 - f2) + f3
proof
let f1, f2, f3 be complex-valued Function; ::_thesis: f1 - (f2 - f3) = (f1 - f2) + f3
A1: dom (f1 - (f2 - f3)) = (dom f1) /\ (dom (f2 - f3)) by VALUED_1:12
.= (dom f1) /\ ((dom f2) /\ (dom f3)) by VALUED_1:12
.= ((dom f1) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16
.= (dom (f1 - f2)) /\ (dom f3) by VALUED_1:12
.= dom ((f1 - f2) + f3) by VALUED_1:def_1 ;
now__::_thesis:_for_c_being_set_st_c_in_dom_(f1_-_(f2_-_f3))_holds_
(f1_-_(f2_-_f3))_._c_=_((f1_-_f2)_+_f3)_._c
let c be set ; ::_thesis: ( c in dom (f1 - (f2 - f3)) implies (f1 - (f2 - f3)) . c = ((f1 - f2) + f3) . c )
assume A2: c in dom (f1 - (f2 - f3)) ; ::_thesis: (f1 - (f2 - f3)) . c = ((f1 - f2) + f3) . c
then c in (dom f1) /\ (dom (f2 - f3)) by VALUED_1:12;
then A3: c in dom (f2 - f3) by XBOOLE_0:def_4;
c in (dom (f1 - f2)) /\ (dom f3) by A1, A2, VALUED_1:def_1;
then A4: c in dom (f1 - f2) by XBOOLE_0:def_4;
thus (f1 - (f2 - f3)) . c = (f1 . c) - ((f2 - f3) . c) by A2, VALUED_1:13
.= (f1 . c) - ((f2 . c) - (f3 . c)) by A3, VALUED_1:13
.= ((f1 . c) - (f2 . c)) + (f3 . c)
.= ((f1 - f2) . c) + (f3 . c) by A4, VALUED_1:13
.= ((f1 - f2) + f3) . c by A1, A2, VALUED_1:def_1 ; ::_thesis: verum
end;
hence f1 - (f2 - f3) = (f1 - f2) + f3 by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem :: RFUNCT_1:23
for f1, f2, f3 being complex-valued Function holds f1 + (f2 - f3) = (f1 + f2) - f3
proof
let f1, f2, f3 be complex-valued Function; ::_thesis: f1 + (f2 - f3) = (f1 + f2) - f3
A1: dom (f1 + (f2 - f3)) = (dom f1) /\ (dom (f2 - f3)) by VALUED_1:def_1
.= (dom f1) /\ ((dom f2) /\ (dom f3)) by VALUED_1:12
.= ((dom f1) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16
.= (dom (f1 + f2)) /\ (dom f3) by VALUED_1:def_1
.= dom ((f1 + f2) - f3) by VALUED_1:12 ;
now__::_thesis:_for_c_being_set_st_c_in_dom_(f1_+_(f2_-_f3))_holds_
(f1_+_(f2_-_f3))_._c_=_((f1_+_f2)_-_f3)_._c
let c be set ; ::_thesis: ( c in dom (f1 + (f2 - f3)) implies (f1 + (f2 - f3)) . c = ((f1 + f2) - f3) . c )
assume A2: c in dom (f1 + (f2 - f3)) ; ::_thesis: (f1 + (f2 - f3)) . c = ((f1 + f2) - f3) . c
then c in (dom f1) /\ (dom (f2 - f3)) by VALUED_1:def_1;
then A3: c in dom (f2 - f3) by XBOOLE_0:def_4;
c in (dom (f1 + f2)) /\ (dom f3) by A1, A2, VALUED_1:12;
then A4: c in dom (f1 + f2) by XBOOLE_0:def_4;
thus (f1 + (f2 - f3)) . c = (f1 . c) + ((f2 - f3) . c) by A2, VALUED_1:def_1
.= (f1 . c) + ((f2 . c) - (f3 . c)) by A3, VALUED_1:13
.= ((f1 . c) + (f2 . c)) - (f3 . c)
.= ((f1 + f2) . c) - (f3 . c) by A4, VALUED_1:def_1
.= ((f1 + f2) - f3) . c by A1, A2, VALUED_1:13 ; ::_thesis: verum
end;
hence f1 + (f2 - f3) = (f1 + f2) - f3 by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem Th24: :: RFUNCT_1:24
for f1, f2 being complex-valued Function holds abs (f1 (#) f2) = (abs f1) (#) (abs f2)
proof
let f1, f2 be complex-valued Function; ::_thesis: abs (f1 (#) f2) = (abs f1) (#) (abs f2)
A1: now__::_thesis:_for_c_being_set_st_c_in_dom_(abs_(f1_(#)_f2))_holds_
(abs_(f1_(#)_f2))_._c_=_((abs_f1)_(#)_(abs_f2))_._c
let c be set ; ::_thesis: ( c in dom (abs (f1 (#) f2)) implies (abs (f1 (#) f2)) . c = ((abs f1) (#) (abs f2)) . c )
assume c in dom (abs (f1 (#) f2)) ; ::_thesis: (abs (f1 (#) f2)) . c = ((abs f1) (#) (abs f2)) . c
thus (abs (f1 (#) f2)) . c = abs ((f1 (#) f2) . c) by VALUED_1:18
.= abs ((f1 . c) * (f2 . c)) by VALUED_1:5
.= (abs (f1 . c)) * (abs (f2 . c)) by COMPLEX1:65
.= ((abs f1) . c) * (abs (f2 . c)) by VALUED_1:18
.= ((abs f1) . c) * ((abs f2) . c) by VALUED_1:18
.= ((abs f1) (#) (abs f2)) . c by VALUED_1:5 ; ::_thesis: verum
end;
dom (abs (f1 (#) f2)) = dom (f1 (#) f2) by VALUED_1:def_11
.= (dom f1) /\ (dom f2) by VALUED_1:def_4
.= (dom f1) /\ (dom (abs f2)) by VALUED_1:def_11
.= (dom (abs f1)) /\ (dom (abs f2)) by VALUED_1:def_11
.= dom ((abs f1) (#) (abs f2)) by VALUED_1:def_4 ;
hence abs (f1 (#) f2) = (abs f1) (#) (abs f2) by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem :: RFUNCT_1:25
for f being complex-valued Function
for r being complex number holds abs (r (#) f) = (abs r) (#) (abs f)
proof
let f be complex-valued Function; ::_thesis: for r being complex number holds abs (r (#) f) = (abs r) (#) (abs f)
let r be complex number ; ::_thesis: abs (r (#) f) = (abs r) (#) (abs f)
A1: dom (abs (r (#) f)) = dom (r (#) f) by VALUED_1:def_11
.= dom f by VALUED_1:def_5
.= dom (abs f) by VALUED_1:def_11
.= dom ((abs r) (#) (abs f)) by VALUED_1:def_5 ;
now__::_thesis:_for_c_being_set_st_c_in_dom_(abs_(r_(#)_f))_holds_
(abs_(r_(#)_f))_._c_=_((abs_r)_(#)_(abs_f))_._c
let c be set ; ::_thesis: ( c in dom (abs (r (#) f)) implies (abs (r (#) f)) . c = ((abs r) (#) (abs f)) . c )
assume A2: c in dom (abs (r (#) f)) ; ::_thesis: (abs (r (#) f)) . c = ((abs r) (#) (abs f)) . c
then A3: c in dom (r (#) f) by VALUED_1:def_11;
thus (abs (r (#) f)) . c = abs ((r (#) f) . c) by VALUED_1:18
.= abs (r * (f . c)) by A3, VALUED_1:def_5
.= (abs r) * (abs (f . c)) by COMPLEX1:65
.= (abs r) * ((abs f) . c) by VALUED_1:18
.= ((abs r) (#) (abs f)) . c by A1, A2, VALUED_1:def_5 ; ::_thesis: verum
end;
hence abs (r (#) f) = (abs r) (#) (abs f) by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem Th26: :: RFUNCT_1:26
for f being complex-valued Function holds (f ^) ^ = f | (dom (f ^))
proof
let f be complex-valued Function; ::_thesis: (f ^) ^ = f | (dom (f ^))
A1: dom ((f ^) ^) = dom (f | (dom (f ^))) by Th6;
now__::_thesis:_for_c_being_set_st_c_in_dom_((f_^)_^)_holds_
((f_^)_^)_._c_=_(f_|_(dom_(f_^)))_._c
let c be set ; ::_thesis: ( c in dom ((f ^) ^) implies ((f ^) ^) . c = (f | (dom (f ^))) . c )
assume A2: c in dom ((f ^) ^) ; ::_thesis: ((f ^) ^) . c = (f | (dom (f ^))) . c
then c in (dom f) /\ (dom (f ^)) by A1, RELAT_1:61;
then A3: c in dom (f ^) by XBOOLE_0:def_4;
thus ((f ^) ^) . c = ((f ^) . c) " by A2, Def2
.= ((f . c) ") " by A3, Def2
.= (f | (dom (f ^))) . c by A1, A2, FUNCT_1:47 ; ::_thesis: verum
end;
hence (f ^) ^ = f | (dom (f ^)) by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem Th27: :: RFUNCT_1:27
for f1, f2 being complex-valued Function holds (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^)
proof
let f1, f2 be complex-valued Function; ::_thesis: (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^)
A1: dom ((f1 (#) f2) ^) = (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) by Def2
.= ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) by Th2
.= (dom (f1 ^)) /\ ((dom f2) \ (f2 " {0})) by Def2
.= (dom (f1 ^)) /\ (dom (f2 ^)) by Def2
.= dom ((f1 ^) (#) (f2 ^)) by VALUED_1:def_4 ;
now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_(#)_f2)_^)_holds_
((f1_(#)_f2)_^)_._c_=_((f1_^)_(#)_(f2_^))_._c
let c be set ; ::_thesis: ( c in dom ((f1 (#) f2) ^) implies ((f1 (#) f2) ^) . c = ((f1 ^) (#) (f2 ^)) . c )
assume A2: c in dom ((f1 (#) f2) ^) ; ::_thesis: ((f1 (#) f2) ^) . c = ((f1 ^) (#) (f2 ^)) . c
then A3: c in (dom (f1 ^)) /\ (dom (f2 ^)) by A1, VALUED_1:def_4;
then A4: c in dom (f1 ^) by XBOOLE_0:def_4;
A5: c in dom (f2 ^) by A3, XBOOLE_0:def_4;
thus ((f1 (#) f2) ^) . c = ((f1 (#) f2) . c) " by A2, Def2
.= ((f1 . c) * (f2 . c)) " by VALUED_1:5
.= ((f1 . c) ") * ((f2 . c) ") by XCMPLX_1:204
.= ((f1 ^) . c) * ((f2 . c) ") by A4, Def2
.= ((f1 ^) . c) * ((f2 ^) . c) by A5, Def2
.= ((f1 ^) (#) (f2 ^)) . c by VALUED_1:5 ; ::_thesis: verum
end;
hence (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^) by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem Th28: :: RFUNCT_1:28
for f being complex-valued Function
for r being complex number st r <> 0 holds
(r (#) f) ^ = (r ") (#) (f ^)
proof
let f be complex-valued Function; ::_thesis: for r being complex number st r <> 0 holds
(r (#) f) ^ = (r ") (#) (f ^)
let r be complex number ; ::_thesis: ( r <> 0 implies (r (#) f) ^ = (r ") (#) (f ^) )
assume A1: r <> 0 ; ::_thesis: (r (#) f) ^ = (r ") (#) (f ^)
A2: dom ((r (#) f) ^) = (dom (r (#) f)) \ ((r (#) f) " {0}) by Def2
.= (dom (r (#) f)) \ (f " {0}) by A1, Th7
.= (dom f) \ (f " {0}) by VALUED_1:def_5
.= dom (f ^) by Def2
.= dom ((r ") (#) (f ^)) by VALUED_1:def_5 ;
now__::_thesis:_for_c_being_set_st_c_in_dom_((r_(#)_f)_^)_holds_
((r_(#)_f)_^)_._c_=_((r_")_(#)_(f_^))_._c
let c be set ; ::_thesis: ( c in dom ((r (#) f) ^) implies ((r (#) f) ^) . c = ((r ") (#) (f ^)) . c )
assume A3: c in dom ((r (#) f) ^) ; ::_thesis: ((r (#) f) ^) . c = ((r ") (#) (f ^)) . c
then A4: c in (dom (r (#) f)) \ ((r (#) f) " {0}) by Def2;
A5: c in dom (f ^) by A2, A3, VALUED_1:def_5;
thus ((r (#) f) ^) . c = ((r (#) f) . c) " by A3, Def2
.= (r * (f . c)) " by A4, VALUED_1:def_5
.= (r ") * ((f . c) ") by XCMPLX_1:204
.= (r ") * ((f ^) . c) by A5, Def2
.= ((r ") (#) (f ^)) . c by A2, A3, VALUED_1:def_5 ; ::_thesis: verum
end;
hence (r (#) f) ^ = (r ") (#) (f ^) by A2, FUNCT_1:2; ::_thesis: verum
end;
theorem :: RFUNCT_1:29
for f being complex-valued Function holds (- f) ^ = (- 1) (#) (f ^) by Lm1, Th28;
theorem Th30: :: RFUNCT_1:30
for f being complex-valued Function holds (abs f) ^ = abs (f ^)
proof
let f be complex-valued Function; ::_thesis: (abs f) ^ = abs (f ^)
A1: dom ((abs f) ^) = (dom (abs f)) \ ((abs f) " {0}) by Def2
.= (dom f) \ ((abs f) " {0}) by VALUED_1:def_11
.= (dom f) \ (f " {0}) by Th5
.= dom (f ^) by Def2
.= dom (abs (f ^)) by VALUED_1:def_11 ;
now__::_thesis:_for_c_being_set_st_c_in_dom_((abs_f)_^)_holds_
((abs_f)_^)_._c_=_(abs_(f_^))_._c
let c be set ; ::_thesis: ( c in dom ((abs f) ^) implies ((abs f) ^) . c = (abs (f ^)) . c )
assume A2: c in dom ((abs f) ^) ; ::_thesis: ((abs f) ^) . c = (abs (f ^)) . c
then A3: c in dom (f ^) by A1, VALUED_1:def_11;
thus ((abs f) ^) . c = ((abs f) . c) " by A2, Def2
.= (abs (f . c)) " by VALUED_1:18
.= 1 / (abs (f . c)) by XCMPLX_1:215
.= abs (1 / (f . c)) by COMPLEX1:80
.= abs ((f . c) ") by XCMPLX_1:215
.= abs ((f ^) . c) by A3, Def2
.= (abs (f ^)) . c by VALUED_1:18 ; ::_thesis: verum
end;
hence (abs f) ^ = abs (f ^) by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem Th31: :: RFUNCT_1:31
for f, g being complex-valued Function holds f / g = f (#) (g ^)
proof
let f, g be complex-valued Function; ::_thesis: f / g = f (#) (g ^)
A1: now__::_thesis:_for_c_being_set_st_c_in_dom_(f_/_g)_holds_
(f_/_g)_._c_=_(f_(#)_(g_^))_._c
let c be set ; ::_thesis: ( c in dom (f / g) implies (f / g) . c = (f (#) (g ^)) . c )
assume A2: c in dom (f / g) ; ::_thesis: (f / g) . c = (f (#) (g ^)) . c
then c in (dom f) /\ ((dom g) \ (g " {0})) by Def1;
then c in (dom f) /\ (dom (g ^)) by Def2;
then A3: c in dom (g ^) by XBOOLE_0:def_4;
thus (f / g) . c = (f . c) * ((g . c) ") by A2, Def1
.= (f . c) * ((g ^) . c) by A3, Def2
.= (f (#) (g ^)) . c by VALUED_1:5 ; ::_thesis: verum
end;
dom (f / g) = (dom f) /\ ((dom g) \ (g " {0})) by Def1
.= (dom f) /\ (dom (g ^)) by Def2
.= dom (f (#) (g ^)) by VALUED_1:def_4 ;
hence f / g = f (#) (g ^) by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem Th32: :: RFUNCT_1:32
for g, f being complex-valued Function
for r being complex number holds r (#) (g / f) = (r (#) g) / f
proof
let g, f be complex-valued Function; ::_thesis: for r being complex number holds r (#) (g / f) = (r (#) g) / f
let r be complex number ; ::_thesis: r (#) (g / f) = (r (#) g) / f
thus r (#) (g / f) = r (#) (g (#) (f ^)) by Th31
.= (r (#) g) (#) (f ^) by Th12
.= (r (#) g) / f by Th31 ; ::_thesis: verum
end;
theorem :: RFUNCT_1:33
for f, g being complex-valued Function holds (f / g) (#) g = f | (dom (g ^))
proof
let f, g be complex-valued Function; ::_thesis: (f / g) (#) g = f | (dom (g ^))
A1: dom ((f / g) (#) g) = (dom (f / g)) /\ (dom g) by VALUED_1:def_4
.= ((dom f) /\ ((dom g) \ (g " {0}))) /\ (dom g) by Def1
.= (dom f) /\ (((dom g) \ (g " {0})) /\ (dom g)) by XBOOLE_1:16
.= (dom f) /\ ((dom (g ^)) /\ (dom g)) by Def2
.= (dom f) /\ (dom (g ^)) by Th1, XBOOLE_1:28
.= dom (f | (dom (g ^))) by RELAT_1:61 ;
now__::_thesis:_for_c_being_set_st_c_in_dom_((f_/_g)_(#)_g)_holds_
((f_/_g)_(#)_g)_._c_=_(f_|_(dom_(g_^)))_._c
let c be set ; ::_thesis: ( c in dom ((f / g) (#) g) implies ((f / g) (#) g) . c = (f | (dom (g ^))) . c )
assume A2: c in dom ((f / g) (#) g) ; ::_thesis: ((f / g) (#) g) . c = (f | (dom (g ^))) . c
then c in (dom f) /\ (dom (g ^)) by A1, RELAT_1:61;
then A3: c in dom (g ^) by XBOOLE_0:def_4;
then A4: g . c <> 0 by Th3;
thus ((f / g) (#) g) . c = ((f / g) . c) * (g . c) by VALUED_1:5
.= ((f (#) (g ^)) . c) * (g . c) by Th31
.= ((f . c) * ((g ^) . c)) * (g . c) by VALUED_1:5
.= ((f . c) * ((g . c) ")) * (g . c) by A3, Def2
.= (f . c) * (((g . c) ") * (g . c))
.= (f . c) * 1 by A4, XCMPLX_0:def_7
.= (f | (dom (g ^))) . c by A1, A2, FUNCT_1:47 ; ::_thesis: verum
end;
hence (f / g) (#) g = f | (dom (g ^)) by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem Th34: :: RFUNCT_1:34
for f, g, f1, g1 being complex-valued Function holds (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1)
proof
let f, g, f1, g1 be complex-valued Function; ::_thesis: (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1)
A1: now__::_thesis:_for_c_being_set_st_c_in_dom_((f_/_g)_(#)_(f1_/_g1))_holds_
((f_/_g)_(#)_(f1_/_g1))_._c_=_((f_(#)_f1)_/_(g_(#)_g1))_._c
let c be set ; ::_thesis: ( c in dom ((f / g) (#) (f1 / g1)) implies ((f / g) (#) (f1 / g1)) . c = ((f (#) f1) / (g (#) g1)) . c )
assume c in dom ((f / g) (#) (f1 / g1)) ; ::_thesis: ((f / g) (#) (f1 / g1)) . c = ((f (#) f1) / (g (#) g1)) . c
thus ((f / g) (#) (f1 / g1)) . c = ((f / g) . c) * ((f1 / g1) . c) by VALUED_1:5
.= ((f (#) (g ^)) . c) * ((f1 / g1) . c) by Th31
.= ((f (#) (g ^)) . c) * ((f1 (#) (g1 ^)) . c) by Th31
.= ((f . c) * ((g ^) . c)) * ((f1 (#) (g1 ^)) . c) by VALUED_1:5
.= ((f . c) * ((g ^) . c)) * ((f1 . c) * ((g1 ^) . c)) by VALUED_1:5
.= (f . c) * ((f1 . c) * (((g ^) . c) * ((g1 ^) . c)))
.= (f . c) * ((f1 . c) * (((g ^) (#) (g1 ^)) . c)) by VALUED_1:5
.= ((f . c) * (f1 . c)) * (((g ^) (#) (g1 ^)) . c)
.= ((f . c) * (f1 . c)) * (((g (#) g1) ^) . c) by Th27
.= ((f (#) f1) . c) * (((g (#) g1) ^) . c) by VALUED_1:5
.= ((f (#) f1) (#) ((g (#) g1) ^)) . c by VALUED_1:5
.= ((f (#) f1) / (g (#) g1)) . c by Th31 ; ::_thesis: verum
end;
dom ((f / g) (#) (f1 / g1)) = (dom (f / g)) /\ (dom (f1 / g1)) by VALUED_1:def_4
.= ((dom f) /\ ((dom g) \ (g " {0}))) /\ (dom (f1 / g1)) by Def1
.= ((dom f) /\ ((dom g) \ (g " {0}))) /\ ((dom f1) /\ ((dom g1) \ (g1 " {0}))) by Def1
.= (dom f) /\ (((dom g) \ (g " {0})) /\ ((dom f1) /\ ((dom g1) \ (g1 " {0})))) by XBOOLE_1:16
.= (dom f) /\ ((dom f1) /\ (((dom g) \ (g " {0})) /\ ((dom g1) \ (g1 " {0})))) by XBOOLE_1:16
.= ((dom f) /\ (dom f1)) /\ (((dom g) \ (g " {0})) /\ ((dom g1) \ (g1 " {0}))) by XBOOLE_1:16
.= (dom (f (#) f1)) /\ (((dom g) \ (g " {0})) /\ ((dom g1) \ (g1 " {0}))) by VALUED_1:def_4
.= (dom (f (#) f1)) /\ ((dom (g (#) g1)) \ ((g (#) g1) " {0})) by Th2
.= dom ((f (#) f1) / (g (#) g1)) by Def1 ;
hence (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1) by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem Th35: :: RFUNCT_1:35
for f1, f2 being complex-valued Function holds (f1 / f2) ^ = (f2 | (dom (f2 ^))) / f1
proof
let f1, f2 be complex-valued Function; ::_thesis: (f1 / f2) ^ = (f2 | (dom (f2 ^))) / f1
thus (f1 / f2) ^ = (f1 (#) (f2 ^)) ^ by Th31
.= (f1 ^) (#) ((f2 ^) ^) by Th27
.= (f2 | (dom (f2 ^))) (#) (f1 ^) by Th26
.= (f2 | (dom (f2 ^))) / f1 by Th31 ; ::_thesis: verum
end;
theorem Th36: :: RFUNCT_1:36
for g, f1, f2 being complex-valued Function holds g (#) (f1 / f2) = (g (#) f1) / f2
proof
let g, f1, f2 be complex-valued Function; ::_thesis: g (#) (f1 / f2) = (g (#) f1) / f2
thus g (#) (f1 / f2) = g (#) (f1 (#) (f2 ^)) by Th31
.= (g (#) f1) (#) (f2 ^) by Th9
.= (g (#) f1) / f2 by Th31 ; ::_thesis: verum
end;
theorem :: RFUNCT_1:37
for g, f1, f2 being complex-valued Function holds g / (f1 / f2) = (g (#) (f2 | (dom (f2 ^)))) / f1
proof
let g, f1, f2 be complex-valued Function; ::_thesis: g / (f1 / f2) = (g (#) (f2 | (dom (f2 ^)))) / f1
thus g / (f1 / f2) = g (#) ((f1 / f2) ^) by Th31
.= g (#) ((f2 | (dom (f2 ^))) / f1) by Th35
.= (g (#) (f2 | (dom (f2 ^)))) / f1 by Th36 ; ::_thesis: verum
end;
theorem :: RFUNCT_1:38
for f, g being complex-valued Function holds
( - (f / g) = (- f) / g & f / (- g) = - (f / g) )
proof
let f, g be complex-valued Function; ::_thesis: ( - (f / g) = (- f) / g & f / (- g) = - (f / g) )
thus - (f / g) = (- f) / g by Th32; ::_thesis: f / (- g) = - (f / g)
thus f / (- g) = f (#) ((- g) ^) by Th31
.= f (#) ((- 1) (#) (g ^)) by Lm1, Th28
.= - (f (#) (g ^)) by Th13
.= - (f / g) by Th31 ; ::_thesis: verum
end;
theorem :: RFUNCT_1:39
for f1, f, f2 being complex-valued Function holds
( (f1 / f) + (f2 / f) = (f1 + f2) / f & (f1 / f) - (f2 / f) = (f1 - f2) / f )
proof
let f1, f, f2 be complex-valued Function; ::_thesis: ( (f1 / f) + (f2 / f) = (f1 + f2) / f & (f1 / f) - (f2 / f) = (f1 - f2) / f )
thus (f1 / f) + (f2 / f) = (f1 (#) (f ^)) + (f2 / f) by Th31
.= (f1 (#) (f ^)) + (f2 (#) (f ^)) by Th31
.= (f1 + f2) (#) (f ^) by Th10
.= (f1 + f2) / f by Th31 ; ::_thesis: (f1 / f) - (f2 / f) = (f1 - f2) / f
thus (f1 / f) - (f2 / f) = (f1 (#) (f ^)) - (f2 / f) by Th31
.= (f1 (#) (f ^)) - (f2 (#) (f ^)) by Th31
.= (f1 - f2) (#) (f ^) by Th14
.= (f1 - f2) / f by Th31 ; ::_thesis: verum
end;
theorem Th40: :: RFUNCT_1:40
for f1, f, g1, g being complex-valued Function holds (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g)
proof
let f1, f, g1, g be complex-valued Function; ::_thesis: (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g)
A1: now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_/_f)_+_(g1_/_g))_holds_
((f1_/_f)_+_(g1_/_g))_._c_=_(((f1_(#)_g)_+_(g1_(#)_f))_/_(f_(#)_g))_._c
let c be set ; ::_thesis: ( c in dom ((f1 / f) + (g1 / g)) implies ((f1 / f) + (g1 / g)) . c = (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) . c )
A2: dom (g ^) c= dom g by Th1;
assume A3: c in dom ((f1 / f) + (g1 / g)) ; ::_thesis: ((f1 / f) + (g1 / g)) . c = (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) . c
then A4: c in (dom (f1 / f)) /\ (dom (g1 / g)) by VALUED_1:def_1;
then A5: c in dom (f1 / f) by XBOOLE_0:def_4;
A6: c in dom (g1 / g) by A4, XBOOLE_0:def_4;
A7: dom (f ^) c= dom f by Th1;
A8: c in (dom (f1 (#) (f ^))) /\ (dom (g1 / g)) by A4, Th31;
then c in dom (f1 (#) (f ^)) by XBOOLE_0:def_4;
then A9: c in (dom f1) /\ (dom (f ^)) by VALUED_1:def_4;
then A10: c in dom (f ^) by XBOOLE_0:def_4;
then A11: f . c <> 0 by Th3;
c in (dom (f1 (#) (f ^))) /\ (dom (g1 (#) (g ^))) by A8, Th31;
then c in dom (g1 (#) (g ^)) by XBOOLE_0:def_4;
then A12: c in (dom g1) /\ (dom (g ^)) by VALUED_1:def_4;
then A13: c in dom (g ^) by XBOOLE_0:def_4;
then A14: g . c <> 0 by Th3;
c in dom g1 by A12, XBOOLE_0:def_4;
then c in (dom g1) /\ (dom f) by A10, A7, XBOOLE_0:def_4;
then A15: c in dom (g1 (#) f) by VALUED_1:def_4;
c in dom f1 by A9, XBOOLE_0:def_4;
then c in (dom f1) /\ (dom g) by A13, A2, XBOOLE_0:def_4;
then c in dom (f1 (#) g) by VALUED_1:def_4;
then c in (dom (f1 (#) g)) /\ (dom (g1 (#) f)) by A15, XBOOLE_0:def_4;
then A16: c in dom ((f1 (#) g) + (g1 (#) f)) by VALUED_1:def_1;
c in (dom (f ^)) /\ (dom (g ^)) by A10, A13, XBOOLE_0:def_4;
then c in dom ((f ^) (#) (g ^)) by VALUED_1:def_4;
then c in dom ((f (#) g) ^) by Th27;
then c in (dom ((f1 (#) g) + (g1 (#) f))) /\ (dom ((f (#) g) ^)) by A16, XBOOLE_0:def_4;
then c in dom (((f1 (#) g) + (g1 (#) f)) (#) ((f (#) g) ^)) by VALUED_1:def_4;
then A17: c in dom (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) by Th31;
thus ((f1 / f) + (g1 / g)) . c = ((f1 / f) . c) + ((g1 / g) . c) by A3, VALUED_1:def_1
.= ((f1 . c) * ((f . c) ")) + ((g1 / g) . c) by A5, Def1
.= ((f1 . c) * (1 * ((f . c) "))) + (((g1 . c) * 1) * ((g . c) ")) by A6, Def1
.= ((f1 . c) * (((g . c) * ((g . c) ")) * ((f . c) "))) + ((g1 . c) * (1 * ((g . c) "))) by A14, XCMPLX_0:def_7
.= ((f1 . c) * ((g . c) * (((g . c) ") * ((f . c) ")))) + ((g1 . c) * (((f . c) * ((f . c) ")) * ((g . c) "))) by A11, XCMPLX_0:def_7
.= ((f1 . c) * ((g . c) * (((g . c) * (f . c)) "))) + ((g1 . c) * ((f . c) * (((f . c) ") * ((g . c) ")))) by XCMPLX_1:204
.= ((f1 . c) * ((g . c) * (((f . c) * (g . c)) "))) + ((g1 . c) * ((f . c) * (((f . c) * (g . c)) "))) by XCMPLX_1:204
.= ((f1 . c) * ((g . c) * (((f (#) g) . c) "))) + ((g1 . c) * ((f . c) * (((f . c) * (g . c)) "))) by VALUED_1:5
.= (((f1 . c) * (g . c)) * (((f (#) g) . c) ")) + ((g1 . c) * ((f . c) * (((f (#) g) . c) "))) by VALUED_1:5
.= (((f1 (#) g) . c) * (((f (#) g) . c) ")) + (((g1 . c) * (f . c)) * (((f (#) g) . c) ")) by VALUED_1:5
.= (((f1 (#) g) . c) * (((f (#) g) . c) ")) + (((g1 (#) f) . c) * (((f (#) g) . c) ")) by VALUED_1:5
.= (((f1 (#) g) . c) + ((g1 (#) f) . c)) * (((f (#) g) . c) ")
.= (((f1 (#) g) + (g1 (#) f)) . c) * (((f (#) g) . c) ") by A16, VALUED_1:def_1
.= (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) . c by A17, Def1 ; ::_thesis: verum
end;
dom ((f1 / f) + (g1 / g)) = (dom (f1 / f)) /\ (dom (g1 / g)) by VALUED_1:def_1
.= ((dom f1) /\ ((dom f) \ (f " {0}))) /\ (dom (g1 / g)) by Def1
.= ((dom f1) /\ ((dom f) \ (f " {0}))) /\ ((dom g1) /\ ((dom g) \ (g " {0}))) by Def1
.= ((dom f1) /\ ((dom f) /\ ((dom f) \ (f " {0})))) /\ ((dom g1) /\ ((dom g) \ (g " {0}))) by Th1
.= (((dom f) /\ ((dom f) \ (f " {0}))) /\ (dom f1)) /\ (((dom g) /\ ((dom g) \ (g " {0}))) /\ (dom g1)) by Th1
.= ((dom f) /\ ((dom f) \ (f " {0}))) /\ ((dom f1) /\ (((dom g) /\ ((dom g) \ (g " {0}))) /\ (dom g1))) by XBOOLE_1:16
.= ((dom f) /\ ((dom f) \ (f " {0}))) /\ (((dom f1) /\ ((dom g) /\ ((dom g) \ (g " {0})))) /\ (dom g1)) by XBOOLE_1:16
.= ((dom f) /\ ((dom f) \ (f " {0}))) /\ ((((dom f1) /\ (dom g)) /\ ((dom g) \ (g " {0}))) /\ (dom g1)) by XBOOLE_1:16
.= ((dom f) /\ ((dom f) \ (f " {0}))) /\ (((dom (f1 (#) g)) /\ ((dom g) \ (g " {0}))) /\ (dom g1)) by VALUED_1:def_4
.= ((dom f) /\ ((dom f) \ (f " {0}))) /\ ((dom (f1 (#) g)) /\ ((dom g1) /\ ((dom g) \ (g " {0})))) by XBOOLE_1:16
.= (dom (f1 (#) g)) /\ ((((dom f) \ (f " {0})) /\ (dom f)) /\ ((dom g1) /\ ((dom g) \ (g " {0})))) by XBOOLE_1:16
.= (dom (f1 (#) g)) /\ (((dom f) \ (f " {0})) /\ ((dom f) /\ ((dom g1) /\ ((dom g) \ (g " {0}))))) by XBOOLE_1:16
.= (dom (f1 (#) g)) /\ (((dom f) \ (f " {0})) /\ (((dom g1) /\ (dom f)) /\ ((dom g) \ (g " {0})))) by XBOOLE_1:16
.= (dom (f1 (#) g)) /\ (((dom f) \ (f " {0})) /\ ((dom (g1 (#) f)) /\ ((dom g) \ (g " {0})))) by VALUED_1:def_4
.= (dom (f1 (#) g)) /\ ((dom (g1 (#) f)) /\ (((dom f) \ (f " {0})) /\ ((dom g) \ (g " {0})))) by XBOOLE_1:16
.= ((dom (f1 (#) g)) /\ (dom (g1 (#) f))) /\ (((dom f) \ (f " {0})) /\ ((dom g) \ (g " {0}))) by XBOOLE_1:16
.= (dom ((f1 (#) g) + (g1 (#) f))) /\ (((dom f) \ (f " {0})) /\ ((dom g) \ (g " {0}))) by VALUED_1:def_1
.= (dom ((f1 (#) g) + (g1 (#) f))) /\ ((dom (f (#) g)) \ ((f (#) g) " {0})) by Th2
.= dom (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) by Def1 ;
hence (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g) by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem :: RFUNCT_1:41
for f, g, f1, g1 being complex-valued Function holds (f / g) / (f1 / g1) = (f (#) (g1 | (dom (g1 ^)))) / (g (#) f1)
proof
let f, g, f1, g1 be complex-valued Function; ::_thesis: (f / g) / (f1 / g1) = (f (#) (g1 | (dom (g1 ^)))) / (g (#) f1)
thus (f / g) / (f1 / g1) = (f / g) (#) ((f1 / g1) ^) by Th31
.= (f / g) (#) ((g1 | (dom (g1 ^))) / f1) by Th35
.= (f (#) (g1 | (dom (g1 ^)))) / (g (#) f1) by Th34 ; ::_thesis: verum
end;
theorem :: RFUNCT_1:42
for f1, f, g1, g being complex-valued Function holds (f1 / f) - (g1 / g) = ((f1 (#) g) - (g1 (#) f)) / (f (#) g)
proof
let f1, f, g1, g be complex-valued Function; ::_thesis: (f1 / f) - (g1 / g) = ((f1 (#) g) - (g1 (#) f)) / (f (#) g)
thus (f1 / f) - (g1 / g) = (f1 / f) + (((- 1) (#) g1) / g) by Th32
.= ((f1 (#) g) + (((- 1) (#) g1) (#) f)) / (f (#) g) by Th40
.= ((f1 (#) g) - (g1 (#) f)) / (f (#) g) by Th12 ; ::_thesis: verum
end;
theorem :: RFUNCT_1:43
for f1, f2 being complex-valued Function holds abs (f1 / f2) = (abs f1) / (abs f2)
proof
let f1, f2 be complex-valued Function; ::_thesis: abs (f1 / f2) = (abs f1) / (abs f2)
thus abs (f1 / f2) = abs (f1 (#) (f2 ^)) by Th31
.= (abs f1) (#) (abs (f2 ^)) by Th24
.= (abs f1) (#) ((abs f2) ^) by Th30
.= (abs f1) / (abs f2) by Th31 ; ::_thesis: verum
end;
theorem Th44: :: RFUNCT_1:44
for X being set
for f1, f2 being complex-valued Function holds
( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) )
proof
let X be set ; ::_thesis: for f1, f2 being complex-valued Function holds
( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) )
let f1, f2 be complex-valued Function; ::_thesis: ( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) )
A1: now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_+_f2)_|_X)_holds_
((f1_+_f2)_|_X)_._c_=_((f1_|_X)_+_(f2_|_X))_._c
let c be set ; ::_thesis: ( c in dom ((f1 + f2) | X) implies ((f1 + f2) | X) . c = ((f1 | X) + (f2 | X)) . c )
assume A2: c in dom ((f1 + f2) | X) ; ::_thesis: ((f1 + f2) | X) . c = ((f1 | X) + (f2 | X)) . c
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 VALUED_1:def_1;
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 VALUED_1:def_1;
thus ((f1 + f2) | X) . c = (f1 + f2) . c by A2, FUNCT_1:47
.= (f1 . c) + (f2 . c) by A5, VALUED_1:def_1
.= ((f1 | X) . c) + (f2 . c) by A8, FUNCT_1:47
.= ((f1 | X) . c) + ((f2 | X) . c) by A7, FUNCT_1:47
.= ((f1 | X) + (f2 | X)) . c by A9, VALUED_1:def_1 ; ::_thesis: verum
end;
dom ((f1 + f2) | X) = (dom (f1 + f2)) /\ X by RELAT_1:61
.= ((dom f1) /\ (dom f2)) /\ (X /\ X) by VALUED_1:def_1
.= (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 VALUED_1:def_1 ;
hence (f1 + f2) | X = (f1 | X) + (f2 | X) by A1, FUNCT_1:2; ::_thesis: ( (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) )
A10: now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_+_f2)_|_X)_holds_
((f1_+_f2)_|_X)_._c_=_((f1_|_X)_+_f2)_._c
let c be set ; ::_thesis: ( c in dom ((f1 + f2) | X) implies ((f1 + f2) | X) . c = ((f1 | X) + f2) . c )
assume A11: c in dom ((f1 + f2) | X) ; ::_thesis: ((f1 + f2) | X) . c = ((f1 | X) + f2) . c
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 VALUED_1:def_1;
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 VALUED_1:def_1;
thus ((f1 + f2) | X) . c = (f1 + f2) . c by A11, FUNCT_1:47
.= (f1 . c) + (f2 . c) by A14, VALUED_1:def_1
.= ((f1 | X) . c) + (f2 . c) by A16, FUNCT_1:47
.= ((f1 | X) + f2) . c by A17, VALUED_1:def_1 ; ::_thesis: verum
end;
dom ((f1 + f2) | X) = (dom (f1 + f2)) /\ X by RELAT_1:61
.= ((dom f1) /\ (dom f2)) /\ X by VALUED_1:def_1
.= ((dom f1) /\ X) /\ (dom f2) by XBOOLE_1:16
.= (dom (f1 | X)) /\ (dom f2) by RELAT_1:61
.= dom ((f1 | X) + f2) by VALUED_1:def_1 ;
hence (f1 + f2) | X = (f1 | X) + f2 by A10, FUNCT_1:2; ::_thesis: (f1 + f2) | X = f1 + (f2 | X)
A18: now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_+_f2)_|_X)_holds_
((f1_+_f2)_|_X)_._c_=_(f1_+_(f2_|_X))_._c
let c be set ; ::_thesis: ( c in dom ((f1 + f2) | X) implies ((f1 + f2) | X) . c = (f1 + (f2 | X)) . c )
assume A19: c in dom ((f1 + f2) | X) ; ::_thesis: ((f1 + f2) | X) . c = (f1 + (f2 | X)) . c
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 VALUED_1:def_1;
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 VALUED_1:def_1;
thus ((f1 + f2) | X) . c = (f1 + f2) . c by A19, FUNCT_1:47
.= (f1 . c) + (f2 . c) by A22, VALUED_1:def_1
.= (f1 . c) + ((f2 | X) . c) by A24, FUNCT_1:47
.= (f1 + (f2 | X)) . c by A25, VALUED_1:def_1 ; ::_thesis: verum
end;
dom ((f1 + f2) | X) = (dom (f1 + f2)) /\ X by RELAT_1:61
.= ((dom f1) /\ (dom f2)) /\ X by VALUED_1:def_1
.= (dom f1) /\ ((dom f2) /\ X) by XBOOLE_1:16
.= (dom f1) /\ (dom (f2 | X)) by RELAT_1:61
.= dom (f1 + (f2 | X)) by VALUED_1:def_1 ;
hence (f1 + f2) | X = f1 + (f2 | X) by A18, FUNCT_1:2; ::_thesis: verum
end;
theorem Th45: :: RFUNCT_1:45
for X being set
for f1, f2 being complex-valued Function holds
( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )
proof
let X be set ; ::_thesis: for f1, f2 being complex-valued Function holds
( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )
let f1, f2 be complex-valued Function; ::_thesis: ( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )
A1: now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_(#)_f2)_|_X)_holds_
((f1_(#)_f2)_|_X)_._c_=_((f1_|_X)_(#)_(f2_|_X))_._c
let c be set ; ::_thesis: ( c in dom ((f1 (#) f2) | X) implies ((f1 (#) f2) | X) . c = ((f1 | X) (#) (f2 | X)) . c )
assume A2: c in dom ((f1 (#) f2) | X) ; ::_thesis: ((f1 (#) f2) | X) . c = ((f1 | X) (#) (f2 | X)) . c
then A3: c in (dom (f1 (#) f2)) /\ X by RELAT_1:61;
then A4: c in X by XBOOLE_0:def_4;
c in dom (f1 (#) f2) by A3, XBOOLE_0:def_4;
then A5: c in (dom f1) /\ (dom f2) by VALUED_1:def_4;
then c in dom f1 by XBOOLE_0:def_4;
then c in (dom f1) /\ X by A4, XBOOLE_0:def_4;
then A6: c in dom (f1 | X) by RELAT_1:61;
c in dom f2 by A5, 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;
thus ((f1 (#) f2) | X) . c = (f1 (#) f2) . c by A2, FUNCT_1:47
.= (f1 . c) * (f2 . c) by VALUED_1:5
.= ((f1 | X) . c) * (f2 . c) by A6, FUNCT_1:47
.= ((f1 | X) . c) * ((f2 | X) . c) by A7, FUNCT_1:47
.= ((f1 | X) (#) (f2 | X)) . c by VALUED_1:5 ; ::_thesis: verum
end;
dom ((f1 (#) f2) | X) = (dom (f1 (#) f2)) /\ X by RELAT_1:61
.= ((dom f1) /\ (dom f2)) /\ (X /\ X) by VALUED_1:def_4
.= (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 VALUED_1:def_4 ;
hence (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) by A1, FUNCT_1:2; ::_thesis: ( (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )
A8: now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_(#)_f2)_|_X)_holds_
((f1_(#)_f2)_|_X)_._c_=_((f1_|_X)_(#)_f2)_._c
let c be set ; ::_thesis: ( c in dom ((f1 (#) f2) | X) implies ((f1 (#) f2) | X) . c = ((f1 | X) (#) f2) . c )
assume A9: c in dom ((f1 (#) f2) | X) ; ::_thesis: ((f1 (#) f2) | X) . c = ((f1 | X) (#) f2) . c
then A10: c in (dom (f1 (#) f2)) /\ X by RELAT_1:61;
then c in dom (f1 (#) f2) by XBOOLE_0:def_4;
then c in (dom f1) /\ (dom f2) by VALUED_1:def_4;
then A11: c in dom f1 by XBOOLE_0:def_4;
c in X by A10, XBOOLE_0:def_4;
then c in (dom f1) /\ X by A11, XBOOLE_0:def_4;
then A12: c in dom (f1 | X) by RELAT_1:61;
thus ((f1 (#) f2) | X) . c = (f1 (#) f2) . c by A9, FUNCT_1:47
.= (f1 . c) * (f2 . c) by VALUED_1:5
.= ((f1 | X) . c) * (f2 . c) by A12, FUNCT_1:47
.= ((f1 | X) (#) f2) . c by VALUED_1:5 ; ::_thesis: verum
end;
dom ((f1 (#) f2) | X) = (dom (f1 (#) f2)) /\ X by RELAT_1:61
.= ((dom f1) /\ (dom f2)) /\ X by VALUED_1:def_4
.= ((dom f1) /\ X) /\ (dom f2) by XBOOLE_1:16
.= (dom (f1 | X)) /\ (dom f2) by RELAT_1:61
.= dom ((f1 | X) (#) f2) by VALUED_1:def_4 ;
hence (f1 (#) f2) | X = (f1 | X) (#) f2 by A8, FUNCT_1:2; ::_thesis: (f1 (#) f2) | X = f1 (#) (f2 | X)
A13: now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_(#)_f2)_|_X)_holds_
((f1_(#)_f2)_|_X)_._c_=_(f1_(#)_(f2_|_X))_._c
let c be set ; ::_thesis: ( c in dom ((f1 (#) f2) | X) implies ((f1 (#) f2) | X) . c = (f1 (#) (f2 | X)) . c )
assume A14: c in dom ((f1 (#) f2) | X) ; ::_thesis: ((f1 (#) f2) | X) . c = (f1 (#) (f2 | X)) . c
then A15: c in (dom (f1 (#) f2)) /\ X by RELAT_1:61;
then c in dom (f1 (#) f2) by XBOOLE_0:def_4;
then c in (dom f1) /\ (dom f2) by VALUED_1:def_4;
then A16: c in dom f2 by XBOOLE_0:def_4;
c in X by A15, XBOOLE_0:def_4;
then c in (dom f2) /\ X by A16, XBOOLE_0:def_4;
then A17: c in dom (f2 | X) by RELAT_1:61;
thus ((f1 (#) f2) | X) . c = (f1 (#) f2) . c by A14, FUNCT_1:47
.= (f1 . c) * (f2 . c) by VALUED_1:5
.= (f1 . c) * ((f2 | X) . c) by A17, FUNCT_1:47
.= (f1 (#) (f2 | X)) . c by VALUED_1:5 ; ::_thesis: verum
end;
dom ((f1 (#) f2) | X) = (dom (f1 (#) f2)) /\ X by RELAT_1:61
.= ((dom f1) /\ (dom f2)) /\ X by VALUED_1:def_4
.= (dom f1) /\ ((dom f2) /\ X) by XBOOLE_1:16
.= (dom f1) /\ (dom (f2 | X)) by RELAT_1:61
.= dom (f1 (#) (f2 | X)) by VALUED_1:def_4 ;
hence (f1 (#) f2) | X = f1 (#) (f2 | X) by A13, FUNCT_1:2; ::_thesis: verum
end;
theorem Th46: :: RFUNCT_1:46
for X being set
for f being complex-valued Function holds
( (- f) | X = - (f | X) & (f ^) | X = (f | X) ^ & (abs f) | X = abs (f | X) )
proof
let X be set ; ::_thesis: for f being complex-valued Function holds
( (- f) | X = - (f | X) & (f ^) | X = (f | X) ^ & (abs f) | X = abs (f | X) )
let f be complex-valued Function; ::_thesis: ( (- f) | X = - (f | X) & (f ^) | X = (f | X) ^ & (abs f) | X = abs (f | X) )
A1: now__::_thesis:_for_c_being_set_st_c_in_dom_((-_f)_|_X)_holds_
((-_f)_|_X)_._c_=_(-_(f_|_X))_._c
let c be set ; ::_thesis: ( c in dom ((- f) | X) implies ((- f) | X) . c = (- (f | X)) . c )
assume A2: c in dom ((- f) | X) ; ::_thesis: ((- f) | X) . c = (- (f | X)) . c
then A3: c in (dom (- f)) /\ X by RELAT_1:61;
then c in dom (- f) by XBOOLE_0:def_4;
then A4: c in dom f by VALUED_1:8;
c in X by A3, XBOOLE_0:def_4;
then c in (dom f) /\ X by A4, XBOOLE_0:def_4;
then A5: c in dom (f | X) by RELAT_1:61;
thus ((- f) | X) . c = (- f) . c by A2, FUNCT_1:47
.= - (f . c) by VALUED_1:8
.= - ((f | X) . c) by A5, FUNCT_1:47
.= (- (f | X)) . c by VALUED_1:8 ; ::_thesis: verum
end;
dom ((- f) | X) = (dom (- f)) /\ X by RELAT_1:61
.= (dom f) /\ X by VALUED_1:8
.= dom (f | X) by RELAT_1:61
.= dom (- (f | X)) by VALUED_1:8 ;
hence (- f) | X = - (f | X) by A1, FUNCT_1:2; ::_thesis: ( (f ^) | X = (f | X) ^ & (abs f) | X = abs (f | X) )
A6: dom ((f ^) | X) = (dom (f ^)) /\ X by RELAT_1:61
.= ((dom f) \ (f " {0})) /\ X by Def2
.= ((dom f) /\ X) \ ((f " {0}) /\ X) by XBOOLE_1:50
.= (dom (f | X)) \ (X /\ (f " {0})) by RELAT_1:61
.= (dom (f | X)) \ ((f | X) " {0}) by FUNCT_1:70
.= dom ((f | X) ^) by Def2 ;
A7: dom ((f | X) ^) c= dom (f | X) by Th1;
now__::_thesis:_for_c_being_set_st_c_in_dom_((f_^)_|_X)_holds_
((f_^)_|_X)_._c_=_((f_|_X)_^)_._c
let c be set ; ::_thesis: ( c in dom ((f ^) | X) implies ((f ^) | X) . c = ((f | X) ^) . c )
assume A8: c in dom ((f ^) | X) ; ::_thesis: ((f ^) | X) . c = ((f | X) ^) . c
then c in (dom (f ^)) /\ X by RELAT_1:61;
then A9: c in dom (f ^) by XBOOLE_0:def_4;
thus ((f ^) | X) . c = (f ^) . c by A8, FUNCT_1:47
.= (f . c) " by A9, Def2
.= ((f | X) . c) " by A7, A6, A8, FUNCT_1:47
.= ((f | X) ^) . c by A6, A8, Def2 ; ::_thesis: verum
end;
hence (f ^) | X = (f | X) ^ by A6, FUNCT_1:2; ::_thesis: (abs f) | X = abs (f | X)
A10: dom ((abs f) | X) = (dom (abs f)) /\ X by RELAT_1:61
.= (dom f) /\ X by VALUED_1:def_11
.= dom (f | X) by RELAT_1:61
.= dom (abs (f | X)) by VALUED_1:def_11 ;
now__::_thesis:_for_c_being_set_st_c_in_dom_((abs_f)_|_X)_holds_
((abs_f)_|_X)_._c_=_(abs_(f_|_X))_._c
let c be set ; ::_thesis: ( c in dom ((abs f) | X) implies ((abs f) | X) . c = (abs (f | X)) . c )
assume A11: c in dom ((abs f) | X) ; ::_thesis: ((abs f) | X) . c = (abs (f | X)) . c
then A12: c in dom (f | X) by A10, VALUED_1:def_11;
thus ((abs f) | X) . c = (abs f) . c by A11, FUNCT_1:47
.= abs (f . c) by VALUED_1:18
.= abs ((f | X) . c) by A12, FUNCT_1:47
.= (abs (f | X)) . c by VALUED_1:18 ; ::_thesis: verum
end;
hence (abs f) | X = abs (f | X) by A10, FUNCT_1:2; ::_thesis: verum
end;
theorem :: RFUNCT_1:47
for X being set
for f1, f2 being complex-valued Function holds
( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) )
proof
let X be set ; ::_thesis: for f1, f2 being complex-valued Function holds
( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) )
let f1, f2 be complex-valued Function; ::_thesis: ( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) )
thus (f1 - f2) | X = (f1 | X) + ((- f2) | X) by Th44
.= (f1 | X) - (f2 | X) by Th46 ; ::_thesis: ( (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) )
thus (f1 - f2) | X = (f1 | X) - f2 by Th44; ::_thesis: (f1 - f2) | X = f1 - (f2 | X)
thus (f1 - f2) | X = f1 + ((- f2) | X) by Th44
.= f1 - (f2 | X) by Th46 ; ::_thesis: verum
end;
theorem :: RFUNCT_1:48
for X being set
for f1, f2 being complex-valued Function holds
( (f1 / f2) | X = (f1 | X) / (f2 | X) & (f1 / f2) | X = (f1 | X) / f2 & (f1 / f2) | X = f1 / (f2 | X) )
proof
let X be set ; ::_thesis: for f1, f2 being complex-valued Function holds
( (f1 / f2) | X = (f1 | X) / (f2 | X) & (f1 / f2) | X = (f1 | X) / f2 & (f1 / f2) | X = f1 / (f2 | X) )
let f1, f2 be complex-valued Function; ::_thesis: ( (f1 / f2) | X = (f1 | X) / (f2 | X) & (f1 / f2) | X = (f1 | X) / f2 & (f1 / f2) | X = f1 / (f2 | X) )
thus (f1 / f2) | X = (f1 (#) (f2 ^)) | X by Th31
.= (f1 | X) (#) ((f2 ^) | X) by Th45
.= (f1 | X) (#) ((f2 | X) ^) by Th46
.= (f1 | X) / (f2 | X) by Th31 ; ::_thesis: ( (f1 / f2) | X = (f1 | X) / f2 & (f1 / f2) | X = f1 / (f2 | X) )
thus (f1 / f2) | X = (f1 (#) (f2 ^)) | X by Th31
.= (f1 | X) (#) (f2 ^) by Th45
.= (f1 | X) / f2 by Th31 ; ::_thesis: (f1 / f2) | X = f1 / (f2 | X)
thus (f1 / f2) | X = (f1 (#) (f2 ^)) | X by Th31
.= f1 (#) ((f2 ^) | X) by Th45
.= f1 (#) ((f2 | X) ^) by Th46
.= f1 / (f2 | X) by Th31 ; ::_thesis: verum
end;
theorem Th49: :: RFUNCT_1:49
for X being set
for f being complex-valued Function
for r being complex number holds (r (#) f) | X = r (#) (f | X)
proof
let X be set ; ::_thesis: for f being complex-valued Function
for r being complex number holds (r (#) f) | X = r (#) (f | X)
let f be complex-valued Function; ::_thesis: for r being complex number holds (r (#) f) | X = r (#) (f | X)
let r be complex number ; ::_thesis: (r (#) f) | X = r (#) (f | X)
A1: now__::_thesis:_for_c_being_set_st_c_in_dom_((r_(#)_f)_|_X)_holds_
((r_(#)_f)_|_X)_._c_=_(r_(#)_(f_|_X))_._c
let c be set ; ::_thesis: ( c in dom ((r (#) f) | X) implies ((r (#) f) | X) . c = (r (#) (f | X)) . c )
assume A2: c in dom ((r (#) f) | X) ; ::_thesis: ((r (#) f) | X) . c = (r (#) (f | X)) . c
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 VALUED_1:def_5;
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 VALUED_1:def_5;
thus ((r (#) f) | X) . c = (r (#) f) . c by A2, FUNCT_1:47
.= r * (f . c) by A5, VALUED_1:def_5
.= r * ((f | X) . c) by A6, FUNCT_1:47
.= (r (#) (f | X)) . c by A7, VALUED_1:def_5 ; ::_thesis: verum
end;
dom ((r (#) f) | X) = (dom (r (#) f)) /\ X by RELAT_1:61
.= (dom f) /\ X by VALUED_1:def_5
.= dom (f | X) by RELAT_1:61
.= dom (r (#) (f | X)) by VALUED_1:def_5 ;
hence (r (#) f) | X = r (#) (f | X) by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem Th50: :: RFUNCT_1:50
for C being non empty set
for f1, f2 being PartFunc of C,REAL holds
( ( f1 is total & f2 is total implies f1 + f2 is total ) & ( f1 + f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 - f2 is total ) & ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 (#) f2 is total ) & ( f1 (#) f2 is total implies ( f1 is total & f2 is total ) ) )
proof
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,REAL holds
( ( f1 is total & f2 is total implies f1 + f2 is total ) & ( f1 + f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 - f2 is total ) & ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 (#) f2 is total ) & ( f1 (#) f2 is total implies ( f1 is total & f2 is total ) ) )
let f1, f2 be PartFunc of C,REAL; ::_thesis: ( ( f1 is total & f2 is total implies f1 + f2 is total ) & ( f1 + f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 - f2 is total ) & ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 (#) f2 is total ) & ( f1 (#) f2 is total implies ( f1 is total & f2 is total ) ) )
thus ( ( f1 is total & f2 is total ) iff f1 + f2 is total ) ::_thesis: ( ( f1 is total & f2 is total implies f1 - f2 is total ) & ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 (#) f2 is total ) & ( f1 (#) f2 is total implies ( f1 is total & f2 is total ) ) )
proof
thus ( f1 is total & f2 is total implies f1 + f2 is total ) ; ::_thesis: ( f1 + f2 is total implies ( f1 is total & f2 is total ) )
assume f1 + f2 is total ; ::_thesis: ( f1 is total & f2 is total )
then dom (f1 + f2) = C by PARTFUN1:def_2;
then A4: (dom f1) /\ (dom f2) = C by VALUED_1:def_1;
then A5: C c= dom f2 by XBOOLE_1:17;
C c= dom f1 by A4, XBOOLE_1:17;
hence ( dom f1 = C & dom f2 = C ) by A5, XBOOLE_0:def_10; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
thus ( ( f1 is total & f2 is total ) iff f1 - f2 is total ) ::_thesis: ( ( f1 is total & f2 is total ) iff f1 (#) f2 is total )
proof
thus ( f1 is total & f2 is total implies f1 - f2 is total ) ; ::_thesis: ( f1 - f2 is total implies ( f1 is total & f2 is total ) )
assume f1 - f2 is total ; ::_thesis: ( f1 is total & f2 is total )
then dom (f1 - f2) = C by PARTFUN1:def_2;
then A9: (dom f1) /\ (dom f2) = C by VALUED_1:12;
then A10: C c= dom f2 by XBOOLE_1:17;
C c= dom f1 by A9, XBOOLE_1:17;
hence ( dom f1 = C & dom f2 = C ) by A10, XBOOLE_0:def_10; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
thus ( f1 is total & f2 is total implies f1 (#) f2 is total ) ; ::_thesis: ( f1 (#) f2 is total implies ( f1 is total & f2 is total ) )
assume f1 (#) f2 is total ; ::_thesis: ( f1 is total & f2 is total )
then dom (f1 (#) f2) = C by PARTFUN1:def_2;
then A14: (dom f1) /\ (dom f2) = C by VALUED_1:def_4;
then A15: C c= dom f2 by XBOOLE_1:17;
C c= dom f1 by A14, XBOOLE_1:17;
hence ( dom f1 = C & dom f2 = C ) by A15, XBOOLE_0:def_10; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
theorem Th51: :: RFUNCT_1:51
for C being non empty set
for r being real number
for f being PartFunc of C,REAL holds
( f is total iff r (#) f is total )
proof
let C be non empty set ; ::_thesis: for r being real number
for f being PartFunc of C,REAL holds
( f is total iff r (#) f is total )
let r be real number ; ::_thesis: for f being PartFunc of C,REAL holds
( f is total iff r (#) f is total )
let f be PartFunc of C,REAL; ::_thesis: ( f is total iff r (#) f is total )
thus ( f is total implies r (#) f is total ) ; ::_thesis: ( r (#) f is total implies f is total )
assume r (#) f is total ; ::_thesis: f is total
then dom (r (#) f) = C by PARTFUN1:def_2;
hence dom f = C by VALUED_1:def_5; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
theorem :: RFUNCT_1:52
for C being non empty set
for f being PartFunc of C,REAL holds
( f is total iff - f is total ) by Th51;
theorem :: RFUNCT_1:53
for C being non empty set
for f being PartFunc of C,REAL holds
( f is total iff abs f is total )
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,REAL holds
( f is total iff abs f is total )
let f be PartFunc of C,REAL; ::_thesis: ( f is total iff abs f is total )
thus ( f is total implies abs f is total ) ; ::_thesis: ( abs f is total implies f is total )
assume abs f is total ; ::_thesis: f is total
then dom (abs f) = C by PARTFUN1:def_2;
hence dom f = C by VALUED_1:def_11; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
theorem Th54: :: RFUNCT_1:54
for C being non empty set
for f being PartFunc of C,REAL holds
( f ^ is total iff ( f " {0} = {} & f is total ) )
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,REAL holds
( f ^ is total iff ( f " {0} = {} & f is total ) )
let f be PartFunc of C,REAL; ::_thesis: ( f ^ is total iff ( f " {0} = {} & f is total ) )
thus ( f ^ is total implies ( f " {0} = {} & f is total ) ) ::_thesis: ( f " {0} = {} & f is total implies f ^ is total )
proof
assume f ^ is total ; ::_thesis: ( f " {0} = {} & f is total )
then A1: dom (f ^) = C by PARTFUN1:def_2;
f " {0} c= C ;
then f " {0} c= (dom f) \ (f " {0}) by A1, Def2;
hence f " {0} = {} by XBOOLE_1:38; ::_thesis: f is total
then C = (dom f) \ {} by A1, Def2;
hence dom f = C ; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
assume that
A2: f " {0} = {} and
A3: f is total ; ::_thesis: f ^ is total
thus dom (f ^) = (dom f) \ (f " {0}) by Def2
.= C by A2, A3, PARTFUN1:def_2 ; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
theorem Th55: :: RFUNCT_1:55
for C being non empty set
for f1, f2 being PartFunc of C,REAL holds
( ( f1 is total & f2 " {0} = {} & f2 is total ) iff f1 / f2 is total )
proof
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,REAL holds
( ( f1 is total & f2 " {0} = {} & f2 is total ) iff f1 / f2 is total )
let f1, f2 be PartFunc of C,REAL; ::_thesis: ( ( f1 is total & f2 " {0} = {} & f2 is total ) iff f1 / f2 is total )
thus ( f1 is total & f2 " {0} = {} & f2 is total implies f1 / f2 is total ) ::_thesis: ( f1 / f2 is total implies ( f1 is total & f2 " {0} = {} & f2 is total ) )
proof
assume that
A1: f1 is total and
A2: f2 " {0} = {} and
A3: f2 is total ; ::_thesis: f1 / f2 is total
f2 ^ is total by A2, A3, Th54;
then f1 (#) (f2 ^) is total by A1;
hence f1 / f2 is total by Th31; ::_thesis: verum
end;
assume f1 / f2 is total ; ::_thesis: ( f1 is total & f2 " {0} = {} & f2 is total )
then A4: f1 (#) (f2 ^) is total by Th31;
hence f1 is total by Th50; ::_thesis: ( f2 " {0} = {} & f2 is total )
f2 ^ is total by A4, Th50;
hence ( f2 " {0} = {} & f2 is total ) by Th54; ::_thesis: verum
end;
theorem :: RFUNCT_1:56
for C being non empty set
for c being Element of C
for f1, f2 being PartFunc of C,REAL st f1 is total & f2 is total holds
( (f1 + f2) . c = (f1 . c) + (f2 . c) & (f1 - f2) . c = (f1 . c) - (f2 . c) & (f1 (#) f2) . c = (f1 . c) * (f2 . c) )
proof
let C be non empty set ; ::_thesis: for c being Element of C
for f1, f2 being PartFunc of C,REAL st f1 is total & f2 is total holds
( (f1 + f2) . c = (f1 . c) + (f2 . c) & (f1 - f2) . c = (f1 . c) - (f2 . c) & (f1 (#) f2) . c = (f1 . c) * (f2 . c) )
let c be Element of C; ::_thesis: for f1, f2 being PartFunc of C,REAL st f1 is total & f2 is total holds
( (f1 + f2) . c = (f1 . c) + (f2 . c) & (f1 - f2) . c = (f1 . c) - (f2 . c) & (f1 (#) f2) . c = (f1 . c) * (f2 . c) )
let f1, f2 be PartFunc of C,REAL; ::_thesis: ( f1 is total & f2 is total implies ( (f1 + f2) . c = (f1 . c) + (f2 . c) & (f1 - f2) . c = (f1 . c) - (f2 . c) & (f1 (#) f2) . c = (f1 . c) * (f2 . c) ) )
assume that
A1: f1 is total and
A2: f2 is total ; ::_thesis: ( (f1 + f2) . c = (f1 . c) + (f2 . c) & (f1 - f2) . c = (f1 . c) - (f2 . c) & (f1 (#) f2) . c = (f1 . c) * (f2 . c) )
f1 + f2 is total by A1, A2;
then dom (f1 + f2) = C by PARTFUN1:def_2;
hence (f1 + f2) . c = (f1 . c) + (f2 . c) by VALUED_1:def_1; ::_thesis: ( (f1 - f2) . c = (f1 . c) - (f2 . c) & (f1 (#) f2) . c = (f1 . c) * (f2 . c) )
f1 - f2 is total by A1, A2;
then dom (f1 - f2) = C by PARTFUN1:def_2;
hence (f1 - f2) . c = (f1 . c) - (f2 . c) by VALUED_1:13; ::_thesis: (f1 (#) f2) . c = (f1 . c) * (f2 . c)
thus (f1 (#) f2) . c = (f1 . c) * (f2 . c) by VALUED_1:5; ::_thesis: verum
end;
theorem :: RFUNCT_1:57
for C being non empty set
for c being Element of C
for r being real number
for f being PartFunc of C,REAL st f is total holds
(r (#) f) . c = r * (f . c)
proof
let C be non empty set ; ::_thesis: for c being Element of C
for r being real number
for f being PartFunc of C,REAL st f is total holds
(r (#) f) . c = r * (f . c)
let c be Element of C; ::_thesis: for r being real number
for f being PartFunc of C,REAL st f is total holds
(r (#) f) . c = r * (f . c)
let r be real number ; ::_thesis: for f being PartFunc of C,REAL st f is total holds
(r (#) f) . c = r * (f . c)
let f be PartFunc of C,REAL; ::_thesis: ( f is total implies (r (#) f) . c = r * (f . c) )
assume f is total ; ::_thesis: (r (#) f) . c = r * (f . c)
then r (#) f is total ;
then dom (r (#) f) = C by PARTFUN1:def_2;
hence (r (#) f) . c = r * (f . c) by VALUED_1:def_5; ::_thesis: verum
end;
theorem :: RFUNCT_1:58
for C being non empty set
for c being Element of C
for f being PartFunc of C,REAL st f is total holds
( (- f) . c = - (f . c) & (abs f) . c = abs (f . c) ) by VALUED_1:8, VALUED_1:18;
theorem :: RFUNCT_1:59
for C being non empty set
for c being Element of C
for f being PartFunc of C,REAL st f ^ is total holds
(f ^) . c = (f . c) "
proof
let C be non empty set ; ::_thesis: for c being Element of C
for f being PartFunc of C,REAL st f ^ is total holds
(f ^) . c = (f . c) "
let c be Element of C; ::_thesis: for f being PartFunc of C,REAL st f ^ is total holds
(f ^) . c = (f . c) "
let f be PartFunc of C,REAL; ::_thesis: ( f ^ is total implies (f ^) . c = (f . c) " )
assume f ^ is total ; ::_thesis: (f ^) . c = (f . c) "
then dom (f ^) = C by PARTFUN1:def_2;
hence (f ^) . c = (f . c) " by Def2; ::_thesis: verum
end;
theorem :: RFUNCT_1:60
for C being non empty set
for c being Element of C
for f1, f2 being PartFunc of C,REAL st f1 is total & f2 ^ is total holds
(f1 / f2) . c = (f1 . c) * ((f2 . c) ")
proof
let C be non empty set ; ::_thesis: for c being Element of C
for f1, f2 being PartFunc of C,REAL st f1 is total & f2 ^ is total holds
(f1 / f2) . c = (f1 . c) * ((f2 . c) ")
let c be Element of C; ::_thesis: for f1, f2 being PartFunc of C,REAL st f1 is total & f2 ^ is total holds
(f1 / f2) . c = (f1 . c) * ((f2 . c) ")
let f1, f2 be PartFunc of C,REAL; ::_thesis: ( f1 is total & f2 ^ is total implies (f1 / f2) . c = (f1 . c) * ((f2 . c) ") )
assume that
A1: f1 is total and
A2: f2 ^ is total ; ::_thesis: (f1 / f2) . c = (f1 . c) * ((f2 . c) ")
A3: f2 is total by A2, Th54;
f2 " {0} = {} by A2, Th54;
then f1 / f2 is total by A1, A3, Th55;
then dom (f1 / f2) = C by PARTFUN1:def_2;
hence (f1 / f2) . c = (f1 . c) * ((f2 . c) ") by Def1; ::_thesis: verum
end;
definition
let X, C be set ;
:: original: chi
redefine func chi (X,C) -> PartFunc of C,REAL;
coherence
chi (X,C) is PartFunc of C,REAL
proof
now__::_thesis:_for_x_being_set_st_x_in_rng_(chi_(X,C))_holds_
x_in_REAL
let x be set ; ::_thesis: ( x in rng (chi (X,C)) implies x in REAL )
assume x in rng (chi (X,C)) ; ::_thesis: x in REAL
then ( x = 0 or x = 1 ) by TARSKI:def_2;
hence x in REAL ; ::_thesis: verum
end;
then A1: rng (chi (X,C)) c= REAL by TARSKI:def_3;
dom (chi (X,C)) = C by FUNCT_3:def_3;
hence chi (X,C) is PartFunc of C,REAL by A1, RELSET_1:4; ::_thesis: verum
end;
end;
registration
let X, C be set ;
cluster chi (X,C) -> total for PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = chi (X,C) holds
b1 is total
proof
dom (chi (X,C)) = C by FUNCT_3:def_3;
hence for b1 being PartFunc of C,REAL st b1 = chi (X,C) holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
theorem Th61: :: RFUNCT_1:61
for X being set
for C being non empty set
for f being PartFunc of C,REAL holds
( f = chi (X,C) iff ( dom f = C & ( for c being Element of C holds
( ( c in X implies f . c = 1 ) & ( not c in X implies f . c = 0 ) ) ) ) )
proof
let X be set ; ::_thesis: for C being non empty set
for f being PartFunc of C,REAL holds
( f = chi (X,C) iff ( dom f = C & ( for c being Element of C holds
( ( c in X implies f . c = 1 ) & ( not c in X implies f . c = 0 ) ) ) ) )
let C be non empty set ; ::_thesis: for f being PartFunc of C,REAL holds
( f = chi (X,C) iff ( dom f = C & ( for c being Element of C holds
( ( c in X implies f . c = 1 ) & ( not c in X implies f . c = 0 ) ) ) ) )
let f be PartFunc of C,REAL; ::_thesis: ( f = chi (X,C) iff ( dom f = C & ( for c being Element of C holds
( ( c in X implies f . c = 1 ) & ( not c in X implies f . c = 0 ) ) ) ) )
thus ( f = chi (X,C) implies ( dom f = C & ( for c being Element of C holds
( ( c in X implies f . c = 1 ) & ( not c in X implies f . c = 0 ) ) ) ) ) by FUNCT_3:def_3; ::_thesis: ( dom f = C & ( for c being Element of C holds
( ( c in X implies f . c = 1 ) & ( not c in X implies f . c = 0 ) ) ) implies f = chi (X,C) )
assume that
A1: dom f = C and
A2: for c being Element of C holds
( ( c in X implies f . c = 1 ) & ( not c in X implies f . c = 0 ) ) ; ::_thesis: f = chi (X,C)
for x being set st x in C holds
( ( x in X implies f . x = 1 ) & ( not x in X implies f . x = 0 ) ) by A2;
hence f = chi (X,C) by A1, FUNCT_3:def_3; ::_thesis: verum
end;
theorem :: RFUNCT_1:62
for X being set
for C being non empty set holds chi (X,C) is total ;
theorem :: RFUNCT_1:63
for X being set
for C being non empty set
for c being Element of C holds
( c in X iff (chi (X,C)) . c = 1 ) by Th61;
theorem :: RFUNCT_1:64
for X being set
for C being non empty set
for c being Element of C holds
( not c in X iff (chi (X,C)) . c = 0 ) by Th61;
theorem :: RFUNCT_1:65
for X being set
for C being non empty set
for c being Element of C holds
( c in C \ X iff (chi (X,C)) . c = 0 )
proof
let X be set ; ::_thesis: for C being non empty set
for c being Element of C holds
( c in C \ X iff (chi (X,C)) . c = 0 )
let C be non empty set ; ::_thesis: for c being Element of C holds
( c in C \ X iff (chi (X,C)) . c = 0 )
let c be Element of C; ::_thesis: ( c in C \ X iff (chi (X,C)) . c = 0 )
thus ( c in C \ X implies (chi (X,C)) . c = 0 ) ::_thesis: ( (chi (X,C)) . c = 0 implies c in C \ X )
proof
assume c in C \ X ; ::_thesis: (chi (X,C)) . c = 0
then not c in X by XBOOLE_0:def_5;
hence (chi (X,C)) . c = 0 by Th61; ::_thesis: verum
end;
assume (chi (X,C)) . c = 0 ; ::_thesis: c in C \ X
then not c in X by Th61;
hence c in C \ X by XBOOLE_0:def_5; ::_thesis: verum
end;
theorem :: RFUNCT_1:66
for C being non empty set
for c being Element of C holds (chi (C,C)) . c = 1 by Th61;
theorem Th67: :: RFUNCT_1:67
for X being set
for C being non empty set
for c being Element of C holds
( (chi (X,C)) . c <> 1 iff (chi (X,C)) . c = 0 )
proof
let X be set ; ::_thesis: for C being non empty set
for c being Element of C holds
( (chi (X,C)) . c <> 1 iff (chi (X,C)) . c = 0 )
let C be non empty set ; ::_thesis: for c being Element of C holds
( (chi (X,C)) . c <> 1 iff (chi (X,C)) . c = 0 )
let c be Element of C; ::_thesis: ( (chi (X,C)) . c <> 1 iff (chi (X,C)) . c = 0 )
thus ( (chi (X,C)) . c <> 1 implies (chi (X,C)) . c = 0 ) ::_thesis: ( (chi (X,C)) . c = 0 implies (chi (X,C)) . c <> 1 )
proof
c in C ;
then c in dom (chi (X,C)) by Th61;
then A1: (chi (X,C)) . c in rng (chi (X,C)) by FUNCT_1:def_3;
A2: rng (chi (X,C)) c= {0,1} by FUNCT_3:39;
assume (chi (X,C)) . c <> 1 ; ::_thesis: (chi (X,C)) . c = 0
hence (chi (X,C)) . c = 0 by A1, A2, TARSKI:def_2; ::_thesis: verum
end;
assume that
A3: (chi (X,C)) . c = 0 and
A4: (chi (X,C)) . c = 1 ; ::_thesis: contradiction
thus contradiction by A3, A4; ::_thesis: verum
end;
theorem :: RFUNCT_1:68
for X, Y being set
for C being non empty set st X misses Y holds
(chi (X,C)) + (chi (Y,C)) = chi ((X \/ Y),C)
proof
let X, Y be set ; ::_thesis: for C being non empty set st X misses Y holds
(chi (X,C)) + (chi (Y,C)) = chi ((X \/ Y),C)
let C be non empty set ; ::_thesis: ( X misses Y implies (chi (X,C)) + (chi (Y,C)) = chi ((X \/ Y),C) )
assume A1: X /\ Y = {} ; :: according to XBOOLE_0:def_7 ::_thesis: (chi (X,C)) + (chi (Y,C)) = chi ((X \/ Y),C)
A2: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((chi_(X,C))_+_(chi_(Y,C)))_holds_
((chi_(X,C))_+_(chi_(Y,C)))_._c_=_(chi_((X_\/_Y),C))_._c
let c be Element of C; ::_thesis: ( c in dom ((chi (X,C)) + (chi (Y,C))) implies ((chi (X,C)) + (chi (Y,C))) . c = (chi ((X \/ Y),C)) . c )
assume A3: c in dom ((chi (X,C)) + (chi (Y,C))) ; ::_thesis: ((chi (X,C)) + (chi (Y,C))) . c = (chi ((X \/ Y),C)) . c
now__::_thesis:_((chi_(X,C))_._c)_+_((chi_(Y,C))_._c)_=_(chi_((X_\/_Y),C))_._c
percases ( c in X or not c in X ) ;
supposeA4: c in X ; ::_thesis: ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c
then not c in Y by A1, XBOOLE_0:def_4;
then A5: (chi (Y,C)) . c = 0 by Th61;
A6: c in X \/ Y by A4, XBOOLE_0:def_3;
(chi (X,C)) . c = 1 by A4, Th61;
hence ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c by A5, A6, Th61; ::_thesis: verum
end;
supposeA7: not c in X ; ::_thesis: ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c
then A8: (chi (X,C)) . c = 0 by Th61;
now__::_thesis:_((chi_(X,C))_._c)_+_((chi_(Y,C))_._c)_=_(chi_((X_\/_Y),C))_._c
percases ( c in Y or not c in Y ) ;
supposeA9: c in Y ; ::_thesis: ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c
then A10: c in X \/ Y by XBOOLE_0:def_3;
(chi (Y,C)) . c = 1 by A9, Th61;
hence ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c by A8, A10, Th61; ::_thesis: verum
end;
supposeA11: not c in Y ; ::_thesis: ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c
then A12: not c in X \/ Y by A7, XBOOLE_0:def_3;
(chi (Y,C)) . c = 0 by A11, Th61;
hence ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c by A8, A12, Th61; ::_thesis: verum
end;
end;
end;
hence ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c ; ::_thesis: verum
end;
end;
end;
hence ((chi (X,C)) + (chi (Y,C))) . c = (chi ((X \/ Y),C)) . c by A3, VALUED_1:def_1; ::_thesis: verum
end;
dom ((chi (X,C)) + (chi (Y,C))) = (dom (chi (X,C))) /\ (dom (chi (Y,C))) by VALUED_1:def_1
.= C /\ (dom (chi (Y,C))) by Th61
.= C /\ C by Th61
.= dom (chi ((X \/ Y),C)) by Th61 ;
hence (chi (X,C)) + (chi (Y,C)) = chi ((X \/ Y),C) by A2, PARTFUN1:5; ::_thesis: verum
end;
theorem :: RFUNCT_1:69
for X, Y being set
for C being non empty set holds (chi (X,C)) (#) (chi (Y,C)) = chi ((X /\ Y),C)
proof
let X, Y be set ; ::_thesis: for C being non empty set holds (chi (X,C)) (#) (chi (Y,C)) = chi ((X /\ Y),C)
let C be non empty set ; ::_thesis: (chi (X,C)) (#) (chi (Y,C)) = chi ((X /\ Y),C)
A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((chi_(X,C))_(#)_(chi_(Y,C)))_holds_
((chi_(X,C))_(#)_(chi_(Y,C)))_._c_=_(chi_((X_/\_Y),C))_._c
let c be Element of C; ::_thesis: ( c in dom ((chi (X,C)) (#) (chi (Y,C))) implies ((chi (X,C)) (#) (chi (Y,C))) . c = (chi ((X /\ Y),C)) . c )
assume c in dom ((chi (X,C)) (#) (chi (Y,C))) ; ::_thesis: ((chi (X,C)) (#) (chi (Y,C))) . c = (chi ((X /\ Y),C)) . c
now__::_thesis:_((chi_(X,C))_._c)_*_((chi_(Y,C))_._c)_=_(chi_((X_/\_Y),C))_._c
percases ( ((chi (X,C)) . c) * ((chi (Y,C)) . c) = 0 or ((chi (X,C)) . c) * ((chi (Y,C)) . c) <> 0 ) ;
supposeA2: ((chi (X,C)) . c) * ((chi (Y,C)) . c) = 0 ; ::_thesis: ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c
now__::_thesis:_((chi_(X,C))_._c)_*_((chi_(Y,C))_._c)_=_(chi_((X_/\_Y),C))_._c
percases ( (chi (X,C)) . c = 0 or (chi (Y,C)) . c = 0 ) by A2;
suppose (chi (X,C)) . c = 0 ; ::_thesis: ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c
then not c in X by Th61;
then not c in X /\ Y by XBOOLE_0:def_4;
hence ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c by A2, Th61; ::_thesis: verum
end;
suppose (chi (Y,C)) . c = 0 ; ::_thesis: ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c
then not c in Y by Th61;
then not c in X /\ Y by XBOOLE_0:def_4;
hence ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c by A2, Th61; ::_thesis: verum
end;
end;
end;
hence ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c ; ::_thesis: verum
end;
supposeA3: ((chi (X,C)) . c) * ((chi (Y,C)) . c) <> 0 ; ::_thesis: ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c
then A4: (chi (Y,C)) . c <> 0 ;
then A5: (chi (Y,C)) . c = 1 by Th67;
A6: c in Y by A4, Th61;
A7: (chi (X,C)) . c <> 0 by A3;
then c in X by Th61;
then A8: c in X /\ Y by A6, XBOOLE_0:def_4;
(chi (X,C)) . c = 1 by A7, Th67;
hence ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c by A5, A8, Th61; ::_thesis: verum
end;
end;
end;
hence ((chi (X,C)) (#) (chi (Y,C))) . c = (chi ((X /\ Y),C)) . c by VALUED_1:5; ::_thesis: verum
end;
dom ((chi (X,C)) (#) (chi (Y,C))) = (dom (chi (X,C))) /\ (dom (chi (Y,C))) by VALUED_1:def_4
.= C /\ (dom (chi (Y,C))) by Th61
.= C /\ C by Th61
.= dom (chi ((X /\ Y),C)) by Th61 ;
hence (chi (X,C)) (#) (chi (Y,C)) = chi ((X /\ Y),C) by A1, PARTFUN1:5; ::_thesis: verum
end;
theorem Th70: :: RFUNCT_1:70
for Y being set
for f being real-valued Function holds
( f | Y is bounded_above iff ex r being real number st
for c being set st c in Y /\ (dom f) holds
f . c <= r )
proof
let Y be set ; ::_thesis: for f being real-valued Function holds
( f | Y is bounded_above iff ex r being real number st
for c being set st c in Y /\ (dom f) holds
f . c <= r )
let f be real-valued Function; ::_thesis: ( f | Y is bounded_above iff ex r being real number st
for c being set st c in Y /\ (dom f) holds
f . c <= r )
thus ( f | Y is bounded_above implies ex r being real number st
for c being set st c in Y /\ (dom f) holds
f . c <= r ) ::_thesis: ( ex r being real number st
for c being set st c in Y /\ (dom f) holds
f . c <= r implies f | Y is bounded_above )
proof
given r being real number such that A1: for p being set st p in dom (f | Y) holds
(f | Y) . p < r ; :: according to SEQ_2:def_1 ::_thesis: ex r being real number st
for c being set st c in Y /\ (dom f) holds
f . c <= r
take r ; ::_thesis: for c being set st c in Y /\ (dom f) holds
f . c <= r
let c be set ; ::_thesis: ( c in Y /\ (dom f) implies f . c <= r )
assume c in Y /\ (dom f) ; ::_thesis: f . c <= r
then A2: c in dom (f | Y) by RELAT_1:61;
then (f | Y) . c < r by A1;
hence f . c <= r by A2, FUNCT_1:47; ::_thesis: verum
end;
given r being real number such that A3: for c being set st c in Y /\ (dom f) holds
f . c <= r ; ::_thesis: f | Y is bounded_above
reconsider r1 = r + 1 as real number ;
take r1 ; :: according to SEQ_2:def_1 ::_thesis: for b1 being set holds
( not b1 in dom (f | Y) or not r1 <= K260((f | Y),b1) )
let p be set ; ::_thesis: ( not p in dom (f | Y) or not r1 <= K260((f | Y),p) )
assume A4: p in dom (f | Y) ; ::_thesis: not r1 <= K260((f | Y),p)
then p in Y /\ (dom f) by RELAT_1:61;
then f . p <= r by A3;
then A5: (f | Y) . p <= r by A4, FUNCT_1:47;
r < r1 by XREAL_1:29;
hence not r1 <= K260((f | Y),p) by A5, XXREAL_0:2; ::_thesis: verum
end;
theorem Th71: :: RFUNCT_1:71
for Y being set
for f being real-valued Function holds
( f | Y is bounded_below iff ex r being real number st
for c being set st c in Y /\ (dom f) holds
r <= f . c )
proof
let Y be set ; ::_thesis: for f being real-valued Function holds
( f | Y is bounded_below iff ex r being real number st
for c being set st c in Y /\ (dom f) holds
r <= f . c )
let f be real-valued Function; ::_thesis: ( f | Y is bounded_below iff ex r being real number st
for c being set st c in Y /\ (dom f) holds
r <= f . c )
thus ( f | Y is bounded_below implies ex r being real number st
for c being set st c in Y /\ (dom f) holds
r <= f . c ) ::_thesis: ( ex r being real number st
for c being set st c in Y /\ (dom f) holds
r <= f . c implies f | Y is bounded_below )
proof
given r being real number such that A1: for p being set st p in dom (f | Y) holds
r < (f | Y) . p ; :: according to SEQ_2:def_2 ::_thesis: ex r being real number st
for c being set st c in Y /\ (dom f) holds
r <= f . c
take r ; ::_thesis: for c being set st c in Y /\ (dom f) holds
r <= f . c
let c be set ; ::_thesis: ( c in Y /\ (dom f) implies r <= f . c )
assume c in Y /\ (dom f) ; ::_thesis: r <= f . c
then A2: c in dom (f | Y) by RELAT_1:61;
then r < (f | Y) . c by A1;
hence r <= f . c by A2, FUNCT_1:47; ::_thesis: verum
end;
given r being real number such that A3: for c being set st c in Y /\ (dom f) holds
r <= f . c ; ::_thesis: f | Y is bounded_below
reconsider r1 = r - 1 as real number ;
take r1 ; :: according to SEQ_2:def_2 ::_thesis: for b1 being set holds
( not b1 in dom (f | Y) or not K260((f | Y),b1) <= r1 )
let p be set ; ::_thesis: ( not p in dom (f | Y) or not K260((f | Y),p) <= r1 )
assume A4: p in dom (f | Y) ; ::_thesis: not K260((f | Y),p) <= r1
then p in Y /\ (dom f) by RELAT_1:61;
then r <= f . p by A3;
then A5: r <= (f | Y) . p by A4, FUNCT_1:47;
r1 < r by XREAL_1:44;
hence not K260((f | Y),p) <= r1 by A5, XXREAL_0:2; ::_thesis: verum
end;
theorem Th72: :: RFUNCT_1:72
for f being real-valued Function holds
( f is bounded iff ex r being real number st
for c being set st c in dom f holds
abs (f . c) <= r )
proof
let f be real-valued Function; ::_thesis: ( f is bounded iff ex r being real number st
for c being set st c in dom f holds
abs (f . c) <= r )
thus ( f is bounded implies ex r being real number st
for c being set st c in dom f holds
abs (f . c) <= r ) ::_thesis: ( ex r being real number st
for c being set st c in dom f holds
abs (f . c) <= r implies f is bounded )
proof
assume A1: f is bounded ; ::_thesis: ex r being real number st
for c being set st c in dom f holds
abs (f . c) <= r
then consider r1 being real number such that
A2: for c being set st c in dom f holds
f . c < r1 by SEQ_2:def_1;
consider r2 being real number such that
A3: for c being set st c in dom f holds
r2 < f . c by A1, SEQ_2:def_2;
take g = (abs r1) + (abs r2); ::_thesis: for c being set st c in dom f holds
abs (f . c) <= g
let c be set ; ::_thesis: ( c in dom f implies abs (f . c) <= g )
assume A4: c in dom f ; ::_thesis: abs (f . c) <= g
A5: 0 <= abs r2 by COMPLEX1:46;
r1 <= abs r1 by ABSVALUE:4;
then f . c <= abs r1 by A2, A4, XXREAL_0:2;
then A6: (f . c) + 0 <= (abs r1) + (abs r2) by A5, XREAL_1:7;
A7: 0 <= abs r1 by COMPLEX1:46;
- (abs r2) <= r2 by ABSVALUE:4;
then - (abs r2) <= f . c by A3, A4, XXREAL_0:2;
then A8: (- (abs r1)) + (- (abs r2)) <= 0 + (f . c) by A7, XREAL_1:7;
(- (abs r1)) + (- (abs r2)) = - g ;
hence abs (f . c) <= g by A6, A8, ABSVALUE:5; ::_thesis: verum
end;
given r being real number such that A9: for c being set st c in dom f holds
abs (f . c) <= r ; ::_thesis: f is bounded
thus f is bounded_above :: according to SEQ_2:def_8 ::_thesis: f is bounded_below
proof
take r + 1 ; :: according to SEQ_2:def_1 ::_thesis: for b1 being set holds
( not b1 in dom f or not r + 1 <= K260(f,b1) )
let c be set ; ::_thesis: ( not c in dom f or not r + 1 <= K260(f,c) )
assume c in dom f ; ::_thesis: not r + 1 <= K260(f,c)
then A10: abs (f . c) < r + 1 by A9, XREAL_1:39;
f . c <= abs (f . c) by ABSVALUE:4;
hence not r + 1 <= K260(f,c) by A10, XXREAL_0:2; ::_thesis: verum
end;
take - (r + 1) ; :: according to SEQ_2:def_2 ::_thesis: for b1 being set holds
( not b1 in dom f or not K260(f,b1) <= - (r + 1) )
let c be set ; ::_thesis: ( not c in dom f or not K260(f,c) <= - (r + 1) )
assume c in dom f ; ::_thesis: not K260(f,c) <= - (r + 1)
then abs (f . c) < r + 1 by A9, XREAL_1:39;
then A11: - (r + 1) < - (abs (f . c)) by XREAL_1:24;
- (abs (f . c)) <= f . c by ABSVALUE:4;
hence not K260(f,c) <= - (r + 1) by A11, XXREAL_0:2; ::_thesis: verum
end;
theorem :: RFUNCT_1:73
for Y being set
for f being real-valued Function holds
( f | Y is bounded iff ex r being real number st
for c being set st c in Y /\ (dom f) holds
abs (f . c) <= r )
proof
let Y be set ; ::_thesis: for f being real-valued Function holds
( f | Y is bounded iff ex r being real number st
for c being set st c in Y /\ (dom f) holds
abs (f . c) <= r )
let f be real-valued Function; ::_thesis: ( f | Y is bounded iff ex r being real number st
for c being set st c in Y /\ (dom f) holds
abs (f . c) <= r )
thus ( f | Y is bounded implies ex r being real number st
for c being set st c in Y /\ (dom f) holds
abs (f . c) <= r ) ::_thesis: ( ex r being real number st
for c being set st c in Y /\ (dom f) holds
abs (f . c) <= r implies f | Y is bounded )
proof
assume A1: f | Y is bounded ; ::_thesis: ex r being real number st
for c being set st c in Y /\ (dom f) holds
abs (f . c) <= r
then consider r1 being real number such that
A2: for c being set st c in Y /\ (dom f) holds
f . c <= r1 by Th70;
consider r2 being real number such that
A3: for c being set st c in Y /\ (dom f) holds
r2 <= f . c by A1, Th71;
take g = (abs r1) + (abs r2); ::_thesis: for c being set st c in Y /\ (dom f) holds
abs (f . c) <= g
A4: r1 <= abs r1 by ABSVALUE:4;
let c be set ; ::_thesis: ( c in Y /\ (dom f) implies abs (f . c) <= g )
assume A5: c in Y /\ (dom f) ; ::_thesis: abs (f . c) <= g
f . c <= r1 by A2, A5;
then A6: f . c <= abs r1 by A4, XXREAL_0:2;
A7: - (abs r2) <= r2 by ABSVALUE:4;
r2 <= f . c by A3, A5;
then A8: - (abs r2) <= f . c by A7, XXREAL_0:2;
0 <= abs r1 by COMPLEX1:46;
then A9: (- (abs r1)) + (- (abs r2)) <= 0 + (f . c) by A8, XREAL_1:7;
0 <= abs r2 by COMPLEX1:46;
then A10: (f . c) + 0 <= (abs r1) + (abs r2) by A6, XREAL_1:7;
(- (abs r1)) + (- (abs r2)) = - g ;
hence abs (f . c) <= g by A10, A9, ABSVALUE:5; ::_thesis: verum
end;
given r being real number such that A11: for c being set st c in Y /\ (dom f) holds
abs (f . c) <= r ; ::_thesis: f | Y is bounded
now__::_thesis:_for_c_being_set_st_c_in_Y_/\_(dom_f)_holds_
-_r_<=_f_._c
let c be set ; ::_thesis: ( c in Y /\ (dom f) implies - r <= f . c )
assume c in Y /\ (dom f) ; ::_thesis: - r <= f . c
then abs (f . c) <= r by A11;
then A12: - r <= - (abs (f . c)) by XREAL_1:24;
- (abs (f . c)) <= f . c by ABSVALUE:4;
hence - r <= f . c by A12, XXREAL_0:2; ::_thesis: verum
end;
then A13: f | Y is bounded_below by Th71;
now__::_thesis:_for_c_being_set_st_c_in_Y_/\_(dom_f)_holds_
f_._c_<=_r
let c be set ; ::_thesis: ( c in Y /\ (dom f) implies f . c <= r )
assume c in Y /\ (dom f) ; ::_thesis: f . c <= r
then A14: abs (f . c) <= r by A11;
f . c <= abs (f . c) by ABSVALUE:4;
hence f . c <= r by A14, XXREAL_0:2; ::_thesis: verum
end;
then f | Y is bounded_above by Th70;
hence f | Y is bounded by A13; ::_thesis: verum
end;
theorem :: RFUNCT_1:74
for Y, X being set
for f being real-valued Function holds
( ( Y c= X & f | X is bounded_above implies f | Y is bounded_above ) & ( Y c= X & f | X is bounded_below implies f | Y is bounded_below ) & ( Y c= X & f | X is bounded implies f | Y is bounded ) )
proof
let Y, X be set ; ::_thesis: for f being real-valued Function holds
( ( Y c= X & f | X is bounded_above implies f | Y is bounded_above ) & ( Y c= X & f | X is bounded_below implies f | Y is bounded_below ) & ( Y c= X & f | X is bounded implies f | Y is bounded ) )
let f be real-valued Function; ::_thesis: ( ( Y c= X & f | X is bounded_above implies f | Y is bounded_above ) & ( Y c= X & f | X is bounded_below implies f | Y is bounded_below ) & ( Y c= X & f | X is bounded implies f | Y is bounded ) )
thus A1: ( Y c= X & f | X is bounded_above implies f | Y is bounded_above ) ::_thesis: ( ( Y c= X & f | X is bounded_below implies f | Y is bounded_below ) & ( Y c= X & f | X is bounded implies f | Y is bounded ) )
proof
assume that
A2: Y c= X and
A3: f | X is bounded_above ; ::_thesis: f | Y is bounded_above
consider r being real number such that
A4: for c being set st c in X /\ (dom f) holds
f . c <= r by A3, Th70;
now__::_thesis:_ex_r_being_real_number_st_
for_c_being_set_st_c_in_Y_/\_(dom_f)_holds_
f_._c_<=_r
take r = r; ::_thesis: for c being set st c in Y /\ (dom f) holds
f . c <= r
let c be set ; ::_thesis: ( c in Y /\ (dom f) implies f . c <= r )
assume A5: c in Y /\ (dom f) ; ::_thesis: f . c <= r
then A6: c in dom f by XBOOLE_0:def_4;
c in Y by A5, XBOOLE_0:def_4;
then c in X /\ (dom f) by A2, A6, XBOOLE_0:def_4;
hence f . c <= r by A4; ::_thesis: verum
end;
hence f | Y is bounded_above by Th70; ::_thesis: verum
end;
thus A7: ( Y c= X & f | X is bounded_below implies f | Y is bounded_below ) ::_thesis: ( Y c= X & f | X is bounded implies f | Y is bounded )
proof
assume that
A8: Y c= X and
A9: f | X is bounded_below ; ::_thesis: f | Y is bounded_below
consider r being real number such that
A10: for c being set st c in X /\ (dom f) holds
r <= f . c by A9, Th71;
now__::_thesis:_ex_r_being_real_number_st_
for_c_being_set_st_c_in_Y_/\_(dom_f)_holds_
r_<=_f_._c
take r = r; ::_thesis: for c being set st c in Y /\ (dom f) holds
r <= f . c
let c be set ; ::_thesis: ( c in Y /\ (dom f) implies r <= f . c )
assume A11: c in Y /\ (dom f) ; ::_thesis: r <= f . c
then A12: c in dom f by XBOOLE_0:def_4;
c in Y by A11, XBOOLE_0:def_4;
then c in X /\ (dom f) by A8, A12, XBOOLE_0:def_4;
hence r <= f . c by A10; ::_thesis: verum
end;
hence f | Y is bounded_below by Th71; ::_thesis: verum
end;
assume that
A13: Y c= X and
A14: f | X is bounded ; ::_thesis: f | Y is bounded
thus f | Y is bounded by A1, A7, A13, A14; ::_thesis: verum
end;
theorem :: RFUNCT_1:75
for X, Y being set
for f being real-valued Function st f | X is bounded_above & f | Y is bounded_below holds
f | (X /\ Y) is bounded
proof
let X, Y be set ; ::_thesis: for f being real-valued Function st f | X is bounded_above & f | Y is bounded_below holds
f | (X /\ Y) is bounded
let f be real-valued Function; ::_thesis: ( f | X is bounded_above & f | Y is bounded_below implies f | (X /\ Y) is bounded )
assume that
A1: f | X is bounded_above and
A2: f | Y is bounded_below ; ::_thesis: f | (X /\ Y) is bounded
consider r1 being real number such that
A3: for c being set st c in X /\ (dom f) holds
f . c <= r1 by A1, Th70;
now__::_thesis:_for_c_being_set_st_c_in_(X_/\_Y)_/\_(dom_f)_holds_
f_._c_<=_r1
let c be set ; ::_thesis: ( c in (X /\ Y) /\ (dom f) implies f . c <= r1 )
assume A4: c in (X /\ Y) /\ (dom f) ; ::_thesis: f . c <= r1
then c in X /\ Y by XBOOLE_0:def_4;
then A5: c in X by XBOOLE_0:def_4;
c in dom f by A4, XBOOLE_0:def_4;
then c in X /\ (dom f) by A5, XBOOLE_0:def_4;
hence f . c <= r1 by A3; ::_thesis: verum
end;
hence f | (X /\ Y) is bounded_above by Th70; :: according to SEQ_2:def_8 ::_thesis: f | (X /\ Y) is bounded_below
consider r2 being real number such that
A6: for c being set st c in Y /\ (dom f) holds
r2 <= f . c by A2, Th71;
now__::_thesis:_for_c_being_set_st_c_in_(X_/\_Y)_/\_(dom_f)_holds_
r2_<=_f_._c
let c be set ; ::_thesis: ( c in (X /\ Y) /\ (dom f) implies r2 <= f . c )
assume A7: c in (X /\ Y) /\ (dom f) ; ::_thesis: r2 <= f . c
then c in X /\ Y by XBOOLE_0:def_4;
then A8: c in Y by XBOOLE_0:def_4;
c in dom f by A7, XBOOLE_0:def_4;
then c in Y /\ (dom f) by A8, XBOOLE_0:def_4;
hence r2 <= f . c by A6; ::_thesis: verum
end;
hence f | (X /\ Y) is bounded_below by Th71; ::_thesis: verum
end;
registration
cluster Relation-like Function-like constant real-valued -> real-valued bounded for set ;
coherence
for b1 being real-valued Function st b1 is constant holds
b1 is bounded
proof
let f be real-valued Function; ::_thesis: ( f is constant implies f is bounded )
percases ( f is empty or not f is empty ) ;
supposeA1: f is empty ; ::_thesis: ( f is constant implies f is bounded )
reconsider z = 0 as real number ;
assume f is constant ; ::_thesis: f is bounded
thus f is bounded_above :: according to SEQ_2:def_8 ::_thesis: f is bounded_below
proof
take z ; :: according to SEQ_2:def_1 ::_thesis: for b1 being set holds
( not b1 in dom f or not z <= K260(f,b1) )
let x be set ; ::_thesis: ( not x in dom f or not z <= K260(f,x) )
thus ( not x in dom f or not z <= K260(f,x) ) by A1; ::_thesis: verum
end;
take z ; :: according to SEQ_2:def_2 ::_thesis: for b1 being set holds
( not b1 in dom f or not K260(f,b1) <= z )
let x be set ; ::_thesis: ( not x in dom f or not K260(f,x) <= z )
thus ( not x in dom f or not K260(f,x) <= z ) by A1; ::_thesis: verum
end;
supposeA2: not f is empty ; ::_thesis: ( f is constant implies f is bounded )
assume f is constant ; ::_thesis: f is bounded
then consider r being real number such that
A3: for c being set st c in dom f holds
f . c = r by A2, VALUED_0:15;
thus f is bounded_above :: according to SEQ_2:def_8 ::_thesis: f is bounded_below
proof
take r + 1 ; :: according to SEQ_2:def_1 ::_thesis: for b1 being set holds
( not b1 in dom f or not r + 1 <= K260(f,b1) )
let y be set ; ::_thesis: ( not y in dom f or not r + 1 <= K260(f,y) )
assume y in dom f ; ::_thesis: not r + 1 <= K260(f,y)
then f . y = r by A3;
hence not r + 1 <= K260(f,y) by XREAL_1:39; ::_thesis: verum
end;
take r - 1 ; :: according to SEQ_2:def_2 ::_thesis: for b1 being set holds
( not b1 in dom f or not K260(f,b1) <= r - 1 )
let y be set ; ::_thesis: ( not y in dom f or not K260(f,y) <= r - 1 )
assume y in dom f ; ::_thesis: not K260(f,y) <= r - 1
then f . y = r by A3;
hence not K260(f,y) <= r - 1 by XREAL_1:231; ::_thesis: verum
end;
end;
end;
end;
theorem :: RFUNCT_1:76
for X being set
for f being real-valued Function st X misses dom f holds
f | X is bounded
proof
let X be set ; ::_thesis: for f being real-valued Function st X misses dom f holds
f | X is bounded
let f be real-valued Function; ::_thesis: ( X misses dom f implies f | X is bounded )
assume X /\ (dom f) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: f | X is bounded
then dom (f | X) = {} by RELAT_1:61;
then f | X = {} ;
hence f | X is bounded ; ::_thesis: verum
end;
theorem :: RFUNCT_1:77
for Y being set
for f being real-valued Function holds (0 (#) f) | Y is bounded
proof
let Y be set ; ::_thesis: for f being real-valued Function holds (0 (#) f) | Y is bounded
let f be real-valued Function; ::_thesis: (0 (#) f) | Y is bounded
reconsider p1 = 0 as Real ;
set r = 0 ;
now__::_thesis:_ex_p_being_Real_st_
for_c_being_set_st_c_in_Y_/\_(dom_(0_(#)_f))_holds_
(0_(#)_f)_._c_<=_p
take p = p1; ::_thesis: for c being set st c in Y /\ (dom (0 (#) f)) holds
(0 (#) f) . c <= p
let c be set ; ::_thesis: ( c in Y /\ (dom (0 (#) f)) implies (0 (#) f) . c <= p )
assume c in Y /\ (dom (0 (#) f)) ; ::_thesis: (0 (#) f) . c <= p
then A1: c in dom (0 (#) f) by XBOOLE_0:def_4;
0 * (f . c) <= 0 ;
hence (0 (#) f) . c <= p by A1, VALUED_1:def_5; ::_thesis: verum
end;
hence (0 (#) f) | Y is bounded_above by Th70; :: according to SEQ_2:def_8 ::_thesis: (0 (#) f) | Y is bounded_below
now__::_thesis:_ex_p_being_Real_st_
for_c_being_set_st_c_in_Y_/\_(dom_(0_(#)_f))_holds_
p_<=_(0_(#)_f)_._c
take p = p1; ::_thesis: for c being set st c in Y /\ (dom (0 (#) f)) holds
p <= (0 (#) f) . c
let c be set ; ::_thesis: ( c in Y /\ (dom (0 (#) f)) implies p <= (0 (#) f) . c )
assume c in Y /\ (dom (0 (#) f)) ; ::_thesis: p <= (0 (#) f) . c
then A2: c in dom (0 (#) f) by XBOOLE_0:def_4;
0 <= 0 * (f . c) ;
hence p <= (0 (#) f) . c by A2, VALUED_1:def_5; ::_thesis: verum
end;
hence (0 (#) f) | Y is bounded_below by Th71; ::_thesis: verum
end;
registration
let f be real-valued bounded_above Function;
let X be set ;
clusterf | X -> real-valued bounded_above for real-valued Function;
coherence
for b1 being real-valued Function st b1 = f | X holds
b1 is bounded_above
proof
consider r being real number such that
A1: for y being set st y in dom f holds
f . y < r by SEQ_2:def_1;
f | X is bounded_above
proof
take r ; :: according to SEQ_2:def_1 ::_thesis: for b1 being set holds
( not b1 in dom (f | X) or not r <= K260((f | X),b1) )
let y be set ; ::_thesis: ( not y in dom (f | X) or not r <= K260((f | X),y) )
assume A2: y in dom (f | X) ; ::_thesis: not r <= K260((f | X),y)
then y in dom f by RELAT_1:57;
then f . y < r by A1;
hence not r <= K260((f | X),y) by A2, FUNCT_1:47; ::_thesis: verum
end;
hence for b1 being real-valued Function st b1 = f | X holds
b1 is bounded_above ; ::_thesis: verum
end;
end;
registration
let f be real-valued bounded_below Function;
let X be set ;
clusterf | X -> real-valued bounded_below for real-valued Function;
coherence
for b1 being real-valued Function st b1 = f | X holds
b1 is bounded_below
proof
consider r being real number such that
A1: for y being set st y in dom f holds
r < f . y by SEQ_2:def_2;
f | X is bounded_below
proof
take r ; :: according to SEQ_2:def_2 ::_thesis: for b1 being set holds
( not b1 in dom (f | X) or not K260((f | X),b1) <= r )
let y be set ; ::_thesis: ( not y in dom (f | X) or not K260((f | X),y) <= r )
assume A2: y in dom (f | X) ; ::_thesis: not K260((f | X),y) <= r
then y in dom f by RELAT_1:57;
then r < f . y by A1;
hence not K260((f | X),y) <= r by A2, FUNCT_1:47; ::_thesis: verum
end;
hence for b1 being real-valued Function st b1 = f | X holds
b1 is bounded_below ; ::_thesis: verum
end;
end;
registration
let f be real-valued bounded_above Function;
let r be non negative real number ;
clusterr (#) f -> real-valued bounded_above for real-valued Function;
coherence
for b1 being real-valued Function st b1 = r (#) f holds
b1 is bounded_above
proof
consider r1 being real number such that
A1: for c being set st c in dom f holds
f . c < r1 by SEQ_2:def_1;
now__::_thesis:_ex_p_being_Element_of_REAL_st_
for_c_being_set_st_c_in_dom_(r_(#)_f)_holds_
(r_(#)_f)_._c_<_p
take p = (r * (abs r1)) + 1; ::_thesis: for c being set st c in dom (r (#) f) holds
(r (#) f) . c < p
let c be set ; ::_thesis: ( c in dom (r (#) f) implies (r (#) f) . c < p )
A2: r1 <= abs r1 by ABSVALUE:4;
assume A3: c in dom (r (#) f) ; ::_thesis: (r (#) f) . c < p
then c in dom f by VALUED_1:def_5;
then f . c < abs r1 by A1, A2, XXREAL_0:2;
then r * (f . c) <= (abs r1) * r by XREAL_1:64;
then (r (#) f) . c <= (abs r1) * r by A3, VALUED_1:def_5;
hence (r (#) f) . c < p by XREAL_1:39; ::_thesis: verum
end;
hence for b1 being real-valued Function st b1 = r (#) f holds
b1 is bounded_above by SEQ_2:def_1; ::_thesis: verum
end;
end;
registration
let f be real-valued bounded_below Function;
let r be non negative real number ;
clusterr (#) f -> real-valued bounded_below for real-valued Function;
coherence
for b1 being real-valued Function st b1 = r (#) f holds
b1 is bounded_below
proof
consider r1 being real number such that
A1: for c being set st c in dom f holds
r1 < f . c by SEQ_2:def_2;
now__::_thesis:_ex_p_being_Element_of_REAL_st_
for_c_being_set_st_c_in_dom_(r_(#)_f)_holds_
(r_(#)_f)_._c_>_p
take p = (r * (- (abs r1))) - 1; ::_thesis: for c being set st c in dom (r (#) f) holds
(r (#) f) . c > p
let c be set ; ::_thesis: ( c in dom (r (#) f) implies (r (#) f) . c > p )
A2: - (abs r1) <= r1 by ABSVALUE:4;
assume A3: c in dom (r (#) f) ; ::_thesis: (r (#) f) . c > p
then c in dom f by VALUED_1:def_5;
then f . c >= - (abs r1) by A1, A2, XXREAL_0:2;
then r * (f . c) >= (- (abs r1)) * r by XREAL_1:64;
then (r (#) f) . c >= (- (abs r1)) * r by A3, VALUED_1:def_5;
hence (r (#) f) . c > p by XREAL_1:231; ::_thesis: verum
end;
hence for b1 being real-valued Function st b1 = r (#) f holds
b1 is bounded_below by SEQ_2:def_2; ::_thesis: verum
end;
end;
registration
let f be real-valued bounded_above Function;
let r be non positive real number ;
clusterr (#) f -> real-valued bounded_below for real-valued Function;
coherence
for b1 being real-valued Function st b1 = r (#) f holds
b1 is bounded_below
proof
consider r1 being real number such that
A1: for c being set st c in dom f holds
f . c < r1 by SEQ_2:def_1;
now__::_thesis:_ex_p_being_Element_of_REAL_st_
for_c_being_set_st_c_in_dom_(r_(#)_f)_holds_
p_<_(r_(#)_f)_._c
take p = (r * (abs r1)) - 1; ::_thesis: for c being set st c in dom (r (#) f) holds
p < (r (#) f) . c
let c be set ; ::_thesis: ( c in dom (r (#) f) implies p < (r (#) f) . c )
A2: r1 <= abs r1 by ABSVALUE:4;
assume A3: c in dom (r (#) f) ; ::_thesis: p < (r (#) f) . c
then c in dom f by VALUED_1:def_5;
then f . c <= abs r1 by A1, A2, XXREAL_0:2;
then r * (abs r1) <= r * (f . c) by XREAL_1:65;
then r * (abs r1) <= (r (#) f) . c by A3, VALUED_1:def_5;
hence p < (r (#) f) . c by XREAL_1:231; ::_thesis: verum
end;
hence for b1 being real-valued Function st b1 = r (#) f holds
b1 is bounded_below by SEQ_2:def_2; ::_thesis: verum
end;
end;
registration
let f be real-valued bounded_below Function;
let r be non positive real number ;
clusterr (#) f -> real-valued bounded_above for real-valued Function;
coherence
for b1 being real-valued Function st b1 = r (#) f holds
b1 is bounded_above
proof
consider r1 being real number such that
A1: for c being set st c in dom f holds
r1 < f . c by SEQ_2:def_2;
now__::_thesis:_ex_p_being_Element_of_REAL_st_
for_c_being_set_st_c_in_dom_(r_(#)_f)_holds_
(r_(#)_f)_._c_<_p
take p = (r * (- (abs r1))) + 1; ::_thesis: for c being set st c in dom (r (#) f) holds
(r (#) f) . c < p
let c be set ; ::_thesis: ( c in dom (r (#) f) implies (r (#) f) . c < p )
A2: - (abs r1) <= r1 by ABSVALUE:4;
assume A3: c in dom (r (#) f) ; ::_thesis: (r (#) f) . c < p
then c in dom f by VALUED_1:def_5;
then - (abs r1) <= f . c by A1, A2, XXREAL_0:2;
then r * (f . c) <= r * (- (abs r1)) by XREAL_1:65;
then (r (#) f) . c <= r * (- (abs r1)) by A3, VALUED_1:def_5;
hence (r (#) f) . c < p by XREAL_1:39; ::_thesis: verum
end;
hence for b1 being real-valued Function st b1 = r (#) f holds
b1 is bounded_above by SEQ_2:def_1; ::_thesis: verum
end;
end;
theorem Th78: :: RFUNCT_1:78
for Y being set
for r being real number
for f being real-valued Function holds
( ( f | Y is bounded_above & 0 <= r implies (r (#) f) | Y is bounded_above ) & ( f | Y is bounded_above & r <= 0 implies (r (#) f) | Y is bounded_below ) )
proof
let Y be set ; ::_thesis: for r being real number
for f being real-valued Function holds
( ( f | Y is bounded_above & 0 <= r implies (r (#) f) | Y is bounded_above ) & ( f | Y is bounded_above & r <= 0 implies (r (#) f) | Y is bounded_below ) )
let r be real number ; ::_thesis: for f being real-valued Function holds
( ( f | Y is bounded_above & 0 <= r implies (r (#) f) | Y is bounded_above ) & ( f | Y is bounded_above & r <= 0 implies (r (#) f) | Y is bounded_below ) )
let f be real-valued Function; ::_thesis: ( ( f | Y is bounded_above & 0 <= r implies (r (#) f) | Y is bounded_above ) & ( f | Y is bounded_above & r <= 0 implies (r (#) f) | Y is bounded_below ) )
(r (#) f) | Y = r (#) (f | Y) by Th49;
hence ( ( f | Y is bounded_above & 0 <= r implies (r (#) f) | Y is bounded_above ) & ( f | Y is bounded_above & r <= 0 implies (r (#) f) | Y is bounded_below ) ) ; ::_thesis: verum
end;
theorem Th79: :: RFUNCT_1:79
for Y being set
for r being real number
for f being real-valued Function holds
( ( f | Y is bounded_below & 0 <= r implies (r (#) f) | Y is bounded_below ) & ( f | Y is bounded_below & r <= 0 implies (r (#) f) | Y is bounded_above ) )
proof
let Y be set ; ::_thesis: for r being real number
for f being real-valued Function holds
( ( f | Y is bounded_below & 0 <= r implies (r (#) f) | Y is bounded_below ) & ( f | Y is bounded_below & r <= 0 implies (r (#) f) | Y is bounded_above ) )
let r be real number ; ::_thesis: for f being real-valued Function holds
( ( f | Y is bounded_below & 0 <= r implies (r (#) f) | Y is bounded_below ) & ( f | Y is bounded_below & r <= 0 implies (r (#) f) | Y is bounded_above ) )
let f be real-valued Function; ::_thesis: ( ( f | Y is bounded_below & 0 <= r implies (r (#) f) | Y is bounded_below ) & ( f | Y is bounded_below & r <= 0 implies (r (#) f) | Y is bounded_above ) )
(r (#) f) | Y = r (#) (f | Y) by Th49;
hence ( ( f | Y is bounded_below & 0 <= r implies (r (#) f) | Y is bounded_below ) & ( f | Y is bounded_below & r <= 0 implies (r (#) f) | Y is bounded_above ) ) ; ::_thesis: verum
end;
theorem Th80: :: RFUNCT_1:80
for Y being set
for r being real number
for f being real-valued Function st f | Y is bounded holds
(r (#) f) | Y is bounded
proof
let Y be set ; ::_thesis: for r being real number
for f being real-valued Function st f | Y is bounded holds
(r (#) f) | Y is bounded
let r be real number ; ::_thesis: for f being real-valued Function st f | Y is bounded holds
(r (#) f) | Y is bounded
let f be real-valued Function; ::_thesis: ( f | Y is bounded implies (r (#) f) | Y is bounded )
assume A1: f | Y is bounded ; ::_thesis: (r (#) f) | Y is bounded
percases ( 0 <= r or r <= 0 ) ;
supposeA2: 0 <= r ; ::_thesis: (r (#) f) | Y is bounded
hence (r (#) f) | Y is bounded_above by A1, Th78; :: according to SEQ_2:def_8 ::_thesis: (r (#) f) | Y is bounded_below
thus (r (#) f) | Y is bounded_below by A1, A2, Th79; ::_thesis: verum
end;
supposeA3: r <= 0 ; ::_thesis: (r (#) f) | Y is bounded
hence (r (#) f) | Y is bounded_above by A1, Th79; :: according to SEQ_2:def_8 ::_thesis: (r (#) f) | Y is bounded_below
thus (r (#) f) | Y is bounded_below by A1, A3, Th78; ::_thesis: verum
end;
end;
end;
registration
let f be real-valued Function;
cluster|.f.| -> bounded_below ;
coherence
abs f is bounded_below
proof
now__::_thesis:_ex_p_being_real_number_st_
for_c_being_set_st_c_in_dom_(abs_f)_holds_
p_<_(abs_f)_._c
reconsider p = - 1 as real number ;
take p = p; ::_thesis: for c being set st c in dom (abs f) holds
p < (abs f) . c
let c be set ; ::_thesis: ( c in dom (abs f) implies p < (abs f) . c )
assume c in dom (abs f) ; ::_thesis: p < (abs f) . c
0 <= abs (f . c) by COMPLEX1:46;
hence p < (abs f) . c by VALUED_1:18; ::_thesis: verum
end;
hence abs f is bounded_below by SEQ_2:def_2; ::_thesis: verum
end;
end;
theorem :: RFUNCT_1:81
for X being set
for f being real-valued Function holds (abs f) | X is bounded_below ;
registration
let f be real-valued bounded Function;
cluster|.f.| -> real-valued bounded for real-valued Function;
coherence
for b1 being real-valued Function st b1 = abs f holds
b1 is bounded
proof
consider r1 being real number such that
A1: for c being set st c in dom f holds
abs (f . c) <= r1 by Th72;
now__::_thesis:_ex_r1_being_real_number_st_
for_c_being_set_st_c_in_dom_(abs_f)_holds_
abs_((abs_f)_._c)_<=_r1
take r1 = r1; ::_thesis: for c being set st c in dom (abs f) holds
abs ((abs f) . c) <= r1
let c be set ; ::_thesis: ( c in dom (abs f) implies abs ((abs f) . c) <= r1 )
assume c in dom (abs f) ; ::_thesis: abs ((abs f) . c) <= r1
then c in dom f by VALUED_1:def_11;
then abs (abs (f . c)) <= r1 by A1;
hence abs ((abs f) . c) <= r1 by VALUED_1:18; ::_thesis: verum
end;
hence for b1 being real-valued Function st b1 = abs f holds
b1 is bounded by Th72; ::_thesis: verum
end;
end;
registration
let f be real-valued bounded_above Function;
cluster - f -> real-valued bounded_below for real-valued Function;
coherence
for b1 being real-valued Function st b1 = - f holds
b1 is bounded_below ;
end;
theorem Th82: :: RFUNCT_1:82
for Y being set
for f being real-valued Function st f | Y is bounded holds
( (abs f) | Y is bounded & (- f) | Y is bounded )
proof
let Y be set ; ::_thesis: for f being real-valued Function st f | Y is bounded holds
( (abs f) | Y is bounded & (- f) | Y is bounded )
let f be real-valued Function; ::_thesis: ( f | Y is bounded implies ( (abs f) | Y is bounded & (- f) | Y is bounded ) )
assume A1: f | Y is bounded ; ::_thesis: ( (abs f) | Y is bounded & (- f) | Y is bounded )
(abs f) | Y = abs (f | Y) by Th46;
hence (abs f) | Y is bounded by A1; ::_thesis: (- f) | Y is bounded
thus (- f) | Y is bounded by A1, Th80; ::_thesis: verum
end;
registration
let f1, f2 be real-valued bounded_above Function;
clusterf1 + f2 -> real-valued bounded_above for real-valued Function;
coherence
for b1 being real-valued Function st b1 = f1 + f2 holds
b1 is bounded_above
proof
consider r2 being real number such that
A1: for c being set st c in dom f2 holds
f2 . c < r2 by SEQ_2:def_1;
consider r1 being real number such that
A2: for c being set st c in dom f1 holds
f1 . c < r1 by SEQ_2:def_1;
now__::_thesis:_ex_r_being_set_st_
for_c_being_set_st_c_in_dom_(f1_+_f2)_holds_
(f1_+_f2)_._c_<_r
take r = r1 + r2; ::_thesis: for c being set st c in dom (f1 + f2) holds
(f1 + f2) . c < r
let c be set ; ::_thesis: ( c in dom (f1 + f2) implies (f1 + f2) . c < r )
assume A3: c in dom (f1 + f2) ; ::_thesis: (f1 + f2) . c < r
then A4: c in (dom f1) /\ (dom f2) by VALUED_1:def_1;
then c in dom f1 by XBOOLE_0:def_4;
then A5: f1 . c < r1 by A2;
c in dom f2 by A4, XBOOLE_0:def_4;
then (f1 . c) + (f2 . c) < r by A1, A5, XREAL_1:8;
hence (f1 + f2) . c < r by A3, VALUED_1:def_1; ::_thesis: verum
end;
hence for b1 being real-valued Function st b1 = f1 + f2 holds
b1 is bounded_above by SEQ_2:def_1; ::_thesis: verum
end;
end;
registration
let f1, f2 be real-valued bounded_below Function;
clusterf1 + f2 -> real-valued bounded_below for real-valued Function;
coherence
for b1 being real-valued Function st b1 = f1 + f2 holds
b1 is bounded_below
proof
consider r2 being real number such that
A1: for c being set st c in dom f2 holds
f2 . c > r2 by SEQ_2:def_2;
consider r1 being real number such that
A2: for c being set st c in dom f1 holds
f1 . c > r1 by SEQ_2:def_2;
now__::_thesis:_ex_r_being_set_st_
for_c_being_set_st_c_in_dom_(f1_+_f2)_holds_
(f1_+_f2)_._c_>_r
take r = r1 + r2; ::_thesis: for c being set st c in dom (f1 + f2) holds
(f1 + f2) . c > r
let c be set ; ::_thesis: ( c in dom (f1 + f2) implies (f1 + f2) . c > r )
assume A3: c in dom (f1 + f2) ; ::_thesis: (f1 + f2) . c > r
then A4: c in (dom f1) /\ (dom f2) by VALUED_1:def_1;
then c in dom f1 by XBOOLE_0:def_4;
then A5: f1 . c > r1 by A2;
c in dom f2 by A4, XBOOLE_0:def_4;
then (f1 . c) + (f2 . c) > r by A1, A5, XREAL_1:8;
hence (f1 + f2) . c > r by A3, VALUED_1:def_1; ::_thesis: verum
end;
hence for b1 being real-valued Function st b1 = f1 + f2 holds
b1 is bounded_below by SEQ_2:def_2; ::_thesis: verum
end;
end;
theorem Th83: :: RFUNCT_1:83
for X, Y being set
for f1, f2 being real-valued Function holds
( ( f1 | X is bounded_above & f2 | Y is bounded_above implies (f1 + f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is bounded_below implies (f1 + f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is bounded implies (f1 + f2) | (X /\ Y) is bounded ) )
proof
let X, Y be set ; ::_thesis: for f1, f2 being real-valued Function holds
( ( f1 | X is bounded_above & f2 | Y is bounded_above implies (f1 + f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is bounded_below implies (f1 + f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is bounded implies (f1 + f2) | (X /\ Y) is bounded ) )
let f1, f2 be real-valued Function; ::_thesis: ( ( f1 | X is bounded_above & f2 | Y is bounded_above implies (f1 + f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is bounded_below implies (f1 + f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is bounded implies (f1 + f2) | (X /\ Y) is bounded ) )
(f1 + f2) | (X /\ Y) = (f1 | (X /\ Y)) + (f2 | (X /\ Y)) by Th44
.= (f1 | (X /\ Y)) + ((f2 | Y) | X) by RELAT_1:71
.= ((f1 | X) | Y) + ((f2 | Y) | X) by RELAT_1:71 ;
hence ( ( f1 | X is bounded_above & f2 | Y is bounded_above implies (f1 + f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is bounded_below implies (f1 + f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is bounded implies (f1 + f2) | (X /\ Y) is bounded ) ) ; ::_thesis: verum
end;
registration
let f1, f2 be real-valued bounded Function;
clusterf1 (#) f2 -> real-valued bounded for real-valued Function;
coherence
for b1 being real-valued Function st b1 = f1 (#) f2 holds
b1 is bounded
proof
consider r2 being real number such that
A1: for c being set st c in dom f2 holds
abs (f2 . c) <= r2 by Th72;
consider r1 being real number such that
A2: for c being set st c in dom f1 holds
abs (f1 . c) <= r1 by Th72;
now__::_thesis:_ex_r_being_set_st_
for_c_being_set_st_c_in_dom_(f1_(#)_f2)_holds_
abs_((f1_(#)_f2)_._c)_<=_r
take r = r1 * r2; ::_thesis: for c being set st c in dom (f1 (#) f2) holds
abs ((f1 (#) f2) . c) <= r
let c be set ; ::_thesis: ( c in dom (f1 (#) f2) implies abs ((f1 (#) f2) . c) <= r )
A3: 0 <= abs (f2 . c) by COMPLEX1:46;
assume c in dom (f1 (#) f2) ; ::_thesis: abs ((f1 (#) f2) . c) <= r
then A4: c in (dom f1) /\ (dom f2) by VALUED_1:def_4;
then c in dom f1 by XBOOLE_0:def_4;
then A5: abs (f1 . c) <= r1 by A2;
c in dom f2 by A4, XBOOLE_0:def_4;
then A6: abs (f2 . c) <= r2 by A1;
0 <= abs (f1 . c) by COMPLEX1:46;
then (abs (f1 . c)) * (abs (f2 . c)) <= r by A5, A6, A3, XREAL_1:66;
then abs ((f1 . c) * (f2 . c)) <= r by COMPLEX1:65;
hence abs ((f1 (#) f2) . c) <= r by VALUED_1:5; ::_thesis: verum
end;
hence for b1 being real-valued Function st b1 = f1 (#) f2 holds
b1 is bounded by Th72; ::_thesis: verum
end;
end;
theorem Th84: :: RFUNCT_1:84
for X, Y being set
for f1, f2 being real-valued Function st f1 | X is bounded & f2 | Y is bounded holds
( (f1 (#) f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded )
proof
let X, Y be set ; ::_thesis: for f1, f2 being real-valued Function st f1 | X is bounded & f2 | Y is bounded holds
( (f1 (#) f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded )
let f1, f2 be real-valued Function; ::_thesis: ( f1 | X is bounded & f2 | Y is bounded implies ( (f1 (#) f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded ) )
assume that
A1: f1 | X is bounded and
A2: f2 | Y is bounded ; ::_thesis: ( (f1 (#) f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded )
(f1 (#) f2) | (X /\ Y) = (f1 | (X /\ Y)) (#) (f2 | (X /\ Y)) by Th45
.= (f1 | (X /\ Y)) (#) ((f2 | Y) | X) by RELAT_1:71
.= ((f1 | X) | Y) (#) ((f2 | Y) | X) by RELAT_1:71 ;
hence (f1 (#) f2) | (X /\ Y) is bounded by A1, A2; ::_thesis: (f1 - f2) | (X /\ Y) is bounded
(- f2) | Y is bounded by A2, Th82;
hence (f1 - f2) | (X /\ Y) is bounded by A1, Th83; ::_thesis: verum
end;
theorem Th85: :: RFUNCT_1:85
for X, Y being set
for f being real-valued Function st f | X is bounded_above & f | Y is bounded_above holds
f | (X \/ Y) is bounded_above
proof
let X, Y be set ; ::_thesis: for f being real-valued Function st f | X is bounded_above & f | Y is bounded_above holds
f | (X \/ Y) is bounded_above
let f be real-valued Function; ::_thesis: ( f | X is bounded_above & f | Y is bounded_above implies f | (X \/ Y) is bounded_above )
assume that
A1: f | X is bounded_above and
A2: f | Y is bounded_above ; ::_thesis: f | (X \/ Y) is bounded_above
consider r1 being real number such that
A3: for c being set st c in X /\ (dom f) holds
f . c <= r1 by A1, Th70;
consider r2 being real number such that
A4: for c being set st c in Y /\ (dom f) holds
f . c <= r2 by A2, Th70;
now__::_thesis:_ex_r_being_Element_of_REAL_st_
for_c_being_set_st_c_in_(X_\/_Y)_/\_(dom_f)_holds_
f_._c_<=_r
take r = (abs r1) + (abs r2); ::_thesis: for c being set st c in (X \/ Y) /\ (dom f) holds
f . c <= r
let c be set ; ::_thesis: ( c in (X \/ Y) /\ (dom f) implies f . c <= r )
assume A5: c in (X \/ Y) /\ (dom f) ; ::_thesis: f . c <= r
then A6: c in dom f by XBOOLE_0:def_4;
A7: c in X \/ Y by A5, XBOOLE_0:def_4;
now__::_thesis:_f_._c_<=_r
percases ( c in X or c in Y ) by A7, XBOOLE_0:def_3;
suppose c in X ; ::_thesis: f . c <= r
then c in X /\ (dom f) by A6, XBOOLE_0:def_4;
then A8: f . c <= r1 by A3;
A9: 0 <= abs r2 by COMPLEX1:46;
r1 <= abs r1 by ABSVALUE:4;
then f . c <= abs r1 by A8, XXREAL_0:2;
then (f . c) + 0 <= r by A9, XREAL_1:7;
hence f . c <= r ; ::_thesis: verum
end;
suppose c in Y ; ::_thesis: f . c <= r
then c in Y /\ (dom f) by A6, XBOOLE_0:def_4;
then A10: f . c <= r2 by A4;
A11: 0 <= abs r1 by COMPLEX1:46;
r2 <= abs r2 by ABSVALUE:4;
then f . c <= abs r2 by A10, XXREAL_0:2;
then 0 + (f . c) <= r by A11, XREAL_1:7;
hence f . c <= r ; ::_thesis: verum
end;
end;
end;
hence f . c <= r ; ::_thesis: verum
end;
hence f | (X \/ Y) is bounded_above by Th70; ::_thesis: verum
end;
theorem Th86: :: RFUNCT_1:86
for X, Y being set
for f being real-valued Function st f | X is bounded_below & f | Y is bounded_below holds
f | (X \/ Y) is bounded_below
proof
let X, Y be set ; ::_thesis: for f being real-valued Function st f | X is bounded_below & f | Y is bounded_below holds
f | (X \/ Y) is bounded_below
let f be real-valued Function; ::_thesis: ( f | X is bounded_below & f | Y is bounded_below implies f | (X \/ Y) is bounded_below )
assume that
A1: f | X is bounded_below and
A2: f | Y is bounded_below ; ::_thesis: f | (X \/ Y) is bounded_below
consider r1 being real number such that
A3: for c being set st c in X /\ (dom f) holds
r1 <= f . c by A1, Th71;
consider r2 being real number such that
A4: for c being set st c in Y /\ (dom f) holds
r2 <= f . c by A2, Th71;
now__::_thesis:_ex_r_being_Element_of_REAL_st_
for_c_being_set_st_c_in_(X_\/_Y)_/\_(dom_f)_holds_
r_<=_f_._c
take r = (- (abs r1)) - (abs r2); ::_thesis: for c being set st c in (X \/ Y) /\ (dom f) holds
r <= f . c
let c be set ; ::_thesis: ( c in (X \/ Y) /\ (dom f) implies r <= f . c )
assume A5: c in (X \/ Y) /\ (dom f) ; ::_thesis: r <= f . c
then A6: c in dom f by XBOOLE_0:def_4;
A7: c in X \/ Y by A5, XBOOLE_0:def_4;
now__::_thesis:_r_<=_f_._c
percases ( c in X or c in Y ) by A7, XBOOLE_0:def_3;
suppose c in X ; ::_thesis: r <= f . c
then c in X /\ (dom f) by A6, XBOOLE_0:def_4;
then A8: r1 <= f . c by A3;
A9: 0 <= abs r2 by COMPLEX1:46;
- (abs r1) <= r1 by ABSVALUE:4;
then - (abs r1) <= f . c by A8, XXREAL_0:2;
then r <= (f . c) - 0 by A9, XREAL_1:13;
hence r <= f . c ; ::_thesis: verum
end;
suppose c in Y ; ::_thesis: r <= f . c
then c in Y /\ (dom f) by A6, XBOOLE_0:def_4;
then A10: r2 <= f . c by A4;
A11: 0 <= abs r1 by COMPLEX1:46;
- (abs r2) <= r2 by ABSVALUE:4;
then - (abs r2) <= f . c by A10, XXREAL_0:2;
then (- (abs r2)) - (abs r1) <= (f . c) - 0 by A11, XREAL_1:13;
hence r <= f . c ; ::_thesis: verum
end;
end;
end;
hence r <= f . c ; ::_thesis: verum
end;
hence f | (X \/ Y) is bounded_below by Th71; ::_thesis: verum
end;
theorem :: RFUNCT_1:87
for X, Y being set
for f being real-valued Function st f | X is bounded & f | Y is bounded holds
f | (X \/ Y) is bounded
proof
let X, Y be set ; ::_thesis: for f being real-valued Function st f | X is bounded & f | Y is bounded holds
f | (X \/ Y) is bounded
let f be real-valued Function; ::_thesis: ( f | X is bounded & f | Y is bounded implies f | (X \/ Y) is bounded )
assume that
A1: f | X is bounded and
A2: f | Y is bounded ; ::_thesis: f | (X \/ Y) is bounded
thus f | (X \/ Y) is bounded_above by A1, A2, Th85; :: according to SEQ_2:def_8 ::_thesis: f | (X \/ Y) is bounded_below
thus f | (X \/ Y) is bounded_below by A1, A2, Th86; ::_thesis: verum
end;
registration
let C be non empty set ;
let f1, f2 be constant PartFunc of C,REAL;
clusterf1 + f2 -> constant ;
coherence
f1 + f2 is constant
proof
consider r2 being Real such that
A1: for c being Element of C st c in dom f2 holds
f2 . c = r2 by PARTFUN2:def_1;
consider r1 being Real such that
A2: for c being Element of C st c in dom f1 holds
f1 . c = r1 by PARTFUN2:def_1;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_+_f2)_holds_
(f1_+_f2)_._c_=_r1_+_r2
let c be Element of C; ::_thesis: ( c in dom (f1 + f2) implies (f1 + f2) . c = r1 + r2 )
assume A3: c in dom (f1 + f2) ; ::_thesis: (f1 + f2) . c = r1 + r2
then A4: c in (dom f1) /\ (dom f2) by VALUED_1:def_1;
then A5: c in dom f1 by XBOOLE_0:def_4;
A6: c in dom f2 by A4, XBOOLE_0:def_4;
thus (f1 + f2) . c = (f1 . c) + (f2 . c) by A3, VALUED_1:def_1
.= (f1 . c) + r2 by A1, A6
.= r1 + r2 by A2, A5 ; ::_thesis: verum
end;
hence f1 + f2 is constant by PARTFUN2:def_1; ::_thesis: verum
end;
clusterf1 - f2 -> constant ;
coherence
f1 - f2 is constant
proof
consider r2 being Real such that
A7: for c being Element of C st c in dom f2 holds
f2 . c = r2 by PARTFUN2:def_1;
consider r1 being Real such that
A8: for c being Element of C st c in dom f1 holds
f1 . c = r1 by PARTFUN2:def_1;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_-_f2)_holds_
(f1_-_f2)_._c_=_r1_-_r2
let c be Element of C; ::_thesis: ( c in dom (f1 - f2) implies (f1 - f2) . c = r1 - r2 )
assume A9: c in dom (f1 - f2) ; ::_thesis: (f1 - f2) . c = r1 - r2
then A10: c in (dom f1) /\ (dom f2) by VALUED_1:12;
then A11: c in dom f1 by XBOOLE_0:def_4;
A12: c in dom f2 by A10, XBOOLE_0:def_4;
thus (f1 - f2) . c = (f1 . c) - (f2 . c) by A9, VALUED_1:13
.= (f1 . c) - r2 by A7, A12
.= r1 - r2 by A8, A11 ; ::_thesis: verum
end;
hence f1 - f2 is constant by PARTFUN2:def_1; ::_thesis: verum
end;
clusterf1 (#) f2 -> constant ;
coherence
f1 (#) f2 is constant
proof
consider r2 being Real such that
A13: for c being Element of C st c in dom f2 holds
f2 . c = r2 by PARTFUN2:def_1;
consider r1 being Real such that
A14: for c being Element of C st c in dom f1 holds
f1 . c = r1 by PARTFUN2:def_1;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_(#)_f2)_holds_
(f1_(#)_f2)_._c_=_r1_*_r2
let c be Element of C; ::_thesis: ( c in dom (f1 (#) f2) implies (f1 (#) f2) . c = r1 * r2 )
assume A15: c in dom (f1 (#) f2) ; ::_thesis: (f1 (#) f2) . c = r1 * r2
then A16: c in (dom f1) /\ (dom f2) by VALUED_1:def_4;
then A17: c in dom f1 by XBOOLE_0:def_4;
A18: c in dom f2 by A16, XBOOLE_0:def_4;
thus (f1 (#) f2) . c = (f1 . c) * (f2 . c) by A15, VALUED_1:def_4
.= (f1 . c) * r2 by A13, A18
.= r1 * r2 by A14, A17 ; ::_thesis: verum
end;
hence f1 (#) f2 is constant by PARTFUN2:def_1; ::_thesis: verum
end;
end;
theorem :: RFUNCT_1:88
for X, Y being set
for C being non empty set
for f1, f2 being PartFunc of C,REAL st f1 | X is constant & f2 | Y is constant holds
( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant )
proof
let X, Y be set ; ::_thesis: for C being non empty set
for f1, f2 being PartFunc of C,REAL st f1 | X is constant & f2 | Y is constant holds
( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant )
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,REAL st f1 | X is constant & f2 | Y is constant holds
( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant )
let f1, f2 be PartFunc of C,REAL; ::_thesis: ( f1 | X is constant & f2 | Y is constant implies ( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant ) )
assume that
A1: f1 | X is constant and
A2: f2 | Y is constant ; ::_thesis: ( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant )
consider r1 being Real such that
A3: for c being Element of C st c in X /\ (dom f1) holds
f1 . c = r1 by A1, PARTFUN2:57;
consider r2 being Real such that
A4: for c being Element of C st c in Y /\ (dom f2) holds
f2 . c = r2 by A2, PARTFUN2:57;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_(X_/\_Y)_/\_(dom_(f1_+_f2))_holds_
(f1_+_f2)_._c_=_r1_+_r2
let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 + f2)) implies (f1 + f2) . c = r1 + r2 )
assume A5: c in (X /\ Y) /\ (dom (f1 + f2)) ; ::_thesis: (f1 + f2) . c = r1 + r2
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 VALUED_1:def_1;
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, VALUED_1:def_1
.= r1 + (f2 . c) by A3, A10
.= r1 + r2 by A4, A12 ; ::_thesis: verum
end;
hence (f1 + f2) | (X /\ Y) is constant by PARTFUN2:57; ::_thesis: ( (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant )
now__::_thesis:_for_c_being_Element_of_C_st_c_in_(X_/\_Y)_/\_(dom_(f1_-_f2))_holds_
(f1_-_f2)_._c_=_r1_-_r2
let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 - f2)) implies (f1 - f2) . c = r1 - r2 )
assume A13: c in (X /\ Y) /\ (dom (f1 - f2)) ; ::_thesis: (f1 - f2) . c = r1 - r2
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 VALUED_1:12;
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, VALUED_1:13
.= r1 - (f2 . c) by A3, A18
.= r1 - r2 by A4, A20 ; ::_thesis: verum
end;
hence (f1 - f2) | (X /\ Y) is constant by PARTFUN2:57; ::_thesis: (f1 (#) f2) | (X /\ Y) is constant
now__::_thesis:_for_c_being_Element_of_C_st_c_in_(X_/\_Y)_/\_(dom_(f1_(#)_f2))_holds_
(f1_(#)_f2)_._c_=_r1_*_r2
let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 (#) f2)) implies (f1 (#) f2) . c = r1 * r2 )
assume A21: c in (X /\ Y) /\ (dom (f1 (#) f2)) ; ::_thesis: (f1 (#) f2) . c = r1 * r2
then A22: c in X /\ Y by XBOOLE_0:def_4;
c in dom (f1 (#) f2) by A21, XBOOLE_0:def_4;
then A23: c in (dom f1) /\ (dom f2) by VALUED_1:def_4;
then A24: c in dom f1 by XBOOLE_0:def_4;
A25: c in dom f2 by A23, XBOOLE_0:def_4;
c in Y by A22, XBOOLE_0:def_4;
then A26: c in Y /\ (dom f2) by A25, XBOOLE_0:def_4;
c in X by A22, XBOOLE_0:def_4;
then A27: c in X /\ (dom f1) by A24, XBOOLE_0:def_4;
thus (f1 (#) f2) . c = (f1 . c) * (f2 . c) by VALUED_1:5
.= r1 * (f2 . c) by A3, A27
.= r1 * r2 by A4, A26 ; ::_thesis: verum
end;
hence (f1 (#) f2) | (X /\ Y) is constant by PARTFUN2:57; ::_thesis: verum
end;
registration
let C be non empty set ;
let f be constant PartFunc of C,REAL;
cluster - f -> constant ;
coherence
- f is constant
proof
consider r being Real such that
A1: for c being Element of C st c in dom f holds
f . c = r by PARTFUN2:def_1;
now__::_thesis:_ex_p_being_Element_of_REAL_st_
for_c_being_Element_of_C_st_c_in_dom_(-_f)_holds_
(-_f)_._c_=_p
take p = - r; ::_thesis: for c being Element of C st c in dom (- f) holds
(- f) . c = p
let c be Element of C; ::_thesis: ( c in dom (- f) implies (- f) . c = p )
assume c in dom (- f) ; ::_thesis: (- f) . c = p
then c in dom f by VALUED_1:8;
then - (f . c) = p by A1;
hence (- f) . c = p by VALUED_1:8; ::_thesis: verum
end;
hence - f is constant by PARTFUN2:def_1; ::_thesis: verum
end;
cluster|.f.| -> constant ;
coherence
abs f is constant
proof
consider r being Real such that
A2: for c being Element of C st c in dom f holds
f . c = r by PARTFUN2:def_1;
now__::_thesis:_ex_p_being_Element_of_REAL_st_
for_c_being_Element_of_C_st_c_in_dom_(abs_f)_holds_
(abs_f)_._c_=_p
take p = abs r; ::_thesis: for c being Element of C st c in dom (abs f) holds
(abs f) . c = p
let c be Element of C; ::_thesis: ( c in dom (abs f) implies (abs f) . c = p )
assume c in dom (abs f) ; ::_thesis: (abs f) . c = p
then c in dom f by VALUED_1:def_11;
then abs (f . c) = p by A2;
hence (abs f) . c = p by VALUED_1:18; ::_thesis: verum
end;
hence abs f is constant by PARTFUN2:def_1; ::_thesis: verum
end;
let p be real number ;
clusterp (#) f -> constant ;
coherence
p (#) f is constant
proof
consider r being Real such that
A3: for c being Element of C st c in dom f holds
f . c = r by PARTFUN2:def_1;
now__::_thesis:_ex_r1_being_Element_of_REAL_st_
for_c_being_Element_of_C_st_c_in_dom_(p_(#)_f)_holds_
(p_(#)_f)_._c_=_r1
take r1 = p * r; ::_thesis: for c being Element of C st c in dom (p (#) f) holds
(p (#) f) . c = r1
let c be Element of C; ::_thesis: ( c in dom (p (#) f) implies (p (#) f) . c = r1 )
assume c in dom (p (#) f) ; ::_thesis: (p (#) f) . c = r1
then c in dom f by VALUED_1:def_5;
then p * (f . c) = r1 by A3;
hence (p (#) f) . c = r1 by VALUED_1:6; ::_thesis: verum
end;
hence p (#) f is constant by PARTFUN2:def_1; ::_thesis: verum
end;
end;
theorem Th89: :: RFUNCT_1:89
for Y being set
for C being non empty set
for p being real number
for f being PartFunc of C,REAL st f | Y is constant holds
(p (#) f) | Y is constant
proof
let Y be set ; ::_thesis: for C being non empty set
for p being real number
for f being PartFunc of C,REAL st f | Y is constant holds
(p (#) f) | Y is constant
let C be non empty set ; ::_thesis: for p being real number
for f being PartFunc of C,REAL st f | Y is constant holds
(p (#) f) | Y is constant
let p be real number ; ::_thesis: for f being PartFunc of C,REAL st f | Y is constant holds
(p (#) f) | Y is constant
let f be PartFunc of C,REAL; ::_thesis: ( f | Y is constant implies (p (#) f) | Y is constant )
(p (#) f) | Y = p (#) (f | Y) by Th49;
hence ( f | Y is constant implies (p (#) f) | Y is constant ) ; ::_thesis: verum
end;
theorem Th90: :: RFUNCT_1:90
for Y being set
for C being non empty set
for f being PartFunc of C,REAL st f | Y is constant holds
(- f) | Y is constant
proof
let Y be set ; ::_thesis: for C being non empty set
for f being PartFunc of C,REAL st f | Y is constant holds
(- f) | Y is constant
let C be non empty set ; ::_thesis: for f being PartFunc of C,REAL st f | Y is constant holds
(- f) | Y is constant
let f be PartFunc of C,REAL; ::_thesis: ( f | Y is constant implies (- f) | Y is constant )
(- f) | Y = - (f | Y) by Th46;
hence ( f | Y is constant implies (- f) | Y is constant ) ; ::_thesis: verum
end;
theorem Th91: :: RFUNCT_1:91
for Y being set
for C being non empty set
for f being PartFunc of C,REAL st f | Y is constant holds
(abs f) | Y is constant
proof
let Y be set ; ::_thesis: for C being non empty set
for f being PartFunc of C,REAL st f | Y is constant holds
(abs f) | Y is constant
let C be non empty set ; ::_thesis: for f being PartFunc of C,REAL st f | Y is constant holds
(abs f) | Y is constant
let f be PartFunc of C,REAL; ::_thesis: ( f | Y is constant implies (abs f) | Y is constant )
(abs f) | Y = abs (f | Y) by Th46;
hence ( f | Y is constant implies (abs f) | Y is constant ) ; ::_thesis: verum
end;
theorem :: RFUNCT_1:92
for Y being set
for C being non empty set
for f being PartFunc of C,REAL st f | Y is constant holds
( ( for r being real number holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & (abs f) | Y is bounded )
proof
let Y be set ; ::_thesis: for C being non empty set
for f being PartFunc of C,REAL st f | Y is constant holds
( ( for r being real number holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & (abs f) | Y is bounded )
let C be non empty set ; ::_thesis: for f being PartFunc of C,REAL st f | Y is constant holds
( ( for r being real number holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & (abs f) | Y is bounded )
let f be PartFunc of C,REAL; ::_thesis: ( f | Y is constant implies ( ( for r being real number holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & (abs f) | Y is bounded ) )
assume A1: f | Y is constant ; ::_thesis: ( ( for r being real number holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & (abs f) | Y is bounded )
hereby ::_thesis: ( (- f) | Y is bounded & (abs f) | Y is bounded )
let r be real number ; ::_thesis: (r (#) f) | Y is bounded
(r (#) f) | Y is constant by A1, Th89;
hence (r (#) f) | Y is bounded ; ::_thesis: verum
end;
(- f) | Y is constant by A1, Th90;
hence (- f) | Y is bounded ; ::_thesis: (abs f) | Y is bounded
(abs f) | Y is constant by A1, Th91;
hence (abs f) | Y is bounded ; ::_thesis: verum
end;
theorem :: RFUNCT_1:93
for X, Y being set
for C being non empty set
for f1, f2 being PartFunc of C,REAL holds
( ( f1 | X is bounded_above & f2 | Y is constant implies (f1 + f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is constant implies (f1 + f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is constant implies (f1 + f2) | (X /\ Y) is bounded ) ) by Th83;
theorem :: RFUNCT_1:94
for X, Y being set
for C being non empty set
for f1, f2 being PartFunc of C,REAL holds
( ( f1 | X is bounded_above & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is constant implies ( (f1 - f2) | (X /\ Y) is bounded & (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded ) ) )
proof
let X, Y be set ; ::_thesis: for C being non empty set
for f1, f2 being PartFunc of C,REAL holds
( ( f1 | X is bounded_above & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is constant implies ( (f1 - f2) | (X /\ Y) is bounded & (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded ) ) )
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,REAL holds
( ( f1 | X is bounded_above & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is constant implies ( (f1 - f2) | (X /\ Y) is bounded & (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded ) ) )
let f1, f2 be PartFunc of C,REAL; ::_thesis: ( ( f1 | X is bounded_above & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is constant implies ( (f1 - f2) | (X /\ Y) is bounded & (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded ) ) )
thus ( f1 | X is bounded_above & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_above ) ::_thesis: ( ( f1 | X is bounded_below & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is constant implies ( (f1 - f2) | (X /\ Y) is bounded & (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded ) ) )
proof
assume that
A1: f1 | X is bounded_above and
A2: f2 | Y is constant ; ::_thesis: (f1 - f2) | (X /\ Y) is bounded_above
(- f2) | Y is constant by A2, Th90;
hence (f1 - f2) | (X /\ Y) is bounded_above by A1, Th83; ::_thesis: verum
end;
thus ( f1 | X is bounded_below & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_below ) ::_thesis: ( f1 | X is bounded & f2 | Y is constant implies ( (f1 - f2) | (X /\ Y) is bounded & (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded ) )
proof
assume that
A3: f1 | X is bounded_below and
A4: f2 | Y is constant ; ::_thesis: (f1 - f2) | (X /\ Y) is bounded_below
(- f2) | Y is constant by A4, Th90;
hence (f1 - f2) | (X /\ Y) is bounded_below by A3, Th83; ::_thesis: verum
end;
assume that
A5: f1 | X is bounded and
A6: f2 | Y is constant ; ::_thesis: ( (f1 - f2) | (X /\ Y) is bounded & (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded )
(- f2) | Y is constant by A6, Th90;
hence (f1 - f2) | (X /\ Y) is bounded by A5, Th83; ::_thesis: ( (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded )
thus (f2 - f1) | (X /\ Y) is bounded by A5, A6, Th84; ::_thesis: (f1 (#) f2) | (X /\ Y) is bounded
thus (f1 (#) f2) | (X /\ Y) is bounded by A5, A6, Th84; ::_thesis: verum
end;