:: Vector Function and its Differentiation Formulas in 3-dimensional Euclidean Spaces
:: by Xiquan Liang , Piqing Zhao and Ou Bai
::
:: Received October 10, 2009
:: Copyright (c) 2009-2021 Association of Mizar Users


definition
let x, y, z be Real;
:: original: <*
redefine func |[x,y,z]| -> Element of REAL 3;
coherence
<*x,y,z*> is Element of REAL 3
proof end;
end;

theorem Th1: :: EUCLID_8:1
for p being Element of REAL 3 holds p = |[(p . 1),(p . 2),(p . 3)]|
proof end;

Lm1: for p being Element of REAL 3
for r being Real holds r * p = |[(r * (p . 1)),(r * (p . 2)),(r * (p . 3))]|
proof end;

Lm2: for p1, p2 being Element of REAL 3 holds p1 + p2 = |[((p1 . 1) + (p2 . 1)),((p1 . 2) + (p2 . 2)),((p1 . 3) + (p2 . 3))]|
proof end;

Lm3: for p being Element of REAL 3 holds
( (- p) . 1 = - (p . 1) & (- p) . 2 = - (p . 2) & (- p) . 3 = - (p . 3) )
proof end;

theorem :: EUCLID_8:2
for f being FinSequence of REAL st len f = 3 holds
f is Element of REAL 3
proof end;

Lm4: for p1, p2 being Element of REAL 3 holds p1 - p2 = |[((p1 . 1) - (p2 . 1)),((p1 . 2) - (p2 . 2)),((p1 . 3) - (p2 . 3))]|
proof end;

Lm5: for p1, p2 being Element of REAL 3 holds |(p1,p2)| = (((p1 . 1) * (p2 . 1)) + ((p1 . 2) * (p2 . 2))) + ((p1 . 3) * (p2 . 3))
proof end;

Lm6: for r, x, y, z being Real holds r * |[x,y,z]| = |[(r * x),(r * y),(r * z)]|
proof end;

Lm7: for p1, p2 being Element of REAL 3 holds p1 + (- p2) = |[((p1 . 1) - (p2 . 1)),((p1 . 2) - (p2 . 2)),((p1 . 3) - (p2 . 3))]|
proof end;

Lm8: for x1, x2, x3, y1, y2, y3 being Real holds |[x1,x2,x3]| + |[y1,y2,y3]| = |[(x1 + y1),(x2 + y2),(x3 + y3)]|
proof end;

Lm9: for p1, p2, q1, q2 being Element of REAL 3 holds (p1 + p2) + (q1 + q2) = (p1 + q1) + (p2 + q2)
proof end;

Lm10: for p1, p2, q1, q2 being Element of REAL 3 holds (p1 + p2) - (q1 + q2) = (p1 - q1) + (p2 - q2)
proof end;

Lm11: for x1, x2, x3, y1, y2, y3 being Real holds |[x1,x2,x3]| - |[y1,y2,y3]| = |[(x1 - y1),(x2 - y2),(x3 - y3)]|
proof end;

definition
func <e1> -> Element of REAL 3 equals :: EUCLID_8:def 1
|[1,0,0]|;
coherence
|[1,0,0]| is Element of REAL 3 ;
func <e2> -> Element of REAL 3 equals :: EUCLID_8:def 2
|[0,1,0]|;
coherence
|[0,1,0]| is Element of REAL 3 ;
func <e3> -> Element of REAL 3 equals :: EUCLID_8:def 3
|[0,0,1]|;
coherence
|[0,0,1]| is Element of REAL 3 ;
end;

:: deftheorem defines <e1> EUCLID_8:def 1 :
<e1> = |[1,0,0]|;

:: deftheorem defines <e2> EUCLID_8:def 2 :
<e2> = |[0,1,0]|;

:: deftheorem defines <e3> EUCLID_8:def 3 :
<e3> = |[0,0,1]|;

Lm12: for x, y, z being Real
for p being Element of REAL 3 st p = |[x,y,z]| holds
|(p,p)| = ((x ^2) + (y ^2)) + (z ^2)
proof end;

definition
let p1, p2 be Element of REAL 3;
func p1 <X> p2 -> Element of REAL 3 equals :: EUCLID_8:def 4
|[(((p1 . 2) * (p2 . 3)) - ((p1 . 3) * (p2 . 2))),(((p1 . 3) * (p2 . 1)) - ((p1 . 1) * (p2 . 3))),(((p1 . 1) * (p2 . 2)) - ((p1 . 2) * (p2 . 1)))]|;
correctness
coherence
|[(((p1 . 2) * (p2 . 3)) - ((p1 . 3) * (p2 . 2))),(((p1 . 3) * (p2 . 1)) - ((p1 . 1) * (p2 . 3))),(((p1 . 1) * (p2 . 2)) - ((p1 . 2) * (p2 . 1)))]| is Element of REAL 3;
;
end;

:: deftheorem defines <X> EUCLID_8:def 4 :
for p1, p2 being Element of REAL 3 holds p1 <X> p2 = |[(((p1 . 2) * (p2 . 3)) - ((p1 . 3) * (p2 . 2))),(((p1 . 3) * (p2 . 1)) - ((p1 . 1) * (p2 . 3))),(((p1 . 1) * (p2 . 2)) - ((p1 . 2) * (p2 . 1)))]|;

Lm13: for x1, x2, x3, y1, y2, y3 being Real holds |[x1,x2,x3]| <X> |[y1,y2,y3]| = |[((x2 * y3) - (x3 * y2)),((x3 * y1) - (x1 * y3)),((x1 * y2) - (x2 * y1))]|
proof end;

Lm14: for r being Real
for p1, p2 being Element of REAL 3 holds
( (r * p1) <X> p2 = r * (p1 <X> p2) & (r * p1) <X> p2 = p1 <X> (r * p2) )
proof end;

theorem :: EUCLID_8:3
for p1, p2 being Element of REAL 3 st p1,p2 are_ldependent2 holds
p1 <X> p2 = 0.REAL 3
proof end;

theorem :: EUCLID_8:4
|.<e1>.| = 1
proof end;

theorem :: EUCLID_8:5
|.<e2>.| = 1
proof end;

theorem :: EUCLID_8:6
|.<e3>.| = 1
proof end;

theorem :: EUCLID_8:7
<e1> , <e2> are_orthogonal
proof end;

theorem :: EUCLID_8:8
<e1> , <e3> are_orthogonal
proof end;

theorem :: EUCLID_8:9
<e2> , <e3> are_orthogonal
proof end;

theorem :: EUCLID_8:10
|(<e1>,<e1>)| = 1
proof end;

theorem :: EUCLID_8:11
|(<e2>,<e2>)| = 1
proof end;

theorem :: EUCLID_8:12
|(<e3>,<e3>)| = 1
proof end;

theorem Th13: :: EUCLID_8:13
for p being Element of REAL 3 holds |(p,|[0,0,0]|)| = 0
proof end;

theorem :: EUCLID_8:14
canceled;

theorem :: EUCLID_8:15
canceled;

::$CT 2
theorem :: EUCLID_8:16
<e1> <X> <e2> = <e3>
proof end;

theorem :: EUCLID_8:17
<e2> <X> <e3> = <e1>
proof end;

theorem :: EUCLID_8:18
<e3> <X> <e1> = <e2>
proof end;

theorem :: EUCLID_8:19
<e3> <X> <e2> = - <e1>
proof end;

theorem :: EUCLID_8:20
<e1> <X> <e3> = - <e2>
proof end;

theorem :: EUCLID_8:21
<e2> <X> <e1> = - <e3>
proof end;

theorem :: EUCLID_8:22
for p being Element of REAL 3 holds p <X> |[0,0,0]| = |[0,0,0]|
proof end;

theorem :: EUCLID_8:23
canceled;

theorem :: EUCLID_8:24
canceled;

::$CT 2
theorem Th21: :: EUCLID_8:25
for r being Real holds r * <e1> = |[r,0,0]|
proof end;

theorem Th22: :: EUCLID_8:26
for r being Real holds r * <e2> = |[0,r,0]|
proof end;

theorem Th23: :: EUCLID_8:27
for r being Real holds r * <e3> = |[0,0,r]|
proof end;

theorem :: EUCLID_8:28
for p being Element of REAL 3 holds 1 * p = p by RFUNCT_1:21;

theorem :: EUCLID_8:29
canceled;

theorem :: EUCLID_8:30
canceled;

::$CT 2
theorem :: EUCLID_8:31
- <e1> = |[(- 1),0,0]|
proof end;

theorem :: EUCLID_8:32
- <e2> = |[0,(- 1),0]|
proof end;

theorem :: EUCLID_8:33
- <e3> = |[0,0,(- 1)]|
proof end;

theorem :: EUCLID_8:34
for p being Element of REAL 3 holds 0 * p = |[0,0,0]|
proof end;

theorem :: EUCLID_8:35
canceled;

theorem :: EUCLID_8:36
canceled;

::$CT 2
theorem :: EUCLID_8:37
for p being Element of REAL 3 holds p = (((p . 1) * <e1>) + ((p . 2) * <e2>)) + ((p . 3) * <e3>)
proof end;

theorem Th30: :: EUCLID_8:38
for r being Real
for p being Element of REAL 3 holds r * p = (((r * (p . 1)) * <e1>) + ((r * (p . 2)) * <e2>)) + ((r * (p . 3)) * <e3>)
proof end;

theorem Th31: :: EUCLID_8:39
for x, y, z being Real holds |[x,y,z]| = ((x * <e1>) + (y * <e2>)) + (z * <e3>)
proof end;

theorem Th32: :: EUCLID_8:40
for r, x, y, z being Real holds r * |[x,y,z]| = (((r * x) * <e1>) + ((r * y) * <e2>)) + ((r * z) * <e3>)
proof end;

theorem :: EUCLID_8:41
for p being Element of REAL 3 holds - p = ((- ((p . 1) * <e1>)) - ((p . 2) * <e2>)) - ((p . 3) * <e3>)
proof end;

theorem :: EUCLID_8:42
for x, y, z being Real holds - |[x,y,z]| = ((- (x * <e1>)) - (y * <e2>)) - (z * <e3>)
proof end;

theorem :: EUCLID_8:43
for p1, p2 being Element of REAL 3 holds p1 + p2 = ((((p1 . 1) + (p2 . 1)) * <e1>) + (((p1 . 2) + (p2 . 2)) * <e2>)) + (((p1 . 3) + (p2 . 3)) * <e3>)
proof end;

theorem Th36: :: EUCLID_8:44
for p1, p2 being Element of REAL 3 holds p1 - p2 = ((((p1 . 1) - (p2 . 1)) * <e1>) + (((p1 . 2) - (p2 . 2)) * <e2>)) + (((p1 . 3) - (p2 . 3)) * <e3>)
proof end;

theorem :: EUCLID_8:45
for x1, x2, x3, y1, y2, y3 being Real holds |[x1,x2,x3]| + |[y1,y2,y3]| = (((x1 + y1) * <e1>) + ((x2 + y2) * <e2>)) + ((x3 + y3) * <e3>)
proof end;

theorem :: EUCLID_8:46
for x1, x2, x3, y1, y2, y3 being Real holds |[x1,x2,x3]| - |[y1,y2,y3]| = (((x1 - y1) * <e1>) + ((x2 - y2) * <e2>)) + ((x3 - y3) * <e3>)
proof end;

theorem :: EUCLID_8:47
for p1, p2, p3 being Element of REAL 3 holds
( (((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 end;

definition
let f1, f2, f3 be PartFunc of REAL,REAL;
func VFunc (f1,f2,f3) -> Function of REAL,(REAL 3) means :Def5: :: EUCLID_8:def 5
 for t being Real holds it . t = |[(f1 . t),(f2 . t),(f3 . t)]|;
existence
ex b1 being Function of REAL,(REAL 3) st
for t being Real holds b1 . t = |[(f1 . t),(f2 . t),(f3 . t)]|
proof end;
uniqueness
for b1, b2 being Function of REAL,(REAL 3) st ( for t being Real holds b1 . t = |[(f1 . t),(f2 . t),(f3 . t)]| ) & ( for t being Real holds b2 . t = |[(f1 . t),(f2 . t),(f3 . t)]| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines VFunc EUCLID_8:def 5 :
for f1, f2, f3 being PartFunc of REAL,REAL
for b4 being Function of REAL,(REAL 3) holds
( b4 = VFunc (f1,f2,f3) iff for t being Real holds b4 . t = |[(f1 . t),(f2 . t),(f3 . t)]| );

theorem :: EUCLID_8:48
for f1, f2, f3 being PartFunc of REAL,REAL
for t being Real holds (VFunc (f1,f2,f3)) . t = (((f1 . t) * <e1>) + ((f2 . t) * <e2>)) + ((f3 . t) * <e3>)
proof end;

theorem Th41: :: EUCLID_8:49
for p being Element of REAL 3
for f1, f2, f3 being PartFunc of REAL,REAL
for t being Real holds
( p = (VFunc (f1,f2,f3)) . t iff ( p . 1 = f1 . t & p . 2 = f2 . t & p . 3 = f3 . t ) )
proof end;

theorem Th42: :: EUCLID_8:50
for p being Element of REAL 3 holds
( len p = 3 & dom p = Seg 3 )
proof end;

theorem Th43: :: EUCLID_8:51
for p, q being Element of REAL 3 holds mlt (p,q) = <*((p . 1) * (q . 1)),((p . 2) * (q . 2)),((p . 3) * (q . 3))*>
proof end;

theorem :: EUCLID_8:52
for r being Real
for p being Element of REAL 3 holds r * p = |[(r * (p . 1)),(r * (p . 2)),(r * (p . 3))]| by Lm1;

theorem :: EUCLID_8:53
canceled;

::$CT
theorem :: EUCLID_8:54
for p being Element of REAL 3 holds len (- p) = len p
proof end;

theorem :: EUCLID_8:55
for p, q being Element of REAL 3 holds p + q = |[((p . 1) + (q . 1)),((p . 2) + (q . 2)),((p . 3) + (q . 3))]| by Lm2;

theorem :: EUCLID_8:56
for p, q being Element of REAL 3
for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL
for t1, t2 being Real st p = (VFunc (f1,f2,f3)) . t1 & q = (VFunc (g1,g2,g3)) . t2 & p = q holds
( f1 . t1 = g1 . t2 & f2 . t1 = g2 . t2 & f3 . t1 = g3 . t2 )
proof end;

theorem :: EUCLID_8:57
for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL
for t1, t2 being Real st f1 . t1 = g1 . t2 & f2 . t1 = g2 . t2 & f3 . t1 = g3 . t2 holds
(VFunc (f1,f2,f3)) . t1 = (VFunc (g1,g2,g3)) . t2
proof end;

theorem Th49: :: EUCLID_8:58
for p being Element of REAL 3
for r being Real holds r * p = |[(r * (p . 1)),(r * (p . 2)),(r * (p . 3))]|
proof end;

theorem Th50: :: EUCLID_8:59
for x, y, z, r being Real holds r * |[x,y,z]| = |[(r * x),(r * y),(r * z)]|
proof end;

theorem Th51: :: EUCLID_8:60
for p being Element of REAL 3 holds - p = |[(- (p . 1)),(- (p . 2)),(- (p . 3))]|
proof end;

theorem Th52: :: EUCLID_8:61
for p being Element of REAL 3 holds
( (- p) . 1 = - (p . 1) & (- p) . 2 = - (p . 2) & (- p) . 3 = - (p . 3) )
proof end;

theorem :: EUCLID_8:62
for p1, p2 being Element of REAL 3 holds p1 - p2 = |[((p1 . 1) - (p2 . 1)),((p1 . 2) - (p2 . 2)),((p1 . 3) - (p2 . 3))]|
proof end;

theorem :: EUCLID_8:63
for p, q being Element of REAL 3 holds |(p,q)| = (((p . 1) * (q . 1)) + ((p . 2) * (q . 2))) + ((p . 3) * (q . 3)) by Lm5;

theorem Th55: :: EUCLID_8:64
for p being Element of REAL 3 holds |(p,p)| = (((p . 1) ^2) + ((p . 2) ^2)) + ((p . 3) ^2)
proof end;

theorem Th56: :: EUCLID_8:65
for p being Element of REAL 3 holds |.p.| = sqrt ((((p . 1) ^2) + ((p . 2) ^2)) + ((p . 3) ^2))
proof end;

theorem :: EUCLID_8:66
for r being Real
for p being Element of REAL 3 holds |.(r * p).| = |.r.| * (sqrt ((((p . 1) ^2) + ((p . 2) ^2)) + ((p . 3) ^2)))
proof end;

theorem :: EUCLID_8:67
for r1, r2 being Real
for p being Element of REAL 3 holds (r1 * p) + (r2 * p) = (r1 + r2) * |[(p . 1),(p . 2),(p . 3)]|
proof end;

theorem :: EUCLID_8:68
for r being Real
for p1, p2 being Element of REAL 3 holds |((r * p1),p2)| = r * |(p1,p2)| by RVSUM_1:131;

theorem :: EUCLID_8:69
for r1, r2 being Real
for p being Element of REAL 3 holds (r1 * p) - (r2 * p) = (r1 - r2) * |[(p . 1),(p . 2),(p . 3)]|
proof end;

theorem :: EUCLID_8:70
for r being Real
for p, q being Element of REAL 3 holds |((r * p),q)| = r * ((((p . 1) * (q . 1)) + ((p . 2) * (q . 2))) + ((p . 3) * (q . 3)))
proof end;

theorem :: EUCLID_8:71
for p being Element of REAL 3 holds |(p,(0.REAL 3))| = 0
proof end;

theorem :: EUCLID_8:72
for p1, p2 being Element of REAL 3 holds |((- p1),p2)| = - |(p1,p2)| by RVSUM_1:132;

theorem :: EUCLID_8:73
for p1, p2 being Element of REAL 3 holds |((- p1),(- p2))| = |(p1,p2)| by RVSUM_1:133;

theorem :: EUCLID_8:74
for q, p1, p2 being Element of REAL 3 holds |((p1 - p2),q)| = |(p1,q)| - |(p2,q)| by RVSUM_1:134;

theorem :: EUCLID_8:75
for q, p1, p2 being Element of REAL 3 holds |((p1 + p2),q)| = |(p1,q)| + |(p2,q)| by RVSUM_1:130;

theorem :: EUCLID_8:76
for r1, r2 being Real
for q, p1, p2 being Element of REAL 3 holds |(((r1 * p1) + (r2 * p2)),q)| = (r1 * |(p1,q)|) + (r2 * |(p2,q)|) by RVSUM_1:135;

theorem :: EUCLID_8:77
for p1, p2, q1, q2 being Element of REAL 3 holds |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)| by RVSUM_1:136;

theorem :: EUCLID_8:78
for p1, p2, q1, q2 being Element of REAL 3 holds |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)| by RVSUM_1:137;

theorem Th70: :: EUCLID_8:79
for p being Element of REAL 3 holds
( |(p,p)| = 0 iff p = 0.REAL 3 )
proof end;

theorem :: EUCLID_8:80
for p being Element of REAL 3 holds
( |.p.| = 0 iff p = 0.REAL 3 )
proof end;

theorem :: EUCLID_8:81
for p, q being Element of REAL 3 holds |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| by RVSUM_1:139;

theorem :: EUCLID_8:82
for p, q being Element of REAL 3 holds |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)| by RVSUM_1:138;

theorem Th74: :: EUCLID_8:83
for p1, p2 being Element of REAL 3 holds p1 <X> p2 = - (p2 <X> p1)
proof end;

theorem Th75: :: EUCLID_8:84
for x1, x2, x3, y1, y2, y3 being Real holds |[x1,x2,x3]| <X> |[y1,y2,y3]| = |[((x2 * y3) - (x3 * y2)),((x3 * y1) - (x1 * y3)),((x1 * y2) - (x2 * y1))]|
proof end;

theorem :: EUCLID_8:85
for r being Real
for p1, p2 being Element of REAL 3 holds
( (r * p1) <X> p2 = r * (p1 <X> p2) & (r * p1) <X> p2 = p1 <X> (r * p2) )
proof end;

theorem Th77: :: EUCLID_8:86
for p1, p2, p3 being Element of REAL 3 holds p1 <X> (p2 + p3) = (p1 <X> p2) + (p1 <X> p3)
proof end;

theorem Th78: :: EUCLID_8:87
for p1, p2, p3 being Element of REAL 3 holds (p1 + p2) <X> p3 = (p1 <X> p3) + (p2 <X> p3)
proof end;

theorem :: EUCLID_8:88
for p1, p2, q1, q2 being Element of REAL 3 holds (p1 + p2) <X> (q1 + q2) = (((p1 <X> q1) + (p1 <X> q2)) + (p2 <X> q1)) + (p2 <X> q2)
proof end;

theorem :: EUCLID_8:89
for p1, p2, p3 being Element of REAL 3 holds p1 <X> (p2 <X> p3) = (|(p1,p3)| * p2) - (|(p1,p2)| * p3)
proof end;

definition
let p1, p2, p3 be Element of REAL 3;
func |{p1,p2,p3}| -> Real equals :: EUCLID_8:def 6
|(p1,(p2 <X> p3))|;
coherence
|(p1,(p2 <X> p3))| is Real ;
end;

:: deftheorem defines |{ EUCLID_8:def 6 :
for p1, p2, p3 being Element of REAL 3 holds |{p1,p2,p3}| = |(p1,(p2 <X> p3))|;

theorem :: EUCLID_8:90
for p1, p2 being Element of REAL 3 holds |{p1,p1,p2}| = 0
proof end;

theorem :: EUCLID_8:91
for p1, p2 being Element of REAL 3 holds |{p2,p1,p2}| = 0
proof end;

theorem :: EUCLID_8:92
for p1, p2 being Element of REAL 3 holds |{p1,p2,p2}| = 0
proof end;

theorem Th84: :: EUCLID_8:93
for p1, p2, p3 being Element of REAL 3 holds |{p1,p2,p3}| = |{p2,p3,p1}|
proof end;

theorem :: EUCLID_8:94
for p1, p2, p3 being Element of REAL 3 holds |{p1,p2,p3}| = |((p1 <X> p2),p3)|
proof end;

theorem :: EUCLID_8:95
for q, p1, p2 being Element of REAL 3 holds |{p1,p2,q}| = |((q <X> p1),p2)|
proof end;

definition
let f1, f2, f3 be PartFunc of REAL,REAL;
let t0 be Real;
func VFuncdiff (f1,f2,f3,t0) -> Element of REAL 3 equals :: EUCLID_8:def 7
|[(diff (f1,t0)),(diff (f2,t0)),(diff (f3,t0))]|;
coherence
|[(diff (f1,t0)),(diff (f2,t0)),(diff (f3,t0))]| is Element of REAL 3 ;
end;

:: deftheorem defines VFuncdiff EUCLID_8:def 7 :
for f1, f2, f3 being PartFunc of REAL,REAL
for t0 being Real holds VFuncdiff (f1,f2,f3,t0) = |[(diff (f1,t0)),(diff (f2,t0)),(diff (f3,t0))]|;

theorem :: EUCLID_8:96
for f1, f2, f3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 holds
VFuncdiff (f1,f2,f3,t0) = (((diff (f1,t0)) * <e1>) + ((diff (f2,t0)) * <e2>)) + ((diff (f3,t0)) * <e3>) by Th31;

theorem Th88: :: EUCLID_8:97
for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 holds
VFuncdiff ((f1 + g1),(f2 + g2),(f3 + g3),t0) = (VFuncdiff (f1,f2,f3,t0)) + (VFuncdiff (g1,g2,g3,t0))
proof end;

theorem Th89: :: EUCLID_8:98
for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 holds
VFuncdiff ((f1 - g1),(f2 - g2),(f3 - g3),t0) = (VFuncdiff (f1,f2,f3,t0)) - (VFuncdiff (g1,g2,g3,t0))
proof end;

theorem Th90: :: EUCLID_8:99
for r being Real
for f1, f2, f3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 holds
VFuncdiff ((r (#) f1),(r (#) f2),(r (#) f3),t0) = r * (VFuncdiff (f1,f2,f3,t0))
proof end;

theorem Th91: :: EUCLID_8:100
for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 holds
VFuncdiff ((f1 (#) g1),(f2 (#) g2),(f3 (#) g3),t0) = |[((g1 . t0) * (diff (f1,t0))),((g2 . t0) * (diff (f2,t0))),((g3 . t0) * (diff (f3,t0)))]| + |[((f1 . t0) * (diff (g1,t0))),((f2 . t0) * (diff (g2,t0))),((f3 . t0) * (diff (g3,t0)))]|
proof end;

theorem Th92: :: EUCLID_8:101
for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in f1 . t0 & g2 is_differentiable_in f2 . t0 & g3 is_differentiable_in f3 . t0 holds
VFuncdiff ((g1 * f1),(g2 * f2),(g3 * f3),t0) = |[((diff (g1,(f1 . t0))) * (diff (f1,t0))),((diff (g2,(f2 . t0))) * (diff (f2,t0))),((diff (g3,(f3 . t0))) * (diff (f3,t0)))]|
proof end;

theorem :: EUCLID_8:102
for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 & g1 . t0 <> 0 & g2 . t0 <> 0 & g3 . t0 <> 0 holds
VFuncdiff ((f1 / g1),(f2 / g2),(f3 / g3),t0) = |[((((diff (f1,t0)) * (g1 . t0)) - ((diff (g1,t0)) * (f1 . t0))) / ((g1 . t0) ^2)),((((diff (f2,t0)) * (g2 . t0)) - ((diff (g2,t0)) * (f2 . t0))) / ((g2 . t0) ^2)),((((diff (f3,t0)) * (g3 . t0)) - ((diff (g3,t0)) * (f3 . t0))) / ((g3 . t0) ^2))]|
proof end;

theorem Th94: :: EUCLID_8:103
for f1, f2, f3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & f1 . t0 <> 0 & f2 . t0 <> 0 & f3 . t0 <> 0 holds
VFuncdiff ((f1 ^),(f2 ^),(f3 ^),t0) = - |[((diff (f1,t0)) / ((f1 . t0) ^2)),((diff (f2,t0)) / ((f2 . t0) ^2)),((diff (f3,t0)) / ((f3 . t0) ^2))]|
proof end;

theorem :: EUCLID_8:104
for r being Real
for f1, f2, f3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 holds
VFuncdiff ((r (#) f1),(r (#) f2),(r (#) f3),t0) = (((r * (diff (f1,t0))) * <e1>) + ((r * (diff (f2,t0))) * <e2>)) + ((r * (diff (f3,t0))) * <e3>)
proof end;

theorem :: EUCLID_8:105
for r being Real
for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 holds
VFuncdiff ((r (#) (f1 + g1)),(r (#) (f2 + g2)),(r (#) (f3 + g3)),t0) = (r * (VFuncdiff (f1,f2,f3,t0))) + (r * (VFuncdiff (g1,g2,g3,t0)))
proof end;

theorem :: EUCLID_8:106
for r being Real
for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 holds
VFuncdiff ((r (#) (f1 - g1)),(r (#) (f2 - g2)),(r (#) (f3 - g3)),t0) = (r * (VFuncdiff (f1,f2,f3,t0))) - (r * (VFuncdiff (g1,g2,g3,t0)))
proof end;

theorem :: EUCLID_8:107
for r being Real
for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 holds
VFuncdiff (((r (#) f1) (#) g1),((r (#) f2) (#) g2),((r (#) f3) (#) g3),t0) = (r * |[((g1 . t0) * (diff (f1,t0))),((g2 . t0) * (diff (f2,t0))),((g3 . t0) * (diff (f3,t0)))]|) + (r * |[((f1 . t0) * (diff (g1,t0))),((f2 . t0) * (diff (g2,t0))),((f3 . t0) * (diff (g3,t0)))]|)
proof end;

theorem :: EUCLID_8:108
for r being Real
for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in f1 . t0 & g2 is_differentiable_in f2 . t0 & g3 is_differentiable_in f3 . t0 holds
VFuncdiff (((r (#) g1) * f1),((r (#) g2) * f2),((r (#) g3) * f3),t0) = r * |[((diff (g1,(f1 . t0))) * (diff (f1,t0))),((diff (g2,(f2 . t0))) * (diff (f2,t0))),((diff (g3,(f3 . t0))) * (diff (f3,t0)))]|
proof end;

theorem :: EUCLID_8:109
for r being Real
for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 & g1 . t0 <> 0 & g2 . t0 <> 0 & g3 . t0 <> 0 holds
VFuncdiff (((r (#) f1) / g1),((r (#) f2) / g2),((r (#) f3) / g3),t0) = r * |[((((diff (f1,t0)) * (g1 . t0)) - ((diff (g1,t0)) * (f1 . t0))) / ((g1 . t0) ^2)),((((diff (f2,t0)) * (g2 . t0)) - ((diff (g2,t0)) * (f2 . t0))) / ((g2 . t0) ^2)),((((diff (f3,t0)) * (g3 . t0)) - ((diff (g3,t0)) * (f3 . t0))) / ((g3 . t0) ^2))]|
proof end;

theorem :: EUCLID_8:110
for r being Real
for f1, f2, f3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & f1 . t0 <> 0 & f2 . t0 <> 0 & f3 . t0 <> 0 & r <> 0 holds
VFuncdiff (((r (#) f1) ^),((r (#) f2) ^),((r (#) f3) ^),t0) = - ((1 / r) * |[((diff (f1,t0)) / ((f1 . t0) ^2)),((diff (f2,t0)) / ((f2 . t0) ^2)),((diff (f3,t0)) / ((f3 . t0) ^2))]|)
proof end;

theorem :: EUCLID_8:111
for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 holds
VFuncdiff (((f2 (#) g3) - (f3 (#) g2)),((f3 (#) g1) - (f1 (#) g3)),((f1 (#) g2) - (f2 (#) g1)),t0) = |[(((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0)))),(((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0)))),(((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0))))]| + |[(((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0))),(((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0))),(((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0)))]|
proof end;

::p37-4(5.1) A*(BXC)
theorem :: EUCLID_8:112
for f1, f2, f3, g1, g2, g3, h1, h2, h3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 & h1 is_differentiable_in t0 & h2 is_differentiable_in t0 & h3 is_differentiable_in t0 holds
VFuncdiff ((h1 (#) ((f2 (#) g3) - (f3 (#) g2))),(h2 (#) ((f3 (#) g1) - (f1 (#) g3))),(h3 (#) ((f1 (#) g2) - (f2 (#) g1))),t0) = (|[((diff (h1,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))),((diff (h2,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0)))),((diff (h3,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))))]| + |[((h1 . t0) * (((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0)))),((h2 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0)))),((h3 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0))))]|) + |[((h1 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))),((h2 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0))))),((h3 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0)))))]|
proof end;

::p37-4(5.2) A*BXC
theorem :: EUCLID_8:113
for f1, f2, f3, g1, g2, g3, h1, h2, h3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 & h1 is_differentiable_in t0 & h2 is_differentiable_in t0 & h3 is_differentiable_in t0 holds
VFuncdiff ((((h2 (#) f2) (#) g3) - ((h3 (#) f3) (#) g2)),(((h3 (#) f3) (#) g1) - ((h1 (#) f1) (#) g3)),(((h1 (#) f1) (#) g2) - ((h2 (#) f2) (#) g1)),t0) = (|[((((h2 . t0) * (f2 . t0)) * (diff (g3,t0))) - (((h3 . t0) * (f3 . t0)) * (diff (g2,t0)))),((((h3 . t0) * (f3 . t0)) * (diff (g1,t0))) - (((h1 . t0) * (f1 . t0)) * (diff (g3,t0)))),((((h1 . t0) * (f1 . t0)) * (diff (g2,t0))) - (((h2 . t0) * (f2 . t0)) * (diff (g1,t0))))]| + |[((((h2 . t0) * (diff (f2,t0))) * (g3 . t0)) - (((h3 . t0) * (diff (f3,t0))) * (g2 . t0))),((((h3 . t0) * (diff (f3,t0))) * (g1 . t0)) - (((h1 . t0) * (diff (f1,t0))) * (g3 . t0))),((((h1 . t0) * (diff (f1,t0))) * (g2 . t0)) - (((h2 . t0) * (diff (f2,t0))) * (g1 . t0)))]|) + |[((((diff (h2,t0)) * (f2 . t0)) * (g3 . t0)) - (((diff (h3,t0)) * (f3 . t0)) * (g2 . t0))),((((diff (h3,t0)) * (f3 . t0)) * (g1 . t0)) - (((diff (h1,t0)) * (f1 . t0)) * (g3 . t0))),((((diff (h1,t0)) * (f1 . t0)) * (g2 . t0)) - (((diff (h2,t0)) * (f2 . t0)) * (g1 . t0)))]|
proof end;

::p37-4(6) AX(BXC)
theorem :: EUCLID_8:114
for f1, f2, f3, g1, g2, g3, h1, h2, h3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 & h1 is_differentiable_in t0 & h2 is_differentiable_in t0 & h3 is_differentiable_in t0 holds
VFuncdiff (((h2 (#) ((f1 (#) g2) - (f2 (#) g1))) - (h3 (#) ((f3 (#) g1) - (f1 (#) g3)))),((h3 (#) ((f2 (#) g3) - (f3 (#) g2))) - (h1 (#) ((f1 (#) g2) - (f2 (#) g1)))),((h1 (#) ((f3 (#) g1) - (f1 (#) g3))) - (h2 (#) ((f2 (#) g3) - (f3 (#) g2)))),t0) = (|[(((h2 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0))))) - ((h3 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0)))))),(((h3 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))) - ((h1 . t0) * (((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0)))))),(((h1 . t0) * (((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0))))) - ((h2 . t0) * (((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0))))))]| + |[(((h2 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0)))) - ((h3 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0))))),(((h3 . t0) * (((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0)))) - ((h1 . t0) * (((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0))))),(((h1 . t0) * (((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0)))) - ((h2 . t0) * (((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0)))))]|) + |[(((diff (h2,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0)))) - ((diff (h3,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))))),(((diff (h3,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))) - ((diff (h1,t0)) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))))),(((diff (h1,t0)) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0)))) - ((diff (h2,t0)) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))))]|
proof end;