:: Inner Products, Group, Ring of Quaternion Numbers
:: by Fuguo Ge
::
:: Received March 18, 2008
:: Copyright (c) 2008-2017 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, GROUP_1, VECTSP_1;
equalities SQUARE_1, COMPLEX1, XCMPLX_0, QUATERNI, ALGSTR_0, BINOP_1,
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;
coherence by QUATERNI:def 2;
end;
definition
redefine func 1q -> Element of QUATERNION;
coherence by QUATERNI:def 2;
end;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
theorem Th1:
for x,y,z,w being Real holds [*x,y,z,w*] = x + y** + z* + w*
proof
let x,y,z,w be Real;
reconsider x0=x+0, y0=y+0 as Element of REAL by XREAL_0:def 1;
** = [*In(0,REAL),jj*] by ARYTM_0:def 5;
then ** = [*0,jj,0,0*] by QUATERNI:91;
then
A1: y*** = [*y*0,y*jj,y*0,y*0*] by QUATERNI:def 21
.= [*0,y,0,0*];
A2: z* = [*z*0,z*0,z*jj,y*0*] by QUATERNI:def 21
.= [*0,0,z,0*];
A3: w* = [*w*0,w*0,w*0,w*jj*] by QUATERNI:def 21
.= [*0,0,0,w*];
x + y* ** = [*x0,y0,0,0*] by A1,QUATERNI:def 19
.= [*x,y,0,0*];
then x + y*** + z* = [*x0,y0,0+z,0+0*] by A2,QUATERNI:def 7
.= [*x,y,z,0*];
then x + y*** + z* + w* = [*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 ** -> Element of QUATERNION;
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;
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)***+
(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)*
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)***+
(r0*q2+r1*q3-r2*q0-r3*q1)/(|.r.|^2)*+
(r0*q3-r1*q2+r2*q1-r3*q0)/(|.r.|^2)* 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;
coherence;
end;
theorem
r" = Rea r / (|.r.|^2) - Im1 r / (|.r.|^2)*** -
Im2 r / (|.r.|^2)* - (Im3 r) / (|.r.|^2)*
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))*** +
(-r2/(|.r.|^2))* + (-r3/(|.r.|^2))* by Th1,A4,A8,A9,A10
.=r0/|.r.|^2 + -((r1/|.r.|^2)***) +
(-(r2/|.r.|^2))* + (-(r3/|.r.|^2))* by Th9
.=r0/|.r.|^2 - r1/|.r.|^2*** +
-(r2/|.r.|^2*) + (-(r3/|.r.|^2))* by Th9
.=r0/|.r.|^2 - r1/|.r.|^2*** -
r2/|.r.|^2* + -(r3/|.r.|^2*) 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;
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;
*