:: 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-2011 Association of Mizar Users

begin

definition

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

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 number 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 Element of 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 Element of REAL holds |[x1,x2,x3]| + |[y1,y2,y3]| = |[(x1 + y1),(x2 + y2),(x3 + y3)]|

proof end;

Lm9: 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;

Lm10: for r being Element of REAL
for p1, p2 being Element of REAL 3 holds |((r * p1),p2)| = r * |(p1,p2)|

proof end;

Lm11: for p1, p2, q1, q2 being Element of REAL 3 holds (p1 + p2) + (q1 + q2) = (p1 + q1) + (p2 + q2)

proof end;

Lm12: for p1, p2, q1, q2 being Element of REAL 3 holds (p1 + p2) - (q1 + q2) = (p1 - q1) + (p2 - q2)

proof end;

Lm13: for x1, x2, x3, y1, y2, y3 being Element of 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]|;

Lm14: for x, y, z being Element of REAL
for p being Element of REAL 3 st p = |[x,y,z]| holds
|(p,p)| = ((x ^2) + (y ^2)) + (z ^2)

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)))]|;

Lm15: for x1, x2, x3, y1, y2, y3 being Element of REAL holds |[x1,x2,x3]| <X> |[y1,y2,y3]| = |[((x2 * y3) - (x3 * y2)),((x3 * y1) - (x1 * y3)),((x1 * y2) - (x2 * y1))]|

proof end;

Lm16: for r being Element of 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;

begin

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 :: EUCLID_8:13

|(<e1>,|[0,0,0]|)| = 0

proof end;

theorem :: EUCLID_8:14

|(<e2>,|[0,0,0]|)| = 0

proof end;

theorem :: EUCLID_8:15

|(<e3>,|[0,0,0]|)| = 0

proof end;

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

<e1> <X> |[0,0,0]| = |[0,0,0]|

proof end;

theorem :: EUCLID_8:23

<e2> <X> |[0,0,0]| = |[0,0,0]|

proof end;

theorem :: EUCLID_8:24

<e3> <X> |[0,0,0]| = |[0,0,0]|

proof end;

theorem Th25: :: EUCLID_8:25

for r being Element of REAL holds r * <e1> = |[r,0,0]|

proof end;

theorem Th26: :: EUCLID_8:26

for r being Element of REAL holds r * <e2> = |[0,r,0]|

proof end;

theorem Th27: :: EUCLID_8:27

for r being Element of REAL holds r * <e3> = |[0,0,r]|

proof end;

theorem :: EUCLID_8:28

1 * <e1> = <e1>

proof end;

theorem :: EUCLID_8:29

1 * <e2> = <e2>

proof end;

theorem :: EUCLID_8:30

1 * <e3> = <e3>

proof end;

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

0 * <e1> = |[0,0,0]|

proof end;

theorem :: EUCLID_8:35

0 * <e2> = |[0,0,0]|

proof end;

theorem :: EUCLID_8:36

0 * <e3> = |[0,0,0]|

proof end;

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 Th38: :: EUCLID_8:38

for r being Element of 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 Th39: :: EUCLID_8:39

for x, y, z being Element of REAL holds |[x,y,z]| = ((x * <e1>) + (y * <e2>)) + (z * <e3>)

proof end;

theorem Th40: :: EUCLID_8:40

for r, x, y, z being Element of 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 Element of 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 Th44: :: 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 Element of 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 Element of 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 b₁ being Function of REAL,(REAL 3) st
for t being Real holds b₁ . t = |[(f1 . t),(f2 . t),(f3 . t)]|

proof end;

uniqueness
for b₁, b₂ being Function of REAL,(REAL 3) st ( for t being Real holds b₁ . t = |[(f1 . t),(f2 . t),(f3 . t)]| ) & ( for t being Real holds b₂ . t = |[(f1 . t),(f2 . t),(f3 . t)]| ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines VFunc EUCLID_8:def 5 :
for f1, f2, f3 being PartFunc of REAL,REAL
for b₄ being Function of REAL,(REAL 3) holds
( b₄ = VFunc (f1,f2,f3) iff for t being Real holds b₄ . 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 Th49: :: EUCLID_8:49

for p being Element of REAL 3
for f1, f2, f3 being PartFunc of REAL,REAL
for t being Real holds
( p = (VFunc (f1,f2,f3)) . t iff ( p . 1 = f1 . t & p . 2 = f2 . t & p . 3 = f3 . t ) )

proof end;

theorem Th50: :: EUCLID_8:50

for p being Element of REAL 3 holds
( len p = 3 & dom p = Seg 3 )

proof end;

theorem Th51: :: EUCLID_8:51

for p, q being Element of REAL 3 holds mlt (p,q) = <*((p . 1) * (q . 1)),((p . 2) * (q . 2)),((p . 3) * (q . 3))*>

proof end;

theorem :: EUCLID_8:52

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

theorem Th53: :: EUCLID_8:53

for p being Element of REAL 3 holds - p = |[(- (p . 1)),(- (p . 2)),(- (p . 3))]|

proof end;

theorem :: EUCLID_8:54

for p being Element of REAL 3 holds len (- p) = len p

proof end;

theorem Th55: :: 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, g1, f2, g2, f3, g3 being PartFunc of REAL,REAL
for t1, t2 being Real st f1 . t1 = g1 . t2 & f2 . t1 = g2 . t2 & f3 . t1 = g3 . t2 holds
(VFunc (f1,f2,f3)) . t1 = (VFunc (g1,g2,g3)) . t2

proof end;

theorem Th58: :: EUCLID_8:58

for p being Element of REAL 3
for r being real number holds r * p = |[(r * (p . 1)),(r * (p . 2)),(r * (p . 3))]|

proof end;

theorem Th59: :: EUCLID_8:59

for x, y, z being Element of REAL
for r being real number holds r * |[x,y,z]| = |[(r * x),(r * y),(r * z)]|

proof end;

theorem Th60: :: EUCLID_8:60

for p being Element of REAL 3 holds - p = |[(- (p . 1)),(- (p . 2)),(- (p . 3))]|

proof end;

theorem Th61: :: EUCLID_8:61

for p being Element of REAL 3 holds
( (- p) . 1 = - (p . 1) & (- p) . 2 = - (p . 2) & (- p) . 3 = - (p . 3) )

proof end;

theorem Th62: :: 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 Th64: :: 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 Th65: :: 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 Element of REAL
for p being Element of REAL 3 holds |.(r * p).| = (abs r) * (sqrt ((((p . 1) ^2) + ((p . 2) ^2)) + ((p . 3) ^2)))

proof end;

theorem :: EUCLID_8:67

for r1, r2 being Element of REAL
for p being Element of REAL 3 holds (r1 * p) + (r2 * p) = (r1 + r2) * |[(p . 1),(p . 2),(p . 3)]|

proof end;

theorem Th68: :: EUCLID_8:68

for r being Element of REAL
for p1, p2 being Element of REAL 3 holds |((r * p1),p2)| = r * |(p1,p2)|

proof end;

theorem :: EUCLID_8:69

for r1, r2 being Element of REAL
for p being Element of REAL 3 holds (r1 * p) - (r2 * p) = (r1 - r2) * |[(p . 1),(p . 2),(p . 3)]|

proof end;

theorem :: EUCLID_8:70

for r being Element of REAL
for p, q being Element of REAL 3 holds |((r * p),q)| = r * ((((p . 1) * (q . 1)) + ((p . 2) * (q . 2))) + ((p . 3) * (q . 3)))

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)|

proof end;

theorem :: EUCLID_8:73

for p1, p2 being Element of REAL 3 holds |((- p1),(- p2))| = |(p1,p2)|

proof end;

theorem Th74: :: EUCLID_8:74

for p1, p2, q being Element of REAL 3 holds |((p1 - p2),q)| = |(p1,q)| - |(p2,q)|

proof end;

theorem Th75: :: EUCLID_8:75

for p1, p2, q being Element of REAL 3 holds |((p1 + p2),q)| = |(p1,q)| + |(p2,q)|

proof end;

theorem :: EUCLID_8:76

for r1, r2 being Element of REAL
for p1, p2, q being Element of REAL 3 holds |(((r1 * p1) + (r2 * p2)),q)| = (r1 * |(p1,q)|) + (r2 * |(p2,q)|)

proof end;

theorem Th77: :: 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)|

proof end;

theorem Th78: :: 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)|

proof end;

theorem Th79: :: 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)|

proof end;

theorem :: EUCLID_8:82

for p, q being Element of REAL 3 holds |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)|

proof end;

theorem Th83: :: EUCLID_8:83

for p1, p2 being Element of REAL 3 holds p1 <X> p2 = - (p2 <X> p1)

proof end;

theorem Th84: :: EUCLID_8:84

for x1, x2, x3, y1, y2, y3 being Element of 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 Element of 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 Th86: :: 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 Th87: :: 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 number equals :: EUCLID_8:def 6
|(p1,(p2 <X> p3))|;
coherence
|(p1,(p2 <X> p3))| is real number ;

end;

:: deftheorem defines |{ EUCLID_8:def 6 :
for p1, p2, p3 being Element of REAL 3 holds |{p1,p2,p3}| = |(p1,(p2 <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 p2, p1 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 Th93: :: 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 p1, p2, q being Element of REAL 3 holds |{p1,p2,q}| = |((q <X> p1),p2)|

proof end;

begin

definition

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

end;

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

theorem :: EUCLID_8:96

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

theorem Th97: :: EUCLID_8:97

for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 holds
VFuncdiff ((f1 + g1),(f2 + g2),(f3 + g3),t0) = (VFuncdiff (f1,f2,f3,t0)) + (VFuncdiff (g1,g2,g3,t0))

proof end;

theorem Th98: :: EUCLID_8:98

for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 holds
VFuncdiff ((f1 - g1),(f2 - g2),(f3 - g3),t0) = (VFuncdiff (f1,f2,f3,t0)) - (VFuncdiff (g1,g2,g3,t0))

proof end;

theorem Th99: :: EUCLID_8:99

for r being Element of REAL
for f1, f2, f3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 holds
VFuncdiff ((r (#) f1),(r (#) f2),(r (#) f3),t0) = r * (VFuncdiff (f1,f2,f3,t0))

proof end;

theorem Th100: :: EUCLID_8:100

for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 holds
VFuncdiff ((f1 (#) g1),(f2 (#) g2),(f3 (#) g3),t0) = |[((g1 . t0) * (diff (f1,t0))),((g2 . t0) * (diff (f2,t0))),((g3 . t0) * (diff (f3,t0)))]| + |[((f1 . t0) * (diff (g1,t0))),((f2 . t0) * (diff (g2,t0))),((f3 . t0) * (diff (g3,t0)))]|

proof end;

theorem Th101: :: EUCLID_8:101

for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in f1 . t0 & g2 is_differentiable_in f2 . t0 & g3 is_differentiable_in f3 . t0 holds
VFuncdiff ((g1 * f1),(g2 * f2),(g3 * f3),t0) = |[((diff (g1,(f1 . t0))) * (diff (f1,t0))),((diff (g2,(f2 . t0))) * (diff (f2,t0))),((diff (g3,(f3 . t0))) * (diff (f3,t0)))]|

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 Th103: :: EUCLID_8:103

for f1, f2, f3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & f1 . t0 <> 0 & f2 . t0 <> 0 & f3 . t0 <> 0 holds
VFuncdiff ((f1 ^),(f2 ^),(f3 ^),t0) = - |[((diff (f1,t0)) / ((f1 . t0) ^2)),((diff (f2,t0)) / ((f2 . t0) ^2)),((diff (f3,t0)) / ((f3 . t0) ^2))]|

proof end;

theorem :: EUCLID_8:104

for r being Element of REAL
for f1, f2, f3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 holds
VFuncdiff ((r (#) f1),(r (#) f2),(r (#) f3),t0) = (((r * (diff (f1,t0))) * <e1>) + ((r * (diff (f2,t0))) * <e2>)) + ((r * (diff (f3,t0))) * <e3>)

proof end;

theorem :: EUCLID_8:105

for r being Element of REAL
for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 holds
VFuncdiff ((r (#) (f1 + g1)),(r (#) (f2 + g2)),(r (#) (f3 + g3)),t0) = (r * (VFuncdiff (f1,f2,f3,t0))) + (r * (VFuncdiff (g1,g2,g3,t0)))

proof end;

theorem :: EUCLID_8:106

for r being Element of REAL
for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 holds
VFuncdiff ((r (#) (f1 - g1)),(r (#) (f2 - g2)),(r (#) (f3 - g3)),t0) = (r * (VFuncdiff (f1,f2,f3,t0))) - (r * (VFuncdiff (g1,g2,g3,t0)))

proof end;

theorem :: EUCLID_8:107

for r being Element of REAL
for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 holds
VFuncdiff (((r (#) f1) (#) g1),((r (#) f2) (#) g2),((r (#) f3) (#) g3),t0) = (r * |[((g1 . t0) * (diff (f1,t0))),((g2 . t0) * (diff (f2,t0))),((g3 . t0) * (diff (f3,t0)))]|) + (r * |[((f1 . t0) * (diff (g1,t0))),((f2 . t0) * (diff (g2,t0))),((f3 . t0) * (diff (g3,t0)))]|)

proof end;

theorem :: EUCLID_8:108

for r being Element of REAL
for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in f1 . t0 & g2 is_differentiable_in f2 . t0 & g3 is_differentiable_in f3 . t0 holds
VFuncdiff (((r (#) g1) * f1),((r (#) g2) * f2),((r (#) g3) * f3),t0) = r * |[((diff (g1,(f1 . t0))) * (diff (f1,t0))),((diff (g2,(f2 . t0))) * (diff (f2,t0))),((diff (g3,(f3 . t0))) * (diff (f3,t0)))]|

proof end;

theorem :: EUCLID_8:109

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

proof end;

theorem :: EUCLID_8:110

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

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;

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;

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;

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;