:: The Quaternion Numbers :: by Xiquan Liang and Fuguo Ge :: :: Received November 14, 2006 :: Copyright (c) 2006-2012 Association of Mizar Users begin 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 ; attrx 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; definition let x, y, w, z, a, b, c, d be set ; func(x,y,w,z) --> (a,b,c,d) -> set equals :: QUATERNI:def 3 ((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: :: QUATERNI:1 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} proofend; theorem Th2: :: QUATERNI:2 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} proofend; Lm1: 0 ,1,2,3 are_mutually_different by ZFMISC_1:def_6; theorem Th3: :: QUATERNI:3 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 ) proofend; 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)) proofend; theorem :: QUATERNI:4 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} proofend; 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 ) ) proofend; 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 proofend; end; definition func -> set equals :: QUATERNI:def 4 (0,1,2,3) --> (0,0,1,0); coherence (0,1,2,3) --> (0,0,1,0) is set ; func -> set equals :: QUATERNI:def 5 (0,1,2,3) --> (0,0,0,1); coherence (0,1,2,3) --> (0,0,0,1) is set ; end; :: deftheorem defines QUATERNI:def_4_:_ = (0,1,2,3) --> (0,0,1,0); :: deftheorem defines QUATERNI:def_5_:_ = (0,1,2,3) --> (0,0,0,1); Lm3: = [*0,1*] by ARYTM_0:def_5; registration cluster -> quaternion ; coherence is quaternion proofend; cluster -> quaternion ; coherence is quaternion proofend; cluster -> quaternion ; coherence is quaternion proofend; end; registration cluster quaternion for set ; existence ex b1 being number st b1 is quaternion proofend; end; registration cluster -> quaternion for Element of QUATERNION ; coherence for b1 being Element of QUATERNION holds b1 is quaternion by Def2; end; definition let x, y, w, z be real number ; func[*x,y,w,z*] -> Element of QUATERNION means :Def6: :: QUATERNI:def 6 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 b1 being Element of QUATERNION holds verum ; existence ( ( w = 0 & z = 0 implies ex b1 being Element of QUATERNION ex x9, y9 being Element of REAL st ( x9 = x & y9 = y & b1 = [*x9,y9*] ) ) & ( ( not w = 0 or not z = 0 ) implies ex b1 being Element of QUATERNION st b1 = (0,1,2,3) --> (x,y,w,z) ) ) proofend; uniqueness for b1, b2 being Element of QUATERNION holds ( ( w = 0 & z = 0 & ex x9, y9 being Element of REAL st ( x9 = x & y9 = y & b1 = [*x9,y9*] ) & ex x9, y9 being Element of REAL st ( x9 = x & y9 = y & b2 = [*x9,y9*] ) 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 x9, y9 being Element of REAL st ( x9 = x & y9 = y & b5 = [*x9,y9*] ) ) ) & ( ( 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*] proofend; theorem Th6: :: QUATERNI:6 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) proofend; theorem Th7: :: QUATERNI:7 for g being quaternion number ex r, s, t, u being Element of REAL st g = [*r,s,t,u*] proofend; theorem Th8: :: QUATERNI:8 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]} proofend; Lm5: for x, y, z being set st [x,y] = {z} holds ( z = {x} & x = y ) proofend; theorem Th9: :: 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 ) proofend; Lm6: for a, b, c, d being Element of REAL holds not (0,1,2,3) --> (a,b,c,d) in REAL proofend; theorem Th10: :: QUATERNI:10 for a, b, c, d being Element of REAL holds not (0,1,2,3) --> (a,b,c,d) in COMPLEX proofend; theorem Th11: :: QUATERNI:11 for a, b, c, d, x, y, z, w, x9, y9, z9, w9 being set st a,b,c,d are_mutually_different & (a,b,c,d) --> (x,y,z,w) = (a,b,c,d) --> (x9,y9,z9,w9) holds ( x = x9 & y = y9 & z = z9 & w = w9 ) proofend; theorem Th12: :: QUATERNI:12 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 ) proofend; definition let x, y be quaternion number ; consider x1, x2, x3, x4 being Element of REAL such that A1: x = [*x1,x2,x3,x4*] by Th7; consider y1, y2, y3, y4 being Element of REAL such that A2: y = [*y1,y2,y3,y4*] by Th7; funcx + y -> set means :Def7: :: QUATERNI:def 7 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)*] ) proofend; 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 proofend; 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*] proofend; definition let z be quaternion number ; consider v, w, x, y being Element of REAL such that A1: z = [*v,w,x,y*] by Th7; func - z -> quaternion number means :Def8: :: QUATERNI:def 8 z + it = 0 ; existence ex b1 being quaternion number st z + b1 = 0 proofend; uniqueness for b1, b2 being quaternion number st z + b1 = 0 & z + b2 = 0 holds b1 = b2 proofend; involutiveness for b1, b2 being quaternion number st b2 + b1 = 0 holds b1 + b2 = 0 ; end; :: deftheorem Def8 defines - QUATERNI:def_8_:_ for z, b2 being quaternion number holds ( b2 = - z iff z + b2 = 0 ); definition let x, y be quaternion number ; funcx - y -> set equals :: QUATERNI:def 9 x + (- y); coherence x + (- y) is set ; end; :: deftheorem defines - QUATERNI:def_9_:_ for x, y being quaternion number holds x - y = x + (- y); definition let x, y be quaternion number ; consider x1, x2, x3, x4 being Element of REAL such that A1: x = [*x1,x2,x3,x4*] by Th7; consider y1, y2, y3, y4 being Element of REAL such that A2: y = [*y1,y2,y3,y4*] by Th7; funcx * y -> set means :Def10: :: QUATERNI:def 10 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))*] ) proofend; 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 proofend; 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))*] ) ); registration let z, z9 be quaternion number ; clusterz + z9 -> quaternion ; coherence z + z9 is quaternion proofend; clusterz * z9 -> quaternion ; coherence z * z9 is quaternion proofend; end; definition :: original: redefine func -> Element of QUATERNION equals :: QUATERNI:def 11 [*0,0,1,0*]; coherence is Element of QUATERNION by Def2; compatibility for b1 being Element of QUATERNION holds ( b1 = iff b1 = [*0,0,1,0*] ) by Def6; :: original: redefine func -> Element of QUATERNION equals :: QUATERNI:def 12 [*0,0,0,1*]; coherence is Element of QUATERNION by Def2; compatibility for b1 being Element of QUATERNION holds ( b1 = iff b1 = [*0,0,0,1*] ) by Def6; end; :: deftheorem defines QUATERNI:def_11_:_ = [*0,0,1,0*]; :: deftheorem defines QUATERNI:def_12_:_ = [*0,0,0,1*]; theorem :: QUATERNI:13 * = - 1 proofend; theorem :: QUATERNI:14 * = - 1 proofend; theorem :: QUATERNI:15 * = - 1 proofend; theorem :: QUATERNI:16 * = proofend; theorem :: QUATERNI:17 * = proofend; theorem :: QUATERNI:18 * = proofend; theorem :: QUATERNI:19 * = - ( * ) proofend; theorem :: QUATERNI:20 * = - ( * ) proofend; theorem :: QUATERNI:21 * = - ( * ) proofend; definition let z be quaternion number ; func Rea z -> set means :Def13: :: QUATERNI:def 13 ex z9 being complex number 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 b1 being set ex z9 being complex number st ( z = z9 & b1 = Re z9 ) ) & ( not z in COMPLEX implies ex b1 being set ex f being Function of 4,REAL st ( z = f & b1 = f . 0 ) ) ) proofend; uniqueness for b1, b2 being set holds ( ( z in COMPLEX & ex z9 being complex number st ( z = z9 & b1 = Re z9 ) & ex z9 being complex number st ( z = z9 & b2 = Re z9 ) 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: :: QUATERNI:def 14 ex z9 being complex number 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 b1 being set ex z9 being complex number st ( z = z9 & b1 = Im z9 ) ) & ( not z in COMPLEX implies ex b1 being set ex f being Function of 4,REAL st ( z = f & b1 = f . 1 ) ) ) proofend; uniqueness for b1, b2 being set holds ( ( z in COMPLEX & ex z9 being complex number st ( z = z9 & b1 = Im z9 ) & ex z9 being complex number st ( z = z9 & b2 = Im z9 ) 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: :: QUATERNI:def 15 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 ) ) ) proofend; 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: :: QUATERNI:def 16 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 ) ) ) proofend; 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_:_ for z being quaternion number for b2 being set holds ( ( z in COMPLEX implies ( b2 = Rea z iff ex z9 being complex number st ( z = z9 & b2 = Re z9 ) ) ) & ( not z in COMPLEX implies ( b2 = Rea z iff ex f being Function of 4,REAL st ( z = f & b2 = f . 0 ) ) ) ); :: deftheorem Def14 defines Im1 QUATERNI:def_14_:_ for z being quaternion number for b2 being set holds ( ( z in COMPLEX implies ( b2 = Im1 z iff ex z9 being complex number st ( z = z9 & b2 = Im z9 ) ) ) & ( not z in COMPLEX implies ( b2 = Im1 z iff ex f being Function of 4,REAL st ( z = f & b2 = f . 1 ) ) ) ); :: deftheorem Def15 defines Im2 QUATERNI:def_15_:_ for z being quaternion number for b2 being set holds ( ( z in COMPLEX implies ( b2 = Im2 z iff b2 = 0 ) ) & ( not z in COMPLEX implies ( b2 = Im2 z iff ex f being Function of 4,REAL st ( z = f & b2 = f . 2 ) ) ) ); :: deftheorem Def16 defines Im3 QUATERNI:def_16_:_ for z being quaternion number for b2 being set holds ( ( z in COMPLEX implies ( b2 = Im3 z iff b2 = 0 ) ) & ( not z in COMPLEX implies ( b2 = Im3 z iff ex f being Function of 4,REAL st ( z = f & b2 = f . 3 ) ) ) ); registration let z be quaternion number ; cluster Rea z -> real ; coherence Rea z is real proofend; cluster Im1 z -> real ; coherence Im1 z is real proofend; cluster Im2 z -> real ; coherence Im2 z is real proofend; cluster Im3 z -> real ; coherence Im3 z is real proofend; end; definition let z be quaternion number ; :: original:Rea redefine func Rea z -> Real; coherence Rea z is Real by XREAL_0:def_1; :: original:Im1 redefine func Im1 z -> Real; coherence Im1 z is Real by XREAL_0:def_1; :: original:Im2 redefine func Im2 z -> Real; coherence Im2 z is Real by XREAL_0:def_1; :: original:Im3 redefine func Im3 z -> Real; coherence Im3 z is Real by XREAL_0:def_1; end; theorem Th22: :: QUATERNI:22 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) proofend; Lm8: for a, b being Element of REAL holds ( Re [*a,b*] = a & Im [*a,b*] = b ) proofend; Lm9: for z being complex number holds [*(Re z),(Im z)*] = z proofend; theorem Th23: :: QUATERNI:23 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 ) proofend; theorem Th24: :: QUATERNI:24 for z being quaternion number holds z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*] proofend; theorem Th25: :: QUATERNI:25 for z1, z2 being quaternion number st Rea z1 = Rea z2 & Im1 z1 = Im1 z2 & Im2 z1 = Im2 z2 & Im3 z1 = Im3 z2 holds z1 = z2 proofend; definition func 0q -> quaternion number equals :: QUATERNI:def 17 0 ; coherence 0 is quaternion number by Lm7; func 1q -> quaternion number equals :: QUATERNI:def 18 1; coherence 1 is quaternion number proofend; end; :: deftheorem defines 0q QUATERNI:def_17_:_ 0q = 0 ; :: deftheorem defines 1q QUATERNI:def_18_:_ 1q = 1; 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 ) proofend; theorem Th26: :: QUATERNI:26 for z being quaternion number st Rea z = 0 & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 holds z = 0q proofend; theorem :: QUATERNI:27 for z being quaternion number st z = 0 holds ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) = 0 proofend; theorem :: QUATERNI:28 for z being quaternion number st ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) = 0 holds z = 0q proofend; Lm11: [*1,0,0,0*] = 1 proofend; theorem :: QUATERNI:29 ( Rea 1q = 1 & Im1 1q = 0 & Im2 1q = 0 & Im3 1q = 0 ) by Lm11, Th23; theorem Th30: :: QUATERNI:30 ( Rea = 0 & Im1 = 1 & Im2 = 0 & Im3 = 0 ) proofend; theorem Th31: :: QUATERNI:31 ( Rea = 0 & Im1 = 0 & Im2 = 1 & Im3 = 0 & Rea = 0 & Im1 = 0 & Im2 = 0 & Im3 = 1 ) by Th23; 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) ) proofend; 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) ) proofend; 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))*] proofend; 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)) ) proofend; 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))*] proofend; 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)))*] proofend; 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)) ) proofend; theorem :: QUATERNI:32 for z1, z2, z3, z4 being quaternion number 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) ) proofend; 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 ) proofend; theorem :: QUATERNI:33 for z1 being quaternion number for x being Real st z1 = x holds ( Rea (z1 * ) = 0 & Im1 (z1 * ) = x & Im2 (z1 * ) = 0 & Im3 (z1 * ) = 0 ) proofend; theorem :: QUATERNI:34 for z1 being quaternion number for x being Real st z1 = x holds ( Rea (z1 * ) = 0 & Im1 (z1 * ) = 0 & Im2 (z1 * ) = x & Im3 (z1 * ) = 0 ) proofend; theorem :: QUATERNI:35 for z1 being quaternion number for x being Real st z1 = x holds ( Rea (z1 * ) = 0 & Im1 (z1 * ) = 0 & Im2 (z1 * ) = 0 & Im3 (z1 * ) = x ) proofend; definition let x be Real; let y be quaternion number ; consider y1, y2, y3, y4 being Element of REAL such that A1: y = [*y1,y2,y3,y4*] by Th7; funcx + y -> set means :Def19: :: QUATERNI:def 19 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*] ) proofend; 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 proofend; end; :: deftheorem Def19 defines + QUATERNI:def_19_:_ for x being Real for y being quaternion number for b3 being set holds ( b3 = x + y iff ex y1, y2, y3, y4 being Element of REAL st ( y = [*y1,y2,y3,y4*] & b3 = [*(x + y1),y2,y3,y4*] ) ); definition let x be Real; let y be quaternion number ; funcx - y -> set equals :: QUATERNI:def 20 x + (- y); coherence x + (- y) is set ; end; :: deftheorem defines - QUATERNI:def_20_:_ for x being Real for y being quaternion number holds x - y = x + (- y); definition let x be Real; let y be quaternion number ; consider y1, y2, y3, y4 being Element of REAL such that A1: y = [*y1,y2,y3,y4*] by Th7; funcx * y -> set means :Def21: :: QUATERNI:def 21 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)*] ) proofend; 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 proofend; end; :: deftheorem Def21 defines * QUATERNI:def_21_:_ for x being Real for y being quaternion number for b3 being set holds ( b3 = x * y iff ex y1, y2, y3, y4 being Element of REAL st ( y = [*y1,y2,y3,y4*] & b3 = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) ); registration let x be Real; let z9 be quaternion number ; clusterx + z9 -> quaternion ; coherence x + z9 is quaternion proofend; clusterx * z9 -> quaternion ; coherence x * z9 is quaternion proofend; clusterx - z9 -> quaternion ; coherence x - z9 is quaternion ; end; Lm20: for x, y, z, w being Real holds [*x,y,z,w*] = ((x + (y * )) + (z * )) + (w * ) proofend; definition let z1, z2 be quaternion number ; :: original:+ redefine funcz1 + z2 -> Element of QUATERNION ; coherence z1 + z2 is Element of QUATERNION by Def2; end; Lm21: 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)) * ) proofend; theorem Th36: :: QUATERNI:36 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) ) proofend; definition let z1, z2 be quaternion number ; :: original:* redefine funcz1 * z2 -> Element of QUATERNION ; coherence z1 * z2 is Element of QUATERNION by Def2; end; Lm22: 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))) * ) proofend; theorem :: QUATERNI:37 for z being quaternion number holds z = (((Rea z) + ((Im1 z) * )) + ((Im2 z) * )) + ((Im3 z) * ) proofend; Lm23: for c being quaternion number holds c + 0q = c proofend; Lm24: ( 0 * = 0 & 0 * = 0 & 0 * = 0 ) proofend; theorem :: QUATERNI:38 for z1, z2 being quaternion number 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)) ) proofend; theorem :: QUATERNI:39 for z1, z2 being quaternion number 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)) ) proofend; theorem :: QUATERNI:40 for z being quaternion number 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)) ) proofend; definition let z be quaternion number ; :: original:- redefine func - z -> Element of QUATERNION ; coherence - z is Element of QUATERNION by Def2; end; Lm25: for z being quaternion number holds - z = (((- (Rea z)) + ((- (Im1 z)) * )) + ((- (Im2 z)) * )) + ((- (Im3 z)) * ) proofend; theorem Th41: :: QUATERNI:41 for z being quaternion number holds ( Rea (- z) = - (Rea z) & Im1 (- z) = - (Im1 z) & Im2 (- z) = - (Im2 z) & Im3 (- z) = - (Im3 z) ) proofend; definition let z1, z2 be quaternion number ; :: original:- redefine funcz1 - z2 -> Element of QUATERNION ; coherence z1 - z2 is Element of QUATERNION by Def2; end; Lm26: 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)) * ) proofend; theorem Th42: :: QUATERNI:42 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) ) proofend; definition let z be quaternion number ; funcz *' -> quaternion number equals :: QUATERNI:def 22 (((Rea z) + ((- (Im1 z)) * )) + ((- (Im2 z)) * )) + ((- (Im3 z)) * ); coherence (((Rea z) + ((- (Im1 z)) * )) + ((- (Im2 z)) * )) + ((- (Im3 z)) * ) is quaternion number ; end; :: deftheorem defines *' QUATERNI:def_22_:_ for z being quaternion number holds z *' = (((Rea z) + ((- (Im1 z)) * )) + ((- (Im2 z)) * )) + ((- (Im3 z)) * ); definition let z be quaternion number ; :: original:*' redefine funcz *' -> Element of QUATERNION ; coherence z *' is Element of QUATERNION ; end; theorem Th43: :: QUATERNI:43 for z being quaternion number holds z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] proofend; theorem :: QUATERNI:44 for z being quaternion number holds ( Rea (z *') = Rea z & Im1 (z *') = - (Im1 z) & Im2 (z *') = - (Im2 z) & Im3 (z *') = - (Im3 z) ) proofend; theorem :: QUATERNI:45 for z being quaternion number st z = 0 holds z *' = 0 proofend; theorem :: QUATERNI:46 for z being quaternion number st z *' = 0 holds z = 0 proofend; theorem :: QUATERNI:47 1q *' = 1q proofend; theorem :: QUATERNI:48 ( Rea ( *') = 0 & Im1 ( *') = - 1 & Im2 ( *') = 0 & Im3 ( *') = 0 ) proofend; theorem :: QUATERNI:49 ( Rea ( *') = 0 & Im1 ( *') = 0 & Im2 ( *') = - 1 & Im3 ( *') = 0 ) proofend; theorem :: QUATERNI:50 ( Rea ( *') = 0 & Im1 ( *') = 0 & Im2 ( *') = 0 & Im3 ( *') = - 1 ) proofend; theorem :: QUATERNI:51 *' = - by Th30, Lm25; theorem :: QUATERNI:52 *' = - by Th31, Lm25; theorem :: QUATERNI:53 *' = - by Th31, Lm25; theorem :: QUATERNI:54 for z1, z2 being quaternion number holds (z1 + z2) *' = (z1 *') + (z2 *') proofend; theorem Th55: :: QUATERNI:55 for z being quaternion number holds (- z) *' = - (z *') proofend; theorem :: QUATERNI:56 for z1, z2 being quaternion number holds (z1 - z2) *' = (z1 *') - (z2 *') proofend; theorem :: QUATERNI:57 for z1, z2 being quaternion number st (z1 * z2) *' = (z1 *') * (z2 *') holds (Im2 z1) * (Im3 z2) = (Im3 z1) * (Im2 z2) proofend; theorem :: QUATERNI:58 for z being quaternion number st Im1 z = 0 & Im2 z = 0 & Im3 z = 0 holds z *' = z proofend; theorem :: QUATERNI:59 for z being quaternion number st Rea z = 0 holds z *' = - z proofend; theorem :: QUATERNI:60 for z being quaternion number 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 ) proofend; theorem :: QUATERNI:61 for z being quaternion number holds ( Rea (z + (z *')) = 2 * (Rea z) & Im1 (z + (z *')) = 0 & Im2 (z + (z *')) = 0 & Im3 (z + (z *')) = 0 ) proofend; theorem Th62: :: QUATERNI:62 for z being quaternion number holds - z = [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] proofend; theorem :: QUATERNI:63 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))*] proofend; theorem :: QUATERNI:64 for z being quaternion number holds ( Rea (z - (z *')) = 0 & Im1 (z - (z *')) = 2 * (Im1 z) & Im2 (z - (z *')) = 2 * (Im2 z) & Im3 (z - (z *')) = 2 * (Im3 z) ) proofend; definition let z be quaternion number ; func|.z.| -> real number equals :: QUATERNI:def 23 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 number ; end; :: deftheorem defines |. QUATERNI:def_23_:_ for z being quaternion number holds |.z.| = sqrt (((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)); theorem Th65: :: QUATERNI:65 |.0q.| = 0 proofend; theorem Th66: :: QUATERNI:66 for z being quaternion number st |.z.| = 0 holds z = 0 proofend; theorem Th67: :: QUATERNI:67 for z being quaternion number holds 0 <= |.z.| proofend; theorem :: QUATERNI:68 |.1q.| = 1 proofend; theorem :: QUATERNI:69 |..| = 1 by Th30, SQUARE_1:18; theorem :: QUATERNI:70 |..| = 1 by Th31, SQUARE_1:18; theorem :: QUATERNI:71 |..| = 1 by Th31, SQUARE_1:18; theorem Th72: :: QUATERNI:72 for z being quaternion number holds |.(- z).| = |.z.| proofend; theorem Th73: :: QUATERNI:73 for z being quaternion number holds |.(z *').| = |.z.| proofend; theorem Th74: :: QUATERNI:74 for a, b, c, d being real number holds (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) >= 0 proofend; Lm27: for a, b, c, d being Element of REAL holds a ^2 <= (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) proofend; Lm28: for a, b, c, d being real number holds c ^2 <= (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) proofend; Lm29: for d, a, b, c being Element of REAL holds d ^2 <= (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) proofend; Lm30: for a, b being Element of REAL st a >= b ^2 holds sqrt a >= b proofend; Lm31: 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 proofend; Lm32: for a, b being Element of REAL st a >= 0 & b >= 0 & a ^2 >= b ^2 holds a >= b proofend; Lm33: 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))))) proofend; Lm34: 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) proofend; theorem :: QUATERNI:75 for z being quaternion number holds Rea z <= |.z.| proofend; theorem :: QUATERNI:76 for z being quaternion number holds Im1 z <= |.z.| proofend; theorem :: QUATERNI:77 for z being quaternion number holds Im2 z <= |.z.| proofend; theorem :: QUATERNI:78 for z being quaternion number holds Im3 z <= |.z.| proofend; theorem Th79: :: QUATERNI:79 for z1, z2 being quaternion number holds |.(z1 + z2).| <= |.z1.| + |.z2.| proofend; theorem Th80: :: QUATERNI:80 for z1, z2 being quaternion number holds |.(z1 - z2).| <= |.z1.| + |.z2.| proofend; Lm35: for z1, z2 being quaternion number holds z1 = (z1 + z2) - z2 proofend; Lm36: for z1, z2 being quaternion number holds z1 = (z1 - z2) + z2 proofend; Lm37: 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))*] proofend; Lm38: for z1, z2 being quaternion number holds z1 - z2 = - (z2 - z1) proofend; Lm39: for z1, z2 being quaternion number st z1 - z2 = 0 holds z1 = z2 proofend; theorem :: QUATERNI:81 for z1, z2 being quaternion number holds |.z1.| - |.z2.| <= |.(z1 + z2).| proofend; theorem Th82: :: QUATERNI:82 for z1, z2 being quaternion number holds |.z1.| - |.z2.| <= |.(z1 - z2).| proofend; theorem Th83: :: QUATERNI:83 for z1, z2 being quaternion number holds |.(z1 - z2).| = |.(z2 - z1).| proofend; theorem :: QUATERNI:84 for z1, z2 being quaternion number holds ( |.(z1 - z2).| = 0 iff z1 = z2 ) proofend; Lm40: for z, z1, z2 being quaternion number holds z1 - z2 = (z1 - z) + (z - z2) proofend; theorem :: QUATERNI:85 for z1, z2, z being quaternion number holds |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).| proofend; theorem :: QUATERNI:86 for z1, z2 being quaternion number holds |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).| proofend; theorem Th87: :: QUATERNI:87 for z1, z2 being quaternion number holds |.(z1 * z2).| = |.z1.| * |.z2.| proofend; theorem :: QUATERNI:88 for z being quaternion number holds |.(z * z).| = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) proofend; theorem :: QUATERNI:89 for z being quaternion number holds |.(z * z).| = |.(z * (z *')).| proofend; theorem :: QUATERNI:90 for z being quaternion number st z is real holds ( Rea z = z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) proofend; theorem :: QUATERNI:91 for x, y being Element of REAL holds [*x,y,0,0*] = [*x,y*] by Lm4; theorem :: QUATERNI:92 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)) * ) by Lm21; theorem :: QUATERNI:93 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))) * ) by Lm22; theorem :: QUATERNI:94 for z being quaternion number holds - z = (((- (Rea z)) + ((- (Im1 z)) * )) + ((- (Im2 z)) * )) + ((- (Im3 z)) * ) by Lm25; theorem :: QUATERNI:95 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)) * ) by Lm26; theorem :: QUATERNI:96 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 ) by Lm10; theorem :: QUATERNI:97 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)) ) by Lm18;