:: by Xiquan Liang and Fuguo Ge

::

:: Received November 14, 2006

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

definition

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

end;

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;

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

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

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

definition
end;

:: deftheorem Def2 defines quaternion QUATERNI:def 2 :

for x being Number holds

( x is quaternion iff x in QUATERNION );

for x being Number holds

( x is quaternion iff x in QUATERNION );

registration
end;

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

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

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

definition
end;

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

Lm2: <i> = [*zz,jj*]

by ARYTM_0:def 5;

registration

coherence

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

coherence

<j> is quaternion

<k> is quaternion

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

coherence

<j> is quaternion

proof end;

coherence <k> is quaternion

proof end;

definition

let x, y, w, z be Real;

for b_{1} being Element of QUATERNION holds verum
;

existence

( ( w = 0 & z = 0 implies ex b_{1} being Element of QUATERNION ex x9, y9 being Element of REAL st

( x9 = x & y9 = y & b_{1} = [*x9,y9*] ) ) & ( ( not w = 0 or not z = 0 ) implies ex b_{1} being Element of QUATERNION st b_{1} = (0,1,2,3) --> (x,y,w,z) ) )

for b_{1}, b_{2} being Element of QUATERNION holds

( ( w = 0 & z = 0 & ex x9, y9 being Element of REAL st

( x9 = x & y9 = y & b_{1} = [*x9,y9*] ) & ex x9, y9 being Element of REAL st

( x9 = x & y9 = y & b_{2} = [*x9,y9*] ) implies b_{1} = b_{2} ) & ( ( not w = 0 or not z = 0 ) & b_{1} = (0,1,2,3) --> (x,y,w,z) & b_{2} = (0,1,2,3) --> (x,y,w,z) implies b_{1} = b_{2} ) )
;

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

for b

existence

( ( w = 0 & z = 0 implies ex b

( x9 = x & y9 = y & b

proof end;

uniqueness for b

( ( w = 0 & z = 0 & ex x9, y9 being Element of REAL st

( x9 = x & y9 = y & b

( x9 = x & y9 = y & b

:: deftheorem Def5 defines [* QUATERNI:def 5 :

for x, y, w, z being Real

for b_{5} being Element of QUATERNION holds

( ( w = 0 & z = 0 implies ( b_{5} = [*x,y,w,z*] iff ex x9, y9 being Element of REAL st

( x9 = x & y9 = y & b_{5} = [*x9,y9*] ) ) ) & ( ( not w = 0 or not z = 0 ) implies ( b_{5} = [*x,y,w,z*] iff b_{5} = (0,1,2,3) --> (x,y,w,z) ) ) );

for x, y, w, z being Real

for b

( ( w = 0 & z = 0 implies ( b

( x9 = x & y9 = y & b

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

proof end;

::$CT

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 )

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

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

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

ex b_{1} 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_{1} = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] )

for b_{1}, b_{2} 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_{1} = [*(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_{2} = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) holds

b_{1} = b_{2}

for b_{1} 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_{1} = [*(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_{1} = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] )
;

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

ex b

( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b

proof end;

uniqueness for b

( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b

( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b

b

proof end;

commutativity for b

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

ex x1, x2, x3, x4, y1, y2, y3, y4 being Real st

( y = [*x1,x2,x3,x4*] & x = [*y1,y2,y3,y4*] & b

:: deftheorem Def6 defines + QUATERNI:def 6 :

for x, y being Quaternion

for b_{3} being Number holds

( b_{3} = 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_{3} = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) );

for x, y being Quaternion

for b

( b

( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b

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;

existence

ex b_{1} being Quaternion st z + b_{1} = 0

for b_{1}, b_{2} being Quaternion st z + b_{1} = 0 & z + b_{2} = 0 holds

b_{1} = b_{2}

for b_{1}, b_{2} being Quaternion st b_{2} + b_{1} = 0 holds

b_{1} + b_{2} = 0
;

end;
consider v, w, x, y being Real such that

A1: z = [*v,w,x,y*] by Th2;

existence

ex b

proof end;

uniqueness for b

b

proof end;

involutiveness for b

b

:: deftheorem Def7 defines - QUATERNI:def 7 :

for z, b_{2} being Quaternion holds

( b_{2} = - z iff z + b_{2} = 0 );

for z, b

( b

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;

ex b_{1} 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_{1} = [*((((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))*] )

for b_{1}, b_{2} 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_{1} = [*((((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_{2} = [*((((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_{1} = b_{2}

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

ex b

( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b

proof end;

uniqueness for b

( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b

( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b

b

proof end;

:: deftheorem Def9 defines * QUATERNI:def 9 :

for x, y being Quaternion

for b_{3} being Number holds

( b_{3} = 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_{3} = [*((((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))*] ) );

for x, y being Quaternion

for b

( b

( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b

registration

let z, z9 be Quaternion;

coherence

z + z9 is quaternion

z * z9 is quaternion

end;
coherence

z + z9 is quaternion

proof end;

coherence z * z9 is quaternion

proof end;

definition

coherence

<j> is Element of QUATERNION by Def2;

compatibility

for b_{1} being Element of QUATERNION holds

( b_{1} = <j> iff b_{1} = [*0,0,1,0*] )
by Def5;

coherence

<k> is Element of QUATERNION by Def2;

compatibility

for b_{1} being Element of QUATERNION holds

( b_{1} = <k> iff b_{1} = [*0,0,0,1*] )
by Def5;

end;
<j> is Element of QUATERNION by Def2;

compatibility

for b

( b

coherence

<k> is Element of QUATERNION by Def2;

compatibility

for b

( b

definition

let z be Quaternion;

( ( z in COMPLEX implies ex b_{1} being Number ex z9 being Complex st

( z = z9 & b_{1} = Re z9 ) ) & ( not z in COMPLEX implies ex b_{1} being Number ex f being Function of 4,REAL st

( z = f & b_{1} = f . 0 ) ) )

for b_{1}, b_{2} being Number holds

( ( z in COMPLEX & ex z9 being Complex st

( z = z9 & b_{1} = Re z9 ) & ex z9 being Complex st

( z = z9 & b_{2} = Re z9 ) implies b_{1} = b_{2} ) & ( not z in COMPLEX & ex f being Function of 4,REAL st

( z = f & b_{1} = f . 0 ) & ex f being Function of 4,REAL st

( z = f & b_{2} = f . 0 ) implies b_{1} = b_{2} ) )
;

consistency

for b_{1} being Number holds verum
;

( ( z in COMPLEX implies ex b_{1} being Number ex z9 being Complex st

( z = z9 & b_{1} = Im z9 ) ) & ( not z in COMPLEX implies ex b_{1} being Number ex f being Function of 4,REAL st

( z = f & b_{1} = f . 1 ) ) )

for b_{1}, b_{2} being Number holds

( ( z in COMPLEX & ex z9 being Complex st

( z = z9 & b_{1} = Im z9 ) & ex z9 being Complex st

( z = z9 & b_{2} = Im z9 ) implies b_{1} = b_{2} ) & ( not z in COMPLEX & ex f being Function of 4,REAL st

( z = f & b_{1} = f . 1 ) & ex f being Function of 4,REAL st

( z = f & b_{2} = f . 1 ) implies b_{1} = b_{2} ) )
;

consistency

for b_{1} being Number holds verum
;

( ( z in COMPLEX implies ex b_{1} being Number st b_{1} = 0 ) & ( not z in COMPLEX implies ex b_{1} being Number ex f being Function of 4,REAL st

( z = f & b_{1} = f . 2 ) ) )

for b_{1}, b_{2} being Number holds

( ( z in COMPLEX & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) & ( not z in COMPLEX & ex f being Function of 4,REAL st

( z = f & b_{1} = f . 2 ) & ex f being Function of 4,REAL st

( z = f & b_{2} = f . 2 ) implies b_{1} = b_{2} ) )
;

consistency

for b_{1} being Number holds verum
;

( ( z in COMPLEX implies ex b_{1} being Number st b_{1} = 0 ) & ( not z in COMPLEX implies ex b_{1} being Number ex f being Function of 4,REAL st

( z = f & b_{1} = f . 3 ) ) )

for b_{1}, b_{2} being Number holds

( ( z in COMPLEX & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) & ( not z in COMPLEX & ex f being Function of 4,REAL st

( z = f & b_{1} = f . 3 ) & ex f being Function of 4,REAL st

( z = f & b_{2} = f . 3 ) implies b_{1} = b_{2} ) )
;

consistency

for b_{1} being Number holds verum
;

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

( ( z in COMPLEX implies ex b

( z = z9 & b

( z = f & b

proof end;

uniqueness for b

( ( z in COMPLEX & ex z9 being Complex st

( z = z9 & b

( z = z9 & b

( z = f & b

( z = f & b

consistency

for b

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

( ( z in COMPLEX implies ex b

( z = z9 & b

( z = f & b

proof end;

uniqueness for b

( ( z in COMPLEX & ex z9 being Complex st

( z = z9 & b

( z = z9 & b

( z = f & b

( z = f & b

consistency

for b

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 it = 0 if z in COMPLEX

otherwise ex f being Function of 4,REAL st

( z = f & it = f . 2 );

( ( z in COMPLEX implies ex b

( z = f & b

proof end;

uniqueness for b

( ( z in COMPLEX & b

( z = f & b

( z = f & b

consistency

for b

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 it = 0 if z in COMPLEX

otherwise ex f being Function of 4,REAL st

( z = f & it = f . 3 );

( ( z in COMPLEX implies ex b

( z = f & b

proof end;

uniqueness for b

( ( z in COMPLEX & b

( z = f & b

( z = f & b

consistency

for b

:: deftheorem Def12 defines Rea QUATERNI:def 12 :

for z being Quaternion

for b_{2} being Number holds

( ( z in COMPLEX implies ( b_{2} = Rea z iff ex z9 being Complex st

( z = z9 & b_{2} = Re z9 ) ) ) & ( not z in COMPLEX implies ( b_{2} = Rea z iff ex f being Function of 4,REAL st

( z = f & b_{2} = f . 0 ) ) ) );

for z being Quaternion

for b

( ( z in COMPLEX implies ( b

( z = z9 & b

( z = f & b

:: deftheorem Def13 defines Im1 QUATERNI:def 13 :

for z being Quaternion

for b_{2} being Number holds

( ( z in COMPLEX implies ( b_{2} = Im1 z iff ex z9 being Complex st

( z = z9 & b_{2} = Im z9 ) ) ) & ( not z in COMPLEX implies ( b_{2} = Im1 z iff ex f being Function of 4,REAL st

( z = f & b_{2} = f . 1 ) ) ) );

for z being Quaternion

for b

( ( z in COMPLEX implies ( b

( z = z9 & b

( z = f & b

:: deftheorem Def14 defines Im2 QUATERNI:def 14 :

for z being Quaternion

for b_{2} being Number holds

( ( z in COMPLEX implies ( b_{2} = Im2 z iff b_{2} = 0 ) ) & ( not z in COMPLEX implies ( b_{2} = Im2 z iff ex f being Function of 4,REAL st

( z = f & b_{2} = f . 2 ) ) ) );

for z being Quaternion

for b

( ( z in COMPLEX implies ( b

( z = f & b

:: deftheorem Def15 defines Im3 QUATERNI:def 15 :

for z being Quaternion

for b_{2} being Number holds

( ( z in COMPLEX implies ( b_{2} = Im3 z iff b_{2} = 0 ) ) & ( not z in COMPLEX implies ( b_{2} = Im3 z iff ex f being Function of 4,REAL st

( z = f & b_{2} = f . 3 ) ) ) );

for z being Quaternion

for b

( ( z in COMPLEX implies ( b

( z = f & b

registration

let z be Quaternion;

coherence

Rea z is real

Im1 z is real

Im2 z is real

Im3 z is real

end;
coherence

Rea z is real

proof end;

coherence Im1 z is real

proof end;

coherence Im2 z is real

proof end;

coherence Im3 z is real

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 )

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

z1 = z2

proof end;

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 :: QUATERNI:27

for z being Quaternion st z = 0 holds

((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) = 0

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

z = 0q

proof end;

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

proof end;

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

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

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 )

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 )

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;

ex b_{1} being Number ex y1, y2, y3, y4 being Real st

( y = [*y1,y2,y3,y4*] & b_{1} = [*(x + y1),y2,y3,y4*] )

for b_{1}, b_{2} being Number st ex y1, y2, y3, y4 being Real st

( y = [*y1,y2,y3,y4*] & b_{1} = [*(x + y1),y2,y3,y4*] ) & ex y1, y2, y3, y4 being Real st

( y = [*y1,y2,y3,y4*] & b_{2} = [*(x + y1),y2,y3,y4*] ) holds

b_{1} = b_{2}

end;
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 y1, y2, y3, y4 being Real st

( y = [*y1,y2,y3,y4*] & it = [*(x + y1),y2,y3,y4*] );

ex b

( y = [*y1,y2,y3,y4*] & b

proof end;

uniqueness for b

( y = [*y1,y2,y3,y4*] & b

( y = [*y1,y2,y3,y4*] & b

b

proof end;

:: deftheorem Def18 defines + QUATERNI:def 18 :

for x being Real

for y being Quaternion

for b_{3} being Number holds

( b_{3} = x + y iff ex y1, y2, y3, y4 being Real st

( y = [*y1,y2,y3,y4*] & b_{3} = [*(x + y1),y2,y3,y4*] ) );

for x being Real

for y being Quaternion

for b

( b

( y = [*y1,y2,y3,y4*] & b

:: deftheorem defines - QUATERNI:def 19 :

for x being Real

for y being Quaternion holds x - y = x + (- y);

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;

ex b_{1} being Number ex y1, y2, y3, y4 being Real st

( y = [*y1,y2,y3,y4*] & b_{1} = [*(x * y1),(x * y2),(x * y3),(x * y4)*] )

for b_{1}, b_{2} being Number st ex y1, y2, y3, y4 being Real st

( y = [*y1,y2,y3,y4*] & b_{1} = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) & ex y1, y2, y3, y4 being Real st

( y = [*y1,y2,y3,y4*] & b_{2} = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) holds

b_{1} = b_{2}

end;
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 y1, y2, y3, y4 being Real st

( y = [*y1,y2,y3,y4*] & it = [*(x * y1),(x * y2),(x * y3),(x * y4)*] );

ex b

( y = [*y1,y2,y3,y4*] & b

proof end;

uniqueness for b

( y = [*y1,y2,y3,y4*] & b

( y = [*y1,y2,y3,y4*] & b

b

proof end;

:: deftheorem Def20 defines * QUATERNI:def 20 :

for x being Real

for y being Quaternion

for b_{3} being Number holds

( b_{3} = x * y iff ex y1, y2, y3, y4 being Real st

( y = [*y1,y2,y3,y4*] & b_{3} = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) );

for x being Real

for y being Quaternion

for b

( b

( y = [*y1,y2,y3,y4*] & b

registration

let x be Real;

let z9 be Quaternion;

coherence

x + z9 is quaternion

x * z9 is quaternion

x - z9 is quaternion ;

end;
let z9 be Quaternion;

coherence

x + z9 is quaternion

proof end;

coherence x * z9 is quaternion

proof end;

coherence x - z9 is quaternion ;

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;
:: original: +

redefine func z1 + z2 -> Element of QUATERNION ;

coherence

z1 + z2 is Element of QUATERNION by Def2;

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

( 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;
:: original: *

redefine func z1 * z2 -> Element of QUATERNION ;

coherence

z1 * z2 is Element of QUATERNION by Def2;

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;

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

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

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

( 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;
:: original: -

redefine func - z -> Element of QUATERNION ;

coherence

- z is Element of QUATERNION by Def2;

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

( 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;
:: original: -

redefine func z1 - z2 -> Element of QUATERNION ;

coherence

z1 - z2 is Element of QUATERNION by Def2;

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

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

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

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

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

:: deftheorem defines *' QUATERNI:def 21 :

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

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;
:: original: *'

redefine func z *' -> Element of QUATERNION ;

coherence

z *' is Element of QUATERNION ;

theorem :: QUATERNI:44

for z being Quaternion holds

( Rea (z *') = Rea z & Im1 (z *') = - (Im1 z) & Im2 (z *') = - (Im2 z) & Im3 (z *') = - (Im3 z) )

( Rea (z *') = Rea z & Im1 (z *') = - (Im1 z) & Im2 (z *') = - (Im2 z) & Im3 (z *') = - (Im3 z) )

proof end;

theorem :: QUATERNI:57

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

(Im2 z1) * (Im3 z2) = (Im3 z1) * (Im2 z2)

(Im2 z1) * (Im3 z2) = (Im3 z1) * (Im2 z2)

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 )

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

( Rea (z + (z *')) = 2 * (Rea z) & Im1 (z + (z *')) = 0 & Im2 (z + (z *')) = 0 & Im3 (z + (z *')) = 0 )

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

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

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

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

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

:: deftheorem defines |. QUATERNI:def 22 :

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

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

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;

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;

Lm39: for z, z1, z2 being Quaternion holds z1 - z2 = (z1 - z) + (z - 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:90

theorem :: QUATERNI:92

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

theorem :: QUATERNI:95

theorem :: QUATERNI:96

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;

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