:: by Kanchun, Hiroshi Yamazaki and Yatsuka Nakamura

::

:: Received August 8, 2003

:: Copyright (c) 2003-2019 Association of Mizar Users

definition

let p be Point of (TOP-REAL 3);

coherence

p . 1 is Real ;

coherence

p . 2 is Real ;

coherence

p . 3 is Real ;

end;
coherence

p . 1 is Real ;

coherence

p . 2 is Real ;

coherence

p . 3 is Real ;

definition

let x, y, z be Real;

:: original: |[

redefine func |[x,y,z]| -> Point of (TOP-REAL 3);

coherence

|[x,y,z]| is Point of (TOP-REAL 3)

end;
:: original: |[

redefine func |[x,y,z]| -> Point of (TOP-REAL 3);

coherence

|[x,y,z]| is Point of (TOP-REAL 3)

proof end;

theorem Th5: :: EUCLID_5:5

for p1, p2 being Point of (TOP-REAL 3) holds p1 + p2 = |[((p1 `1) + (p2 `1)),((p1 `2) + (p2 `2)),((p1 `3) + (p2 `3))]|

proof end;

theorem Th6: :: EUCLID_5:6

for x1, x2, y1, y2, z1, z2 being Real holds |[x1,y1,z1]| + |[x2,y2,z2]| = |[(x1 + x2),(y1 + y2),(z1 + z2)]|

proof end;

theorem Th7: :: EUCLID_5:7

for x being Real

for p being Point of (TOP-REAL 3) holds x * p = |[(x * (p `1)),(x * (p `2)),(x * (p `3))]|

for p being Point of (TOP-REAL 3) holds x * p = |[(x * (p `1)),(x * (p `2)),(x * (p `3))]|

proof end;

theorem :: EUCLID_5:9

for x being Real

for p being Point of (TOP-REAL 3) holds

( (x * p) `1 = x * (p `1) & (x * p) `2 = x * (p `2) & (x * p) `3 = x * (p `3) )

for p being Point of (TOP-REAL 3) holds

( (x * p) `1 = x * (p `1) & (x * p) `2 = x * (p `2) & (x * p) `3 = x * (p `3) )

proof end;

theorem Th12: :: EUCLID_5:12

for p1, p2 being Point of (TOP-REAL 3) holds p1 - p2 = |[((p1 `1) - (p2 `1)),((p1 `2) - (p2 `2)),((p1 `3) - (p2 `3))]|

proof end;

theorem Th13: :: EUCLID_5:13

for x1, x2, y1, y2, z1, z2 being Real holds |[x1,y1,z1]| - |[x2,y2,z2]| = |[(x1 - x2),(y1 - y2),(z1 - z2)]|

proof end;

definition

let p1, p2 be Point of (TOP-REAL 3);

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 Point of (TOP-REAL 3);

;

end;
func p1 <X> p2 -> Point of (TOP-REAL 3) equals :: EUCLID_5: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 |[(((p1 `2) * (p2 `3)) - ((p1 `3) * (p2 `2))),(((p1 `3) * (p2 `1)) - ((p1 `1) * (p2 `3))),(((p1 `1) * (p2 `2)) - ((p1 `2) * (p2 `1)))]|;

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 Point of (TOP-REAL 3);

;

:: deftheorem defines <X> EUCLID_5:def 4 :

for p1, p2 being Point of (TOP-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)))]|;

for p1, p2 being Point of (TOP-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)))]|;

theorem :: EUCLID_5:14

theorem Th15: :: EUCLID_5:15

for x1, x2, y1, y2, z1, z2 being Real holds |[x1,y1,z1]| <X> |[x2,y2,z2]| = |[((y1 * z2) - (z1 * y2)),((z1 * x2) - (x1 * z2)),((x1 * y2) - (y1 * x2))]|

proof end;

theorem :: EUCLID_5:16

for x being Real

for p1, p2 being Point of (TOP-REAL 3) holds

( (x * p1) <X> p2 = x * (p1 <X> p2) & (x * p1) <X> p2 = p1 <X> (x * p2) )

for p1, p2 being Point of (TOP-REAL 3) holds

( (x * p1) <X> p2 = x * (p1 <X> p2) & (x * p1) <X> p2 = p1 <X> (x * p2) )

proof end;

theorem :: EUCLID_5:26

for p1, p2, p3, p4 being Point of (TOP-REAL 3) holds (p1 + p2) <X> (p3 + p4) = (((p1 <X> p3) + (p1 <X> p4)) + (p2 <X> p3)) + (p2 <X> p4)

proof end;

theorem Th28: :: EUCLID_5:28

for f1, f2 being FinSequence of REAL st len f1 = 3 & len f2 = 3 holds

mlt (f1,f2) = <*((f1 . 1) * (f2 . 1)),((f1 . 2) * (f2 . 2)),((f1 . 3) * (f2 . 3))*>

mlt (f1,f2) = <*((f1 . 1) * (f2 . 1)),((f1 . 2) * (f2 . 2)),((f1 . 3) * (f2 . 3))*>

proof end;

theorem Th29: :: EUCLID_5:29

for p1, p2 being Point of (TOP-REAL 3) holds |(p1,p2)| = (((p1 `1) * (p2 `1)) + ((p1 `2) * (p2 `2))) + ((p1 `3) * (p2 `3))

proof end;

theorem Th30: :: EUCLID_5:30

for x3, y3, x1, x2, y1, y2 being Real holds |(|[x1,x2,x3]|,|[y1,y2,y3]|)| = ((x1 * y1) + (x2 * y2)) + (x3 * y3)

proof end;

::

:: Scalar and Vector : Triple Products

::

:: Scalar and Vector : Triple Products

::

:: deftheorem defines |{ EUCLID_5:def 5 :

for p1, p2, p3 being Point of (TOP-REAL 3) holds |{p1,p2,p3}| = |(p1,(p2 <X> p3))|;

for p1, p2, p3 being Point of (TOP-REAL 3) holds |{p1,p2,p3}| = |(p1,(p2 <X> p3))|;

theorem :: EUCLID_5:32

for p1, p2, p3 being Point of (TOP-REAL 3) holds p1 <X> (p2 <X> p3) = (|(p1,p3)| * p2) - (|(p1,p2)| * p3)

proof end;

theorem :: EUCLID_5:34

registration
end;

:: Inner Product for Point of TOP-REAL 3

::