Substantiation and Operations of Quaternion Numbers in Computer by Software Mizar

In this paper, we define the set H of quaternion numbers as the set of all ordered sequences q =< x,y,w,z >, which is based on the mapping (x,y,w,z)vertical bar ->(a,b,c,d) by software Mizar, where x,y,w and z are real numbers, with the addition, substraction, mul-tiplication and division of the quaternion numbers provided. We also define the real and three imaginary parts of q and denote this by x=Re q, y=Im1 q, w=Im2 q, z=Inz3 q, by which the former operations are redefined and substantiated. Thus the higher operations of quaternion are defined and proved such as inner product, conjugate, etc. Finally, the group and ring of quaternion numbers is given. However, all above-mentioned conclusions are achieved in Mizar, which builds the vital substructure to support a further study on quaternion numbers in mechanical theorem proving.