:: Inner Products, Group, Ring of Quaternion Numbers
::  by Fuguo Ge
::
:: Received March 18, 2008
:: Copyright (c) 2008 Association of Mizar Users

environ

 vocabularies ARYTM, RELAT_1, COMPLEX1, FUNCT_1, QUATERNI, ARYTM_1, ARYTM_3,
      XCMPLX_0, SQUARE_1, VECTSP_1, RLVECT_1, BINOP_1, LATTICES, GROUP_1,
      VECTSP_2, QUATERN2, PROB_2, ALGSTR_0;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, FUNCT_1, COMPLEX1,
      ARYTM_0, XCMPLX_0, XREAL_0, REAL_1, SQUARE_1, XXREAL_0, QUATERNI,
      BINOP_1, STRUCT_0, ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1, FUNCSDOM;
 constructors SQUARE_1, FUNCT_4, ARYTM_0, REAL_1, ORDINAL3, QUATERNI, COMPTRIG,
      SIN_COS, FUNCSDOM, GROUP_1, ALGSTR_0, VECTSP_1;
 registrations XREAL_0, SQUARE_1, XXREAL_0, RELAT_1, QUATERNI, VECTSP_1,
      STRUCT_0, REAL_1, INT_1, XBOOLE_0, NUMBERS, ALGSTR_0, RLVECT_1, BINOM;
 requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
 definitions SQUARE_1, COMPLEX1, XCMPLX_0, QUATERNI, RLVECT_1, ALGSTR_0,
      GROUP_1, VECTSP_1, BINOP_1, STRUCT_0;
 theorems ARYTM_0, SQUARE_1, XREAL_1, QUATERNI, STRUCT_0, RLVECT_1, XCMPLX_1;
 schemes BINOP_1, FUNCT_2, BINOP_2;

begin

QUA7: for g being quaternion number
  ex r,s,t,u being Element of REAL st g = [*r,s,t,u*]
  proof
    let g be quaternion number;
    g in QUATERNION by QUATERNI:def 2;
    hence thesis by QUATERNI:7;
  end;

Lm4: for a,b,c,d being real number holds a^2 + b^2 + c^2 + d^2 >= 0
proof
  let a,b,c,d be real number;
  a^2 >= 0 & b^2>= 0 & c^2 >= 0 & d^2 >= 0 by XREAL_1:65;then
  a^2 + b^2>= 0 & c^2 + d^2 >= 0;then
  (a^2 + b^2) + (c^2 + d^2) >= 0;
  hence thesis;
end;

Lm2:
  for a, b, c, d being real number st a^2 + b^2 + c^2 + d^2 = 0 holds a = 0
  & b = 0 & c = 0 & d = 0
proof
    let a, b, c, d be real number;
    assume
A1: a^2 + b^2 + c^2 + d^2 = 0;
A2: 0 <= a^2 & 0 <= b^2 & 0 <= c^2 & 0 <= d^2 by XREAL_1:65;
    assume
A3: a <> 0 or b <> 0 or c <> 0 or d <> 0;
    per cases by A3;
    suppose a <> 0;then
A4:   0 < a^2 + b^2 by A2,XREAL_1:36,SQUARE_1:74;
      0 <= c^2 +d^2 by A2;then
      0 < (a^2 + b^2) + (c^2 + d^2) by A4;
      hence contradiction by A1;
    end;
    suppose b <> 0;then
A5:   0 < a^2 + b^2 by A2,XREAL_1:36,SQUARE_1:74;
      0 <= c^2 +d^2 by A2;then
      0 < (a^2 + b^2) + (c^2 + d^2) by A5;
      hence contradiction by A1;
    end;
    suppose c <> 0;then
A6:   0 < c^2 + d^2 by A2,XREAL_1:36,SQUARE_1:74;
      0 <= a^2 +b^2 by A2;then
      0 < (a^2 + b^2) + (c^2 + d^2) by A6;
      hence contradiction by A1;
    end;
    suppose d <> 0;then
A7:   0 < c^2 + d^2 by A2,SQUARE_1:74,XREAL_1:36;
      0 <= a^2 +b^2 by A2;then
      0 < (a^2 + b^2) + (c^2 + d^2) by A7;
      hence contradiction by A1;
    end;
 end;

Lm5:
  for a, b, c, d being real number st a^2 + b^2 + c^2 + d^2 = 0 holds a = 0
  & b = 0 & c = 0 & d = 0
proof
    let a, b, c, d be real number;
    assume
A1: a^2 + b^2 + c^2 + d^2 = 0;
A2: 0 <= a^2 & 0 <= b^2 & 0 <= c^2 & 0 <= d^2 by XREAL_1:65;
    assume
A3: a <> 0 or b <> 0 or c <> 0 or d <> 0;
    per cases by A3;
    suppose a <> 0;then
A4:   0 < a^2 + b^2 by A2,XREAL_1:36,SQUARE_1:74;
      0 <= c^2 +d^2 by A2;then
      0 < (a^2 + b^2) + (c^2 + d^2) by A4;
      hence contradiction by A1;
    end;
    suppose b <> 0;then
A5:   0 < a^2 + b^2 by A2,XREAL_1:36,SQUARE_1:74;
      0 <= c^2 +d^2 by A2;then
      0 < (a^2 + b^2) + (c^2 + d^2) by A5;
      hence contradiction by A1;
    end;
    suppose c <> 0;then
A6:   0 < c^2 + d^2 by A2,XREAL_1:36,SQUARE_1:74;
      0 <= a^2 +b^2 by A2;then
      0 < (a^2 + b^2) + (c^2 + d^2) by A6;
      hence contradiction by A1;
    end;
    suppose d <> 0;then
A7:   0 < c^2 + d^2 by A2,XREAL_1:36,SQUARE_1:74;
      0 <= a^2 +b^2 by A2;then
      0 < (a^2 + b^2) + (c^2 + d^2) by A7;
      hence contradiction by A1;
    end;
 end;

reserve q,r,c,c1,c2,c3 for quaternion number;
reserve x1,x2,x3,x4,y1,y2,y3,y4 for Element of REAL;

definition
  redefine func 0q -> Element of QUATERNION;
  coherence by QUATERNI:def 2;
end;

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

theorem Th35:
  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;
A1: <i> = [*0,1,0,0*] by QUATERNI:def 6;
A2: y*<i> = [*y*0,y*1,y*0,y*0*] by A1,QUATERNI:def 21
         .= [*0,y,0,0*];
A3: z*<j> = [*z*0,z*0,z*1,y*0*] by QUATERNI:def 21
         .= [*0,0,z,0*];
A4: w*<k> = [*w*0,w*0,w*0,w*1*] by QUATERNI:def 21
         .= [*0,0,0,w*];
    x + y* <i> = [*x+0,y,0,0*] by A2,QUATERNI:def 19
              .= [*x,y,0,0*];then
    x + y*<i> + z*<j> = [*x+0,y+0,0+z,0+0*] by A3,QUATERNI:def 7
                     .= [*x,y,z,0*];then
    x + y*<i> + z*<j> + w*<k> = [*x+0,y+0,0+z,0+w*] by A4,QUATERNI:def 7;
    hence thesis;
end;

theorem Th5:
  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 QUA7;
      consider x2,y2,w2,z2 be Element of REAL such that
  A2: c2 = [*x2,y2,w2,z2*] by QUA7;
      consider x3,y3,w3,z3 be Element of REAL such that
  A3: c3 = [*x3,y3,w3,z3*] by QUA7;
  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 Th6:
  c + 0q = c
proof
  A1: 0q =[*0,0*] by ARYTM_0:def 7
        .=[*0,0,0,0*] by QUATERNI:def 6;
      consider x,y,w,z be Element of REAL such that
  A2: c = [*x,y,w,z*] by QUA7;
      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 Thc1:
  - [*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
  .=[*0,0*] by QUATERNI:def 6
  .=0 by ARYTM_0:def 7;
  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 Thc1
  .= [*x1-y1,x2-y2,x3-y3,x4-y4*] by QUATERNI:def 7;
  hence thesis;
end;

theorem
  c1 - c2 + c3 = c1 + c3 - c2 by Th5;

theorem Thz1:
  c1 = c1 + c2 - c2
  proof
    thus c1 + c2 - c2 = c1 + (c2 - c2) by Th5
    .= c1 + 0q by QUATERNI:def 8
    .= c1 by Th6;
  end;

theorem
  c1 = c1 - c2 + c2
  proof
    thus c1 - c2 + c2 = c1 + c2 - c2 by Th5
    .= c1 by Thz1;
  end;

theorem Th38:
  (-x1)*c = -(x1*c)
proof
   consider x,y,w,z be Element of REAL such that
  A1: c = [*x,y,w,z*] by QUA7;
  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
    .=[*0,0*] by QUATERNI:def 6
    .=0 by ARYTM_0:def 7;
    hence thesis by A2,A3,QUATERNI:def 8;
end;

definition let q;
  redefine func |.q.| -> Element of REAL;
  coherence;
end;

definition
  redefine func <i> -> Element of QUATERNION;
  coherence by QUATERNI:def 2;
end;

Lm3:
  r <> 0 implies |.r.| <> 0
proof
      assume
  A1: r <> 0;
      assume
  A2: |.r.| = 0;
      consider r0,r1,r2,r3 being Element of REAL such that
  A3: r = [*r0,r1,r2,r3*] by QUA7;
  A4: Rea r = r0 & Im1 r = r1 &
      Im2 r = r2 & Im3 r = r3 by A3,QUATERNI:23;
  A5: 0 <= (Rea r)^2 + (Im1 r)^2 + (Im2 r)^2 + (Im3 r)^2
         by QUATERNI:74;
      |.r.|^2 = r0^2 + r1^2 + r2^2 + r3^2 by A4,A5,SQUARE_1:def 4;then
      r0=0 & r1=0 & r2=0 & r3=0 by A2,Lm2;then
      r = [*0,0*] by A3,QUATERNI:def 6
       .= 0 by ARYTM_0:def 7;
      hence contradiction by A1;
end;

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

theorem Tw0:
 0q = [*0,0,0,0*]
proof
 thus 0q = [*0,0*] by ARYTM_0:def 7
       .= [*0,0,0,0*] by QUATERNI:def 6;
end;

theorem
 for r being quaternion number holds 0q*r = 0
proof let r be quaternion number;
  consider x1,x2,x3,x4,y1,y2,y3,y4 being Element of REAL such that
W1:  0 = [*x1,x2,x3,x4*] and
  r = [*y1,y2,y3,y4*] and
W3:  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;
  x1 = 0 & x2 = 0 & x3 = 0 & x4 = 0 by W1,Tw0,QUATERNI:12;
 hence thesis by W3,Tw0;
end;

theorem
 for r being quaternion number holds r*0q = 0
proof let r be quaternion number;
  consider x1,x2,x3,x4,y1,y2,y3,y4 being Element of REAL such that
  r = [*x1,x2,x3,x4*] and
W2:  0 = [*y1,y2,y3,y4*] and
W3:  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;
  y1 = 0 & y2 = 0 & y3 = 0 & y4 = 0 by W2,Tw0,QUATERNI:12;
 hence thesis by W3,Tw0;
end;

theorem Th1:
  c * 1q = c
proof
  A1: 1q =[*1,0*] by ARYTM_0:def 7
        .=[*1,0,0,0*] by QUATERNI:def 6;
      consider x,y,w,z be Element of REAL such that
  A2: c = [*x,y,w,z*] by QUA7;
      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*1+y*0-w*0 *] by A1,A2,QUATERNI:def 10
            .= [*x,y,w,z*];
  hence thesis by A2;
end;

theorem Th2:
  1q * c = c
proof
  A1: 1q =[*1,0*] by ARYTM_0:def 7
        .=[*1,0,0,0*] by QUATERNI:def 6;
      consider x,y,w,z be Element of REAL such that
  A2: c = [*x,y,w,z*] by QUA7;
      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*1+y*0-w*0 *] by A1,A2,QUATERNI:def 10
            .= [*x,y,w,z*];
   hence thesis by A2;
end;

theorem Th9:
  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 QUA7;
      consider x2,y2,w2,z2 be Element of REAL such that
  A2: c2 = [*x2,y2,w2,z2*] by QUA7;
      consider x3,y3,w3,z3 be Element of REAL such that
  A3: c3 = [*x3,y3,w3,z3*] by QUA7;
  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 Th10:
  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 QUA7;
      consider x2,y2,w2,z2 be Element of REAL such that
  A2: c2 = [*x2,y2,w2,z2*] by QUA7;
      consider x3,y3,w3,z3 be Element of REAL such that
  A3: c3 = [*x3,y3,w3,z3*] by QUA7;
  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 Th11:
  (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 QUA7;
      consider x2,y2,w2,z2 be Element of REAL such that
  A2: c2 = [*x2,y2,w2,z2*] by QUA7;
      consider x3,y3,w3,z3 be Element of REAL such that
  A3: c3 = [*x3,y3,w3,z3*] by QUA7;
  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 Th12:
  -c = (-1q) * c
proof
      consider x,y,w,z be Element of REAL such that
  A1: c = [*x,y,w,z*] by QUA7;
  A2:     c + [*-x,-y,-w,-z*]
        = [*x + -x,y + -y,w + -w,z + -z*] by A1,QUATERNI:def 7
       .= [*0,0*] by QUATERNI:def 6
       .= 0 by ARYTM_0:def 7;
   A3: 1q =[*1,0*] by ARYTM_0:def 7
         .=[*1,0,0,0*] by QUATERNI:def 6;
   A4:     1q + [*-1,0,0,0*]
          =[*1+ -1,0+0,0+0,0+0*] by A3,QUATERNI:def 7
         .=[*0,0*] by QUATERNI:def 6
         .=0 by ARYTM_0:def 7;
      (-1q)*c
           = [*-1,0,0,0*]*[*x,y,w,z*] by A1,A4,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,
                (-1)*z+0*x+0*w-0*y *] by QUATERNI:def 10;
      hence thesis by A2,QUATERNI:def 8;
end;

theorem Thd3:
  (-c1) * c2 = -(c1*c2)
proof
      consider x1,y1,w1,z1 be Element of REAL such that
  A1: c1 = [*x1,y1,w1,z1*] by QUA7;
      consider x2,y2,w2,z2 be Element of REAL such that
  A2: c2 = [*x2,y2,w2,z2*] by QUA7;
  A4:    (-c1)*c2
       = [*-x1,-y1,-w1,-z1*] * [*x2,y2,w2,z2*] by A2,A1,Thc1
      .= [* (-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 *];
  A5:    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;
         (-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 A4,A5,QUATERNI:def 7
      .=[* 0,0 *] by QUATERNI:def 6
      .=0 by ARYTM_0:def 7;
      hence thesis by QUATERNI:def 8;
end;

theorem Thd4a:
  c1 * (-c2) = -(c1*c2)
proof
      consider x1,y1,w1,z1 be Element of REAL such that
  A1: c1 = [*x1,y1,w1,z1*] by QUA7;
      consider x2,y2,w2,z2 be Element of REAL such that
  A2: c2 = [*x2,y2,w2,z2*] by QUA7;
  A4:   c1 * (-c2)
      =[*x1,y1,w1,z1*] * [*-x2,-y2,-w2,-z2*] by A1,A2,Thc1
     .=[* 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 *];
  A5:    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;
         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 A4,A5,QUATERNI:def 7
      .=[* 0,0 *] by QUATERNI:def 6
      .=0 by ARYTM_0:def 7;
      hence thesis by QUATERNI:def 8;
end;

theorem Thd5:
  (-c1) * (-c2) = c1*c2
proof
      consider x1,y1,w1,z1 be Element of REAL such that
  A1: c1 = [*x1,y1,w1,z1*] by QUA7;
      consider x2,y2,w2,z2 be Element of REAL such that
  A2: c2 = [*x2,y2,w2,z2*] by QUA7;
  A3: -c1 = [*-x1,-y1,-w1,-z1*] by A1,Thc1;
      (-c1) * (-c2)=[*-x1,-y1,-w1,-z1*] * [*-x2,-y2,-w2,-z2*] by A3,Thc1,A2
     .=[* (-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 Thd6:
  (c1 - c2) * c3 = c1 * c3 - c2 * c3
proof
  (c1 - c2) * c3=c1 * c3 + (-c2) * c3 by Th11;
  hence thesis by Thd3;
end;

theorem Thd7:
  c1 * (c2 - c3) = c1 * c2 - c1 * c3
proof
   c1 * (c2 - c3)=c1 * c2 + c1 * (-c3) by Th10;
   hence thesis by Thd4a;
end;

theorem Thd3a:
  [*x1,x2,x3,x4*] *' = [*x1,-x2,-x3,-x4*]
proof
  set c = [*x1,x2,x3,x4*];
  Rea c = x1 & Im1 c = x2 &
  Im2 c = x3 & Im3 c = x4 by QUATERNI:23;
  hence thesis by QUATERNI:43;
end;

theorem
  c*'*' =c
proof
  A1: Rea (c*') = Rea c & Im1 (c*') = -Im1 c &
      Im2 (c*') = -Im2 c & Im3 (c*') = -Im3 c by QUATERNI:44;
      c*'*'
       = [*Rea c, -(-Im1 c), -(-Im2 c), -(-Im3 c) *] by A1,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 QUA7;
    consider r0,r1,r2,r3 being Element of REAL such that
A2: r = [*r0,r1,r2,r3*] by QUA7;
 func q / r 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 q0',q1',q2',q3',r0',r1',r2',r3' being Element of REAL such that
A6: q = [*q0',q1',q2',q3'*] and
A7: r = [*r0',r1',r2',r3'*] and
A8: c2 = [* (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 *];
       q0 = q0' & q1 = q1' & q2 = q2' & q3 = q3' & r0 = r0' & r1 = r1' &
       r2 = r2' & r3 = r3' by A3,A4,A6,A7,QUATERNI:12;
   hence c1 = c2 by A5,A8;
  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 q/r in QUATERNION;
  end;
end;

definition let q,r;
  redefine func q / r -> Element of QUATERNION equals
(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>;
  coherence by QUATERNI:def 2;
  compatibility
  proof
       consider q0,q1,q2,q3 being Element of REAL such that
   A1: q = [*q0,q1,q2,q3*] by QUA7;
       consider r0,r1,r2,r3 being Element of REAL such that
   A2: r = [*r0,r1,r2,r3*] by QUA7;
   A3:Rea q = q0 & Im1 q = q1 &
      Im2 q = q2 & Im3 q = q3 by A1,QUATERNI:23;
   A4:Rea r = r0 & Im1 r = r1 &
      Im2 r = r2 & 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 Th35;
           hence thesis by A3,A4;
  end;
end;

definition let c;
  func c" -> quaternion number equals
   1q/c;
  coherence;
end;

definition let r;
  redefine func r" -> Element of QUATERNION equals
  Rea r / (|.r.|^2) - Im1 r / (|.r.|^2)*<i> -
  Im2 r / (|.r.|^2)*<j> - (Im3 r) / (|.r.|^2)*<k>;
  coherence;
  compatibility
  proof
   A2: 1q =[*1,0*] by ARYTM_0:def 7
         .=[*1,0,0,0*] by QUATERNI:def 6;
    consider q0,q1,q2,q3,r0,r1,r2,r3 being Element of REAL such that
W1:  1q = [*q0,q1,q2,q3*] and
W2: r = [*r0,r1,r2,r3*] and
W3:    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:Rea r = r0 & Im1 r = r1 &
      Im2 r = r2 & Im3 r = r3 by W2,QUATERNI:23;
X:  q0 = 1 & q1 = 0 & q2 = 0 & q3 = 0 by A2,W1,QUATERNI:12;
      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*1)/(|.r.|^2) *] by W3,X
         .=r0/(|.r.|^2) + (-r1/(|.r.|^2))*<i> +
           (-r2/(|.r.|^2))*<j> + (-r3/(|.r.|^2))*<k> by Th35
         .=r0/|.r.|^2 + -((r1/|.r.|^2)*<i>) +
           (-(r2/|.r.|^2))*<j> + (-(r3/|.r.|^2))*<k> by Th38
         .=r0/|.r.|^2 - r1/|.r.|^2*<i> +
           -(r2/|.r.|^2*<j>) + (-(r3/|.r.|^2))*<k> by Th38
         .=r0/|.r.|^2 - r1/|.r.|^2*<i> -
           r2/|.r.|^2*<j> + -(r3/|.r.|^2*<k>) by Th38;
   hence thesis by A4;
  end;
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
W1: 1q = [*q0,q1,q2,q3*] and
W2: r = [*r0,r1,r2,r3*] and
W3: 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;
   A2: 1q=[*1,0*] by ARYTM_0:def 7
         .=[*1,0,0,0*] by QUATERNI:def 6;
X:  q0 = 1 & q1 = 0 & q2 = 0 & q3 = 0 by A2,W1,QUATERNI:12;
   A4:Rea r = r0 & Im1 r = r1 &
      Im2 r = r2 & Im3 r = r3 by W2,QUATERNI:23;
      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*1)/(|.r.|^2) *] by W3,X
         .=[*r0/(|.r.|^2), -r1/(|.r.|^2),
             -r2/(|.r.|^2), -r3/(|.r.|^2) *];
    hence thesis by QUATERNI:23,A4;
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 QUA7;
       consider r0,r1,r2,r3 being Element of REAL such that
   A2: r = [*r0,r1,r2,r3*] by QUA7;
   A3:Rea q = q0 & Im1 q = q1 &
      Im2 q = q2 & Im3 q = q3 by A1,QUATERNI:23;
   A4:Rea r = r0 & Im1 r = r1 &
      Im2 r = r2 & 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,QUATERNI:23;
end;

theorem Thaa:
  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 QUA7;
   A3: 1q =[*1,0*] by ARYTM_0:def 7
         .=[*1,0,0,0*] by QUATERNI:def 6;
   A4: Rea r = r0 & Im1 r = r1 &
       Im2 r = r2 & Im3 r = r3 by A2,QUATERNI:23;
   A5: 0 <= (Rea r)^2 + (Im1 r)^2 + (Im2 r)^2 + (Im3 r)^2
         by QUATERNI:74;
   A6:   |.r.|^2
       = r0^2 + r1^2 + r2^2 + r3^2 by A4,A5,SQUARE_1:def 4;
   A7:     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*1)/(|.r.|^2) *] by A2,A3,Def1
         .=[* (r0)/(|.r.|^2),(-r1)/(|.r.|^2),
              (-r2)/(|.r.|^2),(-r3)/(|.r.|^2) *];
       |.r.| <> 0 by A1,Th40;then
   A8: |.r.|^2 > 0 by SQUARE_1:74;
       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,A7,QUATERNI:def 10
  .=[*|.r.|^2/|.r.|^2,0,0,0 *] by A6
  .=[*1,0,0,0 *] by A8,XCMPLX_1:60
  .=[*1,0*] by QUATERNI:def 6
  .=1 by ARYTM_0:def 7;
  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 QUA7;
   A3: 1q =[*1,0*] by ARYTM_0:def 7
         .=[*1,0,0,0*] by QUATERNI:def 6;
   A4: Rea r = r0 & Im1 r = r1 &
       Im2 r = r2 & Im3 r = r3 by A2,QUATERNI:23;
   A5: 0 <= (Rea r)^2 + (Im1 r)^2 + (Im2 r)^2 + (Im3 r)^2
         by QUATERNI:74;
   A6:   |.r.|^2
       = r0^2 + r1^2 + r2^2 + r3^2 by A4,A5,SQUARE_1:def 4;
   A7:     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*1)/(|.r.|^2) *] by A2,A3,Def1
         .=[* (r0)/(|.r.|^2),(-r1)/(|.r.|^2),
              (-r2)/(|.r.|^2),(-r3)/(|.r.|^2) *];
       |.r.| <> 0 by A1,Th40;then
   A8: |.r.|^2 > 0 by SQUARE_1:74;
        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,A7,QUATERNI:def 10
  .=[*|.r.|^2/|.r.|^2,0,0,0 *] by A6
  .=[*1,0,0,0 *] by A8,XCMPLX_1:60
  .=[*1,0*] by QUATERNI:def 6
  .=1 by ARYTM_0:def 7;
  hence thesis;
end;

theorem Thd1:
  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 QUA7;
      |.c.| > 0 by A1,Th40;then
  A3: |.c.|^2 > 0 by SQUARE_1:74;
  A4: Rea c = x1 & Im1 c = x2 &
      Im2 c = x3 & Im3 c = x4 by A2,QUATERNI:23;
  A5: x1^2+x2^2+x3^2+x4^2 >= 0 by Lm4;
      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,SQUARE_1:def 4
         .=[* 1,0,0,0 *] by A3,XCMPLX_1:60
         .=[* 1,0 *] by QUATERNI:def 6
         .=1 by ARYTM_0:def 7;
  hence thesis;
end;

theorem
  (-c)" = -(c")
proof
A1: 1q =[*1,0*] by ARYTM_0:def 7
    .=[*1,0,0,0*] by QUATERNI:def 6;
    consider x1,x2,x3,x4 be Element of REAL such that
A2: c = [*x1,x2,x3,x4*] by QUA7;
A3: -c = [*-x1,-x2,-x3,-x4*] by A2,Thc1;
A4: |.-c.| = |.c.| by QUATERNI:72;
A6: 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*1)/(|.c.|^2) *] by A1,A2,Def1
      .= [*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)*1)/(|.(-c).|^2) *] by A1,A3,Def1
      .= [*-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 A6,QUATERNI:def 7
     .= [*0,0 *] by QUATERNI:def 6
     .=0 by ARYTM_0:def 7;
     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
  :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 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
  :Def8: 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 :Def13:
  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 Def13;
end;

registration
  cluster -> quaternion 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 Def13;
    hence thesis;
  end;
end;

registration
  let x,y be Element of G_Quaternion;
  let a,b be quaternion number;
  identify x+y with a+b when x=a, y=b;
  compatibility
  proof
    assume
  Z:x=a & y=b;
    reconsider a'=a, b'=b as Element of QUATERNION by QUATERNI:def 2;
    thus x+y = addquaternion.(a',b') by Z,Def13
       .= a+b by Def6;
  end;
end;

theorem Th90:
  0.G_Quaternion = 0q by Def13;

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 Th5;
   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 Def13;
    thus x + 0.G_Quaternion = (the addF of G_Quaternion).(x1,0q) by Def13
       .= addquaternion.(x1,0q) by Def13
       .= x1 + 0q by Def6
       .= x by Th6;
   end;
  thus G_Quaternion is right_complementable
  proof
    let x be Element of G_Quaternion;
    reconsider x1=x as Element of QUATERNION by Def13;
    reconsider y=-x1 as Element of G_Quaternion by Def13;
    take y;
    thus thesis by Th90,QUATERNI:def 8;
  end;
 end;
end;

registration let x be Element of G_Quaternion, a be quaternion number;
 identify -x with -a when x = a;
 compatibility
  proof
    assume A1: x = a;
    reconsider x1= x as Element of QUATERNION by Def13;
    reconsider b =-x1 as Element of G_Quaternion by Def13;
    b + x = 0.G_Quaternion by Th90,QUATERNI:def 8;
    hence thesis by A1,RLVECT_1:19;
  end;
end;

registration
  let x,y be Element of G_Quaternion;
  let a,b be quaternion number;
  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 6,RLVECT_1:def 7;

definition
 func R_Quaternion -> strict doubleLoopStr means :Def11:
  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 Def11;
end;

registration
  cluster -> quaternion 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 Def11;
    hence thesis;
  end;
end;

registration let a,b be quaternion number;
 let x,y be Element of R_Quaternion;
 identify x+y with a+b when x=a, y=b;
 compatibility
  proof assume
Z: x=a & y=b;
    reconsider a'=a, b'=b as Element of QUATERNION by QUATERNI:def 2;
    thus x+y = addquaternion.(a',b') by Z,Def11
       .= a+b by Def6;
  end;
 identify x*y with a*b when x=a, y=b;
 compatibility
  proof assume
Z: x=a & y=b;
    reconsider a'=a, b'=b as Element of QUATERNION by QUATERNI:def 2;
    thus x*y = multquaternion.(a',b') by Z,Def11
       .= a*b by Def8;
  end;
end;

registration
 cluster R_Quaternion -> well-unital;
 coherence
 proof
   let x be Element of R_Quaternion;
   1.R_Quaternion = 1q by Def11;
   hence thesis by Th1,Th2;
 end;
end;

theorem
  1.R_Quaternion = 1q by Def11;

theorem
  1_R_Quaternion = 1q by Def11;

theorem Th7:
  0.R_Quaternion = 0q by Def11;

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
    proof
    let x,y,z be Element of R_Quaternion;
    reconsider x1=x, y1=y, z1=z as Element of QUATERNION by Def11;
    thus (x + y) + z = addquaternion.[(the addF of R_Quaternion).[x1,y1],z1]
          by Def11
       .= addquaternion.(addquaternion.(x1,y1),z1) by Def11
       .= addquaternion.(x1 + y1,z1) by Def6
       .=(x1 + y1) + z1 by Def6
       .= x1 + (y1 + z1) by Th5
       .= addquaternion.(x1,y1 + z1) by Def6
       .= addquaternion.[x1,addquaternion.(y1,z1)] by Def6
       .= addquaternion.[x1,(the addF of R_Quaternion).[y1,z1]] by Def11
       .= x + (y + z) by Def11;
   end;
   thus R_Quaternion is right_zeroed
   proof
    let x be Element of R_Quaternion;
    reconsider x1=x as Element of QUATERNION by Def11;
    thus x + 0.R_Quaternion = (the addF of R_Quaternion).(x1,0q) by Def11
       .= addquaternion.(x1,0q) by Def11
       .= x1 + 0q by Def6
       .= x by Th6;
  end;
  thus R_Quaternion is right_complementable
  proof
    let x be Element of R_Quaternion;
    reconsider x1=x as Element of QUATERNION by Def11;
    reconsider y=-x1 as Element of R_Quaternion by Def11;
    take y;
    thus thesis by Th7,QUATERNI:def 8;
 end;
 thus R_Quaternion is Abelian
 proof
    let x,y be Element of R_Quaternion;
    reconsider x1=x ,y1=y as Element of QUATERNION by Def11;
    thus thesis;
 end;
 thus R_Quaternion is associative
 proof
    let x,y,z be Element of R_Quaternion;
    reconsider x1=x, y1=y, z1=z as Element of QUATERNION by Def11;
    thus (x * y) * z =
          multquaternion.((the multF of R_Quaternion).(x1,y1),z1) by Def11
       .= multquaternion.(multquaternion.(x1,y1),z1) by Def11
       .= multquaternion.(x1 * y1,z1) by Def8
       .= (x1 * y1) * z1 by Def8
       .= x1 * (y1 * z1) by Th9
       .= multquaternion.(x1,y1 * z1) by Def8
       .= multquaternion.(x1,multquaternion.(y1,z1)) by Def8
       .= multquaternion.(x1,(the multF of R_Quaternion).(y1,z1)) by Def11
       .= x * (y * z) by Def11;
 end;
 thus R_Quaternion is left_unital right_unital;
 thus R_Quaternion is distributive
 proof
   let x,y,z be Element of R_Quaternion;
   reconsider x1=x, y1=y, z1=z as Element of QUATERNION by Def11;
   thus x*(y+z)= multquaternion.(x1,(the addF of R_Quaternion).(y1,z1))
     by Def11
      .= multquaternion.(x1,addquaternion.(y1,z1)) by Def11
      .= multquaternion.(x1,y1 + z1) by Def6
      .= x1 * (y1 + z1) by Def8
      .= x1 * y1 + x1 * z1 by Th10
      .= addquaternion.(x1 * y1,x1 * z1) by Def6
      .= addquaternion.(multquaternion.(x1,y1),x1 * z1) by Def8
      .= addquaternion.(multquaternion.(x1,y1),multquaternion.(x1,z1))
                                                        by Def8
      .= (the addF of R_Quaternion).
         (multquaternion.(x1,y1),multquaternion.(x1,z1)) by Def11
      .= (the addF of R_Quaternion).((the multF of R_Quaternion).(x1,y1),
                                            multquaternion.(x1,z1)) by Def11
      .= x*y+x*z by Def11;
    thus (y+z)*x = multquaternion.((the addF of R_Quaternion).(y1,z1),x1)
              by Def11
         .= multquaternion.(addquaternion.(y1,z1),x1) by Def11
         .= multquaternion.(y1 + z1,x1) by Def6
         .= (y1 + z1) * x1 by Def8
         .= y1 * x1 + z1 * x1 by Th11
         .= addquaternion.(y1 * x1,z1 * x1) by Def6
         .= addquaternion.(multquaternion.(y1,x1),z1 * x1) by Def8
         .= addquaternion.(multquaternion.(y1,x1),multquaternion.(z1,x1))
                                                           by Def8
         .= (the addF of R_Quaternion).
            (multquaternion.(y1,x1),multquaternion.(z1,x1)) by Def11
         .= (the addF of R_Quaternion).((the multF of R_Quaternion).(y1,x1),
                                               multquaternion.(z1,x1)) by Def11
         .= y * x + z * x by Def11;
     end;
  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 Def11;
      reconsider y=x1" as Element of R_Quaternion by Def11;
      take y;
      A2:x1<>0q by A1,Def11;
      x * y =1 by A2,Thaa
         .=1.R_Quaternion by Def11;
      hence thesis;
     end;
   thus R_Quaternion is non degenerated
   proof
   A: 1.R_Quaternion = 1q by Def11;
     0.R_Quaternion <> 1.R_Quaternion by A,Def11;
      hence thesis by STRUCT_0:def 8;
 end;
 end;
end;

registration let x be Element of R_Quaternion, a be quaternion number;
 identify -x with -a when x = a;
 compatibility
  proof
    assume A1: x = a;
    reconsider x1= x as Element of QUATERNION by Def11;
    reconsider b =-x1 as Element of R_Quaternion by Def11;
    b + x = 0.R_Quaternion by Th7,QUATERNI:def 8;
    hence thesis by A1,RLVECT_1:19;
  end;
end;

registration
  let x,y be Element of R_Quaternion;
  let a,b be quaternion number;
  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;
   coherence by Def11;
end;

reserve z,z1,z2,z3,z4 for Element of R_Quaternion;

theorem
  -z = (-1_R_Quaternion) * z
    proof
     reconsider z'=z as Element of QUATERNION by Def11;
     thus -z = (-1q) * z' by Th12
            .= (-1_R_Quaternion) * z by Def11;
    end;

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

theorem
  (1.R_Quaternion)*' = 1.R_Quaternion
    proof
     1.R_Quaternion = 1r by Def11;
     hence thesis by QUATERNI:47;
    end;

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

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

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

theorem
  (1.R_Quaternion)" = 1.R_Quaternion
proof
    1q"= 1q by Thd1
      .= 1.R_Quaternion by Def11;
    hence thesis by Def11;
end;

definition :: Inner product of quternion numbers
  let x, y be quaternion number;
  func x .|. y -> Element of QUATERNION equals
  x*(y*');
  coherence by QUATERNI:def 2;
end;

theorem Thd4:
  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 QUA7;
    consider x2,y2,w2,z2 be Element of REAL such that
A2: c2 = [*x2,y2,w2,z2*] by QUA7;
A4: Rea c1 = x1 & Im1 c1 = y1 &
    Im2 c1 = w1 & Im3 c1 = z1 by A1,QUATERNI:23;
A5: Rea c2 = x2 & Im1 c2 = y2 &
    Im2 c2 = w2 & Im3 c2 = z2 by A2,QUATERNI:23;
    c1 .|. c2 = [*x1,y1,w1,z1*] * [*x2,-y2,-w2,-z2*] by A1,A2,Thd3a
    .= [* 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 A4,A5;
   hence thesis;
end;

theorem Thd5a:
  c .|. c = |.c.|^2
proof
A2: (Rea c)^2+(Im1 c)^2+(Im2 c)^2+(Im3 c)^2 >= 0 by Lm4;
    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 Thd4
 .=[*(Rea c)^2+(Im1 c)^2+(Im2 c)^2+(Im3 c)^2,0*] by QUATERNI:def 6
 .= (Rea c)^2+(Im1 c)^2+(Im2 c)^2+(Im3 c)^2 by ARYTM_0:def 7
 .= |.c.|^2 by A2,SQUARE_1:def 4;
  hence thesis;
end;

theorem
  Rea (c .|. c) = |.c.|^2 & Im1 (c .|. c) = 0 &
  Im2 (c .|. c) = 0 & Im2 (c .|. c) = 0
proof
A2: (Rea c)^2+(Im1 c)^2+(Im2 c)^2+(Im3 c)^2 >= 0 by Lm4;
    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 Thd4
.=[*|.c.|^2,0,0,0*] by A2,SQUARE_1:def 4;
  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
A1a: |.c.|^2 = 0 by Thd5a;
A2:  (Rea c)^2+(Im1 c)^2+(Im2 c)^2+(Im3 c)^2 >= 0 by Lm4;
A3:  |.c.|^2 = (Rea c)^2+(Im1 c)^2+(Im2 c)^2+(Im3 c)^2
     by A2,SQUARE_1:def 4;
 Rea c = 0 & Im1 c = 0 & Im2 c = 0 & Im3 c = 0 by A1a,A3,Lm5;
 then c = [*0,0,0,0*] by QUATERNI:24
   .= [*0,0*] by QUATERNI:def 6
   .= 0 by ARYTM_0:def 7;
  hence thesis;
end;

theorem
  (c1+c2).|.c3 = c1.|.c3 + c2.|.c3 by Th11;

theorem
  c1.|.(c2+c3) = c1.|.c2 + c1.|.c3
proof
  thus c1.|.(c2+c3)
     = c1 * (c2*' + c3*') by QUATERNI:54
    .= c1.|.c2 + c1.|.c3 by Th10;
end;

theorem
  (-c1).|.c2 = - c1.|.c2 by Thd3;

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

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

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

theorem
  c1.|.(c2 - c3) = c1.|.c2 - c1.|.c3
proof
  c1.|.(c2 - c3)=c1 * (c2*' - c3*') by QUATERNI:56
   .=c1 * c2*' - c1 * c3*' by Thd7;
  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 Th10
    .=c1 * c1*' + c2 * c1*' + (c1 + c2) * c2*' by Th11
    .=c1.|.c1 + c2.|.c1 + (c1.|.c2 + c2.|.c2) by Th11
    .=c1.|.c1 + c2.|.c1 + c1.|.c2 + c2.|.c2 by Th5;
   hence thesis by Th5;
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 Th10
   .=c1* c1*' + (-c2) * c1*' + (c1 + -c2) * -c2*' by Th11
   .=c1.|.c1 + (-c2) * c1*' + (c1* (-c2*') + (-c2) * (-c2*')) by Th11
   .=c1.|.c1 + -(c2 * c1*') + (c1* (-c2*') + (-c2) * (-c2*')) by Thd3
   .=c1.|.c1 + -(c2 * c1*') + (-(c1* c2*') + (-c2) * (-c2*')) by Thd4a
   .=c1.|.c1 + -c2.|.c1 + (-c1.|.c2 + c2.|.c2) by Thd5
   .=c1.|.c1 + -c2.|.c1 + -c1.|.c2 + c2.|.c2 by Th5
   .=c1.|.c1 + -c1.|.c2 + -c2.|.c1  + c2.|.c2 by Th5;
   hence thesis;
end;