:: 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-2026 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;
equalities VALUED_1, EUCLID, SQUARE_1, RCOMP_1, RVSUM_1;
expansions RVSUM_1;
theorems RVSUM_1, FINSEQ_2, FINSEQ_1, XREAL_0, EUCLID_4, EUCLID_5, SQUARE_1,
XCMPLX_1, EUCLIDLP, FDIFF_1, FDIFF_2, EUCLID, FUNCT_2, VALUED_1, FDIFF_3,
XREAL_1, RFUNCT_1;
schemes FUNCT_2;
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; :: redefines |[ (EUCLID_5, synonym) → <* (FINSEQ_1, definition)
coherence
proof
reconsider x,y,z as Element of REAL by XREAL_0:def 1;
<*x,y,z*> is Element of REAL 3 by FINSEQ_2:104;
hence thesis;
end;
end;
theorem Th1:
p = |[ p.1, p.2, p.3 ]|
proof
consider x,y,z being Element of REAL such that
A1: p = <*x,y,z*> by FINSEQ_2:103;
thus thesis by A1;
end;
Lm1:
for r being Real holds r*p = |[ r*p.1, r*p.2, r*p.3 ]|
proof
let r be Real;
A1: (r*p).1 = r*(p.1) by RVSUM_1:44;
A2: (r*p).2 = r*(p.2) by RVSUM_1:44;
(r*p).3 = r*(p.3) by RVSUM_1:44;
hence thesis by A1,A2,Th1;
end;
Lm2:
p1+p2 = |[ p1.1+p2.1, p1.2+p2.2, p1.3+p2.3 ]|
proof
A1: (p1+p2).1 = p1.1+p2.1 by RVSUM_1:11;
A2: (p1+p2).2 = p1.2+p2.2 by RVSUM_1:11;
(p1+p2).3 = p1.3+p2.3 by RVSUM_1:11;
hence thesis by A1,A2,Th1;
end;
Lm3:
(-p).1 = -p.1 & (-p).2 = -p.2 & (-p).3 = -p.3
proof
-p = |[ (-1)*p.1, (-1)*p.2, (-1)*p.3 ]| by Lm1
.= |[ -p.1, -p.2, -p.3 ]|;
hence thesis;
end;
theorem
for f being FinSequence of REAL st len f = 3 holds f is Element of REAL 3
proof
let f be FinSequence of REAL;
assume
A1: len f = 3;
reconsider x1 = f.1, x2 = f.2, x3 = f.3 as Element of REAL
by XREAL_0:def 1;
<*x1,x2,x3*> is Element of 3-tuples_on REAL by FINSEQ_2:104;
hence thesis by A1,FINSEQ_1:45;
end;
Lm4:
p1-p2 = |[ p1.1-p2.1, p1.2-p2.2, p1.3-p2.3 ]|
proof
A1: (-p2).1 = -p2.1 by Lm3;
A2: (-p2).2 = -p2.2 by Lm3;
(-p2).3 = -p2.3 by Lm3;
then p1+-p2 = |[ p1.1+-p2.1, p1.2+-p2.2, p1.3+-p2.3 ]| by A1,A2,Lm2;
hence thesis;
end;
Lm5:
|(p1,p2)| = p1.1*p2.1 + p1.2*p2.2 + p1.3*p2.3
proof
reconsider f1=p1, f2=p2 as FinSequence of REAL;
A1: len f1 = len <* p1.1, p1.2, p1.3 *> by Th1
.= 3 by FINSEQ_1:45;
len f2 = len <* p2.1, p2.2, p2.3 *> by Th1
.= 3 by FINSEQ_1:45;
then
|(p1,p2)| = Sum <* f1.1*f2.1, f1.2*f2.2, f1.3*f2.3 *> by A1,EUCLID_5:28
.= p1.1*p2.1 + p1.2*p2.2 + p1.3*f2.3 by RVSUM_1:78;
hence thesis;
end;
Lm6:
r*|[ x,y,z ]| = |[ r*x, r*y, r*z ]|
proof
set p = |[ x,y,z ]|;
r*p = |[ r*p.1, r*p.2, r*p.3 ]| by Lm1
.=|[ r*x, r*p.2, r*p.3 ]|
.=|[ r*x, r*y, r*p.3 ]|
.=|[ r*x, r*y, r*z ]|;
hence thesis;
end;
Lm7:
p1+-p2 = |[ p1.1-p2.1, p1.2-p2.2, p1.3-p2.3 ]|
proof
A1: -p2 = |[ (-1)*p2.1, (-1)*p2.2, (-1)*p2.3 ]| by Lm1
.= |[ -p2.1, -p2.2, -p2.3 ]|;
p1 + -p2 = |[ (p1).1+(-p2).1, (p1).2+(-p2).2, (p1).3 +(-p2).3]| by Lm2
.= |[ p1.1+-p2.1, (p1).2+(-p2).2, (p1).3+(-p2).3 ]|
by A1
.= |[ p1.1+-p2.1, p1.2+-p2.2, (p1).3+(-p2).3 ]| by A1
.= |[ p1.1+-p2.1, p1.2+-p2.2, p1.3+-p2.3 ]| by A1;
hence thesis;
end;
Lm8:
|[ x1,x2,x3 ]| + |[ y1,y2,y3 ]| = |[ x1+y1, x2+y2, x3+y3 ]|
proof
A4: |[ x1,x2,x3 ]|.1 + |[ y1,y2,y3 ]|.1 = x1+y1;
A5: |[ x1,x2,x3 ]|.2 + |[ y1,y2,y3 ]|.2 = x2+y2;
|[ x1,x2,x3 ]|.3 + |[ y1,y2,y3 ]|.3 = x3+y3;
hence thesis by A4,A5,Lm2;
end;
Lm9:
(p1+p2)+(q1+q2) = (p1+q1)+(p2+q2)
proof
thus (p1+p2)+(q1+q2) = (p1+p2)+q1+q2 by RVSUM_1:15
.= (p1+q1)+p2+q2 by RVSUM_1:15
.= (p1+q1)+(p2+q2) by RVSUM_1:15;
end;
Lm10:
(p1+p2)-(q1+q2) = (p1-q1)+(p2-q2)
proof
thus (p1+p2)-(q1+q2) = (p1+ p2)-q1-q2 by RVSUM_1:39
.= (p1+p2)+(-q1+-q2) by RVSUM_1:15
.= (p1-q1)+(p2-q2) by Lm9;
end;
Lm11:
|[ x1,x2,x3 ]| - |[ y1,y2,y3 ]| = |[ x1-y1,x2-y2,x3-y3 ]|
proof
A4: |[ x1,x2,x3 ]|.1 - |[ y1,y2,y3 ]|.1 = x1-y1;
A5: |[ x1,x2,x3 ]|.2 - |[ y1,y2,y3 ]|.2 = x2-y2;
|[ x1,x2,x3 ]|.3 - |[ y1,y2,y3 ]|.3 = x3-y3;
hence thesis by A4,A5,Lm7;
end;
definition
func <e1> -> Element of REAL 3 equals
|[ 1,0,0 ]|;
coherence;
func <e2> -> Element of REAL 3 equals
|[ 0,1,0 ]|;
coherence;
func <e3> -> Element of REAL 3 equals
|[ 0,0,1 ]|;
coherence;
end;
Lm12:
p = |[ x,y,z ]| implies |(p,p)| = x^2 + y^2 + z^2
proof
assume p = |[ x,y,z ]|;
then p.1 = x & p.2 = y & p.3 = z;
hence thesis by Lm5;
end;
definition let p1, p2;
func p1 <X> p2 -> Element of REAL 3 equals
|[ (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;
end;
Lm14:
(r*p1)<X>p2 = r*(p1<X>p2) & (r*p1)<X>p2 = p1<X>(r*p2)
proof
A2: (r*p1)<X>p2 = |[ r*p1.1,r*p1.2,r*p1.3 ]|<X>p2 by Lm1
.= |[ r*p1.1,r*p1.2,r*p1.3 ]|<X>|[ p2.1,p2.2,p2.3 ]|
.= |[ (r*p1.2*p2.3)-(r*p1.3*p2.2),(r*p1.3*p2.1)-(r*p1.1*p2.3),
(r*p1.1*p2.2)-(r*p1.2*p2.1) ]|;then
A3: (r*p1)<X>p2 = |[ r*(p1<X>p2).1,r*(p1<X>p2).2,r*(p1<X>p2).3 ]|
.= r*(p1<X>p2) by Lm1;
(r*p1)<X>p2 = |[ p1.2*(r*p2.3)-p1.3*(r*p2.2),p1.3*(r*p2.1)-p1.1*(r*p2.3),
p1.1*(r*p2.2)-p1.2*(r*p2.1) ]| by A2
.= |[ p1.1,p1.2,p1.3 ]|<X>|[ r*p2.1,r*p2.2,r*p2.3 ]|
.= p1<X>|[ r*p2.1,r*p2.2,r*p2.3 ]|
.= p1<X>(r*p2) by Lm1;
hence thesis by A3;
end;
theorem
p1,p2 are_ldependent2 implies p1<X>p2 = 0.REAL 3
proof
assume p1,p2 are_ldependent2;then
A1: ex a1,a2 being Real st a1*p1+a2*p2 = 0.REAL 3
& (a1 <> 0 or a2 <> 0) by EUCLIDLP:def 2;
now per cases by A1;
case
ex a1,a2 being Real st a1*p1+a2*p2 = 0.REAL 3 & a1 <> 0;
then consider a1,a2 being Real such that
A2: a1 <> 0 & a1*p1+a2*p2 = 0.REAL 3;
A3: (1/a1)*(a1*p1) = (1/a1)*(-a2*p2) by A2,RVSUM_1:23
.= (1/a1)*(((-1)*a2)*p2) by RVSUM_1:49
.= (1/a1)*((-a2)*p2);
A4: (1/a1)*(a1*p1) = (a1*(1/a1))*p1 by EUCLID_4:4
.= 1*p1 by A2,XCMPLX_1:106;
A5: 1*p1 = |[ 1*p1.1,1*p1.2,1*p1.3]| by Lm1
.= p1 by Th1;
A6: 0.REAL 3 = |[0,0,0 ]| by FINSEQ_2:62;
p1<X>p2 = (((-a2)*(1/a1))*p2)<X>p2 by A3,A4,A5,EUCLID_4:4
.= ((-a2)/a1*p2)<X>p2 by XCMPLX_1:99;then
p1<X>p2 = (-a2)/a1*(p2<X>p2) by Lm14;then
p1<X>p2 = ((-a2)/a1)*0.REAL 3 by FINSEQ_2:62
.= |[ ((-a2)/a1)*(0.REAL 3).1,((-a2)/a1)*(0.REAL 3).2,
((-a2)/a1)*(0.REAL 3).3 ]| by Lm1
.= |[ ((-a2)/a1)*0,((-a2)/a1)*(0.REAL 3).2,
((-a2)/a1)*(0.REAL 3).3 ]| by A6
.= |[ 0,((-a2)/a1)*0,((-a2)/a1)*(0.REAL 3).3 ]|
by A6
.= 0.REAL 3 by A6;
hence thesis;
end;
case
ex a1,a2 being Real st a1*p1+a2*p2 = 0.REAL 3 & a2 <> 0;
then consider a1,a2 being Real such that
A7: a2 <> 0 & a1*p1+a2*p2 = 0.REAL 3;
A8: (1/a2)*(a2*p2) = (1/a2)*(-a1*p1) by A7,RVSUM_1:23
.= (1/a2)*(((-1)*a1)*p1) by RVSUM_1:49
.= (1/a2)*((-a1)*p1);
A9: (1/a2)*(a2*p2) = (a2*(1/a2))*p2 by EUCLID_4:4
.= 1*p2 by A7,XCMPLX_1:106;
A10: 1*p2 = |[ 1*p2.1,1*p2.2,1*p2.3]| by Lm1
.= p2 by Th1;
A11: 0.REAL 3 = |[0,0,0 ]| by FINSEQ_2:62;
p1<X>p2 = p1<X>(((-a1)*(1/a2))*p1) by A8,A9,A10,EUCLID_4:4
.= p1<X>((-a1)/a2*p1) by XCMPLX_1:99
.= (-a1)/a2*p1<X>p1 by Lm14
.= (-a1)/a2*(p1<X>p1) by Lm14
.= ((-a1)/a2)*0.REAL 3 by FINSEQ_2:62
.= |[ ((-a1)/a2)*(0.REAL 3).1,((-a1)/a2)*(0.REAL 3).2,
((-a1)/a2)*(0.REAL 3).3 ]| by Lm1
.= |[ ((-a1)/a2)*0,((-a1)/a2)*(0.REAL 3).2,
((-a1)/a2)*(0.REAL 3).3 ]| by A11
.= |[ 0,((-a1)/a2)*0,((-a1)/a2)*(0.REAL 3).3 ]|
by A11
.= 0.REAL 3 by A11;
hence thesis;
end;
end;
hence thesis;
end;
begin :: Vector Function in 3-dimensional Euclidean Spaces
theorem
|. <e1> .| = 1
proof
|(<e1>,<e1>)| = 1^2 + 0^2 + 0^2 by Lm12 .= 1;
hence thesis;
end;
theorem
|. <e2> .| = 1
proof
|(<e2>,<e2>)| = 0^2 + 1^2 + 0^2 by Lm12 .= 1;
hence thesis;
end;
theorem
|. <e3> .| = 1
proof
|(<e3>,<e3>)| = 0^2 + 0^2 + 1^2 by Lm12 .= 1;
hence thesis;
end;
theorem
<e1>,<e2> are_orthogonal
proof
<e1>.1 = 1 & <e1>.2 = 0 & <e1>.3 = 0 &
<e2>.1 = 0 & <e2>.2 = 1 & <e2>.3 = 0;
then |(<e1>,<e2>)| = 1 * 0 + 0 * 1 + 0 * 0 by Lm5
.= 0;
hence <e1>,<e2> are_orthogonal;
end;
theorem
<e1>,<e3> are_orthogonal
proof
<e1>.1 = 1 & <e1>.2 = 0 & <e1>.3 = 0 &
<e3>.1 = 0 & <e3>.2 = 0 & <e3>.3 = 1;
then |(<e1>,<e3>)| = 1 * 0 + 0 * 0 + 0 * 1 by Lm5
.= 0;
hence <e1>,<e3> are_orthogonal;
end;
theorem
<e2>,<e3> are_orthogonal
proof
<e2>.1 = 0 & <e2>.2 = 1 & <e2>.3 = 0 &
<e3>.1 = 0 & <e3>.2 = 0 & <e3>.3 = 1;
then |(<e2>,<e3>)| = 0 * 0 + 1 * 0 + 0 * 1 by Lm5
.= 0;
hence <e2>,<e3> are_orthogonal;
end;
theorem
|(<e1>,<e1>)| = 1
proof
<e1>.1 = 1 & <e1>.2 = 0 & <e1>.3 = 0;
then |(<e1>,<e1>)| = 1 * 1 + 0 * 0 + 0 * 0 by Lm5
.= 1;
hence thesis;
end;
theorem
|(<e2>,<e2>)| = 1
proof
<e2>.1 = 0 & <e2>.2 = 1 & <e2>.3 = 0;
then |(<e2>,<e2>)| = 0 * 0 + 1 * 1 + 0 * 0 by Lm5
.= 1;
hence thesis;
end;
theorem
|(<e3>,<e3>)| = 1
proof
<e3>.1 = 0 & <e3>.2 = 0 & <e3>.3 = 1;
then |(<e3>,<e3>)| = 0 * 0 + 0 * 0 + 1 * 1 by Lm5
.= 1;
hence thesis;
end;
theorem Th13:
|( p , |[ 0,0,0 ]| )| = 0
proof
set e = |[ 0,0,0 ]|;
e.1 = 0 & e.2 = 0 & e.3 = 0;
hence |(p,e)| = p.1 * 0 + p.2 * 0 + p.3 * 0 by Lm5
.= 0;
end;
::$CT 2
theorem
<e1><X><e2> = <e3>
proof
thus thesis;
end;
theorem
<e2><X><e3> = <e1>
proof
thus thesis;
end;
theorem
<e3><X><e1> = <e2>
proof
thus thesis;
end;
theorem
<e3><X><e2> = -<e1>
proof
<e3><X><e2> = |[ (0 * 0)-(1*1),(1 * 0)-(0 * 0),(0 * 1)-(0 * 0) ]|
.= |[ (-1)*<e1>.1,(-1)*<e1>.2,(-1)*<e1>.3 ]|
.= -<e1> by Lm1;
hence thesis;
end;
theorem
<e1><X><e3> = -<e2>
proof
<e1><X><e3>
= |[ (0 * 1)-(0 * 0),(0 * 0)-(1 * 1),(1 * 0)-(0 * 0 )]|
.= |[ (-1)*<e2>.1,(-1)*<e2>.2,(-1)*<e2>.3 ]|
.= -<e2> by Lm1;
hence thesis;
end;
theorem
<e2><X><e1> = -<e3>
proof
<e2><X><e1> = |[ (1 * 0)-(0 * 0),(0 * 1)-(0 * 0),(0 * 0)-(1 * 1) ]|
.= |[ (-1)*<e3>.1,(-1)*<e3>.2,(-1)*<e3>.3 ]|
.= -<e3> by Lm1;
hence thesis;
end;
theorem
p <X> |[ 0,0,0 ]| = |[ 0,0,0 ]|
proof
thus p <X> |[ 0,0,0 ]|
= |[ (p.2 * 0)-(p.3 * 0),(p.3 * 0)-(p.1 * 0),(p.1 * 0)-(p.2 * 0) ]|
.= |[ 0,0,0 ]|;
end;
::$CT 2
theorem Th21:
r*<e1> = |[ r,0,0 ]|
proof
<e1>.1 = 1 & <e1>.2 = 0 & <e1>.3 = 0;
then r*<e1> = |[ r*1,r*0,r*0 ]| by Lm1 .= |[ r,0,0 ]|;
hence thesis;
end;
theorem Th22:
r*<e2> = |[ 0,r,0 ]|
proof
<e2>.1 = 0 & <e2>.2 = 1 & <e2>.3 = 0;
then r*<e2> = |[ r*0,r*1,r*0 ]| by Lm1 .= |[ 0,r,0 ]|;
hence thesis;
end;
theorem Th23:
r*<e3> = |[ 0,0,r ]|
proof
<e3>.1 = 0 & <e3>.2 = 0 & <e3>.3 = 1;
then r*<e3> = |[ r*0,r*0,r*1 ]| by Lm1 .= |[ 0,0,r ]|;
hence thesis;
end;
theorem
1*p = p by RFUNCT_1:21;
::$CT 2
theorem
-<e1> = |[ -1,0,0 ]|
proof
-<e1> = |[ (-1)*<e1>.1, (-1)*<e1>.2, (-1)*<e1>.3 ]| by Lm1
.= |[ -1,0,0 ]|;
hence thesis;
end;
theorem
-<e2> = |[ 0,-1,0 ]|
proof
-<e2> = |[ (-1)*<e2>.1, (-1)*<e2>.2, (-1)*<e2>.3 ]| by Lm1
.= |[ 0,-1,0 ]|;
hence thesis;
end;
theorem
-<e3> = |[ 0,0,-1 ]|
proof
-<e3> = |[ (-1)*<e3>.1, (-1)*<e3>.2, (-1)*<e3>.3 ]| by Lm1
.= |[ 0,0,-1 ]|;
hence thesis;
end;
theorem
0 * p = |[ 0,0,0 ]|
proof
thus 0 * p = |[ 0 * p.1,0 * p.2,0 * p.3]| by Lm1
.= |[ 0,0,0 ]|;
end;
::$CT 2
theorem
p = p.1*<e1> + p.2*<e2> + p.3*<e3>
proof
A1: <e1>.1 = 1 & <e1>.2 = 0 & <e1>.3 = 0;
A2: <e2>.1 = 0 & <e2>.2 = 1 & <e2>.3 = 0;
A3: <e3>.1 = 0 & <e3>.2 = 0 & <e3>.3 = 1;
A4: p.1*<e1> + p.2*<e2> + p.3*<e3>
= |[ p.1*1,p.1*0,p.1*0 ]| + p.2*<e2> + p.3*<e3> by A1,Lm1
.= |[ p.1,0,0 ]| + |[ p.2*0,p.2*1,p.2*0 ]| + p.3*<e3> by A2,Lm1
.= |[ p.1,0,0 ]| + |[ 0,p.2,0 ]| + |[ p.3*0,p.3*0,p.3*1 ]| by A3,Lm1
.= |[ p.1,0,0 ]| + |[ 0,p.2,0 ]| + |[ 0,0,p.3 ]|;
A5: |[ p.1,0,0 ]|.1 = p.1 & |[ p.1,0,0 ]|.2 = 0 & |[ p.1,0,0 ]|.3 = 0;
A6: |[ 0,p.2,0 ]|.1 = 0 & |[ 0,p.2,0 ]|.2 = p.2 & |[ 0,p.2,0 ]|.3 = 0;
A7: |[ 0,0,p.3 ]|.1 = 0 & |[ 0,0,p.3 ]|.2 = 0 & |[ 0,0,p.3 ]|.3 = p.3;
A8: p.1*<e1> + p.2*<e2> + p.3*<e3>
= |[ p.1+0,0+p.2,0+0 ]| + |[ 0,0,p.3 ]| by A4,A5,A6,Lm2
.= |[ p.1,p.2,0 ]| + |[ 0,0,p.3 ]|;
|[ p.1,p.2,0 ]|.1 = p.1 & |[ p.1,p.2,0 ]|.2 = p.2 &
|[ p.1,p.2,0 ]|.3 = 0;
then
p.1*<e1> + p.2*<e2> + p.3*<e3> = |[ p.1+0,p.2+0,0 +p.3]| by A7,A8,Lm2
.= |[ p.1,p.2,p.3 ]|;
hence p = p.1*<e1> + p.2*<e2> + p.3*<e3> by Th1;
end;
theorem Th30:
r*p = r*p.1*<e1> + r*p.2*<e2> + r*p.3*<e3>
proof
A1: <e1>.1 = 1 & <e1>.2 = 0 & <e1>.3 = 0;
A2: <e2>.1 = 0 & <e2>.2 = 1 & <e2>.3 = 0;
A3: <e3>.1 = 0 & <e3>.2 = 0 & <e3>.3 = 1;
A4: r*p.1*<e1> + r*p.2*<e2> + r*p.3*<e3>
= |[ r*p.1*1,r*p.1*0,r*p.1*0 ]| + r*p.2*<e2> + r*p.3*<e3>
by A1,Lm1
.= |[ r*p.1,0,0 ]| + |[ r*p.2*0,r*p.2*1,r*p.2*0 ]| + r*p.3*<e3>
by A2,Lm1
.= |[ r*p.1,0,0 ]| + |[ 0,r*p.2,0 ]| + |[ r*p.3*0,r*p.3*0,r*p.3*1 ]|
by A3,Lm1
.= |[ r*p.1,0,0 ]| + |[ 0,r*p.2,0 ]| + |[ 0,0,r*p.3 ]|;
A5: |[ r*p.1,0,0 ]|.1 = r*p.1 & |[ r*p.1,0,0 ]|.2 = 0 & |[ r*p.1,0,0 ]|.3 = 0;
A6: |[ 0,r*p.2,0 ]|.1 = 0 & |[ 0,r*p.2,0 ]|.2 = r*p.2 & |[ 0,r*p.2,0 ]|.3 = 0;
A7: |[ 0,0,r*p.3 ]|.1 = 0 & |[ 0,0,r*p.3 ]|.2 = 0 & |[ 0,0,r*p.3 ]|.3 = r*p.3;
A8: r*p.1*<e1> + r*p.2*<e2> + r*p.3*<e3>
= |[ r*p.1+0,0+r*p.2,0+0 ]| + |[ 0,0,r*p.3 ]| by A4,A5,A6,Lm2
.= |[ r*p.1,r*p.2,0 ]| + |[ 0,0,r*p.3 ]|;
|[ r*p.1,r*p.2,0 ]|.1 = r*p.1 & |[ r*p.1,r*p.2,0 ]|.2 = r*p.2 &
|[ r*p.1,r*p.2,0 ]|.3 = 0;
then r*p.1*<e1> + r*p.2*<e2> + r*p.3*<e3>
= |[ r*p.1+0,r*p.2+0,0+r*p.3]| by A7,A8,Lm2
.= |[ r*p.1,r*p.2,r*p.3 ]|;
hence r*p = r*p.1*<e1> + r*p.2*<e2> + r*p.3*<e3> by Lm1;
end;
theorem Th31:
|[ x,y,z ]| = x*<e1> + y*<e2> + z*<e3>
proof
A1: <e1>.1 = 1 & <e1>.2 = 0 & <e1>.3 = 0;
A2: <e2>.1 = 0 & <e2>.2 = 1 & <e2>.3 = 0;
A3: <e3>.1 = 0 & <e3>.2 = 0 & <e3>.3 = 1;
set p = |[ x,y,z ]|;
A4: x*<e1> + y*<e2> + z*<e3> = |[ x*1,x*0,x*0 ]| + y*<e2> + z*<e3> by A1,Lm1
.= |[ x,0,0 ]| + |[ y*0,y*1,y*0 ]| + z*<e3> by A2,Lm1
.= |[ x,0,0 ]| + |[ 0,y,0 ]| + |[ z*0,z*0,z*1 ]| by A3,Lm1
.= |[ x,0,0 ]| + |[ 0,y,0 ]| + |[ 0,0,z ]|;
A5: |[ x,0,0 ]|.1 = x & |[ x,0,0 ]|.2 = 0 & |[ x,0,0 ]|.3 = 0;
A6: |[ 0,y,0 ]|.1 = 0 & |[ 0,y,0 ]|.2 = y & |[ 0,y,0 ]|.3 = 0;
A7: |[ 0,0,z ]|.1 = 0 & |[ 0,0,z ]|.2 = 0 & |[ 0,0,z ]|.3 = z;
A8: x*<e1> + y*<e2> + z*<e3>
= |[ x+0,y+0,0+0 ]| + |[ 0,0,z ]| by A4,A5,A6,Lm2
.= |[ x,y,0 ]| + |[ 0,0,z ]|;
|[ x,y,0 ]|.1 = x & |[ x,y,0 ]|.2 = y & |[ x,y,0 ]|.3 = 0;
then x*<e1> + y*<e2> + z*<e3> = |[ x+0,y+0,0+z ]| by A7,A8,Lm2
.= |[ x,y,z ]|;
hence p = x*<e1> + y*<e2> + z*<e3>;
end;
theorem Th32:
r*|[ x,y,z ]| = r*x*<e1> + r*y*<e2> + r*z*<e3>
proof
A1: <e1>.1 = 1 & <e1>.2 = 0 & <e1>.3 = 0;
A2: <e2>.1 = 0 & <e2>.2 = 1 & <e2>.3 = 0;
A3: <e3>.1 = 0 & <e3>.2 = 0 & <e3>.3 = 1;
set p = |[ x,y,z ]|;
A4: r*x*<e1> + r*y*<e2> + r*z*<e3>
= |[ r*x*1,r*x*0,r*x*0 ]| + r*y*<e2> + r*z*<e3> by A1,Lm1
.= |[ r*x,0,0 ]| + |[ r*y*0,r*y*1,r*y*0 ]| + r*z*<e3> by A2,Lm1
.= |[ r*x,0,0 ]| + |[ 0,r*y,0 ]| + |[ r*z*0,r*z*0,r*z*1 ]| by A3,Lm1
.= |[ r*x,0,0 ]| + |[ 0,r*y,0 ]| + |[ 0,0,r*z ]|;
A5: |[ r*x,0,0 ]|.1 = r*x & |[ r*x,0,0 ]|.2 = 0 & |[ r*x,0,0 ]|.3 = 0;
A6: |[ 0,r*y,0 ]|.1 = 0 & |[ 0,r*y,0 ]|.2 = r*y & |[ 0,r*y,0 ]|.3 = 0;
A7: |[ 0,0,r*z ]|.1 = 0 & |[ 0,0,r*z ]|.2 = 0 & |[ 0,0,r*z ]|.3 = r*z;
A8: r*x*<e1> + r*y*<e2> + r*z*<e3>
= |[ r*x+0,r*y+0,0+0 ]| + |[ 0,0,r*z ]| by A4,A5,A6,Lm2
.= |[ r*x,r*y,0 ]| + |[ 0,0,r*z ]|;
|[ r*x,r*y,0 ]|.1 = r*x & |[ r*x,r*y,0 ]|.2 = r*y & |[ r*x,r*y,0 ]|.3 = 0;
then r*x*<e1> + r*y*<e2> + r*z*<e3>
= |[ r*x+0,r*y+0,0+r*z ]| by A7,A8,Lm2
.= |[ r*x,r*y,r*z ]|;
hence r*p = r*x*<e1> + r*y*<e2> + r*z*<e3> by Lm6;
end;
theorem
-p = - p.1*<e1> - p.2*<e2> - p.3*<e3>
proof
-p = (-1)*p.1*<e1> + (-1)*p.2*<e2> + (-1)*p.3*<e3> by Th30
.= -p.1*<e1> + ((-1)*p.2)*<e2> + (-p.3)*<e3> by RVSUM_1:49
.= -p.1*<e1> + -p.2*<e2> +((-1)*p.3)*<e3> by RVSUM_1:49
.= - p.1*<e1> - p.2*<e2> - p.3*<e3> by RVSUM_1:49;
hence thesis;
end;
theorem
-|[ x,y,z ]| = -x*<e1> - y*<e2> - z*<e3>
proof
-|[ x,y,z ]| = (-1)*x*<e1> + (-1)*y*<e2> + (-1)*z*<e3> by Th32
.=-x*<e1> + ((-1)*y)*<e2> + (-z)*<e3> by RVSUM_1:49
.=-x*<e1> + -y*<e2> + ((-1)*z)*<e3> by RVSUM_1:49
.=-x*<e1> - y*<e2> - z*<e3> by RVSUM_1:49;
hence thesis;
end;
theorem
p1+p2 = (p1.1+p2.1)*<e1>+(p1.2+p2.2)*<e2>+(p1.3+p2.3)*<e3>
proof
A1: <e1>.1 = 1 & <e1>.2 = 0 & <e1>.3 = 0;
A2: <e2>.1 = 0 & <e2>.2 = 1 & <e2>.3 = 0;
A3: <e3>.1 = 0 & <e3>.2 = 0 & <e3>.3 = 1;
A4: (p1+p2).1 = p1.1+p2.1 by RVSUM_1:11;
A5: (p1+p2).2 = p1.2+p2.2 by RVSUM_1:11;
A6: (p1+p2).3 = p1.3+p2.3 by RVSUM_1:11;
A7: (p1+p2).1*<e1> + (p1+p2).2*<e2> + (p1+p2).3*<e3>
= |[ (p1+p2).1*1,(p1+p2).1*0,(p1+p2).1*0 ]| + (p1+p2).2*<e2>
+ (p1+p2).3*<e3> by A1,Lm1
.= |[ (p1+p2).1,0,0 ]| + |[ (p1+p2).2*0,(p1+p2).2*1,(p1+p2).2*0 ]|
+ (p1+p2).3*<e3> by A2,Lm1
.= |[ (p1+p2).1,0,0 ]| + |[ 0,(p1+p2).2,0 ]|
+ |[ (p1+p2).3*0,(p1+p2).3*0,(p1+p2).3*1 ]| by A3,Lm1
.= |[ (p1+p2).1,0,0 ]| + |[ 0,(p1+p2).2,0 ]| + |[ 0,0,(p1+p2).3 ]|;
A8: |[ (p1+p2).1,0,0 ]|.1 = (p1+p2).1 & |[ (p1+p2).1,0,0 ]|.2 = 0 &
|[ (p1+p2).1,0,0 ]|.3 = 0;
A9: |[ 0,(p1+p2).2,0 ]|.1 = 0 & |[ 0,(p1+p2).2,0 ]|.2 = (p1+p2).2 &
|[ 0,(p1+p2).2,0 ]|.3 = 0;
A10: |[ 0,0,(p1+p2).3 ]|.1 = 0 & |[ 0,0,(p1+p2).3 ]|.2 = 0 &
|[ 0,0,(p1+p2).3 ]|.3 = (p1+p2).3;
A11: (p1+p2).1*<e1> + (p1+p2).2*<e2> + (p1+p2).3*<e3>
= |[ (p1+p2).1+0,0+(p1+p2).2,0+0 ]| + |[ 0,0,(p1+p2).3 ]|
by A7,A8,A9,Lm2
.= |[ (p1+p2).1,(p1+p2).2,0 ]| + |[ 0,0,(p1+p2).3 ]|;
|[ (p1+p2).1,(p1+p2).2,0 ]|.1 = (p1+p2).1 &
|[ (p1+p2).1,(p1+p2).2,0 ]|.2 = (p1+p2).2 &
|[ (p1+p2).1,(p1+p2).2,0 ]|.3 = 0;
then (p1+p2).1*<e1> + (p1+p2).2*<e2> + (p1+p2).3*<e3>
= |[ (p1+p2).1+0,(p1+p2).2+0,0 +(p1+p2).3]| by A10,A11,Lm2
.= |[ (p1+p2).1,(p1+p2).2,(p1+p2).3 ]|;
hence thesis by A4,A5,A6,Th1;
end;
theorem Th36:
p1-p2 = (p1.1-p2.1)*<e1>+(p1.2-p2.2)*<e2>+(p1.3-p2.3)*<e3>
proof
A1: <e1>.1 = 1 & <e1>.2 = 0 & <e1>.3 = 0;
A2: <e2>.1 = 0 & <e2>.2 = 1 & <e2>.3 = 0;
A3: <e3>.1 = 0 & <e3>.2 = 0 & <e3>.3 = 1;
A4: (p1-p2).1 = p1.1-p2.1 by RVSUM_1:27;
A5: (p1-p2).2 = p1.2-p2.2 by RVSUM_1:27;
A6: (p1-p2).3 = p1.3-p2.3 by RVSUM_1:27;
A7: (p1-p2).1*<e1> + (p1-p2).2*<e2> + (p1-p2).3*<e3>
= |[ (p1-p2).1*1,(p1-p2).1*0,(p1-p2).1*0 ]| + (p1-p2).2*<e2>
+ (p1-p2).3*<e3> by A1,Lm1
.= |[ (p1-p2).1,0,0 ]| + |[ (p1-p2).2*0,(p1-p2).2*1,(p1-p2).2*0 ]|
+ (p1-p2).3*<e3> by A2,Lm1
.= |[ (p1-p2).1,0,0 ]| + |[ 0,(p1-p2).2,0 ]|
+ |[ (p1-p2).3*0,(p1-p2).3*0,(p1-p2).3*1 ]| by A3,Lm1
.= |[ (p1-p2).1,0,0 ]| + |[ 0,(p1-p2).2,0 ]| + |[ 0,0,(p1-p2).3 ]|;
A8: |[ (p1-p2).1,0,0 ]|.1 = (p1-p2).1 & |[ (p1-p2).1,0,0 ]|.2 = 0 &
|[ (p1-p2).1,0,0 ]|.3 = 0;
A9: |[ 0,(p1-p2).2,0 ]|.1 = 0 & |[ 0,(p1-p2).2,0 ]|.2 = (p1-p2).2 &
|[ 0,(p1-p2).2,0 ]|.3 = 0;
A10: |[ 0,0,(p1-p2).3 ]|.1 = 0 & |[ 0,0,(p1-p2).3 ]|.2 = 0 &
|[ 0,0,(p1-p2).3 ]|.3 = (p1-p2).3;
A11: (p1-p2).1*<e1> + (p1-p2).2*<e2> + (p1-p2).3*<e3>
= |[ (p1-p2).1+0,0+(p1-p2).2,0+0 ]| + |[ 0,0,(p1-p2).3 ]|
by A7,A8,A9,Lm2
.= |[ (p1-p2).1,(p1-p2).2,0 ]| + |[ 0,0,(p1-p2).3 ]|;
|[ (p1-p2).1,(p1-p2).2,0 ]|.1 = (p1-p2).1 &
|[ (p1-p2).1,(p1-p2).2,0 ]|.2 = (p1-p2).2 &
|[ (p1-p2).1,(p1-p2).2,0 ]|.3 = 0;
then (p1-p2).1*<e1> + (p1-p2).2*<e2> + (p1-p2).3*<e3>
= |[ (p1-p2).1+0,(p1-p2).2+0,0 +(p1-p2).3]| by A10,A11,Lm2
.= |[ (p1-p2).1,(p1-p2).2,(p1-p2).3 ]|;
hence thesis by A4,A5,A6,Th1;
end;
theorem
|[ x1,x2,x3 ]| + |[ y1,y2,y3 ]| = (x1+y1)*<e1> + (x2+y2)*<e2> + (x3+y3)*<e3>
proof
A1: <e1>.1 = 1 & <e1>.2 = 0 & <e1>.3 = 0;
A2: <e2>.1 = 0 & <e2>.2 = 1 & <e2>.3 = 0;
A3: <e3>.1 = 0 & <e3>.2 = 0 & <e3>.3 = 1;
A4: (x1+y1)*<e1> + (x2+y2)*<e2> + (x3+y3)*<e3>
= |[ (x1+y1)*1,(x1+y1)*0,(x1+y1)*0 ]| + (x2+y2)*<e2>
+ (x3+y3)*<e3> by A1,Lm1
.= |[ x1+y1,0,0 ]| + |[ (x2+y2)*0,(x2+y2)*1,(x2+y2)*0 ]|
+ (x3+y3)*<e3> by A2,Lm1
.= |[ x1+y1,0,0 ]| + |[ 0,x2+y2,0 ]|
+ |[ (x3+y3)*0,(x3+y3)*0,(x3+y3)*1 ]| by A3,Lm1
.= |[ x1+y1,0,0 ]| + |[ 0,x2+y2,0 ]| + |[ 0,0,x3+y3 ]|;
A5: |[ x1+y1,0,0 ]|.1 = x1+y1 & |[ x1+y1,0,0 ]|.2 = 0
& |[ x1+y1,0,0 ]|.3 = 0;
A6: |[ 0,x2+y2,0 ]|.1 = 0 & |[ 0,x2+y2,0 ]|.2 = x2+y2
& |[ 0,x2+y2,0 ]|.3 = 0;
A7: |[ 0,0,x3+y3 ]|.1 = 0 & |[ 0,0,x3+y3 ]|.2 = 0
& |[ 0,0,x3+y3 ]|.3 = x3+y3;
A8: (x1+y1)*<e1> + (x2+y2)*<e2> + (x3+y3)*<e3>
= |[ (x1+y1) + 0,0 + (x2+y2),0 + 0 ]| + |[ 0,0,x3+y3 ]| by A4,A5,A6,Lm2
.= |[ x1+y1,x2+y2,0 ]| + |[ 0,0,x3+y3 ]|;
|[ x1+y1,x2+y2,0 ]|.1 = x1+y1 & |[ x1+y1,x2+y2,0 ]|.2 = x2+y2
& |[ x1+y1,x2+y2,0 ]|.3 = 0;
then A9: (x1+y1)*<e1> + (x2+y2)*<e2> + (x3+y3)*<e3>
= |[ (x1+y1) + 0 ,(x2+y2) + 0,0 + (x3+y3) ]| by A8,A7,Lm2
.= |[ x1+y1,x2+y2,x3+y3 ]|;
A10: |[ x1,x2,x3 ]|.1 = x1 & |[ x1,x2,x3 ]|.2 = x2 & |[ x1,x2,x3 ]|.3 = x3;
|[ y1,y2,y3 ]|.1 = y1 & |[ y1,y2,y3 ]|.2 = y2 & |[ y1,y2,y3 ]|.3 = y3;
hence thesis by A10,Lm2,A9;
end;
theorem
|[ x1,x2,x3 ]| - |[ y1,y2,y3 ]| = (x1-y1)*<e1> + (x2-y2)*<e2> + (x3-y3)*<e3>
proof
A4: |[ x1,x2,x3 ]|.1 - |[ y1,y2,y3 ]|.1 = x1-y1;
A5: |[ x1,x2,x3 ]|.2 - |[ y1,y2,y3 ]|.2 = x2-y2;
|[ x1,x2,x3 ]|.3 - |[ y1,y2,y3 ]|.3 = x3-y3;
hence thesis by A4,A5,Th36;
end;
theorem
p1.1*<e1> + p1.2*<e2> + p1.3*<e3>
= (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3> iff
p2.1*<e1> + p2.2*<e2> + p2.3*<e3>
= (p1.1 - p3.1)*<e1> + (p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>
proof
A1:r1*R - r2*R = (r1-r2)*R
proof
r1*R - r2*R = r1*R + ((-1)*r2)*R by RVSUM_1:49
.= (r1 + -r2)*R by RVSUM_1:50;
hence thesis;
end;
A2: <e1>.1 = 1 & <e1>.2 = 0 & <e1>.3 = 0;
A3: <e2>.1 = 0 & <e2>.2 = 1 & <e2>.3 = 0;
A4: <e3>.1 = 0 & <e3>.2 = 0 & <e3>.3 = 1;
thus p1.1*<e1> + p1.2*<e2> + p1.3*<e3>
= (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3> implies
p2.1*<e1> + p2.2*<e2> + p2.3*<e3>
= (p1.1 - p3.1)*<e1> + (p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>
proof
assume p1.1*<e1> + p1.2*<e2> + p1.3*<e3>
= (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3>;
then
p1.1*<e1> + (p1.2*<e2> + p1.3*<e3>) - p3.1*<e1> - p3.2*<e2> - p3.3*<e3>
= (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2>
+ (p2.3 + p3.3)*<e3> - p3.1*<e1> - p3.2*<e2> - p3.3*<e3> by RVSUM_1:15;
then
p1.1*<e1> - p3.1*<e1> + (p1.2*<e2> + p1.3*<e3>) - p3.2*<e2> - p3.3*<e3>
= (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2>
+ (p2.3 + p3.3)*<e3> - p3.1*<e1> - p3.2*<e2> - p3.3*<e3>
by RVSUM_1:15;
then (p1.1 - p3.1)*<e1> + (p1.2*<e2> + p1.3*<e3>) - p3.2*<e2> - p3.3*<e3>
= (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2>
+ (p2.3 + p3.3)*<e3> - p3.1*<e1> - p3.2*<e2> - p3.3*<e3> by A1;
then (p1.1 - p3.1)*<e1> + p1.2*<e2> + p1.3*<e3> - p3.2*<e2> - p3.3*<e3>
= (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2>
+ (p2.3 + p3.3)*<e3> - p3.1*<e1> - p3.2*<e2> - p3.3*<e3> by RVSUM_1:15;
then (p1.1 - p3.1)*<e1> + p1.2*<e2> - p3.2*<e2> + p1.3*<e3> - p3.3*<e3>
= (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2>
+ (p2.3 + p3.3)*<e3> - p3.1*<e1> - p3.2*<e2> - p3.3*<e3>
by RVSUM_1:15;
then (p1.1 - p3.1)*<e1> + (p1.2*<e2> + -p3.2*<e2>) + p1.3*<e3> + -p3.3*<e3>
= (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2>
+ (p2.3 + p3.3)*<e3> - p3.1*<e1> - p3.2*<e2> - p3.3*<e3> by RVSUM_1:15;
then (p1.1 - p3.1)*<e1> + (p1.2*<e2> - p3.2*<e2>) + (p1.3*<e3> - p3.3*<e3>)
= (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2>
+ (p2.3 + p3.3)*<e3> - p3.1*<e1> - p3.2*<e2> - p3.3*<e3> by RVSUM_1:15;
then (p1.1 - p3.1)*<e1> + (p1.2 - p3.2)*<e2> + (p1.3*<e3> - p3.3*<e3>)
= (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2>
+ (p2.3 + p3.3)*<e3> - p3.1*<e1> - p3.2*<e2> - p3.3*<e3> by A1;
then (p1.1 - p3.1)*<e1> + (p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>
= (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2>
+ (p2.3 + p3.3)*<e3> - p3.1*<e1> - p3.2*<e2> - p3.3*<e3> by A1;
then (p1.1 - p3.1)*<e1> + (p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>
= (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2>
- p3.1*<e1> + (p2.3 + p3.3)*<e3> - p3.2*<e2> - p3.3*<e3>
by RVSUM_1:15;
then (p1.1 - p3.1)*<e1> + (p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>
= (p2.1 + p3.1)*<e1> - p3.1*<e1> + (p2.2 + p3.2)*<e2>
+ (p2.3 + p3.3)*<e3> - p3.2*<e2> - p3.3*<e3> by RVSUM_1:15;
then (p1.1 - p3.1)*<e1> + (p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>
= (p2.1 + p3.1)*<e1> - p3.1*<e1> + (p2.2 + p3.2)*<e2> - p3.2*<e2>
+ (p2.3 + p3.3)*<e3> - p3.3*<e3> by RVSUM_1:15;
then (p1.1 - p3.1)*<e1> + (p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>
= (p2.1*<e1> + p3.1*<e1> + -p3.1*<e1> + (p2.2 + p3.2)*<e2>- p3.2*<e2>)
+ (p2.3 + p3.3)*<e3> - p3.3*<e3> by RVSUM_1:50;
then (p1.1 - p3.1)*<e1> + (p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>
= p2.1*<e1> + (p3.1*<e1> - p3.1*<e1>) + (p2.2 + p3.2)*<e2> - p3.2*<e2>
+ (p2.3 + p3.3)*<e3> - p3.3*<e3> by RVSUM_1:15;
then (p1.1 - p3.1)*<e1> + (p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>
= p2.1*<e1> + 0.REAL 3 + (p2.2 + p3.2)*<e2> - p3.2*<e2>
+ (p2.3 + p3.3)*<e3> - p3.3*<e3> by EUCLIDLP:2;
then (p1.1 - p3.1)*<e1> + (p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>
= p2.1*<e1> + (p2.2 + p3.2)*<e2> - p3.2*<e2>
+ (p2.3 + p3.3)*<e3> - p3.3*<e3> by EUCLID_4:1;
then (p1.1 - p3.1)*<e1> + (p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>
= p2.1*<e1> + (p2.2*<e2> + p3.2*<e2>) - p3.2*<e2>
+ (p2.3 + p3.3)*<e3> - p3.3*<e3> by RVSUM_1:50;
then (p1.1 - p3.1)*<e1> + (p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>
= (p2.1*<e1> + p2.2*<e2>) + p3.2*<e2> + -p3.2*<e2>
+ (p2.3 + p3.3)*<e3> - p3.3*<e3> by RVSUM_1:15;
then (p1.1 - p3.1)*<e1> + (p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>
= (p2.1*<e1> + p2.2*<e2>) + (p3.2*<e2> + -p3.2*<e2>)
+ (p2.3 + p3.3)*<e3> - p3.3*<e3> by RVSUM_1:15;
then (p1.1 - p3.1)*<e1> + (p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>
= p2.1*<e1> + p2.2*<e2> + 0.REAL 3
+ (p2.3 + p3.3)*<e3> - p3.3*<e3> by EUCLIDLP:2;
then (p1.1 - p3.1)*<e1> + (p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>
= p2.1*<e1> + p2.2*<e2> + (p2.3 + p3.3)*<e3> - p3.3*<e3> by EUCLID_4:1;
then (p1.1 - p3.1)*<e1> + (p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>
= p2.1*<e1> + p2.2*<e2> + (p2.3*<e3> + p3.3*<e3>) - p3.3*<e3>
by RVSUM_1:50;
then (p1.1 - p3.1)*<e1> + (p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>
= p2.1*<e1> + p2.2*<e2> + p2.3*<e3> + p3.3*<e3> - p3.3*<e3>
by RVSUM_1:15;
then (p1.1 - p3.1)*<e1> + (p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>
= p2.1*<e1> + p2.2*<e2> + p2.3*<e3> + (p3.3*<e3> + -p3.3*<e3>)
by RVSUM_1:15;
then (p1.1 - p3.1)*<e1> + (p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>
= p2.1*<e1> + p2.2*<e2> + p2.3*<e3> + 0.REAL 3 by EUCLIDLP:2;
hence thesis by EUCLID_4:1;
end;
now assume
A5: p2.1*<e1> + p2.2*<e2> + p2.3*<e3>
= (p1.1 - p3.1)*<e1> + (p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>;
(p2.1*<e1> + p2.2*<e2> + p2.3*<e3> + p3.1*<e1>) + p3.2*<e2> + p3.3*<e3>
= (p2.1*<e1> + p2.2*<e2> + p2.3*<e3>) + (p3.1*<e1> + p3.2*<e2> + p3.3*<e3>)
proof
A6: (p2.1*<e1>).1 = p2.1*1 by A2,RVSUM_1:44 .= p2.1;
A7: (p2.1*<e1>).2 = p2.1*0 by A2,RVSUM_1:44 .= 0;
A8: (p2.1*<e1>).3 = p2.1*0 by A2,RVSUM_1:44 .= 0;
A9: (p2.2*<e2>).1 = p2.2*<e2>.1 by RVSUM_1:44 .= 0;
A10: (p2.2*<e2>).2 = p2.2*1 by A3,RVSUM_1:44 .= p2.2;
A11: (p2.2*<e2>).3 = p2.2*0 by A3,RVSUM_1:44 .= 0;
A12: (p2.3*<e3>).1 = p2.3*0 by A4,RVSUM_1:44 .= 0;
A13: (p2.3*<e3>).2 = p2.3*0 by A4,RVSUM_1:44 .= 0;
A14: (p2.3*<e3>).3 = p2.3*1 by A4,RVSUM_1:44 .= p2.3;
A15: (p3.1*<e1>).1 = p3.1*1 by A2,RVSUM_1:44 .= p3.1;
A16: (p3.1*<e1>).2 = p3.1*0 by A2,RVSUM_1:44 .= 0;
A17: (p3.1*<e1>).3 = p3.1*0 by A2,RVSUM_1:44 .= 0;
A18: (p3.2*<e2>).1 = p3.2*<e2>.1 by RVSUM_1:44 .= 0;
A19: (p3.2*<e2>).2 = p3.2*1 by A3,RVSUM_1:44 .= p3.2;
A20: (p3.2*<e2>).3 = p3.2*0 by A3,RVSUM_1:44 .= 0;
A21: (p3.3*<e3>).1 = p3.3*0 by A4,RVSUM_1:44 .= 0;
A22: (p3.3*<e3>).2 = p3.3*0 by A4,RVSUM_1:44 .= 0;
A23: (p3.3*<e3>).3 = p3.3*1 by A4,RVSUM_1:44 .= p3.3;
A24: p2.1*<e1> + p2.2*<e2> + p2.3*<e3>
= p2.1*<e1> + (p2.2*<e2> + p2.3*<e3>) by RVSUM_1:15
.= p2.1*<e1> + |[ 0+0, p2.2+0, 0+p2.3 ]| by A9,A10,A11,A12,A13,A14,Lm2
.= |[ p2.1, 0, 0 ]| + |[ 0, p2.2, p2.3 ]| by A6,A7,A8,Th1
.= |[ p2.1+0, 0+p2.2, 0+p2.3 ]| by Lm8
.= |[ p2.1, p2.2, p2.3 ]|;
A25: p3.1*<e1> + p3.2*<e2> + p3.3*<e3>
= p3.1*<e1> + (p3.2*<e2> + p3.3*<e3>) by RVSUM_1:15
.= p3.1*<e1> + |[ 0+0, p3.2+0, 0+p3.3 ]| by A18,A19,A20,A21,A22,A23,Lm2
.= |[ p3.1, 0, 0 ]| + |[ 0, p3.2, p3.3 ]| by A15,A16,A17,Th1
.= |[ p3.1+0, 0+p3.2, 0+p3.3 ]| by Lm8
.= |[ p3.1, p3.2, p3.3 ]|;
(p2.1*<e1> + p2.2*<e2> + p2.3*<e3> + p3.1*<e1>) + p3.2*<e2> + p3.3*<e3>
= p2.1*<e1> + (p2.2*<e2> + p2.3*<e3>) + p3.1*<e1> + p3.2*<e2> + p3.3*<e3>
by RVSUM_1:15
.= p2.1*<e1> + |[ 0+0, p2.2+0, 0+p2.3 ]| + p3.1*<e1> + p3.2*<e2> + p3.3*<e3>
by A9,A10,A11,A12,A13,A14,Lm2
.= |[ p2.1, 0, 0 ]| + |[ 0, p2.2, p2.3 ]| + p3.1*<e1> + p3.2*<e2> + p3.3*<e3>
by A6,A7,A8,Th1
.= |[ p2.1+0, 0+p2.2, 0+p2.3 ]| + p3.1*<e1> + p3.2*<e2> + p3.3*<e3> by Lm8
.= |[ p2.1, p2.2, p2.3 ]| + |[ p3.1, 0, 0 ]| + p3.2*<e2> + p3.3*<e3>
by A15,A16,A17,Th1
.= |[ p2.1+p3.1, p2.2+0, p2.3+0 ]| + p3.2*<e2> + p3.3*<e3> by Lm8
.= |[ p2.1+p3.1, p2.2, p2.3 ]| + |[ 0, p3.2, 0 ]| + p3.3*<e3>
by A18,A19,A20,Th1
.= |[ p2.1+p3.1+0, p2.2+p3.2, p2.3+0 ]| + p3.3*<e3> by Lm8
.= |[ p2.1+p3.1, p2.2+p3.2, p2.3 ]| + |[ 0, 0, p3.3 ]| by A21,A22,A23,Th1
.= |[ p2.1+p3.1+0, p2.2+p3.2+0, p2.3+p3.3 ]| by Lm8;
hence thesis by A24,A25,Lm8;
end;
then (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3>
= (p1.1 - p3.1)*<e1> + (p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>
+ p3.1*<e1> + p3.2*<e2> + p3.3*<e3> by A5,EUCLIDLP:24;
then (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3>
= (p1.1 - p3.1)*<e1> + ((p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>)
+ p3.1*<e1> + p3.2*<e2> + p3.3*<e3> by RVSUM_1:15;
then (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3>
= p1.1*<e1> - p3.1*<e1> + ((p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>)
+ p3.1*<e1> + p3.2*<e2> + p3.3*<e3> by A1;
then (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3>
= p1.1*<e1> + ((p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>) - p3.1*<e1>
+ p3.1*<e1> + p3.2*<e2> + p3.3*<e3> by RVSUM_1:15;
then (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3>
= p1.1*<e1> + ((p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>)
+ (p3.1*<e1> - p3.1*<e1>) + p3.2*<e2> + p3.3*<e3> by RVSUM_1:15;
then (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3>
= p1.1*<e1> + ((p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>)
+ 0.REAL 3 + p3.2*<e2> + p3.3*<e3> by RVSUM_1:37;
then (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3>
= p1.1*<e1> + ((p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>)
+ p3.2*<e2> + p3.3*<e3> by EUCLID_4:1;
then (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3>
= p1.1*<e1> + (p1.2 - p3.2)*<e2> + (p1.3 - p3.3)*<e3>
+ p3.2*<e2> + p3.3*<e3> by RVSUM_1:15;
then (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3>
= p1.1*<e1> + (p1.2 - p3.2)*<e2> + (p1.3*<e3> - p3.3*<e3>)
+ p3.2*<e2> + p3.3*<e3> by A1;
then (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3>
= (p1.1*<e1> + (p1.2 - p3.2)*<e2> + p1.3*<e3> - p3.3*<e3>)
+ p3.2*<e2> + p3.3*<e3> by RVSUM_1:15;
then (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3>
= (p1.1*<e1> + (p1.2 - p3.2)*<e2> + p1.3*<e3> + p3.2*<e2>)
- p3.3*<e3> + p3.3*<e3> by RVSUM_1:15;
then (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3>
= p1.1*<e1> + (p1.2 - p3.2)*<e2> + p1.3*<e3> + p3.2*<e2>
+ (p3.3*<e3> - p3.3*<e3>) by RVSUM_1:15;
then (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3>
= p1.1*<e1> + (p1.2 - p3.2)*<e2> + p1.3*<e3> + p3.2*<e2> + 0.REAL 3
by RVSUM_1:37;
then (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3>
= p1.1*<e1> + (p1.2 - p3.2)*<e2> + p1.3*<e3> + p3.2*<e2> by EUCLID_4:1;
then (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3>
= p1.1*<e1> + (p1.2 - p3.2)*<e2> + (p1.3*<e3> + p3.2*<e2>) by RVSUM_1:15;
then (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3>
= p1.1*<e1> + (p1.2*<e2> - p3.2*<e2>) + (p1.3*<e3> + p3.2*<e2>) by A1;
then (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3>
= p1.1*<e1> + p1.2*<e2> + -p3.2*<e2> + (p1.3*<e3> + p3.2*<e2>)
by RVSUM_1:15;
then (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3>
= p1.1*<e1> + p1.2*<e2> - p3.2*<e2> + p1.3*<e3> + p3.2*<e2>
by RVSUM_1:15;
then (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3>
= p1.1*<e1> + p1.2*<e2> + p1.3*<e3> - p3.2*<e2> + p3.2*<e2>
by RVSUM_1:15;
then (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3>
= p1.1*<e1> + p1.2*<e2> + p1.3*<e3> + (p3.2*<e2> - p3.2*<e2>)
by RVSUM_1:15;
then (p2.1 + p3.1)*<e1> + (p2.2 + p3.2)*<e2> + (p2.3 + p3.3)*<e3>
= p1.1*<e1> + p1.2*<e2> + p1.3*<e3> + 0.REAL 3 by RVSUM_1:37;
hence thesis by EUCLID_4:1;
end;
hence thesis;
end;
definition
let f1,f2,f3 be PartFunc of REAL,REAL;
func VFunc(f1,f2,f3) -> Function of REAL,REAL 3 means :Def5:
for t holds it.t = |[ f1.t,f2.t,f3.t ]|;
existence
proof
defpred P[object,object] means $2 = |[ f1.$1,f2.$1,f3.$1 ]|;
A1: for x being Element of REAL ex y being Element of REAL 3 st P[x,y];
consider F being Function of REAL,REAL 3 such that
A2: for t be Element of REAL holds P[t,F.t] from FUNCT_2:sch 3(A1);
A3: for t be Real holds P[t,F.t]
proof let t be Real;
reconsider t as Element of REAL by XREAL_0:def 1;
P[t,F.t] by A2;
hence thesis;
end;
take F;
thus thesis by A3;
end;
uniqueness
proof
let F,G be Function of REAL,REAL 3;
assume that
A4: for t holds F.t = |[ f1.t,f2.t,f3.t ]| and
A5: for t holds G.t = |[ f1.t,f2.t,f3.t ]|;
now
let t be Element of REAL;
F.t = |[ f1.t,f2.t,f3.t ]| by A4;
hence F.t = G.t by A5;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem
VFunc(f1,f2,f3).t = f1.t*<e1> + f2.t*<e2> + f3.t*<e3>
proof
A1: <e1>.1 = 1 & <e1>.2 = 0 & <e1>.3 = 0;
A2: <e2>.1 = 0 & <e2>.2 = 1 & <e2>.3 = 0;
A3: <e3>.1 = 0 & <e3>.2 = 0 & <e3>.3 = 1;
A4: f1.t*<e1> + f2.t*<e2> + f3.t*<e3>
= |[ f1.t*1,f1.t*0,f1.t*0 ]| + f2.t*<e2> + f3.t*<e3> by A1,Lm1
.= |[ f1.t,0,0 ]| + |[ f2.t*0,f2.t*1,f2.t*0 ]| + f3.t*<e3> by A2,Lm1
.= |[ f1.t,0,0 ]| + |[ 0,f2.t,0 ]| + |[ f3.t*0,f3.t*0,f3.t*1 ]| by A3,Lm1
.= |[ f1.t,0,0 ]| + |[ 0,f2.t,0 ]| + |[ 0,0,f3.t ]|;
A5: |[ f1.t,0,0 ]|.1 = f1.t & |[ f1.t,0,0 ]|.2 = 0 & |[ f1.t,0,0 ]|.3 = 0;
A6: |[ 0,f2.t,0 ]|.1 = 0 & |[ 0,f2.t,0 ]|.2 = f2.t & |[ 0,f2.t,0 ]|.3 = 0;
A7: |[ 0,0,f3.t ]|.1 = 0 & |[ 0,0,f3.t ]|.2 = 0 & |[ 0,0,f3.t ]|.3 = f3.t;
A8: f1.t*<e1> + f2.t*<e2> + f3.t*<e3>
= |[ f1.t+0,0+f2.t,0+0 ]| + |[ 0,0,f3.t ]| by A4,A5,A6,Lm2
.= |[ f1.t,f2.t,0 ]| + |[ 0,0,f3.t ]|;
|[ f1.t,f2.t,0 ]|.1 = f1.t & |[ f1.t,f2.t,0 ]|.2 = f2.t &
|[ f1.t,f2.t,0 ]|.3 = 0;
then f1.t*<e1> + f2.t*<e2> + f3.t*<e3>
= |[ f1.t+0,f2.t+0,0+f3.t ]| by A7,A8,Lm2
.= |[ f1.t,f2.t,f3.t ]|;
hence VFunc(f1,f2,f3).t = f1.t*<e1> + f2.t*<e2> + f3.t*<e3> by Def5;
end;
theorem Th41:
p = VFunc(f1,f2,f3).t iff p.1 = f1.t & p.2 = f2.t & p.3 = f3.t
proof
thus p = VFunc(f1,f2,f3).t implies p.1 = f1.t & p.2 = f2.t & p.3 = f3.t
proof
assume p = VFunc(f1,f2,f3).t;
then p = |[ f1.t,f2.t,f3.t ]| by Def5;
hence thesis;
end;
assume p.1 = f1.t & p.2 = f2.t & p.3 = f3.t;
then p = |[ f1.t,f2.t,f3.t ]| by Th1;
hence p = VFunc(f1,f2,f3).t by Def5;
end;
theorem Th42:
len p = 3 & dom p = Seg 3
proof
p = |[ p.1,p.2,p.3 ]| by Th1;
hence thesis by FINSEQ_1:45,89;
end;
theorem Th43:
mlt(p,q) = <* p.1*q.1, p.2*q.2, p.3*q.3 *>
proof
len p = 3 & len q = 3 by Th42;
hence thesis by EUCLID_5:28;
end;
theorem
r*p = |[ r*p.1, r*p.2, r*p.3 ]| by Lm1;
::$CT
theorem
len(-p) = len p
proof
A1: len p = 3 by Th42;
-p = |[ (-p).1,(-p).2,(-p).3 ]| by Th1;
hence thesis by A1,FINSEQ_1:45;
end;
theorem
p+q = |[ p.1+q.1, p.2+q.2, p.3+q.3 ]| by Lm2;
theorem
(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)
proof
assume
A1: p = VFunc(f1,f2,f3).t1 & q = VFunc(g1,g2,g3).t2 & p = q;
then A2: p.1 = f1.t1 & q.1 = g1.t2 by Th41;
A3: p.2 = f2.t1 & q.2 = g2.t2 by A1,Th41;
p.3 = f3.t1 & q.3 = g3.t2 by A1,Th41;
hence thesis by A1,A2,A3;
end;
theorem
(f1.t1 = g1.t2 & f2.t1 = g2.t2 & f3.t1 = g3.t2) implies
VFunc(f1,f2,f3).t1 = VFunc(g1,g2,g3).t2
proof
assume
A1: f1.t1 = g1.t2 & f2.t1 = g2.t2 & f3.t1 = g3.t2;
set p = |[ f1.t1,f2.t1,f3.t1 ]|;
set q = |[ g1.t2,g2.t2,g3.t2 ]|;
p = VFunc(f1,f2,f3).t1 & q = VFunc(g1,g2,g3).t2 by Def5;
hence thesis by A1;
end;
theorem Th49:
for r being Real holds r*p = |[ r*p.1, r*p.2, r*p.3 ]|
proof
let r be Real;
A1: (r*p).1 = r*(p.1) by RVSUM_1:44;
A2: (r*p).2 = r*(p.2) by RVSUM_1:44;
(r*p).3 = r*(p.3) by RVSUM_1:44;
hence r*p = |[ r*p.1, r*p.2, r*p.3]| by A1,A2,Th1;
end;
theorem Th50:
for r being Real holds r*|[ x,y,z ]| = |[ r*x, r*y, r*z ]|
proof
let r be Real;
set p = |[ x,y,z ]|;
r*p = |[ r*p.1, r*p.2, r*p.3 ]| by Th49
.=|[ r*x, r*p.2, r*p.3 ]|
.=|[ r*x, r*y, r*p.3 ]|
.=|[ r*x, r*y, r*z ]|;
hence thesis;
end;
theorem Th51:
-p = |[ -p.1,-p.2,-p.3 ]|
proof
reconsider r = -1 as Element of REAL by XREAL_0:def 1;
r*p = |[ (-1)*p.1,(-1)*p.2,(-1)*p.3 ]| by Th49
.= |[ -p.1,-p.2,-p.3 ]|;
hence thesis;
end;
theorem Th52:
(-p).1 = -p.1 & (-p).2 = -p.2 & (-p).3 = -p.3
proof
-p = |[ -p.1, -p.2, -p.3 ]| by Th51;
hence thesis;
end;
theorem
p1-p2 = |[ p1.1-p2.1, p1.2-p2.2, p1.3-p2.3 ]|
proof
A1: (-p2).1 = -p2.1 by Th52;
A2: (-p2).2 = -p2.2 by Th52;
(-p2).3 = -p2.3 by Th52;
then p1+-p2 = |[ p1.1+-p2.1, p1.2+-p2.2, p1.3+-p2.3 ]| by A1,A2,Lm2;
hence thesis;
end;
theorem
|(p,q)| = p.1*q.1+p.2*q.2+p.3*q.3 by Lm5;
theorem Th55:
|(p,p)| = (p.1)^2 + (p.2)^2 + (p.3)^2
proof
p = |[ p.1,p.2,p.3 ]| by Th1;
hence thesis by Lm12;
end;
theorem Th56:
|.p.| = sqrt ((p.1)^2+(p.2)^2+(p.3)^2)
proof
|.p.| = sqrt Sum<* p.1*p.1,p.2*p.2,p.3*p.3 *> by Th43
.= sqrt ((p.1)^2+(p.2)^2+(p.3)^2) by RVSUM_1:78;
hence thesis;
end;
theorem
|.r*p.| = |.r.|*(sqrt ((p.1)^2+(p.2)^2+(p.3)^2))
proof
|.r*p.| = |.r.|*|.p.| by EUCLID:11
.= |.r.|*(sqrt ((p.1)^2+(p.2)^2+(p.3)^2)) by Th56;
hence thesis;
end;
theorem
r1*p+r2*p = (r1+r2)*|[ p.1, p.2, p.3 ]|
proof
r1*p+r2*p = (r1+r2)*p by RVSUM_1:50;
hence thesis by Th1;
end;
theorem
|(r*p1,p2)| = r*|(p1,p2)| by RVSUM_1:131;
theorem
r1*p-r2*p = (r1-r2)*|[ p.1, p.2, p.3 ]|
proof
r1*R - r2*R = (r1-r2)*R
proof
r1*R - r2*R = r1*R + ((-1)*r2)*R by RVSUM_1:49
.= (r1 + -r2)*R by RVSUM_1:50;
hence thesis;
end; then
r1*p-r2*p = (r1-r2)*p;
hence thesis by Th1;
end;
theorem
|(r*p,q)| = r*(p.1*q.1+p.2*q.2+p.3*q.3)
proof
|(r*p,q)| = r*|(p,q)| by RVSUM_1:131;
hence thesis by Lm5;
end;
theorem
|(p,0.REAL 3)| = 0
proof
0.REAL 3 = |[ 0,0,0 ]| by FINSEQ_2:62;
hence thesis by Th13;
end;
theorem
|(-p1,p2)| = -|(p1,p2)| by RVSUM_1:132;
theorem
|(-p1,-p2)| = |(p1,p2)| by RVSUM_1:133;
theorem
|(p1-p2,q)| = |(p1,q)| - |(p2,q)| by RVSUM_1:134;
theorem
|(p1+p2,q)| = |(p1,q)|+|(p2,q)| by RVSUM_1:130;
theorem
|(r1*p1+r2*p2,q)| = r1*|(p1,q)| + r2*|(p2,q)| by RVSUM_1:135;
theorem
|(p1+p2,q1+q2)| = |(p1,q1)|+|(p1,q2)|+|(p2,q1)|+|(p2,q2)| by RVSUM_1:136;
theorem
|(p1-p2,q1-q2)| = |(p1,q1)|-|(p1,q2)|-|(p2,q1)|+|(p2,q2)| by RVSUM_1:137;
theorem Th70:
|(p,p)| = 0 iff p = 0.REAL 3
proof
thus |(p,p)|=0 implies p =0.REAL 3
proof
assume |(p,p)|= 0; then
Sum sqr(p) = 0;
hence thesis by RVSUM_1:91;
end;
assume p= 0.REAL 3; then
A1:p = |[ 0,0,0 ]| by FINSEQ_2:62;
then A2:p.1 = 0;
A3:p.2 = 0 by A1;
p.3 = 0 by A1; then
|(p,p)| = 0^2 + 0^2 + 0^2 by A2,A3,Th55;
hence |(p,p)| = 0;
end;
theorem
|.p.| = 0 iff p = 0.REAL 3
proof
thus |.p.| = 0 implies p = 0.REAL 3
proof
assume
A1: |.p.| = 0;
|(p, p)| >= 0 by RVSUM_1:119;
then (sqrt|(p,p)|)^2 = |(p,p)| by SQUARE_1:def 2;
hence thesis by A1,Th70;
end;
assume p = 0.REAL 3; then
A2: p = |[ 0,0,0 ]| by FINSEQ_2:62;
then A3:p.1 = 0;
A4:p.2 = 0 by A2;
p.3 = 0 by A2;
then |(p,p)| = 0^2 + 0^2 + 0^2 by A3,A4,Th55;
hence thesis;
end;
theorem
|(p-q,p-q)| = |(p,p)|-2*|(p,q)|+|(q,q)| by RVSUM_1:139;
theorem
|(p+q,p+q)| = |(p,p)|+2*|(p,q)|+|(q,q)| by RVSUM_1:138;
theorem Th74:
p1<X>p2 = -p2<X>p1
proof
-p2<X>p1 = |[ (-1)*((p2.2*p1.3)-(p2.3*p1.2)),(-1)*((p2.3*p1.1)-(p2.1*p1.3)),
(-1)*((p2.1*p1.2)-(p2.2*p1.1)) ]| by Th50
.= p1<X>p2;
hence thesis;
end;
theorem
|[ x1,x2,x3 ]| <X> |[ y1,y2,y3 ]|
= |[ (x2*y3)-(x3*y2),(x3*y1)-(x1*y3),(x1*y2)-(x2*y1) ]|
proof
set p1 = |[ x1,x2,x3 ]|;
set p2 = |[ y1,y2,y3 ]|;
thus thesis;
end;
theorem
(r*p1)<X>p2 = r*(p1<X>p2) & (r*p1)<X>p2 = p1<X>(r*p2)
proof
A1: (r*p1)<X>p2 = |[ r*p1.1,r*p1.2,r*p1.3 ]|<X>p2 by Th49
.= |[ r*p1.1,r*p1.2,r*p1.3 ]|<X>|[ p2.1,p2.2,p2.3 ]|
.= |[ (r*p1.2*p2.3)-(r*p1.3*p2.2),(r*p1.3*p2.1)-(r*p1.1*p2.3),
(r*p1.1*p2.2)-(r*p1.2*p2.1) ]|; then
A2: (r*p1)<X>p2 = |[ r*((p1.2*p2.3)-(p1.3*p2.2)),r*((p1.3*p2.1)-(p1.1*p2.3)),
r*((p1.1*p2.2)-(p1.2*p2.1)) ]|
.= r*(p1<X>p2) by Th50;
(r*p1)<X>p2 = |[ p1.2*(r*p2.3)-p1.3*(r*p2.2),p1.3*(r*p2.1)-p1.1*(r*p2.3),
p1.1*(r*p2.2)-p1.2*(r*p2.1) ]| by A1
.= |[ p1.1,p1.2,p1.3 ]|<X>|[ r*p2.1,r*p2.2,r*p2.3]|
.= p1<X>|[ r*p2.1,r*p2.2,r*p2.3 ]|
.= p1<X>(r*p2) by Th49;
hence thesis by A2;
end;
theorem Th77:
p1<X>(p2+p3) = (p1<X>p2)+(p1<X>p3)
proof
A1: p2+p3 = |[ p2.1+p3.1, p2.2+p3.2, p2.3+p3.3 ]| by Lm2; then
A2: (p2+p3).1 = p2.1+p3.1;
A3: (p2+p3).2 = p2.2+p3.2 by A1;
A4: (p2+p3).3 = p2.3+p3.3 by A1;
(p1<X>p2)+(p1<X>p3) = |[ (p1.2*p2.3-p1.3*p2.2)+(p1.2*p3.3-p1.3*p3.2),
(p1.3*p2.1-p1.1*p2.3)+(p1.3*p3.1-p1.1*p3.3),
(p1.1*p2.2-p1.2*p2.1)+(p1.1*p3.2-p1.2*p3.1) ]| by Lm8
.= |[ p1.2*p2.3-p1.3*p2.2+p1.2*p3.3-p1.3*p3.2,
p1.3*p2.1-p1.1*p2.3+p1.3*p3.1-p1.1*p3.3,
p1.1*p2.2-p1.2*p2.1+p1.1*p3.2-p1.2*p3.1 ]|;
hence thesis by A2,A3,A4;
end;
theorem Th78:
(p1+p2)<X>p3 = (p1<X>p3)+(p2<X>p3)
proof
(p1+p2)<X>p3 = -(p3<X>(p1+p2)) by Th74
.= -((p3<X>p1)+(p3<X>p2)) by Th77
.= -((p3<X>p1)-(p2<X>p3)) by Th74
.= -(p3<X>p1)+(p2<X>p3) by RVSUM_1:36;
hence thesis by Th74;
end;
theorem
(p1+p2)<X>(q1+q2) = p1<X>q1+p1<X>q2+p2<X>q1+p2<X>q2
proof
(p1+p2)<X>(q1+q2) = (p1<X>(q1+q2))+(p2<X>(q1+q2)) by Th78;
then (p1+p2)<X>(q1+q2) = (p1<X>q1+p1<X>q2)+(p2<X>(q1+q2)) by Th77;
then (p1+p2)<X>(q1+q2) = p1<X>q1+p1<X>q2+(p2<X>q1+p2<X>q2) by Th77;
hence thesis by RVSUM_1:15;
end;
theorem
p1<X>(p2<X>p3) = (|(p1,p3)|*p2)-(|(p1,p2)|*p3)
proof
A1: p2 = |[ p2.1, p2.2, p2.3 ]| by Th1;
A2: p3 = |[ p3.1, p3.2, p3.3 ]| by Th1;
A3: p1<X>(p2<X>p3) = |[(p1.2*p3.2+p1.3*p3.3+p1.1*p3.1)*p2.1-
(p1.2*p2.2+p1.3*p2.3+p1.1*p2.1)*p3.1,
(p1.3*p3.3+p1.1*p3.1+p1.2*p3.2)*p2.2-
(p1.3*p2.3+p1.1*p2.1+p1.2*p2.2)*p3.2,
(p1.1*p3.1+p1.2*p3.2+p1.3*p3.3)*p2.3
-(p1.1*p2.1+p1.2*p2.2+p1.3*p2.3)*p3.3 ]|;
|(p1,p3)| = p1.1*p3.1+p1.2*p3.2+p1.3*p3.3 by Lm5;
then A4: p1<X>(p2<X>p3) = |[ |(p1,p3)|*p2.1, |(p1,p3)|*p2.2, |(p1,p3)|*p2.3 ]|-
|[ (p1.1*p2.1+p1.2*p2.2+p1.3*p2.3)*p3.1,
(p1.1*p2.1+p1.2*p2.2+p1.3*p2.3)*p3.2,
(p1.1*p2.1+p1.2*p2.2+p1.3*p2.3)*p3.3 ]| by A3,Lm11;
|(p1,p2)| = p1.1*p2.1+p1.2*p2.2+p1.3*p2.3 by Lm5;
then p1<X>(p2<X>p3) = (|(p1,p3)|)*|[ p2.1, p2.2, p2.3 ]|-
|[ |(p1,p2)|*p3.1, |(p1,p2)|*p3.2, |(p1,p2)|*p3.3 ]| by A4,Th50;
hence thesis by A1,A2,Th50;
end;
definition let p1,p2,p3;
func |{ p1,p2,p3 }| -> Real equals
|(p1,p2<X>p3)|;
coherence;
end;
theorem
|{ p1,p1,p2 }| = 0
proof
A1:(p1<X>p2).1 = (p1.2*p2.3)-(p1.3*p2.2);
A2:(p1<X>p2).2 = (p1.3*p2.1)-(p1.1*p2.3);
(p1<X>p2).3 = (p1.1*p2.2)-(p1.2*p2.1);
then |{ p1,p1,p2 }| = p1.1*((p1.2*p2.3)-(p1.3*p2.2))
+p1.2*((p1.3*p2.1)-(p1.1*p2.3))
+p1.3*((p1.1*p2.2)-(p1.2*p2.1)) by A2,A1,Lm5
.= 0;
hence thesis;
end;
theorem
|{ p2,p1,p2 }| = 0
proof
A1:(p1<X>p2).1 = (p1.2*p2.3)-(p1.3*p2.2);
A2:(p1<X>p2).2 = (p1.3*p2.1)-(p1.1*p2.3);
(p1<X>p2).3 = (p1.1*p2.2)-(p1.2*p2.1);
then |{ p2,p1,p2 }| = p2.1*((p1.2*p2.3)-(p1.3*p2.2))
+p2.2*((p1.3*p2.1)-(p1.1*p2.3))
+p2.3*((p1.1*p2.2)-(p1.2*p2.1)) by A2,A1,Lm5
.= 0;
hence thesis;
end;
theorem
|{ p1,p2,p2 }| = 0
proof
|{ p1,p2,p2 }| = p1.1*(p2<X>p2).1+p1.2*(p2<X>p2).2+p1.3*(p2<X>p2).3 by Lm5
.= p1.1*((p2.2*p2.3)-(p2.3*p2.2))+p1.2*(p2<X>p2).2+p1.3*(p2<X>p2).3
.= p1.1*((p2.2*p2.3)-(p2.3*p2.2))+p1.2*((p2.3*p2.1)-(p2.1*p2.3))+
p1.3*(p2<X>p2).3
.= (p1.1*(p2.2*p2.3)-p1.1*(p2.3*p2.2))+p1.2*((p2.3*p2.1)-(p2.1*p2.3))+
p1.3*((p2.1*p2.2)-(p2.2*p2.1))
.= 0-p2.2*(p2.1*p2.3)+p2.2*(p2.1*p2.3);
hence thesis;
end;
theorem Th84:
|{ p1,p2,p3 }| = |{ p2,p3,p1 }|
proof
|{ p1,p2,p3 }| = |(|[ p1.1, p1.2, p1.3 ]|, |[ (p2.2*p3.3)-(p2.3*p3.2),
(p2.3*p3.1)-(p2.1*p3.3), (p2.1*p3.2)-(p2.2*p3.1) ]|)| by Th1
.= p1.1*((p2.2*p3.3)-(p2.3*p3.2))+p1.2*((p2.3*p3.1)-(p2.1*p3.3))+
p1.3*((p2.1*p3.2)-(p2.2*p3.1)) by EUCLID_5:30
.= p2.1*(p3.2*p1.3-p3.3*p1.2)+p2.2*(p3.3*p1.1-p3.1*p1.3)+
p2.3*(p3.1*p1.2-p3.2*p1.1)
.= |(|[ p2.1, p2.2, p2.3 ]|,
|[ p3.2*p1.3-p3.3*p1.2, p3.3*p1.1-p3.1*p1.3, p3.1*p1.2-p3.2*p1.1 ]| )|
by EUCLID_5:30
.= |(p2, p3<X>p1)| by Th1;
hence thesis;
end;
theorem
|{ p1,p2,p3 }| = |(p1<X>p2,p3)|
proof
|{ p1,p2,p3 }| = |(|[ p1.1, p1.2, p1.3 ]|,
|[ (p2.2*p3.3)-(p2.3*p3.2),(p2.3*p3.1)-(p2.1*p3.3),
(p2.1*p3.2)-(p2.2*p3.1) ]|)| by Th1
.= p1.1*((p2.2*p3.3)-(p2.3*p3.2))+p1.2*((p2.3*p3.1)-(p2.1*p3.3))+
p1.3*((p2.1*p3.2)-(p2.2*p3.1)) by EUCLID_5:30
.= p2.2*(p1.1*p3.3)-p2.3*(p1.1*p3.2)+(p2.3*(p1.2*p3.1)-
p2.1*(p1.2*p3.3))+(p2.1*(p1.3*p3.2)-p2.2*(p1.3*p3.1));
then |{ p1,p2,p3 }|
= (p2.3*p1.2-p2.2*p1.3)*p3.1+(p2.1*p1.3-p2.3*p1.1)*p3.2+
(p2.2*p1.1-p2.1*p1.2)*p3.3
.= |( p1<X>p2, |[ p3.1, p3.2, p3.3 ]| )| by EUCLID_5:30
.= |( p1<X>p2, p3 )| by Th1;
hence thesis;
end;
theorem
|{ p1,p2,q }| = |(q<X>p1,p2)|
proof
|{ p1,p2,q }| = |{ p2,q,p1 }| by Th84;
hence thesis;
end;
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
|[ diff(f1,t0),diff(f2,t0),diff(f3,t0) ]|;
coherence;
end;
theorem
f1 is_differentiable_in t0 & f2 is_differentiable_in t0 &
f3 is_differentiable_in t0 implies VFuncdiff(f1,f2,f3,t0) =
diff(f1,t0)*<e1>+diff(f2,t0)*<e2>+diff(f3,t0)*<e3> by Th31;
theorem Th88:
(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)
proof
assume that
A1: f1 is_differentiable_in t0 & f2 is_differentiable_in t0 &
f3 is_differentiable_in t0 and
A2: g1 is_differentiable_in t0 & g2 is_differentiable_in t0 &
g3 is_differentiable_in t0;
set p = |[ diff(f1,t0),diff(f2,t0),diff(f3,t0) ]|;
set q = |[ diff(g1,t0),diff(g2,t0),diff(g3,t0) ]|;
VFuncdiff(f1+g1,f2+g2,f3+g3,t0)
= |[ diff(f1,t0)+diff(g1,t0),diff(f2+g2,t0),diff(f3+g3,t0) ]|
by A1,A2,FDIFF_1:13
.= |[ diff(f1,t0)+diff(g1,t0),diff(f2,t0)+diff(g2,t0),diff(f3+g3,t0) ]|
by A1,A2,FDIFF_1:13
.= |[ p.1+q.1,p.2+q.2,p.3+q.3 ]| by A1,A2,FDIFF_1:13
.= VFuncdiff(f1,f2,f3,t0)+VFuncdiff(g1,g2,g3,t0) by Lm2;
hence thesis;
end;
theorem Th89:
(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)
proof
assume that
A1: f1 is_differentiable_in t0 & f2 is_differentiable_in t0 &
f3 is_differentiable_in t0 and
A2: g1 is_differentiable_in t0 & g2 is_differentiable_in t0 &
g3 is_differentiable_in t0;
set p = |[ diff(f1,t0),diff(f2,t0),diff(f3,t0) ]|;
set q = |[ diff(g1,t0),diff(g2,t0),diff(g3,t0) ]|;
VFuncdiff(f1-g1,f2-g2,f3-g3,t0)
= |[ diff(f1,t0)-diff(g1,t0),diff(f2-g2,t0),diff(f3-g3,t0) ]|
by A1,A2,FDIFF_1:14
.= |[ diff(f1,t0)-diff(g1,t0),diff(f2,t0)-diff(g2,t0),diff(f3-g3,t0) ]|
by A1,A2,FDIFF_1:14
.= |[ p.1-q.1,p.2-q.2,p.3-q.3 ]| by A1,A2,FDIFF_1:14
.= VFuncdiff(f1,f2,f3,t0)-VFuncdiff(g1,g2,g3,t0) by Lm4;
hence thesis;
end;
theorem Th90:
(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)
proof
assume
A1: f1 is_differentiable_in t0 & f2 is_differentiable_in t0 &
f3 is_differentiable_in t0;
set p = |[ diff(f1,t0),diff(f2,t0),diff(f3,t0) ]|;
VFuncdiff(r(#)f1,r(#)f2,r(#)f3,t0)
= |[ r*diff(f1,t0),diff(r(#)f2,t0),diff(r(#)f3,t0) ]| by A1,FDIFF_1:15
.= |[ r*diff(f1,t0),r*diff(f2,t0),diff(r(#)f3,t0) ]| by A1,FDIFF_1:15
.= |[ r*p.1,r*p.2,r*p.3 ]| by A1,FDIFF_1:15
.= r*VFuncdiff(f1,f2,f3,t0) by Lm1;
hence thesis;
end;
theorem Th91:
(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) ]|
proof
assume that
A1: f1 is_differentiable_in t0 & f2 is_differentiable_in t0 &
f3 is_differentiable_in t0 and
A2: g1 is_differentiable_in t0 & g2 is_differentiable_in t0 &
g3 is_differentiable_in t0;
set p = |[ (g1.t0)*diff(f1,t0),(g2.t0)*diff(f2,t0),(g3.t0)*diff(f3,t0) ]|;
set q = |[ (f1.t0)*diff(g1,t0),(f2.t0)*diff(g2,t0),(f3.t0)*diff(g3,t0) ]|;
VFuncdiff(f1(#)g1,f2(#)g2,f3(#)g3,t0)
= |[ (g1.t0)*diff(f1,t0)+(f1.t0)*diff(g1,t0),diff(f2(#)g2,t0),
diff(f3(#)g3,t0) ]| by A1,A2,FDIFF_1:16
.= |[ (g1.t0)*diff(f1,t0)+(f1.t0)*diff(g1,t0),
(g2.t0)*diff(f2,t0)+(f2.t0)*diff(g2,t0),diff(f3(#)g3,t0) ]|
by A1,A2,FDIFF_1:16
.= |[ p.1+q.1,p.2+q.2,p.3+q.3 ]| by A1,A2,FDIFF_1:16
.= |[ (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) ]|
by Lm2;
hence thesis;
end;
theorem Th92:
(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) ]|
proof
assume that
A1: f1 is_differentiable_in t0 & f2 is_differentiable_in t0 &
f3 is_differentiable_in t0 and
A2: g1 is_differentiable_in f1.t0 & g2 is_differentiable_in f2.t0 &
g3 is_differentiable_in f3.t0;
VFuncdiff(g1*f1,g2*f2,g3*f3,t0)
= |[ diff(g1,f1.t0)*diff(f1,t0),diff(g2*f2,t0),diff(g3*f3,t0) ]|
by A1,A2,FDIFF_2:13
.= |[ diff(g1,f1.t0)*diff(f1,t0),diff(g2,f2.t0)*diff(f2,t0),
diff(g3*f3,t0) ]| by A1,A2,FDIFF_2:13
.= |[ diff(g1,f1.t0)*diff(f1,t0),diff(g2,f2.t0)*diff(f2,t0),
diff(g3,f3.t0)*diff(f3,t0) ]| by A1,A2,FDIFF_2:13;
hence thesis;
end;
theorem
(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 ]|
proof
assume that
A1: f1 is_differentiable_in t0 & f2 is_differentiable_in t0 &
f3 is_differentiable_in t0 and
A2: g1 is_differentiable_in t0 & g2 is_differentiable_in t0 &
g3 is_differentiable_in t0 and
A3: g1.t0 <> 0 & g2.t0 <> 0 & g3.t0 <> 0;
VFuncdiff(f1/g1,f2/g2,f3/g3,t0)
= |[ (diff(f1,t0)*(g1.t0)-diff(g1,t0)*(f1.t0))/(g1.t0)^2,
diff(f2/g2,t0),diff(f3/g3,t0) ]| by A1,A2,A3,FDIFF_2:14
.= |[ (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/g3,t0) ]| by A1,A2,A3,FDIFF_2:14
.= |[ (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 ]|
by A1,A2,A3,FDIFF_2:14;
hence thesis;
end;
theorem Th94:
(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 ]|
proof
assume that
A1: f1 is_differentiable_in t0 & f2 is_differentiable_in t0 &
f3 is_differentiable_in t0 and
A2: f1.t0 <> 0 & f2.t0 <> 0 & f3.t0 <> 0;
set p = |[ diff(f1,t0)/(f1.t0)^2,diff(f2,t0)/(f2.t0)^2,
diff(f3,t0)/(f3.t0)^2 ]|;
VFuncdiff(f1^,f2^,f3^,t0)
= |[ -diff(f1,t0)/(f1.t0)^2,diff(f2^,t0),diff(f3^,t0) ]|
by A1,A2,FDIFF_2:15
.= |[ -diff(f1,t0)/(f1.t0)^2,-diff(f2,t0)/(f2.t0)^2,diff(f3^,t0) ]|
by A1,A2,FDIFF_2:15
.= |[ -diff(f1,t0)/(f1.t0)^2,-diff(f2,t0)/(f2.t0)^2,
-diff(f3,t0)/(f3.t0)^2 ]| by A1,A2,FDIFF_2:15
.= |[ (-1)*p.1,(-1)*p.2,(-1)*p.3 ]|
.= - |[ diff(f1,t0)/(f1.t0)^2,diff(f2,t0)/(f2.t0)^2,
diff(f3,t0)/(f3.t0)^2 ]| by Lm1;
hence thesis;
end;
theorem
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)*<e1>
+r*diff(f2,t0)*<e2>+r*diff(f3,t0)*<e3>
proof
assume f1 is_differentiable_in t0 &
f2 is_differentiable_in t0 & f3 is_differentiable_in t0;
then VFuncdiff(r(#)f1,r(#)f2,r(#)f3,t0) = r*VFuncdiff(f1,f2,f3,t0) by Th90
.= r*( diff(f1,t0)*<e1>+diff(f2,t0)*<e2>
+diff(f3,t0)*<e3> ) by Th31
.= r*( |[ diff(f1,t0),0,0 ]|+diff(f2,t0)*<e2>
+diff(f3,t0)*<e3> ) by Th21
.= r*( |[ diff(f1,t0),0,0 ]|+|[ 0,diff(f2,t0),0 ]|
+diff(f3,t0)*<e3> ) by Th22
.= r*( (|[ diff(f1,t0),0,0 ]|+|[ 0,diff(f2,t0),0 ]|)
+|[ 0,0,diff(f3,t0) ]| ) by Th23
.= r*( |[ diff(f1,t0)+0,0+diff(f2,t0),0+0 ]|
+|[ 0,0,diff(f3,t0) ]| ) by Lm8
.= r*|[ diff(f1,t0)+0,diff(f2,t0)+0,0+diff(f3,t0) ]| by Lm8
.= r*diff(f1,t0)*<e1>+r*diff(f2,t0)*<e2>
+r*diff(f3,t0)*<e3> by Th32;
hence thesis;
end;
theorem
(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)
proof
assume that
A1: f1 is_differentiable_in t0 & f2 is_differentiable_in t0 &
f3 is_differentiable_in t0 and
A2: g1 is_differentiable_in t0 & g2 is_differentiable_in t0 &
g3 is_differentiable_in t0;
f1+g1 is_differentiable_in t0 & f2+g2 is_differentiable_in t0 &
f3+g3 is_differentiable_in t0 by A1,A2,FDIFF_1:13;
then VFuncdiff(r(#)(f1+g1),r(#)(f2+g2),r(#)(f3+g3),t0)
= r*VFuncdiff(f1+g1,f2+g2,f3+g3,t0) by Th90
.= r*(VFuncdiff(f1,f2,f3,t0)+VFuncdiff(g1,g2,g3,t0)) by A1,A2,Th88
.= r*VFuncdiff(f1,f2,f3,t0)+r*VFuncdiff(g1,g2,g3,t0) by EUCLID_4:6;
hence thesis;
end;
theorem
(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)
proof
assume that
A1: f1 is_differentiable_in t0 & f2 is_differentiable_in t0 &
f3 is_differentiable_in t0 and
A2: g1 is_differentiable_in t0 & g2 is_differentiable_in t0 &
g3 is_differentiable_in t0;
f1-g1 is_differentiable_in t0 & f2-g2 is_differentiable_in t0 &
f3-g3 is_differentiable_in t0 by A1,A2,FDIFF_1:14;
then VFuncdiff(r(#)(f1-g1),r(#)(f2-g2),r(#)(f3-g3),t0)
= r*VFuncdiff(f1-g1,f2-g2,f3-g3,t0) by Th90
.= r*(VFuncdiff(f1,f2,f3,t0)-VFuncdiff(g1,g2,g3,t0)) by A1,A2,Th89
.= r*VFuncdiff(f1,f2,f3,t0)-r*VFuncdiff(g1,g2,g3,t0) by EUCLIDLP:12;
hence thesis;
end;
theorem
(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) ]|
proof
assume that
A1: f1 is_differentiable_in t0 & f2 is_differentiable_in t0 &
f3 is_differentiable_in t0 and
A2: g1 is_differentiable_in t0 & g2 is_differentiable_in t0 &
g3 is_differentiable_in t0;
r(#)f1 is_differentiable_in t0 & r(#)f2 is_differentiable_in t0 &
r(#)f3 is_differentiable_in t0 by A1,FDIFF_1:15;
then VFuncdiff(r(#)f1(#)g1,r(#)f2(#)g2,r(#)f3(#)g3,t0)
= |[ (g1.t0)*diff(r(#)f1,t0),(g2.t0)*diff(r(#)f2,t0),
(g3.t0)*diff(r(#)f3,t0) ]|+
|[ ((r(#)f1).t0)*diff(g1,t0),((r(#)f2).t0)*diff(g2,t0),
((r(#)f3).t0)*diff(g3,t0) ]| by A2,Th91
.= |[ (g1.t0)*(r*diff(f1,t0)),(g2.t0)*diff(r(#)f2,t0),
(g3.t0)*diff(r(#)f3,t0) ]|+
|[ ((r(#)f1).t0)*diff(g1,t0),((r(#)f2).t0)*diff(g2,t0),
((r(#)f3).t0)*diff(g3,t0) ]| by A1,FDIFF_1:15
.= |[ (g1.t0)*(r*diff(f1,t0)),(g2.t0)*(r*diff(f2,t0)),
(g3.t0)*diff(r(#)f3,t0) ]|+
|[ ((r(#)f1).t0)*diff(g1,t0),((r(#)f2).t0)*diff(g2,t0),
((r(#)f3).t0)*diff(g3,t0) ]| by A1,FDIFF_1:15
.= |[ (g1.t0)*(r*diff(f1,t0)),(g2.t0)*(r*diff(f2,t0)),
(g3.t0)*(r*diff(f3,t0)) ]|+
|[ ((r(#)f1).t0)*diff(g1,t0),((r(#)f2).t0)*diff(g2,t0),
((r(#)f3).t0)*diff(g3,t0) ]| by A1,FDIFF_1:15
.= |[ (g1.t0)*(r*diff(f1,t0)),(g2.t0)*(r*diff(f2,t0)),
(g3.t0)*(r*diff(f3,t0)) ]|+
|[ (r*f1.t0)*diff(g1,t0),((r(#)f2).t0)*diff(g2,t0),
((r(#)f3).t0)*diff(g3,t0) ]| by VALUED_1:6
.= |[ (g1.t0)*(r*diff(f1,t0)),(g2.t0)*(r*diff(f2,t0)),
(g3.t0)*(r*diff(f3,t0)) ]|+
|[ (r*f1.t0)*diff(g1,t0),(r*f2.t0)*diff(g2,t0),
((r(#)f3).t0)*diff(g3,t0) ]| by VALUED_1:6
.= |[ (g1.t0)*(r*diff(f1,t0)),(g2.t0)*(r*diff(f2,t0)),
(g3.t0)*(r*diff(f3,t0)) ]|+
|[ r*(f1.t0)*diff(g1,t0),r*(f2.t0)*diff(g2,t0),
r*(f3.t0)*diff(g3,t0) ]| by VALUED_1:6
.= |[ (g1.t0)*(r*diff(f1,t0)),(g2.t0)*(r*diff(f2,t0)),
(g3.t0)*(r*diff(f3,t0)) ]|+
|[ r*((f1.t0)*diff(g1,t0)),r*((f2.t0)*diff(g2,t0)),
r*((f3.t0)*diff(g3,t0)) ]|
.= |[ r*((g1.t0)*diff(f1,t0)),r*((g2.t0)*diff(f2,t0)),
r*((g3.t0)*diff(f3,t0)) ]|+
r*|[ (f1.t0)*diff(g1,t0),(f2.t0)*diff(g2,t0),
(f3.t0)*diff(g3,t0) ]| by Lm6
.= 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) ]| by Lm6;
hence thesis;
end;
theorem
(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) ]|
proof
assume that
A1: f1 is_differentiable_in t0 & f2 is_differentiable_in t0 &
f3 is_differentiable_in t0 and
A2: g1 is_differentiable_in f1.t0 & g2 is_differentiable_in f2.t0 &
g3 is_differentiable_in f3.t0;
r(#)g1 is_differentiable_in f1.t0 & r(#)g2 is_differentiable_in f2.t0 &
r(#)g3 is_differentiable_in f3.t0 by A2,FDIFF_1:15;
then VFuncdiff(r(#)g1*f1,r(#)g2*f2,r(#)g3*f3,t0)
= |[ diff(r(#)g1,f1.t0)*diff(f1,t0),diff(r(#)g2,f2.t0)*diff(f2,t0),
diff(r(#)g3,f3.t0)*diff(f3,t0) ]| by A1,Th92
.= |[ r*diff(g1,f1.t0)*diff(f1,t0),diff(r(#)g2,f2.t0)*diff(f2,t0),
diff(r(#)g3,f3.t0)*diff(f3,t0) ]| by A2,FDIFF_1:15
.= |[ r*diff(g1,f1.t0)*diff(f1,t0),r*diff(g2,f2.t0)*diff(f2,t0),
diff(r(#)g3,f3.t0)*diff(f3,t0) ]| by A2,FDIFF_1:15
.= |[ r*diff(g1,f1.t0)*diff(f1,t0),r*diff(g2,f2.t0)*diff(f2,t0),
r*diff(g3,f3.t0)*diff(f3,t0) ]| by A2,FDIFF_1:15
.= |[ r*(diff(g1,f1.t0)*diff(f1,t0)),r*(diff(g2,f2.t0)*diff(f2,t0)),
r*(diff(g3,f3.t0)*diff(f3,t0)) ]|
.= r*|[ diff(g1,f1.t0)*diff(f1,t0),diff(g2,f2.t0)*diff(f2,t0),
diff(g3,f3.t0)*diff(f3,t0) ]| by Lm6;
hence thesis;
end;
theorem
(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 ]|
proof
assume that
A1: f1 is_differentiable_in t0 & f2 is_differentiable_in t0 &
f3 is_differentiable_in t0 and
A2: g1 is_differentiable_in t0 & g2 is_differentiable_in t0 &
g3 is_differentiable_in t0 and
A3: g1.t0 <> 0 & g2.t0 <> 0 & g3.t0 <> 0;
A4: r(#)f1 is_differentiable_in t0 & r(#)f2 is_differentiable_in t0 &
r(#)f3 is_differentiable_in t0 by A1,FDIFF_1:15;
then VFuncdiff(r(#)f1/g1,r(#)f2/g2,r(#)f3/g3,t0)
= |[ (diff(r(#)f1,t0)*(g1.t0)-diff(g1,t0)*((r(#)f1).t0))/(g1.t0)^2,
diff((r(#)f2)/g2,t0),diff((r(#)f3)/g3,t0) ]|
by A2,A3,FDIFF_2:14
.= |[ (diff(r(#)f1,t0)*(g1.t0)-diff(g1,t0)*((r(#)f1).t0))/(g1.t0)^2,
(diff(r(#)f2,t0)*(g2.t0)-diff(g2,t0)*((r(#)f2).t0))/(g2.t0)^2,
diff((r(#)f3)/g3,t0) ]| by A2,A3,A4,FDIFF_2:14
.= |[ (diff(r(#)f1,t0)*(g1.t0)-diff(g1,t0)*((r(#)f1).t0))/(g1.t0)^2,
(diff(r(#)f2,t0)*(g2.t0)-diff(g2,t0)*((r(#)f2).t0))/(g2.t0)^2,
(diff(r(#)f3,t0)*(g3.t0)-diff(g3,t0)*((r(#)f3).t0))/(g3.t0)^2 ]|
by A2,A3,A4,FDIFF_2:14
.= |[ (r*diff(f1,t0)*(g1.t0)-diff(g1,t0)*((r(#)f1).t0))/(g1.t0)^2,
(diff(r(#)f2,t0)*(g2.t0)-diff(g2,t0)*((r(#)f2).t0))/(g2.t0)^2,
(diff(r(#)f3,t0)*(g3.t0)-diff(g3,t0)*((r(#)f3).t0))/(g3.t0)^2 ]|
by A1,FDIFF_1:15
.= |[ (r*diff(f1,t0)*(g1.t0)-diff(g1,t0)*((r(#)f1).t0))/(g1.t0)^2,
(r*diff(f2,t0)*(g2.t0)-diff(g2,t0)*((r(#)f2).t0))/(g2.t0)^2,
(diff(r(#)f3,t0)*(g3.t0)-diff(g3,t0)*((r(#)f3).t0))/(g3.t0)^2 ]|
by A1,FDIFF_1:15
.= |[ (r*diff(f1,t0)*(g1.t0)-diff(g1,t0)*((r(#)f1).t0))/(g1.t0)^2,
(r*diff(f2,t0)*(g2.t0)-diff(g2,t0)*((r(#)f2).t0))/(g2.t0)^2,
(r*diff(f3,t0)*(g3.t0)-diff(g3,t0)*((r(#)f3).t0))/(g3.t0)^2 ]|
by A1,FDIFF_1:15
.= |[ (r*diff(f1,t0)*(g1.t0)-diff(g1,t0)*(r*f1.t0))/(g1.t0)^2,
(r*diff(f2,t0)*(g2.t0)-diff(g2,t0)*((r(#)f2).t0))/(g2.t0)^2,
(r*diff(f3,t0)*(g3.t0)-diff(g3,t0)*((r(#)f3).t0))/(g3.t0)^2 ]|
by VALUED_1:6
.= |[ (r*diff(f1,t0)*(g1.t0)-diff(g1,t0)*(r*f1.t0))/(g1.t0)^2,
(r*diff(f2,t0)*(g2.t0)-diff(g2,t0)*(r*f2.t0))/(g2.t0)^2,
(r*diff(f3,t0)*(g3.t0)-diff(g3,t0)*((r(#)f3).t0))/(g3.t0)^2 ]|
by VALUED_1:6
.= |[ (r*diff(f1,t0)*(g1.t0)-diff(g1,t0)*(r*f1.t0))/(g1.t0)^2,
(r*diff(f2,t0)*(g2.t0)-diff(g2,t0)*(r*f2.t0))/(g2.t0)^2,
(r*diff(f3,t0)*(g3.t0)-diff(g3,t0)*(r*f3.t0))/(g3.t0)^2 ]|
by VALUED_1:6
.= |[ (r*(diff(f1,t0)*(g1.t0)-diff(g1,t0)*(f1.t0)))/(g1.t0)^2,
(r*(diff(f2,t0)*(g2.t0)-diff(g2,t0)*(f2.t0)))/(g2.t0)^2,
(r*(diff(f3,t0)*(g3.t0)-diff(g3,t0)*(f3.t0)))/(g3.t0)^2 ]|
.= |[ r*((diff(f1,t0)*(g1.t0)-diff(g1,t0)*(f1.t0))/(g1.t0)^2),
(r*(diff(f2,t0)*(g2.t0)-diff(g2,t0)*(f2.t0)))/(g2.t0)^2,
(r*(diff(f3,t0)*(g3.t0)-diff(g3,t0)*(f3.t0)))/(g3.t0)^2 ]|
by XCMPLX_1:74
.= |[ r*((diff(f1,t0)*(g1.t0)-diff(g1,t0)*(f1.t0))/(g1.t0)^2),
r*((diff(f2,t0)*(g2.t0)-diff(g2,t0)*(f2.t0))/(g2.t0)^2),
(r*(diff(f3,t0)*(g3.t0)-diff(g3,t0)*(f3.t0)))/(g3.t0)^2 ]|
by XCMPLX_1:74
.= |[ r*((diff(f1,t0)*(g1.t0)-diff(g1,t0)*(f1.t0))/(g1.t0)^2),
r*((diff(f2,t0)*(g2.t0)-diff(g2,t0)*(f2.t0))/(g2.t0)^2),
r*((diff(f3,t0)*(g3.t0)-diff(g3,t0)*(f3.t0))/(g3.t0)^2) ]|
by XCMPLX_1:74
.= 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 ]| by Lm6;
hence thesis;
end;
theorem
(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 ]|
proof
assume that
A1: f1 is_differentiable_in t0 & f2 is_differentiable_in t0 &
f3 is_differentiable_in t0 and
A2: f1.t0 <> 0 & f2.t0 <> 0 & f3.t0 <> 0 and
A3: r <> 0;
A4: r(#)f1 is_differentiable_in t0 & r(#)f2 is_differentiable_in t0 &
r(#)f3 is_differentiable_in t0 by A1,FDIFF_1:15;
A5: (r(#)f1).t0 = r*(f1.t0) by VALUED_1:6;
A6: (r(#)f2).t0 = r*(f2.t0) by VALUED_1:6;
A7: (r(#)f3).t0 = r*(f3.t0) by VALUED_1:6;
then VFuncdiff(r(#)f1^,r(#)f2^,r(#)f3^,t0)
= - |[ diff(r(#)f1,t0)/((r(#)f1).t0)^2,diff(r(#)f2,t0)/((r(#)f2).t0)^2,
diff(r(#)f3,t0)/((r(#)f3).t0)^2 ]|
by A4,A5,A6,A2,A3,Th94
.= - |[ r*diff(f1,t0)/((r(#)f1).t0)^2,diff(r(#)f2,t0)/((r(#)f2).t0)^2,
diff(r(#)f3,t0)/((r(#)f3).t0)^2 ]| by A1,FDIFF_1:15
.= - |[ r*diff(f1,t0)/((r(#)f1).t0)^2,r*diff(f2,t0)/((r(#)f2).t0)^2,
diff(r(#)f3,t0)/((r(#)f3).t0)^2 ]| by A1,FDIFF_1:15
.= - |[ (r*diff(f1,t0))/((r(#)f1).t0)^2,(r*diff(f2,t0))/((r(#)f2).t0)^2,
(r*diff(f3,t0))/((r(#)f3).t0)^2 ]| by A1,FDIFF_1:15
.= - |[ r*(diff(f1,t0)/((r(#)f1).t0)^2),(r*diff(f2,t0))/((r(#)f2).t0)^2,
(r*diff(f3,t0))/((r(#)f3).t0)^2 ]| by XCMPLX_1:74
.= - |[ r*(diff(f1,t0)/((r(#)f1).t0)^2),r*(diff(f2,t0)/((r(#)f2).t0)^2),
(r*diff(f3,t0))/((r(#)f3).t0)^2 ]| by XCMPLX_1:74
.= - |[ r*(diff(f1,t0)/((r(#)f1).t0)^2),r*(diff(f2,t0)/((r(#)f2).t0)^2),
r*(diff(f3,t0)/((r(#)f3).t0)^2) ]| by XCMPLX_1:74
.= - r*|[ diff(f1,t0)/(r^2*(f1.t0)^2),diff(f2,t0)/(r^2*(f2.t0)^2),
diff(f3,t0)/(r^2*(f3.t0)^2) ]| by A7,A6,A5,Lm6
.= - r*|[ diff(f1,t0)/r^2/(f1.t0)^2,diff(f2,t0)/(r^2*(f2.t0)^2),
diff(f3,t0)/(r^2*(f3.t0)^2) ]| by XCMPLX_1:78
.= - r*|[ diff(f1,t0)/r^2/(f1.t0)^2,diff(f2,t0)/r^2/(f2.t0)^2,
diff(f3,t0)/(r^2*(f3.t0)^2) ]| by XCMPLX_1:78
.= - r*|[ diff(f1,t0)/r^2/(f1.t0)^2,diff(f2,t0)/r^2/(f2.t0)^2,
diff(f3,t0)/r^2/(f3.t0)^2 ]| by XCMPLX_1:78
.= - r*|[ diff(f1,t0)/(f1.t0)^2/r^2,diff(f2,t0)/r^2/(f2.t0)^2,
diff(f3,t0)/r^2/(f3.t0)^2 ]| by XCMPLX_1:48
.= - r*|[ diff(f1,t0)/(f1.t0)^2/r^2,diff(f2,t0)/(f2.t0)^2/r^2,
diff(f3,t0)/r^2/(f3.t0)^2 ]| by XCMPLX_1:48
.= - r*|[ diff(f1,t0)/(f1.t0)^2/r^2,diff(f2,t0)/(f2.t0)^2/r^2,
diff(f3,t0)/(f3.t0)^2/r^2 ]| by XCMPLX_1:48
.= - r*|[ (diff(f1,t0)/(f1.t0)^2)/(1/r^2)",diff(f2,t0)/(f2.t0)^2/r^2,
diff(f3,t0)/(f3.t0)^2/r^2 ]| by XCMPLX_1:217
.= - r*|[ (1/r^2)*(diff(f1,t0)/(f1.t0)^2),diff(f2,t0)/(f2.t0)^2/r^2,
diff(f3,t0)/(f3.t0)^2/r^2 ]| by XCMPLX_1:219
.= - r*|[ (1/r^2)*(diff(f1,t0)/(f1.t0)^2),(diff(f2,t0)/(f2.t0)^2)/(1/r^2)",
diff(f3,t0)/(f3.t0)^2/r^2 ]| by XCMPLX_1:217
.= - r*|[ (1/r^2)*(diff(f1,t0)/(f1.t0)^2),(1/r^2)*(diff(f2,t0)/(f2.t0)^2),
diff(f3,t0)/(f3.t0)^2/r^2 ]| by XCMPLX_1:219
.= - r*|[ (1/r^2)*(diff(f1,t0)/(f1.t0)^2),(1/r^2)*(diff(f2,t0)/(f2.t0)^2),
diff(f3,t0)/(f3.t0)^2/(1/r^2)" ]| by XCMPLX_1:217
.= - r*|[ (1/r^2)*(diff(f1,t0)/(f1.t0)^2),(1/r^2)*(diff(f2,t0)/(f2.t0)^2),
(1/r^2)*(diff(f3,t0)/(f3.t0)^2) ]| by XCMPLX_1:219
.= - r*((1/r^2)*|[ diff(f1,t0)/(f1.t0)^2,diff(f2,t0)/(f2.t0)^2,
diff(f3,t0)/(f3.t0)^2 ]|) by Lm6
.= - (r*(1/r^2))*|[ diff(f1,t0)/(f1.t0)^2,diff(f2,t0)/(f2.t0)^2,
diff(f3,t0)/(f3.t0)^2 ]| by EUCLID_4:4
.= - ((r*1)/r^2)*|[ diff(f1,t0)/(f1.t0)^2,diff(f2,t0)/(f2.t0)^2,
diff(f3,t0)/(f3.t0)^2 ]| by XCMPLX_1:74
.= - (r/r/r)*|[ diff(f1,t0)/(f1.t0)^2,diff(f2,t0)/(f2.t0)^2,
diff(f3,t0)/(f3.t0)^2 ]| by XCMPLX_1:78
.= - (1/r)*|[ diff(f1,t0)/(f1.t0)^2,diff(f2,t0)/(f2.t0)^2,
diff(f3,t0)/(f3.t0)^2 ]| by A3,XCMPLX_1:60;
hence thesis;
end;
theorem
(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) ]|
proof
assume that
A1: f1 is_differentiable_in t0 & f2 is_differentiable_in t0 &
f3 is_differentiable_in t0 and
A2: g1 is_differentiable_in t0 & g2 is_differentiable_in t0 &
g3 is_differentiable_in t0;
f2(#)g3 is_differentiable_in t0 & f3(#)g2 is_differentiable_in t0 &
f3(#)g1 is_differentiable_in t0 &
f1(#)g3 is_differentiable_in t0 &
f1(#)g2 is_differentiable_in t0 &
f2(#)g1 is_differentiable_in t0 by A1,A2,FDIFF_1:16;
then VFuncdiff( f2(#)g3-f3(#)g2,f3(#)g1-f1(#)g3, f1(#)g2-f2(#)g1,t0 )
= VFuncdiff( f2(#)g3,f3(#)g1,f1(#)g2,t0 )
- VFuncdiff( f3(#)g2,f1(#)g3,f2(#)g1,t0 ) by Th89
.= (|[ (g3.t0)*diff(f2,t0),(g1.t0)*diff(f3,t0),
(g2.t0)*diff(f1,t0) ]|+
|[ (f2.t0)*diff(g3,t0),(f3.t0)*diff(g1,t0),
(f1.t0)*diff(g2,t0) ]|)-
VFuncdiff( f3(#)g2,f1(#)g3,f2(#)g1,t0 ) by A1,A2,Th91
.= (|[ (g3.t0)*diff(f2,t0),(g1.t0)*diff(f3,t0),
(g2.t0)*diff(f1,t0) ]|+
|[ (f2.t0)*diff(g3,t0),(f3.t0)*diff(g1,t0),
(f1.t0)*diff(g2,t0) ]|)-
(|[ (g2.t0)*diff(f3,t0),(g3.t0)*diff(f1,t0),
(g1.t0)*diff(f2,t0) ]|+
|[ (f3.t0)*diff(g2,t0),(f1.t0)*diff(g3,t0),
(f2.t0)*diff(g1,t0) ]|) by A1,A2,Th91
.= (|[ (g3.t0)*diff(f2,t0),(g1.t0)*diff(f3,t0),
(g2.t0)*diff(f1,t0) ]|-
|[ (g2.t0)*diff(f3,t0),(g3.t0)*diff(f1,t0),
(g1.t0)*diff(f2,t0) ]|)+
(|[ (f2.t0)*diff(g3,t0),(f3.t0)*diff(g1,t0),
(f1.t0)*diff(g2,t0) ]|-
|[ (f3.t0)*diff(g2,t0),(f1.t0)*diff(g3,t0),
(f2.t0)*diff(g1,t0) ]|) by Lm10
.= (|[ (g3.t0)*diff(f2,t0)-(g2.t0)*diff(f3,t0),
(g1.t0)*diff(f3,t0)-(g3.t0)*diff(f1,t0),
(g2.t0)*diff(f1,t0)-(g1.t0)*diff(f2,t0) ]|)+
(|[ (f2.t0)*diff(g3,t0),(f3.t0)*diff(g1,t0),
(f1.t0)*diff(g2,t0) ]|-
|[ (f3.t0)*diff(g2,t0),(f1.t0)*diff(g3,t0),
(f2.t0)*diff(g1,t0) ]|) by Lm11
.= |[ (g3.t0)*diff(f2,t0)-(g2.t0)*diff(f3,t0),
(g1.t0)*diff(f3,t0)-(g3.t0)*diff(f1,t0),
(g2.t0)*diff(f1,t0)-(g1.t0)*diff(f2,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) ]| by Lm11;
hence thesis;
end;
::p37-4(5.1) A*(BXC)
theorem
(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)) ]|
proof
assume that
A1: f1 is_differentiable_in t0 & f2 is_differentiable_in t0 &
f3 is_differentiable_in t0 and
A2: g1 is_differentiable_in t0 & g2 is_differentiable_in t0 &
g3 is_differentiable_in t0 and
A3: h1 is_differentiable_in t0 & h2 is_differentiable_in t0 &
h3 is_differentiable_in t0;
A4: f2(#)g3 is_differentiable_in t0 & f3(#)g2 is_differentiable_in t0 &
f3(#)g1 is_differentiable_in t0 &
f1(#)g3 is_differentiable_in t0 &
f1(#)g2 is_differentiable_in t0 &
f2(#)g1 is_differentiable_in t0 by A1,A2,FDIFF_1:16;
then A5: f2(#)g3-f3(#)g2 is_differentiable_in t0 &
f3(#)g1-f1(#)g3 is_differentiable_in t0 &
f1(#)g2-f2(#)g1 is_differentiable_in t0 by FDIFF_1:14;
then A6: f2(#)g3-f3(#)g2 is_left_differentiable_in t0 by FDIFF_3:22;
A7: t0 in dom (f2(#)g3-f3(#)g2)
proof
consider r such that
A8: 0 < r & [.t0 - r,t0.] c= dom (f2(#)g3-f3(#)g2) by A6,FDIFF_3:def 4;
t0 - r <= t0 by A8,XREAL_1:44;
then t0 in [.t0 - r,t0.];
hence thesis by A8;
end;
A9: f3(#)g1-f1(#)g3 is_left_differentiable_in t0 by A5,FDIFF_3:22;
A10: t0 in dom (f3(#)g1-f1(#)g3)
proof
consider r1 such that
A11: 0 < r1 & [.t0 - r1,t0.] c= dom (f3(#)g1-f1(#)g3) by A9,FDIFF_3:def 4;
t0 - r1 <= t0 by A11,XREAL_1:44;
then t0 in [.t0 - r1,t0.];
hence thesis by A11;
end;
A12: f1(#)g2-f2(#)g1 is_left_differentiable_in t0 by A5,FDIFF_3:22;
A13: t0 in dom (f1(#)g2-f2(#)g1)
proof
consider r2 such that
A14: 0 < r2 & [.t0 - r2,t0.] c= dom (f1(#)g2-f2(#)g1) by A12,FDIFF_3:def 4;
t0 - r2 <= t0 by A14,XREAL_1:44;
then t0 in [.t0 - r2,t0.];
hence thesis by A14;
end;
VFuncdiff( h1(#)(f2(#)g3-f3(#)g2), h2(#)(f3(#)g1-f1(#)g3),
h3(#)(f1(#)g2-f2(#)g1),t0 )
= |[ ((f2(#)g3-f3(#)g2).t0)*diff(h1,t0),
((f3(#)g1-f1(#)g3).t0)*diff(h2,t0),
((f1(#)g2-f2(#)g1).t0)*diff(h3,t0) ]|+
|[ (h1.t0)*diff((f2(#)g3-f3(#)g2),t0),
(h2.t0)*diff((f3(#)g1-f1(#)g3),t0),
(h3.t0)*diff((f1(#)g2-f2(#)g1),t0) ]| by A3,A5,Th91
.= |[ ((f2(#)g3-f3(#)g2).t0)*diff(h1,t0),
((f3(#)g1-f1(#)g3).t0)*diff(h2,t0),
((f1(#)g2-f2(#)g1).t0)*diff(h3,t0) ]|+
|[ (h1.t0)*(diff(f2(#)g3,t0)-diff(f3(#)g2,t0)),
(h2.t0)*diff((f3(#)g1-f1(#)g3),t0),
(h3.t0)*diff((f1(#)g2-f2(#)g1),t0) ]| by A4,FDIFF_1:14
.= |[ ((f2(#)g3-f3(#)g2).t0)*diff(h1,t0),
((f3(#)g1-f1(#)g3).t0)*diff(h2,t0),
((f1(#)g2-f2(#)g1).t0)*diff(h3,t0) ]|+
|[ (h1.t0)*(diff(f2(#)g3,t0)-diff(f3(#)g2,t0)),
(h2.t0)*(diff(f3(#)g1,t0)-diff(f1(#)g3,t0)),
(h3.t0)*diff((f1(#)g2-f2(#)g1),t0) ]| by A4,FDIFF_1:14
.= |[ ((f2(#)g3-f3(#)g2).t0)*diff(h1,t0),
((f3(#)g1-f1(#)g3).t0)*diff(h2,t0),
((f1(#)g2-f2(#)g1).t0)*diff(h3,t0) ]|+
|[ (h1.t0)*(diff(f2(#)g3,t0)-diff(f3(#)g2,t0)),
(h2.t0)*(diff(f3(#)g1,t0)-diff(f1(#)g3,t0)),
(h3.t0)*(diff(f1(#)g2,t0)-diff(f2(#)g1,t0)) ]| by A4,FDIFF_1:14
.= |[ ((f2(#)g3-f3(#)g2).t0)*diff(h1,t0),
((f3(#)g1-f1(#)g3).t0)*diff(h2,t0),
((f1(#)g2-f2(#)g1).t0)*diff(h3,t0) ]|+
|[ (h1.t0)*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-diff(f3(#)g2,t0)),
(h2.t0)*(diff(f3(#)g1,t0)-diff(f1(#)g3,t0)),
(h3.t0)*(diff(f1(#)g2,t0)-diff(f2(#)g1,t0)) ]| by A1,A2,FDIFF_1:16
.= |[ ((f2(#)g3-f3(#)g2).t0)*diff(h1,t0),
((f3(#)g1-f1(#)g3).t0)*diff(h2,t0),
((f1(#)g2-f2(#)g1).t0)*diff(h3,t0) ]|+
|[ (h1.t0)*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-((g2.t0)*diff(f3,t0)+(f3.t0)*diff(g2,t0))),
(h2.t0)*(diff(f3(#)g1,t0)-diff(f1(#)g3,t0)),
(h3.t0)*(diff(f1(#)g2,t0)-diff(f2(#)g1,t0)) ]| by A1,A2,FDIFF_1:16
.= |[ ((f2(#)g3-f3(#)g2).t0)*diff(h1,t0),
((f3(#)g1-f1(#)g3).t0)*diff(h2,t0),
((f1(#)g2-f2(#)g1).t0)*diff(h3,t0) ]|+
|[ (h1.t0)*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-((g2.t0)*diff(f3,t0)+(f3.t0)*diff(g2,t0))),
(h2.t0)*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-diff(f1(#)g3,t0)),
(h3.t0)*(diff(f1(#)g2,t0)-diff(f2(#)g1,t0)) ]| by A1,A2,FDIFF_1:16
.= |[ ((f2(#)g3-f3(#)g2).t0)*diff(h1,t0),
((f3(#)g1-f1(#)g3).t0)*diff(h2,t0),
((f1(#)g2-f2(#)g1).t0)*diff(h3,t0) ]|+
|[ (h1.t0)*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-((g2.t0)*diff(f3,t0)+(f3.t0)*diff(g2,t0))),
(h2.t0)*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-((g3.t0)*diff(f1,t0)+(f1.t0)*diff(g3,t0))),
(h3.t0)*(diff(f1(#)g2,t0)-diff(f2(#)g1,t0)) ]| by A1,A2,FDIFF_1:16
.= |[ ((f2(#)g3-f3(#)g2).t0)*diff(h1,t0),
((f3(#)g1-f1(#)g3).t0)*diff(h2,t0),
((f1(#)g2-f2(#)g1).t0)*diff(h3,t0) ]|+
|[ (h1.t0)*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-((g2.t0)*diff(f3,t0)+(f3.t0)*diff(g2,t0))),
(h2.t0)*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-((g3.t0)*diff(f1,t0)+(f1.t0)*diff(g3,t0))),
(h3.t0)*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-diff(f2(#)g1,t0)) ]| by A1,A2,FDIFF_1:16
.= |[ ((f2(#)g3-f3(#)g2).t0)*diff(h1,t0),
((f3(#)g1-f1(#)g3).t0)*diff(h2,t0),
((f1(#)g2-f2(#)g1).t0)*diff(h3,t0) ]|+
|[ (h1.t0)*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-((g2.t0)*diff(f3,t0)+(f3.t0)*diff(g2,t0))),
(h2.t0)*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-((g3.t0)*diff(f1,t0)+(f1.t0)*diff(g3,t0))),
(h3.t0)*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-((g1.t0)*diff(f2,t0)+(f2.t0)*diff(g1,t0))) ]| by A1,A2,FDIFF_1:16
.= |[ ((f2(#)g3).t0-(f3(#)g2).t0)*diff(h1,t0),
((f3(#)g1-f1(#)g3).t0)*diff(h2,t0),
((f1(#)g2-f2(#)g1).t0)*diff(h3,t0) ]|+
|[ (h1.t0)*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-((g2.t0)*diff(f3,t0)+(f3.t0)*diff(g2,t0))),
(h2.t0)*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-((g3.t0)*diff(f1,t0)+(f1.t0)*diff(g3,t0))),
(h3.t0)*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-((g1.t0)*diff(f2,t0)+(f2.t0)*diff(g1,t0))) ]| by A7,VALUED_1:13
.= |[ (f2.t0*g3.t0-(f3(#)g2).t0)*diff(h1,t0),
((f3(#)g1-f1(#)g3).t0)*diff(h2,t0),
((f1(#)g2-f2(#)g1).t0)*diff(h3,t0) ]|+
|[ (h1.t0)*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-((g2.t0)*diff(f3,t0)+(f3.t0)*diff(g2,t0))),
(h2.t0)*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-((g3.t0)*diff(f1,t0)+(f1.t0)*diff(g3,t0))),
(h3.t0)*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-((g1.t0)*diff(f2,t0)+(f2.t0)*diff(g1,t0))) ]| by VALUED_1:5
.= |[ (f2.t0*g3.t0-f3.t0*g2.t0)*diff(h1,t0),
((f3(#)g1-f1(#)g3).t0)*diff(h2,t0),
((f1(#)g2-f2(#)g1).t0)*diff(h3,t0) ]|+
|[ (h1.t0)*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-((g2.t0)*diff(f3,t0)+(f3.t0)*diff(g2,t0))),
(h2.t0)*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-((g3.t0)*diff(f1,t0)+(f1.t0)*diff(g3,t0))),
(h3.t0)*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-((g1.t0)*diff(f2,t0)+(f2.t0)*diff(g1,t0))) ]| by VALUED_1:5
.= |[ (f2.t0*g3.t0-f3.t0*g2.t0)*diff(h1,t0),
((f3(#)g1).t0-(f1(#)g3).t0)*diff(h2,t0),
((f1(#)g2-f2(#)g1).t0)*diff(h3,t0) ]|+
|[ (h1.t0)*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-((g2.t0)*diff(f3,t0)+(f3.t0)*diff(g2,t0))),
(h2.t0)*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-((g3.t0)*diff(f1,t0)+(f1.t0)*diff(g3,t0))),
(h3.t0)*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-((g1.t0)*diff(f2,t0)+(f2.t0)*diff(g1,t0))) ]| by A10,VALUED_1:13
.= |[ (f2.t0*g3.t0-f3.t0*g2.t0)*diff(h1,t0),
(f3.t0*g1.t0-(f1(#)g3).t0)*diff(h2,t0),
((f1(#)g2-f2(#)g1).t0)*diff(h3,t0) ]|+
|[ (h1.t0)*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-((g2.t0)*diff(f3,t0)+(f3.t0)*diff(g2,t0))),
(h2.t0)*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-((g3.t0)*diff(f1,t0)+(f1.t0)*diff(g3,t0))),
(h3.t0)*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-((g1.t0)*diff(f2,t0)+(f2.t0)*diff(g1,t0))) ]| by VALUED_1:5
.= |[ (f2.t0*g3.t0-f3.t0*g2.t0)*diff(h1,t0),
(f3.t0*g1.t0-f1.t0*g3.t0)*diff(h2,t0),
((f1(#)g2-f2(#)g1).t0)*diff(h3,t0) ]|+
|[ (h1.t0)*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-((g2.t0)*diff(f3,t0)+(f3.t0)*diff(g2,t0))),
(h2.t0)*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-((g3.t0)*diff(f1,t0)+(f1.t0)*diff(g3,t0))),
(h3.t0)*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-((g1.t0)*diff(f2,t0)+(f2.t0)*diff(g1,t0))) ]| by VALUED_1:5
.= |[ (f2.t0*g3.t0-f3.t0*g2.t0)*diff(h1,t0),
(f3.t0*g1.t0-f1.t0*g3.t0)*diff(h2,t0),
((f1(#)g2).t0-(f2(#)g1).t0)*diff(h3,t0) ]|+
|[ (h1.t0)*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-((g2.t0)*diff(f3,t0)+(f3.t0)*diff(g2,t0))),
(h2.t0)*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-((g3.t0)*diff(f1,t0)+(f1.t0)*diff(g3,t0))),
(h3.t0)*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-((g1.t0)*diff(f2,t0)+(f2.t0)*diff(g1,t0))) ]| by A13,VALUED_1:13
.= |[ (f2.t0*g3.t0-f3.t0*g2.t0)*diff(h1,t0),
(f3.t0*g1.t0-f1.t0*g3.t0)*diff(h2,t0),
(f1.t0*g2.t0-(f2(#)g1).t0)*diff(h3,t0) ]|+
|[ (h1.t0)*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-((g2.t0)*diff(f3,t0)+(f3.t0)*diff(g2,t0))),
(h2.t0)*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-((g3.t0)*diff(f1,t0)+(f1.t0)*diff(g3,t0))),
(h3.t0)*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-((g1.t0)*diff(f2,t0)+(f2.t0)*diff(g1,t0))) ]| by VALUED_1:5
.= |[ 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)*(g3.t0)*diff(f2,t0)-(h1.t0)*(g2.t0)*diff(f3,t0))
+((h1.t0)*(f2.t0)*diff(g3,t0)-(h1.t0)*(f3.t0)*diff(g2,t0)),
((h2.t0)*(g1.t0)*diff(f3,t0)-(h2.t0)*(g3.t0)*diff(f1,t0))
+((h2.t0)*(f3.t0)*diff(g1,t0)-(h2.t0)*(f1.t0)*diff(g3,t0)),
((h3.t0)*(g2.t0)*diff(f1,t0)-(h3.t0)*(g1.t0)*diff(f2,t0))
+((h3.t0)*(f1.t0)*diff(g2,t0)-(h3.t0)*(f2.t0)*diff(g1,t0)) ]|
by VALUED_1:5
.= |[ 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)*(g3.t0)*diff(f2,t0)-(h1.t0)*(g2.t0)*diff(f3,t0),
(h2.t0)*(g1.t0)*diff(f3,t0)-(h2.t0)*(g3.t0)*diff(f1,t0),
(h3.t0)*(g2.t0)*diff(f1,t0)-(h3.t0)*(g1.t0)*diff(f2,t0) ]|+
|[ (h1.t0)*(f2.t0)*diff(g3,t0)-(h1.t0)*(f3.t0)*diff(g2,t0),
(h2.t0)*(f3.t0)*diff(g1,t0)-(h2.t0)*(f1.t0)*diff(g3,t0),
(h3.t0)*(f1.t0)*diff(g2,t0)-(h3.t0)*(f2.t0)*diff(g1,t0) ]|) by Lm8
.= |[ 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)) ]| by RVSUM_1:15;
hence thesis;
end;
::p37-4(5.2) A*BXC
theorem
(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) ]|
proof
assume that
A1: f1 is_differentiable_in t0 & f2 is_differentiable_in t0 &
f3 is_differentiable_in t0 and
A2: g1 is_differentiable_in t0 & g2 is_differentiable_in t0 &
g3 is_differentiable_in t0 and
A3: h1 is_differentiable_in t0 &
h2 is_differentiable_in t0 & h3 is_differentiable_in t0;
A4: h3(#)f3 is_differentiable_in t0 & h1(#)f1 is_differentiable_in t0 &
h2(#)f2 is_differentiable_in t0 by A1,A3,FDIFF_1:16;
then A5: h3(#)f3(#)g1 is_differentiable_in t0 &
h3(#)f3(#)g2 is_differentiable_in t0 &
h1(#)f1(#)g2 is_differentiable_in t0 &
h1(#)f1(#)g3 is_differentiable_in t0 &
h2(#)f2(#)g3 is_differentiable_in t0 &
h2(#)f2(#)g1 is_differentiable_in t0 by A2,FDIFF_1:16;
VFuncdiff( h2(#)f2(#)g3-h3(#)f3(#)g2, h3(#)f3(#)g1-h1(#)f1(#)g3,
h1(#)f1(#)g2-h2(#)f2(#)g1,t0 )
= VFuncdiff( h2(#)f2(#)g3,h3(#)f3(#)g1,h1(#)f1(#)g2,t0 )-
VFuncdiff( h3(#)f3(#)g2,h1(#)f1(#)g3,h2(#)f2(#)g1,t0 ) by A5,Th89
.= |[ (g3.t0)*diff(h2(#)f2,t0),(g1.t0)*diff(h3(#)f3,t0),
(g2.t0)*diff(h1(#)f1,t0) ]|+
|[ (h2(#)f2).t0*diff(g3,t0),(h3(#)f3).t0*diff(g1,t0),
(h1(#)f1).t0*diff(g2,t0) ]|-
VFuncdiff( h3(#)f3(#)g2,h1(#)f1(#)g3,h2(#)f2(#)g1,t0 ) by A2,A4,Th91
.= |[ (g3.t0)*diff(h2(#)f2,t0),(g1.t0)*diff(h3(#)f3,t0),
(g2.t0)*diff(h1(#)f1,t0) ]|+
|[ (h2(#)f2).t0*diff(g3,t0),(h3(#)f3).t0*diff(g1,t0),
(h1(#)f1).t0*diff(g2,t0) ]|-
(|[ (g2.t0)*diff(h3(#)f3,t0),(g3.t0)*diff(h1(#)f1,t0),
(g1.t0)*diff(h2(#)f2,t0) ]|+
|[ (h3(#)f3).t0*diff(g2,t0),(h1(#)f1).t0*diff(g3,t0),
(h2(#)f2).t0*diff(g1,t0) ]|) by A2,A4,Th91
.= |[ (g3.t0)*((f2.t0)*diff(h2,t0)+(h2.t0)*diff(f2,t0)),
(g1.t0)*diff(h3(#)f3,t0),(g2.t0)*diff(h1(#)f1,t0) ]|+
|[ (h2(#)f2).t0*diff(g3,t0),(h3(#)f3).t0*diff(g1,t0),
(h1(#)f1).t0*diff(g2,t0) ]|-
(|[ (g2.t0)*diff(h3(#)f3,t0),(g3.t0)*diff(h1(#)f1,t0),
(g1.t0)*diff(h2(#)f2,t0) ]|+
|[ (h3(#)f3).t0*diff(g2,t0),(h1(#)f1).t0*diff(g3,t0),
(h2(#)f2).t0*diff(g1,t0) ]|) by A1,A3,FDIFF_1:16
.= |[ (g3.t0)*((f2.t0)*diff(h2,t0)+(h2.t0)*diff(f2,t0)),
(g1.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0)),
(g2.t0)*diff(h1(#)f1,t0) ]|+
|[ (h2(#)f2).t0*diff(g3,t0),(h3(#)f3).t0*diff(g1,t0),
(h1(#)f1).t0*diff(g2,t0) ]|-
(|[ (g2.t0)*diff(h3(#)f3,t0),(g3.t0)*diff(h1(#)f1,t0),
(g1.t0)*diff(h2(#)f2,t0) ]|+
|[ (h3(#)f3).t0*diff(g2,t0),(h1(#)f1).t0*diff(g3,t0),
(h2(#)f2).t0*diff(g1,t0) ]|) by A1,A3,FDIFF_1:16
.= |[ (g3.t0)*((f2.t0)*diff(h2,t0)+(h2.t0)*diff(f2,t0)),
(g1.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0)),
(g2.t0)*((f1.t0)*diff(h1,t0)+(h1.t0)*diff(f1,t0)) ]|+
|[ (h2(#)f2).t0*diff(g3,t0),(h3(#)f3).t0*diff(g1,t0),
(h1(#)f1).t0*diff(g2,t0) ]|-
(|[ (g2.t0)*diff(h3(#)f3,t0),(g3.t0)*diff(h1(#)f1,t0),
(g1.t0)*diff(h2(#)f2,t0) ]|+
|[ (h3(#)f3).t0*diff(g2,t0),(h1(#)f1).t0*diff(g3,t0),
(h2(#)f2).t0*diff(g1,t0) ]|) by A1,A3,FDIFF_1:16
.= |[ (g3.t0)*((f2.t0)*diff(h2,t0)+(h2.t0)*diff(f2,t0)),
(g1.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0)),
(g2.t0)*((f1.t0)*diff(h1,t0)+(h1.t0)*diff(f1,t0)) ]|+
|[ h2.t0*f2.t0*diff(g3,t0),(h3(#)f3).t0*diff(g1,t0),
(h1(#)f1).t0*diff(g2,t0) ]|-
(|[ (g2.t0)*diff(h3(#)f3,t0),(g3.t0)*diff(h1(#)f1,t0),
(g1.t0)*diff(h2(#)f2,t0) ]|+
|[ (h3(#)f3).t0*diff(g2,t0),(h1(#)f1).t0*diff(g3,t0),
(h2(#)f2).t0*diff(g1,t0) ]|) by VALUED_1:5
.= |[ (g3.t0)*((f2.t0)*diff(h2,t0)+(h2.t0)*diff(f2,t0)),
(g1.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0)),
(g2.t0)*((f1.t0)*diff(h1,t0)+(h1.t0)*diff(f1,t0)) ]|+
|[ h2.t0*f2.t0*diff(g3,t0),h3.t0*f3.t0*diff(g1,t0),
(h1(#)f1).t0*diff(g2,t0) ]|-
(|[ (g2.t0)*diff(h3(#)f3,t0),(g3.t0)*diff(h1(#)f1,t0),
(g1.t0)*diff(h2(#)f2,t0) ]|+
|[ (h3(#)f3).t0*diff(g2,t0),(h1(#)f1).t0*diff(g3,t0),
(h2(#)f2).t0*diff(g1,t0) ]|) by VALUED_1:5
.= |[ (g3.t0)*((f2.t0)*diff(h2,t0)+(h2.t0)*diff(f2,t0)),
(g1.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0)),
(g2.t0)*((f1.t0)*diff(h1,t0)+(h1.t0)*diff(f1,t0)) ]|+
|[ h2.t0*f2.t0*diff(g3,t0),h3.t0*f3.t0*diff(g1,t0),
h1.t0*f1.t0*diff(g2,t0) ]|-
(|[ (g2.t0)*diff(h3(#)f3,t0),(g3.t0)*diff(h1(#)f1,t0),
(g1.t0)*diff(h2(#)f2,t0) ]|+
|[ (h3(#)f3).t0*diff(g2,t0),(h1(#)f1).t0*diff(g3,t0),
(h2(#)f2).t0*diff(g1,t0) ]|) by VALUED_1:5
.= |[ (g3.t0)*((f2.t0)*diff(h2,t0)+(h2.t0)*diff(f2,t0)),
(g1.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0)),
(g2.t0)*((f1.t0)*diff(h1,t0)+(h1.t0)*diff(f1,t0)) ]|+
|[ h2.t0*f2.t0*diff(g3,t0),h3.t0*f3.t0*diff(g1,t0),
h1.t0*f1.t0*diff(g2,t0) ]|-
(|[ (g2.t0)*diff(h3(#)f3,t0),(g3.t0)*diff(h1(#)f1,t0),
(g1.t0)*diff(h2(#)f2,t0) ]|+
|[ h3.t0*f3.t0*diff(g2,t0),(h1(#)f1).t0*diff(g3,t0),
(h2(#)f2).t0*diff(g1,t0) ]|) by VALUED_1:5
.= |[ (g3.t0)*((f2.t0)*diff(h2,t0)+(h2.t0)*diff(f2,t0)),
(g1.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0)),
(g2.t0)*((f1.t0)*diff(h1,t0)+(h1.t0)*diff(f1,t0)) ]|+
|[ h2.t0*f2.t0*diff(g3,t0),h3.t0*f3.t0*diff(g1,t0),
h1.t0*f1.t0*diff(g2,t0) ]|-
(|[ (g2.t0)*diff(h3(#)f3,t0),(g3.t0)*diff(h1(#)f1,t0),
(g1.t0)*diff(h2(#)f2,t0) ]|+
|[ h3.t0*f3.t0*diff(g2,t0),h1.t0*f1.t0*diff(g3,t0),
(h2(#)f2).t0*diff(g1,t0) ]|) by VALUED_1:5
.= |[ (g3.t0)*((f2.t0)*diff(h2,t0)+(h2.t0)*diff(f2,t0)),
(g1.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0)),
(g2.t0)*((f1.t0)*diff(h1,t0)+(h1.t0)*diff(f1,t0)) ]|+
|[ h2.t0*f2.t0*diff(g3,t0),h3.t0*f3.t0*diff(g1,t0),
h1.t0*f1.t0*diff(g2,t0) ]|-
(|[ (g2.t0)*diff(h3(#)f3,t0),(g3.t0)*diff(h1(#)f1,t0),
(g1.t0)*diff(h2(#)f2,t0) ]|+
|[ h3.t0*f3.t0*diff(g2,t0),h1.t0*f1.t0*diff(g3,t0),
h2.t0*f2.t0*diff(g1,t0) ]|) by VALUED_1:5
.= |[ (g3.t0)*((f2.t0)*diff(h2,t0)+(h2.t0)*diff(f2,t0)),
(g1.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0)),
(g2.t0)*((f1.t0)*diff(h1,t0)+(h1.t0)*diff(f1,t0)) ]|+
|[ h2.t0*f2.t0*diff(g3,t0),h3.t0*f3.t0*diff(g1,t0),
h1.t0*f1.t0*diff(g2,t0) ]|-
(|[ (g2.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0)),
(g3.t0)*diff(h1(#)f1,t0),(g1.t0)*diff(h2(#)f2,t0) ]|+
|[ h3.t0*f3.t0*diff(g2,t0),h1.t0*f1.t0*diff(g3,t0),
h2.t0*f2.t0*diff(g1,t0) ]|) by A1,A3,FDIFF_1:16
.= |[ (g3.t0)*((f2.t0)*diff(h2,t0)+(h2.t0)*diff(f2,t0)),
(g1.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0)),
(g2.t0)*((f1.t0)*diff(h1,t0)+(h1.t0)*diff(f1,t0)) ]|+
|[ h2.t0*f2.t0*diff(g3,t0),h3.t0*f3.t0*diff(g1,t0),
h1.t0*f1.t0*diff(g2,t0) ]|-
(|[ (g2.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0)),
(g3.t0)*((f1.t0)*diff(h1,t0)+(h1.t0)*diff(f1,t0)),
(g1.t0)*diff(h2(#)f2,t0) ]|+
|[ h3.t0*f3.t0*diff(g2,t0),h1.t0*f1.t0*diff(g3,t0),
h2.t0*f2.t0*diff(g1,t0) ]|) by A1,A3,FDIFF_1:16
.= |[ (g3.t0)*((f2.t0)*diff(h2,t0)+(h2.t0)*diff(f2,t0)),
(g1.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0)),
(g2.t0)*((f1.t0)*diff(h1,t0)+(h1.t0)*diff(f1,t0)) ]|+
|[ h2.t0*f2.t0*diff(g3,t0),h3.t0*f3.t0*diff(g1,t0),
h1.t0*f1.t0*diff(g2,t0) ]|-
(|[ (g2.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0)),
(g3.t0)*((f1.t0)*diff(h1,t0)+(h1.t0)*diff(f1,t0)),
(g1.t0)*((f2.t0)*diff(h2,t0)+(h2.t0)*diff(f2,t0)) ]|+
|[ h3.t0*f3.t0*diff(g2,t0),h1.t0*f1.t0*diff(g3,t0),
h2.t0*f2.t0*diff(g1,t0) ]|) by A1,A3,FDIFF_1:16
.= |[ (g3.t0)*((f2.t0)*diff(h2,t0)+(h2.t0)*diff(f2,t0)),
(g1.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0)),
(g2.t0)*((f1.t0)*diff(h1,t0)+(h1.t0)*diff(f1,t0)) ]|+
|[ h2.t0*f2.t0*diff(g3,t0),h3.t0*f3.t0*diff(g1,t0),
h1.t0*f1.t0*diff(g2,t0) ]|-
|[ (g2.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0)),
(g3.t0)*((f1.t0)*diff(h1,t0)+(h1.t0)*diff(f1,t0)),
(g1.t0)*((f2.t0)*diff(h2,t0)+(h2.t0)*diff(f2,t0)) ]|-
|[ h3.t0*f3.t0*diff(g2,t0),h1.t0*f1.t0*diff(g3,t0),
h2.t0*f2.t0*diff(g1,t0) ]| by RVSUM_1:39
.= (|[ (g3.t0)*((f2.t0)*diff(h2,t0)+(h2.t0)*diff(f2,t0)),
(g1.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0)),
(g2.t0)*((f1.t0)*diff(h1,t0)+(h1.t0)*diff(f1,t0)) ]|-
|[ (g2.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0)),
(g3.t0)*((f1.t0)*diff(h1,t0)+(h1.t0)*diff(f1,t0)),
(g1.t0)*((f2.t0)*diff(h2,t0)+(h2.t0)*diff(f2,t0)) ]|)+
|[ h2.t0*f2.t0*diff(g3,t0),h3.t0*f3.t0*diff(g1,t0),
h1.t0*f1.t0*diff(g2,t0) ]|+
-|[ h3.t0*f3.t0*diff(g2,t0),h1.t0*f1.t0*diff(g3,t0),
h2.t0*f2.t0*diff(g1,t0) ]| by RVSUM_1:15
.= (|[ (g3.t0)*((f2.t0)*diff(h2,t0)+(h2.t0)*diff(f2,t0)),
(g1.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0)),
(g2.t0)*((f1.t0)*diff(h1,t0)+(h1.t0)*diff(f1,t0)) ]|-
|[ (g2.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0)),
(g3.t0)*((f1.t0)*diff(h1,t0)+(h1.t0)*diff(f1,t0)),
(g1.t0)*((f2.t0)*diff(h2,t0)+(h2.t0)*diff(f2,t0)) ]|)+
(|[ h2.t0*f2.t0*diff(g3,t0),h3.t0*f3.t0*diff(g1,t0),
h1.t0*f1.t0*diff(g2,t0) ]|-
|[ h3.t0*f3.t0*diff(g2,t0),h1.t0*f1.t0*diff(g3,t0),
h2.t0*f2.t0*diff(g1,t0) ]|) by RVSUM_1:15
.= (|[ (g3.t0)*((f2.t0)*diff(h2,t0)+(h2.t0)*diff(f2,t0)),
(g1.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0)),
(g2.t0)*((f1.t0)*diff(h1,t0)+(h1.t0)*diff(f1,t0)) ]|-
|[ (g2.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0)),
(g3.t0)*((f1.t0)*diff(h1,t0)+(h1.t0)*diff(f1,t0)),
(g1.t0)*((f2.t0)*diff(h2,t0)+(h2.t0)*diff(f2,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) ]| by Lm11
.= |[ 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) ]|+
|[ (g3.t0)*((f2.t0)*diff(h2,t0)+(h2.t0)*diff(f2,t0))-
(g2.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0)),
(g1.t0)*((f3.t0)*diff(h3,t0)+(h3.t0)*diff(f3,t0))-
(g3.t0)*((f1.t0)*diff(h1,t0)+(h1.t0)*diff(f1,t0)),
(g2.t0)*((f1.t0)*diff(h1,t0)+(h1.t0)*diff(f1,t0))-
(g1.t0)*((f2.t0)*diff(h2,t0)+(h2.t0)*diff(f2,t0)) ]| by Lm11
.= |[ 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) ]|+
|[ ((g3.t0)*(h2.t0)*diff(f2,t0)-(g2.t0)*(h3.t0)*diff(f3,t0))
+((g3.t0)*(f2.t0)*diff(h2,t0)-(g2.t0)*(f3.t0)*diff(h3,t0)),
((g1.t0)*(h3.t0)*diff(f3,t0)-(g3.t0)*(h1.t0)*diff(f1,t0))
+((g1.t0)*(f3.t0)*diff(h3,t0)-(g3.t0)*(f1.t0)*diff(h1,t0)),
((g2.t0)*(h1.t0)*diff(f1,t0)-(g1.t0)*(h2.t0)*diff(f2,t0))
+((g2.t0)*(f1.t0)*diff(h1,t0)-(g1.t0)*(f2.t0)*diff(h2,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) ]|+
(|[ (g3.t0)*(h2.t0)*diff(f2,t0)-(g2.t0)*(h3.t0)*diff(f3,t0),
(g1.t0)*(h3.t0)*diff(f3,t0)-(g3.t0)*(h1.t0)*diff(f1,t0),
(g2.t0)*(h1.t0)*diff(f1,t0)-(g1.t0)*(h2.t0)*diff(f2,t0) ]|+
|[ (g3.t0)*(f2.t0)*diff(h2,t0)-(g2.t0)*(f3.t0)*diff(h3,t0),
(g1.t0)*(f3.t0)*diff(h3,t0)-(g3.t0)*(f1.t0)*diff(h1,t0),
(g2.t0)*(f1.t0)*diff(h1,t0)-(g1.t0)*(f2.t0)*diff(h2,t0) ]|) by Lm8
.= |[ 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) ]|+
|[ (g3.t0)*(h2.t0)*diff(f2,t0)-(g2.t0)*(h3.t0)*diff(f3,t0),
(g1.t0)*(h3.t0)*diff(f3,t0)-(g3.t0)*(h1.t0)*diff(f1,t0),
(g2.t0)*(h1.t0)*diff(f1,t0)-(g1.t0)*(h2.t0)*diff(f2,t0) ]|+
|[ (g3.t0)*(f2.t0)*diff(h2,t0)-(g2.t0)*(f3.t0)*diff(h3,t0),
(g1.t0)*(f3.t0)*diff(h3,t0)-(g3.t0)*(f1.t0)*diff(h1,t0),
(g2.t0)*(f1.t0)*diff(h1,t0)-(g1.t0)*(f2.t0)*diff(h2,t0) ]|
by RVSUM_1:15;
hence thesis;
end;
::p37-4(6) AX(BXC)
theorem
(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)) ]|
proof
assume that
A1: f1 is_differentiable_in t0 & f2 is_differentiable_in t0 &
f3 is_differentiable_in t0 and
A2: g1 is_differentiable_in t0 & g2 is_differentiable_in t0 &
g3 is_differentiable_in t0 and
A3: h1 is_differentiable_in t0 & h2 is_differentiable_in t0 &
h3 is_differentiable_in t0;
A4: f2(#)g3 is_differentiable_in t0 & f3(#)g2 is_differentiable_in t0 &
f3(#)g1 is_differentiable_in t0 &
f1(#)g3 is_differentiable_in t0 &
f1(#)g2 is_differentiable_in t0 &
f2(#)g1 is_differentiable_in t0 by A1,A2,FDIFF_1:16;
then A5: f2(#)g3-f3(#)g2 is_differentiable_in t0 &
f3(#)g1-f1(#)g3 is_differentiable_in t0 &
f1(#)g2-f2(#)g1 is_differentiable_in t0 by FDIFF_1:14;
then A6: h3(#)(f2(#)g3-f3(#)g2) is_differentiable_in t0 &
h3(#)(f3(#)g1-f1(#)g3) is_differentiable_in t0 &
h2(#)(f1(#)g2-f2(#)g1) is_differentiable_in t0 &
h2(#)(f2(#)g3-f3(#)g2) is_differentiable_in t0 &
h1(#)(f3(#)g1-f1(#)g3) is_differentiable_in t0 &
h1(#)(f1(#)g2-f2(#)g1) is_differentiable_in t0
by A3,FDIFF_1:16;
A7: f1(#)g2-f2(#)g1 is_left_differentiable_in t0 by A5,FDIFF_3:22;
A8: t0 in dom (f1(#)g2-f2(#)g1)
proof
consider r such that
A9: 0 < r & [.t0 - r,t0.] c= dom (f1(#)g2-f2(#)g1) by A7,FDIFF_3:def 4;
t0 - r <= t0 by A9,XREAL_1:44;
then t0 in [.t0 - r,t0.];
hence thesis by A9;
end;
A10: f2(#)g3-f3(#)g2 is_left_differentiable_in t0 by A5,FDIFF_3:22;
A11: t0 in dom (f2(#)g3-f3(#)g2)
proof
consider r1 such that
A12: 0 < r1 & [.t0 - r1,t0.] c= dom (f2(#)g3-f3(#)g2) by A10,FDIFF_3:def 4;
t0 - r1 <= t0 by A12,XREAL_1:44;
then t0 in [.t0 - r1,t0.];
hence thesis by A12;
end;
A13: f3(#)g1-f1(#)g3 is_left_differentiable_in t0 by A5,FDIFF_3:22;
A14: t0 in dom (f3(#)g1-f1(#)g3)
proof
consider r2 such that
A15: 0 < r2 & [.t0 - r2,t0.] c= dom (f3(#)g1-f1(#)g3) by A13,FDIFF_3:def 4;
t0 - r2 <= t0 by A15,XREAL_1:44;
then t0 in [.t0 - r2,t0.];
hence thesis by A15;
end;
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 )
= VFuncdiff( h2(#)(f1(#)g2-f2(#)g1),
h3(#)(f2(#)g3-f3(#)g2),
h1(#)(f3(#)g1-f1(#)g3),t0 )-
VFuncdiff( h3(#)(f3(#)g1-f1(#)g3),
h1(#)(f1(#)g2-f2(#)g1),
h2(#)(f2(#)g3-f3(#)g2),t0 ) by A6,Th89
.= |[ (f1(#)g2-f2(#)g1).t0*diff(h2,t0),
(f2(#)g3-f3(#)g2).t0*diff(h3,t0),
(f3(#)g1-f1(#)g3).t0*diff(h1,t0) ]|+
|[ h2.t0*diff((f1(#)g2-f2(#)g1),t0),
h3.t0*diff((f2(#)g3-f3(#)g2),t0),
h1.t0*diff((f3(#)g1-f1(#)g3),t0) ]|-
VFuncdiff( h3(#)(f3(#)g1-f1(#)g3),
h1(#)(f1(#)g2-f2(#)g1),
h2(#)(f2(#)g3-f3(#)g2),t0 ) by A3,A5,Th91
.= |[ (f1(#)g2-f2(#)g1).t0*diff(h2,t0),
(f2(#)g3-f3(#)g2).t0*diff(h3,t0),
(f3(#)g1-f1(#)g3).t0*diff(h1,t0) ]|+
|[ h2.t0*diff((f1(#)g2-f2(#)g1),t0),
h3.t0*diff((f2(#)g3-f3(#)g2),t0),
h1.t0*diff((f3(#)g1-f1(#)g3),t0) ]|-
(|[ (f3(#)g1-f1(#)g3).t0*diff(h3,t0),
(f1(#)g2-f2(#)g1).t0*diff(h1,t0),
(f2(#)g3-f3(#)g2).t0*diff(h2,t0) ]|+
|[ h3.t0*diff((f3(#)g1-f1(#)g3),t0),
h1.t0*diff((f1(#)g2-f2(#)g1),t0),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|) by A3,A5,Th91
.= |[ ((f1(#)g2).t0-(f2(#)g1).t0)*diff(h2,t0),
(f2(#)g3-f3(#)g2).t0*diff(h3,t0),
(f3(#)g1-f1(#)g3).t0*diff(h1,t0) ]|+
|[ h2.t0*diff((f1(#)g2-f2(#)g1),t0),
h3.t0*diff((f2(#)g3-f3(#)g2),t0),
h1.t0*diff((f3(#)g1-f1(#)g3),t0) ]|-
(|[ (f3(#)g1-f1(#)g3).t0*diff(h3,t0),
(f1(#)g2-f2(#)g1).t0*diff(h1,t0),
(f2(#)g3-f3(#)g2).t0*diff(h2,t0) ]|+
|[ h3.t0*diff((f3(#)g1-f1(#)g3),t0),
h1.t0*diff((f1(#)g2-f2(#)g1),t0),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|)
by A8,VALUED_1:13
.= |[ ((f1(#)g2).t0-(f2(#)g1).t0)*diff(h2,t0),
((f2(#)g3).t0-(f3(#)g2).t0)*diff(h3,t0),
(f3(#)g1-f1(#)g3).t0*diff(h1,t0) ]|+
|[ h2.t0*diff((f1(#)g2-f2(#)g1),t0),
h3.t0*diff((f2(#)g3-f3(#)g2),t0),
h1.t0*diff((f3(#)g1-f1(#)g3),t0) ]|-
(|[ (f3(#)g1-f1(#)g3).t0*diff(h3,t0),
(f1(#)g2-f2(#)g1).t0*diff(h1,t0),
(f2(#)g3-f3(#)g2).t0*diff(h2,t0) ]|+
|[ h3.t0*diff((f3(#)g1-f1(#)g3),t0),
h1.t0*diff((f1(#)g2-f2(#)g1),t0),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|) by A11,VALUED_1:13
.= |[ ((f1(#)g2).t0-(f2(#)g1).t0)*diff(h2,t0),
((f2(#)g3).t0-(f3(#)g2).t0)*diff(h3,t0),
((f3(#)g1).t0-(f1(#)g3).t0)*diff(h1,t0) ]|+
|[ h2.t0*diff((f1(#)g2-f2(#)g1),t0),
h3.t0*diff((f2(#)g3-f3(#)g2),t0),
h1.t0*diff((f3(#)g1-f1(#)g3),t0) ]|-
(|[ (f3(#)g1-f1(#)g3).t0*diff(h3,t0),
(f1(#)g2-f2(#)g1).t0*diff(h1,t0),
(f2(#)g3-f3(#)g2).t0*diff(h2,t0) ]|+
|[ h3.t0*diff((f3(#)g1-f1(#)g3),t0),
h1.t0*diff((f1(#)g2-f2(#)g1),t0),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|) by A14,VALUED_1:13
.= |[ ((f1(#)g2).t0-(f2(#)g1).t0)*diff(h2,t0),
((f2(#)g3).t0-(f3(#)g2).t0)*diff(h3,t0),
((f3(#)g1).t0-(f1(#)g3).t0)*diff(h1,t0) ]|+
|[ h2.t0*diff((f1(#)g2-f2(#)g1),t0),
h3.t0*diff((f2(#)g3-f3(#)g2),t0),
h1.t0*diff((f3(#)g1-f1(#)g3),t0) ]|-
(|[ ((f3(#)g1).t0-(f1(#)g3).t0)*diff(h3,t0),
(f1(#)g2-f2(#)g1).t0*diff(h1,t0),
(f2(#)g3-f3(#)g2).t0*diff(h2,t0) ]|+
|[ h3.t0*diff((f3(#)g1-f1(#)g3),t0),
h1.t0*diff((f1(#)g2-f2(#)g1),t0),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|) by A14,VALUED_1:13
.= |[ ((f1(#)g2).t0-(f2(#)g1).t0)*diff(h2,t0),
((f2(#)g3).t0-(f3(#)g2).t0)*diff(h3,t0),
((f3(#)g1).t0-(f1(#)g3).t0)*diff(h1,t0) ]|+
|[ h2.t0*diff((f1(#)g2-f2(#)g1),t0),
h3.t0*diff((f2(#)g3-f3(#)g2),t0),
h1.t0*diff((f3(#)g1-f1(#)g3),t0) ]|-
(|[ ((f3(#)g1).t0-(f1(#)g3).t0)*diff(h3,t0),
((f1(#)g2).t0-(f2(#)g1).t0)*diff(h1,t0),
(f2(#)g3-f3(#)g2).t0*diff(h2,t0) ]|+
|[ h3.t0*diff((f3(#)g1-f1(#)g3),t0),
h1.t0*diff((f1(#)g2-f2(#)g1),t0),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|) by A8,VALUED_1:13
.= |[ ((f1(#)g2).t0-(f2(#)g1).t0)*diff(h2,t0),
((f2(#)g3).t0-(f3(#)g2).t0)*diff(h3,t0),
((f3(#)g1).t0-(f1(#)g3).t0)*diff(h1,t0) ]|+
|[ h2.t0*diff((f1(#)g2-f2(#)g1),t0),
h3.t0*diff((f2(#)g3-f3(#)g2),t0),
h1.t0*diff((f3(#)g1-f1(#)g3),t0) ]|-
(|[ ((f3(#)g1).t0-(f1(#)g3).t0)*diff(h3,t0),
((f1(#)g2).t0-(f2(#)g1).t0)*diff(h1,t0),
((f2(#)g3).t0-(f3(#)g2).t0)*diff(h2,t0) ]|+
|[ h3.t0*diff((f3(#)g1-f1(#)g3),t0),
h1.t0*diff((f1(#)g2-f2(#)g1),t0),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|) by A11,VALUED_1:13
.= |[ ((f1.t0*g2.t0)-(f2(#)g1).t0)*diff(h2,t0),
((f2(#)g3).t0-(f3(#)g2).t0)*diff(h3,t0),
((f3(#)g1).t0-(f1(#)g3).t0)*diff(h1,t0) ]|+
|[ h2.t0*diff((f1(#)g2-f2(#)g1),t0),
h3.t0*diff((f2(#)g3-f3(#)g2),t0),
h1.t0*diff((f3(#)g1-f1(#)g3),t0) ]|-
(|[ ((f3(#)g1).t0-(f1(#)g3).t0)*diff(h3,t0),
((f1(#)g2).t0-(f2(#)g1).t0)*diff(h1,t0),
((f2(#)g3).t0-(f3(#)g2).t0)*diff(h2,t0) ]|+
|[ h3.t0*diff((f3(#)g1-f1(#)g3),t0),
h1.t0*diff((f1(#)g2-f2(#)g1),t0),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|) by VALUED_1:5
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2(#)g3).t0-(f3(#)g2).t0)*diff(h3,t0),
((f3(#)g1).t0-(f1(#)g3).t0)*diff(h1,t0) ]|+
|[ h2.t0*diff((f1(#)g2-f2(#)g1),t0),
h3.t0*diff((f2(#)g3-f3(#)g2),t0),
h1.t0*diff((f3(#)g1-f1(#)g3),t0) ]|-
(|[ ((f3(#)g1).t0-(f1(#)g3).t0)*diff(h3,t0),
((f1(#)g2).t0-(f2(#)g1).t0)*diff(h1,t0),
((f2(#)g3).t0-(f3(#)g2).t0)*diff(h2,t0) ]|+
|[ h3.t0*diff((f3(#)g1-f1(#)g3),t0),
h1.t0*diff((f1(#)g2-f2(#)g1),t0),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|) by VALUED_1:5
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3(#)g2).t0)*diff(h3,t0),
((f3(#)g1).t0-(f1(#)g3).t0)*diff(h1,t0) ]|+
|[ h2.t0*diff((f1(#)g2-f2(#)g1),t0),
h3.t0*diff((f2(#)g3-f3(#)g2),t0),
h1.t0*diff((f3(#)g1-f1(#)g3),t0) ]|-
(|[ ((f3(#)g1).t0-(f1(#)g3).t0)*diff(h3,t0),
((f1(#)g2).t0-(f2(#)g1).t0)*diff(h1,t0),
((f2(#)g3).t0-(f3(#)g2).t0)*diff(h2,t0) ]|+
|[ h3.t0*diff((f3(#)g1-f1(#)g3),t0),
h1.t0*diff((f1(#)g2-f2(#)g1),t0),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|) by VALUED_1:5
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3(#)g1).t0-(f1(#)g3).t0)*diff(h1,t0) ]|+
|[ h2.t0*diff((f1(#)g2-f2(#)g1),t0),
h3.t0*diff((f2(#)g3-f3(#)g2),t0),
h1.t0*diff((f3(#)g1-f1(#)g3),t0) ]|-
(|[ ((f3(#)g1).t0-(f1(#)g3).t0)*diff(h3,t0),
((f1(#)g2).t0-(f2(#)g1).t0)*diff(h1,t0),
((f2(#)g3).t0-(f3(#)g2).t0)*diff(h2,t0) ]|+
|[ h3.t0*diff((f3(#)g1-f1(#)g3),t0),
h1.t0*diff((f1(#)g2-f2(#)g1),t0),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|) by VALUED_1:5
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1(#)g3).t0)*diff(h1,t0) ]|+
|[ h2.t0*diff((f1(#)g2-f2(#)g1),t0),
h3.t0*diff((f2(#)g3-f3(#)g2),t0),
h1.t0*diff((f3(#)g1-f1(#)g3),t0) ]|-
(|[ ((f3(#)g1).t0-(f1(#)g3).t0)*diff(h3,t0),
((f1(#)g2).t0-(f2(#)g1).t0)*diff(h1,t0),
((f2(#)g3).t0-(f3(#)g2).t0)*diff(h2,t0) ]|+
|[ h3.t0*diff((f3(#)g1-f1(#)g3),t0),
h1.t0*diff((f1(#)g2-f2(#)g1),t0),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|) by VALUED_1:5
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*diff((f1(#)g2-f2(#)g1),t0),
h3.t0*diff((f2(#)g3-f3(#)g2),t0),
h1.t0*diff((f3(#)g1-f1(#)g3),t0) ]|-
(|[ ((f3(#)g1).t0-(f1(#)g3).t0)*diff(h3,t0),
((f1(#)g2).t0-(f2(#)g1).t0)*diff(h1,t0),
((f2(#)g3).t0-(f3(#)g2).t0)*diff(h2,t0) ]|+
|[ h3.t0*diff((f3(#)g1-f1(#)g3),t0),
h1.t0*diff((f1(#)g2-f2(#)g1),t0),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|) by VALUED_1:5
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*diff((f1(#)g2-f2(#)g1),t0),
h3.t0*diff((f2(#)g3-f3(#)g2),t0),
h1.t0*diff((f3(#)g1-f1(#)g3),t0) ]|-
(|[ ((f3.t0*g1.t0)-(f1(#)g3).t0)*diff(h3,t0),
((f1(#)g2).t0-(f2(#)g1).t0)*diff(h1,t0),
((f2(#)g3).t0-(f3(#)g2).t0)*diff(h2,t0) ]|+
|[ h3.t0*diff((f3(#)g1-f1(#)g3),t0),
h1.t0*diff((f1(#)g2-f2(#)g1),t0),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|) by VALUED_1:5
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*diff((f1(#)g2-f2(#)g1),t0),
h3.t0*diff((f2(#)g3-f3(#)g2),t0),
h1.t0*diff((f3(#)g1-f1(#)g3),t0) ]|-
(|[ ((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h3,t0),
((f1(#)g2).t0-(f2(#)g1).t0)*diff(h1,t0),
((f2(#)g3).t0-(f3(#)g2).t0)*diff(h2,t0) ]|+
|[ h3.t0*diff((f3(#)g1-f1(#)g3),t0),
h1.t0*diff((f1(#)g2-f2(#)g1),t0),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|) by VALUED_1:5
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*diff((f1(#)g2-f2(#)g1),t0),
h3.t0*diff((f2(#)g3-f3(#)g2),t0),
h1.t0*diff((f3(#)g1-f1(#)g3),t0) ]|-
(|[ ((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h3,t0),
((f1.t0*g2.t0)-(f2(#)g1).t0)*diff(h1,t0),
((f2(#)g3).t0-(f3(#)g2).t0)*diff(h2,t0) ]|+
|[ h3.t0*diff((f3(#)g1-f1(#)g3),t0),
h1.t0*diff((f1(#)g2-f2(#)g1),t0),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|) by VALUED_1:5
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*diff((f1(#)g2-f2(#)g1),t0),
h3.t0*diff((f2(#)g3-f3(#)g2),t0),
h1.t0*diff((f3(#)g1-f1(#)g3),t0) ]|-
(|[ ((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h3,t0),
((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h1,t0),
((f2(#)g3).t0-(f3(#)g2).t0)*diff(h2,t0) ]|+
|[ h3.t0*diff((f3(#)g1-f1(#)g3),t0),
h1.t0*diff((f1(#)g2-f2(#)g1),t0),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|) by VALUED_1:5
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*diff((f1(#)g2-f2(#)g1),t0),
h3.t0*diff((f2(#)g3-f3(#)g2),t0),
h1.t0*diff((f3(#)g1-f1(#)g3),t0) ]|-
(|[ ((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h3,t0),
((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h1,t0),
((f2.t0*g3.t0)-(f3(#)g2).t0)*diff(h2,t0) ]|+
|[ h3.t0*diff((f3(#)g1-f1(#)g3),t0),
h1.t0*diff((f1(#)g2-f2(#)g1),t0),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|) by VALUED_1:5
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*diff((f1(#)g2-f2(#)g1),t0),
h3.t0*diff((f2(#)g3-f3(#)g2),t0),
h1.t0*diff((f3(#)g1-f1(#)g3),t0) ]|-
(|[ ((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h3,t0),
((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h1,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h2,t0) ]|+
|[ h3.t0*diff((f3(#)g1-f1(#)g3),t0),
h1.t0*diff((f1(#)g2-f2(#)g1),t0),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|) by VALUED_1:5
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*(diff(f1(#)g2,t0)-diff(f2(#)g1,t0)),
h3.t0*diff((f2(#)g3-f3(#)g2),t0),
h1.t0*diff((f3(#)g1-f1(#)g3),t0) ]|-
(|[ ((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h3,t0),
((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h1,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h2,t0) ]|+
|[ h3.t0*diff((f3(#)g1-f1(#)g3),t0),
h1.t0*diff((f1(#)g2-f2(#)g1),t0),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|) by A4,FDIFF_1:14
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*(diff(f1(#)g2,t0)-diff(f2(#)g1,t0)),
h3.t0*(diff(f2(#)g3,t0)-diff(f3(#)g2,t0)),
h1.t0*diff((f3(#)g1-f1(#)g3),t0) ]|-
(|[ ((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h3,t0),
((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h1,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h2,t0) ]|+
|[ h3.t0*diff((f3(#)g1-f1(#)g3),t0),
h1.t0*diff((f1(#)g2-f2(#)g1),t0),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|) by A4,FDIFF_1:14
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*(diff(f1(#)g2,t0)-diff(f2(#)g1,t0)),
h3.t0*(diff(f2(#)g3,t0)-diff(f3(#)g2,t0)),
h1.t0*(diff(f3(#)g1,t0)-diff(f1(#)g3,t0)) ]|-
(|[ ((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h3,t0),
((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h1,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h2,t0) ]|+
|[ h3.t0*diff((f3(#)g1-f1(#)g3),t0),
h1.t0*diff((f1(#)g2-f2(#)g1),t0),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|) by A4,FDIFF_1:14
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*(diff(f1(#)g2,t0)-diff(f2(#)g1,t0)),
h3.t0*(diff(f2(#)g3,t0)-diff(f3(#)g2,t0)),
h1.t0*(diff(f3(#)g1,t0)-diff(f1(#)g3,t0)) ]|-
(|[ ((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h3,t0),
((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h1,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h2,t0) ]|+
|[ h3.t0*(diff(f3(#)g1,t0)-diff(f1(#)g3,t0)),
h1.t0*diff((f1(#)g2-f2(#)g1),t0),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|) by A4,FDIFF_1:14
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*(diff(f1(#)g2,t0)-diff(f2(#)g1,t0)),
h3.t0*(diff(f2(#)g3,t0)-diff(f3(#)g2,t0)),
h1.t0*(diff(f3(#)g1,t0)-diff(f1(#)g3,t0)) ]|-
(|[ ((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h3,t0),
((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h1,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h2,t0) ]|+
|[ h3.t0*(diff(f3(#)g1,t0)-diff(f1(#)g3,t0)),
h1.t0*(diff(f1(#)g2,t0)-diff(f2(#)g1,t0)),
h2.t0*diff((f2(#)g3-f3(#)g2),t0) ]|) by A4,FDIFF_1:14
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*(diff(f1(#)g2,t0)-diff(f2(#)g1,t0)),
h3.t0*(diff(f2(#)g3,t0)-diff(f3(#)g2,t0)),
h1.t0*(diff(f3(#)g1,t0)-diff(f1(#)g3,t0)) ]|-
(|[ ((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h3,t0),
((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h1,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h2,t0) ]|+
|[ h3.t0*(diff(f3(#)g1,t0)-diff(f1(#)g3,t0)),
h1.t0*(diff(f1(#)g2,t0)-diff(f2(#)g1,t0)),
h2.t0*(diff(f2(#)g3,t0)-diff(f3(#)g2,t0)) ]|) by A4,FDIFF_1:14
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-diff(f2(#)g1,t0)),
h3.t0*(diff(f2(#)g3,t0)-diff(f3(#)g2,t0)),
h1.t0*(diff(f3(#)g1,t0)-diff(f1(#)g3,t0)) ]|-
(|[ ((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h3,t0),
((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h1,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h2,t0) ]|+
|[ h3.t0*(diff(f3(#)g1,t0)-diff(f1(#)g3,t0)),
h1.t0*(diff(f1(#)g2,t0)-diff(f2(#)g1,t0)),
h2.t0*(diff(f2(#)g3,t0)-diff(f3(#)g2,t0)) ]|) by A1,A2,FDIFF_1:16
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-((g1.t0)*diff(f2,t0)+(f2.t0)*diff(g1,t0))),
h3.t0*(diff(f2(#)g3,t0)-diff(f3(#)g2,t0)),
h1.t0*(diff(f3(#)g1,t0)-diff(f1(#)g3,t0)) ]|-
(|[ ((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h3,t0),
((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h1,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h2,t0) ]|+
|[ h3.t0*(diff(f3(#)g1,t0)-diff(f1(#)g3,t0)),
h1.t0*(diff(f1(#)g2,t0)-diff(f2(#)g1,t0)),
h2.t0*(diff(f2(#)g3,t0)-diff(f3(#)g2,t0)) ]|) by A1,A2,FDIFF_1:16
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-((g1.t0)*diff(f2,t0)+(f2.t0)*diff(g1,t0))),
h3.t0*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-diff(f3(#)g2,t0)),
h1.t0*(diff(f3(#)g1,t0)-diff(f1(#)g3,t0)) ]|-
(|[ ((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h3,t0),
((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h1,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h2,t0) ]|+
|[ h3.t0*(diff(f3(#)g1,t0)-diff(f1(#)g3,t0)),
h1.t0*(diff(f1(#)g2,t0)-diff(f2(#)g1,t0)),
h2.t0*(diff(f2(#)g3,t0)-diff(f3(#)g2,t0)) ]|) by A1,A2,FDIFF_1:16
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-((g1.t0)*diff(f2,t0)+(f2.t0)*diff(g1,t0))),
h3.t0*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-((g2.t0)*diff(f3,t0)+(f3.t0)*diff(g2,t0))),
h1.t0*(diff(f3(#)g1,t0)-diff(f1(#)g3,t0)) ]|-
(|[ ((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h3,t0),
((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h1,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h2,t0) ]|+
|[ h3.t0*(diff(f3(#)g1,t0)-diff(f1(#)g3,t0)),
h1.t0*(diff(f1(#)g2,t0)-diff(f2(#)g1,t0)),
h2.t0*(diff(f2(#)g3,t0)-diff(f3(#)g2,t0)) ]|) by A1,A2,FDIFF_1:16
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-((g1.t0)*diff(f2,t0)+(f2.t0)*diff(g1,t0))),
h3.t0*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-((g2.t0)*diff(f3,t0)+(f3.t0)*diff(g2,t0))),
h1.t0*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-diff(f1(#)g3,t0)) ]|-
(|[ ((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h3,t0),
((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h1,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h2,t0) ]|+
|[ h3.t0*(diff(f3(#)g1,t0)-diff(f1(#)g3,t0)),
h1.t0*(diff(f1(#)g2,t0)-diff(f2(#)g1,t0)),
h2.t0*(diff(f2(#)g3,t0)-diff(f3(#)g2,t0)) ]|) by A1,A2,FDIFF_1:16
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-((g1.t0)*diff(f2,t0)+(f2.t0)*diff(g1,t0))),
h3.t0*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-((g2.t0)*diff(f3,t0)+(f3.t0)*diff(g2,t0))),
h1.t0*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-((g3.t0)*diff(f1,t0)+(f1.t0)*diff(g3,t0))) ]|-
(|[ ((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h3,t0),
((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h1,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h2,t0) ]|+
|[ h3.t0*(diff(f3(#)g1,t0)-diff(f1(#)g3,t0)),
h1.t0*(diff(f1(#)g2,t0)-diff(f2(#)g1,t0)),
h2.t0*(diff(f2(#)g3,t0)-diff(f3(#)g2,t0)) ]|) by A1,A2,FDIFF_1:16
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-((g1.t0)*diff(f2,t0)+(f2.t0)*diff(g1,t0))),
h3.t0*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-((g2.t0)*diff(f3,t0)+(f3.t0)*diff(g2,t0))),
h1.t0*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-((g3.t0)*diff(f1,t0)+(f1.t0)*diff(g3,t0))) ]|-
(|[ ((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h3,t0),
((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h1,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h2,t0) ]|+
|[ h3.t0*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-diff(f1(#)g3,t0)),
h1.t0*(diff(f1(#)g2,t0)-diff(f2(#)g1,t0)),
h2.t0*(diff(f2(#)g3,t0)-diff(f3(#)g2,t0)) ]|) by A1,A2,FDIFF_1:16
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-((g1.t0)*diff(f2,t0)+(f2.t0)*diff(g1,t0))),
h3.t0*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-((g2.t0)*diff(f3,t0)+(f3.t0)*diff(g2,t0))),
h1.t0*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-((g3.t0)*diff(f1,t0)+(f1.t0)*diff(g3,t0))) ]|-
(|[ ((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h3,t0),
((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h1,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h2,t0) ]|+
|[ h3.t0*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-((g3.t0)*diff(f1,t0)+(f1.t0)*diff(g3,t0))),
h1.t0*(diff(f1(#)g2,t0)-diff(f2(#)g1,t0)),
h2.t0*(diff(f2(#)g3,t0)-diff(f3(#)g2,t0)) ]|) by A1,A2,FDIFF_1:16
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-((g1.t0)*diff(f2,t0)+(f2.t0)*diff(g1,t0))),
h3.t0*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-((g2.t0)*diff(f3,t0)+(f3.t0)*diff(g2,t0))),
h1.t0*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-((g3.t0)*diff(f1,t0)+(f1.t0)*diff(g3,t0))) ]|-
(|[ ((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h3,t0),
((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h1,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h2,t0) ]|+
|[ h3.t0*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-((g3.t0)*diff(f1,t0)+(f1.t0)*diff(g3,t0))),
h1.t0*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-diff(f2(#)g1,t0)),
h2.t0*(diff(f2(#)g3,t0)-diff(f3(#)g2,t0)) ]|) by A1,A2,FDIFF_1:16
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-((g1.t0)*diff(f2,t0)+(f2.t0)*diff(g1,t0))),
h3.t0*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-((g2.t0)*diff(f3,t0)+(f3.t0)*diff(g2,t0))),
h1.t0*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-((g3.t0)*diff(f1,t0)+(f1.t0)*diff(g3,t0))) ]|-
(|[ ((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h3,t0),
((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h1,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h2,t0) ]|+
|[ h3.t0*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-((g3.t0)*diff(f1,t0)+(f1.t0)*diff(g3,t0))),
h1.t0*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-((g1.t0)*diff(f2,t0)+(f2.t0)*diff(g1,t0))),
h2.t0*(diff(f2(#)g3,t0)-diff(f3(#)g2,t0)) ]|)
by A1,A2,FDIFF_1:16
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-((g1.t0)*diff(f2,t0)+(f2.t0)*diff(g1,t0))),
h3.t0*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-((g2.t0)*diff(f3,t0)+(f3.t0)*diff(g2,t0))),
h1.t0*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-((g3.t0)*diff(f1,t0)+(f1.t0)*diff(g3,t0))) ]|-
(|[ ((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h3,t0),
((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h1,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h2,t0) ]|+
|[ h3.t0*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-((g3.t0)*diff(f1,t0)+(f1.t0)*diff(g3,t0))),
h1.t0*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-((g1.t0)*diff(f2,t0)+(f2.t0)*diff(g1,t0))),
h2.t0*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-diff(f3(#)g2,t0)) ]|) by A1,A2,FDIFF_1:16
.= |[ ((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h2,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h3,t0),
((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h1,t0) ]|+
|[ h2.t0*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-((g1.t0)*diff(f2,t0)+(f2.t0)*diff(g1,t0))),
h3.t0*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-((g2.t0)*diff(f3,t0)+(f3.t0)*diff(g2,t0))),
h1.t0*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-((g3.t0)*diff(f1,t0)+(f1.t0)*diff(g3,t0))) ]|-
(|[ ((f3.t0*g1.t0)-(f1.t0*g3.t0))*diff(h3,t0),
((f1.t0*g2.t0)-(f2.t0*g1.t0))*diff(h1,t0),
((f2.t0*g3.t0)-(f3.t0*g2.t0))*diff(h2,t0) ]|+
|[ h3.t0*((g1.t0)*diff(f3,t0)+(f3.t0)*diff(g1,t0)
-((g3.t0)*diff(f1,t0)+(f1.t0)*diff(g3,t0))),
h1.t0*((g2.t0)*diff(f1,t0)+(f1.t0)*diff(g2,t0)
-((g1.t0)*diff(f2,t0)+(f2.t0)*diff(g1,t0))),
h2.t0*((g3.t0)*diff(f2,t0)+(f2.t0)*diff(g3,t0)
-((g2.t0)*diff(f3,t0)+(f3.t0)*diff(g2,t0))) ]|)
by A1,A2,FDIFF_1:16
.= |[ (h2.t0)*((f1.t0)*diff(g2,t0)-(f2.t0)*diff(g1,t0))+
(h2.t0)*(diff(f1,t0)*(g2.t0)-diff(f2,t0)*(g1.t0)),
(h3.t0)*((f2.t0)*diff(g3,t0)-(f3.t0)*diff(g2,t0))+
(h3.t0)*(diff(f2,t0)*(g3.t0)-diff(f3,t0)*(g2.t0)),
(h1.t0)*((f3.t0)*diff(g1,t0)-(f1.t0)*diff(g3,t0))+
(h1.t0)*(diff(f3,t0)*(g1.t0)-diff(f1,t0)*(g3.t0)) ]|+
|[ diff(h2,t0)*((f1.t0)*(g2.t0)-(f2.t0)*(g1.t0)),
diff(h3,t0)*((f2.t0)*(g3.t0)-(f3.t0)*(g2.t0)),
diff(h1,t0)*((f3.t0)*(g1.t0)-(f1.t0)*(g3.t0)) ]|-
|[ diff(h3,t0)*((f3.t0)*(g1.t0)-(f1.t0)*(g3.t0)),
diff(h1,t0)*((f1.t0)*(g2.t0)-(f2.t0)*(g1.t0)),
diff(h2,t0)*((f2.t0)*(g3.t0)-(f3.t0)*(g2.t0)) ]|-
|[ (h3.t0)*((f3.t0)*diff(g1,t0)-(f1.t0)*diff(g3,t0))+
(h3.t0)*(diff(f3,t0)*(g1.t0)-diff(f1,t0)*(g3.t0)),
(h1.t0)*((f1.t0)*diff(g2,t0)-(f2.t0)*diff(g1,t0))+
(h1.t0)*(diff(f1,t0)*(g2.t0)-diff(f2,t0)*(g1.t0)),
(h2.t0)*((g3.t0)*diff(f2,t0)-(g2.t0)*diff(f3,t0))+
(h2.t0)*((f2.t0)*diff(g3,t0)-(f3.t0)*diff(g2,t0)) ]| by RVSUM_1:39
.= |[ (h2.t0)*((f1.t0)*diff(g2,t0)-(f2.t0)*diff(g1,t0))+
(h2.t0)*(diff(f1,t0)*(g2.t0)-diff(f2,t0)*(g1.t0)),
(h3.t0)*((f2.t0)*diff(g3,t0)-(f3.t0)*diff(g2,t0))+
(h3.t0)*(diff(f2,t0)*(g3.t0)-diff(f3,t0)*(g2.t0)),
(h1.t0)*((f3.t0)*diff(g1,t0)-(f1.t0)*diff(g3,t0))+
(h1.t0)*(diff(f3,t0)*(g1.t0)-diff(f1,t0)*(g3.t0)) ]|+
(|[ diff(h2,t0)*((f1.t0)*(g2.t0)-(f2.t0)*(g1.t0)),
diff(h3,t0)*((f2.t0)*(g3.t0)-(f3.t0)*(g2.t0)),
diff(h1,t0)*((f3.t0)*(g1.t0)-(f1.t0)*(g3.t0)) ]|-
|[ diff(h3,t0)*((f3.t0)*(g1.t0)-(f1.t0)*(g3.t0)),
diff(h1,t0)*((f1.t0)*(g2.t0)-(f2.t0)*(g1.t0)),
diff(h2,t0)*((f2.t0)*(g3.t0)-(f3.t0)*(g2.t0)) ]|)-
|[ (h3.t0)*((f3.t0)*diff(g1,t0)-(f1.t0)*diff(g3,t0))+
(h3.t0)*(diff(f3,t0)*(g1.t0)-diff(f1,t0)*(g3.t0)),
(h1.t0)*((f1.t0)*diff(g2,t0)-(f2.t0)*diff(g1,t0))+
(h1.t0)*(diff(f1,t0)*(g2.t0)-diff(f2,t0)*(g1.t0)),
(h2.t0)*((g3.t0)*diff(f2,t0)-(g2.t0)*diff(f3,t0))+
(h2.t0)*((f2.t0)*diff(g3,t0)-(f3.t0)*diff(g2,t0)) ]| by RVSUM_1:15
.= |[ (h2.t0)*((f1.t0)*diff(g2,t0)-(f2.t0)*diff(g1,t0))+
(h2.t0)*(diff(f1,t0)*(g2.t0)-diff(f2,t0)*(g1.t0)),
(h3.t0)*((f2.t0)*diff(g3,t0)-(f3.t0)*diff(g2,t0))+
(h3.t0)*(diff(f2,t0)*(g3.t0)-diff(f3,t0)*(g2.t0)),
(h1.t0)*((f3.t0)*diff(g1,t0)-(f1.t0)*diff(g3,t0))+
(h1.t0)*(diff(f3,t0)*(g1.t0)-diff(f1,t0)*(g3.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)) ]|-
|[ (h3.t0)*((f3.t0)*diff(g1,t0)-(f1.t0)*diff(g3,t0))+
(h3.t0)*(diff(f3,t0)*(g1.t0)-diff(f1,t0)*(g3.t0)),
(h1.t0)*((f1.t0)*diff(g2,t0)-(f2.t0)*diff(g1,t0))+
(h1.t0)*(diff(f1,t0)*(g2.t0)-diff(f2,t0)*(g1.t0)),
(h2.t0)*((g3.t0)*diff(f2,t0)-(g2.t0)*diff(f3,t0))+
(h2.t0)*((f2.t0)*diff(g3,t0)-(f3.t0)*diff(g2,t0)) ]| by Lm11
.= |[ (h2.t0)*((f1.t0)*diff(g2,t0)-(f2.t0)*diff(g1,t0))+
(h2.t0)*(diff(f1,t0)*(g2.t0)-diff(f2,t0)*(g1.t0)),
(h3.t0)*((f2.t0)*diff(g3,t0)-(f3.t0)*diff(g2,t0))+
(h3.t0)*(diff(f2,t0)*(g3.t0)-diff(f3,t0)*(g2.t0)),
(h1.t0)*((f3.t0)*diff(g1,t0)-(f1.t0)*diff(g3,t0))+
(h1.t0)*(diff(f3,t0)*(g1.t0)-diff(f1,t0)*(g3.t0)) ]|-
|[ (h3.t0)*((f3.t0)*diff(g1,t0)-(f1.t0)*diff(g3,t0))+
(h3.t0)*(diff(f3,t0)*(g1.t0)-diff(f1,t0)*(g3.t0)),
(h1.t0)*((f1.t0)*diff(g2,t0)-(f2.t0)*diff(g1,t0))+
(h1.t0)*(diff(f1,t0)*(g2.t0)-diff(f2,t0)*(g1.t0)),
(h2.t0)*((g3.t0)*diff(f2,t0)-(g2.t0)*diff(f3,t0))+
(h2.t0)*((f2.t0)*diff(g3,t0)-(f3.t0)*diff(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)) ]| by RVSUM_1:15
.= |[ (h2.t0)*((f1.t0)*diff(g2,t0)-(f2.t0)*diff(g1,t0))+
(h2.t0)*(diff(f1,t0)*(g2.t0)-diff(f2,t0)*(g1.t0))-
((h3.t0)*((f3.t0)*diff(g1,t0)-(f1.t0)*diff(g3,t0))+
(h3.t0)*(diff(f3,t0)*(g1.t0)-diff(f1,t0)*(g3.t0))),
(h3.t0)*((f2.t0)*diff(g3,t0)-(f3.t0)*diff(g2,t0))+
(h3.t0)*(diff(f2,t0)*(g3.t0)-diff(f3,t0)*(g2.t0))-
((h1.t0)*((f1.t0)*diff(g2,t0)-(f2.t0)*diff(g1,t0))+
(h1.t0)*(diff(f1,t0)*(g2.t0)-diff(f2,t0)*(g1.t0))),
(h1.t0)*((f3.t0)*diff(g1,t0)-(f1.t0)*diff(g3,t0))+
(h1.t0)*(diff(f3,t0)*(g1.t0)-diff(f1,t0)*(g3.t0))-
((h2.t0)*((g3.t0)*diff(f2,t0)-(g2.t0)*diff(f3,t0))+
(h2.t0)*((f2.t0)*diff(g3,t0)-(f3.t0)*diff(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)) ]| by Lm11
.= |[ ((h2.t0)*((f1.t0)*diff(g2,t0)-(f2.t0)*diff(g1,t0))-
(h3.t0)*((f3.t0)*diff(g1,t0)-(f1.t0)*diff(g3,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)*((f2.t0)*diff(g3,t0)-(f3.t0)*diff(g2,t0))-
(h1.t0)*((f1.t0)*diff(g2,t0)-(f2.t0)*diff(g1,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)*((f3.t0)*diff(g1,t0)-(f1.t0)*diff(g3,t0))-
(h2.t0)*((f2.t0)*diff(g3,t0)-(f3.t0)*diff(g2,t0)))+
((h1.t0)*(diff(f3,t0)*(g1.t0)-diff(f1,t0)*(g3.t0))-
(h2.t0)*((g3.t0)*diff(f2,t0)-(g2.t0)*diff(f3,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)) ]|
.= |[ (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)) ]| by Lm8;
hence thesis;
end;