QUATERN2

:: Inner Products, Group, Ring of Quaternion Numbers
::  by Fuguo Ge
::
:: Received March 18, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, QUATERNI, ORDINAL1, SUBSET_1, ARYTM_0, SQUARE_1,
      ARYTM_3, XXREAL_0, CARD_1, REAL_1, RELAT_1, XCMPLX_0, ARYTM_1, COMPLEX1,
      BINOP_1, FUNCT_1, STRUCT_0, ALGSTR_0, SUPINF_2, XBOOLE_0, RLVECT_1,
      MESFUNC1, VECTSP_1, GROUP_1, LATTICES, PROB_2, QUATERN2, FUNCT_7;
 notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, FUNCT_1, XCMPLX_0, COMPLEX1,
      ARYTM_0, XREAL_0, REAL_1, SQUARE_1, XXREAL_0, QUATERNI, BINOP_1,
      STRUCT_0, ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1;
 constructors SQUARE_1, FUNCT_4, ARYTM_0, REAL_1, QUATERNI, FUNCSDOM, VECTSP_1,
      COMPLEX1, XXREAL_0, XREAL_0, NUMBERS, GROUP_1;
 registrations XREAL_0, SQUARE_1, XXREAL_0, RELAT_1, QUATERNI, VECTSP_1,
      STRUCT_0, ORDINAL1;
 requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
 definitions RLVECT_1, ALGSTR_0, VECTSP_1;
 equalities SQUARE_1, COMPLEX1, XCMPLX_0, QUATERNI, ALGSTR_0, STRUCT_0;
 expansions RLVECT_1, GROUP_1, VECTSP_1, STRUCT_0;
 theorems ARYTM_0, SQUARE_1, QUATERNI, RLVECT_1, XCMPLX_1, XREAL_0;
 schemes BINOP_1, FUNCT_2, BINOP_2;

begin

Lm1: for g being Quaternion
ex r,s,t,u being Element of REAL st g = [*r,s,t,u*]
 proof let g be Quaternion;
  consider r,s,t,u being 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 being Real holds a^2 + b^2 + c^2 + d^2 >= 0
  by QUATERNI:74;

Lm3: for a, b, c, d being 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
  redefine func 0q -> Element of QUATERNION;  :: redefines 0q (QUATERNI, definition)
  coherence by QUATERNI:def 2;
end;

definition
  redefine func 1q -> Element of QUATERNION;  :: redefines 1q (QUATERNI, definition)
  coherence by QUATERNI:def 2;
end;

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

theorem Th1:
  for x,y,z,w being Real holds [*x,y,z,w*] = x + y*<i> + 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;
  <i> = [*In(0,REAL),jj*] by ARYTM_0:def 5;
  then <i> = [*0,jj,0,0*] by QUATERNI:91;
  then
A1: y*<i> = [*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* <i> = [*x0,y0,0,0*] by A1,QUATERNI:def 19
    .= [*x,y,0,0*];
  then x + y*<i> + z*<j> = [*x0,y0,0+z,0+0*] by A2,QUATERNI:def 7
    .= [*x,y,z,0*];
  then x + y*<i> + z*<j> + w*<k> = [*x0,y0,0+z,0+w*] by A3,QUATERNI:def 7;
  hence thesis;
end;

theorem 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 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 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
  [*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
  c1 - c2 + c3 = c1 + c3 - c2 by Th2;

theorem 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
  c1 = c1 - c2 + c2
proof
  thus c1 - c2 + c2 = c1 + c2 - c2 by Th2
    .= c1 by Th7;
end;

theorem 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
  redefine func <i> -> Element of QUATERNION;  :: redefines <i> (XCMPLX_0, definition)
  coherence by QUATERNI:def 2;
end;

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

theorem Th10:
  r <> 0 implies |.r.| > 0
proof
  assume r <> 0;
  then |.r.| <> 0 by Lm4;
  hence thesis by QUATERNI:67;
end;

theorem 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
  for r being Quaternion holds 0q*r = 0
proof
  let r be Quaternion;
  consider x1,x2,x3,x4,y1,y2,y3,y4 being 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
  for r being Quaternion holds r*0q = 0
proof
  let r be Quaternion;
  consider x1,x2,x3,x4,y1,y2,y3,y4 being 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 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 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 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 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 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 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 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 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 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 Th23:
  (c1 - c2) * c3 = c1 * c3 - c2 * c3
proof
  (c1 - c2) * c3=c1 * c3 + (-c2) * c3 by Th18;
  hence thesis by Th20;
end;

theorem Th24:
  c1 * (c2 - c3) = c1 * c2 - c1 * c3
proof
  c1 * (c2 - c3)=c1 * c2 + c1 * (-c3) by Th17;
  hence thesis by Th21;
end;

theorem 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
  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 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 -> Number means
  :Def1:
  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
  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 being 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 being 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 being 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;
  redefine func q/r -> Element of QUATERNION;  :: redefines / (QUATERN2, definition)
  coherence by QUATERNI:def 2;
end;

theorem
  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)*<i>+
(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 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;
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)*<i>+
  (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;
  func c" -> Quaternion equals
  1q / c;
  coherence;
end;

definition let r;
  redefine func r" -> Element of QUATERNION;  :: redefines " (QUATERN2, definition)
  coherence;
end;

theorem
  r" = Rea r / (|.r.|^2) - Im1 r / (|.r.|^2)*<i> -
  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 being 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))*<i> +
  (-r2/(|.r.|^2))*<j> + (-r3/(|.r.|^2))*<k> by Th1,A4,A8,A9,A10
    .=r0/|.r.|^2 + -((r1/|.r.|^2)*<i>) +
  (-(r2/|.r.|^2))*<j> + (-(r3/|.r.|^2))*<k> by Th9
    .=r0/|.r.|^2 - r1/|.r.|^2*<i> +
  -(r2/|.r.|^2*<j>) + (-(r3/|.r.|^2))*<k> by Th9
    .=r0/|.r.|^2 - r1/|.r.|^2*<i> -
  r2/|.r.|^2*<j> + -(r3/|.r.|^2*<k>) by Th9;
  hence thesis by A3,A5,A6,A7,QUATERNI:23;
end;

theorem
  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 being 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
  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 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;
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 Th31:
  r <> 0 implies r * r" = 1
proof
  assume
A1: r <> 0;
  consider r0,r1,r2,r3 being 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
  r <> 0 implies r" * r = 1
proof
  assume
A1: r <> 0;
  consider r0,r1,r2,r3 being 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 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
  (-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
  func compquaternion -> UnOp of QUATERNION means
  for c being Element of QUATERNION holds it.c = -c;
  existence from FUNCT_2:sch 4;
  uniqueness from BINOP_2:sch 1;
  func addquaternion -> BinOp of QUATERNION means
  :Def4:
  for c1,c2 being Element of QUATERNION holds it.(c1,c2) = c1 + c2;
  existence from BINOP_1:sch 4;
  uniqueness from BINOP_2:sch 2;
  func diffquaternion -> BinOp of QUATERNION means
  for c1,c2 being Element of QUATERNION holds it.(c1,c2) = c1 - c2;
  existence from BINOP_1:sch 4;
  uniqueness from BINOP_2:sch 2;
  func multquaternion -> BinOp of QUATERNION means
  :Def6:
  for c1,c2 being Element of QUATERNION holds it.(c1,c2) = c1 * c2;
  existence from BINOP_1:sch 4;
  uniqueness from BINOP_2:sch 2;
  func divquaternion -> BinOp of QUATERNION means
  for c1,c2 being Element of QUATERNION holds it.(c1,c2) = c1 / c2;
  existence from BINOP_1:sch 4;
  uniqueness from BINOP_2:sch 2;
  func invquaternion -> UnOp of QUATERNION means
  for c being Element of QUATERNION holds it.c = c";
  existence from FUNCT_2:sch 4;
  uniqueness from BINOP_2:sch 1;
end;

definition
  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 x+y with a+b 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 Th35:
  0.G_Quaternion = 0q by Def9;

registration
  cluster G_Quaternion -> Abelian add-associative right_zeroed
    right_complementable;
  coherence
  proof
    thus for x,y being Element of G_Quaternion holds x+y = y+x;
    thus
    for x,y,z being Element of G_Quaternion holds (x+y)+z = x+(y+z) by Th2;
    thus for x being 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 -x with -a 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 x-y with a-b when x=a, y=b;
  compatibility;
end;

theorem
  for x,y,z being 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,def 4;

definition
  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 x+y with a+b 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 x*y with a*b 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
  1.R_Quaternion = 1q by Def10;

theorem
  1_R_Quaternion = 1q by Def10;

theorem 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 -x with -a 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 x-y with a-b when x=a, y=b;
  compatibility;
end;

definition
  let z be Element of R_Quaternion;
  redefine func z *' -> Element of R_Quaternion;  :: redefines *' (QUATERNI, definition)
  coherence by Def10;
end;

reserve z for Element of R_Quaternion;

theorem
  -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
  (0.R_Quaternion)*' = 0.R_Quaternion
proof
  0.R_Quaternion = 0q by Def10;
  hence thesis by QUATERNI:45;
end;

theorem
  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
  (1.R_Quaternion)*' = 1.R_Quaternion
proof
  1.R_Quaternion = 1r by Def10;
  hence thesis by QUATERNI:47;
end;

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

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

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

theorem
  (1.R_Quaternion)" = 1.R_Quaternion
proof
  1q"= 1q by Th33
    .= 1.R_Quaternion by Def10;
  hence thesis by Def10;
end;

definition :: Inner product of quternion numbers
  let x, y be Quaternion;
  func x .|. y -> Element of QUATERNION equals
  x*(y*');
  coherence;
end;

theorem 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 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
  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
  |. c1.|.c2 .| = |.c1.|*|.c2.|
proof
  thus |.(c1.|.c2).| =(|.c1.|)*(|.c2*'.|) by QUATERNI:87
    .=|.c1.|*|.c2.| by QUATERNI:73;
end;

theorem
  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
  (c1+c2).|.c3 = c1.|.c3 + c2.|.c3 by Th18;

theorem
  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
  (-c1).|.c2 = - c1.|.c2 by Th20;

theorem
  - c1.|.c2 = c1.|.(-c2)
proof
  c1.|.(-c2)=c1 * -(c2*') by QUATERNI:55
    .=-(c1 * c2*') by Th21;
  hence thesis;
end;

theorem
  (-c1).|.(-c2) = c1.|.c2
proof
  (-c1).|.(-c2)=(-c1) * -(c2*') by QUATERNI:55
    .=c1 * c2*' by Th22;
  hence thesis;
end;

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

theorem
  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
  (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
  (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;