:: 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 by XREAL_1:35;then
(a^2 + b^2) + (c^2 + d^2) >= 0 by XREAL_1:35;
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,XREAL_1:35;then
0 < (a^2 + b^2) + (c^2 + d^2) by A4,XREAL_1:36;
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,XREAL_1:35;then
0 < (a^2 + b^2) + (c^2 + d^2) by A5,XREAL_1:36;
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,XREAL_1:35;then
0 < (a^2 + b^2) + (c^2 + d^2) by A6,XREAL_1:36;
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,XREAL_1:35;then
0 < (a^2 + b^2) + (c^2 + d^2) by A7,XREAL_1:36;
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,XREAL_1:35;then
0 < (a^2 + b^2) + (c^2 + d^2) by A4,XREAL_1:36;
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,XREAL_1:35;then
0 < (a^2 + b^2) + (c^2 + d^2) by A5,XREAL_1:36;
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,XREAL_1:35;then
0 < (a^2 + b^2) + (c^2 + d^2) by A6,XREAL_1:36;
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,XREAL_1:35;then
0 < (a^2 + b^2) + (c^2 + d^2) by A7,XREAL_1:36;
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** + z* + w*
proof
let x,y,z,w be Real;
A1: ** = [*0,1,0,0*] by QUATERNI:def 6;
A2: y*** = [*y*0,y*1,y*0,y*0*] by A1,QUATERNI:def 21
.= [*0,y,0,0*];
A3: z* = [*z*0,z*0,z*1,y*0*] by QUATERNI:def 21
.= [*0,0,z,0*];
A4: w* = [*w*0,w*0,w*0,w*1*] by QUATERNI:def 21
.= [*0,0,0,w*];
x + y* ** = [*x+0,y,0,0*] by A2,QUATERNI:def 19
.= [*x,y,0,0*];then
x + y*** + z* = [*x+0,y+0,0+z,0+0*] by A3,QUATERNI:def 7
.= [*x,y,z,0*];then
x + y*** + z* + w* = [*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 ** -> 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
q = 0 implies q * c = 0
proof
assume A1: q = 0;
A2: 0 = [*0,0*] by ARYTM_0:def 7
.= [*0,0,0,0*] by QUATERNI:def 6;
consider r,s,t,u being Element of REAL such that
A7: c = [*r,s,t,u*] by QUA7;
thus q*c = [* 0*r-0*s-0*t-0*u,
0*s+0*r+0*u-0*t,
0*t+r*0+s*0-u*0,
0*u+0*r+0*t-0*s *] by A1,A2,A7,QUATERNI:def 10
.=[*0,0*] by QUATERNI:def 6
.=0 by ARYTM_0:def 7;
end;
theorem
q = 0 implies c * q = 0
proof
assume
A1: q = 0;
A2: 0 = [*0,0*] by ARYTM_0:def 7
.= [*0,0,0,0*] by QUATERNI:def 6;
consider r,s,t,u being Element of REAL such that
A7: c = [*r,s,t,u*] by QUA7;
thus c*q = [* r*0-s*0-t*0-u*0,
r*0+s*0+t*0-u*0,
r*0+0*t+0*u-0*s,
r*0+u*0+s*0-t*0 *] by A1,A2,A7,QUATERNI:def 10
.=[*0,0*] by QUATERNI:def 6
.=0 by ARYTM_0:def 7;
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)***+
(Rea r * Im2 q + Im1 r * Im3 q -Im2 r * Rea q - Im3 r * Im1 q) / (|.r.|^2)*+
(Rea r * Im3 q - Im1 r * Im2 q +Im2 r * Im1 q - Im3 r * Rea q) / (|.r.|^2)*;
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)***+
(r0*q2+r1*q3-r2*q0-r3*q1)/(|.r.|^2)*+
(r0*q3-r1*q2+r2*q1-r3*q0)/(|.r.|^2)* 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)*** -
Im2 r / (|.r.|^2)* - (Im3 r) / (|.r.|^2)*;
coherence;
compatibility
proof
consider r0,r1,r2,r3 being Element of REAL such that
A1: r = [*r0,r1,r2,r3*] by QUA7;
A2: 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 A1,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 A1,A2,Def1
.=r0/(|.r.|^2) + (-r1/(|.r.|^2))*** +
(-r2/(|.r.|^2))* + (-r3/(|.r.|^2))* by Th35
.=r0/|.r.|^2 + -((r1/|.r.|^2)***) +
(-(r2/|.r.|^2))* + (-(r3/|.r.|^2))* by Th38
.=r0/|.r.|^2 - r1/|.r.|^2*** +
-(r2/|.r.|^2*) + (-(r3/|.r.|^2))* by Th38
.=r0/|.r.|^2 - r1/|.r.|^2*** -
r2/|.r.|^2* + -(r3/|.r.|^2*) 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 r0,r1,r2,r3 being Element of REAL such that
A1: r = [*r0,r1,r2,r3*] by QUA7;
A2: 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 A1,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 A1,A2,Def1
.=[*r0/(|.r.|^2), -r1/(|.r.|^2),
-r2/(|.r.|^2), -r3/(|.r.|^2) *];
hence thesis by A4,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 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
proof
the carrier of G_Quaternion = QUATERNION by Def13;
hence G_Quaternion is non empty by STRUCT_0:def 1;
end;
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 by QUATERNI:def 2;
end;
end;
registration
let x,y be Element of G_Quaternion;
let a,b be quaternion number;
cluster x+y; cluster a+b;
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;
cluster -x; cluster -a;
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;
cluster x-y; cluster a-b;
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
proof
the carrier of R_Quaternion = QUATERNION by Def11;
hence R_Quaternion is non empty by STRUCT_0:def 1;
end;
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 by QUATERNI:def 2;
end;
end;
registration let a,b be quaternion number;
let x,y be Element of R_Quaternion;
cluster x+y; cluster a+b;
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;
cluster x*y; cluster a*b;
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;
cluster -x; cluster -a;
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;
cluster x-y; cluster a-b;
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;*