let E, F, G be RealNormSpace; for f being PartFunc of [:E,F:],G
for Z being Subset of [:E,F:]
for z being Point of [:E,F:] st Z is open & z in Z & Z c= dom f holds
( ( f is_partial_differentiable_in`1 z implies ( f | Z is_partial_differentiable_in`1 z & partdiff`1 (f,z) = partdiff`1 ((f | Z),z) ) ) & ( f is_partial_differentiable_in`2 z implies ( f | Z is_partial_differentiable_in`2 z & partdiff`2 (f,z) = partdiff`2 ((f | Z),z) ) ) )
let f be PartFunc of [:E,F:],G; for Z being Subset of [:E,F:]
for z being Point of [:E,F:] st Z is open & z in Z & Z c= dom f holds
( ( f is_partial_differentiable_in`1 z implies ( f | Z is_partial_differentiable_in`1 z & partdiff`1 (f,z) = partdiff`1 ((f | Z),z) ) ) & ( f is_partial_differentiable_in`2 z implies ( f | Z is_partial_differentiable_in`2 z & partdiff`2 (f,z) = partdiff`2 ((f | Z),z) ) ) )
let Z be Subset of [:E,F:]; for z being Point of [:E,F:] st Z is open & z in Z & Z c= dom f holds
( ( f is_partial_differentiable_in`1 z implies ( f | Z is_partial_differentiable_in`1 z & partdiff`1 (f,z) = partdiff`1 ((f | Z),z) ) ) & ( f is_partial_differentiable_in`2 z implies ( f | Z is_partial_differentiable_in`2 z & partdiff`2 (f,z) = partdiff`2 ((f | Z),z) ) ) )
let z be Point of [:E,F:]; ( Z is open & z in Z & Z c= dom f implies ( ( f is_partial_differentiable_in`1 z implies ( f | Z is_partial_differentiable_in`1 z & partdiff`1 (f,z) = partdiff`1 ((f | Z),z) ) ) & ( f is_partial_differentiable_in`2 z implies ( f | Z is_partial_differentiable_in`2 z & partdiff`2 (f,z) = partdiff`2 ((f | Z),z) ) ) ) )
assume A1:
( Z is open & z in Z & Z c= dom f )
; ( ( f is_partial_differentiable_in`1 z implies ( f | Z is_partial_differentiable_in`1 z & partdiff`1 (f,z) = partdiff`1 ((f | Z),z) ) ) & ( f is_partial_differentiable_in`2 z implies ( f | Z is_partial_differentiable_in`2 z & partdiff`2 (f,z) = partdiff`2 ((f | Z),z) ) ) )
A2:
ex x1 being Point of E ex x2 being Point of F st z = [x1,x2]
by PRVECT_3:18;
thus
( f is_partial_differentiable_in`1 z implies ( f | Z is_partial_differentiable_in`1 z & partdiff`1 (f,z) = partdiff`1 ((f | Z),z) ) )
( f is_partial_differentiable_in`2 z implies ( f | Z is_partial_differentiable_in`2 z & partdiff`2 (f,z) = partdiff`2 ((f | Z),z) ) )proof
assume A4:
f is_partial_differentiable_in`1 z
;
( f | Z is_partial_differentiable_in`1 z & partdiff`1 (f,z) = partdiff`1 ((f | Z),z) )
set g =
f * (reproj1 z);
consider N being
Neighbourhood of
z `1 such that A6:
(
N c= dom (f * (reproj1 z)) & ex
R being
RestFunc of
E,
G st
for
x being
Point of
E st
x in N holds
((f * (reproj1 z)) /. x) - ((f * (reproj1 z)) /. (z `1)) = ((partdiff`1 (f,z)) . (x - (z `1))) + (R /. (x - (z `1))) )
by A4, NDIFF_1:def 7;
consider R being
RestFunc of
E,
G such that A7:
for
x being
Point of
E st
x in N holds
((f * (reproj1 z)) /. x) - ((f * (reproj1 z)) /. (z `1)) = ((partdiff`1 (f,z)) . (x - (z `1))) + (R /. (x - (z `1)))
by A6;
set h =
(f | Z) * (reproj1 z);
A9:
(reproj1 z) . (z `1) =
[(z `1),(z `2)]
by NDIFF_7:def 1
.=
z
by A2
;
consider r1 being
Real such that A10:
(
r1 > 0 &
Ball (
z,
r1)
c= Z )
by A1, NDIFF_8:20;
A11:
Ball (
z,
r1)
= { y where y is Point of [:E,F:] : ||.(y - z).|| < r1 }
by NDIFF_8:17;
consider r2 being
Real such that A13:
(
r2 > 0 &
{ y where y is Point of E : ||.(y - (z `1)).|| < r2 } c= N )
by NFCONT_1:def 1;
set r =
min (
r1,
r2);
A14:
(
0 < min (
r1,
r2) &
min (
r1,
r2)
<= r1 &
min (
r1,
r2)
<= r2 )
by A10, A13, XXREAL_0:15, XXREAL_0:17;
set M =
Ball (
(z `1),
(min (r1,r2)));
A15:
Ball (
(z `1),
(min (r1,r2)))
= { y where y is Point of E : ||.(y - (z `1)).|| < min (r1,r2) }
by NDIFF_8:17;
then reconsider M =
Ball (
(z `1),
(min (r1,r2))) as
Neighbourhood of
z `1 by A14, NFCONT_1:def 1;
A17:
{ y where y is Point of E : ||.(y - (z `1)).|| < r2 } = Ball (
(z `1),
r2)
by NDIFF_8:17;
A18:
M c= Ball (
(z `1),
r2)
by A14, NDIFF_8:15;
A19:
(
M c= N & ( for
x being
Point of
E st
x in M holds
(reproj1 z) . x in Z ) )
proof
thus
M c= N
by A13, A17, A18, XBOOLE_1:1;
for x being Point of E st x in M holds
(reproj1 z) . x in Z
let x be
Point of
E;
( x in M implies (reproj1 z) . x in Z )
assume
x in M
;
(reproj1 z) . x in Z
then A20:
ex
y being
Point of
E st
(
x = y &
||.(y - (z `1)).|| < min (
r1,
r2) )
by A15;
A21:
(reproj1 z) . x = [x,(z `2)]
by NDIFF_7:def 1;
- z = [(- (z `1)),(- (z `2))]
by A2, PRVECT_3:18;
then ((reproj1 z) . x) - z =
[(x - (z `1)),((z `2) - (z `2))]
by A21, PRVECT_3:18
.=
[(x - (z `1)),(0. F)]
by RLVECT_1:15
;
then
||.(((reproj1 z) . x) - z).|| = ||.(x - (z `1)).||
by NDIFF_8:2;
then
||.(((reproj1 z) . x) - z).|| < r1
by A14, A20, XXREAL_0:2;
then
(reproj1 z) . x in { y where y is Point of [:E,F:] : ||.(y - z).|| < r1 }
;
hence
(reproj1 z) . x in Z
by A10, A11;
verum
end;
A22:
dom (reproj1 z) = the
carrier of
E
by FUNCT_2:def 1;
A23:
dom (f | Z) = Z
by A1, RELAT_1:62;
A24:
M c= dom ((f | Z) * (reproj1 z))
A27:
for
x being
Point of
E st
x in M holds
(((f | Z) * (reproj1 z)) /. x) - (((f | Z) * (reproj1 z)) /. (z `1)) = ((partdiff`1 (f,z)) . (x - (z `1))) + (R /. (x - (z `1)))
proof
let x be
Point of
E;
( x in M implies (((f | Z) * (reproj1 z)) /. x) - (((f | Z) * (reproj1 z)) /. (z `1)) = ((partdiff`1 (f,z)) . (x - (z `1))) + (R /. (x - (z `1))) )
assume A28:
x in M
;
(((f | Z) * (reproj1 z)) /. x) - (((f | Z) * (reproj1 z)) /. (z `1)) = ((partdiff`1 (f,z)) . (x - (z `1))) + (R /. (x - (z `1)))
then A29:
x in N
by A19;
A30:
z `1 in N
by NFCONT_1:4;
A31:
z `1 in M
by NFCONT_1:4;
A33:
((f | Z) * (reproj1 z)) /. x =
((f | Z) * (reproj1 z)) . x
by A24, A28, PARTFUN1:def 6
.=
(f | Z) . ((reproj1 z) . x)
by A22, FUNCT_1:13
.=
f . ((reproj1 z) . x)
by A19, A28, FUNCT_1:49
.=
(f * (reproj1 z)) . x
by A22, FUNCT_1:13
.=
(f * (reproj1 z)) /. x
by A6, A29, PARTFUN1:def 6
;
((f | Z) * (reproj1 z)) /. (z `1) =
((f | Z) * (reproj1 z)) . (z `1)
by A24, A31, PARTFUN1:def 6
.=
(f | Z) . ((reproj1 z) . (z `1))
by A22, FUNCT_1:13
.=
f . ((reproj1 z) . (z `1))
by A1, A9, FUNCT_1:49
.=
(f * (reproj1 z)) . (z `1)
by A22, FUNCT_1:13
.=
(f * (reproj1 z)) /. (z `1)
by A6, A30, PARTFUN1:def 6
;
hence
(((f | Z) * (reproj1 z)) /. x) - (((f | Z) * (reproj1 z)) /. (z `1)) = ((partdiff`1 (f,z)) . (x - (z `1))) + (R /. (x - (z `1)))
by A7, A19, A28, A33;
verum
end;
then A35:
(f | Z) * (reproj1 z) is_differentiable_in z `1
by A24, NDIFF_1:def 6;
thus
f | Z is_partial_differentiable_in`1 z
by A24, A27, NDIFF_1:def 6;
partdiff`1 (f,z) = partdiff`1 ((f | Z),z)
thus
partdiff`1 (
(f | Z),
z)
= partdiff`1 (
f,
z)
by A35, A24, A27, NDIFF_1:def 7;
verum
end;
assume A38:
f is_partial_differentiable_in`2 z
; ( f | Z is_partial_differentiable_in`2 z & partdiff`2 (f,z) = partdiff`2 ((f | Z),z) )
set g = f * (reproj2 z);
consider N being Neighbourhood of z `2 such that
A40:
( N c= dom (f * (reproj2 z)) & ex R being RestFunc of F,G st
for x being Point of F st x in N holds
((f * (reproj2 z)) /. x) - ((f * (reproj2 z)) /. (z `2)) = ((partdiff`2 (f,z)) . (x - (z `2))) + (R /. (x - (z `2))) )
by A38, NDIFF_1:def 7;
consider R being RestFunc of F,G such that
A41:
for x being Point of F st x in N holds
((f * (reproj2 z)) /. x) - ((f * (reproj2 z)) /. (z `2)) = ((partdiff`2 (f,z)) . (x - (z `2))) + (R /. (x - (z `2)))
by A40;
set h = (f | Z) * (reproj2 z);
A43: (reproj2 z) . (z `2) =
[(z `1),(z `2)]
by NDIFF_7:def 2
.=
z
by A2
;
consider r1 being Real such that
A44:
( r1 > 0 & Ball (z,r1) c= Z )
by A1, NDIFF_8:20;
A45:
Ball (z,r1) = { y where y is Point of [:E,F:] : ||.(y - z).|| < r1 }
by NDIFF_8:17;
consider r2 being Real such that
A47:
( r2 > 0 & { y where y is Point of F : ||.(y - (z `2)).|| < r2 } c= N )
by NFCONT_1:def 1;
set r = min (r1,r2);
A48:
( 0 < min (r1,r2) & min (r1,r2) <= r1 & min (r1,r2) <= r2 )
by A44, A47, XXREAL_0:15, XXREAL_0:17;
set M = Ball ((z `2),(min (r1,r2)));
A49:
Ball ((z `2),(min (r1,r2))) = { y where y is Point of F : ||.(y - (z `2)).|| < min (r1,r2) }
by NDIFF_8:17;
then reconsider M = Ball ((z `2),(min (r1,r2))) as Neighbourhood of z `2 by A48, NFCONT_1:def 1;
A51:
{ y where y is Point of F : ||.(y - (z `2)).|| < r2 } = Ball ((z `2),r2)
by NDIFF_8:17;
A52:
M c= Ball ((z `2),r2)
by A48, NDIFF_8:15;
A53:
( M c= N & ( for x being Point of F st x in M holds
(reproj2 z) . x in Z ) )
proof
thus
M c= N
by A47, A51, A52, XBOOLE_1:1;
for x being Point of F st x in M holds
(reproj2 z) . x in Z
let x be
Point of
F;
( x in M implies (reproj2 z) . x in Z )
assume
x in M
;
(reproj2 z) . x in Z
then A54:
ex
y being
Point of
F st
(
x = y &
||.(y - (z `2)).|| < min (
r1,
r2) )
by A49;
A55:
(reproj2 z) . x = [(z `1),x]
by NDIFF_7:def 2;
- z = [(- (z `1)),(- (z `2))]
by A2, PRVECT_3:18;
then ((reproj2 z) . x) - z =
[((z `1) - (z `1)),(x - (z `2))]
by A55, PRVECT_3:18
.=
[(0. E),(x - (z `2))]
by RLVECT_1:15
;
then
||.(((reproj2 z) . x) - z).|| = ||.(x - (z `2)).||
by NDIFF_8:3;
then
||.(((reproj2 z) . x) - z).|| < r1
by A48, A54, XXREAL_0:2;
then
(reproj2 z) . x in { y where y is Point of [:E,F:] : ||.(y - z).|| < r1 }
;
hence
(reproj2 z) . x in Z
by A44, A45;
verum
end;
A56:
dom (reproj2 z) = the carrier of F
by FUNCT_2:def 1;
A57:
dom (f | Z) = Z
by A1, RELAT_1:62;
A58:
M c= dom ((f | Z) * (reproj2 z))
A61:
for x being Point of F st x in M holds
(((f | Z) * (reproj2 z)) /. x) - (((f | Z) * (reproj2 z)) /. (z `2)) = ((partdiff`2 (f,z)) . (x - (z `2))) + (R /. (x - (z `2)))
proof
let x be
Point of
F;
( x in M implies (((f | Z) * (reproj2 z)) /. x) - (((f | Z) * (reproj2 z)) /. (z `2)) = ((partdiff`2 (f,z)) . (x - (z `2))) + (R /. (x - (z `2))) )
assume A62:
x in M
;
(((f | Z) * (reproj2 z)) /. x) - (((f | Z) * (reproj2 z)) /. (z `2)) = ((partdiff`2 (f,z)) . (x - (z `2))) + (R /. (x - (z `2)))
then A63:
x in N
by A53;
A64:
z `2 in N
by NFCONT_1:4;
A65:
z `2 in M
by NFCONT_1:4;
A67:
((f | Z) * (reproj2 z)) /. x =
((f | Z) * (reproj2 z)) . x
by A58, A62, PARTFUN1:def 6
.=
(f | Z) . ((reproj2 z) . x)
by A56, FUNCT_1:13
.=
f . ((reproj2 z) . x)
by A53, A62, FUNCT_1:49
.=
(f * (reproj2 z)) . x
by A56, FUNCT_1:13
.=
(f * (reproj2 z)) /. x
by A40, A63, PARTFUN1:def 6
;
((f | Z) * (reproj2 z)) /. (z `2) =
((f | Z) * (reproj2 z)) . (z `2)
by A58, A65, PARTFUN1:def 6
.=
(f | Z) . ((reproj2 z) . (z `2))
by A56, FUNCT_1:13
.=
f . ((reproj2 z) . (z `2))
by A1, A43, FUNCT_1:49
.=
(f * (reproj2 z)) . (z `2)
by A56, FUNCT_1:13
.=
(f * (reproj2 z)) /. (z `2)
by A40, A64, PARTFUN1:def 6
;
hence
(((f | Z) * (reproj2 z)) /. x) - (((f | Z) * (reproj2 z)) /. (z `2)) = ((partdiff`2 (f,z)) . (x - (z `2))) + (R /. (x - (z `2)))
by A41, A53, A62, A67;
verum
end;
hence
f | Z is_partial_differentiable_in`2 z
by A58, NDIFF_1:def 6; partdiff`2 (f,z) = partdiff`2 ((f | Z),z)
(f | Z) * (reproj2 z) is_differentiable_in z `2
by A58, A61, NDIFF_1:def 6;
hence
partdiff`2 ((f | Z),z) = partdiff`2 (f,z)
by A58, A61, NDIFF_1:def 7; verum