let p be Element of REAL 3; :: thesis: 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; :: thesis: ( f is total & f is constant implies grad (f,p) = 0.REAL 3 )
assume A1: ( f is total & f is constant ) ; :: thesis: 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;
now :: thesis: for x being Element of REAL st x in dom (f * (reproj (1,p))) holds
(f * (reproj (1,p))) . x = a
let x be Element of REAL ; :: thesis: ( x in dom (f * (reproj (1,p))) implies (f * (reproj (1,p))) . x = a )
assume x in dom (f * (reproj (1,p))) ; :: thesis: (f * (reproj (1,p))) . x = a
then (f * (reproj (1,p))) . x = f . ((reproj (1,p)) . x) by FUNCT_1:12;
hence (f * (reproj (1,p))) . x = a by A3; :: thesis: verum
end;
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; :: thesis: ( x in REAL implies diff ((f * (reproj (1,p))),x) = 0 )
assume x in REAL ; :: thesis: 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 ; :: thesis: verum
end;
then A8: partdiff (f,p,1) = 0 ;
now :: thesis: for y being Element of REAL st y in dom (f * (reproj (2,p))) holds
(f * (reproj (2,p))) . y = a
let y be Element of REAL ; :: thesis: ( y in dom (f * (reproj (2,p))) implies (f * (reproj (2,p))) . y = a )
assume y in dom (f * (reproj (2,p))) ; :: thesis: (f * (reproj (2,p))) . y = a
then (f * (reproj (2,p))) . y = f . ((reproj (2,p)) . y) by FUNCT_1:12;
hence (f * (reproj (2,p))) . y = a by A3; :: thesis: verum
end;
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; :: thesis: ( y in REAL implies diff ((f * (reproj (2,p))),y) = 0 )
assume y in REAL ; :: thesis: 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 ; :: thesis: verum
end;
then A13: partdiff (f,p,2) = 0 ;
now :: thesis: for z being Element of REAL st z in dom (f * (reproj (3,p))) holds
(f * (reproj (3,p))) . z = a
let z be Element of REAL ; :: thesis: ( z in dom (f * (reproj (3,p))) implies (f * (reproj (3,p))) . z = a )
assume z in dom (f * (reproj (3,p))) ; :: thesis: (f * (reproj (3,p))) . z = a
then (f * (reproj (3,p))) . z = f . ((reproj (3,p)) . z) by FUNCT_1:12;
hence (f * (reproj (3,p))) . z = a by A3; :: thesis: verum
end;
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; :: thesis: ( z in REAL implies diff ((f * (reproj (3,p))),z) = 0 )
assume z in REAL ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: verum