:: Partial Differentiation of Real Ternary Functions :: by Takao Inou\'e , Bing Xie and Xiquan Liang :: :: Received November 7, 2009 :: Copyright (c) 2009-2012 Association of Mizar Users begin theorem Th1: :: PDIFF_4:1 ( dom (proj (1,3)) = REAL 3 & rng (proj (1,3)) = REAL & ( for x, y, z being Element of REAL holds (proj (1,3)) . <*x,y,z*> = x ) ) proofend; theorem Th2: :: PDIFF_4:2 ( dom (proj (2,3)) = REAL 3 & rng (proj (2,3)) = REAL & ( for x, y, z being Element of REAL holds (proj (2,3)) . <*x,y,z*> = y ) ) proofend; theorem Th3: :: PDIFF_4:3 ( dom (proj (3,3)) = REAL 3 & rng (proj (3,3)) = REAL & ( for x, y, z being Element of REAL holds (proj (3,3)) . <*x,y,z*> = z ) ) proofend; begin theorem Th4: :: PDIFF_4:4 for x, y, z being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x,y,z*> & f is_partial_differentiable_in u,1 holds SVF1 (1,f,u) is_differentiable_in x proofend; theorem Th5: :: PDIFF_4:5 for x, y, z being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x,y,z*> & f is_partial_differentiable_in u,2 holds SVF1 (2,f,u) is_differentiable_in y proofend; theorem Th6: :: PDIFF_4:6 for x, y, z being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x,y,z*> & f is_partial_differentiable_in u,3 holds SVF1 (3,f,u) is_differentiable_in z proofend; theorem Th7: :: PDIFF_4:7 for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 holds ( ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & SVF1 (1,f,u) is_differentiable_in x0 ) iff f is_partial_differentiable_in u,1 ) proofend; theorem Th8: :: PDIFF_4:8 for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 holds ( ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & SVF1 (2,f,u) is_differentiable_in y0 ) iff f is_partial_differentiable_in u,2 ) proofend; theorem Th9: :: PDIFF_4:9 for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 holds ( ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & SVF1 (3,f,u) is_differentiable_in z0 ) iff f is_partial_differentiable_in u,3 ) proofend; theorem :: PDIFF_4:10 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 holds ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) proofend; theorem :: PDIFF_4:11 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 holds ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) proofend; theorem :: PDIFF_4:12 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 holds ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st for z being Real st z in N holds ((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) proofend; theorem Th13: :: PDIFF_4:13 for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 holds ( f is_partial_differentiable_in u,1 iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) proofend; theorem Th14: :: PDIFF_4:14 for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 holds ( f is_partial_differentiable_in u,2 iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) proofend; theorem Th15: :: PDIFF_4:15 for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 holds ( f is_partial_differentiable_in u,3 iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st for z being Real st z in N holds ((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) proofend; Lm1: for x0, y0, z0, r being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 holds ( r = diff ((SVF1 (1,f,u)),x0) iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) ) proofend; Lm2: for x0, y0, z0, r being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 holds ( r = diff ((SVF1 (2,f,u)),y0) iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) ) proofend; Lm3: for x0, y0, z0, r being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 holds ( r = diff ((SVF1 (3,f,u)),z0) iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for z being Real st z in N holds ((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) ) proofend; theorem Th16: :: PDIFF_4:16 for x0, y0, z0, r being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 holds ( r = partdiff (f,u,1) iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) ) proofend; theorem Th17: :: PDIFF_4:17 for x0, y0, z0, r being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 holds ( r = partdiff (f,u,2) iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) ) proofend; theorem Th18: :: PDIFF_4:18 for x0, y0, z0, r being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 holds ( r = partdiff (f,u,3) iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for z being Real st z in N holds ((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) ) proofend; theorem :: PDIFF_4:19 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> holds partdiff (f,u,1) = diff ((SVF1 (1,f,u)),x0) by Th1; theorem :: PDIFF_4:20 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> holds partdiff (f,u,2) = diff ((SVF1 (2,f,u)),y0) by Th2; theorem :: PDIFF_4:21 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> holds partdiff (f,u,3) = diff ((SVF1 (3,f,u)),z0) by Th3; definition let f be PartFunc of (REAL 3),REAL; let D be set ; predf is_partial_differentiable`1_on D means :Def1: :: PDIFF_4:def 1 ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_partial_differentiable_in u,1 ) ); predf is_partial_differentiable`2_on D means :Def2: :: PDIFF_4:def 2 ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_partial_differentiable_in u,2 ) ); predf is_partial_differentiable`3_on D means :Def3: :: PDIFF_4:def 3 ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_partial_differentiable_in u,3 ) ); end; :: deftheorem Def1 defines is_partial_differentiable`1_on PDIFF_4:def_1_:_ for f being PartFunc of (REAL 3),REAL for D being set holds ( f is_partial_differentiable`1_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_partial_differentiable_in u,1 ) ) ); :: deftheorem Def2 defines is_partial_differentiable`2_on PDIFF_4:def_2_:_ for f being PartFunc of (REAL 3),REAL for D being set holds ( f is_partial_differentiable`2_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_partial_differentiable_in u,2 ) ) ); :: deftheorem Def3 defines is_partial_differentiable`3_on PDIFF_4:def_3_:_ for f being PartFunc of (REAL 3),REAL for D being set holds ( f is_partial_differentiable`3_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_partial_differentiable_in u,3 ) ) ); theorem :: PDIFF_4:22 for D being set for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable`1_on D holds ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f is_partial_differentiable_in u,1 ) ) proofend; theorem :: PDIFF_4:23 for D being set for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable`2_on D holds ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f is_partial_differentiable_in u,2 ) ) proofend; theorem :: PDIFF_4:24 for D being set for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable`3_on D holds ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f is_partial_differentiable_in u,3 ) ) proofend; definition let f be PartFunc of (REAL 3),REAL; let D be set ; assume A1: f is_partial_differentiable`1_on D ; funcf `partial1| D -> PartFunc of (REAL 3),REAL means :: PDIFF_4:def 4 ( dom it = D & ( for u being Element of REAL 3 st u in D holds it . u = partdiff (f,u,1) ) ); existence ex b1 being PartFunc of (REAL 3),REAL st ( dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = partdiff (f,u,1) ) ) proofend; uniqueness for b1, b2 being PartFunc of (REAL 3),REAL st dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = partdiff (f,u,1) ) & dom b2 = D & ( for u being Element of REAL 3 st u in D holds b2 . u = partdiff (f,u,1) ) holds b1 = b2 proofend; end; :: deftheorem defines `partial1| PDIFF_4:def_4_:_ for f being PartFunc of (REAL 3),REAL for D being set st f is_partial_differentiable`1_on D holds for b3 being PartFunc of (REAL 3),REAL holds ( b3 = f `partial1| D iff ( dom b3 = D & ( for u being Element of REAL 3 st u in D holds b3 . u = partdiff (f,u,1) ) ) ); definition let f be PartFunc of (REAL 3),REAL; let D be set ; assume A1: f is_partial_differentiable`2_on D ; funcf `partial2| D -> PartFunc of (REAL 3),REAL means :: PDIFF_4:def 5 ( dom it = D & ( for u being Element of REAL 3 st u in D holds it . u = partdiff (f,u,2) ) ); existence ex b1 being PartFunc of (REAL 3),REAL st ( dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = partdiff (f,u,2) ) ) proofend; uniqueness for b1, b2 being PartFunc of (REAL 3),REAL st dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = partdiff (f,u,2) ) & dom b2 = D & ( for u being Element of REAL 3 st u in D holds b2 . u = partdiff (f,u,2) ) holds b1 = b2 proofend; end; :: deftheorem defines `partial2| PDIFF_4:def_5_:_ for f being PartFunc of (REAL 3),REAL for D being set st f is_partial_differentiable`2_on D holds for b3 being PartFunc of (REAL 3),REAL holds ( b3 = f `partial2| D iff ( dom b3 = D & ( for u being Element of REAL 3 st u in D holds b3 . u = partdiff (f,u,2) ) ) ); definition let f be PartFunc of (REAL 3),REAL; let D be set ; assume A1: f is_partial_differentiable`3_on D ; funcf `partial3| D -> PartFunc of (REAL 3),REAL means :: PDIFF_4:def 6 ( dom it = D & ( for u being Element of REAL 3 st u in D holds it . u = partdiff (f,u,3) ) ); existence ex b1 being PartFunc of (REAL 3),REAL st ( dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = partdiff (f,u,3) ) ) proofend; uniqueness for b1, b2 being PartFunc of (REAL 3),REAL st dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = partdiff (f,u,3) ) & dom b2 = D & ( for u being Element of REAL 3 st u in D holds b2 . u = partdiff (f,u,3) ) holds b1 = b2 proofend; end; :: deftheorem defines `partial3| PDIFF_4:def_6_:_ for f being PartFunc of (REAL 3),REAL for D being set st f is_partial_differentiable`3_on D holds for b3 being PartFunc of (REAL 3),REAL holds ( b3 = f `partial3| D iff ( dom b3 = D & ( for u being Element of REAL 3 st u in D holds b3 . u = partdiff (f,u,3) ) ) ); begin theorem :: PDIFF_4:25 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 for N being Neighbourhood of (proj (1,3)) . u0 st f is_partial_differentiable_in u0,1 & N c= dom (SVF1 (1,f,u0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (1,3)) . u0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c)) is convergent & partdiff (f,u0,1) = lim ((h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c))) ) proofend; theorem :: PDIFF_4:26 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 for N being Neighbourhood of (proj (2,3)) . u0 st f is_partial_differentiable_in u0,2 & N c= dom (SVF1 (2,f,u0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (2,3)) . u0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c)) is convergent & partdiff (f,u0,2) = lim ((h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c))) ) proofend; theorem :: PDIFF_4:27 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 for N being Neighbourhood of (proj (3,3)) . u0 st f is_partial_differentiable_in u0,3 & N c= dom (SVF1 (3,f,u0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (3,3)) . u0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c)) is convergent & partdiff (f,u0,3) = lim ((h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c))) ) proofend; theorem :: PDIFF_4:28 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_partial_differentiable_in u0,1 & f2 is_partial_differentiable_in u0,1 holds f1 (#) f2 is_partial_differentiable_in u0,1 proofend; theorem :: PDIFF_4:29 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_partial_differentiable_in u0,2 & f2 is_partial_differentiable_in u0,2 holds f1 (#) f2 is_partial_differentiable_in u0,2 proofend; theorem :: PDIFF_4:30 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_partial_differentiable_in u0,3 & f2 is_partial_differentiable_in u0,3 holds f1 (#) f2 is_partial_differentiable_in u0,3 proofend; theorem :: PDIFF_4:31 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 st f is_partial_differentiable_in u0,1 holds SVF1 (1,f,u0) is_continuous_in (proj (1,3)) . u0 proofend; theorem :: PDIFF_4:32 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 st f is_partial_differentiable_in u0,2 holds SVF1 (2,f,u0) is_continuous_in (proj (2,3)) . u0 proofend; theorem :: PDIFF_4:33 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 st f is_partial_differentiable_in u0,3 holds SVF1 (3,f,u0) is_continuous_in (proj (3,3)) . u0 proofend; begin Lm4: for x1, y1, z1, x2, y2, z2 being Real holds |[x1,y1,z1]| + |[x2,y2,z2]| = |[(x1 + x2),(y1 + y2),(z1 + z2)]| proofend; definition let f be PartFunc of (REAL 3),REAL; let p be Element of REAL 3; func grad (f,p) -> Element of REAL 3 equals :: PDIFF_4:def 7 (((partdiff (f,p,1)) * ) + ((partdiff (f,p,2)) * )) + ((partdiff (f,p,3)) * ); coherence (((partdiff (f,p,1)) * ) + ((partdiff (f,p,2)) * )) + ((partdiff (f,p,3)) * ) is Element of REAL 3 ; end; :: deftheorem defines grad PDIFF_4:def_7_:_ for f being PartFunc of (REAL 3),REAL for p being Element of REAL 3 holds grad (f,p) = (((partdiff (f,p,1)) * ) + ((partdiff (f,p,2)) * )) + ((partdiff (f,p,3)) * ); theorem Th34: :: PDIFF_4:34 for p being Element of REAL 3 for f being PartFunc of (REAL 3),REAL holds grad (f,p) = |[(partdiff (f,p,1)),(partdiff (f,p,2)),(partdiff (f,p,3))]| proofend; theorem Th35: :: PDIFF_4:35 for p being Element of REAL 3 for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds grad ((f + g),p) = (grad (f,p)) + (grad (g,p)) proofend; theorem Th36: :: PDIFF_4:36 for p being Element of REAL 3 for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds grad ((f - g),p) = (grad (f,p)) - (grad (g,p)) proofend; theorem Th37: :: PDIFF_4:37 for r being Real for p being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 holds grad ((r (#) f),p) = r * (grad (f,p)) proofend; theorem :: PDIFF_4:38 for s, t being Real for p being Element of REAL 3 for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds grad (((s (#) f) + (t (#) g)),p) = (s * (grad (f,p))) + (t * (grad (g,p))) proofend; theorem :: PDIFF_4:39 for s, t being Real for p being Element of REAL 3 for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds grad (((s (#) f) - (t (#) g)),p) = (s * (grad (f,p))) - (t * (grad (g,p))) proofend; theorem :: PDIFF_4:40 for p being 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 proofend; definition let a be Element of REAL 3; func unitvector a -> Element of REAL 3 equals :: PDIFF_4:def 8 |[((a . 1) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 2) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 3) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2))))]|; coherence |[((a . 1) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 2) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 3) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2))))]| is Element of REAL 3 ; end; :: deftheorem defines unitvector PDIFF_4:def_8_:_ for a being Element of REAL 3 holds unitvector a = |[((a . 1) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 2) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 3) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2))))]|; definition let f be PartFunc of (REAL 3),REAL; let p, a be Element of REAL 3; func Directiondiff (f,p,a) -> Real equals :: PDIFF_4:def 9 (((partdiff (f,p,1)) * ((unitvector a) . 1)) + ((partdiff (f,p,2)) * ((unitvector a) . 2))) + ((partdiff (f,p,3)) * ((unitvector a) . 3)); coherence (((partdiff (f,p,1)) * ((unitvector a) . 1)) + ((partdiff (f,p,2)) * ((unitvector a) . 2))) + ((partdiff (f,p,3)) * ((unitvector a) . 3)) is Real ; end; :: deftheorem defines Directiondiff PDIFF_4:def_9_:_ for f being PartFunc of (REAL 3),REAL for p, a being Element of REAL 3 holds Directiondiff (f,p,a) = (((partdiff (f,p,1)) * ((unitvector a) . 1)) + ((partdiff (f,p,2)) * ((unitvector a) . 2))) + ((partdiff (f,p,3)) * ((unitvector a) . 3)); theorem :: PDIFF_4:41 for x0, y0, z0 being Real for a, p being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st a = <*x0,y0,z0*> holds Directiondiff (f,p,a) = ((((partdiff (f,p,1)) * x0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2)))) + (((partdiff (f,p,2)) * y0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2))))) + (((partdiff (f,p,3)) * z0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2)))) proofend; theorem :: PDIFF_4:42 for p, a being Element of REAL 3 for f being PartFunc of (REAL 3),REAL holds Directiondiff (f,p,a) = |((grad (f,p)),(unitvector a))| proofend; definition let f1, f2, f3 be PartFunc of (REAL 3),REAL; let p be Element of REAL 3; func curl (f1,f2,f3,p) -> Element of REAL 3 equals :: PDIFF_4:def 10 ((((partdiff (f3,p,2)) - (partdiff (f2,p,3))) * ) + (((partdiff (f1,p,3)) - (partdiff (f3,p,1))) * )) + (((partdiff (f2,p,1)) - (partdiff (f1,p,2))) * ); coherence ((((partdiff (f3,p,2)) - (partdiff (f2,p,3))) * ) + (((partdiff (f1,p,3)) - (partdiff (f3,p,1))) * )) + (((partdiff (f2,p,1)) - (partdiff (f1,p,2))) * ) is Element of REAL 3 ; end; :: deftheorem defines curl PDIFF_4:def_10_:_ for f1, f2, f3 being PartFunc of (REAL 3),REAL for p being Element of REAL 3 holds curl (f1,f2,f3,p) = ((((partdiff (f3,p,2)) - (partdiff (f2,p,3))) * ) + (((partdiff (f1,p,3)) - (partdiff (f3,p,1))) * )) + (((partdiff (f2,p,1)) - (partdiff (f1,p,2))) * ); theorem :: PDIFF_4:43 for p being Element of REAL 3 for f1, f2, f3 being PartFunc of (REAL 3),REAL holds curl (f1,f2,f3,p) = |[((partdiff (f3,p,2)) - (partdiff (f2,p,3))),((partdiff (f1,p,3)) - (partdiff (f3,p,1))),((partdiff (f2,p,1)) - (partdiff (f1,p,2)))]| proofend;