:: Inner Products, Group, Ring of Quaternion Numbers :: by Fuguo Ge :: :: Received March 18, 2008 :: Copyright (c) 2008-2012 Association of Mizar Users begin Lm1: for g being quaternion number ex r, s, t, u being Element of REAL st g = [*r,s,t,u*] by QUATERNI:7; Lm2: for a, b, c, d being real number holds (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) >= 0 by QUATERNI:74; Lm3: 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 QUATERNI:96; definition :: original:0q redefine func 0q -> Element of QUATERNION ; coherence 0q is Element of QUATERNION by QUATERNI:def_2; end; definition :: original:1q redefine func 1q -> Element of QUATERNION ; coherence 1q is Element of QUATERNION by QUATERNI:def_2; end; theorem Th1: :: QUATERN2:1 for x, y, z, w being Real holds [*x,y,z,w*] = ((x + (y * )) + (z * )) + (w * ) proofend; theorem Th2: :: QUATERN2:2 for c1, c2, c3 being quaternion number holds (c1 + c2) + c3 = c1 + (c2 + c3) proofend; theorem Th3: :: QUATERN2:3 for c being quaternion number holds c + 0q = c proofend; theorem Th4: :: QUATERN2:4 for x1, x2, x3, x4 being Element of REAL holds - [*x1,x2,x3,x4*] = [*(- x1),(- x2),(- x3),(- x4)*] proofend; theorem :: QUATERN2:5 for x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL holds [*x1,x2,x3,x4*] - [*y1,y2,y3,y4*] = [*(x1 - y1),(x2 - y2),(x3 - y3),(x4 - y4)*] proofend; theorem :: QUATERN2:6 for c1, c2, c3 being quaternion number holds (c1 - c2) + c3 = (c1 + c3) - c2 by Th2; theorem Th7: :: QUATERN2:7 for c1, c2 being quaternion number holds c1 = (c1 + c2) - c2 proofend; theorem :: QUATERN2:8 for c1, c2 being quaternion number holds c1 = (c1 - c2) + c2 proofend; theorem Th9: :: QUATERN2:9 for c being quaternion number for x1 being Element of REAL holds (- x1) * c = - (x1 * c) proofend; definition let q be quaternion number ; :: original:|. redefine func|.q.| -> Element of REAL ; coherence |.q.| is Element of REAL ; end; definition :: original: redefine func -> Element of QUATERNION ; coherence is Element of QUATERNION by QUATERNI:def_2; end; Lm4: for r being quaternion number st |.r.| = 0 holds r = 0 by QUATERNI:66; theorem Th10: :: QUATERN2:10 for r being quaternion number st r <> 0 holds |.r.| > 0 proofend; theorem Th11: :: QUATERN2:11 0q = [*0,0,0,0*] proofend; theorem :: QUATERN2:12 for r being quaternion number holds 0q * r = 0 proofend; theorem :: QUATERN2:13 for r being quaternion number holds r * 0q = 0 proofend; theorem Th14: :: QUATERN2:14 for c being quaternion number holds c * 1q = c proofend; theorem Th15: :: QUATERN2:15 for c being quaternion number holds 1q * c = c proofend; theorem Th16: :: QUATERN2:16 for c1, c2, c3 being quaternion number holds (c1 * c2) * c3 = c1 * (c2 * c3) proofend; theorem Th17: :: QUATERN2:17 for c1, c2, c3 being quaternion number holds c1 * (c2 + c3) = (c1 * c2) + (c1 * c3) proofend; theorem Th18: :: QUATERN2:18 for c1, c2, c3 being quaternion number holds (c1 + c2) * c3 = (c1 * c3) + (c2 * c3) proofend; theorem Th19: :: QUATERN2:19 for c being quaternion number holds - c = (- 1q) * c proofend; theorem Th20: :: QUATERN2:20 for c1, c2 being quaternion number holds (- c1) * c2 = - (c1 * c2) proofend; theorem Th21: :: QUATERN2:21 for c1, c2 being quaternion number holds c1 * (- c2) = - (c1 * c2) proofend; theorem Th22: :: QUATERN2:22 for c1, c2 being quaternion number holds (- c1) * (- c2) = c1 * c2 proofend; theorem Th23: :: QUATERN2:23 for c1, c2, c3 being quaternion number holds (c1 - c2) * c3 = (c1 * c3) - (c2 * c3) proofend; theorem Th24: :: QUATERN2:24 for c1, c2, c3 being quaternion number holds c1 * (c2 - c3) = (c1 * c2) - (c1 * c3) proofend; theorem Th25: :: QUATERN2:25 for x1, x2, x3, x4 being Element of REAL holds [*x1,x2,x3,x4*] *' = [*x1,(- x2),(- x3),(- x4)*] proofend; theorem :: QUATERN2:26 for c being quaternion number holds (c *') *' = c proofend; definition let q, r be quaternion number ; consider q0, q1, q2, q3 being Element of REAL such that A1: q = [*q0,q1,q2,q3*] by Lm1; consider r0, r1, r2, r3 being Element of REAL such that A2: r = [*r0,r1,r2,r3*] by Lm1; funcq / r -> set means :Def1: :: QUATERN2:def 1 ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st ( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & it = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] ); existence ex b1 being set ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st ( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & b1 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] ) proofend; uniqueness for b1, b2 being set st ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st ( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & b1 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] ) & ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st ( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & b2 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines / QUATERN2:def_1_:_ for q, r being quaternion number for b3 being set holds ( b3 = q / r iff ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st ( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & b3 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2)),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2)),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2)),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2))*] ) ); registration let q, r be quaternion number ; clusterq / r -> quaternion ; coherence q / r is quaternion proofend; end; definition let q, r be quaternion number ; :: original:/ redefine funcq / r -> Element of QUATERNION ; coherence q / r is Element of QUATERNION by QUATERNI:def_2; end; theorem :: QUATERN2:27 for q, r being quaternion number holds q / r = ((((((((Rea r) * (Rea q)) + ((Im1 q) * (Im1 r))) + ((Im2 r) * (Im2 q))) + ((Im3 r) * (Im3 q))) / (|.r.| ^2)) + (((((((Rea r) * (Im1 q)) - ((Im1 r) * (Rea q))) - ((Im2 r) * (Im3 q))) + ((Im3 r) * (Im2 q))) / (|.r.| ^2)) * )) + (((((((Rea r) * (Im2 q)) + ((Im1 r) * (Im3 q))) - ((Im2 r) * (Rea q))) - ((Im3 r) * (Im1 q))) / (|.r.| ^2)) * )) + (((((((Rea r) * (Im3 q)) - ((Im1 r) * (Im2 q))) + ((Im2 r) * (Im1 q))) - ((Im3 r) * (Rea q))) / (|.r.| ^2)) * ) proofend; definition let c be quaternion number ; funcc " -> quaternion number equals :: QUATERN2:def 2 1q / c; coherence 1q / c is quaternion number ; end; :: deftheorem defines " QUATERN2:def_2_:_ for c being quaternion number holds c " = 1q / c; definition let r be quaternion number ; :: original:" redefine funcr " -> Element of QUATERNION ; coherence r " is Element of QUATERNION ; end; theorem :: QUATERN2:28 for r being quaternion number holds r " = ((((Rea r) / (|.r.| ^2)) - (((Im1 r) / (|.r.| ^2)) * )) - (((Im2 r) / (|.r.| ^2)) * )) - (((Im3 r) / (|.r.| ^2)) * ) proofend; theorem :: QUATERN2:29 for r being quaternion number holds ( Rea (r ") = (Rea r) / (|.r.| ^2) & Im1 (r ") = - ((Im1 r) / (|.r.| ^2)) & Im2 (r ") = - ((Im2 r) / (|.r.| ^2)) & Im3 (r ") = - ((Im3 r) / (|.r.| ^2)) ) proofend; theorem :: QUATERN2:30 for q, r being quaternion number holds ( Rea (q / r) = (((((Rea r) * (Rea q)) + ((Im1 q) * (Im1 r))) + ((Im2 r) * (Im2 q))) + ((Im3 r) * (Im3 q))) / (|.r.| ^2) & Im1 (q / r) = (((((Rea r) * (Im1 q)) - ((Im1 r) * (Rea q))) - ((Im2 r) * (Im3 q))) + ((Im3 r) * (Im2 q))) / (|.r.| ^2) & Im2 (q / r) = (((((Rea r) * (Im2 q)) + ((Im1 r) * (Im3 q))) - ((Im2 r) * (Rea q))) - ((Im3 r) * (Im1 q))) / (|.r.| ^2) & Im3 (q / r) = (((((Rea r) * (Im3 q)) - ((Im1 r) * (Im2 q))) + ((Im2 r) * (Im1 q))) - ((Im3 r) * (Rea q))) / (|.r.| ^2) ) proofend; theorem Th31: :: QUATERN2:31 for r being quaternion number st r <> 0 holds r * (r ") = 1 proofend; theorem :: QUATERN2:32 for r being quaternion number st r <> 0 holds (r ") * r = 1 proofend; theorem Th33: :: QUATERN2:33 for c being quaternion number st c <> 0q holds c / c = 1q proofend; theorem :: QUATERN2:34 for c being quaternion number holds (- c) " = - (c ") proofend; definition func compquaternion -> UnOp of QUATERNION means :: QUATERN2:def 3 for c being Element of QUATERNION holds it . c = - c; existence ex b1 being UnOp of QUATERNION st for c being Element of QUATERNION holds b1 . c = - c from FUNCT_2:sch_4(); uniqueness for b1, b2 being UnOp of QUATERNION st ( for c being Element of QUATERNION holds b1 . c = - c ) & ( for c being Element of QUATERNION holds b2 . c = - c ) holds b1 = b2 from BINOP_2:sch_1(); func addquaternion -> BinOp of QUATERNION means :Def4: :: QUATERN2:def 4 for c1, c2 being Element of QUATERNION holds it . (c1,c2) = c1 + c2; existence ex b1 being BinOp of QUATERNION st for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 + c2 from BINOP_1:sch_4(); uniqueness for b1, b2 being BinOp of QUATERNION st ( for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 + c2 ) & ( for c1, c2 being Element of QUATERNION holds b2 . (c1,c2) = c1 + c2 ) holds b1 = b2 from BINOP_2:sch_2(); func diffquaternion -> BinOp of QUATERNION means :: QUATERN2:def 5 for c1, c2 being Element of QUATERNION holds it . (c1,c2) = c1 - c2; existence ex b1 being BinOp of QUATERNION st for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 - c2 from BINOP_1:sch_4(); uniqueness for b1, b2 being BinOp of QUATERNION st ( for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 - c2 ) & ( for c1, c2 being Element of QUATERNION holds b2 . (c1,c2) = c1 - c2 ) holds b1 = b2 from BINOP_2:sch_2(); func multquaternion -> BinOp of QUATERNION means :Def6: :: QUATERN2:def 6 for c1, c2 being Element of QUATERNION holds it . (c1,c2) = c1 * c2; existence ex b1 being BinOp of QUATERNION st for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 * c2 from BINOP_1:sch_4(); uniqueness for b1, b2 being BinOp of QUATERNION st ( for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 * c2 ) & ( for c1, c2 being Element of QUATERNION holds b2 . (c1,c2) = c1 * c2 ) holds b1 = b2 from BINOP_2:sch_2(); func divquaternion -> BinOp of QUATERNION means :: QUATERN2:def 7 for c1, c2 being Element of QUATERNION holds it . (c1,c2) = c1 / c2; existence ex b1 being BinOp of QUATERNION st for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 / c2 from BINOP_1:sch_4(); uniqueness for b1, b2 being BinOp of QUATERNION st ( for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 / c2 ) & ( for c1, c2 being Element of QUATERNION holds b2 . (c1,c2) = c1 / c2 ) holds b1 = b2 from BINOP_2:sch_2(); func invquaternion -> UnOp of QUATERNION means :: QUATERN2:def 8 for c being Element of QUATERNION holds it . c = c " ; existence ex b1 being UnOp of QUATERNION st for c being Element of QUATERNION holds b1 . c = c " from FUNCT_2:sch_4(); uniqueness for b1, b2 being UnOp of QUATERNION st ( for c being Element of QUATERNION holds b1 . c = c " ) & ( for c being Element of QUATERNION holds b2 . c = c " ) holds b1 = b2 from BINOP_2:sch_1(); end; :: deftheorem defines compquaternion QUATERN2:def_3_:_ for b1 being UnOp of QUATERNION holds ( b1 = compquaternion iff for c being Element of QUATERNION holds b1 . c = - c ); :: deftheorem Def4 defines addquaternion QUATERN2:def_4_:_ for b1 being BinOp of QUATERNION holds ( b1 = addquaternion iff for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 + c2 ); :: deftheorem defines diffquaternion QUATERN2:def_5_:_ for b1 being BinOp of QUATERNION holds ( b1 = diffquaternion iff for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 - c2 ); :: deftheorem Def6 defines multquaternion QUATERN2:def_6_:_ for b1 being BinOp of QUATERNION holds ( b1 = multquaternion iff for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 * c2 ); :: deftheorem defines divquaternion QUATERN2:def_7_:_ for b1 being BinOp of QUATERNION holds ( b1 = divquaternion iff for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 / c2 ); :: deftheorem defines invquaternion QUATERN2:def_8_:_ for b1 being UnOp of QUATERNION holds ( b1 = invquaternion iff for c being Element of QUATERNION holds b1 . c = c " ); definition func G_Quaternion -> strict addLoopStr means :Def9: :: QUATERN2:def 9 ( the carrier of it = QUATERNION & the addF of it = addquaternion & 0. it = 0q ); existence ex b1 being strict addLoopStr st ( the carrier of b1 = QUATERNION & the addF of b1 = addquaternion & 0. b1 = 0q ) proofend; uniqueness for b1, b2 being strict addLoopStr st the carrier of b1 = QUATERNION & the addF of b1 = addquaternion & 0. b1 = 0q & the carrier of b2 = QUATERNION & the addF of b2 = addquaternion & 0. b2 = 0q holds b1 = b2 ; end; :: deftheorem Def9 defines G_Quaternion QUATERN2:def_9_:_ for b1 being strict addLoopStr holds ( b1 = G_Quaternion iff ( the carrier of b1 = QUATERNION & the addF of b1 = addquaternion & 0. b1 = 0q ) ); registration cluster G_Quaternion -> non empty strict ; coherence not G_Quaternion is empty by Def9; end; registration cluster -> quaternion for Element of the carrier of G_Quaternion; coherence for b1 being Element of G_Quaternion holds b1 is quaternion proofend; end; registration let x, y be Element of G_Quaternion; let a, b be quaternion number ; identifyx + y with a + b when x = a, y = b; compatibility ( x = a & y = b implies x + y = a + b ) proofend; end; theorem Th35: :: QUATERN2:35 0. G_Quaternion = 0q by Def9; registration cluster G_Quaternion -> strict right_complementable Abelian add-associative right_zeroed ; coherence ( G_Quaternion is Abelian & G_Quaternion is add-associative & G_Quaternion is right_zeroed & G_Quaternion is right_complementable ) proofend; end; registration let x be Element of G_Quaternion; let a be quaternion number ; identify - x with - a when x = a; compatibility ( x = a implies - x = - a ) proofend; end; registration let x, y be Element of G_Quaternion; let a, b be quaternion number ; identifyx - y with a - b when x = a, y = b; compatibility ( x = a & y = b implies x - y = a - b ) ; end; theorem :: QUATERN2:36 for x, y, z being Element of G_Quaternion holds ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. G_Quaternion) = x ) by RLVECT_1:def_3, RLVECT_1:def_4; definition func R_Quaternion -> strict doubleLoopStr means :Def10: :: QUATERN2:def 10 ( the carrier of it = QUATERNION & the addF of it = addquaternion & the multF of it = multquaternion & 1. it = 1q & 0. it = 0q ); existence ex b1 being strict doubleLoopStr st ( the carrier of b1 = QUATERNION & the addF of b1 = addquaternion & the multF of b1 = multquaternion & 1. b1 = 1q & 0. b1 = 0q ) proofend; uniqueness for b1, b2 being strict doubleLoopStr st the carrier of b1 = QUATERNION & the addF of b1 = addquaternion & the multF of b1 = multquaternion & 1. b1 = 1q & 0. b1 = 0q & the carrier of b2 = QUATERNION & the addF of b2 = addquaternion & the multF of b2 = multquaternion & 1. b2 = 1q & 0. b2 = 0q holds b1 = b2 ; end; :: deftheorem Def10 defines R_Quaternion QUATERN2:def_10_:_ for b1 being strict doubleLoopStr holds ( b1 = R_Quaternion iff ( the carrier of b1 = QUATERNION & the addF of b1 = addquaternion & the multF of b1 = multquaternion & 1. b1 = 1q & 0. b1 = 0q ) ); registration cluster R_Quaternion -> non empty strict ; coherence not R_Quaternion is empty by Def10; end; registration cluster -> quaternion for Element of the carrier of R_Quaternion; coherence for b1 being Element of R_Quaternion holds b1 is quaternion proofend; end; registration let a, b be quaternion number ; let x, y be Element of R_Quaternion; identifyx + y with a + b when x = a, y = b; compatibility ( x = a & y = b implies x + y = a + b ) proofend; identifyx * y with a * b when x = a, y = b; compatibility ( x = a & y = b implies x * y = a * b ) proofend; end; registration cluster R_Quaternion -> strict well-unital ; coherence R_Quaternion is well-unital proofend; end; theorem :: QUATERN2:37 1. R_Quaternion = 1q by Def10; theorem :: QUATERN2:38 1_ R_Quaternion = 1q by Def10; theorem Th39: :: QUATERN2:39 0. R_Quaternion = 0q by Def10; registration cluster R_Quaternion -> non degenerated right_complementable almost_right_invertible strict Abelian add-associative right_zeroed associative right_unital distributive left_unital ; coherence ( R_Quaternion is add-associative & R_Quaternion is right_zeroed & R_Quaternion is right_complementable & R_Quaternion is Abelian & R_Quaternion is associative & R_Quaternion is left_unital & R_Quaternion is right_unital & R_Quaternion is distributive & R_Quaternion is almost_right_invertible & not R_Quaternion is degenerated ) proofend; end; registration let x be Element of R_Quaternion; let a be quaternion number ; identify - x with - a when x = a; compatibility ( x = a implies - x = - a ) proofend; end; registration let x, y be Element of R_Quaternion; let a, b be quaternion number ; identifyx - y with a - b when x = a, y = b; compatibility ( x = a & y = b implies x - y = a - b ) ; end; definition let z be Element of R_Quaternion; :: original:*' redefine funcz *' -> Element of R_Quaternion; coherence z *' is Element of R_Quaternion by Def10; end; theorem :: QUATERN2:40 for z being Element of R_Quaternion holds - z = (- (1_ R_Quaternion)) * z proofend; theorem :: QUATERN2:41 (0. R_Quaternion) *' = 0. R_Quaternion proofend; theorem :: QUATERN2:42 for z being Element of R_Quaternion st z *' = 0. R_Quaternion holds z = 0. R_Quaternion proofend; theorem :: QUATERN2:43 (1. R_Quaternion) *' = 1. R_Quaternion proofend; theorem :: QUATERN2:44 |.(0. R_Quaternion).| = 0 by Def10, QUATERNI:65; theorem :: QUATERN2:45 for z being Element of R_Quaternion st |.z.| = 0 holds z = 0. R_Quaternion by Th39, QUATERNI:66; theorem :: QUATERN2:46 |.(1. R_Quaternion).| = 1 by Def10, QUATERNI:68; theorem :: QUATERN2:47 (1. R_Quaternion) " = 1. R_Quaternion proofend; definition let x, y be quaternion number ; funcx .|. y -> Element of QUATERNION equals :: QUATERN2:def 11 x * (y *'); coherence x * (y *') is Element of QUATERNION ; end; :: deftheorem defines .|. QUATERN2:def_11_:_ for x, y being quaternion number holds x .|. y = x * (y *'); theorem Th48: :: QUATERN2:48 for c1, c2 being quaternion number holds c1 .|. c2 = [*(((((Rea c1) * (Rea c2)) + ((Im1 c1) * (Im1 c2))) + ((Im2 c1) * (Im2 c2))) + ((Im3 c1) * (Im3 c2))),(((((Rea c1) * (- (Im1 c2))) + ((Im1 c1) * (Rea c2))) - ((Im2 c1) * (Im3 c2))) + ((Im3 c1) * (Im2 c2))),(((((Rea c1) * (- (Im2 c2))) + ((Rea c2) * (Im2 c1))) - ((Im1 c2) * (Im3 c1))) + ((Im3 c2) * (Im1 c1))),(((((Rea c1) * (- (Im3 c2))) + ((Im3 c1) * (Rea c2))) - ((Im1 c1) * (Im2 c2))) + ((Im2 c1) * (Im1 c2)))*] proofend; theorem Th49: :: QUATERN2:49 for c being quaternion number holds c .|. c = |.c.| ^2 proofend; theorem :: QUATERN2:50 for c being quaternion number holds ( Rea (c .|. c) = |.c.| ^2 & Im1 (c .|. c) = 0 & Im2 (c .|. c) = 0 & Im2 (c .|. c) = 0 ) proofend; theorem :: QUATERN2:51 for c1, c2 being quaternion number holds |.(c1 .|. c2).| = |.c1.| * |.c2.| proofend; theorem :: QUATERN2:52 for c being quaternion number st c .|. c = 0 holds c = 0 proofend; theorem :: QUATERN2:53 for c1, c2, c3 being quaternion number holds (c1 + c2) .|. c3 = (c1 .|. c3) + (c2 .|. c3) by Th18; theorem :: QUATERN2:54 for c1, c2, c3 being quaternion number holds c1 .|. (c2 + c3) = (c1 .|. c2) + (c1 .|. c3) proofend; theorem :: QUATERN2:55 for c1, c2 being quaternion number holds (- c1) .|. c2 = - (c1 .|. c2) by Th20; theorem :: QUATERN2:56 for c1, c2 being quaternion number holds - (c1 .|. c2) = c1 .|. (- c2) proofend; theorem :: QUATERN2:57 for c1, c2 being quaternion number holds (- c1) .|. (- c2) = c1 .|. c2 proofend; theorem :: QUATERN2:58 for c1, c2, c3 being quaternion number holds (c1 - c2) .|. c3 = (c1 .|. c3) - (c2 .|. c3) by Th23; theorem :: QUATERN2:59 for c1, c2, c3 being quaternion number holds c1 .|. (c2 - c3) = (c1 .|. c2) - (c1 .|. c3) proofend; theorem :: QUATERN2:60 for c1, c2 being quaternion number holds (c1 + c2) .|. (c1 + c2) = (((c1 .|. c1) + (c1 .|. c2)) + (c2 .|. c1)) + (c2 .|. c2) proofend; theorem :: QUATERN2:61 for c1, c2 being quaternion number holds (c1 - c2) .|. (c1 - c2) = (((c1 .|. c1) - (c1 .|. c2)) - (c2 .|. c1)) + (c2 .|. c2) proofend;