:: Cross Products and Tripple Vector Products in 3-dimensional Euclidian Space
:: by Kanchun, Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received August 8, 2003
:: Copyright (c) 2003 Association of Mizar Users
theorem Th1: :: EUCLID_5:1
:: deftheorem defines `1 EUCLID_5:def 1 :
:: deftheorem defines `2 EUCLID_5:def 2 :
:: deftheorem defines `3 EUCLID_5:def 3 :
theorem :: EUCLID_5:2
theorem Th3: :: EUCLID_5:3
theorem Th4: :: EUCLID_5:4
theorem Th5: :: EUCLID_5:5
theorem Th6: :: EUCLID_5:6
for
x1,
y1,
z1,
x2,
y2,
z2 being
Real holds
|[x1,y1,z1]| + |[x2,y2,z2]| = |[(x1 + x2),(y1 + y2),(z1 + z2)]|
theorem Th7: :: EUCLID_5:7
theorem Th8: :: EUCLID_5:8
theorem :: EUCLID_5:9
theorem Th10: :: EUCLID_5:10
theorem :: EUCLID_5:11
theorem Th12: :: EUCLID_5:12
theorem Th13: :: EUCLID_5:13
for
x1,
y1,
z1,
x2,
y2,
z2 being
Real holds
|[x1,y1,z1]| - |[x2,y2,z2]| = |[(x1 - x2),(y1 - y2),(z1 - z2)]|
:: deftheorem EUCLID_5:def 4 :
canceled;
:: deftheorem defines <X> EUCLID_5:def 5 :
theorem :: EUCLID_5:14
theorem Th15: :: EUCLID_5:15
for
x1,
y1,
z1,
x2,
y2,
z2 being
Real holds
|[x1,y1,z1]| <X> |[x2,y2,z2]| = |[((y1 * z2) - (z1 * y2)),((z1 * x2) - (x1 * z2)),((x1 * y2) - (y1 * x2))]|
theorem :: EUCLID_5:16
theorem Th17: :: EUCLID_5:17
theorem :: EUCLID_5:18
theorem :: EUCLID_5:19
theorem :: EUCLID_5:20
theorem :: EUCLID_5:21
theorem :: EUCLID_5:22
theorem Th23: :: EUCLID_5:23
theorem Th24: :: EUCLID_5:24
theorem :: EUCLID_5:25
theorem :: EUCLID_5:26
theorem Th27: :: EUCLID_5:27
theorem Th28: :: EUCLID_5:28
theorem Th29: :: EUCLID_5:29
theorem Th30: :: EUCLID_5:30
:: deftheorem defines |{ EUCLID_5:def 6 :
theorem :: EUCLID_5:31
theorem :: EUCLID_5:32
theorem Th33: :: EUCLID_5:33
theorem :: EUCLID_5:34
theorem :: EUCLID_5:35