quatern2.miz

begin



 Lm1: for g be Quaternion holds ex r,s,t,u be Element of REAL st g = [*r, s, t, u*]

 proof

 let g be Quaternion;

 consider r,s,t,u be Real such that

 A1: g = [*r, s, t, u*] by QUATERNI: 7;

 reconsider r, s, t, u as Element of REAL by XREAL_0:def 1;

 g = [*r, s, t, u*] by A1;

 hence thesis;

 end;



 Lm2: for a,b,c,d be Real holds ((((a ^2 ) + (b ^2 )) + (c ^2 )) + (d ^2 )) >= 0 by QUATERNI: 74;



 Lm3: for a,b,c,d be Real st ((((a ^2 ) + (b ^2 )) + (c ^2 )) + (d ^2 )) = 0 holds a = 0 & b = 0 & c = 0 & d = 0 by QUATERNI: 96;

 reserve q,r,c,c1,c2,c3 for Quaternion;

 reserve x1,x2,x3,x4,y1,y2,y3,y4 for Real;

 definition

 :: original: 0q

 redefine

 func 0q -> Element of QUATERNION ;

 coherence by QUATERNI:def 2;

 end

 definition

 :: original: 1q

 redefine

 func 1q -> Element of QUATERNION ;

 coherence by QUATERNI:def 2;

 end

 reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

 theorem :: QUATERN2:1



 Th1: for x,y,z,w be Real holds [*x, y, z, w*] = (((x + (y * )) + (z * <j> )) + (w * <k> ))

 proof

 let x,y,z,w be Real;

 reconsider x0 = (x + 0 ), y0 = (y + 0 ) as Element of REAL by XREAL_0:def 1;

 = [*( In ( 0 , REAL )), jj*] by ARYTM_0:def 5;

 then = [* 0 , jj, 0 , 0 *] by QUATERNI: 91;



 then

 A1: (y * ) = [*(y * 0 ), (y * jj), (y * 0 ), (y * 0 )*] by QUATERNI:def 21

 .= [* 0 , y, 0 , 0 *];



 A2: (z * <j> ) = [*(z * 0 ), (z * 0 ), (z * jj), (y * 0 )*] by QUATERNI:def 21

 .= [* 0 , 0 , z, 0 *];



 A3: (w * <k> ) = [*(w * 0 ), (w * 0 ), (w * 0 ), (w * jj)*] by QUATERNI:def 21

 .= [* 0 , 0 , 0 , w*];

 (x + (y * )) = [*x0, y0, 0 , 0 *] by A1, QUATERNI:def 19

 .= [*x, y, 0 , 0 *];



 then ((x + (y * )) + (z * <j> )) = [*x0, y0, ( 0 + z), ( 0 + 0 )*] by A2, QUATERNI:def 7

 .= [*x, y, z, 0 *];

 then (((x + (y * )) + (z * <j> )) + (w * <k> )) = [*x0, y0, ( 0 + z), ( 0 + w)*] by A3, QUATERNI:def 7;

 hence thesis;

 end;

 theorem :: QUATERN2:2



 Th2: ((c1 + c2) + c3) = (c1 + (c2 + c3))

 proof

 consider x1,y1,w1,z1 be Element of REAL such that

 A1: c1 = [*x1, y1, w1, z1*] by Lm1;

 consider x2,y2,w2,z2 be Element of REAL such that

 A2: c2 = [*x2, y2, w2, z2*] by Lm1;

 consider x3,y3,w3,z3 be Element of REAL such that

 A3: c3 = [*x3, y3, w3, z3*] by Lm1;



 A4: (c2 + c3) = [*(x2 + x3), (y2 + y3), (w2 + w3), (z2 + z3)*] by A2, A3, QUATERNI:def 7;

 ((c1 + c2) + c3) = ( [*(x1 + x2), (y1 + y2), (w1 + w2), (z1 + z2)*] + [*x3, y3, w3, z3*]) by A1, A2, A3, QUATERNI:def 7

 .= [*((x1 + x2) + x3), ((y1 + y2) + y3), ((w1 + w2) + w3), ((z1 + z2) + z3)*] by QUATERNI:def 7

 .= [*(x1 + (x2 + x3)), (y1 + (y2 + y3)), (w1 + (w2 + w3)), (z1 + (z2 + z3))*]

 .= (c1 + (c2 + c3)) by A1, A4, QUATERNI:def 7;

 hence thesis;

 end;

 theorem :: QUATERN2:3



 Th3: (c + 0q ) = c

 proof



 A1: 0q = [*( In ( 0 , REAL )), ( In ( 0 , REAL ))*] by ARYTM_0:def 5

 .= [* 0 , 0 , 0 , 0 *] by QUATERNI: 91;

 consider x,y,w,z be Element of REAL such that

 A2: c = [*x, y, w, z*] by Lm1;

 (c + 0q ) = [*(x + 0 ), (y + 0 ), (w + 0 ), (z + 0 )*] by A1, A2, QUATERNI:def 7

 .= [*x, y, w, z*];

 hence thesis by A2;

 end;

 theorem :: QUATERN2:4



 Th4: ( - [*x1, x2, x3, x4*]) = [*( - x1), ( - x2), ( - x3), ( - x4)*]

 proof

 ( [*x1, x2, x3, x4*] + [*( - x1), ( - x2), ( - x3), ( - x4)*]) = [*(x1 - x1), (x2 - x2), (x3 - x3), (x4 - x4)*] by QUATERNI:def 7

 .= [*( In ( 0 , REAL )), ( In ( 0 , REAL ))*] by QUATERNI: 91

 .= 0 by ARYTM_0:def 5;

 hence thesis by QUATERNI:def 8;

 end;

 theorem :: QUATERN2:5

 ( [*x1, x2, x3, x4*] - [*y1, y2, y3, y4*]) = [*(x1 - y1), (x2 - y2), (x3 - y3), (x4 - y4)*]

 proof

 ( [*x1, x2, x3, x4*] - [*y1, y2, y3, y4*]) = ( [*x1, x2, x3, x4*] + [*( - y1), ( - y2), ( - y3), ( - y4)*]) by Th4

 .= [*(x1 - y1), (x2 - y2), (x3 - y3), (x4 - y4)*] by QUATERNI:def 7;

 hence thesis;

 end;

 theorem :: QUATERN2:6

 ((c1 - c2) + c3) = ((c1 + c3) - c2) by Th2;

 theorem :: QUATERN2:7



 Th7: c1 = ((c1 + c2) - c2)

 proof



 thus ((c1 + c2) - c2) = (c1 + (c2 - c2)) by Th2

 .= (c1 + 0q ) by QUATERNI:def 8

 .= c1 by Th3;

 end;

 theorem :: QUATERN2:8

 c1 = ((c1 - c2) + c2)

 proof



 thus ((c1 - c2) + c2) = ((c1 + c2) - c2) by Th2

 .= c1 by Th7;

 end;

 theorem :: QUATERN2:9



 Th9: (( - x1) * c) = ( - (x1 * c))

 proof

 consider x,y,w,z be Element of REAL such that

 A1: c = [*x, y, w, z*] by Lm1;



 A2: (( - x1) * c) = [*(( - x1) * x), (( - x1) * y), (( - x1) * w), (( - x1) * z)*] by A1, QUATERNI:def 21

 .= [*( - (x1 * x)), ( - (x1 * y)), ( - (x1 * w)), ( - (x1 * z))*];



 A3: ( - (x1 * c)) = ( - [*(x1 * x), (x1 * y), (x1 * w), (x1 * z)*]) by A1, QUATERNI:def 21;

 ( [*(x1 * x), (x1 * y), (x1 * w), (x1 * z)*] + [*( - (x1 * x)), ( - (x1 * y)), ( - (x1 * w)), ( - (x1 * z))*]) = [*((x1 * x) + ( - (x1 * x))), ((x1 * y) + ( - (x1 * y))), ((x1 * w) + ( - (x1 * w))), ((x1 * z) + ( - (x1 * z)))*] by QUATERNI:def 7

 .= [*( In ( 0 , REAL )), ( In ( 0 , REAL ))*] by QUATERNI: 91

 .= 0 by ARYTM_0:def 5;

 hence thesis by A2, A3, QUATERNI:def 8;

 end;

 definition

 :: original: 

 redefine

 func -> Element of QUATERNION ;

 coherence by QUATERNI:def 2;

 end



 Lm4: |.r.| = 0 implies r = 0 by QUATERNI: 66;

 theorem :: QUATERN2:10



 Th10: r <> 0 implies |.r.| > 0

 proof

 assume r <> 0 ;

 then |.r.| <> 0 by Lm4;

 hence thesis by QUATERNI: 67;

 end;

 theorem :: QUATERN2:11



 Th11: 0q = [* 0 , 0 , 0 , 0 *]

 proof



 thus 0q = [*( In ( 0 , REAL )), ( In ( 0 , REAL ))*] by ARYTM_0:def 5

 .= [* 0 , 0 , 0 , 0 *] by QUATERNI: 91;

 end;

 theorem :: QUATERN2:12

 for r be Quaternion holds ( 0q * r) = 0

 proof

 let r be Quaternion;

 consider x1,x2,x3,x4,y1,y2,y3,y4 be Real such that

 A1: 0 = [*x1, x2, x3, x4*] and r = [*y1, y2, y3, y4*] and

 A2: ( 0q * r) = [*((((x1 * y1) - (x2 * y2)) - (x3 * y3)) - (x4 * y4)), ((((x1 * y2) + (x2 * y1)) + (x3 * y4)) - (x4 * y3)), ((((x1 * y3) + (y1 * x3)) + (y2 * x4)) - (y4 * x2)), ((((x1 * y4) + (x4 * y1)) + (x2 * y3)) - (x3 * y2))*] by QUATERNI:def 10;



 A3: x1 = 0 by A1, Th11, QUATERNI: 12;



 A4: x2 = 0 by A1, Th11, QUATERNI: 12;



 A5: x3 = 0 by A1, Th11, QUATERNI: 12;

 x4 = 0 by A1, Th11, QUATERNI: 12;

 hence thesis by A2, A3, A4, A5, Th11;

 end;

 theorem :: QUATERN2:13

 for r be Quaternion holds (r * 0q ) = 0

 proof

 let r be Quaternion;

 consider x1,x2,x3,x4,y1,y2,y3,y4 be Real such that r = [*x1, x2, x3, x4*] and

 A1: 0 = [*y1, y2, y3, y4*] and

 A2: (r * 0q ) = [*((((x1 * y1) - (x2 * y2)) - (x3 * y3)) - (x4 * y4)), ((((x1 * y2) + (x2 * y1)) + (x3 * y4)) - (x4 * y3)), ((((x1 * y3) + (y1 * x3)) + (y2 * x4)) - (y4 * x2)), ((((x1 * y4) + (x4 * y1)) + (x2 * y3)) - (x3 * y2))*] by QUATERNI:def 10;



 A3: y1 = 0 by A1, Th11, QUATERNI: 12;



 A4: y2 = 0 by A1, Th11, QUATERNI: 12;



 A5: y3 = 0 by A1, Th11, QUATERNI: 12;

 y4 = 0 by A1, Th11, QUATERNI: 12;

 hence thesis by A2, A3, A4, A5, Th11;

 end;

 theorem :: QUATERN2:14



 Th14: (c * 1q ) = c

 proof



 A1: 1q = [*jj, ( In ( 0 , REAL ))*] by ARYTM_0:def 5

 .= [*1, 0 , 0 , 0 *] by QUATERNI: 91;

 consider x,y,w,z be Element of REAL such that

 A2: c = [*x, y, w, z*] by Lm1;

 (c * 1q ) = [*((((x * 1) - (y * 0 )) - (w * 0 )) - (z * 0 )), ((((x * 0 ) + (y * 1)) + (w * 0 )) - (z * 0 )), ((((x * 0 ) + (1 * w)) + ( 0 * z)) - ( 0 * y)), ((((x * 0 ) + (z * jj)) + (y * 0 )) - (w * 0 ))*] by A1, A2, QUATERNI:def 10

 .= [*x, y, w, z*];

 hence thesis by A2;

 end;

 theorem :: QUATERN2:15



 Th15: ( 1q * c) = c

 proof



 A1: 1q = [*jj, ( In ( 0 , REAL ))*] by ARYTM_0:def 5

 .= [*1, 0 , 0 , 0 *] by QUATERNI: 91;

 consider x,y,w,z be Element of REAL such that

 A2: c = [*x, y, w, z*] by Lm1;

 ( 1q * c) = [*((((x * 1) - (y * 0 )) - (w * 0 )) - (z * 0 )), ((((x * 0 ) + (y * 1)) + (w * 0 )) - (z * 0 )), ((((x * 0 ) + (1 * w)) + ( 0 * z)) - ( 0 * y)), ((((x * 0 ) + (z * jj)) + (y * 0 )) - (w * 0 ))*] by A1, A2, QUATERNI:def 10

 .= [*x, y, w, z*];

 hence thesis by A2;

 end;

 theorem :: QUATERN2:16



 Th16: ((c1 * c2) * c3) = (c1 * (c2 * c3))

 proof

 consider x1,y1,w1,z1 be Element of REAL such that

 A1: c1 = [*x1, y1, w1, z1*] by Lm1;

 consider x2,y2,w2,z2 be Element of REAL such that

 A2: c2 = [*x2, y2, w2, z2*] by Lm1;

 consider x3,y3,w3,z3 be Element of REAL such that

 A3: c3 = [*x3, y3, w3, z3*] by Lm1;



 A4: ((c1 * c2) * c3) = ( [*((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2)), ((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2)), ((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1)), ((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2))*] * c3) by A1, A2, QUATERNI:def 10

 .= [*((((((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2)) * x3) - (((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2)) * y3)) - (((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1)) * w3)) - (((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2)) * z3)), ((((((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2)) * y3) + (((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2)) * x3)) + (((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1)) * z3)) - (((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2)) * w3)), ((((((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2)) * w3) + (x3 * ((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1)))) + (y3 * ((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2)))) - (z3 * ((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2)))), ((((((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2)) * z3) + (((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2)) * x3)) + (((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2)) * w3)) - (((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1)) * y3))*] by A3, QUATERNI:def 10

 .= [*((((((((x1 * x2) * x3) - ((y1 * y2) * x3)) - ((w1 * w2) * x3)) - ((z1 * z2) * x3)) - (((((x1 * y2) * y3) + ((y1 * x2) * y3)) + ((w1 * z2) * y3)) - ((z1 * w2) * y3))) - (((((x1 * w2) * w3) + ((x2 * w1) * w3)) + ((y2 * z1) * w3)) - ((z2 * y1) * w3))) - (((((x1 * z2) * z3) + ((z1 * x2) * z3)) + ((y1 * w2) * z3)) - ((w1 * y2) * z3))), ((((((((x1 * x2) * y3) - ((y1 * y2) * y3)) - ((w1 * w2) * y3)) - ((z1 * z2) * y3)) + (((((x1 * y2) * x3) + ((y1 * x2) * x3)) + ((w1 * z2) * x3)) - ((z1 * w2) * x3))) + (((((x1 * w2) * z3) + ((x2 * w1) * z3)) + ((y2 * z1) * z3)) - ((z2 * y1) * z3))) - (((((x1 * z2) * w3) + ((z1 * x2) * w3)) + ((y1 * w2) * w3)) - ((w1 * y2) * w3))), ((((((((x1 * x2) * w3) - ((y1 * y2) * w3)) - ((w1 * w2) * w3)) - ((z1 * z2) * w3)) + (((((x3 * x1) * w2) + ((x3 * x2) * w1)) + ((x3 * y2) * z1)) - ((x3 * z2) * y1))) + (((((y3 * x1) * z2) + ((y3 * z1) * x2)) + ((y3 * y1) * w2)) - ((y3 * w1) * y2))) - (((((z3 * x1) * y2) + ((z3 * y1) * x2)) + ((z3 * w1) * z2)) - ((z3 * z1) * w2))), ((((((((x1 * x2) * z3) - ((y1 * y2) * z3)) - ((w1 * w2) * z3)) - ((z1 * z2) * z3)) + (((((x1 * z2) * x3) + ((z1 * x2) * x3)) + ((y1 * w2) * x3)) - ((w1 * y2) * x3))) + (((((x1 * y2) * w3) + ((y1 * x2) * w3)) + ((w1 * z2) * w3)) - ((z1 * w2) * w3))) - (((((x1 * w2) * y3) + ((x2 * w1) * y3)) + ((y2 * z1) * y3)) - ((z2 * y1) * y3)))*];

 (c1 * (c2 * c3)) = (c1 * [*((((x2 * x3) - (y2 * y3)) - (w2 * w3)) - (z2 * z3)), ((((x2 * y3) + (y2 * x3)) + (w2 * z3)) - (z2 * w3)), ((((x2 * w3) + (x3 * w2)) + (y3 * z2)) - (z3 * y2)), ((((x2 * z3) + (z2 * x3)) + (y2 * w3)) - (w2 * y3))*]) by A2, A3, QUATERNI:def 10

 .= [*((((x1 * ((((x2 * x3) - (y2 * y3)) - (w2 * w3)) - (z2 * z3))) - (y1 * ((((x2 * y3) + (y2 * x3)) + (w2 * z3)) - (z2 * w3)))) - (w1 * ((((x2 * w3) + (x3 * w2)) + (y3 * z2)) - (z3 * y2)))) - (z1 * ((((x2 * z3) + (z2 * x3)) + (y2 * w3)) - (w2 * y3)))), ((((x1 * ((((x2 * y3) + (y2 * x3)) + (w2 * z3)) - (z2 * w3))) + (y1 * ((((x2 * x3) - (y2 * y3)) - (w2 * w3)) - (z2 * z3)))) + (w1 * ((((x2 * z3) + (z2 * x3)) + (y2 * w3)) - (w2 * y3)))) - (z1 * ((((x2 * w3) + (x3 * w2)) + (y3 * z2)) - (z3 * y2)))), ((((x1 * ((((x2 * w3) + (x3 * w2)) + (y3 * z2)) - (z3 * y2))) + (((((x2 * x3) - (y2 * y3)) - (w2 * w3)) - (z2 * z3)) * w1)) + (((((x2 * y3) + (y2 * x3)) + (w2 * z3)) - (z2 * w3)) * z1)) - (((((x2 * z3) + (z2 * x3)) + (y2 * w3)) - (w2 * y3)) * y1)), ((((x1 * ((((x2 * z3) + (z2 * x3)) + (y2 * w3)) - (w2 * y3))) + (z1 * ((((x2 * x3) - (y2 * y3)) - (w2 * w3)) - (z2 * z3)))) + (y1 * ((((x2 * w3) + (x3 * w2)) + (y3 * z2)) - (z3 * y2)))) - (w1 * ((((x2 * y3) + (y2 * x3)) + (w2 * z3)) - (z2 * w3))))*] by A1, QUATERNI:def 10

 .= ((c1 * c2) * c3) by A4;

 hence thesis;

 end;

 theorem :: QUATERN2:17



 Th17: (c1 * (c2 + c3)) = ((c1 * c2) + (c1 * c3))

 proof

 consider x1,y1,w1,z1 be Element of REAL such that

 A1: c1 = [*x1, y1, w1, z1*] by Lm1;

 consider x2,y2,w2,z2 be Element of REAL such that

 A2: c2 = [*x2, y2, w2, z2*] by Lm1;

 consider x3,y3,w3,z3 be Element of REAL such that

 A3: c3 = [*x3, y3, w3, z3*] by Lm1;



 A4: (c1 * (c2 + c3)) = (c1 * [*(x2 + x3), (y2 + y3), (w2 + w3), (z2 + z3)*]) by A2, A3, QUATERNI:def 7

 .= [*((((x1 * (x2 + x3)) - (y1 * (y2 + y3))) - (w1 * (w2 + w3))) - (z1 * (z2 + z3))), ((((x1 * (y2 + y3)) + (y1 * (x2 + x3))) + (w1 * (z2 + z3))) - (z1 * (w2 + w3))), ((((x1 * (w2 + w3)) + ((x2 + x3) * w1)) + ((y2 + y3) * z1)) - ((z2 + z3) * y1)), ((((x1 * (z2 + z3)) + (z1 * (x2 + x3))) + (y1 * (w2 + w3))) - (w1 * (y2 + y3)))*] by A1, QUATERNI:def 10

 .= [*(((((x1 * x2) + (x1 * x3)) - ((y1 * y2) + (y1 * y3))) - ((w1 * w2) + (w1 * w3))) - ((z1 * z2) + (z1 * z3))), (((((x1 * y2) + (x1 * y3)) + ((y1 * x2) + (y1 * x3))) + ((w1 * z2) + (w1 * z3))) - ((z1 * w2) + (z1 * w3))), (((((x1 * w2) + (x1 * w3)) + ((x2 * w1) + (x3 * w1))) + ((y2 * z1) + (y3 * z1))) - ((z2 * y1) + (z3 * y1))), (((((x1 * z2) + (x1 * z3)) + ((z1 * x2) + (z1 * x3))) + ((y1 * w2) + (y1 * w3))) - ((w1 * y2) + (w1 * y3)))*];

 ((c1 * c2) + (c1 * c3)) = ( [*((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2)), ((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2)), ((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1)), ((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2))*] + (c1 * c3)) by A1, A2, QUATERNI:def 10

 .= ( [*((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2)), ((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2)), ((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1)), ((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2))*] + [*((((x1 * x3) - (y1 * y3)) - (w1 * w3)) - (z1 * z3)), ((((x1 * y3) + (y1 * x3)) + (w1 * z3)) - (z1 * w3)), ((((x1 * w3) + (x3 * w1)) + (y3 * z1)) - (z3 * y1)), ((((x1 * z3) + (z1 * x3)) + (y1 * w3)) - (w1 * y3))*]) by A1, A3, QUATERNI:def 10

 .= [*(((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2)) + ((((x1 * x3) - (y1 * y3)) - (w1 * w3)) - (z1 * z3))), (((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2)) + ((((x1 * y3) + (y1 * x3)) + (w1 * z3)) - (z1 * w3))), (((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1)) + ((((x1 * w3) + (x3 * w1)) + (y3 * z1)) - (z3 * y1))), (((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2)) + ((((x1 * z3) + (z1 * x3)) + (y1 * w3)) - (w1 * y3)))*] by QUATERNI:def 7;

 hence thesis by A4;

 end;

 theorem :: QUATERN2:18



 Th18: ((c1 + c2) * c3) = ((c1 * c3) + (c2 * c3))

 proof

 consider x1,y1,w1,z1 be Element of REAL such that

 A1: c1 = [*x1, y1, w1, z1*] by Lm1;

 consider x2,y2,w2,z2 be Element of REAL such that

 A2: c2 = [*x2, y2, w2, z2*] by Lm1;

 consider x3,y3,w3,z3 be Element of REAL such that

 A3: c3 = [*x3, y3, w3, z3*] by Lm1;



 A4: ((c1 + c2) * c3) = ( [*(x1 + x2), (y1 + y2), (w1 + w2), (z1 + z2)*] * c3) by A1, A2, QUATERNI:def 7

 .= [*(((((x1 + x2) * x3) - ((y1 + y2) * y3)) - ((w1 + w2) * w3)) - ((z1 + z2) * z3)), (((((x1 + x2) * y3) + ((y1 + y2) * x3)) + ((w1 + w2) * z3)) - ((z1 + z2) * w3)), (((((x1 + x2) * w3) + (x3 * (w1 + w2))) + (y3 * (z1 + z2))) - (z3 * (y1 + y2))), (((((x1 + x2) * z3) + ((z1 + z2) * x3)) + ((y1 + y2) * w3)) - ((w1 + w2) * y3))*] by A3, QUATERNI:def 10

 .= [*(((((x1 * x3) + (x2 * x3)) - ((y1 * y3) + (y2 * y3))) - ((w1 * w3) + (w2 * w3))) - ((z1 * z3) + (z2 * z3))), (((((x1 * y3) + (x2 * y3)) + ((y1 * x3) + (y2 * x3))) + ((w1 * z3) + (w2 * z3))) - ((z1 * w3) + (z2 * w3))), (((((x1 * w3) + (x2 * w3)) + ((x3 * w1) + (x3 * w2))) + ((y3 * z1) + (y3 * z2))) - ((z3 * y1) + (z3 * y2))), (((((x1 * z3) + (x2 * z3)) + ((z1 * x3) + (z2 * x3))) + ((y1 * w3) + (y2 * w3))) - ((w1 * y3) + (w2 * y3)))*];

 ((c1 * c3) + (c2 * c3)) = ( [*((((x1 * x3) - (y1 * y3)) - (w1 * w3)) - (z1 * z3)), ((((x1 * y3) + (y1 * x3)) + (w1 * z3)) - (z1 * w3)), ((((x1 * w3) + (x3 * w1)) + (y3 * z1)) - (z3 * y1)), ((((x1 * z3) + (z1 * x3)) + (y1 * w3)) - (w1 * y3))*] + (c2 * c3)) by A1, A3, QUATERNI:def 10

 .= ( [*((((x1 * x3) - (y1 * y3)) - (w1 * w3)) - (z1 * z3)), ((((x1 * y3) + (y1 * x3)) + (w1 * z3)) - (z1 * w3)), ((((x1 * w3) + (x3 * w1)) + (y3 * z1)) - (z3 * y1)), ((((x1 * z3) + (z1 * x3)) + (y1 * w3)) - (w1 * y3))*] + [*((((x2 * x3) - (y2 * y3)) - (w2 * w3)) - (z2 * z3)), ((((x2 * y3) + (y2 * x3)) + (w2 * z3)) - (z2 * w3)), ((((x2 * w3) + (x3 * w2)) + (y3 * z2)) - (z3 * y2)), ((((x2 * z3) + (z2 * x3)) + (y2 * w3)) - (w2 * y3))*]) by A2, A3, QUATERNI:def 10

 .= [*(((((x1 * x3) - (y1 * y3)) - (w1 * w3)) - (z1 * z3)) + ((((x2 * x3) - (y2 * y3)) - (w2 * w3)) - (z2 * z3))), (((((x1 * y3) + (y1 * x3)) + (w1 * z3)) - (z1 * w3)) + ((((x2 * y3) + (y2 * x3)) + (w2 * z3)) - (z2 * w3))), (((((x1 * w3) + (x3 * w1)) + (y3 * z1)) - (z3 * y1)) + ((((x2 * w3) + (x3 * w2)) + (y3 * z2)) - (z3 * y2))), (((((x1 * z3) + (z1 * x3)) + (y1 * w3)) - (w1 * y3)) + ((((x2 * z3) + (z2 * x3)) + (y2 * w3)) - (w2 * y3)))*] by QUATERNI:def 7;

 hence thesis by A4;

 end;

 theorem :: QUATERN2:19



 Th19: ( - c) = (( - 1q ) * c)

 proof

 consider x,y,w,z be Element of REAL such that

 A1: c = [*x, y, w, z*] by Lm1;



 A2: (c + [*( - x), ( - y), ( - w), ( - z)*]) = [*(x + ( - x)), (y + ( - y)), (w + ( - w)), (z + ( - z))*] by A1, QUATERNI:def 7

 .= [*( In ( 0 , REAL )), ( In ( 0 , REAL ))*] by QUATERNI: 91

 .= 0 by ARYTM_0:def 5;

 1q = [*jj, ( In ( 0 , REAL ))*] by ARYTM_0:def 5

 .= [*1, 0 , 0 , 0 *] by QUATERNI: 91;



 then ( 1q + [*( - 1), 0 , 0 , 0 *]) = [*(jj + ( - jj)), ( 0 + 0 ), ( 0 + 0 ), ( 0 + 0 )*] by QUATERNI:def 7

 .= [*( In ( 0 , REAL )), ( In ( 0 , REAL ))*] by QUATERNI: 91

 .= 0 by ARYTM_0:def 5;



 then (( - 1q ) * c) = ( [*( - 1), 0 , 0 , 0 *] * [*x, y, w, z*]) by A1, QUATERNI:def 8

 .= [*((((( - 1) * x) - ( 0 * y)) - ( 0 * w)) - ( 0 * z)), ((((( - 1) * y) + ( 0 * x)) + ( 0 * z)) - ( 0 * w)), ((((( - 1) * w) + (x * 0 )) + (y * 0 )) - (z * 0 )), ((((( - jj) * z) + ( 0 * x)) + ( 0 * w)) - ( 0 * y))*] by QUATERNI:def 10;

 hence thesis by A2, QUATERNI:def 8;

 end;

 theorem :: QUATERN2:20



 Th20: (( - c1) * c2) = ( - (c1 * c2))

 proof

 consider x1,y1,w1,z1 be Element of REAL such that

 A1: c1 = [*x1, y1, w1, z1*] by Lm1;

 consider x2,y2,w2,z2 be Element of REAL such that

 A2: c2 = [*x2, y2, w2, z2*] by Lm1;



 A3: (( - c1) * c2) = ( [*( - x1), ( - y1), ( - w1), ( - z1)*] * [*x2, y2, w2, z2*]) by A1, A2, Th4

 .= [*((((( - x1) * x2) - (( - y1) * y2)) - (( - w1) * w2)) - (( - z1) * z2)), ((((( - x1) * y2) + (( - y1) * x2)) + (( - w1) * z2)) - (( - z1) * w2)), ((((( - x1) * w2) + (x2 * ( - w1))) + (y2 * ( - z1))) - (z2 * ( - y1))), ((((( - x1) * z2) + (( - z1) * x2)) + (( - y1) * w2)) - (( - w1) * y2))*] by QUATERNI:def 10

 .= [*(((( - (x1 * x2)) + (y1 * y2)) + (w1 * w2)) + (z1 * z2)), (((( - (x1 * y2)) - (y1 * x2)) - (w1 * z2)) + (z1 * w2)), (((( - (x1 * w2)) - (x2 * w1)) - (y2 * z1)) + (z2 * y1)), (((( - (x1 * z2)) - (z1 * x2)) - (y1 * w2)) + (w1 * y2))*];

 (c1 * c2) = [*((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2)), ((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2)), ((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1)), ((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2))*] by A1, A2, QUATERNI:def 10;



 then ((( - c1) * c2) + (c1 * c2)) = [*((((( - (x1 * x2)) + (y1 * y2)) + (w1 * w2)) + (z1 * z2)) + ((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2))), ((((( - (x1 * y2)) - (y1 * x2)) - (w1 * z2)) + (z1 * w2)) + ((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2))), ((((( - (x1 * w2)) - (x2 * w1)) - (y2 * z1)) + (z2 * y1)) + ((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1))), ((((( - (x1 * z2)) - (z1 * x2)) - (y1 * w2)) + (w1 * y2)) + ((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2)))*] by A3, QUATERNI:def 7

 .= [*( In ( 0 , REAL )), ( In ( 0 , REAL ))*] by QUATERNI: 91

 .= 0 by ARYTM_0:def 5;

 hence thesis by QUATERNI:def 8;

 end;

 theorem :: QUATERN2:21



 Th21: (c1 * ( - c2)) = ( - (c1 * c2))

 proof

 consider x1,y1,w1,z1 be Element of REAL such that

 A1: c1 = [*x1, y1, w1, z1*] by Lm1;

 consider x2,y2,w2,z2 be Element of REAL such that

 A2: c2 = [*x2, y2, w2, z2*] by Lm1;



 A3: (c1 * ( - c2)) = ( [*x1, y1, w1, z1*] * [*( - x2), ( - y2), ( - w2), ( - z2)*]) by A1, A2, Th4

 .= [*((((x1 * ( - x2)) - (y1 * ( - y2))) - (w1 * ( - w2))) - (z1 * ( - z2))), ((((x1 * ( - y2)) + (y1 * ( - x2))) + (w1 * ( - z2))) - (z1 * ( - w2))), ((((x1 * ( - w2)) + (( - x2) * w1)) + (( - y2) * z1)) - (( - z2) * y1)), ((((x1 * ( - z2)) + (z1 * ( - x2))) + (y1 * ( - w2))) - (w1 * ( - y2)))*] by QUATERNI:def 10

 .= [*(((( - (x1 * x2)) + (y1 * y2)) + (w1 * w2)) + (z1 * z2)), (((( - (x1 * y2)) - (y1 * x2)) - (w1 * z2)) + (z1 * w2)), (((( - (x1 * w2)) - (x2 * w1)) - (y2 * z1)) + (z2 * y1)), (((( - (x1 * z2)) - (z1 * x2)) - (y1 * w2)) + (w1 * y2))*];

 (c1 * c2) = [*((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2)), ((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2)), ((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1)), ((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2))*] by A1, A2, QUATERNI:def 10;



 then ((c1 * ( - c2)) + (c1 * c2)) = [*((((( - (x1 * x2)) + (y1 * y2)) + (w1 * w2)) + (z1 * z2)) + ((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2))), ((((( - (x1 * y2)) - (y1 * x2)) - (w1 * z2)) + (z1 * w2)) + ((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2))), ((((( - (x1 * w2)) - (x2 * w1)) - (y2 * z1)) + (z2 * y1)) + ((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1))), ((((( - (x1 * z2)) - (z1 * x2)) - (y1 * w2)) + (w1 * y2)) + ((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2)))*] by A3, QUATERNI:def 7

 .= [*( In ( 0 , REAL )), ( In ( 0 , REAL ))*] by QUATERNI: 91

 .= 0 by ARYTM_0:def 5;

 hence thesis by QUATERNI:def 8;

 end;

 theorem :: QUATERN2:22



 Th22: (( - c1) * ( - c2)) = (c1 * c2)

 proof

 consider x1,y1,w1,z1 be Element of REAL such that

 A1: c1 = [*x1, y1, w1, z1*] by Lm1;

 consider x2,y2,w2,z2 be Element of REAL such that

 A2: c2 = [*x2, y2, w2, z2*] by Lm1;

 ( - c1) = [*( - x1), ( - y1), ( - w1), ( - z1)*] by A1, Th4;



 then (( - c1) * ( - c2)) = ( [*( - x1), ( - y1), ( - w1), ( - z1)*] * [*( - x2), ( - y2), ( - w2), ( - z2)*]) by A2, Th4

 .= [*((((( - x1) * ( - x2)) - (( - y1) * ( - y2))) - (( - w1) * ( - w2))) - (( - z1) * ( - z2))), ((((( - x1) * ( - y2)) + (( - y1) * ( - x2))) + (( - w1) * ( - z2))) - (( - z1) * ( - w2))), ((((( - x1) * ( - w2)) + (( - x2) * ( - w1))) + (( - y2) * ( - z1))) - (( - z2) * ( - y1))), ((((( - x1) * ( - z2)) + (( - z1) * ( - x2))) + (( - y1) * ( - w2))) - (( - w1) * ( - y2)))*] by QUATERNI:def 10

 .= [*((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2)), ((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2)), ((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1)), ((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2))*]

 .= (c1 * c2) by A1, A2, QUATERNI:def 10;

 hence thesis;

 end;

 theorem :: QUATERN2:23



 Th23: ((c1 - c2) * c3) = ((c1 * c3) - (c2 * c3))

 proof

 ((c1 - c2) * c3) = ((c1 * c3) + (( - c2) * c3)) by Th18;

 hence thesis by Th20;

 end;

 theorem :: QUATERN2:24



 Th24: (c1 * (c2 - c3)) = ((c1 * c2) - (c1 * c3))

 proof

 (c1 * (c2 - c3)) = ((c1 * c2) + (c1 * ( - c3))) by Th17;

 hence thesis by Th21;

 end;

 theorem :: QUATERN2:25



 Th25: ( [*x1, x2, x3, x4*] *' ) = [*x1, ( - x2), ( - x3), ( - x4)*]

 proof

 set c = [*x1, x2, x3, x4*];



 A1: ( Rea c) = x1 by QUATERNI: 23;



 A2: ( Im1 c) = x2 by QUATERNI: 23;



 A3: ( Im2 c) = x3 by QUATERNI: 23;

 ( Im3 c) = x4 by QUATERNI: 23;

 hence thesis by A1, A2, A3, QUATERNI: 43;

 end;

 theorem :: QUATERN2:26

 ((c *' ) *' ) = c

 proof



 A1: ( Rea (c *' )) = ( Rea c) by QUATERNI: 44;



 A2: ( Im1 (c *' )) = ( - ( Im1 c)) by QUATERNI: 44;



 A3: ( Im2 (c *' )) = ( - ( Im2 c)) by QUATERNI: 44;

 ( Im3 (c *' )) = ( - ( Im3 c)) by QUATERNI: 44;



 then ((c *' ) *' ) = [*( Rea c), ( - ( - ( Im1 c))), ( - ( - ( Im2 c))), ( - ( - ( Im3 c)))*] by A1, A2, A3, QUATERNI: 43

 .= c by QUATERNI: 24;

 hence thesis;

 end;

 definition

 let q, r;

 consider q0,q1,q2,q3 be Element of REAL such that

 A1: q = [*q0, q1, q2, q3*] by Lm1;

 consider r0,r1,r2,r3 be Element of REAL such that

 A2: r = [*r0, r1, r2, r3*] by Lm1;

 :: QUATERN2:def1

 func q / r -> Number means

 : Def1: ex q0,q1,q2,q3,r0,r1,r2,r3 be 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

 proof

 take [*(((((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 ))*];

 thus thesis by A1, A2;

 end;

 uniqueness

 proof

 let c1,c2 be Number;

 given q0,q1,q2,q3,r0,r1,r2,r3 be Element of REAL such that

 A3: q = [*q0, q1, q2, q3*] and

 A4: r = [*r0, r1, r2, r3*] and

 A5: c1 = [*(((((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 ))*];

 given q09,q19,q29,q39,r09,r19,r29,r39 be Element of REAL such that

 A6: q = [*q09, q19, q29, q39*] and

 A7: r = [*r09, r19, r29, r39*] and

 A8: c2 = [*(((((r09 * q09) + (r19 * q19)) + (r29 * q29)) + (r39 * q39)) / ( |.r.| ^2 )), (((((r09 * q19) - (r19 * q09)) - (r29 * q39)) + (r39 * q29)) / ( |.r.| ^2 )), (((((r09 * q29) + (r19 * q39)) - (r29 * q09)) - (r39 * q19)) / ( |.r.| ^2 )), (((((r09 * q39) - (r19 * q29)) + (r29 * q19)) - (r39 * q09)) / ( |.r.| ^2 ))*];



 A9: q0 = q09 by A3, A6, QUATERNI: 12;



 A10: q1 = q19 by A3, A6, QUATERNI: 12;



 A11: q2 = q29 by A3, A6, QUATERNI: 12;



 A12: q3 = q39 by A3, A6, QUATERNI: 12;



 A13: r0 = r09 by A4, A7, QUATERNI: 12;



 A14: r1 = r19 by A4, A7, QUATERNI: 12;



 A15: r2 = r29 by A4, A7, QUATERNI: 12;

 r3 = r39 by A4, A7, QUATERNI: 12;

 hence thesis by A5, A8, A9, A10, A11, A12, A13, A14, A15;

 end;

 end

 registration

 let q, r;

 cluster (q / r) -> quaternion;

 coherence

 proof

 ex q0,q1,q2,q3,r0,r1,r2,r3 be Element of REAL st q = [*q0, q1, q2, q3*] & r = [*r0, r1, r2, r3*] & (q / r) = [*(((((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 ))*] by Def1;

 hence thesis;

 end;

 end

 definition

 let q, r;

 :: original: /

 redefine

 func q / r -> Element of QUATERNION ;

 coherence by QUATERNI:def 2;

 end

 theorem :: QUATERN2:27

 (q / r) = ((((((((( Rea r) * ( Rea q)) + (( Im1 q) * ( Im1 r))) + (( Im2 r) * ( Im2 q))) + (( Im3 r) * ( Im3 q))) / ( |.r.| ^2 )) + ((((((( Rea r) * ( Im1 q)) - (( Im1 r) * ( Rea q))) - (( Im2 r) * ( Im3 q))) + (( Im3 r) * ( Im2 q))) / ( |.r.| ^2 )) * )) + ((((((( Rea r) * ( Im2 q)) + (( Im1 r) * ( Im3 q))) - (( Im2 r) * ( Rea q))) - (( Im3 r) * ( Im1 q))) / ( |.r.| ^2 )) * <j> )) + ((((((( Rea r) * ( Im3 q)) - (( Im1 r) * ( Im2 q))) + (( Im2 r) * ( Im1 q))) - (( Im3 r) * ( Rea q))) / ( |.r.| ^2 )) * <k> ))

 proof

 consider q0,q1,q2,q3 be Element of REAL such that

 A1: q = [*q0, q1, q2, q3*] by Lm1;

 consider r0,r1,r2,r3 be Element of REAL such that

 A2: r = [*r0, r1, r2, r3*] by Lm1;



 A3: ( Rea q) = q0 by A1, QUATERNI: 23;



 A4: ( Im1 q) = q1 by A1, QUATERNI: 23;



 A5: ( Im2 q) = q2 by A1, QUATERNI: 23;



 A6: ( Im3 q) = q3 by A1, QUATERNI: 23;



 A7: ( Rea r) = r0 by A2, QUATERNI: 23;



 A8: ( Im1 r) = r1 by A2, QUATERNI: 23;



 A9: ( Im2 r) = r2 by A2, QUATERNI: 23;



 A10: ( Im3 r) = r3 by A2, QUATERNI: 23;

 (q / r) = [*(((((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 ))*] by A1, A2, Def1

 .= ((((((((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 )) * <j> )) + ((((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / ( |.r.| ^2 )) * <k> )) by Th1;

 hence thesis by A3, A4, A5, A6, A7, A8, A9, A10;

 end;

 definition

 let c;

 :: QUATERN2:def2

 func c " -> Quaternion equals ( 1q / c);

 coherence ;

 end

 definition

 let r;

 :: original: "

 redefine

 func r " -> Element of QUATERNION ;

 coherence ;

 end

 theorem :: QUATERN2:28

 (r " ) = ((((( Rea r) / ( |.r.| ^2 )) - ((( Im1 r) / ( |.r.| ^2 )) * )) - ((( Im2 r) / ( |.r.| ^2 )) * <j> )) - ((( Im3 r) / ( |.r.| ^2 )) * <k> ))

 proof



 A1: 1q = [*jj, ( In ( 0 , REAL ))*] by ARYTM_0:def 5

 .= [*jj, 0 , 0 , 0 *] by QUATERNI: 91;

 consider q0,q1,q2,q3,r0,r1,r2,r3 be Element of REAL such that

 A2: 1q = [*q0, q1, q2, q3*] and

 A3: r = [*r0, r1, r2, r3*] and

 A4: (r " ) = [*(((((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 ))*] by Def1;



 A5: ( Rea r) = r0 by A3, QUATERNI: 23;



 A6: ( Im1 r) = r1 by A3, QUATERNI: 23;



 A7: ( Im2 r) = r2 by A3, QUATERNI: 23;



 A8: q0 = jj by A1, A2, QUATERNI: 12;



 A9: q1 = 0 by A1, A2, QUATERNI: 12;



 A10: q2 = 0 by A1, A2, QUATERNI: 12;

 q3 = 0 by A1, A2, QUATERNI: 12;



 then (r " ) = ((((r0 / ( |.r.| ^2 )) + (( - (r1 / ( |.r.| ^2 ))) * )) + (( - (r2 / ( |.r.| ^2 ))) * <j> )) + (( - (r3 / ( |.r.| ^2 ))) * <k> )) by Th1, A4, A8, A9, A10

 .= ((((r0 / ( |.r.| ^2 )) + ( - ((r1 / ( |.r.| ^2 )) * ))) + (( - (r2 / ( |.r.| ^2 ))) * <j> )) + (( - (r3 / ( |.r.| ^2 ))) * <k> )) by Th9

 .= ((((r0 / ( |.r.| ^2 )) - ((r1 / ( |.r.| ^2 )) * )) + ( - ((r2 / ( |.r.| ^2 )) * <j> ))) + (( - (r3 / ( |.r.| ^2 ))) * <k> )) by Th9

 .= ((((r0 / ( |.r.| ^2 )) - ((r1 / ( |.r.| ^2 )) * )) - ((r2 / ( |.r.| ^2 )) * <j> )) + ( - ((r3 / ( |.r.| ^2 )) * <k> ))) by Th9;

 hence thesis by A3, A5, A6, A7, QUATERNI: 23;

 end;

 theorem :: QUATERN2:29

 ( Rea (r " )) = (( Rea r) / ( |.r.| ^2 )) & ( Im1 (r " )) = ( - (( Im1 r) / ( |.r.| ^2 ))) & ( Im2 (r " )) = ( - (( Im2 r) / ( |.r.| ^2 ))) & ( Im3 (r " )) = ( - (( Im3 r) / ( |.r.| ^2 )))

 proof

 consider q0,q1,q2,q3,r0,r1,r2,r3 be Element of REAL such that

 A1: 1q = [*q0, q1, q2, q3*] and

 A2: r = [*r0, r1, r2, r3*] and

 A3: (r " ) = [*(((((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 ))*] by Def1;



 A4: 1q = [*jj, ( In ( 0 , REAL ))*] by ARYTM_0:def 5

 .= [*jj, 0 , 0 , 0 *] by QUATERNI: 91;

 then

 A5: q0 = jj by A1, QUATERNI: 12;



 A6: q1 = 0 by A1, A4, QUATERNI: 12;



 A7: q2 = 0 by A1, A4, QUATERNI: 12;



 A8: q3 = 0 by A1, A4, QUATERNI: 12;



 A9: ( Rea r) = r0 by A2, QUATERNI: 23;



 A10: ( Im1 r) = r1 by A2, QUATERNI: 23;



 A11: ( Im2 r) = r2 by A2, QUATERNI: 23;



 A12: ( Im3 r) = r3 by A2, QUATERNI: 23;

 (r " ) = [*(r0 / ( |.r.| ^2 )), ( - (r1 / ( |.r.| ^2 ))), ( - (r2 / ( |.r.| ^2 ))), ( - (r3 / ( |.r.| ^2 )))*] by A3, A5, A6, A7, A8;

 hence thesis by A9, A10, A11, A12, QUATERNI: 23;

 end;

 theorem :: QUATERN2:30

 ( Rea (q / r)) = (((((( Rea r) * ( Rea q)) + (( Im1 q) * ( Im1 r))) + (( Im2 r) * ( Im2 q))) + (( Im3 r) * ( Im3 q))) / ( |.r.| ^2 )) & ( Im1 (q / r)) = (((((( Rea r) * ( Im1 q)) - (( Im1 r) * ( Rea q))) - (( Im2 r) * ( Im3 q))) + (( Im3 r) * ( Im2 q))) / ( |.r.| ^2 )) & ( Im2 (q / r)) = (((((( Rea r) * ( Im2 q)) + (( Im1 r) * ( Im3 q))) - (( Im2 r) * ( Rea q))) - (( Im3 r) * ( Im1 q))) / ( |.r.| ^2 )) & ( Im3 (q / r)) = (((((( Rea r) * ( Im3 q)) - (( Im1 r) * ( Im2 q))) + (( Im2 r) * ( Im1 q))) - (( Im3 r) * ( Rea q))) / ( |.r.| ^2 ))

 proof

 consider q0,q1,q2,q3 be Element of REAL such that

 A1: q = [*q0, q1, q2, q3*] by Lm1;

 consider r0,r1,r2,r3 be Element of REAL such that

 A2: r = [*r0, r1, r2, r3*] by Lm1;



 A3: ( Rea q) = q0 by A1, QUATERNI: 23;



 A4: ( Im1 q) = q1 by A1, QUATERNI: 23;



 A5: ( Im2 q) = q2 by A1, QUATERNI: 23;



 A6: ( Im3 q) = q3 by A1, QUATERNI: 23;



 A7: ( Rea r) = r0 by A2, QUATERNI: 23;



 A8: ( Im1 r) = r1 by A2, QUATERNI: 23;



 A9: ( Im2 r) = r2 by A2, QUATERNI: 23;



 A10: ( Im3 r) = r3 by A2, QUATERNI: 23;

 (q / r) = [*(((((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 ))*] by A1, A2, Def1;

 hence thesis by A3, A4, A5, A6, A7, A8, A9, A10, QUATERNI: 23;

 end;



 Lm5: 0 in REAL by XREAL_0:def 1;

 theorem :: QUATERN2:31



 Th31: r <> 0 implies (r * (r " )) = 1

 proof

 assume

 A1: r <> 0 ;

 consider r0,r1,r2,r3 be Element of REAL such that

 A2: r = [*r0, r1, r2, r3*] by Lm1;



 A3: 1q = [*jj, ( In ( 0 , REAL ))*] by ARYTM_0:def 5

 .= [*1, 0 , 0 , 0 *] by QUATERNI: 91;



 A4: ( Rea r) = r0 by A2, QUATERNI: 23;



 A5: ( Im1 r) = r1 by A2, QUATERNI: 23;



 A6: ( Im2 r) = r2 by A2, QUATERNI: 23;



 A7: ( Im3 r) = r3 by A2, QUATERNI: 23;

 0 <= ((((( Rea r) ^2 ) + (( Im1 r) ^2 )) + (( Im2 r) ^2 )) + (( Im3 r) ^2 )) by QUATERNI: 74;

 then

 A8: ( |.r.| ^2 ) = ((((r0 ^2 ) + (r1 ^2 )) + (r2 ^2 )) + (r3 ^2 )) by A4, A5, A6, A7, SQUARE_1:def 2;



 A9: (r " ) = [*(((((r0 * 1) + (r1 * 0 )) + (r2 * 0 )) + (r3 * 0 )) / ( |.r.| ^2 )), (((((r0 * 0 ) - (r1 * 1)) - (r2 * 0 )) + (r3 * 0 )) / ( |.r.| ^2 )), (((((r0 * 0 ) + (r1 * 0 )) - (r2 * 1)) - (r3 * 0 )) / ( |.r.| ^2 )), (((((r0 * 0 ) - (r1 * 0 )) + (r2 * 0 )) - (r3 * jj)) / ( |.r.| ^2 ))*] by A2, A3, Def1, Lm5

 .= [*(r0 / ( |.r.| ^2 )), (( - r1) / ( |.r.| ^2 )), (( - r2) / ( |.r.| ^2 )), (( - r3) / ( |.r.| ^2 ))*];

 |.r.| <> 0 by A1, Th10;

 then

 A10: ( |.r.| ^2 ) > 0 by SQUARE_1: 12;

 (r * (r " )) = [*((((r0 * (r0 / ( |.r.| ^2 ))) - (r1 * (( - r1) / ( |.r.| ^2 )))) - (r2 * (( - r2) / ( |.r.| ^2 )))) - (r3 * (( - r3) / ( |.r.| ^2 )))), ((((r0 * (( - r1) / ( |.r.| ^2 ))) + (r1 * (r0 / ( |.r.| ^2 )))) + (r2 * (( - r3) / ( |.r.| ^2 )))) - (r3 * (( - r2) / ( |.r.| ^2 )))), ((((r0 * (( - r2) / ( |.r.| ^2 ))) + ((r0 / ( |.r.| ^2 )) * r2)) + ((( - r1) / ( |.r.| ^2 )) * r3)) - ((( - r3) / ( |.r.| ^2 )) * r1)), ((((r0 * (( - r3) / ( |.r.| ^2 ))) + (r3 * (r0 / ( |.r.| ^2 )))) + (r1 * (( - r2) / ( |.r.| ^2 )))) - (r2 * (( - r1) / ( |.r.| ^2 ))))*] by A2, A9, QUATERNI:def 10

 .= [*(( |.r.| ^2 ) / ( |.r.| ^2 )), 0 , 0 , 0 *] by A8

 .= [*1, 0 , 0 , 0 *] by A10, XCMPLX_1: 60

 .= [*jj, ( In ( 0 , REAL ))*] by QUATERNI: 91

 .= 1 by ARYTM_0:def 5;

 hence thesis;

 end;

 theorem :: QUATERN2:32

 r <> 0 implies ((r " ) * r) = 1

 proof

 assume

 A1: r <> 0 ;

 consider r0,r1,r2,r3 be Element of REAL such that

 A2: r = [*r0, r1, r2, r3*] by Lm1;



 A3: 1q = [*jj, ( In ( 0 , REAL ))*] by ARYTM_0:def 5

 .= [*1, 0 , 0 , 0 *] by QUATERNI: 91;



 A4: ( Rea r) = r0 by A2, QUATERNI: 23;



 A5: ( Im1 r) = r1 by A2, QUATERNI: 23;



 A6: ( Im2 r) = r2 by A2, QUATERNI: 23;



 A7: ( Im3 r) = r3 by A2, QUATERNI: 23;

 0 <= ((((( Rea r) ^2 ) + (( Im1 r) ^2 )) + (( Im2 r) ^2 )) + (( Im3 r) ^2 )) by QUATERNI: 74;

 then

 A8: ( |.r.| ^2 ) = ((((r0 ^2 ) + (r1 ^2 )) + (r2 ^2 )) + (r3 ^2 )) by A4, A5, A6, A7, SQUARE_1:def 2;



 A9: (r " ) = [*(((((r0 * 1) + (r1 * 0 )) + (r2 * 0 )) + (r3 * 0 )) / ( |.r.| ^2 )), (((((r0 * 0 ) - (r1 * 1)) - (r2 * 0 )) + (r3 * 0 )) / ( |.r.| ^2 )), (((((r0 * 0 ) + (r1 * 0 )) - (r2 * 1)) - (r3 * 0 )) / ( |.r.| ^2 )), (((((r0 * 0 ) - (r1 * 0 )) + (r2 * 0 )) - (r3 * jj)) / ( |.r.| ^2 ))*] by A2, A3, Def1, Lm5

 .= [*(r0 / ( |.r.| ^2 )), (( - r1) / ( |.r.| ^2 )), (( - r2) / ( |.r.| ^2 )), (( - r3) / ( |.r.| ^2 ))*];

 |.r.| <> 0 by A1, Th10;

 then

 A10: ( |.r.| ^2 ) > 0 by SQUARE_1: 12;

 ((r " ) * r) = [*((((r0 * (r0 / ( |.r.| ^2 ))) - (r1 * (( - r1) / ( |.r.| ^2 )))) - (r2 * (( - r2) / ( |.r.| ^2 )))) - (r3 * (( - r3) / ( |.r.| ^2 )))), ((((r0 * (( - r1) / ( |.r.| ^2 ))) + (r1 * (r0 / ( |.r.| ^2 )))) + (r2 * (( - r3) / ( |.r.| ^2 )))) - (r3 * (( - r2) / ( |.r.| ^2 )))), ((((r0 * (( - r2) / ( |.r.| ^2 ))) + ((r0 / ( |.r.| ^2 )) * r2)) + ((( - r1) / ( |.r.| ^2 )) * r3)) - ((( - r3) / ( |.r.| ^2 )) * r1)), ((((r0 * (( - r3) / ( |.r.| ^2 ))) + (r3 * (r0 / ( |.r.| ^2 )))) + (r1 * (( - r2) / ( |.r.| ^2 )))) - (r2 * (( - r1) / ( |.r.| ^2 ))))*] by A2, A9, QUATERNI:def 10

 .= [*(( |.r.| ^2 ) / ( |.r.| ^2 )), 0 , 0 , 0 *] by A8

 .= [*1, 0 , 0 , 0 *] by A10, XCMPLX_1: 60

 .= [*jj, ( In ( 0 , REAL ))*] by QUATERNI: 91

 .= 1 by ARYTM_0:def 5;

 hence thesis;

 end;

 theorem :: QUATERN2:33



 Th33: c <> 0q implies (c / c) = 1q

 proof

 assume

 A1: c <> 0q ;

 consider x1,x2,x3,x4 be Element of REAL such that

 A2: c = [*x1, x2, x3, x4*] by Lm1;

 |.c.| > 0 by A1, Th10;

 then

 A3: ( |.c.| ^2 ) > 0 by SQUARE_1: 12;



 A4: ( Rea c) = x1 by A2, QUATERNI: 23;



 A5: ( Im1 c) = x2 by A2, QUATERNI: 23;



 A6: ( Im2 c) = x3 by A2, QUATERNI: 23;



 A7: ( Im3 c) = x4 by A2, QUATERNI: 23;



 A8: ((((x1 ^2 ) + (x2 ^2 )) + (x3 ^2 )) + (x4 ^2 )) >= 0 by Lm2;

 (c / c) = [*(((((x1 * x1) + (x2 * x2)) + (x3 * x3)) + (x4 * x4)) / ( |.c.| ^2 )), (((((x1 * x2) - (x2 * x1)) - (x3 * x4)) + (x4 * x3)) / ( |.c.| ^2 )), (((((x1 * x3) + (x2 * x4)) - (x3 * x1)) - (x4 * x2)) / ( |.c.| ^2 )), (((((x1 * x4) - (x2 * x3)) + (x3 * x2)) - (x4 * x1)) / ( |.c.| ^2 ))*] by A2, Def1

 .= [*(( |.c.| ^2 ) / ( |.c.| ^2 )), 0 , 0 , 0 *] by A4, A5, A6, A7, A8, SQUARE_1:def 2

 .= [*1, 0 , 0 , 0 *] by A3, XCMPLX_1: 60

 .= [*jj, ( In ( 0 , REAL ))*] by QUATERNI: 91

 .= 1 by ARYTM_0:def 5;

 hence thesis;

 end;

 theorem :: QUATERN2:34

 (( - c) " ) = ( - (c " ))

 proof



 A1: 1q = [*jj, ( In ( 0 , REAL ))*] by ARYTM_0:def 5

 .= [*1, 0 , 0 , 0 *] by QUATERNI: 91;

 consider x1,x2,x3,x4 be Element of REAL such that

 A2: c = [*x1, x2, x3, x4*] by Lm1;



 A3: ( - c) = [*( - x1), ( - x2), ( - x3), ( - x4)*] by A2, Th4;



 A4: |.( - c).| = |.c.| by QUATERNI: 72;



 A5: (c " ) = [*(((((x1 * 1) + (x2 * 0 )) + (x3 * 0 )) + (x4 * 0 )) / ( |.c.| ^2 )), (((((x1 * 0 ) - (x2 * 1)) - (x3 * 0 )) + (x4 * 0 )) / ( |.c.| ^2 )), (((((x1 * 0 ) + (x2 * 0 )) - (x3 * 1)) - (x4 * 0 )) / ( |.c.| ^2 )), (((((x1 * 0 ) - (x2 * 0 )) + (x3 * 0 )) - (x4 * jj)) / ( |.c.| ^2 ))*] by A1, A2, Def1, Lm5

 .= [*(x1 / ( |.c.| ^2 )), ( - (x2 / ( |.c.| ^2 ))), ( - (x3 / ( |.c.| ^2 ))), ( - (x4 / ( |.c.| ^2 )))*];

 (( - c) " ) = [*(((((( - x1) * 1) + (( - x2) * 0 )) + (( - x3) * 0 )) + (( - x4) * 0 )) / ( |.( - c).| ^2 )), (((((( - x1) * 0 ) - (( - x2) * 1)) - (( - x3) * 0 )) + (( - x4) * 0 )) / ( |.( - c).| ^2 )), (((((( - x1) * 0 ) + (( - x2) * 0 )) - (( - x3) * 1)) - (( - x4) * 0 )) / ( |.( - c).| ^2 )), (((((( - x1) * 0 ) - (( - x2) * 0 )) + (( - x3) * 0 )) - (( - x4) * jj)) / ( |.( - c).| ^2 ))*] by A1, A3, Def1, Lm5

 .= [*( - (x1 / ( |.c.| ^2 ))), (x2 / ( |.c.| ^2 )), (x3 / ( |.c.| ^2 )), (x4 / ( |.c.| ^2 ))*] by A4;



 then ((c " ) + (( - c) " )) = [*((x1 / ( |.c.| ^2 )) + ( - (x1 / ( |.c.| ^2 )))), (( - (x2 / ( |.c.| ^2 ))) + (x2 / ( |.c.| ^2 ))), (( - (x3 / ( |.c.| ^2 ))) + (x3 / ( |.c.| ^2 ))), (( - (x4 / ( |.c.| ^2 ))) + (x4 / ( |.c.| ^2 )))*] by A5, QUATERNI:def 7

 .= [*( In ( 0 , REAL )), ( In ( 0 , REAL ))*] by QUATERNI: 91

 .= 0 by ARYTM_0:def 5;

 hence thesis by QUATERNI:def 8;

 end;

 definition

 :: QUATERN2:def3

 func compquaternion -> UnOp of QUATERNION means for c be Element of QUATERNION holds (it . c) = ( - c);

 existence from FUNCT_2:sch 4;

 uniqueness from BINOP_2:sch 1;

 :: QUATERN2:def4

 func addquaternion -> BinOp of QUATERNION means

 : Def4: for c1,c2 be Element of QUATERNION holds (it . (c1,c2)) = (c1 + c2);

 existence from BINOP_1:sch 4;

 uniqueness from BINOP_2:sch 2;

 :: QUATERN2:def5

 func diffquaternion -> BinOp of QUATERNION means for c1,c2 be Element of QUATERNION holds (it . (c1,c2)) = (c1 - c2);

 existence from BINOP_1:sch 4;

 uniqueness from BINOP_2:sch 2;

 :: QUATERN2:def6

 func multquaternion -> BinOp of QUATERNION means

 : Def6: for c1,c2 be Element of QUATERNION holds (it . (c1,c2)) = (c1 * c2);

 existence from BINOP_1:sch 4;

 uniqueness from BINOP_2:sch 2;

 :: QUATERN2:def7

 func divquaternion -> BinOp of QUATERNION means for c1,c2 be Element of QUATERNION holds (it . (c1,c2)) = (c1 / c2);

 existence from BINOP_1:sch 4;

 uniqueness from BINOP_2:sch 2;

 :: QUATERN2:def8

 func invquaternion -> UnOp of QUATERNION means for c be Element of QUATERNION holds (it . c) = (c " );

 existence from FUNCT_2:sch 4;

 uniqueness from BINOP_2:sch 1;

 end

 definition

 :: QUATERN2:def9

 func G_Quaternion -> strict addLoopStr means

 : Def9: the carrier of it = QUATERNION & the addF of it = addquaternion & ( 0. it ) = 0q ;

 existence

 proof

 take addLoopStr (# QUATERNION , addquaternion , 0q #);

 thus thesis;

 end;

 uniqueness ;

 end

 registration

 cluster G_Quaternion -> non empty;

 coherence by Def9;

 end

 registration

 cluster -> quaternion for Element of G_Quaternion ;

 coherence

 proof

 let c be Element of G_Quaternion ;

 c in the carrier of G_Quaternion ;

 then c in QUATERNION by Def9;

 hence thesis;

 end;

 end

 registration

 let x,y be Element of G_Quaternion ;

 let a,b be Quaternion;

 identify a + b with x + y when x = a, y = b;

 compatibility

 proof

 assume that

 A1: x = a and

 A2: y = b;

 reconsider a9 = a, b9 = b as Element of QUATERNION by QUATERNI:def 2;



 thus (x + y) = ( addquaternion . (a9,b9)) by A1, A2, Def9

 .= (a + b) by Def4;

 end;

 end

 theorem :: QUATERN2:35



 Th35: ( 0. G_Quaternion ) = 0q by Def9;

 registration

 cluster G_Quaternion -> Abelian add-associative right_zeroed right_complementable;

 coherence

 proof

 thus for x,y be Element of G_Quaternion holds (x + y) = (y + x);

 thus for x,y,z be Element of G_Quaternion holds ((x + y) + z) = (x + (y + z)) by Th2;

 thus for x be Element of G_Quaternion holds (x + ( 0. G_Quaternion )) = x

 proof

 let x be Element of G_Quaternion ;

 reconsider x1 = x as Element of QUATERNION by Def9;



 thus (x + ( 0. G_Quaternion )) = (the addF of G_Quaternion . (x1, 0q )) by Def9

 .= ( addquaternion . (x1, 0q )) by Def9

 .= (x1 + 0q ) by Def4

 .= x by Th3;

 end;

 thus G_Quaternion is right_complementable

 proof

 let x be Element of G_Quaternion ;

 reconsider x1 = x as Element of QUATERNION by Def9;

 reconsider y = ( - x1) as Element of G_Quaternion by Def9;

 take y;

 thus thesis by Th35, QUATERNI:def 8;

 end;

 end;

 end

 registration

 let x be Element of G_Quaternion , a be Quaternion;

 identify - a with - x when x = a;

 compatibility

 proof

 assume

 A1: x = a;

 reconsider x1 = x as Element of QUATERNION by Def9;

 reconsider b = ( - x1) as Element of G_Quaternion by Def9;

 (b + x) = ( 0. G_Quaternion ) by Th35, QUATERNI:def 8;

 hence thesis by A1, RLVECT_1: 6;

 end;

 end

 registration

 let x,y be Element of G_Quaternion ;

 let a,b be Quaternion;

 identify a - b with x - y when x = a, y = b;

 compatibility ;

 end

 theorem :: QUATERN2:36

 for x,y,z be Element of G_Quaternion holds (x + y) = (y + x) & ((x + y) + z) = (x + (y + z)) & (x + ( 0. G_Quaternion )) = x by RLVECT_1:def 3, RLVECT_1:def 4;

 definition

 :: QUATERN2:def10

 func R_Quaternion -> strict doubleLoopStr means

 : Def10: the carrier of it = QUATERNION & the addF of it = addquaternion & the multF of it = multquaternion & ( 1. it ) = 1q & ( 0. it ) = 0q ;

 existence

 proof

 take doubleLoopStr (# QUATERNION , addquaternion , multquaternion , 1q , 0q #);

 thus thesis;

 end;

 uniqueness ;

 end

 registration

 cluster R_Quaternion -> non empty;

 coherence by Def10;

 end

 registration

 cluster -> quaternion for Element of R_Quaternion ;

 coherence

 proof

 let c be Element of R_Quaternion ;

 c in the carrier of R_Quaternion ;

 then c in QUATERNION by Def10;

 hence thesis;

 end;

 end

 registration

 let a,b be Quaternion;

 let x,y be Element of R_Quaternion ;

 identify a + b with x + y when x = a, y = b;

 compatibility

 proof

 assume that

 A1: x = a and

 A2: y = b;

 reconsider a9 = a, b9 = b as Element of QUATERNION by QUATERNI:def 2;



 thus (x + y) = ( addquaternion . (a9,b9)) by A1, A2, Def10

 .= (a + b) by Def4;

 end;

 identify a * b with x * y when x = a, y = b;

 compatibility

 proof

 assume that

 A3: x = a and

 A4: y = b;

 reconsider a9 = a, b9 = b as Element of QUATERNION by QUATERNI:def 2;



 thus (x * y) = ( multquaternion . (a9,b9)) by A3, A4, Def10

 .= (a * b) by Def6;

 end;

 end

 registration

 cluster R_Quaternion -> well-unital;

 coherence

 proof

 let x be Element of R_Quaternion ;

 ( 1. R_Quaternion ) = 1q by Def10;

 hence thesis by Th14, Th15;

 end;

 end

 theorem :: QUATERN2:37

 ( 1. R_Quaternion ) = 1q by Def10;

 theorem :: QUATERN2:38

 ( 1_ R_Quaternion ) = 1q by Def10;

 theorem :: QUATERN2:39



 Th39: ( 0. R_Quaternion ) = 0q by Def10;

 registration

 cluster R_Quaternion -> add-associative right_zeroed right_complementable Abelian associative left_unital right_unital distributive almost_right_invertible non degenerated;

 coherence

 proof

 thus R_Quaternion is add-associative by Th2;

 thus R_Quaternion is right_zeroed

 proof

 let x be Element of R_Quaternion ;

 reconsider x1 = x as Element of QUATERNION by Def10;



 thus (x + ( 0. R_Quaternion )) = (the addF of R_Quaternion . (x1, 0q )) by Def10

 .= ( addquaternion . (x1, 0q )) by Def10

 .= (x1 + 0q ) by Def4

 .= x by Th3;

 end;

 thus R_Quaternion is right_complementable

 proof

 let x be Element of R_Quaternion ;

 reconsider x1 = x as Element of QUATERNION by Def10;

 reconsider y = ( - x1) as Element of R_Quaternion by Def10;

 take y;

 thus thesis by Th39, QUATERNI:def 8;

 end;

 thus R_Quaternion is Abelian;

 thus R_Quaternion is associative by Th16;

 thus R_Quaternion is left_unital right_unital;

 thus R_Quaternion is distributive by Th17, Th18;

 thus R_Quaternion is almost_right_invertible

 proof

 let x be Element of R_Quaternion ;

 assume

 A1: x <> ( 0. R_Quaternion );

 reconsider x1 = x as Element of QUATERNION by Def10;

 reconsider y = (x1 " ) as Element of R_Quaternion by Def10;

 take y;

 x1 <> 0q by A1, Def10;



 then (x * y) = 1 by Th31

 .= ( 1. R_Quaternion ) by Def10;

 hence thesis;

 end;

 ( 1. R_Quaternion ) = 1q by Def10;

 then ( 0. R_Quaternion ) <> ( 1. R_Quaternion ) by Def10;

 hence R_Quaternion is non degenerated;

 end;

 end

 registration

 let x be Element of R_Quaternion , a be Quaternion;

 identify - a with - x when x = a;

 compatibility

 proof

 assume

 A1: x = a;

 reconsider x1 = x as Element of QUATERNION by Def10;

 reconsider b = ( - x1) as Element of R_Quaternion by Def10;

 (b + x) = ( 0. R_Quaternion ) by Th39, QUATERNI:def 8;

 hence thesis by A1, RLVECT_1: 6;

 end;

 end

 registration

 let x,y be Element of R_Quaternion ;

 let a,b be Quaternion;

 identify a - b with x - y when x = a, y = b;

 compatibility ;

 end

 definition

 let z be Element of R_Quaternion ;

 :: original: *'

 redefine

 func z *' -> Element of R_Quaternion ;

 coherence by Def10;

 end

 reserve z for Element of R_Quaternion ;

 theorem :: QUATERN2:40

 ( - z) = (( - ( 1_ R_Quaternion )) * z)

 proof

 reconsider z9 = z as Element of QUATERNION by Def10;



 thus ( - z) = (( - 1q ) * z9) by Th19

 .= (( - ( 1_ R_Quaternion )) * z) by Def10;

 end;

 theorem :: QUATERN2:41

 (( 0. R_Quaternion ) *' ) = ( 0. R_Quaternion )

 proof

 ( 0. R_Quaternion ) = 0q by Def10;

 hence thesis by QUATERNI: 45;

 end;

 theorem :: QUATERN2:42

 (z *' ) = ( 0. R_Quaternion ) implies z = ( 0. R_Quaternion )

 proof

 assume (z *' ) = ( 0. R_Quaternion );

 then (z *' ) = 0q by Def10;

 then z = 0q by QUATERNI: 46;

 hence thesis by Def10;

 end;

 theorem :: QUATERN2:43

 (( 1. R_Quaternion ) *' ) = ( 1. R_Quaternion )

 proof

 ( 1. R_Quaternion ) = 1r by Def10;

 hence thesis by QUATERNI: 47;

 end;

 theorem :: QUATERN2:44

 |.( 0. R_Quaternion ).| = 0 by Def10, QUATERNI: 65;

 theorem :: QUATERN2:45

 |.z.| = 0 implies z = ( 0. R_Quaternion ) by Th39, QUATERNI: 66;

 theorem :: QUATERN2:46

 |.( 1. R_Quaternion ).| = 1 by Def10, QUATERNI: 68;

 theorem :: QUATERN2:47

 (( 1. R_Quaternion ) " ) = ( 1. R_Quaternion )

 proof

 ( 1q " ) = 1q by Th33

 .= ( 1. R_Quaternion ) by Def10;

 hence thesis by Def10;

 end;

 definition

 let x,y be Quaternion;

 :: QUATERN2:def11

 func x .|. y -> Element of QUATERNION equals (x * (y *' ));

 coherence ;

 end

 theorem :: QUATERN2:48



 Th48: (c1 .|. c2) = [*((((( Rea c1) * ( Rea c2)) + (( Im1 c1) * ( Im1 c2))) + (( Im2 c1) * ( Im2 c2))) + (( Im3 c1) * ( Im3 c2))), ((((( Rea c1) * ( - ( Im1 c2))) + (( Im1 c1) * ( Rea c2))) - (( Im2 c1) * ( Im3 c2))) + (( Im3 c1) * ( Im2 c2))), ((((( Rea c1) * ( - ( Im2 c2))) + (( Rea c2) * ( Im2 c1))) - (( Im1 c2) * ( Im3 c1))) + (( Im3 c2) * ( Im1 c1))), ((((( Rea c1) * ( - ( Im3 c2))) + (( Im3 c1) * ( Rea c2))) - (( Im1 c1) * ( Im2 c2))) + (( Im2 c1) * ( Im1 c2)))*]

 proof

 consider x1,y1,w1,z1 be Element of REAL such that

 A1: c1 = [*x1, y1, w1, z1*] by Lm1;

 consider x2,y2,w2,z2 be Element of REAL such that

 A2: c2 = [*x2, y2, w2, z2*] by Lm1;



 A3: ( Rea c1) = x1 by A1, QUATERNI: 23;



 A4: ( Im1 c1) = y1 by A1, QUATERNI: 23;



 A5: ( Im2 c1) = w1 by A1, QUATERNI: 23;



 A6: ( Im3 c1) = z1 by A1, QUATERNI: 23;



 A7: ( Rea c2) = x2 by A2, QUATERNI: 23;



 A8: ( Im1 c2) = y2 by A2, QUATERNI: 23;



 A9: ( Im2 c2) = w2 by A2, QUATERNI: 23;



 A10: ( Im3 c2) = z2 by A2, QUATERNI: 23;

 (c1 .|. c2) = ( [*x1, y1, w1, z1*] * [*x2, ( - y2), ( - w2), ( - z2)*]) by A1, A2, Th25

 .= [*((((x1 * x2) - (y1 * ( - y2))) - (w1 * ( - w2))) - (z1 * ( - z2))), ((((x1 * ( - y2)) + (y1 * x2)) + (w1 * ( - z2))) - (z1 * ( - w2))), ((((x1 * ( - w2)) + (x2 * w1)) + (( - y2) * z1)) - (( - z2) * y1)), ((((x1 * ( - z2)) + (z1 * x2)) + (y1 * ( - w2))) - (w1 * ( - y2)))*] by QUATERNI:def 10

 .= [*((((( Rea c1) * ( Rea c2)) + (( Im1 c1) * ( Im1 c2))) + (( Im2 c1) * ( Im2 c2))) + (( Im3 c1) * ( Im3 c2))), ((((( Rea c1) * ( - ( Im1 c2))) + (( Im1 c1) * ( Rea c2))) - (( Im2 c1) * ( Im3 c2))) + (( Im3 c1) * ( Im2 c2))), ((((( Rea c1) * ( - ( Im2 c2))) + (( Rea c2) * ( Im2 c1))) - (( Im1 c2) * ( Im3 c1))) + (( Im3 c2) * ( Im1 c1))), ((((( Rea c1) * ( - ( Im3 c2))) + (( Im3 c1) * ( Rea c2))) - (( Im1 c1) * ( Im2 c2))) + (( Im2 c1) * ( Im1 c2)))*] by A3, A4, A5, A6, A7, A8, A9, A10;

 hence thesis;

 end;

 theorem :: QUATERN2:49



 Th49: (c .|. c) = ( |.c.| ^2 )

 proof

 reconsider z = 0 , z1 = ((((( Rea c) ^2 ) + (( Im1 c) ^2 )) + (( Im2 c) ^2 )) + (( Im3 c) ^2 )) as Element of REAL by XREAL_0:def 1;



 A1: ((((( Rea c) ^2 ) + (( Im1 c) ^2 )) + (( Im2 c) ^2 )) + (( Im3 c) ^2 )) >= 0 by Lm2;

 (c .|. c) = [*((((( Rea c) * ( Rea c)) + (( Im1 c) * ( Im1 c))) + (( Im2 c) * ( Im2 c))) + (( Im3 c) * ( Im3 c))), ((((( Rea c) * ( - ( Im1 c))) + (( Im1 c) * ( Rea c))) - (( Im2 c) * ( Im3 c))) + (( Im3 c) * ( Im2 c))), ((((( Rea c) * ( - ( Im2 c))) + (( Rea c) * ( Im2 c))) - (( Im1 c) * ( Im3 c))) + (( Im3 c) * ( Im1 c))), ((((( Rea c) * ( - ( Im3 c))) + (( Im3 c) * ( Rea c))) - (( Im1 c) * ( Im2 c))) + (( Im2 c) * ( Im1 c)))*] by Th48

 .= [*z1, z*] by QUATERNI: 91

 .= ((((( Rea c) ^2 ) + (( Im1 c) ^2 )) + (( Im2 c) ^2 )) + (( Im3 c) ^2 )) by ARYTM_0:def 5

 .= ( |.c.| ^2 ) by A1, SQUARE_1:def 2;

 hence thesis;

 end;

 theorem :: QUATERN2:50

 ( Rea (c .|. c)) = ( |.c.| ^2 ) & ( Im1 (c .|. c)) = 0 & ( Im2 (c .|. c)) = 0 & ( Im2 (c .|. c)) = 0

 proof



 A1: ((((( Rea c) ^2 ) + (( Im1 c) ^2 )) + (( Im2 c) ^2 )) + (( Im3 c) ^2 )) >= 0 by Lm2;

 (c .|. c) = [*((((( Rea c) * ( Rea c)) + (( Im1 c) * ( Im1 c))) + (( Im2 c) * ( Im2 c))) + (( Im3 c) * ( Im3 c))), ((((( Rea c) * ( - ( Im1 c))) + (( Im1 c) * ( Rea c))) - (( Im2 c) * ( Im3 c))) + (( Im3 c) * ( Im2 c))), ((((( Rea c) * ( - ( Im2 c))) + (( Rea c) * ( Im2 c))) - (( Im1 c) * ( Im3 c))) + (( Im3 c) * ( Im1 c))), ((((( Rea c) * ( - ( Im3 c))) + (( Im3 c) * ( Rea c))) - (( Im1 c) * ( Im2 c))) + (( Im2 c) * ( Im1 c)))*] by Th48

 .= [*( |.c.| ^2 ), 0 , 0 , 0 *] by A1, SQUARE_1:def 2;

 hence thesis by QUATERNI: 23;

 end;

 theorem :: QUATERN2:51

 |.(c1 .|. c2).| = ( |.c1.| * |.c2.|)

 proof



 thus |.(c1 .|. c2).| = ( |.c1.| * |.(c2 *' ).|) by QUATERNI: 87

 .= ( |.c1.| * |.c2.|) by QUATERNI: 73;

 end;

 theorem :: QUATERN2:52

 (c .|. c) = 0 implies c = 0

 proof

 assume (c .|. c) = 0 ;

 then

 A1: ( |.c.| ^2 ) = 0 by Th49;

 ((((( Rea c) ^2 ) + (( Im1 c) ^2 )) + (( Im2 c) ^2 )) + (( Im3 c) ^2 )) >= 0 by Lm2;

 then

 A2: ( |.c.| ^2 ) = ((((( Rea c) ^2 ) + (( Im1 c) ^2 )) + (( Im2 c) ^2 )) + (( Im3 c) ^2 )) by SQUARE_1:def 2;

 then

 A3: ( Rea c) = 0 by A1, Lm3;



 A4: ( Im1 c) = 0 by A1, A2, Lm3;



 A5: ( Im2 c) = 0 by A1, A2, Lm3;

 ( Im3 c) = 0 by A1, A2, Lm3;



 then c = [* 0 , 0 , 0 , 0 *] by A3, A4, A5, QUATERNI: 24

 .= [*( In ( 0 , REAL )), ( In ( 0 , REAL ))*] by QUATERNI: 91

 .= 0 by ARYTM_0:def 5;

 hence thesis;

 end;

 theorem :: QUATERN2:53

 ((c1 + c2) .|. c3) = ((c1 .|. c3) + (c2 .|. c3)) by Th18;

 theorem :: QUATERN2:54

 (c1 .|. (c2 + c3)) = ((c1 .|. c2) + (c1 .|. c3))

 proof



 thus (c1 .|. (c2 + c3)) = (c1 * ((c2 *' ) + (c3 *' ))) by QUATERNI: 54

 .= ((c1 .|. c2) + (c1 .|. c3)) by Th17;

 end;

 theorem :: QUATERN2:55

 (( - c1) .|. c2) = ( - (c1 .|. c2)) by Th20;

 theorem :: QUATERN2:56

 ( - (c1 .|. c2)) = (c1 .|. ( - c2))

 proof

 (c1 .|. ( - c2)) = (c1 * ( - (c2 *' ))) by QUATERNI: 55

 .= ( - (c1 * (c2 *' ))) by Th21;

 hence thesis;

 end;

 theorem :: QUATERN2:57

 (( - c1) .|. ( - c2)) = (c1 .|. c2)

 proof

 (( - c1) .|. ( - c2)) = (( - c1) * ( - (c2 *' ))) by QUATERNI: 55

 .= (c1 * (c2 *' )) by Th22;

 hence thesis;

 end;

 theorem :: QUATERN2:58

 ((c1 - c2) .|. c3) = ((c1 .|. c3) - (c2 .|. c3)) by Th23;

 theorem :: QUATERN2:59

 (c1 .|. (c2 - c3)) = ((c1 .|. c2) - (c1 .|. c3))

 proof

 (c1 .|. (c2 - c3)) = (c1 * ((c2 *' ) - (c3 *' ))) by QUATERNI: 56

 .= ((c1 * (c2 *' )) - (c1 * (c3 *' ))) by Th24;

 hence thesis;

 end;

 theorem :: QUATERN2:60

 ((c1 + c2) .|. (c1 + c2)) = ((((c1 .|. c1) + (c1 .|. c2)) + (c2 .|. c1)) + (c2 .|. c2))

 proof

 ((c1 + c2) .|. (c1 + c2)) = ((c1 + c2) * ((c1 *' ) + (c2 *' ))) by QUATERNI: 54

 .= (((c1 + c2) * (c1 *' )) + ((c1 + c2) * (c2 *' ))) by Th17

 .= (((c1 * (c1 *' )) + (c2 * (c1 *' ))) + ((c1 + c2) * (c2 *' ))) by Th18

 .= (((c1 .|. c1) + (c2 .|. c1)) + ((c1 .|. c2) + (c2 .|. c2))) by Th18

 .= ((((c1 .|. c1) + (c2 .|. c1)) + (c1 .|. c2)) + (c2 .|. c2)) by Th2;

 hence thesis by Th2;

 end;

 theorem :: QUATERN2:61

 ((c1 - c2) .|. (c1 - c2)) = ((((c1 .|. c1) - (c1 .|. c2)) - (c2 .|. c1)) + (c2 .|. c2))

 proof

 ((c1 - c2) .|. (c1 - c2)) = ((c1 - c2) * ((c1 *' ) - (c2 *' ))) by QUATERNI: 56

 .= (((c1 + ( - c2)) * (c1 *' )) + ((c1 + ( - c2)) * ( - (c2 *' )))) by Th17

 .= (((c1 * (c1 *' )) + (( - c2) * (c1 *' ))) + ((c1 + ( - c2)) * ( - (c2 *' )))) by Th18

 .= (((c1 .|. c1) + (( - c2) * (c1 *' ))) + ((c1 * ( - (c2 *' ))) + (( - c2) * ( - (c2 *' ))))) by Th18

 .= (((c1 .|. c1) + ( - (c2 * (c1 *' )))) + ((c1 * ( - (c2 *' ))) + (( - c2) * ( - (c2 *' ))))) by Th20

 .= (((c1 .|. c1) + ( - (c2 * (c1 *' )))) + (( - (c1 * (c2 *' ))) + (( - c2) * ( - (c2 *' ))))) by Th21

 .= (((c1 .|. c1) + ( - (c2 .|. c1))) + (( - (c1 .|. c2)) + (c2 .|. c2))) by Th22

 .= ((((c1 .|. c1) + ( - (c2 .|. c1))) + ( - (c1 .|. c2))) + (c2 .|. c2)) by Th2

 .= ((((c1 .|. c1) + ( - (c1 .|. c2))) + ( - (c2 .|. c1))) + (c2 .|. c2)) by Th2;

 hence thesis;

 end;