:: PDIFF_1 semantic presentation
begin
definition
let i, n be Nat;
func proj (i,n) -> Function of (REAL n),REAL means :Def1: :: PDIFF_1:def 1
for x being Element of REAL n holds it . x = x . i;
existence
ex b1 being Function of (REAL n),REAL st
for x being Element of REAL n holds b1 . x = x . i
proof
deffunc H1( Element of REAL n) -> Element of REAL = $1 . i;
thus ex f being Function of (REAL n),REAL st
for x being Element of REAL n holds f . x = H1(x) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (REAL n),REAL st ( for x being Element of REAL n holds b1 . x = x . i ) & ( for x being Element of REAL n holds b2 . x = x . i ) holds
b1 = b2
proof
let f, g be Function of (REAL n),REAL; ::_thesis: ( ( for x being Element of REAL n holds f . x = x . i ) & ( for x being Element of REAL n holds g . x = x . i ) implies f = g )
assume that
A1: for x being Element of REAL n holds f . x = x . i and
A2: for x being Element of REAL n holds g . x = x . i ; ::_thesis: f = g
now__::_thesis:_for_x_being_Element_of_REAL_n_holds_f_._x_=_g_._x
let x be Element of REAL n; ::_thesis: f . x = g . x
f . x = x . i by A1;
hence f . x = g . x by A2; ::_thesis: verum
end;
hence f = g by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines proj PDIFF_1:def_1_:_
for i, n being Nat
for b3 being Function of (REAL n),REAL holds
( b3 = proj (i,n) iff for x being Element of REAL n holds b3 . x = x . i );
set W = (proj (1,1)) " ;
Lm1: ( proj (1,1) is bijective & dom (proj (1,1)) = REAL 1 & rng (proj (1,1)) = REAL & ( for x being Element of REAL holds
( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) )
proof
set f = proj (1,1);
for x1, x2 being set st x1 in dom (proj (1,1)) & x2 in dom (proj (1,1)) & (proj (1,1)) . x1 = (proj (1,1)) . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom (proj (1,1)) & x2 in dom (proj (1,1)) & (proj (1,1)) . x1 = (proj (1,1)) . x2 implies x1 = x2 )
assume that
A1: x1 in dom (proj (1,1)) and
A2: x2 in dom (proj (1,1)) and
A3: (proj (1,1)) . x1 = (proj (1,1)) . x2 ; ::_thesis: x1 = x2
reconsider y1 = x1, y2 = x2 as Element of REAL 1 by A1, A2;
x1 is Tuple of 1, REAL by A1, FINSEQ_2:131;
then consider d1 being Element of REAL such that
A4: x1 = <*d1*> by FINSEQ_2:97;
d1 = <*d1*> . 1 by FINSEQ_1:40;
then d1 = (proj (1,1)) . y1 by A4, Def1;
then A5: d1 = y2 . 1 by A3, Def1;
x2 is Tuple of 1, REAL by A2, FINSEQ_2:131;
then ex d2 being Element of REAL st x2 = <*d2*> by FINSEQ_2:97;
hence x1 = x2 by A4, A5, FINSEQ_1:40; ::_thesis: verum
end;
then A6: proj (1,1) is one-to-one by FUNCT_1:def_4;
A7: dom (proj (1,1)) = REAL 1 by FUNCT_2:def_1;
A8: now__::_thesis:_for_x_being_Element_of_REAL_holds_
(_(proj_(1,1))_._<*x*>_=_x_&_((proj_(1,1))_")_._x_=_<*x*>_)
let x be Element of REAL ; ::_thesis: ( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> )
A9: <*x*> is Element of 1 -tuples_on REAL by FINSEQ_2:98;
then (proj (1,1)) . <*x*> = <*x*> . 1 by Def1;
hence (proj (1,1)) . <*x*> = x by FINSEQ_1:40; ::_thesis: ((proj (1,1)) ") . x = <*x*>
hence ((proj (1,1)) ") . x = <*x*> by A7, A6, A9, FUNCT_1:34; ::_thesis: verum
end;
A10: for y being set st y in REAL holds
ex x being set st
( x in REAL 1 & y = (proj (1,1)) . x )
proof
let y be set ; ::_thesis: ( y in REAL implies ex x being set st
( x in REAL 1 & y = (proj (1,1)) . x ) )
assume y in REAL ; ::_thesis: ex x being set st
( x in REAL 1 & y = (proj (1,1)) . x )
then reconsider y1 = y as Element of REAL ;
reconsider x = <*y1*> as Element of REAL 1 by FINSEQ_2:98;
(proj (1,1)) . x = x . 1 by Def1;
then (proj (1,1)) . x = y by FINSEQ_1:40;
hence ex x being set st
( x in REAL 1 & y = (proj (1,1)) . x ) ; ::_thesis: verum
end;
then rng (proj (1,1)) = REAL by FUNCT_2:10;
then proj (1,1) is onto by FUNCT_2:def_3;
hence ( proj (1,1) is bijective & dom (proj (1,1)) = REAL 1 & rng (proj (1,1)) = REAL & ( for x being Element of REAL holds
( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) ) by A6, A10, A8, FUNCT_2:10, FUNCT_2:def_1; ::_thesis: verum
end;
Lm2: for i, n being Element of NAT st i in Seg n holds
proj (i,n) is onto
proof
let i, n be Element of NAT ; ::_thesis: ( i in Seg n implies proj (i,n) is onto )
set f = proj (i,n);
assume A1: i in Seg n ; ::_thesis: proj (i,n) is onto
for y being set st y in REAL holds
ex x being set st
( x in REAL n & y = (proj (i,n)) . x )
proof
let y be set ; ::_thesis: ( y in REAL implies ex x being set st
( x in REAL n & y = (proj (i,n)) . x ) )
assume y in REAL ; ::_thesis: ex x being set st
( x in REAL n & y = (proj (i,n)) . x )
then reconsider y1 = y as Element of REAL ;
reconsider x = n |-> y1 as Element of REAL n ;
(proj (i,n)) . x = x . i by Def1;
then (proj (i,n)) . x = y by A1, FINSEQ_2:57;
hence ex x being set st
( x in REAL n & y = (proj (i,n)) . x ) ; ::_thesis: verum
end;
then rng (proj (i,n)) = REAL by FUNCT_2:10;
hence proj (i,n) is onto by FUNCT_2:def_3; ::_thesis: verum
end;
theorem :: PDIFF_1:1
( ( for i, n being Element of NAT st i in Seg n holds
( dom (proj (i,n)) = REAL n & rng (proj (i,n)) = REAL ) ) & ( for x being Element of REAL holds
( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) )
proof
now__::_thesis:_for_i,_n_being_Element_of_NAT_st_i_in_Seg_n_holds_
(_dom_(proj_(i,n))_=_REAL_n_&_rng_(proj_(i,n))_=_REAL_)
let i, n be Element of NAT ; ::_thesis: ( i in Seg n implies ( dom (proj (i,n)) = REAL n & rng (proj (i,n)) = REAL ) )
assume A1: i in Seg n ; ::_thesis: ( dom (proj (i,n)) = REAL n & rng (proj (i,n)) = REAL )
thus dom (proj (i,n)) = REAL n by FUNCT_2:def_1; ::_thesis: rng (proj (i,n)) = REAL
proj (i,n) is onto by A1, Lm2;
hence rng (proj (i,n)) = REAL by FUNCT_2:def_3; ::_thesis: verum
end;
hence ( ( for i, n being Element of NAT st i in Seg n holds
( dom (proj (i,n)) = REAL n & rng (proj (i,n)) = REAL ) ) & ( for x being Element of REAL holds
( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) ) by Lm1; ::_thesis: verum
end;
theorem Th2: :: PDIFF_1:2
( (proj (1,1)) " is Function of REAL,(REAL 1) & (proj (1,1)) " is one-to-one & dom ((proj (1,1)) ") = REAL & rng ((proj (1,1)) ") = REAL 1 & ex g being Function of REAL,(REAL 1) st
( g is bijective & (proj (1,1)) " = g ) )
proof
A1: REAL 1 = rng ((proj (1,1)) ") by Lm1, FUNCT_1:33;
REAL = dom ((proj (1,1)) ") by Lm1, FUNCT_1:33;
then reconsider g = (proj (1,1)) " as Function of REAL,(REAL 1) by A1, FUNCT_2:1;
g is onto by A1, FUNCT_2:def_3;
hence ( (proj (1,1)) " is Function of REAL,(REAL 1) & (proj (1,1)) " is one-to-one & dom ((proj (1,1)) ") = REAL & rng ((proj (1,1)) ") = REAL 1 & ex g being Function of REAL,(REAL 1) st
( g is bijective & (proj (1,1)) " = g ) ) by Lm1, FUNCT_1:33; ::_thesis: verum
end;
registration
cluster proj (1,1) -> bijective ;
coherence
proj (1,1) is bijective by Lm1;
end;
definition
let g be PartFunc of REAL,REAL;
func <>* g -> PartFunc of (REAL 1),(REAL 1) equals :: PDIFF_1:def 2
(((proj (1,1)) ") * g) * (proj (1,1));
coherence
(((proj (1,1)) ") * g) * (proj (1,1)) is PartFunc of (REAL 1),(REAL 1)
proof
reconsider f = (proj (1,1)) " as PartFunc of REAL,(REAL 1) by PARTFUN1:9;
(f * g) * (proj (1,1)) is PartFunc of (REAL 1),(REAL 1) ;
hence (((proj (1,1)) ") * g) * (proj (1,1)) is PartFunc of (REAL 1),(REAL 1) ; ::_thesis: verum
end;
end;
:: deftheorem defines <>* PDIFF_1:def_2_:_
for g being PartFunc of REAL,REAL holds <>* g = (((proj (1,1)) ") * g) * (proj (1,1));
definition
let n be Nat;
let g be PartFunc of (REAL n),REAL;
func <>* g -> PartFunc of (REAL n),(REAL 1) equals :: PDIFF_1:def 3
((proj (1,1)) ") * g;
correctness
coherence
((proj (1,1)) ") * g is PartFunc of (REAL n),(REAL 1);
proof
reconsider f = (proj (1,1)) " as PartFunc of REAL,(REAL 1) by PARTFUN1:9;
f * g is PartFunc of (REAL n),(REAL 1) ;
hence ((proj (1,1)) ") * g is PartFunc of (REAL n),(REAL 1) ; ::_thesis: verum
end;
end;
:: deftheorem defines <>* PDIFF_1:def_3_:_
for n being Nat
for g being PartFunc of (REAL n),REAL holds <>* g = ((proj (1,1)) ") * g;
definition
let i, n be Nat;
func Proj (i,n) -> Function of (REAL-NS n),(REAL-NS 1) means :Def4: :: PDIFF_1:def 4
for x being Point of (REAL-NS n) holds it . x = <*((proj (i,n)) . x)*>;
existence
ex b1 being Function of (REAL-NS n),(REAL-NS 1) st
for x being Point of (REAL-NS n) holds b1 . x = <*((proj (i,n)) . x)*>
proof
deffunc H1( Point of (REAL-NS n)) -> FinSequence of REAL = <*((proj (i,n)) . $1)*>;
A1: for x being Point of (REAL-NS n) holds H1(x) is Element of (REAL-NS 1)
proof
let x be Point of (REAL-NS n); ::_thesis: H1(x) is Element of (REAL-NS 1)
len H1(x) = 1 by FINSEQ_1:39;
then H1(x) is Element of 1 -tuples_on REAL by FINSEQ_2:92;
then H1(x) in REAL 1 ;
hence H1(x) is Element of (REAL-NS 1) by REAL_NS1:def_4; ::_thesis: verum
end;
thus ex f being Function of (REAL-NS n),(REAL-NS 1) st
for x being Point of (REAL-NS n) holds f . x = H1(x) from FUNCT_2:sch_9(A1); ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (REAL-NS n),(REAL-NS 1) st ( for x being Point of (REAL-NS n) holds b1 . x = <*((proj (i,n)) . x)*> ) & ( for x being Point of (REAL-NS n) holds b2 . x = <*((proj (i,n)) . x)*> ) holds
b1 = b2
proof
let f, g be Function of (REAL-NS n),(REAL-NS 1); ::_thesis: ( ( for x being Point of (REAL-NS n) holds f . x = <*((proj (i,n)) . x)*> ) & ( for x being Point of (REAL-NS n) holds g . x = <*((proj (i,n)) . x)*> ) implies f = g )
assume that
A2: for x being Point of (REAL-NS n) holds f . x = <*((proj (i,n)) . x)*> and
A3: for x being Point of (REAL-NS n) holds g . x = <*((proj (i,n)) . x)*> ; ::_thesis: f = g
now__::_thesis:_for_x_being_Point_of_(REAL-NS_n)_holds_f_._x_=_g_._x
let x be Point of (REAL-NS n); ::_thesis: f . x = g . x
f . x = <*((proj (i,n)) . x)*> by A2;
hence f . x = g . x by A3; ::_thesis: verum
end;
hence f = g by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines Proj PDIFF_1:def_4_:_
for i, n being Nat
for b3 being Function of (REAL-NS n),(REAL-NS 1) holds
( b3 = Proj (i,n) iff for x being Point of (REAL-NS n) holds b3 . x = <*((proj (i,n)) . x)*> );
definition
let i be Element of NAT ;
let x be FinSequence of REAL ;
func reproj (i,x) -> Function means :Def5: :: PDIFF_1:def 5
( dom it = REAL & ( for r being Element of REAL holds it . r = Replace (x,i,r) ) );
existence
ex b1 being Function st
( dom b1 = REAL & ( for r being Element of REAL holds b1 . r = Replace (x,i,r) ) )
proof
deffunc H1( Element of REAL ) -> FinSequence of REAL = Replace (x,i,$1);
consider f being Function such that
A1: ( dom f = REAL & ( for r being Element of REAL st r in REAL holds
f . r = H1(r) ) ) from GRAPH_5:sch_1();
take f ; ::_thesis: ( dom f = REAL & ( for r being Element of REAL holds f . r = Replace (x,i,r) ) )
thus ( dom f = REAL & ( for r being Element of REAL holds f . r = Replace (x,i,r) ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function st dom b1 = REAL & ( for r being Element of REAL holds b1 . r = Replace (x,i,r) ) & dom b2 = REAL & ( for r being Element of REAL holds b2 . r = Replace (x,i,r) ) holds
b1 = b2
proof
let f, g be Function; ::_thesis: ( dom f = REAL & ( for r being Element of REAL holds f . r = Replace (x,i,r) ) & dom g = REAL & ( for r being Element of REAL holds g . r = Replace (x,i,r) ) implies f = g )
assume that
A2: dom f = REAL and
A3: for r being Element of REAL holds f . r = Replace (x,i,r) and
A4: dom g = REAL and
A5: for r being Element of REAL holds g . r = Replace (x,i,r) ; ::_thesis: f = g
now__::_thesis:_for_p_being_set_st_p_in_dom_f_holds_
f_._p_=_g_._p
let p be set ; ::_thesis: ( p in dom f implies f . p = g . p )
assume p in dom f ; ::_thesis: f . p = g . p
then reconsider r = p as Element of REAL by A2;
f . r = Replace (x,i,r) by A3;
hence f . p = g . p by A5; ::_thesis: verum
end;
hence f = g by A2, A4, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines reproj PDIFF_1:def_5_:_
for i being Element of NAT
for x being FinSequence of REAL
for b3 being Function holds
( b3 = reproj (i,x) iff ( dom b3 = REAL & ( for r being Element of REAL holds b3 . r = Replace (x,i,r) ) ) );
definition
let n, i be Element of NAT ;
let x be Element of REAL n;
:: original: reproj
redefine func reproj (i,x) -> Function of REAL,(REAL n);
correctness
coherence
reproj (i,x) is Function of REAL,(REAL n);
proof
A1: now__::_thesis:_for_p_being_set_st_p_in_REAL_holds_
(reproj_(i,x))_._p_in_REAL_n
let p be set ; ::_thesis: ( p in REAL implies (reproj (i,x)) . p in REAL n )
assume p in REAL ; ::_thesis: (reproj (i,x)) . p in REAL n
then reconsider r = p as Element of REAL ;
A2: (reproj (i,x)) . r = Replace (x,i,r) by Def5;
then reconsider IT = (reproj (i,x)) . r as FinSequence of REAL ;
len IT = len x by A2, FINSEQ_7:5
.= n by CARD_1:def_7 ;
then reconsider IT = IT as Element of n -tuples_on REAL by FINSEQ_2:92;
IT is Element of REAL n ;
hence (reproj (i,x)) . p in REAL n ; ::_thesis: verum
end;
dom (reproj (i,x)) = REAL by Def5;
hence reproj (i,x) is Function of REAL,(REAL n) by A1, FUNCT_2:3; ::_thesis: verum
end;
end;
definition
let n, i be Element of NAT ;
let x be Point of (REAL-NS n);
func reproj (i,x) -> Function of (REAL-NS 1),(REAL-NS n) means :Def6: :: PDIFF_1:def 6
for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st
( r = <*q*> & y = x & it . r = (reproj (i,y)) . q );
existence
ex b1 being Function of (REAL-NS 1),(REAL-NS n) st
for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st
( r = <*q*> & y = x & b1 . r = (reproj (i,y)) . q )
proof
defpred S1[ Element of (REAL-NS 1), Point of (REAL-NS n)] means ex q being Element of REAL ex z being Element of REAL n st
( $1 = <*q*> & z = x & $2 = (reproj (i,z)) . q );
A1: for r being Element of (REAL-NS 1) ex y being Element of (REAL-NS n) st S1[r,y]
proof
reconsider z = x as Element of REAL n by REAL_NS1:def_4;
let r be Element of (REAL-NS 1); ::_thesis: ex y being Element of (REAL-NS n) st S1[r,y]
r is Element of REAL 1 by REAL_NS1:def_4;
then consider q being Element of REAL such that
A2: r = <*q*> by FINSEQ_2:97;
(reproj (i,z)) . q is Element of (REAL-NS n) by REAL_NS1:def_4;
hence ex y being Element of (REAL-NS n) st S1[r,y] by A2; ::_thesis: verum
end;
thus ex f being Function of (REAL-NS 1),(REAL-NS n) st
for r being Element of (REAL-NS 1) holds S1[r,f . r] from FUNCT_2:sch_3(A1); ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (REAL-NS 1),(REAL-NS n) st ( for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st
( r = <*q*> & y = x & b1 . r = (reproj (i,y)) . q ) ) & ( for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st
( r = <*q*> & y = x & b2 . r = (reproj (i,y)) . q ) ) holds
b1 = b2
proof
let f, g be Function of (REAL-NS 1),(REAL-NS n); ::_thesis: ( ( for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st
( r = <*q*> & y = x & f . r = (reproj (i,y)) . q ) ) & ( for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st
( r = <*q*> & y = x & g . r = (reproj (i,y)) . q ) ) implies f = g )
assume that
A3: for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st
( r = <*q*> & y = x & f . r = (reproj (i,y)) . q ) and
A4: for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st
( r = <*q*> & y = x & g . r = (reproj (i,y)) . q ) ; ::_thesis: f = g
now__::_thesis:_for_r_being_Point_of_(REAL-NS_1)_holds_f_._r_=_g_._r
let r be Point of (REAL-NS 1); ::_thesis: f . r = g . r
consider p being Element of REAL , y being Element of REAL n such that
A5: r = <*p*> and
A6: y = x and
A7: f . r = (reproj (i,y)) . p by A3;
A8: ex q being Element of REAL ex z being Element of REAL n st
( r = <*q*> & z = x & g . r = (reproj (i,z)) . q ) by A4;
p = <*p*> . 1 by FINSEQ_1:def_8;
hence f . r = g . r by A5, A6, A7, A8, FINSEQ_1:def_8; ::_thesis: verum
end;
hence f = g by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines reproj PDIFF_1:def_6_:_
for n, i being Element of NAT
for x being Point of (REAL-NS n)
for b4 being Function of (REAL-NS 1),(REAL-NS n) holds
( b4 = reproj (i,x) iff for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st
( r = <*q*> & y = x & b4 . r = (reproj (i,y)) . q ) );
definition
let m, n be non empty Element of NAT ;
let f be PartFunc of (REAL m),(REAL n);
let x be Element of REAL m;
predf is_differentiable_in x means :Def7: :: PDIFF_1:def 7
ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & g is_differentiable_in y );
end;
:: deftheorem Def7 defines is_differentiable_in PDIFF_1:def_7_:_
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m holds
( f is_differentiable_in x iff ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & g is_differentiable_in y ) );
definition
let m, n be non empty Element of NAT ;
let f be PartFunc of (REAL m),(REAL n);
let x be Element of REAL m;
assume A1: f is_differentiable_in x ;
func diff (f,x) -> Function of (REAL m),(REAL n) means :Def8: :: PDIFF_1:def 8
ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & it = diff (g,y) );
correctness
existence
ex b1 being Function of (REAL m),(REAL n) ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b1 = diff (g,y) );
uniqueness
for b1, b2 being Function of (REAL m),(REAL n) st ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b1 = diff (g,y) ) & ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b2 = diff (g,y) ) holds
b1 = b2;
proof
A2: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def_4;
consider g being PartFunc of (REAL-NS m),(REAL-NS n), y being Point of (REAL-NS m) such that
A3: f = g and
A4: x = y and
g is_differentiable_in y by A1, Def7;
the carrier of (REAL-NS m) = REAL m by REAL_NS1:def_4;
then diff (g,y) is Function of (REAL m),(REAL n) by A2, LOPBAN_1:def_9;
hence ( ex b1 being Function of (REAL m),(REAL n) ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b1 = diff (g,y) ) & ( for b1, b2 being Function of (REAL m),(REAL n) st ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b1 = diff (g,y) ) & ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b2 = diff (g,y) ) holds
b1 = b2 ) ) by A3, A4; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines diff PDIFF_1:def_8_:_
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m st f is_differentiable_in x holds
for b5 being Function of (REAL m),(REAL n) holds
( b5 = diff (f,x) iff ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b5 = diff (g,y) ) );
theorem Th3: :: PDIFF_1:3
for I being Function of REAL,(REAL 1) st I = (proj (1,1)) " holds
( ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL st x = I . y holds
||.x.|| = abs y ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st x = I . a & y = I . b holds
x + y = I . (a + b) ) & ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL
for a being Real st x = I . y holds
a * x = I . (a * y) ) & ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st x = I . a holds
- x = I . (- a) ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st x = I . a & y = I . b holds
x - y = I . (a - b) ) )
proof
let I be Function of REAL,(REAL 1); ::_thesis: ( I = (proj (1,1)) " implies ( ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL st x = I . y holds
||.x.|| = abs y ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st x = I . a & y = I . b holds
x + y = I . (a + b) ) & ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL
for a being Real st x = I . y holds
a * x = I . (a * y) ) & ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st x = I . a holds
- x = I . (- a) ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st x = I . a & y = I . b holds
x - y = I . (a - b) ) ) )
assume A1: I = (proj (1,1)) " ; ::_thesis: ( ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL st x = I . y holds
||.x.|| = abs y ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st x = I . a & y = I . b holds
x + y = I . (a + b) ) & ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL
for a being Real st x = I . y holds
a * x = I . (a * y) ) & ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st x = I . a holds
- x = I . (- a) ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st x = I . a & y = I . b holds
x - y = I . (a - b) ) )
hereby ::_thesis: ( ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st x = I . a & y = I . b holds
x + y = I . (a + b) ) & ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL
for a being Real st x = I . y holds
a * x = I . (a * y) ) & ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st x = I . a holds
- x = I . (- a) ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st x = I . a & y = I . b holds
x - y = I . (a - b) ) )
let x be VECTOR of (REAL-NS 1); ::_thesis: for y being Element of REAL st x = I . y holds
||.x.|| = abs y
let y be Element of REAL ; ::_thesis: ( x = I . y implies ||.x.|| = abs y )
reconsider xx = x as Element of REAL 1 by REAL_NS1:def_4;
assume x = I . y ; ::_thesis: ||.x.|| = abs y
then xx = <*y*> by A1, Lm1;
then sqrt (Sum (sqr xx)) = sqrt (Sum <*(y ^2)*>) by RVSUM_1:55;
then A2: sqrt (Sum (sqr xx)) = sqrt (y ^2) by RVSUM_1:73;
||.x.|| = |.xx.| by REAL_NS1:1;
hence ||.x.|| = abs y by A2, COMPLEX1:72; ::_thesis: verum
end;
A3: now__::_thesis:_for_x,_y_being_VECTOR_of_(REAL-NS_1)
for_a,_b_being_Element_of_REAL_st_x_=_I_._a_&_y_=_I_._b_holds_
x_-_y_=_I_._(a_-_b)
let x, y be VECTOR of (REAL-NS 1); ::_thesis: for a, b being Element of REAL st x = I . a & y = I . b holds
x - y = I . (a - b)
let a, b be Element of REAL ; ::_thesis: ( x = I . a & y = I . b implies x - y = I . (a - b) )
reconsider xx = x, yy = y as Element of REAL 1 by REAL_NS1:def_4;
assume that
A4: x = I . a and
A5: y = I . b ; ::_thesis: x - y = I . (a - b)
A6: <*b*> = yy by A1, A5, Lm1;
<*a*> = xx by A1, A4, Lm1;
then x - y = <*a*> - <*b*> by A6, REAL_NS1:5;
then x - y = <*(a - b)*> by RVSUM_1:29;
hence x - y = I . (a - b) by A1, Lm1; ::_thesis: verum
end;
hereby ::_thesis: ( ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL
for a being Real st x = I . y holds
a * x = I . (a * y) ) & ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st x = I . a holds
- x = I . (- a) ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st x = I . a & y = I . b holds
x - y = I . (a - b) ) )
let x, y be VECTOR of (REAL-NS 1); ::_thesis: for a, b being Element of REAL st x = I . a & y = I . b holds
x + y = I . (a + b)
let a, b be Element of REAL ; ::_thesis: ( x = I . a & y = I . b implies x + y = I . (a + b) )
reconsider xx = x, yy = y as Element of REAL 1 by REAL_NS1:def_4;
assume that
A7: x = I . a and
A8: y = I . b ; ::_thesis: x + y = I . (a + b)
A9: <*b*> = yy by A1, A8, Lm1;
<*a*> = xx by A1, A7, Lm1;
then x + y = <*a*> + <*b*> by A9, REAL_NS1:2;
then x + y = <*(a + b)*> by RVSUM_1:13;
hence x + y = I . (a + b) by A1, Lm1; ::_thesis: verum
end;
A10: now__::_thesis:_for_x_being_VECTOR_of_(REAL-NS_1)
for_y_being_Element_of_REAL_
for_a_being_Real_st_x_=_I_._y_holds_
a_*_x_=_I_._(a_*_y)
let x be VECTOR of (REAL-NS 1); ::_thesis: for y being Element of REAL
for a being Real st x = I . y holds
a * x = I . (a * y)
let y be Element of REAL ; ::_thesis: for a being Real st x = I . y holds
a * x = I . (a * y)
let a be Real; ::_thesis: ( x = I . y implies a * x = I . (a * y) )
reconsider xx = x as Element of REAL 1 by REAL_NS1:def_4;
assume x = I . y ; ::_thesis: a * x = I . (a * y)
then A11: xx = <*y*> by A1, Lm1;
a * x = a * xx by REAL_NS1:3;
then a * x = <*(a * y)*> by A11, RVSUM_1:47;
hence a * x = I . (a * y) by A1, Lm1; ::_thesis: verum
end;
now__::_thesis:_for_x_being_VECTOR_of_(REAL-NS_1)
for_a_being_Element_of_REAL_st_x_=_I_._a_holds_
-_x_=_I_._(-_a)
let x be VECTOR of (REAL-NS 1); ::_thesis: for a being Element of REAL st x = I . a holds
- x = I . (- a)
let a be Element of REAL ; ::_thesis: ( x = I . a implies - x = I . (- a) )
assume x = I . a ; ::_thesis: - x = I . (- a)
then (- 1) * x = I . ((- 1) * a) by A10;
hence - x = I . (- a) by RLVECT_1:16; ::_thesis: verum
end;
hence ( ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL
for a being Real st x = I . y holds
a * x = I . (a * y) ) & ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st x = I . a holds
- x = I . (- a) ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st x = I . a & y = I . b holds
x - y = I . (a - b) ) ) by A10, A3; ::_thesis: verum
end;
reconsider I = (proj (1,1)) " as Function of REAL,(REAL 1) by Th2;
theorem Th4: :: PDIFF_1:4
for J being Function of (REAL 1),REAL st J = proj (1,1) holds
( ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL st J . x = y holds
||.x.|| = abs y ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x + y) = a + b ) & ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL
for a being Real st J . x = y holds
J . (a * x) = a * y ) & ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st J . x = a holds
J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x - y) = a - b ) )
proof
let J be Function of (REAL 1),REAL; ::_thesis: ( J = proj (1,1) implies ( ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL st J . x = y holds
||.x.|| = abs y ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x + y) = a + b ) & ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL
for a being Real st J . x = y holds
J . (a * x) = a * y ) & ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st J . x = a holds
J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x - y) = a - b ) ) )
assume A1: J = proj (1,1) ; ::_thesis: ( ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL st J . x = y holds
||.x.|| = abs y ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x + y) = a + b ) & ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL
for a being Real st J . x = y holds
J . (a * x) = a * y ) & ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st J . x = a holds
J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x - y) = a - b ) )
hereby ::_thesis: ( ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x + y) = a + b ) & ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL
for a being Real st J . x = y holds
J . (a * x) = a * y ) & ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st J . x = a holds
J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x - y) = a - b ) )
let x be VECTOR of (REAL-NS 1); ::_thesis: for y being Element of REAL st J . x = y holds
||.x.|| = abs y
let y be Element of REAL ; ::_thesis: ( J . x = y implies ||.x.|| = abs y )
reconsider xx = x as Element of REAL 1 by REAL_NS1:def_4;
assume J . x = y ; ::_thesis: ||.x.|| = abs y
then I . (J . xx) = I . y ;
then x = I . y by A1, Lm1, FUNCT_1:34;
hence ||.x.|| = abs y by Th3; ::_thesis: verum
end;
hereby ::_thesis: ( ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL
for a being Real st J . x = y holds
J . (a * x) = a * y ) & ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st J . x = a holds
J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x - y) = a - b ) )
let x, y be VECTOR of (REAL-NS 1); ::_thesis: for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x + y) = a + b
let a, b be Element of REAL ; ::_thesis: ( J . x = a & J . y = b implies J . (x + y) = a + b )
reconsider xx = x, yy = y as Element of REAL 1 by REAL_NS1:def_4;
assume that
A2: J . x = a and
A3: J . y = b ; ::_thesis: J . (x + y) = a + b
I . (J . yy) = I . b by A3;
then A4: y = I . b by A1, Lm1, FUNCT_1:34;
I . (J . xx) = I . a by A2;
then x = I . a by A1, Lm1, FUNCT_1:34;
then J . (x + y) = J . (I . (a + b)) by A4, Th3;
hence J . (x + y) = a + b by A1, Lm1, FUNCT_1:35; ::_thesis: verum
end;
hereby ::_thesis: ( ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st J . x = a holds
J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x - y) = a - b ) )
let x be VECTOR of (REAL-NS 1); ::_thesis: for y being Element of REAL
for a being Real st J . x = y holds
J . (a * x) = a * y
let y be Element of REAL ; ::_thesis: for a being Real st J . x = y holds
J . (a * x) = a * y
let a be Real; ::_thesis: ( J . x = y implies J . (a * x) = a * y )
reconsider xx = x as Element of REAL 1 by REAL_NS1:def_4;
assume J . x = y ; ::_thesis: J . (a * x) = a * y
then I . (J . xx) = I . y ;
then x = I . y by A1, Lm1, FUNCT_1:34;
then J . (a * x) = J . (I . (a * y)) by Th3;
hence J . (a * x) = a * y by A1, Lm1, FUNCT_1:35; ::_thesis: verum
end;
hereby ::_thesis: for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x - y) = a - b
let x be VECTOR of (REAL-NS 1); ::_thesis: for y being Element of REAL st J . x = y holds
J . (- x) = - y
let y be Element of REAL ; ::_thesis: ( J . x = y implies J . (- x) = - y )
reconsider xx = x as Element of REAL 1 by REAL_NS1:def_4;
assume J . x = y ; ::_thesis: J . (- x) = - y
then I . y = I . (J . xx) ;
then x = I . y by A1, Lm1, FUNCT_1:34;
then J . (- x) = J . (I . (- y)) by Th3;
hence J . (- x) = - y by A1, Lm1, FUNCT_1:35; ::_thesis: verum
end;
let x, y be VECTOR of (REAL-NS 1); ::_thesis: for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x - y) = a - b
let a, b be Element of REAL ; ::_thesis: ( J . x = a & J . y = b implies J . (x - y) = a - b )
reconsider xx = x, yy = y as Element of REAL 1 by REAL_NS1:def_4;
assume that
A5: J . x = a and
A6: J . y = b ; ::_thesis: J . (x - y) = a - b
I . (J . yy) = I . b by A6;
then A7: y = I . b by A1, Lm1, FUNCT_1:34;
I . (J . xx) = I . a by A5;
then x = I . a by A1, Lm1, FUNCT_1:34;
then J . (x - y) = J . (I . (a - b)) by A7, Th3;
hence J . (x - y) = a - b by A1, Lm1, FUNCT_1:35; ::_thesis: verum
end;
theorem Th5: :: PDIFF_1:5
for I being Function of REAL,(REAL 1)
for J being Function of (REAL 1),REAL st I = (proj (1,1)) " & J = proj (1,1) holds
( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) )
proof
let I be Function of REAL,(REAL 1); ::_thesis: for J being Function of (REAL 1),REAL st I = (proj (1,1)) " & J = proj (1,1) holds
( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) )
let J be Function of (REAL 1),REAL; ::_thesis: ( I = (proj (1,1)) " & J = proj (1,1) implies ( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) ) )
assume that
A1: I = (proj (1,1)) " and
A2: J = proj (1,1) ; ::_thesis: ( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) )
thus for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ::_thesis: for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc
proof
let R be RestFunc of (REAL-NS 1),(REAL-NS 1); ::_thesis: (J * R) * I is RestFunc
A3: R is total by NDIFF_1:def_5;
the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4;
then reconsider R0 = R as Function of (REAL 1),(REAL 1) by A3;
reconsider R1 = (J * R) * I as PartFunc of REAL,REAL ;
A4: (J * R0) * I is Function of REAL,REAL ;
then A5: dom R1 = REAL by FUNCT_2:def_1;
A6: for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z1 being Real st z1 <> 0 & abs z1 < d holds
((abs z1) ") * (abs (R1 . z1)) < r ) )
proof
let r be Real; ::_thesis: ( r > 0 implies ex d being Real st
( d > 0 & ( for z1 being Real st z1 <> 0 & abs z1 < d holds
((abs z1) ") * (abs (R1 . z1)) < r ) ) )
assume r > 0 ; ::_thesis: ex d being Real st
( d > 0 & ( for z1 being Real st z1 <> 0 & abs z1 < d holds
((abs z1) ") * (abs (R1 . z1)) < r ) )
then consider d being Real such that
A7: d > 0 and
A8: for z being Point of (REAL-NS 1) st z <> 0. (REAL-NS 1) & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r by A3, NDIFF_1:23;
take d ; ::_thesis: ( d > 0 & ( for z1 being Real st z1 <> 0 & abs z1 < d holds
((abs z1) ") * (abs (R1 . z1)) < r ) )
for z1 being Real st z1 <> 0 & abs z1 < d holds
((abs z1) ") * (abs (R1 . z1)) < r
proof
let z1 be Real; ::_thesis: ( z1 <> 0 & abs z1 < d implies ((abs z1) ") * (abs (R1 . z1)) < r )
assume that
A9: z1 <> 0 and
A10: abs z1 < d ; ::_thesis: ((abs z1) ") * (abs (R1 . z1)) < r
reconsider z = I . z1 as Point of (REAL-NS 1) by REAL_NS1:def_4;
z1 in REAL ;
then reconsider z1r = z1 as R_eal by NUMBERS:31;
0 < |.z1r.| by A9, EXTREAL2:4;
then abs z1 > 0 by EXTREAL2:1;
then ||.z.|| <> 0 by A1, Th3;
then A11: z <> 0. (REAL-NS 1) by NORMSP_0:def_6;
I * J = id (dom (proj (1,1))) by A1, A2, FUNCT_1:39;
then A12: I * J = id (REAL 1) by FUNCT_2:def_1;
A13: dom (J * R0) = REAL 1 by FUNCT_2:def_1;
R is total by NDIFF_1:def_5;
then A14: dom R = the carrier of (REAL-NS 1) by PARTFUN1:def_2;
then R /. z = R . z by PARTFUN1:def_6;
then R /. z = ((id the carrier of (REAL-NS 1)) * R) . (I . z1) by FUNCT_2:17;
then R /. z = ((I * J) * R) . (I . z1) by A12, REAL_NS1:def_4;
then A15: R /. z = (I * J) . (R . (I . z1)) by A14, FUNCT_1:13;
dom J = REAL 1 by FUNCT_2:def_1;
then R /. z = I . (J . (R0 . z)) by A15, FUNCT_1:13, FUNCT_2:5;
then R /. z = I . ((J * R0) . (I . z1)) by A13, FUNCT_1:12;
then R /. z = I . (R1 . z1) by A5, FUNCT_1:12;
then A16: ||.(R /. z).|| = abs (R1 . z1) by A1, Th3;
A17: ||.z.|| " = (abs z1) " by A1, Th3;
||.z.|| < d by A1, A10, Th3;
hence ((abs z1) ") * (abs (R1 . z1)) < r by A8, A11, A17, A16; ::_thesis: verum
end;
hence ( d > 0 & ( for z1 being Real st z1 <> 0 & abs z1 < d holds
((abs z1) ") * (abs (R1 . z1)) < r ) ) by A7; ::_thesis: verum
end;
for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 )
proof
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 )
A18: now__::_thesis:_for_r0_being_real_number_st_r0_>_0_holds_
ex_m_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_m_<=_n_holds_
abs_((((h_")_(#)_(R1_/*_h))_._n)_-_0)_<_r0
let r0 be real number ; ::_thesis: ( r0 > 0 implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs ((((h ") (#) (R1 /* h)) . n) - 0) < r0 )
reconsider r = r0 as Real by XREAL_0:def_1;
A19: lim h = 0 ;
assume r0 > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs ((((h ") (#) (R1 /* h)) . n) - 0) < r0
then consider d being Real such that
A20: d > 0 and
A21: for z1 being Real st z1 <> 0 & abs z1 < d holds
((abs z1) ") * (abs (R1 . z1)) < r by A6;
reconsider d1 = d as real number ;
consider m being Element of NAT such that
A22: for n being Element of NAT st m <= n holds
abs ((h . n) - 0) < d1 by A20, A19, SEQ_2:def_7;
take m = m; ::_thesis: for n being Element of NAT st m <= n holds
abs ((((h ") (#) (R1 /* h)) . n) - 0) < r0
hereby ::_thesis: verum
let n be Element of NAT ; ::_thesis: ( m <= n implies abs ((((h ") (#) (R1 /* h)) . n) - 0) < r0 )
A23: h . n <> 0 by SEQ_1:5;
rng h c= dom R1 by A5;
then A24: ((abs (h . n)) ") * (abs (R1 . (h . n))) = ((abs (h . n)) ") * (abs ((R1 /* h) . n)) by FUNCT_2:108
.= (((abs h) . n) ") * (abs ((R1 /* h) . n)) by SEQ_1:12
.= (((abs h) ") . n) * (abs ((R1 /* h) . n)) by VALUED_1:10
.= ((abs (h ")) . n) * (abs ((R1 /* h) . n)) by SEQ_1:54
.= (abs ((h ") . n)) * (abs ((R1 /* h) . n)) by SEQ_1:12
.= abs (((h ") . n) * ((R1 /* h) . n)) by COMPLEX1:65
.= abs ((((h ") (#) (R1 /* h)) . n) - 0) by SEQ_1:8 ;
assume m <= n ; ::_thesis: abs ((((h ") (#) (R1 /* h)) . n) - 0) < r0
then abs ((h . n) - 0) < d by A22;
hence abs ((((h ") (#) (R1 /* h)) . n) - 0) < r0 by A21, A23, A24; ::_thesis: verum
end;
end;
hence (h ") (#) (R1 /* h) is convergent by SEQ_2:def_6; ::_thesis: lim ((h ") (#) (R1 /* h)) = 0
hence lim ((h ") (#) (R1 /* h)) = 0 by A18, SEQ_2:def_7; ::_thesis: verum
end;
hence (J * R) * I is RestFunc by A4, FDIFF_1:def_2; ::_thesis: verum
end;
thus for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ::_thesis: verum
proof
let L be LinearOperator of (REAL-NS 1),(REAL-NS 1); ::_thesis: (J * L) * I is LinearFunc
A25: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4;
then reconsider L0 = L as Function of (REAL 1),(REAL 1) ;
reconsider L1 = (J * L0) * I as PartFunc of REAL,REAL ;
A26: dom (J * L0) = REAL 1 by FUNCT_2:def_1;
consider r being Real such that
A27: r = L1 . 1 ;
A28: dom ((J * L0) * I) = REAL by FUNCT_2:def_1;
A29: dom L0 = REAL 1 by FUNCT_2:def_1;
for p being Real holds L1 . p = r * p
proof
reconsider 1p = I . 1 as VECTOR of (REAL-NS 1) by REAL_NS1:def_4;
let p be Real; ::_thesis: L1 . p = r * p
dom I = REAL by FUNCT_2:def_1;
then L1 . p = (J * L) . (I . (p * 1)) by FUNCT_1:13;
then L1 . p = (J * L) . (p * 1p) by A1, Th3;
then L1 . p = J . (L . (p * 1p)) by A25, A29, FUNCT_1:13;
then L1 . p = J . (p * (L . 1p)) by LOPBAN_1:def_5;
then L1 . p = p * (J . (L . 1p)) by A2, Th4;
then L1 . p = p * ((J * L0) . (I . 1)) by A26, FUNCT_1:12;
hence L1 . p = r * p by A28, A27, FUNCT_1:12; ::_thesis: verum
end;
hence (J * L) * I is LinearFunc by FDIFF_1:def_3; ::_thesis: verum
end;
end;
theorem Th6: :: PDIFF_1:6
for I being Function of REAL,(REAL 1)
for J being Function of (REAL 1),REAL st I = (proj (1,1)) " & J = proj (1,1) holds
( ( for R being RestFunc holds (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) ) & ( for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) ) )
proof
let I be Function of REAL,(REAL 1); ::_thesis: for J being Function of (REAL 1),REAL st I = (proj (1,1)) " & J = proj (1,1) holds
( ( for R being RestFunc holds (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) ) & ( for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) ) )
let J be Function of (REAL 1),REAL; ::_thesis: ( I = (proj (1,1)) " & J = proj (1,1) implies ( ( for R being RestFunc holds (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) ) & ( for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) ) ) )
assume that
A1: I = (proj (1,1)) " and
A2: J = proj (1,1) ; ::_thesis: ( ( for R being RestFunc holds (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) ) & ( for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) ) )
thus for R being RestFunc holds (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) ::_thesis: for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1)
proof
let R be RestFunc; ::_thesis: (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1)
R is total by FDIFF_1:def_2;
then reconsider R0 = R as Function of REAL,REAL ;
A3: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4;
then reconsider R1 = (I * R0) * J as PartFunc of (REAL-NS 1),(REAL-NS 1) ;
for h being non-zero 0. (REAL-NS 1) -convergent sequence of (REAL-NS 1) holds
( (||.h.|| ") (#) (R1 /* h) is convergent & lim ((||.h.|| ") (#) (R1 /* h)) = 0. (REAL-NS 1) )
proof
let h be non-zero 0. (REAL-NS 1) -convergent sequence of (REAL-NS 1); ::_thesis: ( (||.h.|| ") (#) (R1 /* h) is convergent & lim ((||.h.|| ") (#) (R1 /* h)) = 0. (REAL-NS 1) )
A4: lim h = 0. (REAL-NS 1) by NDIFF_1:def_4;
deffunc H1( Element of NAT ) -> Element of REAL = J . (h . $1);
consider s being Real_Sequence such that
A5: for n being Element of NAT holds s . n = H1(n) from SEQ_1:sch_1();
A6: h is convergent by NDIFF_1:def_4;
A7: now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_
ex_m_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_m_<=_n_holds_
abs_((s_._n)_-_0)_<_p
let p be real number ; ::_thesis: ( 0 < p implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs ((s . n) - 0) < p )
A8: p is Real by XREAL_0:def_1;
assume 0 < p ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs ((s . n) - 0) < p
then consider m being Element of NAT such that
A9: for n being Element of NAT st m <= n holds
||.((h . n) - (0. (REAL-NS 1))).|| < p by A6, A4, A8, NORMSP_1:def_7;
take m = m; ::_thesis: for n being Element of NAT st m <= n holds
abs ((s . n) - 0) < p
now__::_thesis:_for_n_being_Element_of_NAT_st_m_<=_n_holds_
abs_((s_._n)_-_0)_<_p
let n be Element of NAT ; ::_thesis: ( m <= n implies abs ((s . n) - 0) < p )
assume m <= n ; ::_thesis: abs ((s . n) - 0) < p
then ||.((h . n) - (0. (REAL-NS 1))).|| < p by A9;
then A10: ||.(h . n).|| < p by RLVECT_1:13;
s . n = J . (h . n) by A5;
hence abs ((s . n) - 0) < p by A2, A10, Th4; ::_thesis: verum
end;
hence for n being Element of NAT st m <= n holds
abs ((s . n) - 0) < p ; ::_thesis: verum
end;
then A11: s is convergent by SEQ_2:def_6;
then A12: lim s = 0 by A7, SEQ_2:def_7;
now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
s_._x_<>_0
let x be set ; ::_thesis: ( x in NAT implies s . x <> 0 )
assume x in NAT ; ::_thesis: s . x <> 0
then reconsider n = x as Element of NAT ;
A13: 0 <= abs (s . n) by COMPLEX1:46;
h . n <> 0. (REAL-NS 1) by NDIFF_1:6;
then A14: ||.(h . n).|| <> 0 by NORMSP_0:def_5;
s . n = J . (h . n) by A5;
then abs (s . n) <> 0 by A2, A14, Th4;
hence s . x <> 0 by A13, COMPLEX1:47; ::_thesis: verum
end;
then s is non-zero by SEQ_1:4;
then reconsider s = s as non-zero 0 -convergent Real_Sequence by A11, A12, FDIFF_1:def_1;
A15: J * I = id REAL by A1, A2, Lm1, FUNCT_1:39;
now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((||.h.||_")_(#)_(R1_/*_h)).||_._n_=_(abs_((s_")_(#)_(R_/*_s)))_._n
reconsider f1 = R1 as Function ;
let n be Element of NAT ; ::_thesis: ||.((||.h.|| ") (#) (R1 /* h)).|| . n = (abs ((s ") (#) (R /* s))) . n
A16: rng h c= the carrier of (REAL-NS 1) ;
h . n in the carrier of (REAL-NS 1) ;
then A17: h . n in REAL 1 by REAL_NS1:def_4;
R1 is total by A3;
then (R /* s) . n = R . (s . n) by FUNCT_2:115;
then (R /* s) . n = R . (J . (h . n)) by A5;
then (R /* s) . n = (J * I) . (R0 . (J . (h . n))) by A15, FUNCT_1:18;
then (R /* s) . n = (J * I) . ((R0 * J) . (h . n)) by A17, FUNCT_2:15;
then (R /* s) . n = J . (I . ((R0 * J) . (h . n))) by FUNCT_2:15;
then A18: (R /* s) . n = J . ((I * (R0 * J)) . (h . n)) by A17, FUNCT_2:15;
NAT = dom h by FUNCT_2:def_1;
then A19: R1 . (h . n) = (f1 * h) . n by FUNCT_1:13;
dom R1 = REAL 1 by FUNCT_2:def_1;
then rng h c= dom R1 by A16, REAL_NS1:def_4;
then R1 . (h . n) = (R1 /* h) . n by A19, FUNCT_2:def_11;
then A20: (R /* s) . n = J . ((R1 /* h) . n) by A18, RELAT_1:36;
A21: ||.(h . n).|| >= 0 by NORMSP_1:4;
A22: s . n = J . (h . n) by A5;
||.((||.h.|| ") (#) (R1 /* h)).|| . n = ||.(((||.h.|| ") (#) (R1 /* h)) . n).|| by NORMSP_0:def_4
.= ||.(((||.h.|| ") . n) * ((R1 /* h) . n)).|| by NDIFF_1:def_2
.= (abs ((||.h.|| ") . n)) * ||.((R1 /* h) . n).|| by NORMSP_1:def_1
.= (abs ((||.h.|| . n) ")) * ||.((R1 /* h) . n).|| by VALUED_1:10
.= (abs (||.(h . n).|| ")) * ||.((R1 /* h) . n).|| by NORMSP_0:def_4
.= (||.(h . n).|| ") * ||.((R1 /* h) . n).|| by A21, ABSVALUE:def_1
.= ((abs (s . n)) ") * ||.((R1 /* h) . n).|| by A2, A22, Th4
.= ((abs (s . n)) ") * (abs ((R /* s) . n)) by A2, A20, Th4
.= ((abs (s . n)) ") * ((abs (R /* s)) . n) by SEQ_1:12
.= (((abs s) . n) ") * ((abs (R /* s)) . n) by SEQ_1:12
.= (((abs s) ") . n) * ((abs (R /* s)) . n) by VALUED_1:10
.= (((abs s) ") (#) (abs (R /* s))) . n by SEQ_1:8
.= ((abs (s ")) (#) (abs (R /* s))) . n by SEQ_1:54 ;
hence ||.((||.h.|| ") (#) (R1 /* h)).|| . n = (abs ((s ") (#) (R /* s))) . n by SEQ_1:52; ::_thesis: verum
end;
then A23: ||.((||.h.|| ") (#) (R1 /* h)).|| = abs ((s ") (#) (R /* s)) by FUNCT_2:63;
A24: lim ((s ") (#) (R /* s)) = 0 by FDIFF_1:def_2;
A25: (s ") (#) (R /* s) is convergent by FDIFF_1:def_2;
then lim (abs ((s ") (#) (R /* s))) = abs (lim ((s ") (#) (R /* s))) by SEQ_4:14;
then A26: lim (abs ((s ") (#) (R /* s))) = 0 by A24, ABSVALUE:2;
A27: abs ((s ") (#) (R /* s)) is convergent by A25, SEQ_4:13;
A28: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_m_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_m_<=_n_holds_
||.((((||.h.||_")_(#)_(R1_/*_h))_._n)_-_(0._(REAL-NS_1))).||_<_p
let p be Real; ::_thesis: ( 0 < p implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p )
assume 0 < p ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p
then consider m being Element of NAT such that
A29: for n being Element of NAT st m <= n holds
abs ((||.((||.h.|| ") (#) (R1 /* h)).|| . n) - 0) < p by A23, A27, A26, SEQ_2:def_7;
take m = m; ::_thesis: for n being Element of NAT st m <= n holds
||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p
hereby ::_thesis: verum
let n be Element of NAT ; ::_thesis: ( m <= n implies ||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p )
assume m <= n ; ::_thesis: ||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p
then abs ((||.((||.h.|| ") (#) (R1 /* h)).|| . n) - 0) < p by A29;
then A30: abs ||.(((||.h.|| ") (#) (R1 /* h)) . n).|| < p by NORMSP_0:def_4;
0 <= ||.(((||.h.|| ") (#) (R1 /* h)) . n).|| by NORMSP_1:4;
then ||.(((||.h.|| ") (#) (R1 /* h)) . n).|| < p by A30, ABSVALUE:def_1;
hence ||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p by RLVECT_1:13; ::_thesis: verum
end;
end;
then (||.h.|| ") (#) (R1 /* h) is convergent by NORMSP_1:def_6;
hence ( (||.h.|| ") (#) (R1 /* h) is convergent & lim ((||.h.|| ") (#) (R1 /* h)) = 0. (REAL-NS 1) ) by A28, NORMSP_1:def_7; ::_thesis: verum
end;
hence (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) by A3, NDIFF_1:def_5; ::_thesis: verum
end;
thus for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) ::_thesis: verum
proof
let L be LinearFunc; ::_thesis: (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1)
consider r being Real such that
A31: for p being Real holds L . p = r * p by FDIFF_1:def_3;
L is total by FDIFF_1:def_3;
then reconsider L0 = L as Function of REAL,REAL ;
set K = abs r;
A32: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4;
(I * L0) * J is Function of (REAL 1),(REAL 1) ;
then reconsider L1 = (I * L) * J as Function of (REAL-NS 1),(REAL-NS 1) by A32;
A33: dom L1 = REAL 1 by A32, FUNCT_2:def_1;
A34: dom L0 = REAL by FUNCT_2:def_1;
A35: now__::_thesis:_for_x,_y_being_VECTOR_of_(REAL-NS_1)_holds_L1_._(x_+_y)_=_(L1_._x)_+_(L1_._y)
let x, y be VECTOR of (REAL-NS 1); ::_thesis: L1 . (x + y) = (L1 . x) + (L1 . y)
I . (L . (J . y)) = (I * L) . (J . y) by A34, FUNCT_1:13;
then A36: I . (L . (J . y)) = L1 . y by A32, A33, FUNCT_1:12;
L1 . (x + y) = (I * L) . (J . (x + y)) by A32, A33, FUNCT_1:12;
then L1 . (x + y) = (I * L) . ((J . x) + (J . y)) by A2, Th4;
then L1 . (x + y) = I . (L . ((J . x) + (J . y))) by A34, FUNCT_1:13;
then L1 . (x + y) = I . (r * ((J . x) + (J . y))) by A31;
then L1 . (x + y) = I . ((r * (J . x)) + (r * (J . y))) ;
then L1 . (x + y) = I . ((L . (J . x)) + (r * (J . y))) by A31;
then A37: L1 . (x + y) = I . ((L . (J . x)) + (L . (J . y))) by A31;
I . (L . (J . x)) = (I * L) . (J . x) by A34, FUNCT_1:13;
then I . (L . (J . x)) = L1 . x by A32, A33, FUNCT_1:12;
hence L1 . (x + y) = (L1 . x) + (L1 . y) by A1, A36, A37, Th3; ::_thesis: verum
end;
now__::_thesis:_for_x_being_VECTOR_of_(REAL-NS_1)
for_a_being_Real_holds_L1_._(a_*_x)_=_a_*_(L1_._x)
let x be VECTOR of (REAL-NS 1); ::_thesis: for a being Real holds L1 . (a * x) = a * (L1 . x)
let a be Real; ::_thesis: L1 . (a * x) = a * (L1 . x)
L1 . (a * x) = (I * L) . (J . (a * x)) by A32, A33, FUNCT_1:12;
then L1 . (a * x) = (I * L) . (a * (J . x)) by A2, Th4;
then L1 . (a * x) = I . (L . (a * (J . x))) by A34, FUNCT_1:13;
then L1 . (a * x) = I . (r * (a * (J . x))) by A31;
then L1 . (a * x) = I . (a * (r * (J . x))) ;
then A38: L1 . (a * x) = I . (a * (L . (J . x))) by A31;
I . (L . (J . x)) = (I * L) . (J . x) by A34, FUNCT_1:13;
then I . (L . (J . x)) = L1 . x by A32, A33, FUNCT_1:12;
hence L1 . (a * x) = a * (L1 . x) by A1, A38, Th3; ::_thesis: verum
end;
then reconsider L1 = L1 as LinearOperator of (REAL-NS 1),(REAL-NS 1) by A35, VECTSP_1:def_20, LOPBAN_1:def_5;
A39: now__::_thesis:_for_x_being_VECTOR_of_(REAL-NS_1)_holds_||.(L1_._x).||_<=_(abs_r)_*_||.x.||
let x be VECTOR of (REAL-NS 1); ::_thesis: ||.(L1 . x).|| <= (abs r) * ||.x.||
I . (L . (J . x)) = (I * L) . (J . x) by A34, FUNCT_1:13;
then I . (L . (J . x)) = L1 . x by A32, A33, FUNCT_1:12;
then ||.(L1 . x).|| = abs (L . (J . x)) by A1, Th3;
then ||.(L1 . x).|| = abs (r * (J . x)) by A31;
then ||.(L1 . x).|| = (abs r) * (abs (J . x)) by COMPLEX1:65;
hence ||.(L1 . x).|| <= (abs r) * ||.x.|| by A2, Th4; ::_thesis: verum
end;
0 <= abs r by COMPLEX1:46;
hence (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) by A39, LOPBAN_1:def_8; ::_thesis: verum
end;
end;
theorem Th7: :: PDIFF_1:7
for f being PartFunc of (REAL-NS 1),(REAL-NS 1)
for g being PartFunc of REAL,REAL
for x being Point of (REAL-NS 1)
for y being Element of REAL st f = <>* g & x = <*y*> & f is_differentiable_in x holds
( g is_differentiable_in y & diff (g,y) = (((proj (1,1)) * (diff (f,x))) * ((proj (1,1)) ")) . 1 )
proof
let f be PartFunc of (REAL-NS 1),(REAL-NS 1); ::_thesis: for g being PartFunc of REAL,REAL
for x being Point of (REAL-NS 1)
for y being Element of REAL st f = <>* g & x = <*y*> & f is_differentiable_in x holds
( g is_differentiable_in y & diff (g,y) = (((proj (1,1)) * (diff (f,x))) * ((proj (1,1)) ")) . 1 )
let g be PartFunc of REAL,REAL; ::_thesis: for x being Point of (REAL-NS 1)
for y being Element of REAL st f = <>* g & x = <*y*> & f is_differentiable_in x holds
( g is_differentiable_in y & diff (g,y) = (((proj (1,1)) * (diff (f,x))) * ((proj (1,1)) ")) . 1 )
let x be Point of (REAL-NS 1); ::_thesis: for y being Element of REAL st f = <>* g & x = <*y*> & f is_differentiable_in x holds
( g is_differentiable_in y & diff (g,y) = (((proj (1,1)) * (diff (f,x))) * ((proj (1,1)) ")) . 1 )
let y be Element of REAL ; ::_thesis: ( f = <>* g & x = <*y*> & f is_differentiable_in x implies ( g is_differentiable_in y & diff (g,y) = (((proj (1,1)) * (diff (f,x))) * ((proj (1,1)) ")) . 1 ) )
set J = proj (1,1);
reconsider L = diff (f,x) as Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) by LOPBAN_1:def_9;
A1: rng g c= dom I by Th2;
reconsider L0 = ((proj (1,1)) * L) * I as LinearFunc by Th5;
assume that
A2: f = <>* g and
A3: x = <*y*> and
A4: f is_differentiable_in x ; ::_thesis: ( g is_differentiable_in y & diff (g,y) = (((proj (1,1)) * (diff (f,x))) * ((proj (1,1)) ")) . 1 )
consider NN being Neighbourhood of x such that
A5: NN c= dom f and
A6: ex R being RestFunc of (REAL-NS 1),(REAL-NS 1) st
for y being Point of (REAL-NS 1) st y in NN holds
(f /. y) - (f /. x) = ((diff (f,x)) . (y - x)) + (R /. (y - x)) by A4, NDIFF_1:def_7;
consider e being Real such that
A7: 0 < e and
A8: { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } c= NN by NFCONT_1:def_1;
consider R being RestFunc of (REAL-NS 1),(REAL-NS 1) such that
A9: for x9 being Point of (REAL-NS 1) st x9 in NN holds
(f /. x9) - (f /. x) = ((diff (f,x)) . (x9 - x)) + (R /. (x9 - x)) by A6;
set N = { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ;
A10: { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } c= the carrier of (REAL-NS 1)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } or y in the carrier of (REAL-NS 1) )
assume y in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ; ::_thesis: y in the carrier of (REAL-NS 1)
then ex z being Point of (REAL-NS 1) st
( y = z & ||.(z - x).|| < e ) ;
hence y in the carrier of (REAL-NS 1) ; ::_thesis: verum
end;
then reconsider N = { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } as Neighbourhood of x by A7, NFCONT_1:def_1;
set N0 = { z where z is Element of REAL : abs (z - y) < e } ;
A11: N c= dom f by A5, A8, XBOOLE_1:1;
now__::_thesis:_for_z_being_set_holds_
(_(_z_in__{__z_where_z_is_Element_of_REAL_:_abs_(z_-_y)_<_e__}__implies_z_in_(proj_(1,1))_.:_N_)_&_(_z_in_(proj_(1,1))_.:_N_implies_z_in__{__z_where_z_is_Element_of_REAL_:_abs_(z_-_y)_<_e__}__)_)
let z be set ; ::_thesis: ( ( z in { z where z is Element of REAL : abs (z - y) < e } implies z in (proj (1,1)) .: N ) & ( z in (proj (1,1)) .: N implies z in { z where z is Element of REAL : abs (z - y) < e } ) )
hereby ::_thesis: ( z in (proj (1,1)) .: N implies z in { z where z is Element of REAL : abs (z - y) < e } )
assume z in { z where z is Element of REAL : abs (z - y) < e } ; ::_thesis: z in (proj (1,1)) .: N
then consider y9 being Element of REAL such that
A12: z = y9 and
A13: abs (y9 - y) < e ;
reconsider w = I . y9 as Point of (REAL-NS 1) by REAL_NS1:def_4;
x = I . y by A3, Lm1;
then w - x = I . (y9 - y) by Th3;
then ||.(w - x).|| = abs (y9 - y) by Th3;
then w in { z0 where z0 is Point of (REAL-NS 1) : ||.(z0 - x).|| < e } by A13;
then (proj (1,1)) . w in (proj (1,1)) .: N by FUNCT_2:35;
hence z in (proj (1,1)) .: N by A12, Lm1, FUNCT_1:35; ::_thesis: verum
end;
assume z in (proj (1,1)) .: N ; ::_thesis: z in { z where z is Element of REAL : abs (z - y) < e }
then consider ww being set such that
ww in REAL 1 and
A14: ww in N and
A15: z = (proj (1,1)) . ww by FUNCT_2:64;
consider w being Point of (REAL-NS 1) such that
A16: ww = w and
A17: ||.(w - x).|| < e by A14;
reconsider y9 = (proj (1,1)) . w as Element of REAL ;
(proj (1,1)) . x = y by A3, Lm1;
then (proj (1,1)) . (w - x) = y9 - y by Th4;
then abs (y9 - y) < e by A17, Th4;
hence z in { z where z is Element of REAL : abs (z - y) < e } by A15, A16; ::_thesis: verum
end;
then A18: { z where z is Element of REAL : abs (z - y) < e } = (proj (1,1)) .: N by TARSKI:1;
dom f = (proj (1,1)) " (dom (I * g)) by A2, RELAT_1:147;
then (proj (1,1)) .: (dom f) = (proj (1,1)) .: ((proj (1,1)) " (dom g)) by A1, RELAT_1:27;
then A19: (proj (1,1)) .: (dom f) = dom g by Lm1, FUNCT_1:77;
A20: I * (proj (1,1)) = id (REAL 1) by Lm1, FUNCT_1:39;
reconsider R0 = ((proj (1,1)) * R) * I as RestFunc by Th5;
A21: (proj (1,1)) * I = id REAL by Lm1, FUNCT_1:39;
N c= dom f by A5, A8, XBOOLE_1:1;
then A22: { z where z is Element of REAL : abs (z - y) < e } c= dom g by A19, A18, RELAT_1:123;
A23: ].(y - e),(y + e).[ c= { z where z is Element of REAL : abs (z - y) < e }
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in ].(y - e),(y + e).[ or d in { z where z is Element of REAL : abs (z - y) < e } )
assume A24: d in ].(y - e),(y + e).[ ; ::_thesis: d in { z where z is Element of REAL : abs (z - y) < e }
reconsider y0 = d as Element of REAL by A24;
abs (y0 - y) < e by A24, RCOMP_1:1;
hence d in { z where z is Element of REAL : abs (z - y) < e } ; ::_thesis: verum
end;
{ z where z is Element of REAL : abs (z - y) < e } c= ].(y - e),(y + e).[
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in { z where z is Element of REAL : abs (z - y) < e } or d in ].(y - e),(y + e).[ )
assume d in { z where z is Element of REAL : abs (z - y) < e } ; ::_thesis: d in ].(y - e),(y + e).[
then ex r being Element of REAL st
( d = r & abs (r - y) < e ) ;
hence d in ].(y - e),(y + e).[ by RCOMP_1:1; ::_thesis: verum
end;
then { z where z is Element of REAL : abs (z - y) < e } = ].(y - e),(y + e).[ by A23, XBOOLE_0:def_10;
then A25: { z where z is Element of REAL : abs (z - y) < e } is Neighbourhood of y by A7, RCOMP_1:def_6;
N c= REAL 1 by A10, REAL_NS1:def_4;
then (I * (proj (1,1))) .: N = N by A20, FRECHET:13;
then A26: I .: { z where z is Element of REAL : abs (z - y) < e } = N by A18, RELAT_1:126;
A27: for y0 being Real st y0 in { z where z is Element of REAL : abs (z - y) < e } holds
(g . y0) - (g . y) = (L0 . (y0 - y)) + (R0 . (y0 - y))
proof
let y0 be Real; ::_thesis: ( y0 in { z where z is Element of REAL : abs (z - y) < e } implies (g . y0) - (g . y) = (L0 . (y0 - y)) + (R0 . (y0 - y)) )
reconsider y9 = I . y0 as Point of (REAL-NS 1) by REAL_NS1:def_4;
R is total by NDIFF_1:def_5;
then A28: dom R = the carrier of (REAL-NS 1) by PARTFUN1:def_2;
R0 is total by FDIFF_1:def_2;
then dom (((proj (1,1)) * R) * I) = REAL by PARTFUN1:def_2;
then y0 - y in dom (((proj (1,1)) * R) * I) ;
then A29: y0 - y in dom ((proj (1,1)) * (R * I)) by RELAT_1:36;
I . (y0 - y) in REAL 1 ;
then I . (y0 - y) in dom R by A28, REAL_NS1:def_4;
then (proj (1,1)) . (R /. (I . (y0 - y))) = (proj (1,1)) . (R . (I . (y0 - y))) by PARTFUN1:def_6;
then (proj (1,1)) . (R /. (I . (y0 - y))) = (proj (1,1)) . ((R * I) . (y0 - y)) by Th2, FUNCT_1:13;
then (proj (1,1)) . (R /. (I . (y0 - y))) = ((proj (1,1)) * (R * I)) . (y0 - y) by A29, FUNCT_1:12;
then A30: (proj (1,1)) . (R /. (I . (y0 - y))) = R0 . (y0 - y) by RELAT_1:36;
L0 is total by FDIFF_1:def_3;
then dom (((proj (1,1)) * L) * I) = REAL by PARTFUN1:def_2;
then y0 - y in dom (((proj (1,1)) * L) * I) ;
then A31: y0 - y in dom ((proj (1,1)) * (L * I)) by RELAT_1:36;
assume A32: y0 in { z where z is Element of REAL : abs (z - y) < e } ; ::_thesis: (g . y0) - (g . y) = (L0 . (y0 - y)) + (R0 . (y0 - y))
then A33: I . y0 in N by A26, FUNCT_2:35;
then (proj (1,1)) . (f /. (I . y0)) = (proj (1,1)) . (f . (I . y0)) by A11, PARTFUN1:def_6;
then A34: (proj (1,1)) . (f /. (I . y0)) = (proj (1,1)) . ((f * I) . y0) by Th2, FUNCT_1:13;
(proj (1,1)) * f = (proj (1,1)) * (I * (g * (proj (1,1)))) by A2, RELAT_1:36;
then A35: (proj (1,1)) * f = (id REAL) * (g * (proj (1,1))) by A21, RELAT_1:36;
rng (g * (proj (1,1))) c= REAL ;
then ((proj (1,1)) * f) * I = (g * (proj (1,1))) * I by A35, RELAT_1:53;
then A36: ((proj (1,1)) * f) * I = g * (id REAL) by A21, RELAT_1:36;
dom g c= REAL ;
then A37: g = ((proj (1,1)) * f) * I by A36, RELAT_1:51;
y0 in dom g by A22, A32;
then y0 in dom ((proj (1,1)) * (f * I)) by A37, RELAT_1:36;
then (proj (1,1)) . (f /. (I . y0)) = ((proj (1,1)) * (f * I)) . y0 by A34, FUNCT_1:12;
then A38: (proj (1,1)) . (f /. (I . y0)) = g . y0 by A37, RELAT_1:36;
A39: x = I . y by A3, Lm1;
x in N by NFCONT_1:4;
then (proj (1,1)) . (f /. (I . y)) = (proj (1,1)) . (f . (I . y)) by A11, A39, PARTFUN1:def_6;
then A40: (proj (1,1)) . (f /. (I . y)) = (proj (1,1)) . ((f * I) . y) by Th2, FUNCT_1:13;
y in { z where z is Element of REAL : abs (z - y) < e } by A25, RCOMP_1:16;
then y in dom g by A22;
then y in dom ((proj (1,1)) * (f * I)) by A37, RELAT_1:36;
then (proj (1,1)) . (f /. (I . y)) = ((proj (1,1)) * (f * I)) . y by A40, FUNCT_1:12;
then A41: (proj (1,1)) . (f /. (I . y)) = g . y by A37, RELAT_1:36;
(proj (1,1)) . ((f /. y9) - (f /. x)) = (proj (1,1)) . ((L . (y9 - x)) + (R /. (y9 - x))) by A9, A8, A33;
then ((proj (1,1)) . (f /. y9)) - ((proj (1,1)) . (f /. x)) = (proj (1,1)) . ((L . (y9 - x)) + (R /. (y9 - x))) by Th4;
then ((proj (1,1)) . (f /. (I . y0))) - ((proj (1,1)) . (f /. (I . y))) = ((proj (1,1)) . (L . (y9 - x))) + ((proj (1,1)) . (R /. (y9 - x))) by A39, Th4;
then A42: ((proj (1,1)) . (f /. (I . y0))) - ((proj (1,1)) . (f /. (I . y))) = ((proj (1,1)) . (L . (I . (y0 - y)))) + ((proj (1,1)) . (R /. (y9 - x))) by A39, Th3;
(proj (1,1)) . (L . (I . (y0 - y))) = (proj (1,1)) . ((L * I) . (y0 - y)) by Th2, FUNCT_1:13;
then (proj (1,1)) . (L . (I . (y0 - y))) = ((proj (1,1)) * (L * I)) . (y0 - y) by A31, FUNCT_1:12;
then (proj (1,1)) . (L . (I . (y0 - y))) = L0 . (y0 - y) by RELAT_1:36;
hence (g . y0) - (g . y) = (L0 . (y0 - y)) + (R0 . (y0 - y)) by A39, A42, A38, A41, A30, Th3; ::_thesis: verum
end;
hence g is_differentiable_in y by A25, A22, FDIFF_1:def_4; ::_thesis: diff (g,y) = (((proj (1,1)) * (diff (f,x))) * ((proj (1,1)) ")) . 1
hence diff (g,y) = (((proj (1,1)) * (diff (f,x))) * ((proj (1,1)) ")) . 1 by A25, A22, A27, FDIFF_1:def_5; ::_thesis: verum
end;
theorem Th8: :: PDIFF_1:8
for f being PartFunc of (REAL-NS 1),(REAL-NS 1)
for g being PartFunc of REAL,REAL
for x being Point of (REAL-NS 1)
for y being Element of REAL st f = <>* g & x = <*y*> & g is_differentiable_in y holds
( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> )
proof
let f be PartFunc of (REAL-NS 1),(REAL-NS 1); ::_thesis: for g being PartFunc of REAL,REAL
for x being Point of (REAL-NS 1)
for y being Element of REAL st f = <>* g & x = <*y*> & g is_differentiable_in y holds
( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> )
let g be PartFunc of REAL,REAL; ::_thesis: for x being Point of (REAL-NS 1)
for y being Element of REAL st f = <>* g & x = <*y*> & g is_differentiable_in y holds
( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> )
let x be Point of (REAL-NS 1); ::_thesis: for y being Element of REAL st f = <>* g & x = <*y*> & g is_differentiable_in y holds
( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> )
let y be Element of REAL ; ::_thesis: ( f = <>* g & x = <*y*> & g is_differentiable_in y implies ( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> ) )
set J = proj (1,1);
assume that
A1: f = <>* g and
A2: x = <*y*> and
A3: g is_differentiable_in y ; ::_thesis: ( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> )
reconsider x0 = y as Real ;
consider N0 being Neighbourhood of x0 such that
A4: N0 c= dom g and
A5: ex L0 being LinearFunc ex R0 being RestFunc st
( diff (g,x0) = L0 . 1 & ( for y0 being Real st y0 in N0 holds
(g . y0) - (g . x0) = (L0 . (y0 - x0)) + (R0 . (y0 - x0)) ) ) by A3, FDIFF_1:def_5;
consider e0 being real number such that
A6: 0 < e0 and
A7: N0 = ].(x0 - e0),(x0 + e0).[ by RCOMP_1:def_6;
reconsider e = e0 as Real by XREAL_0:def_1;
set N = { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ;
A8: rng (g * (proj (1,1))) c= REAL ;
consider L0 being LinearFunc, R0 being RestFunc such that
A9: diff (g,x0) = L0 . 1 and
A10: for y0 being Real st y0 in N0 holds
(g . y0) - (g . x0) = (L0 . (y0 - x0)) + (R0 . (y0 - x0)) by A5;
reconsider R = (I * R0) * (proj (1,1)) as RestFunc of (REAL-NS 1),(REAL-NS 1) by Th6;
reconsider L = (I * L0) * (proj (1,1)) as Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) by Th6;
A11: dom g c= REAL ;
dom f c= the carrier of (REAL-NS 1) ;
then A12: dom f c= rng I by Th2, REAL_NS1:def_4;
A13: (proj (1,1)) * I = id REAL by Lm1, FUNCT_1:39;
now__::_thesis:_for_z_being_set_holds_
(_(_z_in__{__z_where_z_is_Point_of_(REAL-NS_1)_:_||.(z_-_x).||_<_e__}__implies_z_in_I_.:_N0_)_&_(_z_in_I_.:_N0_implies_z_in__{__z_where_z_is_Point_of_(REAL-NS_1)_:_||.(z_-_x).||_<_e__}__)_)
let z be set ; ::_thesis: ( ( z in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } implies z in I .: N0 ) & ( z in I .: N0 implies z in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ) )
hereby ::_thesis: ( z in I .: N0 implies z in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } )
assume z in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ; ::_thesis: z in I .: N0
then consider w being Point of (REAL-NS 1) such that
A14: z = w and
A15: ||.(w - x).|| < e ;
reconsider y = (proj (1,1)) . w as Element of REAL ;
(proj (1,1)) . x = x0 by A2, Lm1;
then (proj (1,1)) . (w - x) = y - x0 by Th4;
then abs (y - x0) < e by A15, Th4;
then A16: y in N0 by A7, RCOMP_1:1;
w in the carrier of (REAL-NS 1) ;
then w in dom (proj (1,1)) by Lm1, REAL_NS1:def_4;
then w = I . y by FUNCT_1:34;
hence z in I .: N0 by A14, A16, FUNCT_2:35; ::_thesis: verum
end;
assume z in I .: N0 ; ::_thesis: z in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e }
then consider yy being set such that
A17: yy in REAL and
A18: yy in N0 and
A19: z = I . yy by FUNCT_2:64;
reconsider y = yy as Element of REAL by A17;
reconsider w = I . y as Point of (REAL-NS 1) by REAL_NS1:def_4;
I . x0 = x by A2, Lm1;
then A20: w - x = I . (y - x0) by Th3;
abs (y - x0) < e by A7, A18, RCOMP_1:1;
then ||.(w - x).|| < e by A20, Th3;
hence z in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } by A19; ::_thesis: verum
end;
then A21: { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } = I .: N0 by TARSKI:1;
(proj (1,1)) * f = (proj (1,1)) * (I * (g * (proj (1,1)))) by A1, RELAT_1:36;
then (proj (1,1)) * f = (id REAL) * (g * (proj (1,1))) by A13, RELAT_1:36;
then ((proj (1,1)) * f) * I = (g * (proj (1,1))) * I by A8, RELAT_1:53;
then ((proj (1,1)) * f) * I = g * (id REAL) by A13, RELAT_1:36;
then g = ((proj (1,1)) * f) * I by A11, RELAT_1:51;
then A22: dom g = I " (dom ((proj (1,1)) * f)) by RELAT_1:147;
rng f c= the carrier of (REAL-NS 1) ;
then rng f c= dom (proj (1,1)) by Lm1, REAL_NS1:def_4;
then I .: (dom g) = I .: (I " (dom f)) by A22, RELAT_1:27;
then I .: (dom g) = dom f by A12, FUNCT_1:77;
then A23: { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } c= dom f by A4, A21, RELAT_1:123;
{ z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } c= the carrier of (REAL-NS 1)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } or y in the carrier of (REAL-NS 1) )
assume y in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ; ::_thesis: y in the carrier of (REAL-NS 1)
then ex z being Point of (REAL-NS 1) st
( y = z & ||.(z - x).|| < e ) ;
hence y in the carrier of (REAL-NS 1) ; ::_thesis: verum
end;
then A24: { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } is Neighbourhood of x by A6, NFCONT_1:def_1;
(proj (1,1)) * I = id REAL by Lm1, FUNCT_1:39;
then ((proj (1,1)) * I) .: N0 = N0 by FRECHET:13;
then A25: (proj (1,1)) .: { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } = N0 by A21, RELAT_1:126;
A26: for y being Point of (REAL-NS 1) st y in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } holds
(f /. y) - (f /. x) = (L . (y - x)) + (R /. (y - x))
proof
x in the carrier of (REAL-NS 1) ;
then x in dom (proj (1,1)) by Lm1, REAL_NS1:def_4;
then A27: I . (g . ((proj (1,1)) . x)) = I . ((g * (proj (1,1))) . x) by FUNCT_1:13;
A28: x in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } by A24, NFCONT_1:4;
then x in dom f by A23;
then x in dom (I * (g * (proj (1,1)))) by A1, RELAT_1:36;
then I . (g . ((proj (1,1)) . x)) = (I * (g * (proj (1,1)))) . x by A27, FUNCT_1:12;
then I . (g . ((proj (1,1)) . x)) = f . x by A1, RELAT_1:36;
then A29: I . (g . ((proj (1,1)) . x)) = f /. x by A23, A28, PARTFUN1:def_6;
let y be Point of (REAL-NS 1); ::_thesis: ( y in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } implies (f /. y) - (f /. x) = (L . (y - x)) + (R /. (y - x)) )
assume A30: y in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ; ::_thesis: (f /. y) - (f /. x) = (L . (y - x)) + (R /. (y - x))
reconsider y0 = (proj (1,1)) . y as Element of REAL ;
reconsider p1 = I . (g . y0), p2 = I . (g . x0), q1 = I . (L0 . (y0 - x0)), q2 = I . (R0 . (y0 - x0)) as VECTOR of (REAL-NS 1) by REAL_NS1:def_4;
A31: (proj (1,1)) . x = x0 by A2, Lm1;
y in the carrier of (REAL-NS 1) ;
then y in REAL 1 by REAL_NS1:def_4;
then I . ((g . y0) - (g . x0)) = I . ((L0 . (y0 - x0)) + (R0 . (y0 - x0))) by A10, A25, A30, FUNCT_2:35;
then p1 - p2 = I . ((L0 . (y0 - x0)) + (R0 . (y0 - x0))) by Th3;
then p1 - p2 = q1 + q2 by Th3;
then (I . (g . y0)) - (I . (g . x0)) = q1 + q2 by REAL_NS1:5;
then (I . (g . ((proj (1,1)) . y))) - (I . (g . ((proj (1,1)) . x))) = (I . (L0 . (y0 - x0))) + (I . (R0 . (y0 - x0))) by A31, REAL_NS1:2;
then (I . (g . ((proj (1,1)) . y))) - (I . (g . ((proj (1,1)) . x))) = (I . (L0 . ((proj (1,1)) . (y - x)))) + (I . (R0 . (y0 - x0))) by A31, Th4;
then A32: (I . (g . ((proj (1,1)) . y))) - (I . (g . ((proj (1,1)) . x))) = (I . (L0 . ((proj (1,1)) . (y - x)))) + (I . (R0 . ((proj (1,1)) . (y - x)))) by A31, Th4;
dom L = the carrier of (REAL-NS 1) by FUNCT_2:def_1;
then y - x in dom ((I * L0) * (proj (1,1))) ;
then A33: y - x in dom (I * (L0 * (proj (1,1)))) by RELAT_1:36;
y - x in the carrier of (REAL-NS 1) ;
then A34: y - x in dom (proj (1,1)) by Lm1, REAL_NS1:def_4;
then A35: I . (R0 . ((proj (1,1)) . (y - x))) = I . ((R0 * (proj (1,1))) . (y - x)) by FUNCT_1:13;
R is total by NDIFF_1:def_5;
then A36: dom ((I * R0) * (proj (1,1))) = the carrier of (REAL-NS 1) by PARTFUN1:def_2;
then y - x in dom ((I * R0) * (proj (1,1))) ;
then y - x in dom (I * (R0 * (proj (1,1)))) by RELAT_1:36;
then I . (R0 . ((proj (1,1)) . (y - x))) = (I * (R0 * (proj (1,1)))) . (y - x) by A35, FUNCT_1:12;
then I . (R0 . ((proj (1,1)) . (y - x))) = ((I * R0) * (proj (1,1))) . (y - x) by RELAT_1:36;
then A37: I . (R0 . ((proj (1,1)) . (y - x))) = R /. (y - x) by A36, PARTFUN1:def_6;
y in the carrier of (REAL-NS 1) ;
then y in dom (proj (1,1)) by Lm1, REAL_NS1:def_4;
then A38: I . (g . ((proj (1,1)) . y)) = I . ((g * (proj (1,1))) . y) by FUNCT_1:13;
I . (L0 . ((proj (1,1)) . (y - x))) = I . ((L0 * (proj (1,1))) . (y - x)) by A34, FUNCT_1:13;
then I . (L0 . ((proj (1,1)) . (y - x))) = (I * (L0 * (proj (1,1)))) . (y - x) by A33, FUNCT_1:12;
then A39: I . (L0 . ((proj (1,1)) . (y - x))) = L . (y - x) by RELAT_1:36;
y in dom f by A23, A30;
then y in dom (I * (g * (proj (1,1)))) by A1, RELAT_1:36;
then I . (g . ((proj (1,1)) . y)) = (I * (g * (proj (1,1)))) . y by A38, FUNCT_1:12;
then I . (g . ((proj (1,1)) . y)) = f . y by A1, RELAT_1:36;
then I . (g . ((proj (1,1)) . y)) = f /. y by A23, A30, PARTFUN1:def_6;
then (I . (g . ((proj (1,1)) . y))) - (I . (g . ((proj (1,1)) . x))) = (f /. y) - (f /. x) by A29, REAL_NS1:5;
hence (f /. y) - (f /. x) = (L . (y - x)) + (R /. (y - x)) by A32, A37, A39, REAL_NS1:2; ::_thesis: verum
end;
L0 is total by FDIFF_1:def_3;
then A40: dom L0 = REAL by PARTFUN1:def_2;
A41: L is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))) by LOPBAN_1:def_9;
then f is_differentiable_in x by A24, A23, A26, NDIFF_1:def_6;
then diff (f,x) = (I * L0) * (proj (1,1)) by A24, A23, A41, A26, NDIFF_1:def_7;
then (diff (f,x)) . <*1*> = ((I * L0) * (proj (1,1))) . (I . 1) by Lm1;
then (diff (f,x)) . <*1*> = (I * L0) . ((proj (1,1)) . (I . 1)) by Lm1, FUNCT_1:13;
then (diff (f,x)) . <*1*> = I . (L0 . ((proj (1,1)) . (I . 1))) by A40, FUNCT_1:13;
then (diff (f,x)) . <*1*> = I . (L0 . 1) by Lm1, FUNCT_1:35;
hence ( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> ) by A24, A23, A9, A41, A26, Lm1, NDIFF_1:def_6; ::_thesis: verum
end;
theorem :: PDIFF_1:9
for f being PartFunc of (REAL-NS 1),(REAL-NS 1)
for g being PartFunc of REAL,REAL
for x being Point of (REAL-NS 1)
for y being Element of REAL st f = <>* g & x = <*y*> holds
( f is_differentiable_in x iff g is_differentiable_in y ) by Th7, Th8;
theorem Th10: :: PDIFF_1:10
for f being PartFunc of (REAL-NS 1),(REAL-NS 1)
for g being PartFunc of REAL,REAL
for x being Point of (REAL-NS 1)
for y being Element of REAL st f = <>* g & x = <*y*> & f is_differentiable_in x holds
(diff (f,x)) . <*1*> = <*(diff (g,y))*>
proof
let f be PartFunc of (REAL-NS 1),(REAL-NS 1); ::_thesis: for g being PartFunc of REAL,REAL
for x being Point of (REAL-NS 1)
for y being Element of REAL st f = <>* g & x = <*y*> & f is_differentiable_in x holds
(diff (f,x)) . <*1*> = <*(diff (g,y))*>
let g be PartFunc of REAL,REAL; ::_thesis: for x being Point of (REAL-NS 1)
for y being Element of REAL st f = <>* g & x = <*y*> & f is_differentiable_in x holds
(diff (f,x)) . <*1*> = <*(diff (g,y))*>
let x be Point of (REAL-NS 1); ::_thesis: for y being Element of REAL st f = <>* g & x = <*y*> & f is_differentiable_in x holds
(diff (f,x)) . <*1*> = <*(diff (g,y))*>
let y be Element of REAL ; ::_thesis: ( f = <>* g & x = <*y*> & f is_differentiable_in x implies (diff (f,x)) . <*1*> = <*(diff (g,y))*> )
assume that
A1: f = <>* g and
A2: x = <*y*> and
A3: f is_differentiable_in x ; ::_thesis: (diff (f,x)) . <*1*> = <*(diff (g,y))*>
g is_differentiable_in y by A1, A2, A3, Th7;
hence (diff (f,x)) . <*1*> = <*(diff (g,y))*> by A1, A2, Th8; ::_thesis: verum
end;
begin
definition
let n, m be non empty Element of NAT ;
let i be Element of NAT ;
let f be PartFunc of (REAL-NS m),(REAL-NS n);
let x be Point of (REAL-NS m);
predf is_partial_differentiable_in x,i means :Def9: :: PDIFF_1:def 9
f * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x;
end;
:: deftheorem Def9 defines is_partial_differentiable_in PDIFF_1:def_9_:_
for n, m being non empty Element of NAT
for i being Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds
( f is_partial_differentiable_in x,i iff f * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x );
definition
let m, n be non empty Element of NAT ;
let i be Element of NAT ;
let f be PartFunc of (REAL-NS m),(REAL-NS n);
let x be Point of (REAL-NS m);
func partdiff (f,x,i) -> Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) equals :: PDIFF_1:def 10
diff ((f * (reproj (i,x))),((Proj (i,m)) . x));
coherence
diff ((f * (reproj (i,x))),((Proj (i,m)) . x)) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) ;
end;
:: deftheorem defines partdiff PDIFF_1:def_10_:_
for m, n being non empty Element of NAT
for i being Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds partdiff (f,x,i) = diff ((f * (reproj (i,x))),((Proj (i,m)) . x));
definition
let n be non empty Element of NAT ;
let i be Element of NAT ;
let f be PartFunc of (REAL n),REAL;
let x be Element of REAL n;
predf is_partial_differentiable_in x,i means :Def11: :: PDIFF_1:def 11
f * (reproj (i,x)) is_differentiable_in (proj (i,n)) . x;
end;
:: deftheorem Def11 defines is_partial_differentiable_in PDIFF_1:def_11_:_
for n being non empty Element of NAT
for i being Element of NAT
for f being PartFunc of (REAL n),REAL
for x being Element of REAL n holds
( f is_partial_differentiable_in x,i iff f * (reproj (i,x)) is_differentiable_in (proj (i,n)) . x );
definition
let n be non empty Element of NAT ;
let i be Element of NAT ;
let f be PartFunc of (REAL n),REAL;
let x be Element of REAL n;
func partdiff (f,x,i) -> real number equals :: PDIFF_1:def 12
diff ((f * (reproj (i,x))),((proj (i,n)) . x));
coherence
diff ((f * (reproj (i,x))),((proj (i,n)) . x)) is real number ;
end;
:: deftheorem defines partdiff PDIFF_1:def_12_:_
for n being non empty Element of NAT
for i being Element of NAT
for f being PartFunc of (REAL n),REAL
for x being Element of REAL n holds partdiff (f,x,i) = diff ((f * (reproj (i,x))),((proj (i,n)) . x));
definition
let n be non empty Element of NAT ;
let i be Element of NAT ;
let f be PartFunc of (REAL n),REAL;
let x be Element of REAL n;
:: original: partdiff
redefine func partdiff (f,x,i) -> Real;
coherence
partdiff (f,x,i) is Real ;
end;
theorem Th11: :: PDIFF_1:11
for n being non empty Element of NAT
for i being Element of NAT holds Proj (i,n) = ((proj (1,1)) ") * (proj (i,n))
proof
let n be non empty Element of NAT ; ::_thesis: for i being Element of NAT holds Proj (i,n) = ((proj (1,1)) ") * (proj (i,n))
let i be Element of NAT ; ::_thesis: Proj (i,n) = ((proj (1,1)) ") * (proj (i,n))
reconsider h = (proj (1,1)) " as Function of REAL,(REAL 1) by Th2;
A1: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def_4;
A2: now__::_thesis:_for_x_being_Element_of_REAL_n_holds_
(_(h_*_(proj_(i,n)))_._x_=_<*((proj_(i,n))_._x)*>_&_(Proj_(i,n))_._x_=_(h_*_(proj_(i,n)))_._x_)
let x be Element of REAL n; ::_thesis: ( (h * (proj (i,n))) . x = <*((proj (i,n)) . x)*> & (Proj (i,n)) . x = (h * (proj (i,n))) . x )
reconsider z = x as Point of (REAL-NS n) by REAL_NS1:def_4;
A3: (h * (proj (i,n))) . x = h . ((proj (i,n)) . x) by FUNCT_2:15;
hence (h * (proj (i,n))) . x = <*((proj (i,n)) . x)*> by Lm1; ::_thesis: (Proj (i,n)) . x = (h * (proj (i,n))) . x
(Proj (i,n)) . x = (Proj (i,n)) . z ;
then (Proj (i,n)) . x = <*((proj (i,n)) . x)*> by Def4;
hence (Proj (i,n)) . x = (h * (proj (i,n))) . x by A3, Lm1; ::_thesis: verum
end;
the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4;
hence Proj (i,n) = ((proj (1,1)) ") * (proj (i,n)) by A1, A2, FUNCT_2:63; ::_thesis: verum
end;
theorem Th12: :: PDIFF_1:12
for n being non empty Element of NAT
for i being Element of NAT
for x being Point of (REAL-NS n)
for y being Element of REAL n st x = y holds
(reproj (i,y)) * (proj (1,1)) = reproj (i,x)
proof
let n be non empty Element of NAT ; ::_thesis: for i being Element of NAT
for x being Point of (REAL-NS n)
for y being Element of REAL n st x = y holds
(reproj (i,y)) * (proj (1,1)) = reproj (i,x)
let i be Element of NAT ; ::_thesis: for x being Point of (REAL-NS n)
for y being Element of REAL n st x = y holds
(reproj (i,y)) * (proj (1,1)) = reproj (i,x)
let x be Point of (REAL-NS n); ::_thesis: for y being Element of REAL n st x = y holds
(reproj (i,y)) * (proj (1,1)) = reproj (i,x)
let y be Element of REAL n; ::_thesis: ( x = y implies (reproj (i,y)) * (proj (1,1)) = reproj (i,x) )
reconsider k = proj (1,1) as Function of (REAL 1),REAL ;
A1: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def_4;
assume A2: x = y ; ::_thesis: (reproj (i,y)) * (proj (1,1)) = reproj (i,x)
A3: now__::_thesis:_for_s_being_Element_of_REAL_1_holds_(reproj_(i,x))_._s_=_((reproj_(i,y))_*_k)_._s
let s be Element of REAL 1; ::_thesis: (reproj (i,x)) . s = ((reproj (i,y)) * k) . s
reconsider r = s as Point of (REAL-NS 1) by REAL_NS1:def_4;
A4: ((reproj (i,y)) * k) . s = (reproj (i,y)) . (k . s) by FUNCT_2:15;
ex q being Element of REAL ex z being Element of REAL n st
( r = <*q*> & z = x & (reproj (i,x)) . r = (reproj (i,z)) . q ) by Def6;
hence (reproj (i,x)) . s = ((reproj (i,y)) * k) . s by A2, A4, Lm1; ::_thesis: verum
end;
the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4;
hence (reproj (i,y)) * (proj (1,1)) = reproj (i,x) by A1, A3, FUNCT_2:63; ::_thesis: verum
end;
theorem Th13: :: PDIFF_1:13
for n being non empty Element of NAT
for i being Element of NAT
for f being PartFunc of (REAL-NS n),(REAL-NS 1)
for g being PartFunc of (REAL n),REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y holds
<>* (g * (reproj (i,y))) = f * (reproj (i,x))
proof
let n be non empty Element of NAT ; ::_thesis: for i being Element of NAT
for f being PartFunc of (REAL-NS n),(REAL-NS 1)
for g being PartFunc of (REAL n),REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y holds
<>* (g * (reproj (i,y))) = f * (reproj (i,x))
let i be Element of NAT ; ::_thesis: for f being PartFunc of (REAL-NS n),(REAL-NS 1)
for g being PartFunc of (REAL n),REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y holds
<>* (g * (reproj (i,y))) = f * (reproj (i,x))
let f be PartFunc of (REAL-NS n),(REAL-NS 1); ::_thesis: for g being PartFunc of (REAL n),REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y holds
<>* (g * (reproj (i,y))) = f * (reproj (i,x))
let g be PartFunc of (REAL n),REAL; ::_thesis: for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y holds
<>* (g * (reproj (i,y))) = f * (reproj (i,x))
let x be Point of (REAL-NS n); ::_thesis: for y being Element of REAL n st f = <>* g & x = y holds
<>* (g * (reproj (i,y))) = f * (reproj (i,x))
let y be Element of REAL n; ::_thesis: ( f = <>* g & x = y implies <>* (g * (reproj (i,y))) = f * (reproj (i,x)) )
reconsider h = (proj (1,1)) " as Function of REAL,(REAL 1) by Th2;
assume that
A1: f = <>* g and
A2: x = y ; ::_thesis: <>* (g * (reproj (i,y))) = f * (reproj (i,x))
(reproj (i,y)) * (proj (1,1)) = reproj (i,x) by A2, Th12;
then ((h * g) * (reproj (i,y))) * (proj (1,1)) = f * (reproj (i,x)) by A1, RELAT_1:36;
hence <>* (g * (reproj (i,y))) = f * (reproj (i,x)) by RELAT_1:36; ::_thesis: verum
end;
theorem Th14: :: PDIFF_1:14
for n being non empty Element of NAT
for i being Element of NAT
for f being PartFunc of (REAL-NS n),(REAL-NS 1)
for g being PartFunc of (REAL n),REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y holds
( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i )
proof
let n be non empty Element of NAT ; ::_thesis: for i being Element of NAT
for f being PartFunc of (REAL-NS n),(REAL-NS 1)
for g being PartFunc of (REAL n),REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y holds
( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i )
let i be Element of NAT ; ::_thesis: for f being PartFunc of (REAL-NS n),(REAL-NS 1)
for g being PartFunc of (REAL n),REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y holds
( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i )
let f be PartFunc of (REAL-NS n),(REAL-NS 1); ::_thesis: for g being PartFunc of (REAL n),REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y holds
( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i )
let g be PartFunc of (REAL n),REAL; ::_thesis: for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y holds
( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i )
let x be Point of (REAL-NS n); ::_thesis: for y being Element of REAL n st f = <>* g & x = y holds
( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i )
let y be Element of REAL n; ::_thesis: ( f = <>* g & x = y implies ( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i ) )
assume that
A1: f = <>* g and
A2: x = y ; ::_thesis: ( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i )
A3: <*((proj (i,n)) . y)*> = (Proj (i,n)) . x by A2, Def4;
A4: f * (reproj (i,x)) = <>* (g * (reproj (i,y))) by A1, A2, Th13;
hereby ::_thesis: ( g is_partial_differentiable_in y,i implies f is_partial_differentiable_in x,i )
assume f is_partial_differentiable_in x,i ; ::_thesis: g is_partial_differentiable_in y,i
then f * (reproj (i,x)) is_differentiable_in (Proj (i,n)) . x by Def9;
then g * (reproj (i,y)) is_differentiable_in (proj (i,n)) . y by A4, A3, Th7;
hence g is_partial_differentiable_in y,i by Def11; ::_thesis: verum
end;
assume g is_partial_differentiable_in y,i ; ::_thesis: f is_partial_differentiable_in x,i
then g * (reproj (i,y)) is_differentiable_in (proj (i,n)) . y by Def11;
then f * (reproj (i,x)) is_differentiable_in (Proj (i,n)) . x by A4, A3, Th8;
hence f is_partial_differentiable_in x,i by Def9; ::_thesis: verum
end;
theorem Th15: :: PDIFF_1:15
for n being non empty Element of NAT
for i being Element of NAT
for f being PartFunc of (REAL-NS n),(REAL-NS 1)
for g being PartFunc of (REAL n),REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y & f is_partial_differentiable_in x,i holds
(partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*>
proof
let n be non empty Element of NAT ; ::_thesis: for i being Element of NAT
for f being PartFunc of (REAL-NS n),(REAL-NS 1)
for g being PartFunc of (REAL n),REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y & f is_partial_differentiable_in x,i holds
(partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*>
let i be Element of NAT ; ::_thesis: for f being PartFunc of (REAL-NS n),(REAL-NS 1)
for g being PartFunc of (REAL n),REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y & f is_partial_differentiable_in x,i holds
(partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*>
let f be PartFunc of (REAL-NS n),(REAL-NS 1); ::_thesis: for g being PartFunc of (REAL n),REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y & f is_partial_differentiable_in x,i holds
(partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*>
let g be PartFunc of (REAL n),REAL; ::_thesis: for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y & f is_partial_differentiable_in x,i holds
(partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*>
let x be Point of (REAL-NS n); ::_thesis: for y being Element of REAL n st f = <>* g & x = y & f is_partial_differentiable_in x,i holds
(partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*>
let y be Element of REAL n; ::_thesis: ( f = <>* g & x = y & f is_partial_differentiable_in x,i implies (partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*> )
assume that
A1: f = <>* g and
A2: x = y and
A3: f is_partial_differentiable_in x,i ; ::_thesis: (partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*>
A4: f * (reproj (i,x)) is_differentiable_in (Proj (i,n)) . x by A3, Def9;
A5: <*((proj (i,n)) . y)*> = (Proj (i,n)) . x by A2, Def4;
f * (reproj (i,x)) = <>* (g * (reproj (i,y))) by A1, A2, Th13;
hence (partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*> by A4, A5, Th10; ::_thesis: verum
end;
definition
let m, n be non empty Element of NAT ;
let i be Element of NAT ;
let f be PartFunc of (REAL m),(REAL n);
let x be Element of REAL m;
predf is_partial_differentiable_in x,i means :Def13: :: PDIFF_1:def 13
ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & g is_partial_differentiable_in y,i );
end;
:: deftheorem Def13 defines is_partial_differentiable_in PDIFF_1:def_13_:_
for m, n being non empty Element of NAT
for i being Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m holds
( f is_partial_differentiable_in x,i iff ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & g is_partial_differentiable_in y,i ) );
definition
let m, n be non empty Element of NAT ;
let i be Element of NAT ;
let f be PartFunc of (REAL m),(REAL n);
let x be Element of REAL m;
assume A1: f is_partial_differentiable_in x,i ;
func partdiff (f,x,i) -> Element of REAL n means :Def14: :: PDIFF_1:def 14
ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & it = (partdiff (g,y,i)) . <*1*> );
correctness
existence
ex b1 being Element of REAL n ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b1 = (partdiff (g,y,i)) . <*1*> );
uniqueness
for b1, b2 being Element of REAL n st ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b1 = (partdiff (g,y,i)) . <*1*> ) & ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b2 = (partdiff (g,y,i)) . <*1*> ) holds
b1 = b2;
proof
A2: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def_4;
consider g being PartFunc of (REAL-NS m),(REAL-NS n), y being Point of (REAL-NS m) such that
A3: f = g and
A4: x = y and
g is_partial_differentiable_in y,i by A1, Def13;
the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4;
then partdiff (g,y,i) is Function of (REAL 1),(REAL n) by A2, LOPBAN_1:def_9;
then (partdiff (g,y,i)) . <*1*> is Element of REAL n by FINSEQ_2:98, FUNCT_2:5;
hence ( ex b1 being Element of REAL n ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b1 = (partdiff (g,y,i)) . <*1*> ) & ( for b1, b2 being Element of REAL n st ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b1 = (partdiff (g,y,i)) . <*1*> ) & ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b2 = (partdiff (g,y,i)) . <*1*> ) holds
b1 = b2 ) ) by A3, A4; ::_thesis: verum
end;
end;
:: deftheorem Def14 defines partdiff PDIFF_1:def_14_:_
for m, n being non empty Element of NAT
for i being Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m st f is_partial_differentiable_in x,i holds
for b6 being Element of REAL n holds
( b6 = partdiff (f,x,i) iff ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b6 = (partdiff (g,y,i)) . <*1*> ) );
theorem Th16: :: PDIFF_1:16
for i being Element of NAT
for m, n being non empty Element of NAT
for F being PartFunc of (REAL-NS m),(REAL-NS n)
for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y holds
( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i )
proof
let i be Element of NAT ; ::_thesis: for m, n being non empty Element of NAT
for F being PartFunc of (REAL-NS m),(REAL-NS n)
for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y holds
( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i )
let m, n be non empty Element of NAT ; ::_thesis: for F being PartFunc of (REAL-NS m),(REAL-NS n)
for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y holds
( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i )
let F be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y holds
( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i )
let G be PartFunc of (REAL m),(REAL n); ::_thesis: for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y holds
( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i )
let x be Point of (REAL-NS m); ::_thesis: for y being Element of REAL m st F = G & x = y holds
( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i )
let y be Element of REAL m; ::_thesis: ( F = G & x = y implies ( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i ) )
assume that
A1: F = G and
A2: x = y ; ::_thesis: ( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i )
now__::_thesis:_(_G_is_partial_differentiable_in_y,i_implies_F_is_partial_differentiable_in_x,i_)
assume G is_partial_differentiable_in y,i ; ::_thesis: F is_partial_differentiable_in x,i
then ex f1 being PartFunc of (REAL-NS m),(REAL-NS n) ex y1 being Point of (REAL-NS m) st
( G = f1 & y = y1 & f1 is_partial_differentiable_in y1,i ) by Def13;
hence F is_partial_differentiable_in x,i by A1, A2; ::_thesis: verum
end;
hence ( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i ) by A1, A2, Def13; ::_thesis: verum
end;
theorem Th17: :: PDIFF_1:17
for i being Element of NAT
for m, n being non empty Element of NAT
for F being PartFunc of (REAL-NS m),(REAL-NS n)
for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y & F is_partial_differentiable_in x,i holds
(partdiff (F,x,i)) . <*1*> = partdiff (G,y,i)
proof
let i be Element of NAT ; ::_thesis: for m, n being non empty Element of NAT
for F being PartFunc of (REAL-NS m),(REAL-NS n)
for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y & F is_partial_differentiable_in x,i holds
(partdiff (F,x,i)) . <*1*> = partdiff (G,y,i)
let m, n be non empty Element of NAT ; ::_thesis: for F being PartFunc of (REAL-NS m),(REAL-NS n)
for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y & F is_partial_differentiable_in x,i holds
(partdiff (F,x,i)) . <*1*> = partdiff (G,y,i)
let F be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y & F is_partial_differentiable_in x,i holds
(partdiff (F,x,i)) . <*1*> = partdiff (G,y,i)
let G be PartFunc of (REAL m),(REAL n); ::_thesis: for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y & F is_partial_differentiable_in x,i holds
(partdiff (F,x,i)) . <*1*> = partdiff (G,y,i)
let x be Point of (REAL-NS m); ::_thesis: for y being Element of REAL m st F = G & x = y & F is_partial_differentiable_in x,i holds
(partdiff (F,x,i)) . <*1*> = partdiff (G,y,i)
let y be Element of REAL m; ::_thesis: ( F = G & x = y & F is_partial_differentiable_in x,i implies (partdiff (F,x,i)) . <*1*> = partdiff (G,y,i) )
assume that
A1: F = G and
A2: x = y and
A3: F is_partial_differentiable_in x,i ; ::_thesis: (partdiff (F,x,i)) . <*1*> = partdiff (G,y,i)
A4: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def_4;
the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4;
then partdiff (F,x,i) is Function of (REAL 1),(REAL n) by A4, LOPBAN_1:def_9;
then A5: (partdiff (F,x,i)) . <*1*> is Element of REAL n by FINSEQ_2:98, FUNCT_2:5;
G is_partial_differentiable_in y,i by A1, A2, A3, Th16;
hence (partdiff (F,x,i)) . <*1*> = partdiff (G,y,i) by A1, A2, A5, Def14; ::_thesis: verum
end;
theorem :: PDIFF_1:18
for n being non empty Element of NAT
for i being Element of NAT
for g being PartFunc of (REAL n),REAL
for y being Element of REAL n
for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g holds
( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i )
proof
let n be non empty Element of NAT ; ::_thesis: for i being Element of NAT
for g being PartFunc of (REAL n),REAL
for y being Element of REAL n
for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g holds
( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i )
let i be Element of NAT ; ::_thesis: for g being PartFunc of (REAL n),REAL
for y being Element of REAL n
for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g holds
( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i )
let g be PartFunc of (REAL n),REAL; ::_thesis: for y being Element of REAL n
for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g holds
( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i )
let y be Element of REAL n; ::_thesis: for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g holds
( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i )
let g1 be PartFunc of (REAL n),(REAL 1); ::_thesis: ( g1 = <>* g implies ( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i ) )
assume A1: g1 = <>* g ; ::_thesis: ( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i )
reconsider y9 = y as Point of (REAL-NS n) by REAL_NS1:def_4;
the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4;
then reconsider h = g1 as PartFunc of (REAL-NS n),(REAL-NS 1) by REAL_NS1:def_4;
( h is_partial_differentiable_in y9,i iff g1 is_partial_differentiable_in y,i ) by Th16;
hence ( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i ) by A1, Th14; ::_thesis: verum
end;
theorem :: PDIFF_1:19
for n being non empty Element of NAT
for i being Element of NAT
for g being PartFunc of (REAL n),REAL
for y being Element of REAL n
for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g & g1 is_partial_differentiable_in y,i holds
partdiff (g1,y,i) = <*(partdiff (g,y,i))*>
proof
let n be non empty Element of NAT ; ::_thesis: for i being Element of NAT
for g being PartFunc of (REAL n),REAL
for y being Element of REAL n
for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g & g1 is_partial_differentiable_in y,i holds
partdiff (g1,y,i) = <*(partdiff (g,y,i))*>
let i be Element of NAT ; ::_thesis: for g being PartFunc of (REAL n),REAL
for y being Element of REAL n
for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g & g1 is_partial_differentiable_in y,i holds
partdiff (g1,y,i) = <*(partdiff (g,y,i))*>
let g be PartFunc of (REAL n),REAL; ::_thesis: for y being Element of REAL n
for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g & g1 is_partial_differentiable_in y,i holds
partdiff (g1,y,i) = <*(partdiff (g,y,i))*>
let y be Element of REAL n; ::_thesis: for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g & g1 is_partial_differentiable_in y,i holds
partdiff (g1,y,i) = <*(partdiff (g,y,i))*>
let g1 be PartFunc of (REAL n),(REAL 1); ::_thesis: ( g1 = <>* g & g1 is_partial_differentiable_in y,i implies partdiff (g1,y,i) = <*(partdiff (g,y,i))*> )
assume that
A1: g1 = <>* g and
A2: g1 is_partial_differentiable_in y,i ; ::_thesis: partdiff (g1,y,i) = <*(partdiff (g,y,i))*>
reconsider y9 = y as Point of (REAL-NS n) by REAL_NS1:def_4;
the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4;
then reconsider h = g1 as PartFunc of (REAL-NS n),(REAL-NS 1) by REAL_NS1:def_4;
A3: h is_partial_differentiable_in y9,i by A2, Th16;
then (partdiff (h,y9,i)) . <*1*> = partdiff (g1,y,i) by Th17;
hence partdiff (g1,y,i) = <*(partdiff (g,y,i))*> by A1, A3, Th15; ::_thesis: verum
end;
begin
definition
let m, n be non empty Element of NAT ;
let i, j be Element of NAT ;
let f be PartFunc of (REAL-NS m),(REAL-NS n);
let x be Point of (REAL-NS m);
predf is_partial_differentiable_in x,i,j means :Def15: :: PDIFF_1:def 15
((Proj (j,n)) * f) * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x;
end;
:: deftheorem Def15 defines is_partial_differentiable_in PDIFF_1:def_15_:_
for m, n being non empty Element of NAT
for i, j being Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds
( f is_partial_differentiable_in x,i,j iff ((Proj (j,n)) * f) * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x );
definition
let m, n be non empty Element of NAT ;
let i, j be Element of NAT ;
let f be PartFunc of (REAL-NS m),(REAL-NS n);
let x be Point of (REAL-NS m);
func partdiff (f,x,i,j) -> Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))) equals :: PDIFF_1:def 16
diff ((((Proj (j,n)) * f) * (reproj (i,x))),((Proj (i,m)) . x));
correctness
coherence
diff ((((Proj (j,n)) * f) * (reproj (i,x))),((Proj (i,m)) . x)) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)));
;
end;
:: deftheorem defines partdiff PDIFF_1:def_16_:_
for m, n being non empty Element of NAT
for i, j being Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds partdiff (f,x,i,j) = diff ((((Proj (j,n)) * f) * (reproj (i,x))),((Proj (i,m)) . x));
definition
let m, n be non empty Element of NAT ;
let i, j be Element of NAT ;
let h be PartFunc of (REAL m),(REAL n);
let z be Element of REAL m;
predh is_partial_differentiable_in z,i,j means :Def17: :: PDIFF_1:def 17
((proj (j,n)) * h) * (reproj (i,z)) is_differentiable_in (proj (i,m)) . z;
end;
:: deftheorem Def17 defines is_partial_differentiable_in PDIFF_1:def_17_:_
for m, n being non empty Element of NAT
for i, j being Element of NAT
for h being PartFunc of (REAL m),(REAL n)
for z being Element of REAL m holds
( h is_partial_differentiable_in z,i,j iff ((proj (j,n)) * h) * (reproj (i,z)) is_differentiable_in (proj (i,m)) . z );
definition
let m, n be non empty Element of NAT ;
let i, j be Element of NAT ;
let h be PartFunc of (REAL m),(REAL n);
let z be Element of REAL m;
func partdiff (h,z,i,j) -> real number equals :: PDIFF_1:def 18
diff ((((proj (j,n)) * h) * (reproj (i,z))),((proj (i,m)) . z));
correctness
coherence
diff ((((proj (j,n)) * h) * (reproj (i,z))),((proj (i,m)) . z)) is real number ;
;
end;
:: deftheorem defines partdiff PDIFF_1:def_18_:_
for m, n being non empty Element of NAT
for i, j being Element of NAT
for h being PartFunc of (REAL m),(REAL n)
for z being Element of REAL m holds partdiff (h,z,i,j) = diff ((((proj (j,n)) * h) * (reproj (i,z))),((proj (i,m)) . z));
theorem Th20: :: PDIFF_1:20
for m, n being non empty Element of NAT
for F being PartFunc of (REAL-NS m),(REAL-NS n)
for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y holds
( F is_differentiable_in x iff G is_differentiable_in y )
proof
let m, n be non empty Element of NAT ; ::_thesis: for F being PartFunc of (REAL-NS m),(REAL-NS n)
for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y holds
( F is_differentiable_in x iff G is_differentiable_in y )
let F be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y holds
( F is_differentiable_in x iff G is_differentiable_in y )
let G be PartFunc of (REAL m),(REAL n); ::_thesis: for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y holds
( F is_differentiable_in x iff G is_differentiable_in y )
let x be Point of (REAL-NS m); ::_thesis: for y being Element of REAL m st F = G & x = y holds
( F is_differentiable_in x iff G is_differentiable_in y )
let y be Element of REAL m; ::_thesis: ( F = G & x = y implies ( F is_differentiable_in x iff G is_differentiable_in y ) )
assume that
A1: F = G and
A2: x = y ; ::_thesis: ( F is_differentiable_in x iff G is_differentiable_in y )
now__::_thesis:_(_G_is_differentiable_in_y_implies_F_is_differentiable_in_x_)
assume G is_differentiable_in y ; ::_thesis: F is_differentiable_in x
then ex f1 being PartFunc of (REAL-NS m),(REAL-NS n) ex y1 being Point of (REAL-NS m) st
( G = f1 & y = y1 & f1 is_differentiable_in y1 ) by Def7;
hence F is_differentiable_in x by A1, A2; ::_thesis: verum
end;
hence ( F is_differentiable_in x iff G is_differentiable_in y ) by A1, A2, Def7; ::_thesis: verum
end;
theorem :: PDIFF_1:21
for m, n being non empty Element of NAT
for F being PartFunc of (REAL-NS m),(REAL-NS n)
for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y & F is_differentiable_in x holds
diff (F,x) = diff (G,y)
proof
let m, n be non empty Element of NAT ; ::_thesis: for F being PartFunc of (REAL-NS m),(REAL-NS n)
for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y & F is_differentiable_in x holds
diff (F,x) = diff (G,y)
let F be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y & F is_differentiable_in x holds
diff (F,x) = diff (G,y)
let G be PartFunc of (REAL m),(REAL n); ::_thesis: for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y & F is_differentiable_in x holds
diff (F,x) = diff (G,y)
let x be Point of (REAL-NS m); ::_thesis: for y being Element of REAL m st F = G & x = y & F is_differentiable_in x holds
diff (F,x) = diff (G,y)
let y be Element of REAL m; ::_thesis: ( F = G & x = y & F is_differentiable_in x implies diff (F,x) = diff (G,y) )
assume that
A1: F = G and
A2: x = y and
A3: F is_differentiable_in x ; ::_thesis: diff (F,x) = diff (G,y)
A4: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def_4;
the carrier of (REAL-NS m) = REAL m by REAL_NS1:def_4;
then A5: diff (F,x) is Function of (REAL m),(REAL n) by A4, LOPBAN_1:def_9;
G is_differentiable_in y by A1, A2, A3, Th20;
hence diff (F,x) = diff (G,y) by A1, A2, A5, Def8; ::_thesis: verum
end;
theorem Th22: :: PDIFF_1:22
for m, n being non empty Element of NAT
for j, i being Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for h being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z holds
((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z)))
proof
let m, n be non empty Element of NAT ; ::_thesis: for j, i being Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for h being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z holds
((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z)))
let j, i be Element of NAT ; ::_thesis: for f being PartFunc of (REAL-NS m),(REAL-NS n)
for h being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z holds
((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z)))
let f be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for h being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z holds
((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z)))
let h be PartFunc of (REAL m),(REAL n); ::_thesis: for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z holds
((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z)))
let x be Point of (REAL-NS m); ::_thesis: for z being Element of REAL m st f = h & x = z holds
((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z)))
let z be Element of REAL m; ::_thesis: ( f = h & x = z implies ((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z))) )
reconsider h1 = (proj (1,1)) " as Function of REAL,(REAL 1) by Th2;
assume that
A1: f = h and
A2: x = z ; ::_thesis: ((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z)))
<>* (((proj (j,n)) * h) * (reproj (i,z))) = (h1 * ((proj (j,n)) * (h * (reproj (i,z))))) * (proj (1,1)) by RELAT_1:36
.= ((h1 * (proj (j,n))) * (h * (reproj (i,z)))) * (proj (1,1)) by RELAT_1:36
.= (h1 * (proj (j,n))) * ((h * (reproj (i,z))) * (proj (1,1))) by RELAT_1:36
.= (h1 * (proj (j,n))) * (h * ((reproj (i,z)) * (proj (1,1)))) by RELAT_1:36
.= (Proj (j,n)) * (h * ((reproj (i,z)) * (proj (1,1)))) by Th11
.= (Proj (j,n)) * (h * (reproj (i,x))) by A2, Th12 ;
hence ((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z))) by A1, RELAT_1:36; ::_thesis: verum
end;
theorem :: PDIFF_1:23
for n, m being non empty Element of NAT
for i, j being Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for h being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z holds
( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j )
proof
let n, m be non empty Element of NAT ; ::_thesis: for i, j being Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for h being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z holds
( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j )
let i, j be Element of NAT ; ::_thesis: for f being PartFunc of (REAL-NS m),(REAL-NS n)
for h being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z holds
( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j )
let f be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for h being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z holds
( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j )
let h be PartFunc of (REAL m),(REAL n); ::_thesis: for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z holds
( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j )
let x be Point of (REAL-NS m); ::_thesis: for z being Element of REAL m st f = h & x = z holds
( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j )
let z be Element of REAL m; ::_thesis: ( f = h & x = z implies ( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j ) )
assume that
A1: f = h and
A2: x = z ; ::_thesis: ( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j )
A3: (Proj (i,m)) . x = <*((proj (i,m)) . z)*> by A2, Def4;
A4: ((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z))) by A1, A2, Th22;
hereby ::_thesis: ( h is_partial_differentiable_in z,i,j implies f is_partial_differentiable_in x,i,j )
assume f is_partial_differentiable_in x,i,j ; ::_thesis: h is_partial_differentiable_in z,i,j
then ((Proj (j,n)) * f) * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by Def15;
then ((proj (j,n)) * h) * (reproj (i,z)) is_differentiable_in (proj (i,m)) . z by A4, A3, Th7;
hence h is_partial_differentiable_in z,i,j by Def17; ::_thesis: verum
end;
assume h is_partial_differentiable_in z,i,j ; ::_thesis: f is_partial_differentiable_in x,i,j
then ((proj (j,n)) * h) * (reproj (i,z)) is_differentiable_in (proj (i,m)) . z by Def17;
then ((Proj (j,n)) * f) * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by A4, A3, Th8;
hence f is_partial_differentiable_in x,i,j by Def15; ::_thesis: verum
end;
theorem :: PDIFF_1:24
for n, m being non empty Element of NAT
for i, j being Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for h being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z & f is_partial_differentiable_in x,i,j holds
(partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,z,i,j))*>
proof
let n, m be non empty Element of NAT ; ::_thesis: for i, j being Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for h being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z & f is_partial_differentiable_in x,i,j holds
(partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,z,i,j))*>
let i, j be Element of NAT ; ::_thesis: for f being PartFunc of (REAL-NS m),(REAL-NS n)
for h being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z & f is_partial_differentiable_in x,i,j holds
(partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,z,i,j))*>
let f be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for h being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z & f is_partial_differentiable_in x,i,j holds
(partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,z,i,j))*>
let h be PartFunc of (REAL m),(REAL n); ::_thesis: for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z & f is_partial_differentiable_in x,i,j holds
(partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,z,i,j))*>
let x be Point of (REAL-NS m); ::_thesis: for z being Element of REAL m st f = h & x = z & f is_partial_differentiable_in x,i,j holds
(partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,z,i,j))*>
let z be Element of REAL m; ::_thesis: ( f = h & x = z & f is_partial_differentiable_in x,i,j implies (partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,z,i,j))*> )
assume that
A1: f = h and
A2: x = z and
A3: f is_partial_differentiable_in x,i,j ; ::_thesis: (partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,z,i,j))*>
A4: (Proj (i,m)) . x = <*((proj (i,m)) . z)*> by A2, Def4;
A5: ((Proj (j,n)) * f) * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by A3, Def15;
((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z))) by A1, A2, Th22;
hence (partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,z,i,j))*> by A4, A5, Th10; ::_thesis: verum
end;
definition
let m, n be non empty Element of NAT ;
let i be Element of NAT ;
let f be PartFunc of (REAL-NS m),(REAL-NS n);
let X be set ;
predf is_partial_differentiable_on X,i means :Def19: :: PDIFF_1:def 19
( X c= dom f & ( for x being Point of (REAL-NS m) st x in X holds
f | X is_partial_differentiable_in x,i ) );
end;
:: deftheorem Def19 defines is_partial_differentiable_on PDIFF_1:def_19_:_
for m, n being non empty Element of NAT
for i being Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for X being set holds
( f is_partial_differentiable_on X,i iff ( X c= dom f & ( for x being Point of (REAL-NS m) st x in X holds
f | X is_partial_differentiable_in x,i ) ) );
theorem Th25: :: PDIFF_1:25
for n, m being non empty Element of NAT
for i being Element of NAT
for X being set
for f being PartFunc of (REAL-NS m),(REAL-NS n) st f is_partial_differentiable_on X,i holds
X is Subset of (REAL-NS m)
proof
let n, m be non empty Element of NAT ; ::_thesis: for i being Element of NAT
for X being set
for f being PartFunc of (REAL-NS m),(REAL-NS n) st f is_partial_differentiable_on X,i holds
X is Subset of (REAL-NS m)
let i be Element of NAT ; ::_thesis: for X being set
for f being PartFunc of (REAL-NS m),(REAL-NS n) st f is_partial_differentiable_on X,i holds
X is Subset of (REAL-NS m)
let X be set ; ::_thesis: for f being PartFunc of (REAL-NS m),(REAL-NS n) st f is_partial_differentiable_on X,i holds
X is Subset of (REAL-NS m)
let f be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: ( f is_partial_differentiable_on X,i implies X is Subset of (REAL-NS m) )
assume f is_partial_differentiable_on X,i ; ::_thesis: X is Subset of (REAL-NS m)
then X c= dom f by Def19;
hence X is Subset of (REAL-NS m) by XBOOLE_1:1; ::_thesis: verum
end;
definition
let m, n be non empty Element of NAT ;
let i be Element of NAT ;
let f be PartFunc of (REAL-NS m),(REAL-NS n);
let X be set ;
assume A1: f is_partial_differentiable_on X,i ;
funcf `partial| (X,i) -> PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) means :: PDIFF_1:def 20
( dom it = X & ( for x being Point of (REAL-NS m) st x in X holds
it /. x = partdiff (f,x,i) ) );
existence
ex b1 being PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) st
( dom b1 = X & ( for x being Point of (REAL-NS m) st x in X holds
b1 /. x = partdiff (f,x,i) ) )
proof
deffunc H1( Element of (REAL-NS m)) -> Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) = partdiff (f,$1,i);
defpred S1[ Element of (REAL-NS m)] means $1 in X;
consider F being PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) such that
A2: ( ( for x being Point of (REAL-NS m) holds
( x in dom F iff S1[x] ) ) & ( for x being Point of (REAL-NS m) st x in dom F holds
F . x = H1(x) ) ) from SEQ_1:sch_3();
take F ; ::_thesis: ( dom F = X & ( for x being Point of (REAL-NS m) st x in X holds
F /. x = partdiff (f,x,i) ) )
now__::_thesis:_for_y_being_set_st_y_in_X_holds_
y_in_dom_F
A3: X is Subset of (REAL-NS m) by A1, Th25;
let y be set ; ::_thesis: ( y in X implies y in dom F )
assume y in X ; ::_thesis: y in dom F
hence y in dom F by A2, A3; ::_thesis: verum
end;
then A4: X c= dom F by TARSKI:def_3;
for y being set st y in dom F holds
y in X by A2;
then dom F c= X by TARSKI:def_3;
hence dom F = X by A4, XBOOLE_0:def_10; ::_thesis: for x being Point of (REAL-NS m) st x in X holds
F /. x = partdiff (f,x,i)
hereby ::_thesis: verum
let x be Point of (REAL-NS m); ::_thesis: ( x in X implies F /. x = partdiff (f,x,i) )
assume x in X ; ::_thesis: F /. x = partdiff (f,x,i)
then A5: x in dom F by A2;
then F . x = partdiff (f,x,i) by A2;
hence F /. x = partdiff (f,x,i) by A5, PARTFUN1:def_6; ::_thesis: verum
end;
end;
uniqueness
for b1, b2 being PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) st dom b1 = X & ( for x being Point of (REAL-NS m) st x in X holds
b1 /. x = partdiff (f,x,i) ) & dom b2 = X & ( for x being Point of (REAL-NS m) st x in X holds
b2 /. x = partdiff (f,x,i) ) holds
b1 = b2
proof
let F, G be PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))); ::_thesis: ( dom F = X & ( for x being Point of (REAL-NS m) st x in X holds
F /. x = partdiff (f,x,i) ) & dom G = X & ( for x being Point of (REAL-NS m) st x in X holds
G /. x = partdiff (f,x,i) ) implies F = G )
assume that
A6: dom F = X and
A7: for x being Point of (REAL-NS m) st x in X holds
F /. x = partdiff (f,x,i) and
A8: dom G = X and
A9: for x being Point of (REAL-NS m) st x in X holds
G /. x = partdiff (f,x,i) ; ::_thesis: F = G
now__::_thesis:_for_x_being_Point_of_(REAL-NS_m)_st_x_in_dom_F_holds_
F_/._x_=_G_/._x
let x be Point of (REAL-NS m); ::_thesis: ( x in dom F implies F /. x = G /. x )
assume A10: x in dom F ; ::_thesis: F /. x = G /. x
then F /. x = partdiff (f,x,i) by A6, A7;
hence F /. x = G /. x by A6, A9, A10; ::_thesis: verum
end;
hence F = G by A6, A8, PARTFUN2:1; ::_thesis: verum
end;
end;
:: deftheorem defines `partial| PDIFF_1:def_20_:_
for m, n being non empty Element of NAT
for i being Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for X being set st f is_partial_differentiable_on X,i holds
for b6 being PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) holds
( b6 = f `partial| (X,i) iff ( dom b6 = X & ( for x being Point of (REAL-NS m) st x in X holds
b6 /. x = partdiff (f,x,i) ) ) );
theorem Th26: :: PDIFF_1:26
for n, m being non empty Element of NAT
for i being Element of NAT
for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds
( (f1 + f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) + (f2 * (reproj (i,x))) & (f1 - f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) - (f2 * (reproj (i,x))) )
proof
let n, m be non empty Element of NAT ; ::_thesis: for i being Element of NAT
for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds
( (f1 + f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) + (f2 * (reproj (i,x))) & (f1 - f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) - (f2 * (reproj (i,x))) )
let i be Element of NAT ; ::_thesis: for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds
( (f1 + f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) + (f2 * (reproj (i,x))) & (f1 - f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) - (f2 * (reproj (i,x))) )
let f1, f2 be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for x being Point of (REAL-NS m) holds
( (f1 + f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) + (f2 * (reproj (i,x))) & (f1 - f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) - (f2 * (reproj (i,x))) )
let x be Point of (REAL-NS m); ::_thesis: ( (f1 + f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) + (f2 * (reproj (i,x))) & (f1 - f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) - (f2 * (reproj (i,x))) )
A1: dom (reproj (i,x)) = the carrier of (REAL-NS 1) by FUNCT_2:def_1;
A2: dom (f1 + f2) = (dom f1) /\ (dom f2) by VFUNCT_1:def_1;
for s being Element of (REAL-NS 1) holds
( s in dom ((f1 + f2) * (reproj (i,x))) iff s in dom ((f1 * (reproj (i,x))) + (f2 * (reproj (i,x)))) )
proof
let s be Element of (REAL-NS 1); ::_thesis: ( s in dom ((f1 + f2) * (reproj (i,x))) iff s in dom ((f1 * (reproj (i,x))) + (f2 * (reproj (i,x)))) )
( s in dom ((f1 + f2) * (reproj (i,x))) iff (reproj (i,x)) . s in (dom f1) /\ (dom f2) ) by A2, A1, FUNCT_1:11;
then ( s in dom ((f1 + f2) * (reproj (i,x))) iff ( (reproj (i,x)) . s in dom f1 & (reproj (i,x)) . s in dom f2 ) ) by XBOOLE_0:def_4;
then ( s in dom ((f1 + f2) * (reproj (i,x))) iff ( s in dom (f1 * (reproj (i,x))) & s in dom (f2 * (reproj (i,x))) ) ) by A1, FUNCT_1:11;
then ( s in dom ((f1 + f2) * (reproj (i,x))) iff s in (dom (f1 * (reproj (i,x)))) /\ (dom (f2 * (reproj (i,x)))) ) by XBOOLE_0:def_4;
hence ( s in dom ((f1 + f2) * (reproj (i,x))) iff s in dom ((f1 * (reproj (i,x))) + (f2 * (reproj (i,x)))) ) by VFUNCT_1:def_1; ::_thesis: verum
end;
then for s being set holds
( s in dom ((f1 + f2) * (reproj (i,x))) iff s in dom ((f1 * (reproj (i,x))) + (f2 * (reproj (i,x)))) ) ;
then A3: dom ((f1 + f2) * (reproj (i,x))) = dom ((f1 * (reproj (i,x))) + (f2 * (reproj (i,x)))) by TARSKI:1;
A4: for z being Element of (REAL-NS 1) st z in dom ((f1 + f2) * (reproj (i,x))) holds
((f1 + f2) * (reproj (i,x))) . z = ((f1 * (reproj (i,x))) + (f2 * (reproj (i,x)))) . z
proof
let z be Element of (REAL-NS 1); ::_thesis: ( z in dom ((f1 + f2) * (reproj (i,x))) implies ((f1 + f2) * (reproj (i,x))) . z = ((f1 * (reproj (i,x))) + (f2 * (reproj (i,x)))) . z )
assume A5: z in dom ((f1 + f2) * (reproj (i,x))) ; ::_thesis: ((f1 + f2) * (reproj (i,x))) . z = ((f1 * (reproj (i,x))) + (f2 * (reproj (i,x)))) . z
then A6: (reproj (i,x)) . z in dom (f1 + f2) by FUNCT_1:11;
A7: (reproj (i,x)) . z in (dom f1) /\ (dom f2) by A2, A5, FUNCT_1:11;
then A8: (reproj (i,x)) . z in dom f1 by XBOOLE_0:def_4;
then A9: z in dom (f1 * (reproj (i,x))) by A1, FUNCT_1:11;
A10: (reproj (i,x)) . z in dom f2 by A7, XBOOLE_0:def_4;
then A11: z in dom (f2 * (reproj (i,x))) by A1, FUNCT_1:11;
A12: f2 /. ((reproj (i,x)) . z) = f2 . ((reproj (i,x)) . z) by A10, PARTFUN1:def_6
.= (f2 * (reproj (i,x))) . z by A11, FUNCT_1:12
.= (f2 * (reproj (i,x))) /. z by A11, PARTFUN1:def_6 ;
A13: f1 /. ((reproj (i,x)) . z) = f1 . ((reproj (i,x)) . z) by A8, PARTFUN1:def_6
.= (f1 * (reproj (i,x))) . z by A9, FUNCT_1:12
.= (f1 * (reproj (i,x))) /. z by A9, PARTFUN1:def_6 ;
((f1 + f2) * (reproj (i,x))) . z = (f1 + f2) . ((reproj (i,x)) . z) by A5, FUNCT_1:12
.= (f1 + f2) /. ((reproj (i,x)) . z) by A6, PARTFUN1:def_6
.= (f1 /. ((reproj (i,x)) . z)) + (f2 /. ((reproj (i,x)) . z)) by A6, VFUNCT_1:def_1
.= ((f1 * (reproj (i,x))) + (f2 * (reproj (i,x)))) /. z by A3, A5, A13, A12, VFUNCT_1:def_1 ;
hence ((f1 + f2) * (reproj (i,x))) . z = ((f1 * (reproj (i,x))) + (f2 * (reproj (i,x)))) . z by A3, A5, PARTFUN1:def_6; ::_thesis: verum
end;
A14: dom (f1 - f2) = (dom f1) /\ (dom f2) by VFUNCT_1:def_2;
for s being Element of (REAL-NS 1) holds
( s in dom ((f1 - f2) * (reproj (i,x))) iff s in dom ((f1 * (reproj (i,x))) - (f2 * (reproj (i,x)))) )
proof
let s be Element of (REAL-NS 1); ::_thesis: ( s in dom ((f1 - f2) * (reproj (i,x))) iff s in dom ((f1 * (reproj (i,x))) - (f2 * (reproj (i,x)))) )
( s in dom ((f1 - f2) * (reproj (i,x))) iff (reproj (i,x)) . s in (dom f1) /\ (dom f2) ) by A14, A1, FUNCT_1:11;
then ( s in dom ((f1 - f2) * (reproj (i,x))) iff ( (reproj (i,x)) . s in dom f1 & (reproj (i,x)) . s in dom f2 ) ) by XBOOLE_0:def_4;
then ( s in dom ((f1 - f2) * (reproj (i,x))) iff ( s in dom (f1 * (reproj (i,x))) & s in dom (f2 * (reproj (i,x))) ) ) by A1, FUNCT_1:11;
then ( s in dom ((f1 - f2) * (reproj (i,x))) iff s in (dom (f1 * (reproj (i,x)))) /\ (dom (f2 * (reproj (i,x)))) ) by XBOOLE_0:def_4;
hence ( s in dom ((f1 - f2) * (reproj (i,x))) iff s in dom ((f1 * (reproj (i,x))) - (f2 * (reproj (i,x)))) ) by VFUNCT_1:def_2; ::_thesis: verum
end;
then for s being set holds
( s in dom ((f1 - f2) * (reproj (i,x))) iff s in dom ((f1 * (reproj (i,x))) - (f2 * (reproj (i,x)))) ) ;
then A15: dom ((f1 - f2) * (reproj (i,x))) = dom ((f1 * (reproj (i,x))) - (f2 * (reproj (i,x)))) by TARSKI:1;
for z being Element of (REAL-NS 1) st z in dom ((f1 - f2) * (reproj (i,x))) holds
((f1 - f2) * (reproj (i,x))) . z = ((f1 * (reproj (i,x))) - (f2 * (reproj (i,x)))) . z
proof
let z be Element of (REAL-NS 1); ::_thesis: ( z in dom ((f1 - f2) * (reproj (i,x))) implies ((f1 - f2) * (reproj (i,x))) . z = ((f1 * (reproj (i,x))) - (f2 * (reproj (i,x)))) . z )
assume A16: z in dom ((f1 - f2) * (reproj (i,x))) ; ::_thesis: ((f1 - f2) * (reproj (i,x))) . z = ((f1 * (reproj (i,x))) - (f2 * (reproj (i,x)))) . z
then A17: (reproj (i,x)) . z in dom (f1 - f2) by FUNCT_1:11;
A18: (reproj (i,x)) . z in (dom f1) /\ (dom f2) by A14, A16, FUNCT_1:11;
then A19: (reproj (i,x)) . z in dom f1 by XBOOLE_0:def_4;
then A20: z in dom (f1 * (reproj (i,x))) by A1, FUNCT_1:11;
A21: (reproj (i,x)) . z in dom f2 by A18, XBOOLE_0:def_4;
then A22: z in dom (f2 * (reproj (i,x))) by A1, FUNCT_1:11;
A23: f2 /. ((reproj (i,x)) . z) = f2 . ((reproj (i,x)) . z) by A21, PARTFUN1:def_6
.= (f2 * (reproj (i,x))) . z by A22, FUNCT_1:12
.= (f2 * (reproj (i,x))) /. z by A22, PARTFUN1:def_6 ;
A24: f1 /. ((reproj (i,x)) . z) = f1 . ((reproj (i,x)) . z) by A19, PARTFUN1:def_6
.= (f1 * (reproj (i,x))) . z by A20, FUNCT_1:12
.= (f1 * (reproj (i,x))) /. z by A20, PARTFUN1:def_6 ;
thus ((f1 - f2) * (reproj (i,x))) . z = (f1 - f2) . ((reproj (i,x)) . z) by A16, FUNCT_1:12
.= (f1 - f2) /. ((reproj (i,x)) . z) by A17, PARTFUN1:def_6
.= (f1 /. ((reproj (i,x)) . z)) - (f2 /. ((reproj (i,x)) . z)) by A17, VFUNCT_1:def_2
.= ((f1 * (reproj (i,x))) - (f2 * (reproj (i,x)))) /. z by A15, A16, A24, A23, VFUNCT_1:def_2
.= ((f1 * (reproj (i,x))) - (f2 * (reproj (i,x)))) . z by A15, A16, PARTFUN1:def_6 ; ::_thesis: verum
end;
hence ( (f1 + f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) + (f2 * (reproj (i,x))) & (f1 - f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) - (f2 * (reproj (i,x))) ) by A3, A15, A4, PARTFUN1:5; ::_thesis: verum
end;
theorem Th27: :: PDIFF_1:27
for n, m being non empty Element of NAT
for i being Element of NAT
for r being Real
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x))
proof
let n, m be non empty Element of NAT ; ::_thesis: for i being Element of NAT
for r being Real
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x))
let i be Element of NAT ; ::_thesis: for r being Real
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x))
let r be Real; ::_thesis: for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x))
let f be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for x being Point of (REAL-NS m) holds r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x))
let x be Point of (REAL-NS m); ::_thesis: r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x))
A1: dom (r (#) f) = dom f by VFUNCT_1:def_4;
A2: dom (r (#) (f * (reproj (i,x)))) = dom (f * (reproj (i,x))) by VFUNCT_1:def_4;
A3: dom (reproj (i,x)) = the carrier of (REAL-NS 1) by FUNCT_2:def_1;
for s being Element of (REAL-NS 1) holds
( s in dom ((r (#) f) * (reproj (i,x))) iff s in dom (f * (reproj (i,x))) )
proof
let s be Element of (REAL-NS 1); ::_thesis: ( s in dom ((r (#) f) * (reproj (i,x))) iff s in dom (f * (reproj (i,x))) )
( s in dom ((r (#) f) * (reproj (i,x))) iff (reproj (i,x)) . s in dom (r (#) f) ) by A3, FUNCT_1:11;
hence ( s in dom ((r (#) f) * (reproj (i,x))) iff s in dom (f * (reproj (i,x))) ) by A1, A3, FUNCT_1:11; ::_thesis: verum
end;
then for s being set holds
( s in dom (r (#) (f * (reproj (i,x)))) iff s in dom ((r (#) f) * (reproj (i,x))) ) by A2;
then A4: dom (r (#) (f * (reproj (i,x)))) = dom ((r (#) f) * (reproj (i,x))) by TARSKI:1;
A5: for s being Element of (REAL-NS 1) holds
( s in dom ((r (#) f) * (reproj (i,x))) iff (reproj (i,x)) . s in dom (r (#) f) )
proof
let s be Element of (REAL-NS 1); ::_thesis: ( s in dom ((r (#) f) * (reproj (i,x))) iff (reproj (i,x)) . s in dom (r (#) f) )
dom (reproj (i,x)) = the carrier of (REAL-NS 1) by FUNCT_2:def_1;
hence ( s in dom ((r (#) f) * (reproj (i,x))) iff (reproj (i,x)) . s in dom (r (#) f) ) by FUNCT_1:11; ::_thesis: verum
end;
for z being Element of (REAL-NS 1) st z in dom (r (#) (f * (reproj (i,x)))) holds
(r (#) (f * (reproj (i,x)))) . z = ((r (#) f) * (reproj (i,x))) . z
proof
let z be Element of (REAL-NS 1); ::_thesis: ( z in dom (r (#) (f * (reproj (i,x)))) implies (r (#) (f * (reproj (i,x)))) . z = ((r (#) f) * (reproj (i,x))) . z )
assume A6: z in dom (r (#) (f * (reproj (i,x)))) ; ::_thesis: (r (#) (f * (reproj (i,x)))) . z = ((r (#) f) * (reproj (i,x))) . z
then A7: z in dom (f * (reproj (i,x))) by VFUNCT_1:def_4;
A8: (reproj (i,x)) . z in dom f by A1, A5, A4, A6;
then A9: f /. ((reproj (i,x)) . z) = f . ((reproj (i,x)) . z) by PARTFUN1:def_6
.= (f * (reproj (i,x))) . z by A7, FUNCT_1:12
.= (f * (reproj (i,x))) /. z by A7, PARTFUN1:def_6 ;
A10: (r (#) (f * (reproj (i,x)))) . z = (r (#) (f * (reproj (i,x)))) /. z by A6, PARTFUN1:def_6
.= r * (f /. ((reproj (i,x)) . z)) by A6, A9, VFUNCT_1:def_4 ;
((r (#) f) * (reproj (i,x))) . z = (r (#) f) . ((reproj (i,x)) . z) by A4, A6, FUNCT_1:12
.= (r (#) f) /. ((reproj (i,x)) . z) by A1, A8, PARTFUN1:def_6
.= r * (f /. ((reproj (i,x)) . z)) by A1, A8, VFUNCT_1:def_4 ;
hence (r (#) (f * (reproj (i,x)))) . z = ((r (#) f) * (reproj (i,x))) . z by A10; ::_thesis: verum
end;
hence r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x)) by A4, PARTFUN1:5; ::_thesis: verum
end;
theorem Th28: :: PDIFF_1:28
for n, m being non empty Element of NAT
for i being Element of NAT
for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds
( f1 + f2 is_partial_differentiable_in x,i & partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) )
proof
let n, m be non empty Element of NAT ; ::_thesis: for i being Element of NAT
for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds
( f1 + f2 is_partial_differentiable_in x,i & partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) )
let i be Element of NAT ; ::_thesis: for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds
( f1 + f2 is_partial_differentiable_in x,i & partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) )
let f1, f2 be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds
( f1 + f2 is_partial_differentiable_in x,i & partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) )
let x be Point of (REAL-NS m); ::_thesis: ( f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i implies ( f1 + f2 is_partial_differentiable_in x,i & partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) ) )
assume that
A1: f1 is_partial_differentiable_in x,i and
A2: f2 is_partial_differentiable_in x,i ; ::_thesis: ( f1 + f2 is_partial_differentiable_in x,i & partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) )
A3: f1 * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by A1, Def9;
A4: f2 * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by A2, Def9;
(f1 + f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) + (f2 * (reproj (i,x))) by Th26;
then (f1 + f2) * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by A3, A4, NDIFF_1:35;
hence f1 + f2 is_partial_differentiable_in x,i by Def9; ::_thesis: partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i))
diff (((f1 * (reproj (i,x))) + (f2 * (reproj (i,x)))),((Proj (i,m)) . x)) = partdiff ((f1 + f2),x,i) by Th26;
hence partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) by A3, A4, NDIFF_1:35; ::_thesis: verum
end;
theorem :: PDIFF_1:29
for n being non empty Element of NAT
for i being Element of NAT
for g1, g2 being PartFunc of (REAL n),REAL
for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds
( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) )
proof
let n be non empty Element of NAT ; ::_thesis: for i being Element of NAT
for g1, g2 being PartFunc of (REAL n),REAL
for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds
( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) )
let i be Element of NAT ; ::_thesis: for g1, g2 being PartFunc of (REAL n),REAL
for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds
( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) )
let g1, g2 be PartFunc of (REAL n),REAL; ::_thesis: for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds
( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) )
let y be Element of REAL n; ::_thesis: ( g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i implies ( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) ) )
assume that
A1: g1 is_partial_differentiable_in y,i and
A2: g2 is_partial_differentiable_in y,i ; ::_thesis: ( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) )
reconsider x = y as Point of (REAL-NS n) by REAL_NS1:def_4;
A3: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4;
then reconsider f1 = <>* g1, f2 = <>* g2 as PartFunc of (REAL-NS n),(REAL-NS 1) by REAL_NS1:def_4;
reconsider One = <*1*> as VECTOR of (REAL-NS 1) by A3, FINSEQ_2:98;
A4: f1 is_partial_differentiable_in x,i by A1, Th14;
then A5: (partdiff (f1,x,i)) . One = <*(partdiff (g1,y,i))*> by Th15;
reconsider Pd2 = <*(partdiff (g2,y,i))*> as Element of REAL 1 by FINSEQ_2:98;
reconsider Pd1 = <*(partdiff (g1,y,i))*> as Element of REAL 1 by FINSEQ_2:98;
A6: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def_4;
rng g2 c= dom ((proj (1,1)) ") by Th2;
then A7: dom (((proj (1,1)) ") * g2) = dom g2 by RELAT_1:27;
rng g1 c= dom ((proj (1,1)) ") by Th2;
then A8: dom (((proj (1,1)) ") * g1) = dom g1 by RELAT_1:27;
then dom (f1 + f2) = (dom g1) /\ (dom g2) by A7, VFUNCT_1:def_1;
then A9: dom (f1 + f2) = dom (g1 + g2) by VALUED_1:def_1;
A10: rng (g1 + g2) c= dom ((proj (1,1)) ") by Th2;
then A11: dom (((proj (1,1)) ") * (g1 + g2)) = dom (g1 + g2) by RELAT_1:27;
A12: now__::_thesis:_for_x_being_Element_of_(REAL-NS_n)_st_x_in_dom_(f1_+_f2)_holds_
(f1_+_f2)_._x_=_(<>*_(g1_+_g2))_._x
let x be Element of (REAL-NS n); ::_thesis: ( x in dom (f1 + f2) implies (f1 + f2) . x = (<>* (g1 + g2)) . x )
assume A13: x in dom (f1 + f2) ; ::_thesis: (f1 + f2) . x = (<>* (g1 + g2)) . x
then (f1 + f2) . x = (f1 + f2) /. x by PARTFUN1:def_6;
then A14: (f1 + f2) . x = (f1 /. x) + (f2 /. x) by A13, VFUNCT_1:def_1;
A15: x in (dom f1) /\ (dom f2) by A13, VFUNCT_1:def_1;
then x in dom f1 by XBOOLE_0:def_4;
then A16: f1 /. x = (((proj (1,1)) ") * g1) . x by PARTFUN1:def_6;
x in dom f2 by A15, XBOOLE_0:def_4;
then A17: f2 /. x = (((proj (1,1)) ") * g2) . x by PARTFUN1:def_6;
x in dom g2 by A7, A15, XBOOLE_0:def_4;
then A18: f2 /. x = ((proj (1,1)) ") . (g2 . x) by A17, FUNCT_1:13;
x in dom g1 by A8, A15, XBOOLE_0:def_4;
then A19: f1 /. x = ((proj (1,1)) ") . (g1 . x) by A16, FUNCT_1:13;
(<>* (g1 + g2)) . x = ((proj (1,1)) ") . ((g1 + g2) . x) by A9, A11, A13, FUNCT_1:12;
then (<>* (g1 + g2)) . x = ((proj (1,1)) ") . ((g1 . x) + (g2 . x)) by A9, A13, VALUED_1:def_1;
hence (f1 + f2) . x = (<>* (g1 + g2)) . x by A14, A19, A18, Th2, Th3; ::_thesis: verum
end;
A20: f2 is_partial_differentiable_in x,i by A2, Th14;
then A21: (partdiff (f2,x,i)) . One = <*(partdiff (g2,y,i))*> by Th15;
A22: f1 + f2 is_partial_differentiable_in x,i by A4, A20, Th28;
dom (f1 + f2) = dom (<>* (g1 + g2)) by A9, A10, RELAT_1:27;
then A23: f1 + f2 = <>* (g1 + g2) by A6, A3, A12, PARTFUN1:5;
then <*(partdiff ((g1 + g2),y,i))*> = (partdiff ((f1 + f2),x,i)) . <*1*> by A4, A20, Th15, Th28
.= ((partdiff (f1,x,i)) + (partdiff (f2,x,i))) . <*1*> by A4, A20, Th28
.= ((partdiff (f1,x,i)) . One) + ((partdiff (f2,x,i)) . One) by LOPBAN_1:35
.= Pd1 + Pd2 by A5, A21, REAL_NS1:2
.= <*((partdiff (g1,y,i)) + (partdiff (g2,y,i)))*> by RVSUM_1:13 ;
then partdiff ((g1 + g2),y,i) = <*((partdiff (g1,y,i)) + (partdiff (g2,y,i)))*> . 1 by FINSEQ_1:40;
hence ( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) ) by A23, A22, Th14, FINSEQ_1:40; ::_thesis: verum
end;
theorem Th30: :: PDIFF_1:30
for n, m being non empty Element of NAT
for i being Element of NAT
for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds
( f1 - f2 is_partial_differentiable_in x,i & partdiff ((f1 - f2),x,i) = (partdiff (f1,x,i)) - (partdiff (f2,x,i)) )
proof
let n, m be non empty Element of NAT ; ::_thesis: for i being Element of NAT
for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds
( f1 - f2 is_partial_differentiable_in x,i & partdiff ((f1 - f2),x,i) = (partdiff (f1,x,i)) - (partdiff (f2,x,i)) )
let i be Element of NAT ; ::_thesis: for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds
( f1 - f2 is_partial_differentiable_in x,i & partdiff ((f1 - f2),x,i) = (partdiff (f1,x,i)) - (partdiff (f2,x,i)) )
let f1, f2 be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds
( f1 - f2 is_partial_differentiable_in x,i & partdiff ((f1 - f2),x,i) = (partdiff (f1,x,i)) - (partdiff (f2,x,i)) )
let x be Point of (REAL-NS m); ::_thesis: ( f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i implies ( f1 - f2 is_partial_differentiable_in x,i & partdiff ((f1 - f2),x,i) = (partdiff (f1,x,i)) - (partdiff (f2,x,i)) ) )
assume that
A1: f1 is_partial_differentiable_in x,i and
A2: f2 is_partial_differentiable_in x,i ; ::_thesis: ( f1 - f2 is_partial_differentiable_in x,i & partdiff ((f1 - f2),x,i) = (partdiff (f1,x,i)) - (partdiff (f2,x,i)) )
A3: f1 * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by A1, Def9;
A4: f2 * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by A2, Def9;
(f1 - f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) - (f2 * (reproj (i,x))) by Th26;
then (f1 - f2) * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by A3, A4, NDIFF_1:36;
hence f1 - f2 is_partial_differentiable_in x,i by Def9; ::_thesis: partdiff ((f1 - f2),x,i) = (partdiff (f1,x,i)) - (partdiff (f2,x,i))
diff (((f1 * (reproj (i,x))) - (f2 * (reproj (i,x)))),((Proj (i,m)) . x)) = partdiff ((f1 - f2),x,i) by Th26;
hence partdiff ((f1 - f2),x,i) = (partdiff (f1,x,i)) - (partdiff (f2,x,i)) by A3, A4, NDIFF_1:36; ::_thesis: verum
end;
theorem :: PDIFF_1:31
for n being non empty Element of NAT
for i being Element of NAT
for g1, g2 being PartFunc of (REAL n),REAL
for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds
( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) )
proof
let n be non empty Element of NAT ; ::_thesis: for i being Element of NAT
for g1, g2 being PartFunc of (REAL n),REAL
for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds
( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) )
let i be Element of NAT ; ::_thesis: for g1, g2 being PartFunc of (REAL n),REAL
for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds
( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) )
let g1, g2 be PartFunc of (REAL n),REAL; ::_thesis: for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds
( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) )
let y be Element of REAL n; ::_thesis: ( g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i implies ( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) ) )
assume that
A1: g1 is_partial_differentiable_in y,i and
A2: g2 is_partial_differentiable_in y,i ; ::_thesis: ( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) )
reconsider x = y as Point of (REAL-NS n) by REAL_NS1:def_4;
A3: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4;
then reconsider f1 = <>* g1, f2 = <>* g2 as PartFunc of (REAL-NS n),(REAL-NS 1) by REAL_NS1:def_4;
reconsider One = <*1*> as VECTOR of (REAL-NS 1) by A3, FINSEQ_2:98;
A4: f1 is_partial_differentiable_in x,i by A1, Th14;
then A5: (partdiff (f1,x,i)) . One = <*(partdiff (g1,y,i))*> by Th15;
reconsider Pd2 = <*(partdiff (g2,y,i))*> as Element of REAL 1 by FINSEQ_2:98;
reconsider Pd1 = <*(partdiff (g1,y,i))*> as Element of REAL 1 by FINSEQ_2:98;
A6: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def_4;
rng g2 c= dom ((proj (1,1)) ") by Th2;
then A7: dom (((proj (1,1)) ") * g2) = dom g2 by RELAT_1:27;
rng g1 c= dom ((proj (1,1)) ") by Th2;
then A8: dom (((proj (1,1)) ") * g1) = dom g1 by RELAT_1:27;
then dom (f1 - f2) = (dom g1) /\ (dom g2) by A7, VFUNCT_1:def_2;
then A9: dom (f1 - f2) = dom (g1 - g2) by VALUED_1:12;
A10: rng (g1 - g2) c= dom ((proj (1,1)) ") by Th2;
then A11: dom (((proj (1,1)) ") * (g1 - g2)) = dom (g1 - g2) by RELAT_1:27;
A12: now__::_thesis:_for_x_being_Element_of_(REAL-NS_n)_st_x_in_dom_(f1_-_f2)_holds_
(f1_-_f2)_._x_=_(<>*_(g1_-_g2))_._x
let x be Element of (REAL-NS n); ::_thesis: ( x in dom (f1 - f2) implies (f1 - f2) . x = (<>* (g1 - g2)) . x )
assume A13: x in dom (f1 - f2) ; ::_thesis: (f1 - f2) . x = (<>* (g1 - g2)) . x
then (f1 - f2) . x = (f1 - f2) /. x by PARTFUN1:def_6;
then A14: (f1 - f2) . x = (f1 /. x) - (f2 /. x) by A13, VFUNCT_1:def_2;
A15: x in (dom f1) /\ (dom f2) by A13, VFUNCT_1:def_2;
then x in dom f1 by XBOOLE_0:def_4;
then A16: f1 /. x = (((proj (1,1)) ") * g1) . x by PARTFUN1:def_6;
x in dom f2 by A15, XBOOLE_0:def_4;
then A17: f2 /. x = (((proj (1,1)) ") * g2) . x by PARTFUN1:def_6;
x in dom g2 by A7, A15, XBOOLE_0:def_4;
then A18: f2 /. x = ((proj (1,1)) ") . (g2 . x) by A17, FUNCT_1:13;
x in dom g1 by A8, A15, XBOOLE_0:def_4;
then A19: f1 /. x = ((proj (1,1)) ") . (g1 . x) by A16, FUNCT_1:13;
(<>* (g1 - g2)) . x = ((proj (1,1)) ") . ((g1 - g2) . x) by A9, A11, A13, FUNCT_1:12;
then (<>* (g1 - g2)) . x = ((proj (1,1)) ") . ((g1 . x) - (g2 . x)) by A9, A13, VALUED_1:13;
hence (f1 - f2) . x = (<>* (g1 - g2)) . x by A14, A19, A18, Th2, Th3; ::_thesis: verum
end;
A20: f2 is_partial_differentiable_in x,i by A2, Th14;
then A21: (partdiff (f2,x,i)) . One = <*(partdiff (g2,y,i))*> by Th15;
A22: f1 - f2 is_partial_differentiable_in x,i by A4, A20, Th30;
dom (f1 - f2) = dom (<>* (g1 - g2)) by A9, A10, RELAT_1:27;
then A23: f1 - f2 = <>* (g1 - g2) by A6, A3, A12, PARTFUN1:5;
then <*(partdiff ((g1 - g2),y,i))*> = (partdiff ((f1 - f2),x,i)) . <*1*> by A4, A20, Th15, Th30
.= ((partdiff (f1,x,i)) - (partdiff (f2,x,i))) . <*1*> by A4, A20, Th30
.= ((partdiff (f1,x,i)) . One) - ((partdiff (f2,x,i)) . One) by LOPBAN_1:40
.= Pd1 - Pd2 by A5, A21, REAL_NS1:5
.= <*((partdiff (g1,y,i)) - (partdiff (g2,y,i)))*> by RVSUM_1:29 ;
then partdiff ((g1 - g2),y,i) = <*((partdiff (g1,y,i)) - (partdiff (g2,y,i)))*> . 1 by FINSEQ_1:40;
hence ( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) ) by A23, A22, Th14, FINSEQ_1:40; ::_thesis: verum
end;
theorem Th32: :: PDIFF_1:32
for n, m being non empty Element of NAT
for i being Element of NAT
for r being Real
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) st f is_partial_differentiable_in x,i holds
( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) )
proof
let n, m be non empty Element of NAT ; ::_thesis: for i being Element of NAT
for r being Real
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) st f is_partial_differentiable_in x,i holds
( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) )
let i be Element of NAT ; ::_thesis: for r being Real
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) st f is_partial_differentiable_in x,i holds
( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) )
let r be Real; ::_thesis: for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) st f is_partial_differentiable_in x,i holds
( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) )
let f be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for x being Point of (REAL-NS m) st f is_partial_differentiable_in x,i holds
( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) )
let x be Point of (REAL-NS m); ::_thesis: ( f is_partial_differentiable_in x,i implies ( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) ) )
assume f is_partial_differentiable_in x,i ; ::_thesis: ( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) )
then A1: f * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by Def9;
r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x)) by Th27;
then (r (#) f) * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by A1, NDIFF_1:37;
hence r (#) f is_partial_differentiable_in x,i by Def9; ::_thesis: partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i))
diff ((r (#) (f * (reproj (i,x)))),((Proj (i,m)) . x)) = partdiff ((r (#) f),x,i) by Th27;
hence partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) by A1, NDIFF_1:37; ::_thesis: verum
end;
theorem :: PDIFF_1:33
for n being non empty Element of NAT
for i being Element of NAT
for r being Real
for g being PartFunc of (REAL n),REAL
for y being Element of REAL n st g is_partial_differentiable_in y,i holds
( r (#) g is_partial_differentiable_in y,i & partdiff ((r (#) g),y,i) = r * (partdiff (g,y,i)) )
proof
let n be non empty Element of NAT ; ::_thesis: for i being Element of NAT
for r being Real
for g being PartFunc of (REAL n),REAL
for y being Element of REAL n st g is_partial_differentiable_in y,i holds
( r (#) g is_partial_differentiable_in y,i & partdiff ((r (#) g),y,i) = r * (partdiff (g,y,i)) )
let i be Element of NAT ; ::_thesis: for r being Real
for g being PartFunc of (REAL n),REAL
for y being Element of REAL n st g is_partial_differentiable_in y,i holds
( r (#) g is_partial_differentiable_in y,i & partdiff ((r (#) g),y,i) = r * (partdiff (g,y,i)) )
let r be Real; ::_thesis: for g being PartFunc of (REAL n),REAL
for y being Element of REAL n st g is_partial_differentiable_in y,i holds
( r (#) g is_partial_differentiable_in y,i & partdiff ((r (#) g),y,i) = r * (partdiff (g,y,i)) )
let g be PartFunc of (REAL n),REAL; ::_thesis: for y being Element of REAL n st g is_partial_differentiable_in y,i holds
( r (#) g is_partial_differentiable_in y,i & partdiff ((r (#) g),y,i) = r * (partdiff (g,y,i)) )
let y be Element of REAL n; ::_thesis: ( g is_partial_differentiable_in y,i implies ( r (#) g is_partial_differentiable_in y,i & partdiff ((r (#) g),y,i) = r * (partdiff (g,y,i)) ) )
A1: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def_4;
A2: rng g c= dom ((proj (1,1)) ") by Th2;
then A3: dom (((proj (1,1)) ") * g) = dom g by RELAT_1:27;
reconsider Pd = <*(partdiff (g,y,i))*> as Element of REAL 1 by FINSEQ_2:98;
reconsider x = y as Point of (REAL-NS n) by REAL_NS1:def_4;
A4: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4;
then reconsider f = <>* g as PartFunc of (REAL-NS n),(REAL-NS 1) by REAL_NS1:def_4;
reconsider One = <*1*> as VECTOR of (REAL-NS 1) by A4, FINSEQ_2:98;
assume g is_partial_differentiable_in y,i ; ::_thesis: ( r (#) g is_partial_differentiable_in y,i & partdiff ((r (#) g),y,i) = r * (partdiff (g,y,i)) )
then A5: f is_partial_differentiable_in x,i by Th14;
then A6: r (#) f is_partial_differentiable_in x,i by Th32;
dom (r (#) f) = dom (((proj (1,1)) ") * g) by VFUNCT_1:def_4;
then dom (r (#) f) = dom g by A2, RELAT_1:27;
then A7: dom (r (#) f) = dom (r (#) g) by VALUED_1:def_5;
A8: rng (r (#) g) c= dom ((proj (1,1)) ") by Th2;
then A9: dom (((proj (1,1)) ") * (r (#) g)) = dom (r (#) g) by RELAT_1:27;
A10: now__::_thesis:_for_x_being_Element_of_(REAL-NS_n)_st_x_in_dom_(r_(#)_f)_holds_
(r_(#)_f)_._x_=_(<>*_(r_(#)_g))_._x
let x be Element of (REAL-NS n); ::_thesis: ( x in dom (r (#) f) implies (r (#) f) . x = (<>* (r (#) g)) . x )
consider I being Function of REAL,(REAL 1) such that
I is bijective and
A11: (proj (1,1)) " = I by Th2;
assume A12: x in dom (r (#) f) ; ::_thesis: (r (#) f) . x = (<>* (r (#) g)) . x
then A13: (<>* (r (#) g)) . x = ((proj (1,1)) ") . ((r (#) g) . x) by A7, A9, FUNCT_1:12;
(r (#) f) . x = (r (#) f) /. x by A12, PARTFUN1:def_6;
then A14: (r (#) f) . x = r * (f /. x) by A12, VFUNCT_1:def_4;
A15: x in dom g by A3, A12, VFUNCT_1:def_4;
then A16: x in dom (r (#) g) by VALUED_1:def_5;
x in dom f by A12, VFUNCT_1:def_4;
then f /. x = (((proj (1,1)) ") * g) . x by PARTFUN1:def_6;
then f /. x = ((proj (1,1)) ") . (g . x) by A15, FUNCT_1:13;
then r * (f /. x) = I . (r * (g . x)) by A11, Th3;
hence (r (#) f) . x = (<>* (r (#) g)) . x by A16, A14, A13, A11, VALUED_1:def_5; ::_thesis: verum
end;
A17: (partdiff (f,x,i)) . One = <*(partdiff (g,y,i))*> by A5, Th15;
dom (r (#) f) = dom (<>* (r (#) g)) by A7, A8, RELAT_1:27;
then A18: r (#) f = <>* (r (#) g) by A1, A4, A10, PARTFUN1:5;
then <*(partdiff ((r (#) g),y,i))*> = (partdiff ((r (#) f),x,i)) . <*1*> by A5, Th15, Th32
.= (r * (partdiff (f,x,i))) . <*1*> by A5, Th32
.= r * ((partdiff (f,x,i)) . One) by LOPBAN_1:36
.= r * Pd by A17, REAL_NS1:3
.= <*(r * (partdiff (g,y,i)))*> by RVSUM_1:47 ;
then partdiff ((r (#) g),y,i) = <*(r * (partdiff (g,y,i)))*> . 1 by FINSEQ_1:40;
hence ( r (#) g is_partial_differentiable_in y,i & partdiff ((r (#) g),y,i) = r * (partdiff (g,y,i)) ) by A18, A6, Th14, FINSEQ_1:40; ::_thesis: verum
end;