begin
:: deftheorem defines QUATERNION QUATERNI:def 1 :
:: deftheorem Def2 defines quaternion QUATERNI:def 2 :
definition
let x,
y,
w,
z,
a,
b,
c,
d be
set ;
func x,
y,
w,
z --> a,
b,
c,
d -> set equals
(x,y --> a,b) +* (w,z --> c,d);
coherence
(x,y --> a,b) +* (w,z --> c,d) is set
;
end;
:: deftheorem defines --> QUATERNI:def 3 :
for
x,
y,
w,
z,
a,
b,
c,
d being
set holds
x,
y,
w,
z --> a,
b,
c,
d = (x,y --> a,b) +* (w,z --> c,d);
registration
let x,
y,
w,
z,
a,
b,
c,
d be
set ;
cluster x,
y,
w,
z --> a,
b,
c,
d -> Relation-like Function-like ;
coherence
( x,y,w,z --> a,b,c,d is Function-like & x,y,w,z --> a,b,c,d is Relation-like )
;
end;
theorem Th1:
for
x,
y,
w,
z,
a,
b,
c,
d being
set holds
dom (x,y,w,z --> a,b,c,d) = {x,y,w,z}
theorem Th2:
for
x,
y,
w,
z,
a,
b,
c,
d being
set holds
rng (x,y,w,z --> a,b,c,d) c= {a,b,c,d}
Lm1:
0 ,1,2,3 are_mutually_different
by ZFMISC_1:def 6;
theorem Th3:
for
x,
y,
w,
z,
a,
b,
c,
d being
set st
x,
y,
w,
z are_mutually_different holds
(
(x,y,w,z --> a,b,c,d) . x = a &
(x,y,w,z --> a,b,c,d) . y = b &
(x,y,w,z --> a,b,c,d) . w = c &
(x,y,w,z --> a,b,c,d) . z = d )
Lm2:
for x, y, w, z, a, b, c, d being set st x,y,w,z are_mutually_different holds
{a,b,c,d} c= rng (x,y,w,z --> a,b,c,d)
theorem
for
x,
y,
w,
z,
a,
b,
c,
d being
set st
x,
y,
w,
z are_mutually_different holds
rng (x,y,w,z --> a,b,c,d) = {a,b,c,d}
theorem
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 ) )
definition
let A be non
empty set ;
let x,
y,
w,
z be
set ;
let a,
b,
c,
d be
Element of
A;
-->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;
definition
func <j> -> set equals
0 ,1,2,3
--> 0 ,
0 ,1,
0 ;
coherence
0 ,1,2,3 --> 0 ,0 ,1,0 is set
;
func <k> -> set equals
0 ,1,2,3
--> 0 ,
0 ,
0 ,1;
coherence
0 ,1,2,3 --> 0 ,0 ,0 ,1 is set
;
end;
:: deftheorem defines <j> QUATERNI:def 4 :
:: deftheorem defines <k> QUATERNI:def 5 :
Lm3:
<i> = [*0 ,1*]
by ARYTM_0:def 7;
definition
let x,
y,
w,
z be
real number ;
func [*x,y,w,z*] -> Element of
QUATERNION means :
Def6:
ex
x',
y' being
Element of
REAL st
(
x' = x &
y' = y &
it = [*x',y'*] )
if (
w = 0 &
z = 0 )
otherwise it = 0 ,1,2,3
--> x,
y,
w,
z;
consistency
for b1 being Element of QUATERNION holds verum
;
existence
( ( w = 0 & z = 0 implies ex b1 being Element of QUATERNION ex x', y' being Element of REAL st
( x' = x & y' = y & b1 = [*x',y'*] ) ) & ( ( not w = 0 or not z = 0 ) implies ex b1 being Element of QUATERNION st b1 = 0 ,1,2,3 --> x,y,w,z ) )
uniqueness
for b1, b2 being Element of QUATERNION holds
( ( w = 0 & z = 0 & ex x', y' being Element of REAL st
( x' = x & y' = y & b1 = [*x',y'*] ) & ex x', y' being Element of REAL st
( x' = x & y' = y & b2 = [*x',y'*] ) implies b1 = b2 ) & ( ( not w = 0 or not z = 0 ) & b1 = 0 ,1,2,3 --> x,y,w,z & b2 = 0 ,1,2,3 --> x,y,w,z implies b1 = b2 ) )
;
end;
:: deftheorem Def6 defines [* QUATERNI:def 6 :
for
x,
y,
w,
z being
real number for
b5 being
Element of
QUATERNION holds
( (
w = 0 &
z = 0 implies (
b5 = [*x,y,w,z*] iff ex
x',
y' being
Element of
REAL st
(
x' = x &
y' = y &
b5 = [*x',y'*] ) ) ) & ( ( not
w = 0 or not
z = 0 ) implies (
b5 = [*x,y,w,z*] iff
b5 = 0 ,1,2,3
--> x,
y,
w,
z ) ) );
Lm4:
for x, y being Element of REAL holds [*x,y,0 ,0 *] = [*x,y*]
theorem Th6:
for
a,
b,
c,
d,
e,
i,
j,
k being
set for
g being
Function st
a <> b &
c <> d &
dom g = {a,b,c,d} &
g . a = e &
g . b = i &
g . c = j &
g . d = k holds
g = a,
b,
c,
d --> e,
i,
j,
k
theorem Th7:
theorem Th8:
for
a,
c,
x,
w,
b,
d,
y,
z being
set st
a,
c,
x,
w are_mutually_different holds
a,
c,
x,
w --> b,
d,
y,
z = {[a,b],[c,d],[x,y],[w,z]}
Lm5:
for x, y, z being set st [x,y] = {z} holds
( z = {x} & x = y )
theorem Th9:
Lm6:
for a, b, c, d being Element of REAL holds not 0 ,1,2,3 --> a,b,c,d in REAL
theorem Th10:
theorem Th11:
for
a,
b,
c,
d,
x,
y,
z,
w,
x',
y',
z',
w' being
set st
a,
b,
c,
d are_mutually_different &
a,
b,
c,
d --> x,
y,
z,
w = a,
b,
c,
d --> x',
y',
z',
w' holds
(
x = x' &
y = y' &
z = z' &
w = w' )
theorem Th12:
for
x1,
x2,
x3,
x4,
y1,
y2,
y3,
y4 being
Element of
REAL st
[*x1,x2,x3,x4*] = [*y1,y2,y3,y4*] holds
(
x1 = y1 &
x2 = y2 &
x3 = y3 &
x4 = y4 )
definition
let x,
y be
quaternion number ;
x in QUATERNION
by Def2;
then consider x1,
x2,
x3,
x4 being
Element of
REAL such that A1:
x = [*x1,x2,x3,x4*]
by Th7;
y in QUATERNION
by Def2;
then consider y1,
y2,
y3,
y4 being
Element of
REAL such that A2:
y = [*y1,y2,y3,y4*]
by Th7;
func x + y -> set means :
Def7:
ex
x1,
x2,
x3,
x4,
y1,
y2,
y3,
y4 being
Element of
REAL st
(
x = [*x1,x2,x3,x4*] &
y = [*y1,y2,y3,y4*] &
it = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] );
existence
ex b1 being set ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b1 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] )
uniqueness
for b1, b2 being set st ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b1 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) & ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b2 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) holds
b1 = b2
commutativity
for b1 being set
for x, y being quaternion number st ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b1 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) holds
ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( y = [*x1,x2,x3,x4*] & x = [*y1,y2,y3,y4*] & b1 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] )
;
end;
:: deftheorem Def7 defines + QUATERNI:def 7 :
for
x,
y being
quaternion number for
b3 being
set holds
(
b3 = x + y iff ex
x1,
x2,
x3,
x4,
y1,
y2,
y3,
y4 being
Element of
REAL st
(
x = [*x1,x2,x3,x4*] &
y = [*y1,y2,y3,y4*] &
b3 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) );
Lm7:
0 = [*0 ,0 ,0 ,0 *]
:: deftheorem Def8 defines - QUATERNI:def 8 :
:: deftheorem defines - QUATERNI:def 9 :
definition
let x,
y be
quaternion number ;
x in QUATERNION
by Def2;
then consider x1,
x2,
x3,
x4 being
Element of
REAL such that A1:
x = [*x1,x2,x3,x4*]
by Th7;
y in QUATERNION
by Def2;
then consider y1,
y2,
y3,
y4 being
Element of
REAL such that A2:
y = [*y1,y2,y3,y4*]
by Th7;
func x * y -> set means :
Def10:
ex
x1,
x2,
x3,
x4,
y1,
y2,
y3,
y4 being
Element of
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 b1 being set ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b1 = [*((((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))*] )
uniqueness
for b1, b2 being set st ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b1 = [*((((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 Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b2 = [*((((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
b1 = b2
end;
:: deftheorem Def10 defines * QUATERNI:def 10 :
for
x,
y being
quaternion number for
b3 being
set holds
(
b3 = x * y iff ex
x1,
x2,
x3,
x4,
y1,
y2,
y3,
y4 being
Element of
REAL st
(
x = [*x1,x2,x3,x4*] &
y = [*y1,y2,y3,y4*] &
b3 = [*((((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))*] ) );
definition
<j>redefine func <j> -> Element of
QUATERNION equals
[*0 ,0 ,1,0 *];
coherence
<j> is Element of QUATERNION
by Def2;
compatibility
for b1 being Element of QUATERNION holds
( b1 = <j> iff b1 = [*0 ,0 ,1,0 *] )
by Def6;
<k>redefine func <k> -> Element of
QUATERNION equals
[*0 ,0 ,0 ,1*];
coherence
<k> is Element of QUATERNION
by Def2;
compatibility
for b1 being Element of QUATERNION holds
( b1 = <k> iff b1 = [*0 ,0 ,0 ,1*] )
by Def6;
end;
:: deftheorem defines <j> QUATERNI:def 11 :
:: deftheorem defines <k> QUATERNI:def 12 :
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
definition
let z be
quaternion number ;
func Rea z -> set means :
Def13:
ex
z' being
complex number st
(
z = z' &
it = Re z' )
if z in COMPLEX otherwise ex
f being
Function of 4,
REAL st
(
z = f &
it = f . 0 );
existence
( ( z in COMPLEX implies ex b1 being set ex z' being complex number st
( z = z' & b1 = Re z' ) ) & ( not z in COMPLEX implies ex b1 being set ex f being Function of 4, REAL st
( z = f & b1 = f . 0 ) ) )
uniqueness
for b1, b2 being set holds
( ( z in COMPLEX & ex z' being complex number st
( z = z' & b1 = Re z' ) & ex z' being complex number st
( z = z' & b2 = Re z' ) implies b1 = b2 ) & ( not z in COMPLEX & ex f being Function of 4, REAL st
( z = f & b1 = f . 0 ) & ex f being Function of 4, REAL st
( z = f & b2 = f . 0 ) implies b1 = b2 ) )
;
consistency
for b1 being set holds verum
;
func Im1 z -> set means :
Def14:
ex
z' being
complex number st
(
z = z' &
it = Im z' )
if z in COMPLEX otherwise ex
f being
Function of 4,
REAL st
(
z = f &
it = f . 1 );
existence
( ( z in COMPLEX implies ex b1 being set ex z' being complex number st
( z = z' & b1 = Im z' ) ) & ( not z in COMPLEX implies ex b1 being set ex f being Function of 4, REAL st
( z = f & b1 = f . 1 ) ) )
uniqueness
for b1, b2 being set holds
( ( z in COMPLEX & ex z' being complex number st
( z = z' & b1 = Im z' ) & ex z' being complex number st
( z = z' & b2 = Im z' ) implies b1 = b2 ) & ( not z in COMPLEX & ex f being Function of 4, REAL st
( z = f & b1 = f . 1 ) & ex f being Function of 4, REAL st
( z = f & b2 = f . 1 ) implies b1 = b2 ) )
;
consistency
for b1 being set holds verum
;
func Im2 z -> set means :
Def15:
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 b1 being set st b1 = 0 ) & ( not z in COMPLEX implies ex b1 being set ex f being Function of 4, REAL st
( z = f & b1 = f . 2 ) ) )
uniqueness
for b1, b2 being set holds
( ( z in COMPLEX & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( not z in COMPLEX & ex f being Function of 4, REAL st
( z = f & b1 = f . 2 ) & ex f being Function of 4, REAL st
( z = f & b2 = f . 2 ) implies b1 = b2 ) )
;
consistency
for b1 being set holds verum
;
func Im3 z -> set means :
Def16:
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 b1 being set st b1 = 0 ) & ( not z in COMPLEX implies ex b1 being set ex f being Function of 4, REAL st
( z = f & b1 = f . 3 ) ) )
uniqueness
for b1, b2 being set holds
( ( z in COMPLEX & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( not z in COMPLEX & ex f being Function of 4, REAL st
( z = f & b1 = f . 3 ) & ex f being Function of 4, REAL st
( z = f & b2 = f . 3 ) implies b1 = b2 ) )
;
consistency
for b1 being set holds verum
;
end;
:: deftheorem Def13 defines Rea QUATERNI:def 13 :
:: deftheorem Def14 defines Im1 QUATERNI:def 14 :
:: deftheorem Def15 defines Im2 QUATERNI:def 15 :
:: deftheorem Def16 defines Im3 QUATERNI:def 16 :
theorem Th22:
for
f being
Function of 4,
REAL ex
a,
b,
c,
d being
Element of
REAL st
f = 0 ,1,2,3
--> a,
b,
c,
d
Lm8:
for a, b being Element of REAL holds
( Re [*a,b*] = a & Im [*a,b*] = b )
Lm9:
for z being complex number holds [*(Re z),(Im z)*] = z
theorem Th23:
for
a,
b,
c,
d being
Element of
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 )
theorem Th24:
theorem Th25:
:: deftheorem defines 0q QUATERNI:def 17 :
:: deftheorem defines 1q QUATERNI:def 18 :
Lm10:
for a, b, c, d being real number st (((a ^2 ) + (b ^2 )) + (c ^2 )) + (d ^2 ) = 0 holds
( a = 0 & b = 0 & c = 0 & d = 0 )
theorem Th26:
theorem
theorem
Lm11:
[*1,0 ,0 ,0 *] = 1
theorem
theorem Th30:
theorem Th31:
Lm12:
for m, n, x, y, z being quaternion number 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) )
Lm13:
for x, y, z being quaternion number 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) )
Lm14:
for z1, z2 being quaternion number holds z1 + z2 = [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*]
Lm15:
for x, y, z being quaternion number 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)) )
Lm16:
for z1, z2, z3, z4 being quaternion number 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))*]
Lm17:
for z1, z2 being quaternion number 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)))*]
Lm18:
for z1, z2 being quaternion number 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)) )
theorem
Lm19:
for z being quaternion number
for x being Real st z = x holds
( Rea z = x & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 )
theorem
theorem
theorem
definition
let x be
Real;
let y be
quaternion number ;
y in QUATERNION
by Def2;
then consider y1,
y2,
y3,
y4 being
Element of
REAL such that A1:
y = [*y1,y2,y3,y4*]
by Th7;
func x + y -> set means :
Def19:
ex
y1,
y2,
y3,
y4 being
Element of
REAL st
(
y = [*y1,y2,y3,y4*] &
it = [*(x + y1),y2,y3,y4*] );
existence
ex b1 being set ex y1, y2, y3, y4 being Element of REAL st
( y = [*y1,y2,y3,y4*] & b1 = [*(x + y1),y2,y3,y4*] )
uniqueness
for b1, b2 being set st ex y1, y2, y3, y4 being Element of REAL st
( y = [*y1,y2,y3,y4*] & b1 = [*(x + y1),y2,y3,y4*] ) & ex y1, y2, y3, y4 being Element of REAL st
( y = [*y1,y2,y3,y4*] & b2 = [*(x + y1),y2,y3,y4*] ) holds
b1 = b2
end;
:: deftheorem Def19 defines + QUATERNI:def 19 :
:: deftheorem defines - QUATERNI:def 20 :
definition
let x be
Real;
let y be
quaternion number ;
y in QUATERNION
by Def2;
then consider y1,
y2,
y3,
y4 being
Element of
REAL such that A1:
y = [*y1,y2,y3,y4*]
by Th7;
func x * y -> set means :
Def21:
ex
y1,
y2,
y3,
y4 being
Element of
REAL st
(
y = [*y1,y2,y3,y4*] &
it = [*(x * y1),(x * y2),(x * y3),(x * y4)*] );
existence
ex b1 being set ex y1, y2, y3, y4 being Element of REAL st
( y = [*y1,y2,y3,y4*] & b1 = [*(x * y1),(x * y2),(x * y3),(x * y4)*] )
uniqueness
for b1, b2 being set st ex y1, y2, y3, y4 being Element of REAL st
( y = [*y1,y2,y3,y4*] & b1 = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) & ex y1, y2, y3, y4 being Element of REAL st
( y = [*y1,y2,y3,y4*] & b2 = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) holds
b1 = b2
end;
:: deftheorem Def21 defines * QUATERNI:def 21 :
Lm20:
for x, y, z, w being Real holds [*x,y,z,w*] = ((x + (y * <i> )) + (z * <j> )) + (w * <k> )
:: deftheorem Def22 defines + QUATERNI:def 22 :
theorem
:: deftheorem defines * QUATERNI:def 23 :
theorem
theorem
theorem
theorem
:: deftheorem defines - QUATERNI:def 24 :
theorem Th41:
:: deftheorem defines - QUATERNI:def 25 :
theorem Th42:
:: deftheorem defines *' QUATERNI:def 26 :
theorem Th43:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
Lm21:
for z1, z2 being quaternion number 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) )
theorem
theorem Th55:
Lm22:
for z1, z2 being quaternion number 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) )
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th62:
theorem
theorem
:: deftheorem defines |. QUATERNI:def 27 :
theorem Th65:
theorem Th66:
theorem Th67:
theorem
theorem
theorem
theorem
theorem Th72:
theorem Th73:
Lm23:
for a, b, c, d being real number holds (((a ^2 ) + (b ^2 )) + (c ^2 )) + (d ^2 ) >= 0
theorem
Lm24:
for a, b, c, d being Element of REAL holds a ^2 <= (((a ^2 ) + (b ^2 )) + (c ^2 )) + (d ^2 )
Lm25:
for a, b, c, d being real number holds c ^2 <= (((a ^2 ) + (b ^2 )) + (c ^2 )) + (d ^2 )
Lm26:
for d, a, b, c being Element of REAL holds d ^2 <= (((a ^2 ) + (b ^2 )) + (c ^2 )) + (d ^2 )
theorem
theorem
theorem
theorem
Lm27:
for z1, z2 being quaternion number 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) )
Lm28:
for a, b being Element of REAL st a >= b ^2 holds
sqrt a >= b
Lm29:
for a1, a2, a3, a4, a5, a6, b1, b2, b3, b4, b5, b6 being real number 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
Lm30:
for a, b being Element of REAL st a >= 0 & b >= 0 & a ^2 >= b ^2 holds
a >= b
Lm31:
for m1, m2, m4, m3, n1, n2, n3, n4 being real number 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 )))))
Lm32:
for m1, m2, m3, m4, n1, n2, n3, n4 being real number 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 )
theorem Th79:
theorem Th80:
Lm33:
for z1, z2 being quaternion number holds z1 = (z1 + z2) - z2
Lm34:
for z1, z2 being quaternion number holds z1 = (z1 - z2) + z2
Lm35:
for z1, z2 being quaternion number holds z1 - z2 = [*((Rea z1) - (Rea z2)),((Im1 z1) - (Im1 z2)),((Im2 z1) - (Im2 z2)),((Im3 z1) - (Im3 z2))*]
Lm36:
for z1, z2 being quaternion number 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) )
Lm37:
for z1, z2 being quaternion number holds z1 - z2 = - (z2 - z1)
Lm38:
for z1, z2 being quaternion number st z1 - z2 = 0 holds
z1 = z2
theorem
theorem Th82:
theorem Th83:
theorem
Lm39:
for z, z1, z2 being quaternion number holds z1 - z2 = (z1 - z) + (z - z2)
theorem
theorem
theorem Th87:
theorem
theorem
theorem
theorem