:: by Fuguo Ge

::

:: Received March 18, 2008

:: Copyright (c) 2008-2021 Association of Mizar Users

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

proof 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;

definition

:: original: 0q

redefine func 0q -> Element of QUATERNION ;

coherence

0q is Element of QUATERNION by QUATERNI:def 2;

end;
redefine func 0q -> Element of QUATERNION ;

coherence

0q is Element of QUATERNION by QUATERNI:def 2;

definition

:: original: 1q

redefine func 1q -> Element of QUATERNION ;

coherence

1q is Element of QUATERNION by QUATERNI:def 2;

end;
redefine func 1q -> Element of QUATERNION ;

coherence

1q is Element of QUATERNION by QUATERNI:def 2;

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

theorem :: QUATERN2:5

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

proof end;

definition

:: original: <i>

redefine func <i> -> Element of QUATERNION ;

coherence

<i> is Element of QUATERNION by QUATERNI:def 2;

end;
redefine func <i> -> Element of QUATERNION ;

coherence

<i> is Element of QUATERNION by QUATERNI:def 2;

Lm4: for r being Quaternion st |.r.| = 0 holds

r = 0

by QUATERNI:66;

definition

let q, r be Quaternion;

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;

ex b_{1} being Number ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st

( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & b_{1} = [*(((((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))*] )

for b_{1}, b_{2} being Number st ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st

( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & b_{1} = [*(((((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))*] ) & ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st

( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & b_{2} = [*(((((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))*] ) holds

b_{1} = b_{2}

end;
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: :: QUATERN2:def 1

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

ex b

( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & b

proof end;

uniqueness for b

( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & b

( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & b

b

proof end;

:: deftheorem Def1 defines / QUATERN2:def 1 :

for q, r being Quaternion

for b_{3} being Number holds

( b_{3} = q / r iff ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st

( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & b_{3} = [*(((((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))*] ) );

for q, r being Quaternion

for b

( b

( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & b

registration
end;

definition

let q, r be Quaternion;

:: original: /

redefine func q / r -> Element of QUATERNION ;

coherence

q / r is Element of QUATERNION by QUATERNI:def 2;

end;
:: original: /

redefine func q / r -> Element of QUATERNION ;

coherence

q / r is Element of QUATERNION by QUATERNI:def 2;

theorem :: QUATERN2:27

for q, r being Quaternion holds q / r = ((((((((Rea r) * (Rea q)) + ((Im1 q) * (Im1 r))) + ((Im2 r) * (Im2 q))) + ((Im3 r) * (Im3 q))) / (|.r.| ^2)) + (((((((Rea r) * (Im1 q)) - ((Im1 r) * (Rea q))) - ((Im2 r) * (Im3 q))) + ((Im3 r) * (Im2 q))) / (|.r.| ^2)) * <i>)) + (((((((Rea r) * (Im2 q)) + ((Im1 r) * (Im3 q))) - ((Im2 r) * (Rea q))) - ((Im3 r) * (Im1 q))) / (|.r.| ^2)) * <j>)) + (((((((Rea r) * (Im3 q)) - ((Im1 r) * (Im2 q))) + ((Im2 r) * (Im1 q))) - ((Im3 r) * (Rea q))) / (|.r.| ^2)) * <k>)

proof end;

definition

let r be Quaternion;

:: original: "

redefine func r " -> Element of QUATERNION ;

coherence

r " is Element of QUATERNION ;

end;
:: original: "

redefine func r " -> Element of QUATERNION ;

coherence

r " is Element of QUATERNION ;

theorem :: QUATERN2:28

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

proof end;

theorem :: QUATERN2:29

for r being Quaternion holds

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

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

theorem :: QUATERN2:30

for q, r being Quaternion holds

( 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) )

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

Lm5: 0 in REAL

by XREAL_0:def 1;

definition

ex b_{1} being UnOp of QUATERNION st

for c being Element of QUATERNION holds b_{1} . c = - c
from FUNCT_2:sch 4();

uniqueness

for b_{1}, b_{2} being UnOp of QUATERNION st ( for c being Element of QUATERNION holds b_{1} . c = - c ) & ( for c being Element of QUATERNION holds b_{2} . c = - c ) holds

b_{1} = b_{2}
from BINOP_2:sch 1();

ex b_{1} being BinOp of QUATERNION st

for c1, c2 being Element of QUATERNION holds b_{1} . (c1,c2) = c1 + c2
from BINOP_1:sch 4();

uniqueness

for b_{1}, b_{2} being BinOp of QUATERNION st ( for c1, c2 being Element of QUATERNION holds b_{1} . (c1,c2) = c1 + c2 ) & ( for c1, c2 being Element of QUATERNION holds b_{2} . (c1,c2) = c1 + c2 ) holds

b_{1} = b_{2}
from BINOP_2:sch 2();

ex b_{1} being BinOp of QUATERNION st

for c1, c2 being Element of QUATERNION holds b_{1} . (c1,c2) = c1 - c2
from BINOP_1:sch 4();

uniqueness

for b_{1}, b_{2} being BinOp of QUATERNION st ( for c1, c2 being Element of QUATERNION holds b_{1} . (c1,c2) = c1 - c2 ) & ( for c1, c2 being Element of QUATERNION holds b_{2} . (c1,c2) = c1 - c2 ) holds

b_{1} = b_{2}
from BINOP_2:sch 2();

ex b_{1} being BinOp of QUATERNION st

for c1, c2 being Element of QUATERNION holds b_{1} . (c1,c2) = c1 * c2
from BINOP_1:sch 4();

uniqueness

for b_{1}, b_{2} being BinOp of QUATERNION st ( for c1, c2 being Element of QUATERNION holds b_{1} . (c1,c2) = c1 * c2 ) & ( for c1, c2 being Element of QUATERNION holds b_{2} . (c1,c2) = c1 * c2 ) holds

b_{1} = b_{2}
from BINOP_2:sch 2();

ex b_{1} being BinOp of QUATERNION st

for c1, c2 being Element of QUATERNION holds b_{1} . (c1,c2) = c1 / c2
from BINOP_1:sch 4();

uniqueness

for b_{1}, b_{2} being BinOp of QUATERNION st ( for c1, c2 being Element of QUATERNION holds b_{1} . (c1,c2) = c1 / c2 ) & ( for c1, c2 being Element of QUATERNION holds b_{2} . (c1,c2) = c1 / c2 ) holds

b_{1} = b_{2}
from BINOP_2:sch 2();

ex b_{1} being UnOp of QUATERNION st

for c being Element of QUATERNION holds b_{1} . c = c "
from FUNCT_2:sch 4();

uniqueness

for b_{1}, b_{2} being UnOp of QUATERNION st ( for c being Element of QUATERNION holds b_{1} . c = c " ) & ( for c being Element of QUATERNION holds b_{2} . c = c " ) holds

b_{1} = b_{2}
from BINOP_2:sch 1();

end;

func compquaternion -> UnOp of QUATERNION means :: QUATERN2:def 3

for c being Element of QUATERNION holds it . c = - c;

existence for c being Element of QUATERNION holds it . c = - c;

ex b

for c being Element of QUATERNION holds b

uniqueness

for b

b

func addquaternion -> BinOp of QUATERNION means :Def4: :: QUATERN2:def 4

for c1, c2 being Element of QUATERNION holds it . (c1,c2) = c1 + c2;

existence for c1, c2 being Element of QUATERNION holds it . (c1,c2) = c1 + c2;

ex b

for c1, c2 being Element of QUATERNION holds b

uniqueness

for b

b

func diffquaternion -> BinOp of QUATERNION means :: QUATERN2:def 5

for c1, c2 being Element of QUATERNION holds it . (c1,c2) = c1 - c2;

existence for c1, c2 being Element of QUATERNION holds it . (c1,c2) = c1 - c2;

ex b

for c1, c2 being Element of QUATERNION holds b

uniqueness

for b

b

func multquaternion -> BinOp of QUATERNION means :Def6: :: QUATERN2:def 6

for c1, c2 being Element of QUATERNION holds it . (c1,c2) = c1 * c2;

existence for c1, c2 being Element of QUATERNION holds it . (c1,c2) = c1 * c2;

ex b

for c1, c2 being Element of QUATERNION holds b

uniqueness

for b

b

func divquaternion -> BinOp of QUATERNION means :: QUATERN2:def 7

for c1, c2 being Element of QUATERNION holds it . (c1,c2) = c1 / c2;

existence for c1, c2 being Element of QUATERNION holds it . (c1,c2) = c1 / c2;

ex b

for c1, c2 being Element of QUATERNION holds b

uniqueness

for b

b

func invquaternion -> UnOp of QUATERNION means :: QUATERN2:def 8

for c being Element of QUATERNION holds it . c = c " ;

existence for c being Element of QUATERNION holds it . c = c " ;

ex b

for c being Element of QUATERNION holds b

uniqueness

for b

b

:: deftheorem defines compquaternion QUATERN2:def 3 :

for b_{1} being UnOp of QUATERNION holds

( b_{1} = compquaternion iff for c being Element of QUATERNION holds b_{1} . c = - c );

for b

( b

:: deftheorem Def4 defines addquaternion QUATERN2:def 4 :

for b_{1} being BinOp of QUATERNION holds

( b_{1} = addquaternion iff for c1, c2 being Element of QUATERNION holds b_{1} . (c1,c2) = c1 + c2 );

for b

( b

:: deftheorem defines diffquaternion QUATERN2:def 5 :

for b_{1} being BinOp of QUATERNION holds

( b_{1} = diffquaternion iff for c1, c2 being Element of QUATERNION holds b_{1} . (c1,c2) = c1 - c2 );

for b

( b

:: deftheorem Def6 defines multquaternion QUATERN2:def 6 :

for b_{1} being BinOp of QUATERNION holds

( b_{1} = multquaternion iff for c1, c2 being Element of QUATERNION holds b_{1} . (c1,c2) = c1 * c2 );

for b

( b

:: deftheorem defines divquaternion QUATERN2:def 7 :

for b_{1} being BinOp of QUATERNION holds

( b_{1} = divquaternion iff for c1, c2 being Element of QUATERNION holds b_{1} . (c1,c2) = c1 / c2 );

for b

( b

:: deftheorem defines invquaternion QUATERN2:def 8 :

for b_{1} being UnOp of QUATERNION holds

( b_{1} = invquaternion iff for c being Element of QUATERNION holds b_{1} . c = c " );

for b

( b

definition

ex b_{1} being strict addLoopStr st

( the carrier of b_{1} = QUATERNION & the addF of b_{1} = addquaternion & 0. b_{1} = 0q )

for b_{1}, b_{2} being strict addLoopStr st the carrier of b_{1} = QUATERNION & the addF of b_{1} = addquaternion & 0. b_{1} = 0q & the carrier of b_{2} = QUATERNION & the addF of b_{2} = addquaternion & 0. b_{2} = 0q holds

b_{1} = b_{2}
;

end;

func G_Quaternion -> strict addLoopStr means :Def9: :: QUATERN2:def 9

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

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

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def9 defines G_Quaternion QUATERN2:def 9 :

for b_{1} being strict addLoopStr holds

( b_{1} = G_Quaternion iff ( the carrier of b_{1} = QUATERNION & the addF of b_{1} = addquaternion & 0. b_{1} = 0q ) );

for b

( b

registration
end;

registration
end;

registration

let x, y be Element of G_Quaternion;

let a, b be Quaternion;

compatibility

( x = a & y = b implies x + y = a + b )

end;
let a, b be Quaternion;

compatibility

( x = a & y = b implies x + y = a + b )

proof end;

registration

coherence

( G_Quaternion is Abelian & G_Quaternion is add-associative & G_Quaternion is right_zeroed & G_Quaternion is right_complementable )

end;
( G_Quaternion is Abelian & G_Quaternion is add-associative & G_Quaternion is right_zeroed & G_Quaternion is right_complementable )

proof end;

registration

let x be Element of G_Quaternion;

let a be Quaternion;

compatibility

( x = a implies - x = - a )

end;
let a be Quaternion;

compatibility

( x = a implies - x = - a )

proof end;

registration

let x, y be Element of G_Quaternion;

let a, b be Quaternion;

compatibility

( x = a & y = b implies x - y = a - b ) ;

end;
let a, b be Quaternion;

compatibility

( x = a & y = b implies x - y = a - b ) ;

theorem :: QUATERN2:36

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, RLVECT_1:def 4;

( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. G_Quaternion) = x ) by RLVECT_1:def 3, RLVECT_1:def 4;

definition

ex b_{1} being strict doubleLoopStr st

( the carrier of b_{1} = QUATERNION & the addF of b_{1} = addquaternion & the multF of b_{1} = multquaternion & 1. b_{1} = 1q & 0. b_{1} = 0q )

for b_{1}, b_{2} being strict doubleLoopStr st the carrier of b_{1} = QUATERNION & the addF of b_{1} = addquaternion & the multF of b_{1} = multquaternion & 1. b_{1} = 1q & 0. b_{1} = 0q & the carrier of b_{2} = QUATERNION & the addF of b_{2} = addquaternion & the multF of b_{2} = multquaternion & 1. b_{2} = 1q & 0. b_{2} = 0q holds

b_{1} = b_{2}
;

end;

func R_Quaternion -> strict doubleLoopStr means :Def10: :: QUATERN2:def 10

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

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

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def10 defines R_Quaternion QUATERN2:def 10 :

for b_{1} being strict doubleLoopStr holds

( b_{1} = R_Quaternion iff ( the carrier of b_{1} = QUATERNION & the addF of b_{1} = addquaternion & the multF of b_{1} = multquaternion & 1. b_{1} = 1q & 0. b_{1} = 0q ) );

for b

( b

registration
end;

registration
end;

registration

let a, b be Quaternion;

let x, y be Element of R_Quaternion;

compatibility

( x = a & y = b implies x + y = a + b )

( x = a & y = b implies x * y = a * b )

end;
let x, y be Element of R_Quaternion;

compatibility

( x = a & y = b implies x + y = a + b )

proof end;

compatibility ( x = a & y = b implies x * y = a * b )

proof end;

registration
end;

registration

( R_Quaternion is add-associative & R_Quaternion is right_zeroed & R_Quaternion is right_complementable & R_Quaternion is Abelian & R_Quaternion is associative & R_Quaternion is left_unital & R_Quaternion is right_unital & R_Quaternion is distributive & R_Quaternion is almost_right_invertible & not R_Quaternion is degenerated )
end;

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

coherence ( R_Quaternion is add-associative & R_Quaternion is right_zeroed & R_Quaternion is right_complementable & R_Quaternion is Abelian & R_Quaternion is associative & R_Quaternion is left_unital & R_Quaternion is right_unital & R_Quaternion is distributive & R_Quaternion is almost_right_invertible & not R_Quaternion is degenerated )

proof end;

registration

let x be Element of R_Quaternion;

let a be Quaternion;

compatibility

( x = a implies - x = - a )

end;
let a be Quaternion;

compatibility

( x = a implies - x = - a )

proof end;

registration

let x, y be Element of R_Quaternion;

let a, b be Quaternion;

compatibility

( x = a & y = b implies x - y = a - b ) ;

end;
let a, b be Quaternion;

compatibility

( x = a & y = b implies x - y = a - b ) ;

definition

let z be Element of R_Quaternion;

:: original: *'

redefine func z *' -> Element of R_Quaternion;

coherence

z *' is Element of R_Quaternion by Def10;

end;
:: original: *'

redefine func z *' -> Element of R_Quaternion;

coherence

z *' is Element of R_Quaternion by Def10;

theorem :: QUATERN2:45

theorem Th48: :: QUATERN2:48

for c1, c2 being Quaternion holds 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 end;

theorem :: QUATERN2:50

for c being Quaternion holds

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

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

proof end;

theorem :: QUATERN2:53

theorem :: QUATERN2:58

theorem :: QUATERN2:60

for c1, c2 being Quaternion holds (c1 + c2) .|. (c1 + c2) = (((c1 .|. c1) + (c1 .|. c2)) + (c2 .|. c1)) + (c2 .|. c2)

proof end;

theorem :: QUATERN2:61

for c1, c2 being Quaternion holds (c1 - c2) .|. (c1 - c2) = (((c1 .|. c1) - (c1 .|. c2)) - (c2 .|. c1)) + (c2 .|. c2)

proof end;