:: Some Operations on Quaternion Numbers
:: by Bo Li , Pan Wang , Xiquan Liang and Yanping Zhuang
::
:: Received October 14, 2008
:: Copyright (c) 2008 Association of Mizar Users
Lm2:
for x, y, z being quaternion number st z = x * y holds
( Rea z = ((((Rea x) * (Rea y)) - ((Im1 x) * (Im1 y))) - ((Im2 x) * (Im2 y))) - ((Im3 x) * (Im3 y)) & Im1 z = ((((Rea x) * (Im1 y)) + ((Im1 x) * (Rea y))) + ((Im2 x) * (Im3 y))) - ((Im3 x) * (Im2 y)) & Im2 z = ((((Rea x) * (Im2 y)) + ((Im2 x) * (Rea y))) + ((Im3 x) * (Im1 y))) - ((Im1 x) * (Im3 y)) & Im3 z = ((((Rea x) * (Im3 y)) + ((Im3 x) * (Rea y))) + ((Im1 x) * (Im2 y))) - ((Im2 x) * (Im1 y)) )
theorem a: :: QUATERN3:1
theorem :: QUATERN3:2
theorem :: QUATERN3:3
theorem :: QUATERN3:4
theorem :: QUATERN3:5
theorem :: QUATERN3:6
theorem :: QUATERN3:7
theorem :: QUATERN3:8
theorem :: QUATERN3:9
theorem :: QUATERN3:10
:: deftheorem defines ~ QUATERN3:def 1 :
:: deftheorem defines - QUATERN3:def 2 :
theorem Th4: :: QUATERN3:11
theorem :: QUATERN3:12
theorem :: QUATERN3:13
theorem :: QUATERN3:14
theorem :: QUATERN3:15
theorem :: QUATERN3:16
theorem :: QUATERN3:17
theorem :: QUATERN3:18
theorem h: :: QUATERN3:19
theorem :: QUATERN3:20
theorem :: QUATERN3:21
theorem :: QUATERN3:22
theorem :: QUATERN3:23
theorem :: QUATERN3:24
theorem :: QUATERN3:25
theorem Th5: :: QUATERN3:26
theorem Th6: :: QUATERN3:27
theorem Th7: :: QUATERN3:28
theorem Th8: :: QUATERN3:29
theorem :: QUATERN3:30
theorem :: QUATERN3:31
theorem th9: :: QUATERN3:32
theorem th10: :: QUATERN3:33
theorem th11: :: QUATERN3:34
theorem th12: :: QUATERN3:35
theorem :: QUATERN3:36
theorem :: QUATERN3:37
theorem thc: :: QUATERN3:38
theorem :: QUATERN3:39
theorem :: QUATERN3:40
theorem :: QUATERN3:41
theorem :: QUATERN3:42
theorem :: QUATERN3:43
theorem :: QUATERN3:44
theorem :: QUATERN3:45
theorem :: QUATERN3:46
theorem :: QUATERN3:47
theorem :: QUATERN3:48
theorem :: QUATERN3:49
theorem :: QUATERN3:50
theorem :: QUATERN3:51
theorem :: QUATERN3:52
theorem :: QUATERN3:53
theorem :: QUATERN3:54
:: deftheorem defines *' QUATERN3:def 3 :
:: deftheorem defines +* QUATERN3:def 4 :
theorem :: QUATERN3:55
theorem :: QUATERN3:56
theorem :: QUATERN3:57
theorem t1: :: QUATERN3:58
theorem t2: :: QUATERN3:59
theorem th13: :: QUATERN3:60
theorem th14: :: QUATERN3:61
theorem :: QUATERN3:62
theorem th15: :: QUATERN3:63
theorem :: QUATERN3:64
theorem :: QUATERN3:65
theorem :: QUATERN3:66
theorem :: QUATERN3:67
theorem :: QUATERN3:68
theorem :: QUATERN3:69
theorem :: QUATERN3:70
theorem :: QUATERN3:71
theorem :: QUATERN3:72
theorem :: QUATERN3:73
theorem :: QUATERN3:74
theorem :: QUATERN3:75
theorem th16: :: QUATERN3:76
theorem :: QUATERN3:77
theorem :: QUATERN3:78
theorem :: QUATERN3:79
theorem :: QUATERN3:80
Lmx:
<i> = [*0 ,1*]
by ARYTM_0:def 7;
theorem :: QUATERN3:81
theorem :: QUATERN3:82
theorem :: QUATERN3:83
:: deftheorem defines ^2 QUATERN3:def 5 :
theorem th: :: QUATERN3:84
theorem :: QUATERN3:85
theorem :: QUATERN3:86
theorem th1: :: QUATERN3:87
:: deftheorem defines ^3 QUATERN3:def 6 :
theorem :: QUATERN3:88
theorem :: QUATERN3:89
theorem :: QUATERN3:90
theorem :: QUATERN3:91
theorem :: QUATERN3:92
theorem :: QUATERN3:93
theorem :: QUATERN3:94
theorem :: QUATERN3:95