:: Vector Function and its Differentiation Formulas in 3-dimensional :: Euclidean Spaces :: by Xiquan Liang , Piqing Zhao and Ou Bai :: :: Received October 10, 2009 :: Copyright (c) 2009-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies SUBSET_1, NUMBERS, FINSEQ_1, FINSEQ_2, PARTFUN1, REAL_1, EUCLID, FUNCT_1, RELAT_1, ARYTM_3, ARYTM_1, RVSUM_1, CARD_3, CARD_1, SQUARE_1, EUCLID_5, EUCLID_3, COMPLEX1, XXREAL_0, FDIFF_1, VALUED_1, ORDINAL4, FDIFF_3, XXREAL_1, TARSKI, EUCLID_8; notations RELAT_1, VALUED_1, FDIFF_1, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, REAL_1, FINSEQ_1, FUNCT_1, FINSEQ_2, RVSUM_1, EUCLID, XCMPLX_0, SQUARE_1, COMPLEX1, PARTFUN1, FUNCT_2, RFUNCT_1, EUCLIDLP, EUCLID_5, FDIFF_3, XXREAL_1, XXREAL_0, TARSKI; constructors FDIFF_1, REAL_1, BINOP_2, FINSEQOP, FINSEQ_4, MONOID_0, SQUARE_1, COMPLEX1, RFUNCT_1, EUCLIDLP, EUCLID_5, FDIFF_3, RCOMP_1, EUCLID_3, COMSEQ_2; registrations NUMBERS, MEMBERED, MONOID_0, EUCLID, VALUED_0, XCMPLX_0, RVSUM_1, RELAT_1, FINSEQ_1, SQUARE_1, XREAL_0, ORDINAL1; requirements SUBSET, NUMERALS, ARITHM; begin :: Preliminaries reserve r, r1, r2, x, y, z, x1, x2, x3, y1, y2, y3 for Real; reserve R, R1, R2, R3 for Element of 3-tuples_on REAL; reserve p, q, p1, p2, p3, q1, q2 for Element of REAL 3; reserve f1, f2, f3, g1, g2, g3, h1, h2, h3 for PartFunc of REAL,REAL; reserve t, t0, t1, t2 for Real; definition let x, y, z be Real; redefine func |[ x,y,z ]| -> Element of REAL 3; end; theorem :: EUCLID_8:1 p = |[ p.1, p.2, p.3 ]|; theorem :: EUCLID_8:2 for f being FinSequence of REAL st len f = 3 holds f is Element of REAL 3; definition func -> Element of REAL 3 equals :: EUCLID_8:def 1 |[ 1,0,0 ]|; func -> Element of REAL 3 equals :: EUCLID_8:def 2 |[ 0,1,0 ]|; func -> Element of REAL 3 equals :: EUCLID_8:def 3 |[ 0,0,1 ]|; end; definition let p1, p2; func p1 p2 -> Element of REAL 3 equals :: EUCLID_8:def 4 |[ (p1.2*p2.3)-(p1.3*p2.2),(p1.3*p2.1)-(p1.1*p2.3), (p1.1*p2.2)-(p1.2*p2.1) ]|; end; theorem :: EUCLID_8:3 p1,p2 are_ldependent2 implies p1p2 = 0.REAL 3; begin :: Vector Function in 3-dimensional Euclidean Spaces theorem :: EUCLID_8:4 |. .| = 1; theorem :: EUCLID_8:5 |. .| = 1; theorem :: EUCLID_8:6 |. .| = 1; theorem :: EUCLID_8:7 , are_orthogonal; theorem :: EUCLID_8:8 , are_orthogonal; theorem :: EUCLID_8:9 , are_orthogonal; theorem :: EUCLID_8:10 |(,)| = 1; theorem :: EUCLID_8:11 |(,)| = 1; theorem :: EUCLID_8:12 |(,)| = 1; theorem :: EUCLID_8:13 |( p , |[ 0,0,0 ]| )| = 0; ::$CT 2 theorem :: EUCLID_8:16 = ; theorem :: EUCLID_8:17 = ; theorem :: EUCLID_8:18 = ; theorem :: EUCLID_8:19 = -; theorem :: EUCLID_8:20 = -; theorem :: EUCLID_8:21 = -; theorem :: EUCLID_8:22 p |[ 0,0,0 ]| = |[ 0,0,0 ]|; ::$CT 2 theorem :: EUCLID_8:25 r* = |[ r,0,0 ]|; theorem :: EUCLID_8:26 r* = |[ 0,r,0 ]|; theorem :: EUCLID_8:27 r* = |[ 0,0,r ]|; theorem :: EUCLID_8:28 1*p = p; ::$CT 2 theorem :: EUCLID_8:31 - = |[ -1,0,0 ]|; theorem :: EUCLID_8:32 - = |[ 0,-1,0 ]|; theorem :: EUCLID_8:33 - = |[ 0,0,-1 ]|; theorem :: EUCLID_8:34 0 * p = |[ 0,0,0 ]|; ::$CT 2 theorem :: EUCLID_8:37 p = p.1* + p.2* + p.3*; theorem :: EUCLID_8:38 r*p = r*p.1* + r*p.2* + r*p.3*; theorem :: EUCLID_8:39 |[ x,y,z ]| = x* + y* + z*; theorem :: EUCLID_8:40 r*|[ x,y,z ]| = r*x* + r*y* + r*z*; theorem :: EUCLID_8:41 -p = - p.1* - p.2* - p.3*; theorem :: EUCLID_8:42 -|[ x,y,z ]| = -x* - y* - z*; theorem :: EUCLID_8:43 p1+p2 = (p1.1+p2.1)*+(p1.2+p2.2)*+(p1.3+p2.3)*; theorem :: EUCLID_8:44 p1-p2 = (p1.1-p2.1)*+(p1.2-p2.2)*+(p1.3-p2.3)*; theorem :: EUCLID_8:45 |[ x1,x2,x3 ]| + |[ y1,y2,y3 ]| = (x1+y1)* + (x2+y2)* + (x3+y3)*; theorem :: EUCLID_8:46 |[ x1,x2,x3 ]| - |[ y1,y2,y3 ]| = (x1-y1)* + (x2-y2)* + (x3-y3)*; theorem :: EUCLID_8:47 p1.1* + p1.2* + p1.3* = (p2.1 + p3.1)* + (p2.2 + p3.2)* + (p2.3 + p3.3)* iff p2.1* + p2.2* + p2.3* = (p1.1 - p3.1)* + (p1.2 - p3.2)* + (p1.3 - p3.3)*; definition let f1,f2,f3 be PartFunc of REAL,REAL; func VFunc(f1,f2,f3) -> Function of REAL,REAL 3 means :: EUCLID_8:def 5 for t holds it.t = |[ f1.t,f2.t,f3.t ]|; end; theorem :: EUCLID_8:48 VFunc(f1,f2,f3).t = f1.t* + f2.t* + f3.t*; theorem :: EUCLID_8:49 p = VFunc(f1,f2,f3).t iff p.1 = f1.t & p.2 = f2.t & p.3 = f3.t; theorem :: EUCLID_8:50 len p = 3 & dom p = Seg 3; theorem :: EUCLID_8:51 mlt(p,q) = <* p.1*q.1, p.2*q.2, p.3*q.3 *>; theorem :: EUCLID_8:52 r*p = |[ r*p.1, r*p.2, r*p.3 ]|; ::$CT theorem :: EUCLID_8:54 len(-p) = len p; theorem :: EUCLID_8:55 p+q = |[ p.1+q.1, p.2+q.2, p.3+q.3 ]|; theorem :: EUCLID_8:56 (p = VFunc(f1,f2,f3).t1 & q = VFunc(g1,g2,g3).t2 & p = q) implies (f1.t1 = g1.t2 & f2.t1 = g2.t2 & f3.t1 = g3.t2); theorem :: EUCLID_8:57 (f1.t1 = g1.t2 & f2.t1 = g2.t2 & f3.t1 = g3.t2) implies VFunc(f1,f2,f3).t1 = VFunc(g1,g2,g3).t2; theorem :: EUCLID_8:58 for r being Real holds r*p = |[ r*p.1, r*p.2, r*p.3 ]|; theorem :: EUCLID_8:59 for r being Real holds r*|[ x,y,z ]| = |[ r*x, r*y, r*z ]|; theorem :: EUCLID_8:60 -p = |[ -p.1,-p.2,-p.3 ]|; theorem :: EUCLID_8:61 (-p).1 = -p.1 & (-p).2 = -p.2 & (-p).3 = -p.3; theorem :: EUCLID_8:62 p1-p2 = |[ p1.1-p2.1, p1.2-p2.2, p1.3-p2.3 ]|; theorem :: EUCLID_8:63 |(p,q)| = p.1*q.1+p.2*q.2+p.3*q.3; theorem :: EUCLID_8:64 |(p,p)| = (p.1)^2 + (p.2)^2 + (p.3)^2; theorem :: EUCLID_8:65 |.p.| = sqrt ((p.1)^2+(p.2)^2+(p.3)^2); theorem :: EUCLID_8:66 |.r*p.| = |.r.|*(sqrt ((p.1)^2+(p.2)^2+(p.3)^2)); theorem :: EUCLID_8:67 r1*p+r2*p = (r1+r2)*|[ p.1, p.2, p.3 ]|; theorem :: EUCLID_8:68 |(r*p1,p2)| = r*|(p1,p2)|; theorem :: EUCLID_8:69 r1*p-r2*p = (r1-r2)*|[ p.1, p.2, p.3 ]|; theorem :: EUCLID_8:70 |(r*p,q)| = r*(p.1*q.1+p.2*q.2+p.3*q.3); theorem :: EUCLID_8:71 |(p,0.REAL 3)| = 0; theorem :: EUCLID_8:72 |(-p1,p2)| = -|(p1,p2)|; theorem :: EUCLID_8:73 |(-p1,-p2)| = |(p1,p2)|; theorem :: EUCLID_8:74 |(p1-p2,q)| = |(p1,q)| - |(p2,q)|; theorem :: EUCLID_8:75 |(p1+p2,q)| = |(p1,q)|+|(p2,q)|; theorem :: EUCLID_8:76 |(r1*p1+r2*p2,q)| = r1*|(p1,q)| + r2*|(p2,q)|; theorem :: EUCLID_8:77 |(p1+p2,q1+q2)| = |(p1,q1)|+|(p1,q2)|+|(p2,q1)|+|(p2,q2)|; theorem :: EUCLID_8:78 |(p1-p2,q1-q2)| = |(p1,q1)|-|(p1,q2)|-|(p2,q1)|+|(p2,q2)|; theorem :: EUCLID_8:79 |(p,p)| = 0 iff p = 0.REAL 3; theorem :: EUCLID_8:80 |.p.| = 0 iff p = 0.REAL 3; theorem :: EUCLID_8:81 |(p-q,p-q)| = |(p,p)|-2*|(p,q)|+|(q,q)|; theorem :: EUCLID_8:82 |(p+q,p+q)| = |(p,p)|+2*|(p,q)|+|(q,q)|; theorem :: EUCLID_8:83 p1p2 = -p2p1; theorem :: EUCLID_8:84 |[ x1,x2,x3 ]| |[ y1,y2,y3 ]| = |[ (x2*y3)-(x3*y2),(x3*y1)-(x1*y3),(x1*y2)-(x2*y1) ]|; theorem :: EUCLID_8:85 (r*p1)p2 = r*(p1p2) & (r*p1)p2 = p1(r*p2); theorem :: EUCLID_8:86 p1(p2+p3) = (p1p2)+(p1p3); theorem :: EUCLID_8:87 (p1+p2)p3 = (p1p3)+(p2p3); theorem :: EUCLID_8:88 (p1+p2)(q1+q2) = p1q1+p1q2+p2q1+p2q2; theorem :: EUCLID_8:89 p1(p2p3) = (|(p1,p3)|*p2)-(|(p1,p2)|*p3); definition let p1,p2,p3; func |{ p1,p2,p3 }| -> Real equals :: EUCLID_8:def 6 |(p1,p2p3)|; end; theorem :: EUCLID_8:90 |{ p1,p1,p2 }| = 0; theorem :: EUCLID_8:91 |{ p2,p1,p2 }| = 0; theorem :: EUCLID_8:92 |{ p1,p2,p2 }| = 0; theorem :: EUCLID_8:93 |{ p1,p2,p3 }| = |{ p2,p3,p1 }|; theorem :: EUCLID_8:94 |{ p1,p2,p3 }| = |(p1p2,p3)|; theorem :: EUCLID_8:95 |{ p1,p2,q }| = |(qp1,p2)|; begin :: the Differentiation Formulas of Vector Function in 3-dimensional Euclidean Spaces definition let f1,f2,f3 be PartFunc of REAL,REAL; let t0 be Real; func VFuncdiff(f1,f2,f3,t0) -> Element of REAL 3 equals :: EUCLID_8:def 7 |[ diff(f1,t0),diff(f2,t0),diff(f3,t0) ]|; end; theorem :: EUCLID_8:96 f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 implies VFuncdiff(f1,f2,f3,t0) = diff(f1,t0)*+diff(f2,t0)*+diff(f3,t0)*; theorem :: EUCLID_8:97 (f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0) & (g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0) implies VFuncdiff(f1+g1,f2+g2,f3+g3,t0) = VFuncdiff(f1,f2,f3,t0)+VFuncdiff(g1,g2,g3,t0); theorem :: EUCLID_8:98 (f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0) & (g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0) implies VFuncdiff(f1-g1,f2-g2,f3-g3,t0) = VFuncdiff(f1,f2,f3,t0)-VFuncdiff(g1,g2,g3,t0); theorem :: EUCLID_8:99 (f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0) implies VFuncdiff(r(#)f1,r(#)f2,r(#)f3,t0) = r*VFuncdiff(f1,f2,f3,t0); theorem :: EUCLID_8:100 (f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0) & (g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0) implies VFuncdiff(f1(#)g1,f2(#)g2,f3(#)g3,t0) = |[ (g1.t0)*diff(f1,t0),(g2.t0)*diff(f2,t0),(g3.t0)*diff(f3,t0) ]|+ |[ (f1.t0)*diff(g1,t0),(f2.t0)*diff(g2,t0),(f3.t0)*diff(g3,t0) ]|; theorem :: EUCLID_8:101 (f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0) & (g1 is_differentiable_in f1.t0 & g2 is_differentiable_in f2.t0 & g3 is_differentiable_in f3.t0) implies VFuncdiff(g1*f1,g2*f2,g3*f3,t0) = |[ diff(g1,f1.t0)*diff(f1,t0),diff(g2,f2.t0)*diff(f2,t0), diff(g3,f3.t0)*diff(f3,t0) ]|; theorem :: EUCLID_8:102 (f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0) & (g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0) & (g1.t0 <> 0 & g2.t0 <> 0 & g3.t0 <> 0) implies VFuncdiff(f1/g1,f2/g2,f3/g3,t0) = |[ (diff(f1,t0)*(g1.t0)-diff(g1,t0)*(f1.t0))/(g1.t0)^2, (diff(f2,t0)*(g2.t0)-diff(g2,t0)*(f2.t0))/(g2.t0)^2, (diff(f3,t0)*(g3.t0)-diff(g3,t0)*(f3.t0))/(g3.t0)^2 ]|; theorem :: EUCLID_8:103 (f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0) & (f1.t0 <> 0 & f2.t0 <> 0 & f3.t0 <> 0) implies VFuncdiff(f1^,f2^,f3^,t0) = - |[ diff(f1,t0)/(f1.t0)^2,diff(f2,t0)/(f2.t0)^2, diff(f3,t0)/(f3.t0)^2 ]|; theorem :: EUCLID_8:104 f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 implies VFuncdiff(r(#)f1,r(#)f2,r(#)f3,t0) = r*diff(f1,t0)* +r*diff(f2,t0)*+r*diff(f3,t0)*; theorem :: EUCLID_8:105 (f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0) & (g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0) implies VFuncdiff(r(#)(f1+g1),r(#)(f2+g2),r(#)(f3+g3),t0) = r*VFuncdiff(f1,f2,f3,t0)+r*VFuncdiff(g1,g2,g3,t0); theorem :: EUCLID_8:106 (f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0) & (g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0) implies VFuncdiff(r(#)(f1-g1),r(#)(f2-g2),r(#)(f3-g3),t0) = r*VFuncdiff(f1,f2,f3,t0)-r*VFuncdiff(g1,g2,g3,t0); theorem :: EUCLID_8:107 (f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0) & (g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0) implies VFuncdiff(r(#)f1(#)g1,r(#)f2(#)g2,r(#)f3(#)g3,t0) = r*|[ (g1.t0)*diff(f1,t0),(g2.t0)*diff(f2,t0),(g3.t0)*diff(f3,t0) ]|+ r*|[ (f1.t0)*diff(g1,t0),(f2.t0)*diff(g2,t0),(f3.t0)*diff(g3,t0) ]|; theorem :: EUCLID_8:108 (f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0) & (g1 is_differentiable_in f1.t0 & g2 is_differentiable_in f2.t0 & g3 is_differentiable_in f3.t0) implies VFuncdiff(r(#)g1*f1,r(#)g2*f2,r(#)g3*f3,t0) = r*|[ diff(g1,f1.t0)*diff(f1,t0),diff(g2,f2.t0)*diff(f2,t0), diff(g3,f3.t0)*diff(f3,t0) ]|; theorem :: EUCLID_8:109 (f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0) & (g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0) & (g1.t0 <> 0 & g2.t0 <> 0 & g3.t0 <> 0) implies VFuncdiff(r(#)f1/g1,r(#)f2/g2,r(#)f3/g3,t0) = r*|[ (diff(f1,t0)*(g1.t0)-diff(g1,t0)*(f1.t0))/(g1.t0)^2, (diff(f2,t0)*(g2.t0)-diff(g2,t0)*(f2.t0))/(g2.t0)^2, (diff(f3,t0)*(g3.t0)-diff(g3,t0)*(f3.t0))/(g3.t0)^2 ]|; theorem :: EUCLID_8:110 (f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0) & (f1.t0 <> 0 & f2.t0 <> 0 & f3.t0 <> 0) & r <> 0 implies VFuncdiff(r(#)f1^,r(#)f2^,r(#)f3^,t0) = - 1/r*|[ diff(f1,t0)/(f1.t0)^2,diff(f2,t0)/(f2.t0)^2, diff(f3,t0)/(f3.t0)^2 ]|; theorem :: EUCLID_8:111 (f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0) & (g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0) implies VFuncdiff( f2(#)g3-f3(#)g2,f3(#)g1-f1(#)g3, f1(#)g2-f2(#)g1,t0 ) = |[ (f2.t0)*diff(g3,t0)-(f3.t0)*diff(g2,t0), (f3.t0)*diff(g1,t0)-(f1.t0)*diff(g3,t0), (f1.t0)*diff(g2,t0)-(f2.t0)*diff(g1,t0) ]| + |[ diff(f2,t0)*(g3.t0)-diff(f3,t0)*(g2.t0), diff(f3,t0)*(g1.t0)-diff(f1,t0)*(g3.t0), diff(f1,t0)*(g2.t0)-diff(f2,t0)*(g1.t0) ]|; ::p37-4(5.1) A*(BXC) theorem :: EUCLID_8:112 (f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0) & (g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0) & (h1 is_differentiable_in t0 & h2 is_differentiable_in t0 & h3 is_differentiable_in t0) implies VFuncdiff( h1(#)(f2(#)g3-f3(#)g2), h2(#)(f3(#)g1-f1(#)g3), h3(#)(f1(#)g2-f2(#)g1),t0 ) = |[ diff(h1,t0)*(f2.t0*g3.t0-f3.t0*g2.t0), diff(h2,t0)*(f3.t0*g1.t0-f1.t0*g3.t0), diff(h3,t0)*(f1.t0*g2.t0-f2.t0*g1.t0) ]|+ |[ (h1.t0)*(diff(f2,t0)*(g3.t0)-diff(f3,t0)*(g2.t0)), (h2.t0)*(diff(f3,t0)*(g1.t0)-diff(f1,t0)*(g3.t0)), (h3.t0)*(diff(f1,t0)*(g2.t0)-diff(f2,t0)*(g1.t0)) ]|+ |[ (h1.t0)*((f2.t0)*diff(g3,t0)-(f3.t0)*diff(g2,t0)), (h2.t0)*((f3.t0)*diff(g1,t0)-(f1.t0)*diff(g3,t0)), (h3.t0)*((f1.t0)*diff(g2,t0)-(f2.t0)*diff(g1,t0)) ]|; ::p37-4(5.2) A*BXC theorem :: EUCLID_8:113 (f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0) & (g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0) & (h1 is_differentiable_in t0 & h2 is_differentiable_in t0 & h3 is_differentiable_in t0) implies VFuncdiff( h2(#)f2(#)g3-h3(#)f3(#)g2, h3(#)f3(#)g1-h1(#)f1(#)g3, h1(#)f1(#)g2-h2(#)f2(#)g1,t0 ) = |[ (h2.t0)*(f2.t0)*diff(g3,t0)-(h3.t0)*(f3.t0)*diff(g2,t0), (h3.t0)*(f3.t0)*diff(g1,t0)-(h1.t0)*(f1.t0)*diff(g3,t0), (h1.t0)*(f1.t0)*diff(g2,t0)-(h2.t0)*(f2.t0)*diff(g1,t0) ]|+ |[ (h2.t0)*diff(f2,t0)*(g3.t0)-(h3.t0)*diff(f3,t0)*(g2.t0), (h3.t0)*diff(f3,t0)*(g1.t0)-(h1.t0)*diff(f1,t0)*(g3.t0), (h1.t0)*diff(f1,t0)*(g2.t0)-(h2.t0)*diff(f2,t0)*(g1.t0) ]|+ |[ diff(h2,t0)*(f2.t0)*(g3.t0)-diff(h3,t0)*(f3.t0)*(g2.t0), diff(h3,t0)*(f3.t0)*(g1.t0)-diff(h1,t0)*(f1.t0)*(g3.t0), diff(h1,t0)*(f1.t0)*(g2.t0)-diff(h2,t0)*(f2.t0)*(g1.t0) ]|; ::p37-4(6) AX(BXC) theorem :: EUCLID_8:114 (f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0) & (g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0) & (h1 is_differentiable_in t0 & h2 is_differentiable_in t0 & h3 is_differentiable_in t0) implies VFuncdiff( h2(#)(f1(#)g2-f2(#)g1)-h3(#)(f3(#)g1-f1(#)g3), h3(#)(f2(#)g3-f3(#)g2)-h1(#)(f1(#)g2-f2(#)g1), h1(#)(f3(#)g1-f1(#)g3)-h2(#)(f2(#)g3-f3(#)g2),t0 ) = |[ (h2.t0)*((f1.t0)*diff(g2,t0)-(f2.t0)*diff(g1,t0))- (h3.t0)*((f3.t0)*diff(g1,t0)-(f1.t0)*diff(g3,t0)), (h3.t0)*((f2.t0)*diff(g3,t0)-(f3.t0)*diff(g2,t0))- (h1.t0)*((f1.t0)*diff(g2,t0)-(f2.t0)*diff(g1,t0)), (h1.t0)*((f3.t0)*diff(g1,t0)-(f1.t0)*diff(g3,t0))- (h2.t0)*((f2.t0)*diff(g3,t0)-(f3.t0)*diff(g2,t0)) ]|+ |[ (h2.t0)*(diff(f1,t0)*(g2.t0)-diff(f2,t0)*(g1.t0))- (h3.t0)*(diff(f3,t0)*(g1.t0)-diff(f1,t0)*(g3.t0)), (h3.t0)*(diff(f2,t0)*(g3.t0)-diff(f3,t0)*(g2.t0))- (h1.t0)*(diff(f1,t0)*(g2.t0)-diff(f2,t0)*(g1.t0)), (h1.t0)*(diff(f3,t0)*(g1.t0)-diff(f1,t0)*(g3.t0))- (h2.t0)*(diff(f2,t0)*(g3.t0)-diff(f3,t0)*(g2.t0)) ]|+ |[ diff(h2,t0)*((f1.t0)*(g2.t0)-(f2.t0)*(g1.t0))- diff(h3,t0)*((f3.t0)*(g1.t0)-(f1.t0)*(g3.t0)), diff(h3,t0)*((f2.t0)*(g3.t0)-(f3.t0)*(g2.t0))- diff(h1,t0)*((f1.t0)*(g2.t0)-(f2.t0)*(g1.t0)), diff(h1,t0)*((f3.t0)*(g1.t0)-(f1.t0)*(g3.t0))- diff(h2,t0)*((f2.t0)*(g3.t0)-(f3.t0)*(g2.t0)) ]|;