:: 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-2012 Association of Mizar Users begin definition let x, y, z be real number ; :: original:<* redefine func|[x,y,z]| -> Element of REAL 3; coherence <*x,y,z*> is Element of REAL 3 proofend; end; theorem Th1: :: EUCLID_8:1 for p being Element of REAL 3 holds p = |[(p . 1),(p . 2),(p . 3)]| proofend; Lm1: for p being Element of REAL 3 for r being real number holds r * p = |[(r * (p . 1)),(r * (p . 2)),(r * (p . 3))]| proofend; Lm2: for p1, p2 being Element of REAL 3 holds p1 + p2 = |[((p1 . 1) + (p2 . 1)),((p1 . 2) + (p2 . 2)),((p1 . 3) + (p2 . 3))]| proofend; Lm3: for p being Element of REAL 3 holds ( (- p) . 1 = - (p . 1) & (- p) . 2 = - (p . 2) & (- p) . 3 = - (p . 3) ) proofend; theorem :: EUCLID_8:2 for f being FinSequence of REAL st len f = 3 holds f is Element of REAL 3 proofend; Lm4: for p1, p2 being Element of REAL 3 holds p1 - p2 = |[((p1 . 1) - (p2 . 1)),((p1 . 2) - (p2 . 2)),((p1 . 3) - (p2 . 3))]| proofend; Lm5: for p1, p2 being Element of REAL 3 holds |(p1,p2)| = (((p1 . 1) * (p2 . 1)) + ((p1 . 2) * (p2 . 2))) + ((p1 . 3) * (p2 . 3)) proofend; Lm6: for r, x, y, z being Element of REAL holds r * |[x,y,z]| = |[(r * x),(r * y),(r * z)]| proofend; Lm7: for p1, p2 being Element of REAL 3 holds p1 + (- p2) = |[((p1 . 1) - (p2 . 1)),((p1 . 2) - (p2 . 2)),((p1 . 3) - (p2 . 3))]| proofend; Lm8: for x1, x2, x3, y1, y2, y3 being Element of REAL holds |[x1,x2,x3]| + |[y1,y2,y3]| = |[(x1 + y1),(x2 + y2),(x3 + y3)]| proofend; Lm9: for p1, p2, q1, q2 being Element of REAL 3 holds (p1 + p2) + (q1 + q2) = (p1 + q1) + (p2 + q2) proofend; Lm10: for p1, p2, q1, q2 being Element of REAL 3 holds (p1 + p2) - (q1 + q2) = (p1 - q1) + (p2 - q2) proofend; Lm11: for x1, x2, x3, y1, y2, y3 being Element of REAL holds |[x1,x2,x3]| - |[y1,y2,y3]| = |[(x1 - y1),(x2 - y2),(x3 - y3)]| proofend; definition func -> Element of REAL 3 equals :: EUCLID_8:def 1 |[1,0,0]|; coherence |[1,0,0]| is Element of REAL 3 ; func -> Element of REAL 3 equals :: EUCLID_8:def 2 |[0,1,0]|; coherence |[0,1,0]| is Element of REAL 3 ; func -> Element of REAL 3 equals :: EUCLID_8:def 3 |[0,0,1]|; coherence |[0,0,1]| is Element of REAL 3 ; end; :: deftheorem defines EUCLID_8:def_1_:_ = |[1,0,0]|; :: deftheorem defines EUCLID_8:def_2_:_ = |[0,1,0]|; :: deftheorem defines EUCLID_8:def_3_:_ = |[0,0,1]|; Lm12: for x, y, z being Element of REAL for p being Element of REAL 3 st p = |[x,y,z]| holds |(p,p)| = ((x ^2) + (y ^2)) + (z ^2) proofend; definition let p1, p2 be Element of REAL 3; funcp1 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)))]|; correctness coherence |[(((p1 . 2) * (p2 . 3)) - ((p1 . 3) * (p2 . 2))),(((p1 . 3) * (p2 . 1)) - ((p1 . 1) * (p2 . 3))),(((p1 . 1) * (p2 . 2)) - ((p1 . 2) * (p2 . 1)))]| is Element of REAL 3; ; end; :: deftheorem defines EUCLID_8:def_4_:_ for p1, p2 being Element of REAL 3 holds p1 p2 = |[(((p1 . 2) * (p2 . 3)) - ((p1 . 3) * (p2 . 2))),(((p1 . 3) * (p2 . 1)) - ((p1 . 1) * (p2 . 3))),(((p1 . 1) * (p2 . 2)) - ((p1 . 2) * (p2 . 1)))]|; Lm13: for x1, x2, x3, y1, y2, y3 being Element of REAL holds |[x1,x2,x3]| |[y1,y2,y3]| = |[((x2 * y3) - (x3 * y2)),((x3 * y1) - (x1 * y3)),((x1 * y2) - (x2 * y1))]| proofend; Lm14: for r being Element of REAL for p1, p2 being Element of REAL 3 holds ( (r * p1) p2 = r * (p1 p2) & (r * p1) p2 = p1 (r * p2) ) proofend; theorem :: EUCLID_8:3 for p1, p2 being Element of REAL 3 st p1,p2 are_ldependent2 holds p1 p2 = 0.REAL 3 proofend; begin theorem :: EUCLID_8:4 |..| = 1 proofend; theorem :: EUCLID_8:5 |..| = 1 proofend; theorem :: EUCLID_8:6 |..| = 1 proofend; theorem :: EUCLID_8:7 , are_orthogonal proofend; theorem :: EUCLID_8:8 , are_orthogonal proofend; theorem :: EUCLID_8:9 , are_orthogonal proofend; theorem :: EUCLID_8:10 |(,)| = 1 proofend; theorem :: EUCLID_8:11 |(,)| = 1 proofend; theorem :: EUCLID_8:12 |(,)| = 1 proofend; theorem Th13: :: EUCLID_8:13 for p being Element of REAL 3 holds |(p,|[0,0,0]|)| = 0 proofend; theorem :: EUCLID_8:14 canceled; theorem :: EUCLID_8:15 canceled; theorem :: EUCLID_8:16 = proofend; theorem :: EUCLID_8:17 = proofend; theorem :: EUCLID_8:18 = proofend; theorem :: EUCLID_8:19 = - proofend; theorem :: EUCLID_8:20 = - proofend; theorem :: EUCLID_8:21 = - proofend; theorem :: EUCLID_8:22 for p being Element of REAL 3 holds p |[0,0,0]| = |[0,0,0]| proofend; theorem :: EUCLID_8:23 canceled; theorem :: EUCLID_8:24 canceled; theorem Th25: :: EUCLID_8:25 for r being Element of REAL holds r * = |[r,0,0]| proofend; theorem Th26: :: EUCLID_8:26 for r being Element of REAL holds r * = |[0,r,0]| proofend; theorem Th27: :: EUCLID_8:27 for r being Element of REAL holds r * = |[0,0,r]| proofend; theorem :: EUCLID_8:28 for p being Element of REAL 3 holds 1 * p = p by RFUNCT_1:21; theorem :: EUCLID_8:29 canceled; theorem :: EUCLID_8:30 canceled; theorem :: EUCLID_8:31 - = |[(- 1),0,0]| proofend; theorem :: EUCLID_8:32 - = |[0,(- 1),0]| proofend; theorem :: EUCLID_8:33 - = |[0,0,(- 1)]| proofend; theorem :: EUCLID_8:34 for p being Element of REAL 3 holds 0 * p = |[0,0,0]| proofend; theorem :: EUCLID_8:35 canceled; theorem :: EUCLID_8:36 canceled; theorem :: EUCLID_8:37 for p being Element of REAL 3 holds p = (((p . 1) * ) + ((p . 2) * )) + ((p . 3) * ) proofend; theorem Th38: :: EUCLID_8:38 for r being Element of REAL for p being Element of REAL 3 holds r * p = (((r * (p . 1)) * ) + ((r * (p . 2)) * )) + ((r * (p . 3)) * ) proofend; theorem Th39: :: EUCLID_8:39 for x, y, z being Element of REAL holds |[x,y,z]| = ((x * ) + (y * )) + (z * ) proofend; theorem Th40: :: EUCLID_8:40 for r, x, y, z being Element of REAL holds r * |[x,y,z]| = (((r * x) * ) + ((r * y) * )) + ((r * z) * ) proofend; theorem :: EUCLID_8:41 for p being Element of REAL 3 holds - p = ((- ((p . 1) * )) - ((p . 2) * )) - ((p . 3) * ) proofend; theorem :: EUCLID_8:42 for x, y, z being Element of REAL holds - |[x,y,z]| = ((- (x * )) - (y * )) - (z * ) proofend; theorem :: EUCLID_8:43 for p1, p2 being Element of REAL 3 holds p1 + p2 = ((((p1 . 1) + (p2 . 1)) * ) + (((p1 . 2) + (p2 . 2)) * )) + (((p1 . 3) + (p2 . 3)) * ) proofend; theorem Th44: :: EUCLID_8:44 for p1, p2 being Element of REAL 3 holds p1 - p2 = ((((p1 . 1) - (p2 . 1)) * ) + (((p1 . 2) - (p2 . 2)) * )) + (((p1 . 3) - (p2 . 3)) * ) proofend; theorem :: EUCLID_8:45 for x1, x2, x3, y1, y2, y3 being Element of REAL holds |[x1,x2,x3]| + |[y1,y2,y3]| = (((x1 + y1) * ) + ((x2 + y2) * )) + ((x3 + y3) * ) proofend; theorem :: EUCLID_8:46 for x1, x2, x3, y1, y2, y3 being Element of REAL holds |[x1,x2,x3]| - |[y1,y2,y3]| = (((x1 - y1) * ) + ((x2 - y2) * )) + ((x3 - y3) * ) proofend; theorem :: EUCLID_8:47 for p1, p2, p3 being Element of REAL 3 holds ( (((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)) * ) ) proofend; definition let f1, f2, f3 be PartFunc of REAL,REAL; func VFunc (f1,f2,f3) -> Function of REAL,(REAL 3) means :Def5: :: EUCLID_8:def 5 for t being Real holds it . t = |[(f1 . t),(f2 . t),(f3 . t)]|; existence ex b1 being Function of REAL,(REAL 3) st for t being Real holds b1 . t = |[(f1 . t),(f2 . t),(f3 . t)]| proofend; uniqueness for b1, b2 being Function of REAL,(REAL 3) st ( for t being Real holds b1 . t = |[(f1 . t),(f2 . t),(f3 . t)]| ) & ( for t being Real holds b2 . t = |[(f1 . t),(f2 . t),(f3 . t)]| ) holds b1 = b2 proofend; end; :: deftheorem Def5 defines VFunc EUCLID_8:def_5_:_ for f1, f2, f3 being PartFunc of REAL,REAL for b4 being Function of REAL,(REAL 3) holds ( b4 = VFunc (f1,f2,f3) iff for t being Real holds b4 . t = |[(f1 . t),(f2 . t),(f3 . t)]| ); theorem :: EUCLID_8:48 for f1, f2, f3 being PartFunc of REAL,REAL for t being Real holds (VFunc (f1,f2,f3)) . t = (((f1 . t) * ) + ((f2 . t) * )) + ((f3 . t) * ) proofend; theorem Th49: :: EUCLID_8:49 for p being Element of REAL 3 for f1, f2, f3 being PartFunc of REAL,REAL for t being Real holds ( p = (VFunc (f1,f2,f3)) . t iff ( p . 1 = f1 . t & p . 2 = f2 . t & p . 3 = f3 . t ) ) proofend; theorem Th50: :: EUCLID_8:50 for p being Element of REAL 3 holds ( len p = 3 & dom p = Seg 3 ) proofend; theorem Th51: :: EUCLID_8:51 for p, q being Element of REAL 3 holds mlt (p,q) = <*((p . 1) * (q . 1)),((p . 2) * (q . 2)),((p . 3) * (q . 3))*> proofend; theorem :: EUCLID_8:52 for r being Element of REAL for p being Element of REAL 3 holds r * p = |[(r * (p . 1)),(r * (p . 2)),(r * (p . 3))]| by Lm1; theorem :: EUCLID_8:53 for p being Element of REAL 3 holds - p = |[(- (p . 1)),(- (p . 2)),(- (p . 3))]| proofend; theorem :: EUCLID_8:54 for p being Element of REAL 3 holds len (- p) = len p proofend; theorem :: EUCLID_8:55 for p, q being Element of REAL 3 holds p + q = |[((p . 1) + (q . 1)),((p . 2) + (q . 2)),((p . 3) + (q . 3))]| by Lm2; theorem :: EUCLID_8:56 for p, q being Element of REAL 3 for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL for t1, t2 being Real st p = (VFunc (f1,f2,f3)) . t1 & q = (VFunc (g1,g2,g3)) . t2 & p = q holds ( f1 . t1 = g1 . t2 & f2 . t1 = g2 . t2 & f3 . t1 = g3 . t2 ) proofend; theorem :: EUCLID_8:57 for f1, g1, f2, g2, f3, g3 being PartFunc of REAL,REAL for t1, t2 being Real st f1 . t1 = g1 . t2 & f2 . t1 = g2 . t2 & f3 . t1 = g3 . t2 holds (VFunc (f1,f2,f3)) . t1 = (VFunc (g1,g2,g3)) . t2 proofend; theorem Th58: :: EUCLID_8:58 for p being Element of REAL 3 for r being real number holds r * p = |[(r * (p . 1)),(r * (p . 2)),(r * (p . 3))]| proofend; theorem Th59: :: EUCLID_8:59 for x, y, z being Element of REAL for r being real number holds r * |[x,y,z]| = |[(r * x),(r * y),(r * z)]| proofend; theorem Th60: :: EUCLID_8:60 for p being Element of REAL 3 holds - p = |[(- (p . 1)),(- (p . 2)),(- (p . 3))]| proofend; theorem Th61: :: EUCLID_8:61 for p being Element of REAL 3 holds ( (- p) . 1 = - (p . 1) & (- p) . 2 = - (p . 2) & (- p) . 3 = - (p . 3) ) proofend; theorem :: EUCLID_8:62 for p1, p2 being Element of REAL 3 holds p1 - p2 = |[((p1 . 1) - (p2 . 1)),((p1 . 2) - (p2 . 2)),((p1 . 3) - (p2 . 3))]| proofend; theorem :: EUCLID_8:63 for p, q being Element of REAL 3 holds |(p,q)| = (((p . 1) * (q . 1)) + ((p . 2) * (q . 2))) + ((p . 3) * (q . 3)) by Lm5; theorem Th64: :: EUCLID_8:64 for p being Element of REAL 3 holds |(p,p)| = (((p . 1) ^2) + ((p . 2) ^2)) + ((p . 3) ^2) proofend; theorem Th65: :: EUCLID_8:65 for p being Element of REAL 3 holds |.p.| = sqrt ((((p . 1) ^2) + ((p . 2) ^2)) + ((p . 3) ^2)) proofend; theorem :: EUCLID_8:66 for r being Element of REAL for p being Element of REAL 3 holds |.(r * p).| = (abs r) * (sqrt ((((p . 1) ^2) + ((p . 2) ^2)) + ((p . 3) ^2))) proofend; theorem :: EUCLID_8:67 for r1, r2 being Element of REAL for p being Element of REAL 3 holds (r1 * p) + (r2 * p) = (r1 + r2) * |[(p . 1),(p . 2),(p . 3)]| proofend; theorem :: EUCLID_8:68 for r being Element of REAL for p1, p2 being Element of REAL 3 holds |((r * p1),p2)| = r * |(p1,p2)| by RVSUM_1:131; theorem :: EUCLID_8:69 for r1, r2 being Element of REAL for p being Element of REAL 3 holds (r1 * p) - (r2 * p) = (r1 - r2) * |[(p . 1),(p . 2),(p . 3)]| proofend; theorem :: EUCLID_8:70 for r being Element of REAL for p, q being Element of REAL 3 holds |((r * p),q)| = r * ((((p . 1) * (q . 1)) + ((p . 2) * (q . 2))) + ((p . 3) * (q . 3))) proofend; theorem :: EUCLID_8:71 for p being Element of REAL 3 holds |(p,(0.REAL 3))| = 0 proofend; theorem :: EUCLID_8:72 for p1, p2 being Element of REAL 3 holds |((- p1),p2)| = - |(p1,p2)| by RVSUM_1:132; theorem :: EUCLID_8:73 for p1, p2 being Element of REAL 3 holds |((- p1),(- p2))| = |(p1,p2)| by RVSUM_1:133; theorem :: EUCLID_8:74 for p1, p2, q being Element of REAL 3 holds |((p1 - p2),q)| = |(p1,q)| - |(p2,q)| by RVSUM_1:134; theorem :: EUCLID_8:75 for p1, p2, q being Element of REAL 3 holds |((p1 + p2),q)| = |(p1,q)| + |(p2,q)| by RVSUM_1:130; theorem :: EUCLID_8:76 for r1, r2 being Element of REAL for p1, p2, q being Element of REAL 3 holds |(((r1 * p1) + (r2 * p2)),q)| = (r1 * |(p1,q)|) + (r2 * |(p2,q)|) by RVSUM_1:135; theorem :: EUCLID_8:77 for p1, p2, q1, q2 being Element of REAL 3 holds |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)| by RVSUM_1:136; theorem :: EUCLID_8:78 for p1, p2, q1, q2 being Element of REAL 3 holds |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)| by RVSUM_1:137; theorem Th79: :: EUCLID_8:79 for p being Element of REAL 3 holds ( |(p,p)| = 0 iff p = 0.REAL 3 ) proofend; theorem :: EUCLID_8:80 for p being Element of REAL 3 holds ( |.p.| = 0 iff p = 0.REAL 3 ) proofend; theorem :: EUCLID_8:81 for p, q being Element of REAL 3 holds |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| by RVSUM_1:139; theorem :: EUCLID_8:82 for p, q being Element of REAL 3 holds |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)| by RVSUM_1:138; theorem Th83: :: EUCLID_8:83 for p1, p2 being Element of REAL 3 holds p1 p2 = - (p2 p1) proofend; theorem Th84: :: EUCLID_8:84 for x1, x2, x3, y1, y2, y3 being Element of REAL holds |[x1,x2,x3]| |[y1,y2,y3]| = |[((x2 * y3) - (x3 * y2)),((x3 * y1) - (x1 * y3)),((x1 * y2) - (x2 * y1))]| proofend; theorem :: EUCLID_8:85 for r being Element of REAL for p1, p2 being Element of REAL 3 holds ( (r * p1) p2 = r * (p1 p2) & (r * p1) p2 = p1 (r * p2) ) proofend; theorem Th86: :: EUCLID_8:86 for p1, p2, p3 being Element of REAL 3 holds p1 (p2 + p3) = (p1 p2) + (p1 p3) proofend; theorem Th87: :: EUCLID_8:87 for p1, p2, p3 being Element of REAL 3 holds (p1 + p2) p3 = (p1 p3) + (p2 p3) proofend; theorem :: EUCLID_8:88 for p1, p2, q1, q2 being Element of REAL 3 holds (p1 + p2) (q1 + q2) = (((p1 q1) + (p1 q2)) + (p2 q1)) + (p2 q2) proofend; theorem :: EUCLID_8:89 for p1, p2, p3 being Element of REAL 3 holds p1 (p2 p3) = (|(p1,p3)| * p2) - (|(p1,p2)| * p3) proofend; definition let p1, p2, p3 be Element of REAL 3; func|{p1,p2,p3}| -> real number equals :: EUCLID_8:def 6 |(p1,(p2 p3))|; coherence |(p1,(p2 p3))| is real number ; end; :: deftheorem defines |{ EUCLID_8:def_6_:_ for p1, p2, p3 being Element of REAL 3 holds |{p1,p2,p3}| = |(p1,(p2 p3))|; theorem :: EUCLID_8:90 for p1, p2 being Element of REAL 3 holds |{p1,p1,p2}| = 0 proofend; theorem :: EUCLID_8:91 for p2, p1 being Element of REAL 3 holds |{p2,p1,p2}| = 0 proofend; theorem :: EUCLID_8:92 for p1, p2 being Element of REAL 3 holds |{p1,p2,p2}| = 0 proofend; theorem Th93: :: EUCLID_8:93 for p1, p2, p3 being Element of REAL 3 holds |{p1,p2,p3}| = |{p2,p3,p1}| proofend; theorem :: EUCLID_8:94 for p1, p2, p3 being Element of REAL 3 holds |{p1,p2,p3}| = |((p1 p2),p3)| proofend; theorem :: EUCLID_8:95 for p1, p2, q being Element of REAL 3 holds |{p1,p2,q}| = |((q p1),p2)| proofend; begin 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))]|; coherence |[(diff (f1,t0)),(diff (f2,t0)),(diff (f3,t0))]| is Element of REAL 3 ; end; :: deftheorem defines VFuncdiff EUCLID_8:def_7_:_ for f1, f2, f3 being PartFunc of REAL,REAL for t0 being Real holds VFuncdiff (f1,f2,f3,t0) = |[(diff (f1,t0)),(diff (f2,t0)),(diff (f3,t0))]|; theorem :: EUCLID_8:96 for f1, f2, f3 being PartFunc of REAL,REAL for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 holds VFuncdiff (f1,f2,f3,t0) = (((diff (f1,t0)) * ) + ((diff (f2,t0)) * )) + ((diff (f3,t0)) * ) by Th39; theorem Th97: :: EUCLID_8:97 for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL for t0 being Real st 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 holds VFuncdiff ((f1 + g1),(f2 + g2),(f3 + g3),t0) = (VFuncdiff (f1,f2,f3,t0)) + (VFuncdiff (g1,g2,g3,t0)) proofend; theorem Th98: :: EUCLID_8:98 for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL for t0 being Real st 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 holds VFuncdiff ((f1 - g1),(f2 - g2),(f3 - g3),t0) = (VFuncdiff (f1,f2,f3,t0)) - (VFuncdiff (g1,g2,g3,t0)) proofend; theorem Th99: :: EUCLID_8:99 for r being Element of REAL for f1, f2, f3 being PartFunc of REAL,REAL for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 holds VFuncdiff ((r (#) f1),(r (#) f2),(r (#) f3),t0) = r * (VFuncdiff (f1,f2,f3,t0)) proofend; theorem Th100: :: EUCLID_8:100 for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL for t0 being Real st 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 holds 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)))]| proofend; theorem Th101: :: EUCLID_8:101 for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL for t0 being Real st 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 holds 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)))]| proofend; theorem :: EUCLID_8:102 for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL for t0 being Real st 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 holds 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))]| proofend; theorem Th103: :: EUCLID_8:103 for f1, f2, f3 being PartFunc of REAL,REAL for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & f1 . t0 <> 0 & f2 . t0 <> 0 & f3 . t0 <> 0 holds VFuncdiff ((f1 ^),(f2 ^),(f3 ^),t0) = - |[((diff (f1,t0)) / ((f1 . t0) ^2)),((diff (f2,t0)) / ((f2 . t0) ^2)),((diff (f3,t0)) / ((f3 . t0) ^2))]| proofend; theorem :: EUCLID_8:104 for r being Element of REAL for f1, f2, f3 being PartFunc of REAL,REAL for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 holds VFuncdiff ((r (#) f1),(r (#) f2),(r (#) f3),t0) = (((r * (diff (f1,t0))) * ) + ((r * (diff (f2,t0))) * )) + ((r * (diff (f3,t0))) * ) proofend; theorem :: EUCLID_8:105 for r being Element of REAL for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL for t0 being Real st 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 holds VFuncdiff ((r (#) (f1 + g1)),(r (#) (f2 + g2)),(r (#) (f3 + g3)),t0) = (r * (VFuncdiff (f1,f2,f3,t0))) + (r * (VFuncdiff (g1,g2,g3,t0))) proofend; theorem :: EUCLID_8:106 for r being Element of REAL for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL for t0 being Real st 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 holds VFuncdiff ((r (#) (f1 - g1)),(r (#) (f2 - g2)),(r (#) (f3 - g3)),t0) = (r * (VFuncdiff (f1,f2,f3,t0))) - (r * (VFuncdiff (g1,g2,g3,t0))) proofend; theorem :: EUCLID_8:107 for r being Element of REAL for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL for t0 being Real st 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 holds 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)))]|) proofend; theorem :: EUCLID_8:108 for r being Element of REAL for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL for t0 being Real st 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 holds 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)))]| proofend; theorem :: EUCLID_8:109 for r being Element of REAL for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL for t0 being Real st 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 holds 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))]| proofend; theorem :: EUCLID_8:110 for r being Element of REAL for f1, f2, f3 being PartFunc of REAL,REAL for t0 being Real st 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 holds 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))]|) proofend; theorem :: EUCLID_8:111 for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL for t0 being Real st 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 holds 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)))]| proofend; ::p37-4(5.1) A*(BXC) theorem :: EUCLID_8:112 for f1, f2, f3, g1, g2, g3, h1, h2, h3 being PartFunc of REAL,REAL for t0 being Real st 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 holds 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)))))]| proofend; ::p37-4(5.2) A*BXC theorem :: EUCLID_8:113 for f1, f2, f3, g1, g2, g3, h1, h2, h3 being PartFunc of REAL,REAL for t0 being Real st 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 holds 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)))]| proofend; ::p37-4(6) AX(BXC) theorem :: EUCLID_8:114 for f1, f2, f3, g1, g2, g3, h1, h2, h3 being PartFunc of REAL,REAL for t0 being Real st 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 holds 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)))))]| proofend;