:: Inner Products, Group, Ring of Quaternion Numbers
:: by Fuguo Ge
::
:: Received March 18, 2008
:: Copyright (c) 2008 Association of Mizar Users
Lm1:
for g being quaternion number ex r, s, t, u being Element of REAL st g = [*r,s,t,u*]
Lm2:
for a, b, c, d being real number holds (((a ^2 ) + (b ^2 )) + (c ^2 )) + (d ^2 ) >= 0
Lm3:
for a, b, c, d being real number st (((a ^2 ) + (b ^2 )) + (c ^2 )) + (d ^2 ) = 0 holds
( a = 0 & b = 0 & c = 0 & d = 0 )
Lm4:
for a, b, c, d being real number st (((a ^2 ) + (b ^2 )) + (c ^2 )) + (d ^2 ) = 0 holds
( a = 0 & b = 0 & c = 0 & d = 0 )
theorem Th1: :: QUATERN2:1
theorem Th2: :: QUATERN2:2
theorem Th3: :: QUATERN2:3
theorem Th4: :: QUATERN2:4
theorem :: QUATERN2:5
for
x1,
x2,
x3,
x4,
y1,
y2,
y3,
y4 being
Element of
REAL holds
[*x1,x2,x3,x4*] - [*y1,y2,y3,y4*] = [*(x1 - y1),(x2 - y2),(x3 - y3),(x4 - y4)*]
theorem :: QUATERN2:6
theorem Th7: :: QUATERN2:7
theorem :: QUATERN2:8
theorem Th9: :: QUATERN2:9
Lm5:
for r being quaternion number st r <> 0 holds
|.r.| <> 0
theorem Th10: :: QUATERN2:10
theorem Th11: :: QUATERN2:11
theorem :: QUATERN2:12
theorem :: QUATERN2:13
theorem Th14: :: QUATERN2:14
theorem Th15: :: QUATERN2:15
theorem Th16: :: QUATERN2:16
theorem Th17: :: QUATERN2:17
theorem Th18: :: QUATERN2:18
theorem Th19: :: QUATERN2:19
theorem Th20: :: QUATERN2:20
theorem Th21: :: QUATERN2:21
theorem Th22: :: QUATERN2:22
theorem Th23: :: QUATERN2:23
theorem Th24: :: QUATERN2:24
theorem Th25: :: QUATERN2:25
theorem :: QUATERN2:26
definition
let q,
r be
quaternion number ;
consider q0,
q1,
q2,
q3 being
Element of
REAL such that A1:
q = [*q0,q1,q2,q3*]
by Lm1;
consider r0,
r1,
r2,
r3 being
Element of
REAL such that A2:
r = [*r0,r1,r2,r3*]
by Lm1;
func q / r -> set means :
Def1:
:: QUATERN2:def 1
ex
q0,
q1,
q2,
q3,
r0,
r1,
r2,
r3 being
Element of
REAL st
(
q = [*q0,q1,q2,q3*] &
r = [*r0,r1,r2,r3*] &
it = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2 )),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2 )),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2 )),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2 ))*] );
existence
ex b1 being set ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st
( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & b1 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2 )),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2 )),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2 )),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2 ))*] )
uniqueness
for b1, b2 being set st ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st
( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & b1 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2 )),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2 )),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2 )),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2 ))*] ) & ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st
( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & b2 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2 )),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2 )),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2 )),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2 ))*] ) holds
b1 = b2
end;
:: deftheorem Def1 defines / QUATERN2:def 1 :
for
q,
r being
quaternion number for
b3 being
set holds
(
b3 = q / r iff ex
q0,
q1,
q2,
q3,
r0,
r1,
r2,
r3 being
Element of
REAL st
(
q = [*q0,q1,q2,q3*] &
r = [*r0,r1,r2,r3*] &
b3 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2 )),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2 )),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2 )),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2 ))*] ) );
theorem :: QUATERN2:27
:: deftheorem defines " QUATERN2:def 2 :
theorem :: QUATERN2:28
theorem :: QUATERN2:29
theorem :: QUATERN2:30
theorem Th31: :: QUATERN2:31
theorem :: QUATERN2:32
theorem Th33: :: QUATERN2:33
theorem :: QUATERN2:34
definition
func compquaternion -> UnOp of
QUATERNION means :: QUATERN2:def 3
for
c being
Element of
QUATERNION holds
it . c = - c;
existence
ex b1 being UnOp of QUATERNION st
for c being Element of QUATERNION holds b1 . c = - c
from FUNCT_2:sch 4();
uniqueness
for b1, b2 being UnOp of QUATERNION st ( for c being Element of QUATERNION holds b1 . c = - c ) & ( for c being Element of QUATERNION holds b2 . c = - c ) holds
b1 = b2
from BINOP_2:sch 1();
func addquaternion -> BinOp of
QUATERNION means :
Def4:
:: QUATERN2:def 4
for
c1,
c2 being
Element of
QUATERNION holds
it . c1,
c2 = c1 + c2;
existence
ex b1 being BinOp of QUATERNION st
for c1, c2 being Element of QUATERNION holds b1 . c1,c2 = c1 + c2
from BINOP_1:sch 4();
uniqueness
for b1, b2 being BinOp of QUATERNION st ( for c1, c2 being Element of QUATERNION holds b1 . c1,c2 = c1 + c2 ) & ( for c1, c2 being Element of QUATERNION holds b2 . c1,c2 = c1 + c2 ) holds
b1 = b2
from BINOP_2:sch 2();
func diffquaternion -> BinOp of
QUATERNION means :: QUATERN2:def 5
for
c1,
c2 being
Element of
QUATERNION holds
it . c1,
c2 = c1 - c2;
existence
ex b1 being BinOp of QUATERNION st
for c1, c2 being Element of QUATERNION holds b1 . c1,c2 = c1 - c2
from BINOP_1:sch 4();
uniqueness
for b1, b2 being BinOp of QUATERNION st ( for c1, c2 being Element of QUATERNION holds b1 . c1,c2 = c1 - c2 ) & ( for c1, c2 being Element of QUATERNION holds b2 . c1,c2 = c1 - c2 ) holds
b1 = b2
from BINOP_2:sch 2();
func multquaternion -> BinOp of
QUATERNION means :
Def6:
:: QUATERN2:def 6
for
c1,
c2 being
Element of
QUATERNION holds
it . c1,
c2 = c1 * c2;
existence
ex b1 being BinOp of QUATERNION st
for c1, c2 being Element of QUATERNION holds b1 . c1,c2 = c1 * c2
from BINOP_1:sch 4();
uniqueness
for b1, b2 being BinOp of QUATERNION st ( for c1, c2 being Element of QUATERNION holds b1 . c1,c2 = c1 * c2 ) & ( for c1, c2 being Element of QUATERNION holds b2 . c1,c2 = c1 * c2 ) holds
b1 = b2
from BINOP_2:sch 2();
func divquaternion -> BinOp of
QUATERNION means :: QUATERN2:def 7
for
c1,
c2 being
Element of
QUATERNION holds
it . c1,
c2 = c1 / c2;
existence
ex b1 being BinOp of QUATERNION st
for c1, c2 being Element of QUATERNION holds b1 . c1,c2 = c1 / c2
from BINOP_1:sch 4();
uniqueness
for b1, b2 being BinOp of QUATERNION st ( for c1, c2 being Element of QUATERNION holds b1 . c1,c2 = c1 / c2 ) & ( for c1, c2 being Element of QUATERNION holds b2 . c1,c2 = c1 / c2 ) holds
b1 = b2
from BINOP_2:sch 2();
func invquaternion -> UnOp of
QUATERNION means :: QUATERN2:def 8
for
c being
Element of
QUATERNION holds
it . c = c " ;
existence
ex b1 being UnOp of QUATERNION st
for c being Element of QUATERNION holds b1 . c = c "
from FUNCT_2:sch 4();
uniqueness
for b1, b2 being UnOp of QUATERNION st ( for c being Element of QUATERNION holds b1 . c = c " ) & ( for c being Element of QUATERNION holds b2 . c = c " ) holds
b1 = b2
from BINOP_2:sch 1();
end;
:: deftheorem defines compquaternion QUATERN2:def 3 :
:: deftheorem Def4 defines addquaternion QUATERN2:def 4 :
:: deftheorem defines diffquaternion QUATERN2:def 5 :
:: deftheorem Def6 defines multquaternion QUATERN2:def 6 :
:: deftheorem defines divquaternion QUATERN2:def 7 :
:: deftheorem defines invquaternion QUATERN2:def 8 :
:: deftheorem Def9 defines G_Quaternion QUATERN2:def 9 :
theorem Th35: :: QUATERN2:35
theorem :: QUATERN2:36
:: deftheorem Def10 defines R_Quaternion QUATERN2:def 10 :
theorem :: QUATERN2:37
theorem :: QUATERN2:38
theorem Th39: :: QUATERN2:39
theorem :: QUATERN2:40
theorem :: QUATERN2:41
theorem :: QUATERN2:42
theorem :: QUATERN2:43
theorem :: QUATERN2:44
theorem :: QUATERN2:45
theorem :: QUATERN2:46
theorem :: QUATERN2:47
:: deftheorem defines .|. QUATERN2:def 11 :
theorem Th48: :: QUATERN2:48
theorem Th49: :: QUATERN2:49
theorem :: QUATERN2:50
theorem :: QUATERN2:51
theorem :: QUATERN2:52
theorem :: QUATERN2:53
theorem :: QUATERN2:54
theorem :: QUATERN2:55
theorem :: QUATERN2:56
theorem :: QUATERN2:57
theorem :: QUATERN2:58
theorem :: QUATERN2:59
theorem :: QUATERN2:60
theorem :: QUATERN2:61