let m be non zero Element of NAT ; :: thesis: for Z being Subset of (REAL m)
for i being Nat
for f being PartFunc of (REAL m),REAL
for x being Element of REAL m st Z is open & Z c= dom f & 1 <= i & i <= m & x in Z & f is_partial_differentiable_in x,i holds
( f | Z is_partial_differentiable_in x,i & partdiff (f,x,i) = partdiff ((f | Z),x,i) )
let X be Subset of (REAL m); :: thesis: for i being Nat
for f being PartFunc of (REAL m),REAL
for x being Element of REAL m st X is open & X c= dom f & 1 <= i & i <= m & x in X & f is_partial_differentiable_in x,i holds
( f | X is_partial_differentiable_in x,i & partdiff (f,x,i) = partdiff ((f | X),x,i) )
let i be Nat; :: thesis: for f being PartFunc of (REAL m),REAL
for x being Element of REAL m st X is open & X c= dom f & 1 <= i & i <= m & x in X & f is_partial_differentiable_in x,i holds
( f | X is_partial_differentiable_in x,i & partdiff (f,x,i) = partdiff ((f | X),x,i) )
let f be PartFunc of (REAL m),REAL; :: thesis: for x being Element of REAL m st X is open & X c= dom f & 1 <= i & i <= m & x in X & f is_partial_differentiable_in x,i holds
( f | X is_partial_differentiable_in x,i & partdiff (f,x,i) = partdiff ((f | X),x,i) )
let nx0 be Element of REAL m; :: thesis: ( X is open & X c= dom f & 1 <= i & i <= m & nx0 in X & f is_partial_differentiable_in nx0,i implies ( f | X is_partial_differentiable_in nx0,i & partdiff (f,nx0,i) = partdiff ((f | X),nx0,i) ) )
assume A1: ( X is open & X c= dom f & 1 <= i & i <= m & nx0 in X & f is_partial_differentiable_in nx0,i ) ; :: thesis: ( f | X is_partial_differentiable_in nx0,i & partdiff (f,nx0,i) = partdiff ((f | X),nx0,i) )
set x0 = (proj (i,m)) . nx0;
consider N0 being Neighbourhood of (proj (i,m)) . nx0 such that
A2: ( N0 c= dom (f * (reproj (i,nx0))) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N0 holds
((f * (reproj (i,nx0))) . x) - ((f * (reproj (i,nx0))) . ((proj (i,m)) . nx0)) = (L . (x - ((proj (i,m)) . nx0))) + (R . (x - ((proj (i,m)) . nx0))) ) by A1, FDIFF_1:def 4;
consider N1 being Neighbourhood of (proj (i,m)) . nx0 such that
A3: for x being Element of REAL st x in N1 holds
(reproj (i,nx0)) . x in X by A1, Lm2;
A4: now :: thesis: for x being Element of REAL st x in N1 holds
(reproj (i,nx0)) . x in dom (f | X)
let x be Element of REAL ; :: thesis: ( x in N1 implies (reproj (i,nx0)) . x in dom (f | X) )
assume x in N1 ; :: thesis: (reproj (i,nx0)) . x in dom (f | X)
then (reproj (i,nx0)) . x in X by A3;
then (reproj (i,nx0)) . x in (dom f) /\ X by A1, XBOOLE_0:def 4;
hence (reproj (i,nx0)) . x in dom (f | X) by RELAT_1:61; :: thesis: verum
end;
consider N being Neighbourhood of (proj (i,m)) . nx0 such that
A5: ( N c= N0 & N c= N1 ) by RCOMP_1:17;
N1 c= dom ((f | X) * (reproj (i,nx0)))
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in N1 or z in dom ((f | X) * (reproj (i,nx0))) )
assume A6: z in N1 ; :: thesis: z in dom ((f | X) * (reproj (i,nx0)))
then reconsider x = z as Element of REAL ;
A7: (reproj (i,nx0)) . x in dom (f | X) by A6, A4;
z in REAL by A6;
then z in dom (reproj (i,nx0)) by FUNCT_2:def 1;
hence z in dom ((f | X) * (reproj (i,nx0))) by A7, FUNCT_1:11; :: thesis: verum
end;
then A8: N c= dom ((f | X) * (reproj (i,nx0))) by A5;
consider L being LinearFunc, R being RestFunc such that
A9: for x being Real st x in N0 holds
((f * (reproj (i,nx0))) . x) - ((f * (reproj (i,nx0))) . ((proj (i,m)) . nx0)) = (L . (x - ((proj (i,m)) . nx0))) + (R . (x - ((proj (i,m)) . nx0))) by A2;
A10: now :: thesis: for xx being Real st xx in N holds
(((f | X) * (reproj (i,nx0))) . xx) - (((f | X) * (reproj (i,nx0))) . ((proj (i,m)) . nx0)) = (L . (xx - ((proj (i,m)) . nx0))) + (R . (xx - ((proj (i,m)) . nx0)))
let xx be Real; :: thesis: ( xx in N implies (((f | X) * (reproj (i,nx0))) . xx) - (((f | X) * (reproj (i,nx0))) . ((proj (i,m)) . nx0)) = (L . (xx - ((proj (i,m)) . nx0))) + (R . (xx - ((proj (i,m)) . nx0))) )
assume A11: xx in N ; :: thesis: (((f | X) * (reproj (i,nx0))) . xx) - (((f | X) * (reproj (i,nx0))) . ((proj (i,m)) . nx0)) = (L . (xx - ((proj (i,m)) . nx0))) + (R . (xx - ((proj (i,m)) . nx0)))
reconsider x = xx as Element of REAL by XREAL_0:def 1;
A12: dom (reproj (i,nx0)) = REAL by FUNCT_2:def 1;
A13: (reproj (i,nx0)) . ((proj (i,m)) . nx0) in dom (f | X) by A4, RCOMP_1:16;
A14: ((f | X) * (reproj (i,nx0))) . x = (f | X) . ((reproj (i,nx0)) /. x) by A12, FUNCT_1:13
.= f . ((reproj (i,nx0)) . x) by A4, A11, A5, FUNCT_1:47
.= (f * (reproj (i,nx0))) . x by A12, FUNCT_1:13 ;
((f | X) * (reproj (i,nx0))) . ((proj (i,m)) . nx0) = (f | X) . ((reproj (i,nx0)) . ((proj (i,m)) . nx0)) by A12, FUNCT_1:13
.= f . ((reproj (i,nx0)) . ((proj (i,m)) . nx0)) by A13, FUNCT_1:47
.= (f * (reproj (i,nx0))) . ((proj (i,m)) . nx0) by A12, FUNCT_1:13 ;
hence (((f | X) * (reproj (i,nx0))) . xx) - (((f | X) * (reproj (i,nx0))) . ((proj (i,m)) . nx0)) = (L . (xx - ((proj (i,m)) . nx0))) + (R . (xx - ((proj (i,m)) . nx0))) by A14, A11, A9, A5; :: thesis: verum
end;
hence f | X is_partial_differentiable_in nx0,i by A8, FDIFF_1:def 4; :: thesis: partdiff (f,nx0,i) = partdiff ((f | X),nx0,i)
(f | X) * (reproj (i,nx0)) is_differentiable_in (proj (i,m)) . nx0 by A8, A10, FDIFF_1:def 4;
then partdiff ((f | X),nx0,i) = L . 1 by A10, A8, FDIFF_1:def 5;
hence partdiff (f,nx0,i) = partdiff ((f | X),nx0,i) by A2, A9, A1, FDIFF_1:def 5; :: thesis: verum