let p be Element of REAL 3; for f being PartFunc of (REAL 3),REAL st f is total & f is constant holds
grad (f,p) = 0.REAL 3
let f be PartFunc of (REAL 3),REAL; ( f is total & f is constant implies grad (f,p) = 0.REAL 3 )
assume A1:
( f is total & f is constant )
; grad (f,p) = 0.REAL 3
then A2:
dom f = REAL 3
by FUNCT_2:def 1;
REAL = [#] REAL
;
then reconsider W = REAL as open Subset of REAL ;
consider a being Element of REAL such that
A3:
for p being Element of REAL 3 st p in REAL 3 holds
f . p = a
by A1, A2, PARTFUN2:def 1;
then A4:
f * (reproj (1,p)) is constant
by PARTFUN2:def 1;
set g1 = f * (reproj (1,p));
A5:
dom (f * (reproj (1,p))) = W
by A1, FUNCT_2:def 1;
A6:
(f * (reproj (1,p))) | W is constant
by A4;
then A7:
f * (reproj (1,p)) is_differentiable_on REAL
by A5, FDIFF_1:22;
for x being Real st x in REAL holds
diff ((f * (reproj (1,p))),x) = 0
proof
let x be
Real;
( x in REAL implies diff ((f * (reproj (1,p))),x) = 0 )
assume
x in REAL
;
diff ((f * (reproj (1,p))),x) = 0
reconsider x =
x as
Element of
REAL by XREAL_0:def 1;
diff (
(f * (reproj (1,p))),
x) =
((f * (reproj (1,p))) `| W) . x
by A7, FDIFF_1:def 7
.=
0
by A5, A6, FDIFF_1:22
;
hence
diff (
(f * (reproj (1,p))),
x)
= 0
;
verum
end;
then A8:
partdiff (f,p,1) = 0
;
then A9:
f * (reproj (2,p)) is constant
by PARTFUN2:def 1;
set g2 = f * (reproj (2,p));
A10:
dom (f * (reproj (2,p))) = W
by A1, FUNCT_2:def 1;
A11:
(f * (reproj (2,p))) | W is constant
by A9;
then A12:
( f * (reproj (2,p)) is_differentiable_on REAL & ( for y being Real st y in REAL holds
((f * (reproj (2,p))) `| W) . y = 0 ) )
by A10, FDIFF_1:22;
for y being Real st y in REAL holds
diff ((f * (reproj (2,p))),y) = 0
proof
let y be
Real;
( y in REAL implies diff ((f * (reproj (2,p))),y) = 0 )
assume
y in REAL
;
diff ((f * (reproj (2,p))),y) = 0
reconsider y =
y as
Element of
REAL by XREAL_0:def 1;
diff (
(f * (reproj (2,p))),
y) =
((f * (reproj (2,p))) `| W) . y
by A12, FDIFF_1:def 7
.=
0
by A10, A11, FDIFF_1:22
;
hence
diff (
(f * (reproj (2,p))),
y)
= 0
;
verum
end;
then A13:
partdiff (f,p,2) = 0
;
then A14:
f * (reproj (3,p)) is constant
by PARTFUN2:def 1;
set g3 = f * (reproj (3,p));
A15:
dom (f * (reproj (3,p))) = W
by A1, FUNCT_2:def 1;
A16:
(f * (reproj (3,p))) | W is constant
by A14;
then A17:
( f * (reproj (3,p)) is_differentiable_on REAL & ( for z being Real st z in REAL holds
((f * (reproj (3,p))) `| W) . z = 0 ) )
by A15, FDIFF_1:22;
for z being Real st z in REAL holds
diff ((f * (reproj (3,p))),z) = 0
proof
let z be
Real;
( z in REAL implies diff ((f * (reproj (3,p))),z) = 0 )
assume
z in REAL
;
diff ((f * (reproj (3,p))),z) = 0
reconsider z =
z as
Element of
REAL by XREAL_0:def 1;
diff (
(f * (reproj (3,p))),
z) =
((f * (reproj (3,p))) `| W) . z
by A17, FDIFF_1:def 7
.=
0
by A15, A16, FDIFF_1:22
;
hence
diff (
(f * (reproj (3,p))),
z)
= 0
;
verum
end;
then
partdiff (f,p,3) = 0
;
then grad (f,p) =
|[0,0,0]|
by A8, A13, Th34
.=
0.REAL 3
by FINSEQ_2:62
;
hence
grad (f,p) = 0.REAL 3
; verum