:: The Quaternion Numbers
:: by Xiquan Liang and Fuguo Ge
::
:: Received November 14, 2006
:: Copyright (c) 2006-2021 Association of Mizar Users

definition

func QUATERNION -> set equals :: QUATERNI:def 1
((Funcs (4,REAL)) \ { x where x is Element of Funcs (4,REAL) : ( x . 2 = 0 & x . 3 = 0 ) } ) \/ COMPLEX;

coherence
((Funcs (4,REAL)) \ { x where x is Element of Funcs (4,REAL) : ( x . 2 = 0 & x . 3 = 0 ) } ) \/ COMPLEX is set ;

end;

:: deftheorem defines QUATERNION QUATERNI:def 1 :
QUATERNION = ((Funcs (4,REAL)) \ { x where x is Element of Funcs (4,REAL) : ( x . 2 = 0 & x . 3 = 0 ) } ) \/ COMPLEX;

definition

let x be Number ;

attr x is quaternion means :Def2: :: QUATERNI:def 2
x in QUATERNION ;

end;

:: deftheorem Def2 defines quaternion QUATERNI:def 2 :
for x being Number holds
( x is quaternion iff x in QUATERNION );

registration

cluster QUATERNION -> non empty ;

coherence
not QUATERNION is empty ;

end;

registration

cluster quaternion for object ;

existence
ex b₁ being Number st b₁ is quaternion

proof end;

end;

definition

mode Quaternion is quaternion Number ;

end;

canceled;

theorem :: QUATERNI:1

canceled;

theorem :: QUATERNI:2

canceled;

theorem :: QUATERNI:3

canceled;

theorem :: QUATERNI:4

canceled;

Lm1: 0 ,1,2,3 are_mutually_distinct
;

theorem :: QUATERNI:5

for x1, x2, x3, x4, X being set holds
( {x1,x2,x3,x4} c= X iff ( x1 in X & x2 in X & x3 in X & x4 in X ) )

proof end;

definition

let A be non empty set ;
let x, y, w, z be set ;
let a, b, c, d be Element of A;
:: original: -->
redefine func (x,y,w,z) --> (a,b,c,d) -> Function of {x,y,w,z},A;
coherence
(x,y,w,z) --> (a,b,c,d) is Function of {x,y,w,z},A

proof end;

end;

definition

func <j> -> Number equals :: QUATERNI:def 3
(0,1,2,3) --> (0,0,1,0);

coherence
(0,1,2,3) --> (0,0,1,0) is Number ;

func <k> -> Number equals :: QUATERNI:def 4
(0,1,2,3) --> (0,0,0,1);

coherence
(0,1,2,3) --> (0,0,0,1) is Number ;

end;

:: deftheorem defines <j> QUATERNI:def 3 :
<j> = (0,1,2,3) --> (0,0,1,0);

:: deftheorem defines <k> QUATERNI:def 4 :
<k> = (0,1,2,3) --> (0,0,0,1);

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

Lm2: <i> = [*zz,jj*]
by ARYTM_0:def 5;

registration

cluster <i> -> quaternion ;

coherence
<i> is quaternion by Lm2, XBOOLE_0:def 3;

cluster <j> -> quaternion ;

coherence
<j> is quaternion

proof end;

cluster <k> -> quaternion ;

coherence
<k> is quaternion

proof end;

end;

registration

cluster -> quaternion for Element of QUATERNION ;

coherence
for b₁ being Element of QUATERNION holds b₁ is quaternion ;

end;

definition

let x, y, w, z be Real;

func [*x,y,w,z*] -> Element of QUATERNION means :Def5: :: QUATERNI:def 5
ex x9, y9 being Element of REAL st
( x9 = x & y9 = y & it = [*x9,y9*] ) if ( w = 0 & z = 0 )
otherwise it = (0,1,2,3) --> (x,y,w,z);

consistency
for b₁ being Element of QUATERNION holds verum ;
existence
( ( w = 0 & z = 0 implies ex b₁ being Element of QUATERNION ex x9, y9 being Element of REAL st
( x9 = x & y9 = y & b₁ = [*x9,y9*] ) ) & ( ( not w = 0 or not z = 0 ) implies ex b₁ being Element of QUATERNION st b₁ = (0,1,2,3) --> (x,y,w,z) ) )

proof end;

uniqueness
for b₁, b₂ being Element of QUATERNION holds
( ( w = 0 & z = 0 & ex x9, y9 being Element of REAL st
( x9 = x & y9 = y & b₁ = [*x9,y9*] ) & ex x9, y9 being Element of REAL st
( x9 = x & y9 = y & b₂ = [*x9,y9*] ) implies b₁ = b₂ ) & ( ( not w = 0 or not z = 0 ) & b₁ = (0,1,2,3) --> (x,y,w,z) & b₂ = (0,1,2,3) --> (x,y,w,z) implies b₁ = b₂ ) ) ;

end;

:: deftheorem Def5 defines [* QUATERNI:def 5 :
for x, y, w, z being Real
for b₅ being Element of QUATERNION holds
( ( w = 0 & z = 0 implies ( b₅ = [*x,y,w,z*] iff ex x9, y9 being Element of REAL st
( x9 = x & y9 = y & b₅ = [*x9,y9*] ) ) ) & ( ( not w = 0 or not z = 0 ) implies ( b₅ = [*x,y,w,z*] iff b₅ = (0,1,2,3) --> (x,y,w,z) ) ) );

Lm3: for x, y being Element of REAL holds [*x,y,0,0*] = [*x,y*]

proof end;

theorem :: QUATERNI:6

canceled;

::$CT

theorem Th2: :: QUATERNI:7

for g being Quaternion ex r, s, t, u being Real st g = [*r,s,t,u*]

proof end;

theorem :: QUATERNI:8

canceled;

Lm4: for x, y, z being object st [x,y] = {z} holds
( z = {x} & x = y )

proof end;

theorem Th3: :: QUATERNI:9

for A being Subset of RAT+ st ex t being Element of RAT+ st
( t in A & t <> {} ) & ( for r, s being Element of RAT+ st r in A & s <=' r holds
s in A ) holds
ex r1, r2, r3, r4, r5 being Element of RAT+ st
( r1 in A & r2 in A & r3 in A & r4 in A & r5 in A & r1 <> r2 & r1 <> r3 & r1 <> r4 & r1 <> r5 & r2 <> r3 & r2 <> r4 & r2 <> r5 & r3 <> r4 & r3 <> r5 & r4 <> r5 )

proof end;

Lm5: for a, b, c, d being Real holds not (0,1,2,3) --> (a,b,c,d) in REAL

proof end;

theorem Th4: :: QUATERNI:10

for a, b, c, d being Real holds not (0,1,2,3) --> (a,b,c,d) in COMPLEX

proof end;

theorem :: QUATERNI:11

canceled;

::$CT

theorem Th5: :: QUATERNI:12

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

proof end;

definition

let x, y be Quaternion;
consider x1, x2, x3, x4 being Real such that
A1: x = [*x1,x2,x3,x4*] by Th2;
consider y1, y2, y3, y4 being Real such that
A2: y = [*y1,y2,y3,y4*] by Th2;

func x + y -> Number means :Def6: :: QUATERNI:def 6
ex x1, x2, x3, x4, y1, y2, y3, y4 being Real st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & it = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] );

existence
ex b₁ being Number ex x1, x2, x3, x4, y1, y2, y3, y4 being Real st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b₁ = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] )

proof end;

uniqueness
for b₁, b₂ being Number st ex x1, x2, x3, x4, y1, y2, y3, y4 being Real st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b₁ = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) & ex x1, x2, x3, x4, y1, y2, y3, y4 being Real st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b₂ = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) holds
b₁ = b₂

proof end;

commutativity
for b₁ being Number
for x, y being Quaternion st ex x1, x2, x3, x4, y1, y2, y3, y4 being Real st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b₁ = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) holds
ex x1, x2, x3, x4, y1, y2, y3, y4 being Real st
( y = [*x1,x2,x3,x4*] & x = [*y1,y2,y3,y4*] & b₁ = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) ;

end;

:: deftheorem Def6 defines + QUATERNI:def 6 :
for x, y being Quaternion
for b₃ being Number holds
( b₃ = x + y iff ex x1, x2, x3, x4, y1, y2, y3, y4 being Real st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b₃ = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) );

Lm6: 0 = [*0,0,0,0*]

proof end;

definition

let z be Quaternion;
consider v, w, x, y being Real such that
A1: z = [*v,w,x,y*] by Th2;

func - z -> Quaternion means :Def7: :: QUATERNI:def 7
z + it = 0 ;

existence
ex b₁ being Quaternion st z + b₁ = 0

proof end;

uniqueness
for b₁, b₂ being Quaternion st z + b₁ = 0 & z + b₂ = 0 holds
b₁ = b₂

proof end;

involutiveness
for b₁, b₂ being Quaternion st b₂ + b₁ = 0 holds
b₁ + b₂ = 0 ;

end;

:: deftheorem Def7 defines - QUATERNI:def 7 :
for z, b₂ being Quaternion holds
( b₂ = - z iff z + b₂ = 0 );

definition

let x, y be Quaternion;

func x - y -> Number equals :: QUATERNI:def 8
x + (- y);

coherence
x + (- y) is Number ;

end;

:: deftheorem defines - QUATERNI:def 8 :
for x, y being Quaternion holds x - y = x + (- y);

definition

let x, y be Quaternion;
consider x1, x2, x3, x4 being Real such that
A1: x = [*x1,x2,x3,x4*] by Th2;
consider y1, y2, y3, y4 being Real such that
A2: y = [*y1,y2,y3,y4*] by Th2;

func x * y -> Number means :Def9: :: QUATERNI:def 9
ex x1, x2, x3, x4, y1, y2, y3, y4 being Real st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & it = [*((((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))*] );

existence
ex b₁ being Number ex x1, x2, x3, x4, y1, y2, y3, y4 being Real st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b₁ = [*((((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))*] )

proof end;

uniqueness
for b₁, b₂ being Number st ex x1, x2, x3, x4, y1, y2, y3, y4 being Real st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b₁ = [*((((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))*] ) & ex x1, x2, x3, x4, y1, y2, y3, y4 being Real st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b₂ = [*((((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))*] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines * QUATERNI:def 9 :
for x, y being Quaternion
for b₃ being Number holds
( b₃ = x * y iff ex x1, x2, x3, x4, y1, y2, y3, y4 being Real st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b₃ = [*((((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))*] ) );

registration

let z, z9 be Quaternion;

cluster z + z9 -> quaternion ;

coherence
z + z9 is quaternion

proof end;

cluster z * z9 -> quaternion ;

coherence
z * z9 is quaternion

proof end;

end;

definition

:: original: <j>
redefine func <j> -> Element of QUATERNION equals :: QUATERNI:def 10
[*0,0,1,0*];

coherence
<j> is Element of QUATERNION by Def2;
compatibility
for b₁ being Element of QUATERNION holds
( b₁ = <j> iff b₁ = [*0,0,1,0*] ) by Def5;

:: original: <k>
redefine func <k> -> Element of QUATERNION equals :: QUATERNI:def 11
[*0,0,0,1*];

coherence
<k> is Element of QUATERNION by Def2;
compatibility
for b₁ being Element of QUATERNION holds
( b₁ = <k> iff b₁ = [*0,0,0,1*] ) by Def5;

end;

:: deftheorem defines <j> QUATERNI:def 10 :
<j> = [*0,0,1,0*];

:: deftheorem defines <k> QUATERNI:def 11 :
<k> = [*0,0,0,1*];

theorem :: QUATERNI:13

<i> * <i> = - 1

proof end;

theorem :: QUATERNI:14

<j> * <j> = - 1

proof end;

theorem :: QUATERNI:15

<k> * <k> = - 1

proof end;

theorem :: QUATERNI:16

<i> * <j> = <k>

proof end;

theorem :: QUATERNI:17

<j> * <k> = <i>

proof end;

theorem :: QUATERNI:18

<k> * <i> = <j>

proof end;

theorem :: QUATERNI:19

<i> * <j> = - (<j> * <i>)

proof end;

theorem :: QUATERNI:20

<j> * <k> = - (<k> * <j>)

proof end;

theorem :: QUATERNI:21

<k> * <i> = - (<i> * <k>)

proof end;

definition

let z be Quaternion;

func Rea z -> Number means :Def12: :: QUATERNI:def 12
ex z9 being Complex st
( z = z9 & it = Re z9 ) if z in COMPLEX
otherwise ex f being Function of 4,REAL st
( z = f & it = f . 0 );

existence
( ( z in COMPLEX implies ex b₁ being Number ex z9 being Complex st
( z = z9 & b₁ = Re z9 ) ) & ( not z in COMPLEX implies ex b₁ being Number ex f being Function of 4,REAL st
( z = f & b₁ = f . 0 ) ) )

proof end;

uniqueness
for b₁, b₂ being Number holds
( ( z in COMPLEX & ex z9 being Complex st
( z = z9 & b₁ = Re z9 ) & ex z9 being Complex st
( z = z9 & b₂ = Re z9 ) implies b₁ = b₂ ) & ( not z in COMPLEX & ex f being Function of 4,REAL st
( z = f & b₁ = f . 0 ) & ex f being Function of 4,REAL st
( z = f & b₂ = f . 0 ) implies b₁ = b₂ ) ) ;
consistency
for b₁ being Number holds verum ;

func Im1 z -> Number means :Def13: :: QUATERNI:def 13
ex z9 being Complex st
( z = z9 & it = Im z9 ) if z in COMPLEX
otherwise ex f being Function of 4,REAL st
( z = f & it = f . 1 );

existence
( ( z in COMPLEX implies ex b₁ being Number ex z9 being Complex st
( z = z9 & b₁ = Im z9 ) ) & ( not z in COMPLEX implies ex b₁ being Number ex f being Function of 4,REAL st
( z = f & b₁ = f . 1 ) ) )

proof end;

uniqueness
for b₁, b₂ being Number holds
( ( z in COMPLEX & ex z9 being Complex st
( z = z9 & b₁ = Im z9 ) & ex z9 being Complex st
( z = z9 & b₂ = Im z9 ) implies b₁ = b₂ ) & ( not z in COMPLEX & ex f being Function of 4,REAL st
( z = f & b₁ = f . 1 ) & ex f being Function of 4,REAL st
( z = f & b₂ = f . 1 ) implies b₁ = b₂ ) ) ;
consistency
for b₁ being Number holds verum ;

func Im2 z -> Number means :Def14: :: QUATERNI:def 14
it = 0 if z in COMPLEX
otherwise ex f being Function of 4,REAL st
( z = f & it = f . 2 );

existence
( ( z in COMPLEX implies ex b₁ being Number st b₁ = 0 ) & ( not z in COMPLEX implies ex b₁ being Number ex f being Function of 4,REAL st
( z = f & b₁ = f . 2 ) ) )

proof end;

uniqueness
for b₁, b₂ being Number holds
( ( z in COMPLEX & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) & ( not z in COMPLEX & ex f being Function of 4,REAL st
( z = f & b₁ = f . 2 ) & ex f being Function of 4,REAL st
( z = f & b₂ = f . 2 ) implies b₁ = b₂ ) ) ;
consistency
for b₁ being Number holds verum ;

func Im3 z -> Number means :Def15: :: QUATERNI:def 15
it = 0 if z in COMPLEX
otherwise ex f being Function of 4,REAL st
( z = f & it = f . 3 );

existence
( ( z in COMPLEX implies ex b₁ being Number st b₁ = 0 ) & ( not z in COMPLEX implies ex b₁ being Number ex f being Function of 4,REAL st
( z = f & b₁ = f . 3 ) ) )

proof end;

uniqueness
for b₁, b₂ being Number holds
( ( z in COMPLEX & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) & ( not z in COMPLEX & ex f being Function of 4,REAL st
( z = f & b₁ = f . 3 ) & ex f being Function of 4,REAL st
( z = f & b₂ = f . 3 ) implies b₁ = b₂ ) ) ;
consistency
for b₁ being Number holds verum ;

end;

:: deftheorem Def12 defines Rea QUATERNI:def 12 :
for z being Quaternion
for b₂ being Number holds
( ( z in COMPLEX implies ( b₂ = Rea z iff ex z9 being Complex st
( z = z9 & b₂ = Re z9 ) ) ) & ( not z in COMPLEX implies ( b₂ = Rea z iff ex f being Function of 4,REAL st
( z = f & b₂ = f . 0 ) ) ) );

:: deftheorem Def13 defines Im1 QUATERNI:def 13 :
for z being Quaternion
for b₂ being Number holds
( ( z in COMPLEX implies ( b₂ = Im1 z iff ex z9 being Complex st
( z = z9 & b₂ = Im z9 ) ) ) & ( not z in COMPLEX implies ( b₂ = Im1 z iff ex f being Function of 4,REAL st
( z = f & b₂ = f . 1 ) ) ) );

:: deftheorem Def14 defines Im2 QUATERNI:def 14 :
for z being Quaternion
for b₂ being Number holds
( ( z in COMPLEX implies ( b₂ = Im2 z iff b₂ = 0 ) ) & ( not z in COMPLEX implies ( b₂ = Im2 z iff ex f being Function of 4,REAL st
( z = f & b₂ = f . 2 ) ) ) );

:: deftheorem Def15 defines Im3 QUATERNI:def 15 :
for z being Quaternion
for b₂ being Number holds
( ( z in COMPLEX implies ( b₂ = Im3 z iff b₂ = 0 ) ) & ( not z in COMPLEX implies ( b₂ = Im3 z iff ex f being Function of 4,REAL st
( z = f & b₂ = f . 3 ) ) ) );

registration

let z be Quaternion;

cluster Rea z -> real ;

coherence
Rea z is real

proof end;

cluster Im1 z -> real ;

coherence
Im1 z is real

proof end;

cluster Im2 z -> real ;

coherence
Im2 z is real

proof end;

cluster Im3 z -> real ;

coherence
Im3 z is real

proof end;

end;

theorem Th15: :: QUATERNI:22

for f being Function of 4,REAL ex a, b, c, d being Real st f = (0,1,2,3) --> (a,b,c,d)

proof end;

Lm7: for a, b being Element of REAL holds
( Re [*a,b*] = a & Im [*a,b*] = b )

proof end;

Lm8: for z being Complex holds [*(Re z),(Im z)*] = z

proof end;

theorem Th16: :: QUATERNI:23

for a, b, c, d being Real holds
( Rea [*a,b,c,d*] = a & Im1 [*a,b,c,d*] = b & Im2 [*a,b,c,d*] = c & Im3 [*a,b,c,d*] = d )

proof end;

theorem Th17: :: QUATERNI:24

for z being Quaternion holds z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*]

proof end;

theorem Th18: :: QUATERNI:25

for z1, z2 being Quaternion st Rea z1 = Rea z2 & Im1 z1 = Im1 z2 & Im2 z1 = Im2 z2 & Im3 z1 = Im3 z2 holds
z1 = z2

proof end;

definition

func 0q -> Quaternion equals :: QUATERNI:def 16
0 ;

coherence
0 is Quaternion by Lm6;

func 1q -> Quaternion equals :: QUATERNI:def 17
1;

coherence
1 is Quaternion

proof end;

end;

:: deftheorem defines 0q QUATERNI:def 16 :
0q = 0 ;

:: deftheorem defines 1q QUATERNI:def 17 :
1q = 1;

Lm9: 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 )

proof end;

theorem Th19: :: QUATERNI:26

for z being Quaternion st Rea z = 0 & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 holds
z = 0q

proof end;

theorem :: QUATERNI:27

for z being Quaternion st z = 0 holds
((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) = 0

proof end;

theorem :: QUATERNI:28

for z being Quaternion st ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) = 0 holds
z = 0q

proof end;

Lm10: [*jj,zz,zz,zz*] = 1

proof end;

theorem :: QUATERNI:29

( Rea 1q = 1 & Im1 1q = 0 & Im2 1q = 0 & Im3 1q = 0 ) by Lm10, Th16;

theorem Th23: :: QUATERNI:30

( Rea <i> = 0 & Im1 <i> = 1 & Im2 <i> = 0 & Im3 <i> = 0 )

proof end;

theorem Th24: :: QUATERNI:31

( Rea <j> = 0 & Im1 <j> = 0 & Im2 <j> = 1 & Im3 <j> = 0 & Rea <k> = 0 & Im1 <k> = 0 & Im2 <k> = 0 & Im3 <k> = 1 ) by Th16;

Lm11: for m, n, x, y, z being Quaternion st z = ((m + n) + x) + y holds
( Rea z = (((Rea m) + (Rea n)) + (Rea x)) + (Rea y) & Im1 z = (((Im1 m) + (Im1 n)) + (Im1 x)) + (Im1 y) & Im2 z = (((Im2 m) + (Im2 n)) + (Im2 x)) + (Im2 y) & Im3 z = (((Im3 m) + (Im3 n)) + (Im3 x)) + (Im3 y) )

proof end;

Lm12: for x, y, z being Quaternion st z = x + y holds
( Rea z = (Rea x) + (Rea y) & Im1 z = (Im1 x) + (Im1 y) & Im2 z = (Im2 x) + (Im2 y) & Im3 z = (Im3 x) + (Im3 y) )

proof end;

Lm13: for z1, z2 being Quaternion holds z1 + z2 = [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*]

proof end;

Lm14: for x, y, z being Quaternion st z = x * y holds
( Rea z = ((((Rea x) * (Rea y)) - ((Im1 x) * (Im1 y))) - ((Im2 x) * (Im2 y))) - ((Im3 x) * (Im3 y)) & Im1 z = ((((Rea x) * (Im1 y)) + ((Im1 x) * (Rea y))) + ((Im2 x) * (Im3 y))) - ((Im3 x) * (Im2 y)) & Im2 z = ((((Rea x) * (Im2 y)) + ((Im2 x) * (Rea y))) + ((Im3 x) * (Im1 y))) - ((Im1 x) * (Im3 y)) & Im3 z = ((((Rea x) * (Im3 y)) + ((Im3 x) * (Rea y))) + ((Im1 x) * (Im2 y))) - ((Im2 x) * (Im1 y)) )

proof end;

Lm15: for z1, z2, z3, z4 being Quaternion holds ((z1 + z2) + z3) + z4 = [*((((Rea z1) + (Rea z2)) + (Rea z3)) + (Rea z4)),((((Im1 z1) + (Im1 z2)) + (Im1 z3)) + (Im1 z4)),((((Im2 z1) + (Im2 z2)) + (Im2 z3)) + (Im2 z4)),((((Im3 z1) + (Im3 z2)) + (Im3 z3)) + (Im3 z4))*]

proof end;

Lm16: for z1, z2 being Quaternion holds z1 * z2 = [*(((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))),(((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))),(((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2))),(((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2)))*]

proof end;

Lm17: for z1, z2 being Quaternion holds
( Rea (z1 * z2) = ((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2)) & Im1 (z1 * z2) = ((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)) & Im2 (z1 * z2) = ((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2)) & Im3 (z1 * z2) = ((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2)) )

proof end;

theorem :: QUATERNI:32

for z1, z2, z3, z4 being Quaternion holds
( Rea (((z1 + z2) + z3) + z4) = (((Rea z1) + (Rea z2)) + (Rea z3)) + (Rea z4) & Im1 (((z1 + z2) + z3) + z4) = (((Im1 z1) + (Im1 z2)) + (Im1 z3)) + (Im1 z4) & Im2 (((z1 + z2) + z3) + z4) = (((Im2 z1) + (Im2 z2)) + (Im2 z3)) + (Im2 z4) & Im3 (((z1 + z2) + z3) + z4) = (((Im3 z1) + (Im3 z2)) + (Im3 z3)) + (Im3 z4) )

proof end;

Lm18: for z being Quaternion
for x being Real st z = x holds
( Rea z = x & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 )

proof end;

theorem :: QUATERNI:33

for z1 being Quaternion
for x being Real st z1 = x holds
( Rea (z1 * <i>) = 0 & Im1 (z1 * <i>) = x & Im2 (z1 * <i>) = 0 & Im3 (z1 * <i>) = 0 )

proof end;

theorem :: QUATERNI:34

for z1 being Quaternion
for x being Real st z1 = x holds
( Rea (z1 * <j>) = 0 & Im1 (z1 * <j>) = 0 & Im2 (z1 * <j>) = x & Im3 (z1 * <j>) = 0 )

proof end;

theorem :: QUATERNI:35

for z1 being Quaternion
for x being Real st z1 = x holds
( Rea (z1 * <k>) = 0 & Im1 (z1 * <k>) = 0 & Im2 (z1 * <k>) = 0 & Im3 (z1 * <k>) = x )

proof end;

definition

let x be Real;
let y be Quaternion;
consider y1, y2, y3, y4 being Real such that
A1: y = [*y1,y2,y3,y4*] by Th2;

func x + y -> Number means :Def18: :: QUATERNI:def 18
ex y1, y2, y3, y4 being Real st
( y = [*y1,y2,y3,y4*] & it = [*(x + y1),y2,y3,y4*] );

existence
ex b₁ being Number ex y1, y2, y3, y4 being Real st
( y = [*y1,y2,y3,y4*] & b₁ = [*(x + y1),y2,y3,y4*] )

proof end;

uniqueness
for b₁, b₂ being Number st ex y1, y2, y3, y4 being Real st
( y = [*y1,y2,y3,y4*] & b₁ = [*(x + y1),y2,y3,y4*] ) & ex y1, y2, y3, y4 being Real st
( y = [*y1,y2,y3,y4*] & b₂ = [*(x + y1),y2,y3,y4*] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def18 defines + QUATERNI:def 18 :
for x being Real
for y being Quaternion
for b₃ being Number holds
( b₃ = x + y iff ex y1, y2, y3, y4 being Real st
( y = [*y1,y2,y3,y4*] & b₃ = [*(x + y1),y2,y3,y4*] ) );

definition

let x be Real;
let y be Quaternion;

func x - y -> Number equals :: QUATERNI:def 19
x + (- y);

coherence
x + (- y) is Number ;

end;

:: deftheorem defines - QUATERNI:def 19 :
for x being Real
for y being Quaternion holds x - y = x + (- y);

definition

let x be Real;
let y be Quaternion;
consider y1, y2, y3, y4 being Real such that
A1: y = [*y1,y2,y3,y4*] by Th2;

func x * y -> Number means :Def20: :: QUATERNI:def 20
ex y1, y2, y3, y4 being Real st
( y = [*y1,y2,y3,y4*] & it = [*(x * y1),(x * y2),(x * y3),(x * y4)*] );

existence
ex b₁ being Number ex y1, y2, y3, y4 being Real st
( y = [*y1,y2,y3,y4*] & b₁ = [*(x * y1),(x * y2),(x * y3),(x * y4)*] )

proof end;

uniqueness
for b₁, b₂ being Number st ex y1, y2, y3, y4 being Real st
( y = [*y1,y2,y3,y4*] & b₁ = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) & ex y1, y2, y3, y4 being Real st
( y = [*y1,y2,y3,y4*] & b₂ = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def20 defines * QUATERNI:def 20 :
for x being Real
for y being Quaternion
for b₃ being Number holds
( b₃ = x * y iff ex y1, y2, y3, y4 being Real st
( y = [*y1,y2,y3,y4*] & b₃ = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) );

registration

let x be Real;
let z9 be Quaternion;

cluster x + z9 -> quaternion ;

coherence
x + z9 is quaternion

proof end;

cluster x * z9 -> quaternion ;

coherence
x * z9 is quaternion

proof end;

cluster x - z9 -> quaternion ;

coherence
x - z9 is quaternion ;

end;

Lm19: for x, y, z, w being Real holds [*x,y,z,w*] = ((x + (y * <i>)) + (z * <j>)) + (w * <k>)

proof end;

definition

let z1, z2 be Quaternion;
:: original: +
redefine func z1 + z2 -> Element of QUATERNION ;
coherence
z1 + z2 is Element of QUATERNION by Def2;

end;

Lm20: for z1, z2 being Quaternion holds z1 + z2 = ((((Rea z1) + (Rea z2)) + (((Im1 z1) + (Im1 z2)) * <i>)) + (((Im2 z1) + (Im2 z2)) * <j>)) + (((Im3 z1) + (Im3 z2)) * <k>)

proof end;

theorem Th29: :: QUATERNI:36

for z1, z2 being Quaternion holds
( Rea (z1 + z2) = (Rea z1) + (Rea z2) & Im1 (z1 + z2) = (Im1 z1) + (Im1 z2) & Im2 (z1 + z2) = (Im2 z1) + (Im2 z2) & Im3 (z1 + z2) = (Im3 z1) + (Im3 z2) )

proof end;

definition

let z1, z2 be Quaternion;
:: original: *
redefine func z1 * z2 -> Element of QUATERNION ;
coherence
z1 * z2 is Element of QUATERNION by Def2;

end;

Lm21: for z1, z2 being Quaternion holds z1 * z2 = (((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) + ((((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))) * <i>)) + ((((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2))) * <j>)) + ((((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2))) * <k>)

proof end;

theorem :: QUATERNI:37

for z being Quaternion holds z = (((Rea z) + ((Im1 z) * <i>)) + ((Im2 z) * <j>)) + ((Im3 z) * <k>)

proof end;

Lm22: for c being Quaternion holds c + 0q = c

proof end;

Lm23: ( 0 * <i> = 0 & 0 * <j> = 0 & 0 * <k> = 0 )

proof end;

theorem :: QUATERNI:38

for z1, z2 being Quaternion st Im1 z1 = 0 & Im1 z2 = 0 & Im2 z1 = 0 & Im2 z2 = 0 & Im3 z1 = 0 & Im3 z2 = 0 holds
( Rea (z1 * z2) = (Rea z1) * (Rea z2) & Im1 (z1 * z2) = ((Im2 z1) * (Im3 z2)) - ((Im3 z1) * (Im2 z2)) & Im2 (z1 * z2) = ((Im3 z1) * (Im1 z2)) - ((Im1 z1) * (Im3 z2)) & Im3 (z1 * z2) = ((Im1 z1) * (Im2 z2)) - ((Im2 z1) * (Im1 z2)) )

proof end;

theorem :: QUATERNI:39

for z1, z2 being Quaternion st Rea z1 = 0 & Rea z2 = 0 holds
( Rea (z1 * z2) = ((- ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2)) & Im1 (z1 * z2) = ((Im2 z1) * (Im3 z2)) - ((Im3 z1) * (Im2 z2)) & Im2 (z1 * z2) = ((Im3 z1) * (Im1 z2)) - ((Im1 z1) * (Im3 z2)) & Im3 (z1 * z2) = ((Im1 z1) * (Im2 z2)) - ((Im2 z1) * (Im1 z2)) )

proof end;

theorem :: QUATERNI:40

for z being Quaternion holds
( Rea (z * z) = ((((Rea z) ^2) - ((Im1 z) ^2)) - ((Im2 z) ^2)) - ((Im3 z) ^2) & Im1 (z * z) = 2 * ((Rea z) * (Im1 z)) & Im2 (z * z) = 2 * ((Rea z) * (Im2 z)) & Im3 (z * z) = 2 * ((Rea z) * (Im3 z)) )

proof end;

definition

let z be Quaternion;
:: original: -
redefine func - z -> Element of QUATERNION ;
coherence
- z is Element of QUATERNION by Def2;

end;

Lm24: for z being Quaternion holds - z = (((- (Rea z)) + ((- (Im1 z)) * <i>)) + ((- (Im2 z)) * <j>)) + ((- (Im3 z)) * <k>)

proof end;

theorem Th34: :: QUATERNI:41

for z being Quaternion holds
( Rea (- z) = - (Rea z) & Im1 (- z) = - (Im1 z) & Im2 (- z) = - (Im2 z) & Im3 (- z) = - (Im3 z) )

proof end;

definition

let z1, z2 be Quaternion;
:: original: -
redefine func z1 - z2 -> Element of QUATERNION ;
coherence
z1 - z2 is Element of QUATERNION by Def2;

end;

Lm25: for z1, z2 being Quaternion holds z1 - z2 = ((((Rea z1) - (Rea z2)) + (((Im1 z1) - (Im1 z2)) * <i>)) + (((Im2 z1) - (Im2 z2)) * <j>)) + (((Im3 z1) - (Im3 z2)) * <k>)

proof end;

theorem Th35: :: QUATERNI:42

for z1, z2 being Quaternion holds
( Rea (z1 - z2) = (Rea z1) - (Rea z2) & Im1 (z1 - z2) = (Im1 z1) - (Im1 z2) & Im2 (z1 - z2) = (Im2 z1) - (Im2 z2) & Im3 (z1 - z2) = (Im3 z1) - (Im3 z2) )

proof end;

definition

let z be Quaternion;

func z *' -> Quaternion equals :: QUATERNI:def 21
(((Rea z) + ((- (Im1 z)) * <i>)) + ((- (Im2 z)) * <j>)) + ((- (Im3 z)) * <k>);

coherence
(((Rea z) + ((- (Im1 z)) * <i>)) + ((- (Im2 z)) * <j>)) + ((- (Im3 z)) * <k>) is Quaternion ;

end;

:: deftheorem defines *' QUATERNI:def 21 :
for z being Quaternion holds z *' = (((Rea z) + ((- (Im1 z)) * <i>)) + ((- (Im2 z)) * <j>)) + ((- (Im3 z)) * <k>);

definition

let z be Quaternion;
:: original: *'
redefine func z *' -> Element of QUATERNION ;
coherence
z *' is Element of QUATERNION ;

end;

theorem Th36: :: QUATERNI:43

for z being Quaternion holds z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]

proof end;

theorem :: QUATERNI:44

for z being Quaternion holds
( Rea (z *') = Rea z & Im1 (z *') = - (Im1 z) & Im2 (z *') = - (Im2 z) & Im3 (z *') = - (Im3 z) )

proof end;

theorem :: QUATERNI:45

for z being Quaternion st z = 0 holds
z *' = 0

proof end;

theorem :: QUATERNI:46

for z being Quaternion st z *' = 0 holds
z = 0

proof end;

theorem :: QUATERNI:47

1q *' = 1q

proof end;

theorem :: QUATERNI:48

( Rea (<i> *') = 0 & Im1 (<i> *') = - 1 & Im2 (<i> *') = 0 & Im3 (<i> *') = 0 )

proof end;

theorem :: QUATERNI:49

( Rea (<j> *') = 0 & Im1 (<j> *') = 0 & Im2 (<j> *') = - 1 & Im3 (<j> *') = 0 )

proof end;

theorem :: QUATERNI:50

( Rea (<k> *') = 0 & Im1 (<k> *') = 0 & Im2 (<k> *') = 0 & Im3 (<k> *') = - 1 )

proof end;

theorem :: QUATERNI:51

<i> *' = - <i> by Th23, Lm24;

theorem :: QUATERNI:52

<j> *' = - <j> by Th24, Lm24;

theorem :: QUATERNI:53

<k> *' = - <k> by Th24, Lm24;

theorem :: QUATERNI:54

for z1, z2 being Quaternion holds (z1 + z2) *' = (z1 *') + (z2 *')

proof end;

theorem Th48: :: QUATERNI:55

for z being Quaternion holds (- z) *' = - (z *')

proof end;

theorem :: QUATERNI:56

for z1, z2 being Quaternion holds (z1 - z2) *' = (z1 *') - (z2 *')

proof end;

theorem :: QUATERNI:57

for z1, z2 being Quaternion st (z1 * z2) *' = (z1 *') * (z2 *') holds
(Im2 z1) * (Im3 z2) = (Im3 z1) * (Im2 z2)

proof end;

theorem :: QUATERNI:58

for z being Quaternion st Im1 z = 0 & Im2 z = 0 & Im3 z = 0 holds
z *' = z

proof end;

theorem :: QUATERNI:59

for z being Quaternion st Rea z = 0 holds
z *' = - z

proof end;

theorem :: QUATERNI:60

for z being Quaternion holds
( Rea (z * (z *')) = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) & Im1 (z * (z *')) = 0 & Im2 (z * (z *')) = 0 & Im3 (z * (z *')) = 0 )

proof end;

theorem :: QUATERNI:61

for z being Quaternion holds
( Rea (z + (z *')) = 2 * (Rea z) & Im1 (z + (z *')) = 0 & Im2 (z + (z *')) = 0 & Im3 (z + (z *')) = 0 )

proof end;

theorem Th55: :: QUATERNI:62

for z being Quaternion holds - z = [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]

proof end;

theorem :: QUATERNI:63

for z1, z2 being Quaternion holds z1 - z2 = [*((Rea z1) - (Rea z2)),((Im1 z1) - (Im1 z2)),((Im2 z1) - (Im2 z2)),((Im3 z1) - (Im3 z2))*]

proof end;

theorem :: QUATERNI:64

for z being Quaternion holds
( Rea (z - (z *')) = 0 & Im1 (z - (z *')) = 2 * (Im1 z) & Im2 (z - (z *')) = 2 * (Im2 z) & Im3 (z - (z *')) = 2 * (Im3 z) )

proof end;

definition

let z be Quaternion;

func |.z.| -> Real equals :: QUATERNI:def 22
sqrt (((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2));

coherence
sqrt (((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)) is Real ;

end;

:: deftheorem defines |. QUATERNI:def 22 :
for z being Quaternion holds |.z.| = sqrt (((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2));

theorem Th58: :: QUATERNI:65

|.0q.| = 0

proof end;

theorem Th59: :: QUATERNI:66

for z being Quaternion st |.z.| = 0 holds
z = 0

proof end;

theorem Th60: :: QUATERNI:67

for z being Quaternion holds 0 <= |.z.|

proof end;

theorem :: QUATERNI:68

|.1q.| = 1

proof end;

theorem :: QUATERNI:69

|.<i>.| = 1 by Th23, SQUARE_1:18;

theorem :: QUATERNI:70

|.<j>.| = 1 by Th24, SQUARE_1:18;

theorem :: QUATERNI:71

|.<k>.| = 1 by Th24, SQUARE_1:18;

theorem Th65: :: QUATERNI:72

for z being Quaternion holds |.(- z).| = |.z.|

proof end;

theorem Th66: :: QUATERNI:73

for z being Quaternion holds |.(z *').| = |.z.|

proof end;

theorem Th67: :: QUATERNI:74

for a, b, c, d being Real holds (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) >= 0

proof end;

Lm26: for a, b, c, d being Real holds a ^2 <= (((a ^2) + (b ^2)) + (c ^2)) + (d ^2)

proof end;

Lm27: for a, b, c, d being Real holds c ^2 <= (((a ^2) + (b ^2)) + (c ^2)) + (d ^2)

proof end;

Lm28: for a, b, c, d being Real holds d ^2 <= (((a ^2) + (b ^2)) + (c ^2)) + (d ^2)

proof end;

Lm29: for a, b being Real st a >= b ^2 holds
sqrt a >= b

proof end;

Lm30: for a1, a2, a3, a4, a5, a6, b1, b2, b3, b4, b5, b6 being Real st a1 >= b1 & a2 >= b2 & a3 >= b3 & a4 >= b4 & a5 >= b5 & a6 >= b6 holds
((((a1 + a2) + a3) + a4) + a5) + a6 >= ((((b1 + b2) + b3) + b4) + b5) + b6

proof end;

Lm31: for a, b being Real st a >= 0 & b >= 0 & a ^2 >= b ^2 holds
a >= b

proof end;

Lm32: for m1, m2, m4, m3, n1, n2, n3, n4 being Real holds ((sqrt ((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2))) + (sqrt ((((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2)))) ^2 = ((((((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2)) + (n1 ^2)) + (n2 ^2)) + (n3 ^2)) + (n4 ^2)) + (2 * (sqrt (((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2)) * ((((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2)))))

proof end;

Lm33: for m1, m2, m3, m4, n1, n2, n3, n4 being Real holds (sqrt (((((m1 + n1) ^2) + ((m2 + n2) ^2)) + ((m3 + n3) ^2)) + ((m4 + n4) ^2))) ^2 = ((((m1 + n1) ^2) + ((m2 + n2) ^2)) + ((m3 + n3) ^2)) + ((m4 + n4) ^2)

proof end;

theorem :: QUATERNI:75

for z being Quaternion holds Rea z <= |.z.|

proof end;

theorem :: QUATERNI:76

for z being Quaternion holds Im1 z <= |.z.|

proof end;

theorem :: QUATERNI:77

for z being Quaternion holds Im2 z <= |.z.|

proof end;

theorem :: QUATERNI:78

for z being Quaternion holds Im3 z <= |.z.|

proof end;

theorem Th72: :: QUATERNI:79

for z1, z2 being Quaternion holds |.(z1 + z2).| <= |.z1.| + |.z2.|

proof end;

theorem Th73: :: QUATERNI:80

for z1, z2 being Quaternion holds |.(z1 - z2).| <= |.z1.| + |.z2.|

proof end;

Lm34: for z1, z2 being Quaternion holds z1 = (z1 + z2) - z2

proof end;

Lm35: for z1, z2 being Quaternion holds z1 = (z1 - z2) + z2

proof end;

Lm36: for z1, z2 being Quaternion holds z1 - z2 = [*((Rea z1) - (Rea z2)),((Im1 z1) - (Im1 z2)),((Im2 z1) - (Im2 z2)),((Im3 z1) - (Im3 z2))*]

proof end;

Lm37: for z1, z2 being Quaternion holds z1 - z2 = - (z2 - z1)

proof end;

Lm38: for z1, z2 being Quaternion st z1 - z2 = 0 holds
z1 = z2

proof end;

theorem :: QUATERNI:81

for z1, z2 being Quaternion holds |.z1.| - |.z2.| <= |.(z1 + z2).|

proof end;

theorem Th75: :: QUATERNI:82

for z1, z2 being Quaternion holds |.z1.| - |.z2.| <= |.(z1 - z2).|

proof end;

theorem Th76: :: QUATERNI:83

for z1, z2 being Quaternion holds |.(z1 - z2).| = |.(z2 - z1).|

proof end;

theorem :: QUATERNI:84

for z1, z2 being Quaternion holds
( |.(z1 - z2).| = 0 iff z1 = z2 )

proof end;

Lm39: for z, z1, z2 being Quaternion holds z1 - z2 = (z1 - z) + (z - z2)

proof end;

theorem :: QUATERNI:85

for z, z1, z2 being Quaternion holds |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).|

proof end;

theorem :: QUATERNI:86

for z1, z2 being Quaternion holds |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).|

proof end;

theorem Th80: :: QUATERNI:87

for z1, z2 being Quaternion holds |.(z1 * z2).| = |.z1.| * |.z2.|

proof end;

theorem :: QUATERNI:88

for z being Quaternion holds |.(z * z).| = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)

proof end;

theorem :: QUATERNI:89

for z being Quaternion holds |.(z * z).| = |.(z * (z *')).|

proof end;

theorem :: QUATERNI:90

for z being Quaternion st z is real holds
( Rea z = z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) by Lm18;

theorem :: QUATERNI:91

for x, y being Element of REAL holds [*x,y,0,0*] = [*x,y*] by Lm3;

theorem :: QUATERNI:92

for z1, z2 being Quaternion holds z1 + z2 = ((((Rea z1) + (Rea z2)) + (((Im1 z1) + (Im1 z2)) * <i>)) + (((Im2 z1) + (Im2 z2)) * <j>)) + (((Im3 z1) + (Im3 z2)) * <k>) by Lm20;

theorem :: QUATERNI:93

for z1, z2 being Quaternion holds z1 * z2 = (((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) + ((((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))) * <i>)) + ((((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2))) * <j>)) + ((((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2))) * <k>) by Lm21;

theorem :: QUATERNI:94

for z being Quaternion holds - z = (((- (Rea z)) + ((- (Im1 z)) * <i>)) + ((- (Im2 z)) * <j>)) + ((- (Im3 z)) * <k>) by Lm24;

theorem :: QUATERNI:95

for z1, z2 being Quaternion holds z1 - z2 = ((((Rea z1) - (Rea z2)) + (((Im1 z1) - (Im1 z2)) * <i>)) + (((Im2 z1) - (Im2 z2)) * <j>)) + (((Im3 z1) - (Im3 z2)) * <k>) by Lm25;

theorem :: QUATERNI:96

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

theorem :: QUATERNI:97

for z1, z2 being Quaternion holds
( Rea (z1 * z2) = ((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2)) & Im1 (z1 * z2) = ((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)) & Im2 (z1 * z2) = ((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2)) & Im3 (z1 * z2) = ((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2)) ) by Lm17;