:: QUATERN3 semantic presentation begin theorem Th1: :: QUATERN3:1 for z1, z2 being quaternion number holds Rea (z1 * z2) = Rea (z2 * z1) proof let z1, z2 be quaternion number ; ::_thesis: Rea (z1 * z2) = Rea (z2 * z1) Rea (z2 * z1) = ((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) - ((Im3 z2) * (Im3 z1)) by QUATERNI:97; hence Rea (z1 * z2) = Rea (z2 * z1) by QUATERNI:97; ::_thesis: verum end; Lm1: for z being quaternion number st z is Real holds ( z = Rea z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) proof let z be quaternion number ; ::_thesis: ( z is Real implies ( z = Rea z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) ) assume z is Real ; ::_thesis: ( z = Rea z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) then reconsider x = z as Real ; ( x = [*x,0*] & [*x,0*] = [*x,0,0,0*] ) by ARYTM_0:def_5, QUATERNI:91; hence ( z = Rea z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) by QUATERNI:23; ::_thesis: verum end; theorem :: QUATERN3:2 for z, z3 being quaternion number st z is Real holds z + z3 = ((((Rea z) + (Rea z3)) + ((Im1 z3) * )) + ((Im2 z3) * )) + ((Im3 z3) * ) proof let z, z3 be quaternion number ; ::_thesis: ( z is Real implies z + z3 = ((((Rea z) + (Rea z3)) + ((Im1 z3) * )) + ((Im2 z3) * )) + ((Im3 z3) * ) ) reconsider z1 = z + z3 as quaternion number ; assume A1: z is Real ; ::_thesis: z + z3 = ((((Rea z) + (Rea z3)) + ((Im1 z3) * )) + ((Im2 z3) * )) + ((Im3 z3) * ) then A2: Im3 z = 0 by Lm1; set z2 = [*((Rea z) + (Rea z3)),((Im1 z) + (Im1 z3)),((Im2 z) + (Im2 z3)),((Im3 z) + (Im3 z3))*]; A3: Rea [*((Rea z) + (Rea z3)),((Im1 z) + (Im1 z3)),((Im2 z) + (Im2 z3)),((Im3 z) + (Im3 z3))*] = (Rea z) + (Rea z3) by QUATERNI:23 .= Rea z1 by QUATERNI:36 ; A4: Im1 [*((Rea z) + (Rea z3)),((Im1 z) + (Im1 z3)),((Im2 z) + (Im2 z3)),((Im3 z) + (Im3 z3))*] = (Im1 z) + (Im1 z3) by QUATERNI:23 .= Im1 z1 by QUATERNI:36 ; A5: Im3 [*((Rea z) + (Rea z3)),((Im1 z) + (Im1 z3)),((Im2 z) + (Im2 z3)),((Im3 z) + (Im3 z3))*] = (Im3 z) + (Im3 z3) by QUATERNI:23 .= Im3 z1 by QUATERNI:36 ; A6: Im2 [*((Rea z) + (Rea z3)),((Im1 z) + (Im1 z3)),((Im2 z) + (Im2 z3)),((Im3 z) + (Im3 z3))*] = (Im2 z) + (Im2 z3) by QUATERNI:23 .= Im2 z1 by QUATERNI:36 ; ( Im1 z = 0 & Im2 z = 0 ) by A1, Lm1; then z + z3 = [*((Rea z) + (Rea z3)),(Im1 z3),(Im2 z3),(Im3 z3)*] by A2, A3, A4, A6, A5, QUATERNI:25; hence z + z3 = ((((Rea z) + (Rea z3)) + ((Im1 z3) * )) + ((Im2 z3) * )) + ((Im3 z3) * ) by QUATERN2:1; ::_thesis: verum end; theorem :: QUATERN3:3 for z, z3 being quaternion number st z is Real holds z - z3 = [*((Rea z) - (Rea z3)),(- (Im1 z3)),(- (Im2 z3)),(- (Im3 z3))*] proof let z, z3 be quaternion number ; ::_thesis: ( z is Real implies z - z3 = [*((Rea z) - (Rea z3)),(- (Im1 z3)),(- (Im2 z3)),(- (Im3 z3))*] ) reconsider z1 = z + (- z3) as quaternion number ; assume A1: z is Real ; ::_thesis: z - z3 = [*((Rea z) - (Rea z3)),(- (Im1 z3)),(- (Im2 z3)),(- (Im3 z3))*] then A2: Im3 z = 0 by Lm1; set z2 = [*((Rea z) - (Rea z3)),((Im1 z) - (Im1 z3)),((Im2 z) - (Im2 z3)),((Im3 z) - (Im3 z3))*]; A3: Rea [*((Rea z) - (Rea z3)),((Im1 z) - (Im1 z3)),((Im2 z) - (Im2 z3)),((Im3 z) - (Im3 z3))*] = (Rea z) + (- (Rea z3)) by QUATERNI:23 .= (Rea z) + (Rea (- z3)) by QUATERNI:41 .= Rea z1 by QUATERNI:36 ; A4: Im1 [*((Rea z) - (Rea z3)),((Im1 z) - (Im1 z3)),((Im2 z) - (Im2 z3)),((Im3 z) - (Im3 z3))*] = (Im1 z) + (- (Im1 z3)) by QUATERNI:23 .= (Im1 z) + (Im1 (- z3)) by QUATERNI:41 .= Im1 z1 by QUATERNI:36 ; A5: Im3 [*((Rea z) - (Rea z3)),((Im1 z) - (Im1 z3)),((Im2 z) - (Im2 z3)),((Im3 z) - (Im3 z3))*] = (Im3 z) + (- (Im3 z3)) by QUATERNI:23 .= (Im3 z) + (Im3 (- z3)) by QUATERNI:41 .= Im3 z1 by QUATERNI:36 ; A6: Im2 [*((Rea z) - (Rea z3)),((Im1 z) - (Im1 z3)),((Im2 z) - (Im2 z3)),((Im3 z) - (Im3 z3))*] = (Im2 z) + (- (Im2 z3)) by QUATERNI:23 .= (Im2 z) + (Im2 (- z3)) by QUATERNI:41 .= Im2 z1 by QUATERNI:36 ; ( Im1 z = 0 & Im2 z = 0 ) by A1, Lm1; hence z - z3 = [*((Rea z) - (Rea z3)),(- (Im1 z3)),(- (Im2 z3)),(- (Im3 z3))*] by A2, A3, A4, A6, A5, QUATERNI:25; ::_thesis: verum end; theorem :: QUATERN3:4 for z, z3 being quaternion number st z is Real holds z * z3 = [*((Rea z) * (Rea z3)),((Rea z) * (Im1 z3)),((Rea z) * (Im2 z3)),((Rea z) * (Im3 z3))*] proof let z, z3 be quaternion number ; ::_thesis: ( z is Real implies z * z3 = [*((Rea z) * (Rea z3)),((Rea z) * (Im1 z3)),((Rea z) * (Im2 z3)),((Rea z) * (Im3 z3))*] ) assume A1: z is Real ; ::_thesis: z * z3 = [*((Rea z) * (Rea z3)),((Rea z) * (Im1 z3)),((Rea z) * (Im2 z3)),((Rea z) * (Im3 z3))*] then A2: Im3 z = 0 by Lm1; A3: z * z3 = [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*] proof reconsider z9 = z * z3 as quaternion number ; set z1 = [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*]; A4: Im1 [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*] = ((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3)) by QUATERNI:23 .= Im1 z9 by QUATERNI:97 ; A5: Im2 [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*] = ((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3)) by QUATERNI:23 .= Im2 z9 by QUATERNI:97 ; A6: Im3 [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*] = ((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)) by QUATERNI:23 .= Im3 z9 by QUATERNI:97 ; Rea [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*] = ((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3)) by QUATERNI:23 .= Rea z9 by QUATERNI:97 ; hence z * z3 = [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*] by A4, A5, A6, QUATERNI:25; ::_thesis: verum end; ( Im1 z = 0 & Im2 z = 0 ) by A1, Lm1; hence z * z3 = [*((Rea z) * (Rea z3)),((Rea z) * (Im1 z3)),((Rea z) * (Im2 z3)),((Rea z) * (Im3 z3))*] by A2, A3; ::_thesis: verum end; theorem :: QUATERN3:5 for z being quaternion number st z is Real holds z * = [*0,(Rea z),0,0*] proof let z be quaternion number ; ::_thesis: ( z is Real implies z * = [*0,(Rea z),0,0*] ) assume A1: z is Real ; ::_thesis: z * = [*0,(Rea z),0,0*] then reconsider x = z as Real ; A2: x = Rea z by Lm1; z * = [*(Rea (z * )),(Im1 (z * )),(Im2 (z * )),(Im3 (z * ))*] by QUATERNI:24 .= [*0,(Im1 (z * )),(Im2 (z * )),(Im3 (z * ))*] by A1, QUATERNI:33 .= [*0,x,(Im2 (z * )),(Im3 (z * ))*] by QUATERNI:33 .= [*0,x,0,(Im3 (z * ))*] by QUATERNI:33 .= [*0,(Rea z),0,0*] by A2, QUATERNI:33 ; hence z * = [*0,(Rea z),0,0*] ; ::_thesis: verum end; theorem :: QUATERN3:6 for z being quaternion number st z is Real holds z * = [*0,0,(Rea z),0*] proof let z be quaternion number ; ::_thesis: ( z is Real implies z * = [*0,0,(Rea z),0*] ) assume A1: z is Real ; ::_thesis: z * = [*0,0,(Rea z),0*] then reconsider x = z as Real ; A2: x = Rea z by Lm1; z * = [*(Rea (z * )),(Im1 (z * )),(Im2 (z * )),(Im3 (z * ))*] by QUATERNI:24 .= [*0,(Im1 (z * )),(Im2 (z * )),(Im3 (z * ))*] by A1, QUATERNI:34 .= [*0,0,(Im2 (z * )),(Im3 (z * ))*] by A1, QUATERNI:34 .= [*0,0,x,(Im3 (z * ))*] by QUATERNI:34 .= [*0,0,(Rea z),0*] by A2, QUATERNI:34 ; hence z * = [*0,0,(Rea z),0*] ; ::_thesis: verum end; theorem :: QUATERN3:7 for z being quaternion number st z is Real holds z * = [*0,0,0,(Rea z)*] proof let z be quaternion number ; ::_thesis: ( z is Real implies z * = [*0,0,0,(Rea z)*] ) assume A1: z is Real ; ::_thesis: z * = [*0,0,0,(Rea z)*] then reconsider x = z as Real ; A2: x = Rea z by Lm1; z * = [*(Rea (z * )),(Im1 (z * )),(Im2 (z * )),(Im3 (z * ))*] by QUATERNI:24 .= [*0,(Im1 (z * )),(Im2 (z * )),(Im3 (z * ))*] by A1, QUATERNI:35 .= [*0,0,(Im2 (z * )),(Im3 (z * ))*] by A1, QUATERNI:35 .= [*0,0,0,(Im3 (z * ))*] by A1, QUATERNI:35 .= [*0,0,0,(Rea z)*] by A2, QUATERNI:35 ; hence z * = [*0,0,0,(Rea z)*] ; ::_thesis: verum end; theorem :: QUATERN3:8 for z being quaternion number holds z - 0q = z proof let z be quaternion number ; ::_thesis: z - 0q = z consider x, y, w, v being Element of REAL such that A1: z = [*x,y,w,v*] by QUATERNI:7; 0q = [*0,0*] by ARYTM_0:def_5 .= [*0,0,0,0*] by QUATERNI:91 ; then - 0q = [*(- 0),(- 0),(- 0),(- 0)*] by QUATERN2:4; then z - 0q = [*(x + (- 0)),(y + (- 0)),(w + (- 0)),(v + (- 0))*] by A1, QUATERNI:def_7 .= [*x,y,w,v*] ; hence z - 0q = z by A1; ::_thesis: verum end; theorem :: QUATERN3:9 for z, z1 being quaternion number st z is Real holds z * z1 = z1 * z proof let z, z1 be quaternion number ; ::_thesis: ( z is Real implies z * z1 = z1 * z ) assume A1: z is Real ; ::_thesis: z * z1 = z1 * z then A2: Im3 z = 0 by Lm1; A3: ( Im1 z = 0 & Im2 z = 0 ) by A1, Lm1; z1 * z = (((((((Rea z1) * (Rea z)) - ((Im1 z1) * (Im1 z))) - ((Im2 z1) * (Im2 z))) - ((Im3 z1) * (Im3 z))) + ((((((Rea z1) * (Im1 z)) + ((Im1 z1) * (Rea z))) + ((Im2 z1) * (Im3 z))) - ((Im3 z1) * (Im2 z))) * )) + ((((((Rea z1) * (Im2 z)) + ((Im2 z1) * (Rea z))) + ((Im3 z1) * (Im1 z))) - ((Im1 z1) * (Im3 z))) * )) + ((((((Rea z1) * (Im3 z)) + ((Im3 z1) * (Rea z))) + ((Im1 z1) * (Im2 z))) - ((Im2 z1) * (Im1 z))) * ) by QUATERNI:93; hence z * z1 = z1 * z by A2, A3, QUATERNI:93; ::_thesis: verum end; theorem :: QUATERN3:10 for z being quaternion number st Im1 z = 0 & Im2 z = 0 & Im3 z = 0 holds z = Rea z proof let z be quaternion number ; ::_thesis: ( Im1 z = 0 & Im2 z = 0 & Im3 z = 0 implies z = Rea z ) set x = Rea z; assume ( Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) ; ::_thesis: z = Rea z then A1: z = [*(Rea z),0,0,0*] by QUATERNI:24; [*(Rea z),0,0,0*] = [*(Rea z),0*] by QUATERNI:91; hence z = Rea z by A1, ARYTM_0:def_5; ::_thesis: verum end; theorem Th11: :: QUATERN3:11 for z being quaternion number holds |.z.| ^2 = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) proof let z be quaternion number ; ::_thesis: |.z.| ^2 = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) >= 0 by QUATERNI:74; then |.z.| ^2 = sqrt ((((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)) ^2) by SQUARE_1:29 .= ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) by QUATERNI:74, SQUARE_1:22 ; hence |.z.| ^2 = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) ; ::_thesis: verum end; theorem :: QUATERN3:12 for z being quaternion number holds |.z.| ^2 = |.(z * (z *')).| proof let z be quaternion number ; ::_thesis: |.z.| ^2 = |.(z * (z *')).| ( |.(z * z).| = |.(z * (z *')).| & |.z.| ^2 = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) ) by Th11, QUATERNI:89; hence |.z.| ^2 = |.(z * (z *')).| by QUATERNI:88; ::_thesis: verum end; theorem :: QUATERN3:13 for z being quaternion number holds |.z.| ^2 = Rea (z * (z *')) proof let z be quaternion number ; ::_thesis: |.z.| ^2 = Rea (z * (z *')) Rea (z * (z *')) = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) by QUATERNI:60; hence |.z.| ^2 = Rea (z * (z *')) by Th11; ::_thesis: verum end; theorem :: QUATERN3:14 for z being quaternion number holds 2 * (Rea z) = Rea (z + (z *')) proof let z be quaternion number ; ::_thesis: 2 * (Rea z) = Rea (z + (z *')) ( z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*] & z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] ) by QUATERNI:24, QUATERNI:43; then z + (z *') = [*((Rea z) + (Rea z)),((Im1 z) + (- (Im1 z))),((Im2 z) + (- (Im2 z))),((Im3 z) + (- (Im3 z)))*] by QUATERNI:def_7 .= [*(2 * (Rea z)),0,0,0*] ; hence 2 * (Rea z) = Rea (z + (z *')) by QUATERNI:23; ::_thesis: verum end; theorem :: QUATERN3:15 for z, z1 being quaternion number st z is Real holds (z * z1) *' = (z *') * (z1 *') proof let z, z1 be quaternion number ; ::_thesis: ( z is Real implies (z * z1) *' = (z *') * (z1 *') ) A1: ( Im1 (z1 *') = - (Im1 z1) & Im2 (z1 *') = - (Im2 z1) ) by QUATERNI:44; A2: ( Im3 (z1 *') = - (Im3 z1) & Rea (z *') = Rea z ) by QUATERNI:44; A3: Rea (z * z1) = ((((Rea z) * (Rea z1)) - ((Im1 z) * (Im1 z1))) - ((Im2 z) * (Im2 z1))) - ((Im3 z) * (Im3 z1)) by QUATERNI:97; assume A4: z is Real ; ::_thesis: (z * z1) *' = (z *') * (z1 *') then reconsider x = z as Real ; A5: ( Im1 z = 0 & Im2 z = 0 ) by A4, Lm1; A6: Im3 z = 0 by A4, Lm1; A7: Im3 (z *') = - (Im3 z) by QUATERNI:44; A8: ( Im1 (z *') = - (Im1 z) & Im2 (z *') = - (Im2 z) ) by QUATERNI:44; A9: Im3 (z * z1) = ((((Rea z) * (Im3 z1)) + ((Im3 z) * (Rea z1))) + ((Im1 z) * (Im2 z1))) - ((Im2 z) * (Im1 z1)) by QUATERNI:97; A10: Im2 (z * z1) = ((((Rea z) * (Im2 z1)) + ((Im2 z) * (Rea z1))) + ((Im3 z) * (Im1 z1))) - ((Im1 z) * (Im3 z1)) by QUATERNI:97; A11: Im1 (z * z1) = ((((Rea z) * (Im1 z1)) + ((Im1 z) * (Rea z1))) + ((Im2 z) * (Im3 z1))) - ((Im3 z) * (Im2 z1)) by QUATERNI:97; set z3 = z *' ; set z2 = z1 *' ; A12: (z *') * (z1 *') = (((((((Rea (z *')) * (Rea (z1 *'))) - ((Im1 (z *')) * (Im1 (z1 *')))) - ((Im2 (z *')) * (Im2 (z1 *')))) - ((Im3 (z *')) * (Im3 (z1 *')))) + ((((((Rea (z *')) * (Im1 (z1 *'))) + ((Im1 (z *')) * (Rea (z1 *')))) + ((Im2 (z *')) * (Im3 (z1 *')))) - ((Im3 (z *')) * (Im2 (z1 *')))) * )) + ((((((Rea (z *')) * (Im2 (z1 *'))) + ((Im2 (z *')) * (Rea (z1 *')))) + ((Im3 (z *')) * (Im1 (z1 *')))) - ((Im1 (z *')) * (Im3 (z1 *')))) * )) + ((((((Rea (z *')) * (Im3 (z1 *'))) + ((Im3 (z *')) * (Rea (z1 *')))) + ((Im1 (z *')) * (Im2 (z1 *')))) - ((Im2 (z *')) * (Im1 (z1 *')))) * ) by QUATERNI:93; (z * z1) *' = (((Rea ((z * z1) *')) + ((Im1 ((z * z1) *')) * )) + ((Im2 ((z * z1) *')) * )) + ((Im3 ((z * z1) *')) * ) by QUATERNI:37 .= (((((((Rea z) * (Rea z1)) - ((Im1 z) * (Im1 z1))) - ((Im2 z) * (Im2 z1))) - ((Im3 z) * (Im3 z1))) + ((Im1 ((z * z1) *')) * )) + ((Im2 ((z * z1) *')) * )) + ((Im3 ((z * z1) *')) * ) by A3, QUATERNI:44 .= (((((((Rea z) * (Rea z1)) - ((Im1 z) * (Im1 z1))) - ((Im2 z) * (Im2 z1))) - ((Im3 z) * (Im3 z1))) + ((- (((((Rea z) * (Im1 z1)) + ((Im1 z) * (Rea z1))) + ((Im2 z) * (Im3 z1))) - ((Im3 z) * (Im2 z1)))) * )) + ((Im2 ((z * z1) *')) * )) + ((Im3 ((z * z1) *')) * ) by A11, QUATERNI:44 .= (((((((Rea z) * (Rea z1)) - ((Im1 z) * (Im1 z1))) - ((Im2 z) * (Im2 z1))) - ((Im3 z) * (Im3 z1))) + ((- (((((Rea z) * (Im1 z1)) + ((Im1 z) * (Rea z1))) + ((Im2 z) * (Im3 z1))) - ((Im3 z) * (Im2 z1)))) * )) + ((- (((((Rea z) * (Im2 z1)) + ((Im2 z) * (Rea z1))) + ((Im3 z) * (Im1 z1))) - ((Im1 z) * (Im3 z1)))) * )) + ((Im3 ((z * z1) *')) * ) by A10, QUATERNI:44 .= (((((((Rea z) * (Rea z1)) - ((Im1 z) * (Im1 z1))) - ((Im2 z) * (Im2 z1))) - ((Im3 z) * (Im3 z1))) + ((- (((((Rea z) * (Im1 z1)) + ((Im1 z) * (Rea z1))) + ((Im2 z) * (Im3 z1))) - ((Im3 z) * (Im2 z1)))) * )) + ((- (((((Rea z) * (Im2 z1)) + ((Im2 z) * (Rea z1))) + ((Im3 z) * (Im1 z1))) - ((Im1 z) * (Im3 z1)))) * )) + ((- (((((Rea z) * (Im3 z1)) + ((Im3 z) * (Rea z1))) + ((Im1 z) * (Im2 z1))) - ((Im2 z) * (Im1 z1)))) * ) by A9, QUATERNI:44 ; hence (z * z1) *' = (z *') * (z1 *') by A5, A6, A1, A2, A8, A7, A12, QUATERNI:44; ::_thesis: verum end; theorem :: QUATERN3:16 for z1, z2 being quaternion number holds (z1 * z2) *' = (z2 *') * (z1 *') proof let z1, z2 be quaternion number ; ::_thesis: (z1 * z2) *' = (z2 *') * (z1 *') A1: ( Rea (z2 *') = Rea z2 & Im1 (z2 *') = - (Im1 z2) ) by QUATERNI:44; A2: ( Im2 (z2 *') = - (Im2 z2) & Im3 (z2 *') = - (Im3 z2) ) by QUATERNI:44; A3: Rea (z1 * z2) = ((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2)) by QUATERNI:97; A4: Im3 (z1 * z2) = ((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2)) by QUATERNI:97; A5: ( Im2 (z1 *') = - (Im2 z1) & Im3 (z1 *') = - (Im3 z1) ) by QUATERNI:44; A6: ( Rea (z1 *') = Rea z1 & Im1 (z1 *') = - (Im1 z1) ) by QUATERNI:44; A7: Im2 (z1 * z2) = ((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2)) by QUATERNI:97; A8: Im1 (z1 * z2) = ((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)) by QUATERNI:97; set z3 = z2 *' ; set z4 = z1 *' ; A9: (z2 *') * (z1 *') = (((((((Rea (z2 *')) * (Rea (z1 *'))) - ((Im1 (z2 *')) * (Im1 (z1 *')))) - ((Im2 (z2 *')) * (Im2 (z1 *')))) - ((Im3 (z2 *')) * (Im3 (z1 *')))) + ((((((Rea (z2 *')) * (Im1 (z1 *'))) + ((Im1 (z2 *')) * (Rea (z1 *')))) + ((Im2 (z2 *')) * (Im3 (z1 *')))) - ((Im3 (z2 *')) * (Im2 (z1 *')))) * )) + ((((((Rea (z2 *')) * (Im2 (z1 *'))) + ((Im2 (z2 *')) * (Rea (z1 *')))) + ((Im3 (z2 *')) * (Im1 (z1 *')))) - ((Im1 (z2 *')) * (Im3 (z1 *')))) * )) + ((((((Rea (z2 *')) * (Im3 (z1 *'))) + ((Im3 (z2 *')) * (Rea (z1 *')))) + ((Im1 (z2 *')) * (Im2 (z1 *')))) - ((Im2 (z2 *')) * (Im1 (z1 *')))) * ) by QUATERNI:93; (z1 * z2) *' = (((Rea ((z1 * z2) *')) + ((Im1 ((z1 * z2) *')) * )) + ((Im2 ((z1 * z2) *')) * )) + ((Im3 ((z1 * z2) *')) * ) by QUATERNI:37 .= (((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) + ((Im1 ((z1 * z2) *')) * )) + ((Im2 ((z1 * z2) *')) * )) + ((Im3 ((z1 * z2) *')) * ) by A3, QUATERNI:44 .= (((((((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)))) * )) + ((Im2 ((z1 * z2) *')) * )) + ((Im3 ((z1 * z2) *')) * ) by A8, QUATERNI:44 .= (((((((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)))) * )) + ((Im3 ((z1 * z2) *')) * ) by A7, QUATERNI:44 .= (((((((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 A4, QUATERNI:44 ; hence (z1 * z2) *' = (z2 *') * (z1 *') by A1, A2, A6, A5, A9; ::_thesis: verum end; theorem Th17: :: QUATERN3:17 for z1, z2 being quaternion number holds |.(z1 * z2).| ^2 = (|.z1.| ^2) * (|.z2.| ^2) proof let z1, z2 be quaternion number ; ::_thesis: |.(z1 * z2).| ^2 = (|.z1.| ^2) * (|.z2.| ^2) set z3 = z1 * z2; A1: ( 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)) ) by QUATERNI:97; A2: ( 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 QUATERNI:97; ( |.z1.| ^2 = ((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2) & |.z2.| ^2 = ((((Rea z2) ^2) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2) ) by Th11; hence |.(z1 * z2).| ^2 = (|.z1.| ^2) * (|.z2.| ^2) by A1, A2, Th11; ::_thesis: verum end; theorem :: QUATERN3:18 for z1 being quaternion number holds ( * z1) - (z1 * ) = [*0,0,(- (2 * (Im3 z1))),(2 * (Im2 z1))*] proof let z1 be quaternion number ; ::_thesis: ( * z1) - (z1 * ) = [*0,0,(- (2 * (Im3 z1))),(2 * (Im2 z1))*] set z = ; set s = ( * z1) - (z1 * ); A1: ( Rea (z1 * ) = ((((Rea z1) * (Rea )) - ((Im1 z1) * (Im1 ))) - ((Im2 z1) * (Im2 ))) - ((Im3 z1) * (Im3 )) & Im1 (z1 * ) = ((((Rea z1) * (Im1 )) + ((Im1 z1) * (Rea ))) + ((Im2 z1) * (Im3 ))) - ((Im3 z1) * (Im2 )) & Im2 (z1 * ) = ((((Rea z1) * (Im2 )) + ((Im2 z1) * (Rea ))) + ((Im3 z1) * (Im1 ))) - ((Im1 z1) * (Im3 )) & Im3 (z1 * ) = ((((Rea z1) * (Im3 )) + ((Im3 z1) * (Rea ))) + ((Im1 z1) * (Im2 ))) - ((Im2 z1) * (Im1 )) ) by QUATERNI:97; A2: ( Im2 ( * z1) = ((((Rea ) * (Im2 z1)) + ((Im2 ) * (Rea z1))) + ((Im3 ) * (Im1 z1))) - ((Im1 ) * (Im3 z1)) & Im3 ( * z1) = ((((Rea ) * (Im3 z1)) + ((Im3 ) * (Rea z1))) + ((Im1 ) * (Im2 z1))) - ((Im2 ) * (Im1 z1)) ) by QUATERNI:97; ( Rea ( * z1) = - (Im1 z1) & Im1 ( * z1) = Rea z1 ) by A1, QUATERNI:30, QUATERNI:97; then A3: ( Rea (( * z1) - (z1 * )) = (- (Im1 z1)) - (- (Im1 z1)) & Im1 (( * z1) - (z1 * )) = (Rea z1) - (Rea z1) ) by A1, QUATERNI:30, QUATERNI:42; ( Im2 (( * z1) - (z1 * )) = (- (Im3 z1)) - (Im3 z1) & Im3 (( * z1) - (z1 * )) = (Im2 z1) - (- (Im2 z1)) ) by A2, A1, QUATERNI:30, QUATERNI:42; hence ( * z1) - (z1 * ) = [*0,0,(- (2 * (Im3 z1))),(2 * (Im2 z1))*] by A3, QUATERNI:24; ::_thesis: verum end; theorem :: QUATERN3:19 for z1 being quaternion number holds ( * z1) + (z1 * ) = [*(- (2 * (Im1 z1))),(2 * (Rea z1)),0,0*] proof let z1 be quaternion number ; ::_thesis: ( * z1) + (z1 * ) = [*(- (2 * (Im1 z1))),(2 * (Rea z1)),0,0*] set z = ; A1: * z1 = (((((((Rea ) * (Rea z1)) - ((Im1 ) * (Im1 z1))) - ((Im2 ) * (Im2 z1))) - ((Im3 ) * (Im3 z1))) + ((((((Rea ) * (Im1 z1)) + ((Im1 ) * (Rea z1))) + ((Im2 ) * (Im3 z1))) - ((Im3 ) * (Im2 z1))) * )) + ((((((Rea ) * (Im2 z1)) + ((Im2 ) * (Rea z1))) + ((Im3 ) * (Im1 z1))) - ((Im1 ) * (Im3 z1))) * )) + ((((((Rea ) * (Im3 z1)) + ((Im3 ) * (Rea z1))) + ((Im1 ) * (Im2 z1))) - ((Im2 ) * (Im1 z1))) * ) by QUATERNI:93 .= [*(- (Im1 z1)),(Rea z1),(- (Im3 z1)),(Im2 z1)*] by QUATERN2:1, QUATERNI:30 ; then A2: ( Im2 ( * z1) = - (Im3 z1) & Im3 ( * z1) = Im2 z1 ) by QUATERNI:23; A3: z1 * = (((((((Rea z1) * (Rea )) - ((Im1 z1) * (Im1 ))) - ((Im2 z1) * (Im2 ))) - ((Im3 z1) * (Im3 ))) + ((((((Rea z1) * (Im1 )) + ((Im1 z1) * (Rea ))) + ((Im2 z1) * (Im3 ))) - ((Im3 z1) * (Im2 ))) * )) + ((((((Rea z1) * (Im2 )) + ((Im2 z1) * (Rea ))) + ((Im3 z1) * (Im1 ))) - ((Im1 z1) * (Im3 ))) * )) + ((((((Rea z1) * (Im3 )) + ((Im3 z1) * (Rea ))) + ((Im1 z1) * (Im2 ))) - ((Im2 z1) * (Im1 ))) * ) by QUATERNI:93 .= [*(- (Im1 z1)),(Rea z1),(Im3 z1),(- (Im2 z1))*] by QUATERN2:1, QUATERNI:30 ; then A4: ( Rea (z1 * ) = - (Im1 z1) & Im1 (z1 * ) = Rea z1 ) by QUATERNI:23; A5: ( Im2 (z1 * ) = Im3 z1 & Im3 (z1 * ) = - (Im2 z1) ) by A3, QUATERNI:23; ( Rea ( * z1) = - (Im1 z1) & Im1 ( * z1) = Rea z1 ) by A1, QUATERNI:23; then ( * z1) + (z1 * ) = ((((- (Im1 z1)) + (- (Im1 z1))) + (((Rea z1) + (Rea z1)) * )) + (((- (Im3 z1)) + (Im3 z1)) * )) + (((Im2 z1) + (- (Im2 z1))) * ) by A2, A4, A5, QUATERNI:92; hence ( * z1) + (z1 * ) = [*(- (2 * (Im1 z1))),(2 * (Rea z1)),0,0*] by QUATERN2:1; ::_thesis: verum end; theorem :: QUATERN3:20 for z1 being quaternion number holds ( * z1) - (z1 * ) = [*0,(2 * (Im3 z1)),0,(- (2 * (Im1 z1)))*] proof let z1 be quaternion number ; ::_thesis: ( * z1) - (z1 * ) = [*0,(2 * (Im3 z1)),0,(- (2 * (Im1 z1)))*] set z = ; A1: * z1 = (((((((Rea ) * (Rea z1)) - ((Im1 ) * (Im1 z1))) - ((Im2 ) * (Im2 z1))) - ((Im3 ) * (Im3 z1))) + ((((((Rea ) * (Im1 z1)) + ((Im1 ) * (Rea z1))) + ((Im2 ) * (Im3 z1))) - ((Im3 ) * (Im2 z1))) * )) + ((((((Rea ) * (Im2 z1)) + ((Im2 ) * (Rea z1))) + ((Im3 ) * (Im1 z1))) - ((Im1 ) * (Im3 z1))) * )) + ((((((Rea ) * (Im3 z1)) + ((Im3 ) * (Rea z1))) + ((Im1 ) * (Im2 z1))) - ((Im2 ) * (Im1 z1))) * ) by QUATERNI:93 .= [*(- (Im2 z1)),(Im3 z1),(Rea z1),(- (Im1 z1))*] by QUATERN2:1, QUATERNI:31 ; z1 * = (((((((Rea z1) * (Rea )) - ((Im1 z1) * (Im1 ))) - ((Im2 z1) * (Im2 ))) - ((Im3 z1) * (Im3 ))) + ((((((Rea z1) * (Im1 )) + ((Im1 z1) * (Rea ))) + ((Im2 z1) * (Im3 ))) - ((Im3 z1) * (Im2 ))) * )) + ((((((Rea z1) * (Im2 )) + ((Im2 z1) * (Rea ))) + ((Im3 z1) * (Im1 ))) - ((Im1 z1) * (Im3 ))) * )) + ((((((Rea z1) * (Im3 )) + ((Im3 z1) * (Rea ))) + ((Im1 z1) * (Im2 ))) - ((Im2 z1) * (Im1 ))) * ) by QUATERNI:93 .= [*(- (Im2 z1)),(- (Im3 z1)),(Rea z1),(Im1 z1)*] by QUATERN2:1, QUATERNI:31 ; then ( * z1) - (z1 * ) = [*((- (Im2 z1)) - (- (Im2 z1))),((Im3 z1) - (- (Im3 z1))),((Rea z1) - (Rea z1)),((- (Im1 z1)) - (Im1 z1))*] by A1, QUATERN2:5 .= [*0,(2 * (Im3 z1)),0,(- (2 * (Im1 z1)))*] ; hence ( * z1) - (z1 * ) = [*0,(2 * (Im3 z1)),0,(- (2 * (Im1 z1)))*] ; ::_thesis: verum end; theorem :: QUATERN3:21 for z1 being quaternion number holds ( * z1) + (z1 * ) = [*(- (2 * (Im2 z1))),0,(2 * (Rea z1)),0*] proof let z1 be quaternion number ; ::_thesis: ( * z1) + (z1 * ) = [*(- (2 * (Im2 z1))),0,(2 * (Rea z1)),0*] set z = ; A1: * z1 = (((((((Rea ) * (Rea z1)) - ((Im1 ) * (Im1 z1))) - ((Im2 ) * (Im2 z1))) - ((Im3 ) * (Im3 z1))) + ((((((Rea ) * (Im1 z1)) + ((Im1 ) * (Rea z1))) + ((Im2 ) * (Im3 z1))) - ((Im3 ) * (Im2 z1))) * )) + ((((((Rea ) * (Im2 z1)) + ((Im2 ) * (Rea z1))) + ((Im3 ) * (Im1 z1))) - ((Im1 ) * (Im3 z1))) * )) + ((((((Rea ) * (Im3 z1)) + ((Im3 ) * (Rea z1))) + ((Im1 ) * (Im2 z1))) - ((Im2 ) * (Im1 z1))) * ) by QUATERNI:93 .= [*(- (Im2 z1)),(Im3 z1),(Rea z1),(- (Im1 z1))*] by QUATERN2:1, QUATERNI:31 ; then A2: ( Im2 ( * z1) = Rea z1 & Im3 ( * z1) = - (Im1 z1) ) by QUATERNI:23; A3: z1 * = (((((((Rea z1) * (Rea )) - ((Im1 z1) * (Im1 ))) - ((Im2 z1) * (Im2 ))) - ((Im3 z1) * (Im3 ))) + ((((((Rea z1) * (Im1 )) + ((Im1 z1) * (Rea ))) + ((Im2 z1) * (Im3 ))) - ((Im3 z1) * (Im2 ))) * )) + ((((((Rea z1) * (Im2 )) + ((Im2 z1) * (Rea ))) + ((Im3 z1) * (Im1 ))) - ((Im1 z1) * (Im3 ))) * )) + ((((((Rea z1) * (Im3 )) + ((Im3 z1) * (Rea ))) + ((Im1 z1) * (Im2 ))) - ((Im2 z1) * (Im1 ))) * ) by QUATERNI:93 .= [*(- (Im2 z1)),(- (Im3 z1)),(Rea z1),(Im1 z1)*] by QUATERN2:1, QUATERNI:31 ; then A4: ( Rea (z1 * ) = - (Im2 z1) & Im1 (z1 * ) = - (Im3 z1) ) by QUATERNI:23; A5: ( Im2 (z1 * ) = Rea z1 & Im3 (z1 * ) = Im1 z1 ) by A3, QUATERNI:23; ( Rea ( * z1) = - (Im2 z1) & Im1 ( * z1) = Im3 z1 ) by A1, QUATERNI:23; then (z1 * ) + ( * z1) = ((((- (Im2 z1)) + (- (Im2 z1))) + (((Im3 z1) - (Im3 z1)) * )) + (((Rea z1) + (Rea z1)) * )) + (((- (Im1 z1)) + (Im1 z1)) * ) by A2, A4, A5, QUATERNI:92; hence ( * z1) + (z1 * ) = [*(- (2 * (Im2 z1))),0,(2 * (Rea z1)),0*] by QUATERN2:1; ::_thesis: verum end; theorem :: QUATERN3:22 for z1 being quaternion number holds ( * z1) - (z1 * ) = [*0,(- (2 * (Im2 z1))),(2 * (Im1 z1)),0*] proof let z1 be quaternion number ; ::_thesis: ( * z1) - (z1 * ) = [*0,(- (2 * (Im2 z1))),(2 * (Im1 z1)),0*] set z = ; A1: * z1 = (((((((Rea ) * (Rea z1)) - ((Im1 ) * (Im1 z1))) - ((Im2 ) * (Im2 z1))) - ((Im3 ) * (Im3 z1))) + ((((((Rea ) * (Im1 z1)) + ((Im1 ) * (Rea z1))) + ((Im2 ) * (Im3 z1))) - ((Im3 ) * (Im2 z1))) * )) + ((((((Rea ) * (Im2 z1)) + ((Im2 ) * (Rea z1))) + ((Im3 ) * (Im1 z1))) - ((Im1 ) * (Im3 z1))) * )) + ((((((Rea ) * (Im3 z1)) + ((Im3 ) * (Rea z1))) + ((Im1 ) * (Im2 z1))) - ((Im2 ) * (Im1 z1))) * ) by QUATERNI:93 .= [*(- (Im3 z1)),(- (Im2 z1)),(Im1 z1),(Rea z1)*] by QUATERN2:1, QUATERNI:31 ; z1 * = (((((((Rea z1) * (Rea )) - ((Im1 z1) * (Im1 ))) - ((Im2 z1) * (Im2 ))) - ((Im3 z1) * (Im3 ))) + ((((((Rea z1) * (Im1 )) + ((Im1 z1) * (Rea ))) + ((Im2 z1) * (Im3 ))) - ((Im3 z1) * (Im2 ))) * )) + ((((((Rea z1) * (Im2 )) + ((Im2 z1) * (Rea ))) + ((Im3 z1) * (Im1 ))) - ((Im1 z1) * (Im3 ))) * )) + ((((((Rea z1) * (Im3 )) + ((Im3 z1) * (Rea ))) + ((Im1 z1) * (Im2 ))) - ((Im2 z1) * (Im1 ))) * ) by QUATERNI:93 .= [*(- (Im3 z1)),(Im2 z1),(- (Im1 z1)),(Rea z1)*] by QUATERN2:1, QUATERNI:31 ; then ( * z1) - (z1 * ) = [*((- (Im3 z1)) - (- (Im3 z1))),((- (Im2 z1)) - (Im2 z1)),((Im1 z1) - (- (Im1 z1))),((Rea z1) - (Rea z1))*] by A1, QUATERN2:5 .= [*0,(- (2 * (Im2 z1))),(2 * (Im1 z1)),0*] ; hence ( * z1) - (z1 * ) = [*0,(- (2 * (Im2 z1))),(2 * (Im1 z1)),0*] ; ::_thesis: verum end; theorem :: QUATERN3:23 for z1 being quaternion number holds ( * z1) + (z1 * ) = [*(- (2 * (Im3 z1))),0,0,(2 * (Rea z1))*] proof let z1 be quaternion number ; ::_thesis: ( * z1) + (z1 * ) = [*(- (2 * (Im3 z1))),0,0,(2 * (Rea z1))*] set z = ; A1: * z1 = (((((((Rea ) * (Rea z1)) - ((Im1 ) * (Im1 z1))) - ((Im2 ) * (Im2 z1))) - ((Im3 ) * (Im3 z1))) + ((((((Rea ) * (Im1 z1)) + ((Im1 ) * (Rea z1))) + ((Im2 ) * (Im3 z1))) - ((Im3 ) * (Im2 z1))) * )) + ((((((Rea ) * (Im2 z1)) + ((Im2 ) * (Rea z1))) + ((Im3 ) * (Im1 z1))) - ((Im1 ) * (Im3 z1))) * )) + ((((((Rea ) * (Im3 z1)) + ((Im3 ) * (Rea z1))) + ((Im1 ) * (Im2 z1))) - ((Im2 ) * (Im1 z1))) * ) by QUATERNI:93 .= [*(- (Im3 z1)),(- (Im2 z1)),(Im1 z1),(Rea z1)*] by QUATERN2:1, QUATERNI:31 ; then A2: ( Im2 ( * z1) = Im1 z1 & Im3 ( * z1) = Rea z1 ) by QUATERNI:23; A3: z1 * = (((((((Rea z1) * (Rea )) - ((Im1 z1) * (Im1 ))) - ((Im2 z1) * (Im2 ))) - ((Im3 z1) * (Im3 ))) + ((((((Rea z1) * (Im1 )) + ((Im1 z1) * (Rea ))) + ((Im2 z1) * (Im3 ))) - ((Im3 z1) * (Im2 ))) * )) + ((((((Rea z1) * (Im2 )) + ((Im2 z1) * (Rea ))) + ((Im3 z1) * (Im1 ))) - ((Im1 z1) * (Im3 ))) * )) + ((((((Rea z1) * (Im3 )) + ((Im3 z1) * (Rea ))) + ((Im1 z1) * (Im2 ))) - ((Im2 z1) * (Im1 ))) * ) by QUATERNI:93 .= [*(- (Im3 z1)),(Im2 z1),(- (Im1 z1)),(Rea z1)*] by QUATERN2:1, QUATERNI:31 ; then A4: ( Rea (z1 * ) = - (Im3 z1) & Im1 (z1 * ) = Im2 z1 ) by QUATERNI:23; A5: ( Im2 (z1 * ) = - (Im1 z1) & Im3 (z1 * ) = Rea z1 ) by A3, QUATERNI:23; ( Rea ( * z1) = - (Im3 z1) & Im1 ( * z1) = - (Im2 z1) ) by A1, QUATERNI:23; then (z1 * ) + ( * z1) = ((((- (Im3 z1)) + (- (Im3 z1))) + (((- (Im2 z1)) + (Im2 z1)) * )) + (((Im1 z1) - (Im1 z1)) * )) + (((Rea z1) + (Rea z1)) * ) by A2, A4, A5, QUATERNI:92; hence ( * z1) + (z1 * ) = [*(- (2 * (Im3 z1))),0,0,(2 * (Rea z1))*] by QUATERN2:1; ::_thesis: verum end; theorem Th24: :: QUATERN3:24 for z being quaternion number holds Rea ((1 / (|.z.| ^2)) * (z *')) = (1 / (|.z.| ^2)) * (Rea z) proof let z be quaternion number ; ::_thesis: Rea ((1 / (|.z.| ^2)) * (z *')) = (1 / (|.z.| ^2)) * (Rea z) z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by QUATERNI:43; then (1 / (|.z.| ^2)) * (z *') = [*((1 / (|.z.| ^2)) * (Rea z)),((1 / (|.z.| ^2)) * (- (Im1 z))),((1 / (|.z.| ^2)) * (- (Im2 z))),((1 / (|.z.| ^2)) * (- (Im3 z)))*] by QUATERNI:def_21; hence Rea ((1 / (|.z.| ^2)) * (z *')) = (1 / (|.z.| ^2)) * (Rea z) by QUATERNI:23; ::_thesis: verum end; theorem Th25: :: QUATERN3:25 for z being quaternion number holds Im1 ((1 / (|.z.| ^2)) * (z *')) = - ((1 / (|.z.| ^2)) * (Im1 z)) proof let z be quaternion number ; ::_thesis: Im1 ((1 / (|.z.| ^2)) * (z *')) = - ((1 / (|.z.| ^2)) * (Im1 z)) z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by QUATERNI:43; then (1 / (|.z.| ^2)) * (z *') = [*((1 / (|.z.| ^2)) * (Rea z)),((1 / (|.z.| ^2)) * (- (Im1 z))),((1 / (|.z.| ^2)) * (- (Im2 z))),((1 / (|.z.| ^2)) * (- (Im3 z)))*] by QUATERNI:def_21; hence Im1 ((1 / (|.z.| ^2)) * (z *')) = - ((1 / (|.z.| ^2)) * (Im1 z)) by QUATERNI:23; ::_thesis: verum end; theorem Th26: :: QUATERN3:26 for z being quaternion number holds Im2 ((1 / (|.z.| ^2)) * (z *')) = - ((1 / (|.z.| ^2)) * (Im2 z)) proof let z be quaternion number ; ::_thesis: Im2 ((1 / (|.z.| ^2)) * (z *')) = - ((1 / (|.z.| ^2)) * (Im2 z)) z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by QUATERNI:43; then (1 / (|.z.| ^2)) * (z *') = [*((1 / (|.z.| ^2)) * (Rea z)),((1 / (|.z.| ^2)) * (- (Im1 z))),((1 / (|.z.| ^2)) * (- (Im2 z))),((1 / (|.z.| ^2)) * (- (Im3 z)))*] by QUATERNI:def_21; hence Im2 ((1 / (|.z.| ^2)) * (z *')) = - ((1 / (|.z.| ^2)) * (Im2 z)) by QUATERNI:23; ::_thesis: verum end; theorem Th27: :: QUATERN3:27 for z being quaternion number holds Im3 ((1 / (|.z.| ^2)) * (z *')) = - ((1 / (|.z.| ^2)) * (Im3 z)) proof let z be quaternion number ; ::_thesis: Im3 ((1 / (|.z.| ^2)) * (z *')) = - ((1 / (|.z.| ^2)) * (Im3 z)) z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by QUATERNI:43; then (1 / (|.z.| ^2)) * (z *') = [*((1 / (|.z.| ^2)) * (Rea z)),((1 / (|.z.| ^2)) * (- (Im1 z))),((1 / (|.z.| ^2)) * (- (Im2 z))),((1 / (|.z.| ^2)) * (- (Im3 z)))*] by QUATERNI:def_21; hence Im3 ((1 / (|.z.| ^2)) * (z *')) = - ((1 / (|.z.| ^2)) * (Im3 z)) by QUATERNI:23; ::_thesis: verum end; theorem :: QUATERN3:28 for z being quaternion number holds (1 / (|.z.| ^2)) * (z *') = [*((1 / (|.z.| ^2)) * (Rea z)),(- ((1 / (|.z.| ^2)) * (Im1 z))),(- ((1 / (|.z.| ^2)) * (Im2 z))),(- ((1 / (|.z.| ^2)) * (Im3 z)))*] proof let z be quaternion number ; ::_thesis: (1 / (|.z.| ^2)) * (z *') = [*((1 / (|.z.| ^2)) * (Rea z)),(- ((1 / (|.z.| ^2)) * (Im1 z))),(- ((1 / (|.z.| ^2)) * (Im2 z))),(- ((1 / (|.z.| ^2)) * (Im3 z)))*] set zz = |.z.| ^2 ; (1 / (|.z.| ^2)) * (z *') = [*(Rea ((1 / (|.z.| ^2)) * (z *'))),(Im1 ((1 / (|.z.| ^2)) * (z *'))),(Im2 ((1 / (|.z.| ^2)) * (z *'))),(Im3 ((1 / (|.z.| ^2)) * (z *')))*] by QUATERNI:24; then (1 / (|.z.| ^2)) * (z *') = [*((1 / (|.z.| ^2)) * (Rea z)),(Im1 ((1 / (|.z.| ^2)) * (z *'))),(Im2 ((1 / (|.z.| ^2)) * (z *'))),(Im3 ((1 / (|.z.| ^2)) * (z *')))*] by Th24; then (1 / (|.z.| ^2)) * (z *') = [*((1 / (|.z.| ^2)) * (Rea z)),(- ((1 / (|.z.| ^2)) * (Im1 z))),(Im2 ((1 / (|.z.| ^2)) * (z *'))),(Im3 ((1 / (|.z.| ^2)) * (z *')))*] by Th25; then (1 / (|.z.| ^2)) * (z *') = [*((1 / (|.z.| ^2)) * (Rea z)),(- ((1 / (|.z.| ^2)) * (Im1 z))),(- ((1 / (|.z.| ^2)) * (Im2 z))),(Im3 ((1 / (|.z.| ^2)) * (z *')))*] by Th26; hence (1 / (|.z.| ^2)) * (z *') = [*((1 / (|.z.| ^2)) * (Rea z)),(- ((1 / (|.z.| ^2)) * (Im1 z))),(- ((1 / (|.z.| ^2)) * (Im2 z))),(- ((1 / (|.z.| ^2)) * (Im3 z)))*] by Th27; ::_thesis: verum end; theorem :: QUATERN3:29 for z being quaternion number holds z * ((1 / (|.z.| ^2)) * (z *')) = [*((|.z.| ^2) / (|.z.| ^2)),0,0,0*] proof let z be quaternion number ; ::_thesis: z * ((1 / (|.z.| ^2)) * (z *')) = [*((|.z.| ^2) / (|.z.| ^2)),0,0,0*] set zz = |.z.| ^2 ; set z3 = (1 / (|.z.| ^2)) * (z *'); z * ((1 / (|.z.| ^2)) * (z *')) = (((((((Rea z) * (Rea ((1 / (|.z.| ^2)) * (z *')))) - ((Im1 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))) + ((((((Rea z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))) + ((Im1 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im2 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) * )) + ((((((Rea z) * (Im2 ((1 / (|.z.| ^2)) * (z *')))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))) * )) + ((((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) * ) by QUATERNI:93 .= [*(((((Rea z) * (Rea ((1 / (|.z.| ^2)) * (z *')))) - ((Im1 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))) + ((Im1 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im2 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2)) * (z *')))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by QUATERN2:1 .= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))) + ((Im1 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im2 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2)) * (z *')))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th24 .= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))) + ((Im1 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im2 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2)) * (z *')))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th25 .= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))) + ((Im1 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im2 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2)) * (z *')))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th26 .= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))) + ((Im1 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im2 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2)) * (z *')))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th27 .= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im2 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2)) * (z *')))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th25 .= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im2 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2)) * (z *')))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th24 .= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))) - ((Im3 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2)) * (z *')))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th27 .= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))),(((((Rea z) * (Im2 ((1 / (|.z.| ^2)) * (z *')))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th26 .= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im2 z)))) + ((Im2 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th26 .= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im2 z)))) + ((Im2 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im3 z) * (Im1 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th24 .= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im2 z)))) + ((Im2 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im1 z) * (Im3 ((1 / (|.z.| ^2)) * (z *'))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th25 .= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im2 z)))) + ((Im2 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (Im3 ((1 / (|.z.| ^2)) * (z *')))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th27 .= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im2 z)))) + ((Im2 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im3 z)))) + ((Im3 z) * (Rea ((1 / (|.z.| ^2)) * (z *'))))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th27 .= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im2 z)))) + ((Im2 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im3 z)))) + ((Im3 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im1 z) * (Im2 ((1 / (|.z.| ^2)) * (z *'))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th24 .= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im2 z)))) + ((Im2 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im3 z)))) + ((Im3 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im2 z) * (Im1 ((1 / (|.z.| ^2)) * (z *')))))*] by Th26 .= [*(((((Rea z) * ((1 / (|.z.| ^2)) * (Rea z))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))) + ((Im1 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))) - ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im2 z)))) + ((Im2 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im3 z) * (- ((1 / (|.z.| ^2)) * (Im1 z))))) - ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im3 z))))),(((((Rea z) * (- ((1 / (|.z.| ^2)) * (Im3 z)))) + ((Im3 z) * ((1 / (|.z.| ^2)) * (Rea z)))) + ((Im1 z) * (- ((1 / (|.z.| ^2)) * (Im2 z))))) - ((Im2 z) * (- ((1 / (|.z.| ^2)) * (Im1 z)))))*] by Th25 .= [*((((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)) / (|.z.| ^2)),0,0,0*] .= [*((|.z.| ^2) / (|.z.| ^2)),0,0,0*] by Th11 ; hence z * ((1 / (|.z.| ^2)) * (z *')) = [*((|.z.| ^2) / (|.z.| ^2)),0,0,0*] ; ::_thesis: verum end; theorem :: QUATERN3:30 for z1, z2, z3 being quaternion number holds |.((z1 * z2) * z3).| ^2 = ((|.z1.| ^2) * (|.z2.| ^2)) * (|.z3.| ^2) proof let z1, z2, z3 be quaternion number ; ::_thesis: |.((z1 * z2) * z3).| ^2 = ((|.z1.| ^2) * (|.z2.| ^2)) * (|.z3.| ^2) |.((z1 * z2) * z3).| ^2 = |.(z1 * (z2 * z3)).| ^2 by QUATERN2:16 .= (|.z1.| ^2) * (|.(z2 * z3).| ^2) by Th17 .= (|.z1.| ^2) * ((|.z2.| ^2) * (|.z3.| ^2)) by Th17 .= ((|.z1.| ^2) * (|.z2.| ^2)) * (|.z3.| ^2) ; hence |.((z1 * z2) * z3).| ^2 = ((|.z1.| ^2) * (|.z2.| ^2)) * (|.z3.| ^2) ; ::_thesis: verum end; theorem :: QUATERN3:31 for z1, z2, z3 being quaternion number holds Rea ((z1 * z2) * z3) = Rea ((z3 * z1) * z2) proof let z1, z2, z3 be quaternion number ; ::_thesis: Rea ((z1 * z2) * z3) = Rea ((z3 * z1) * z2) Rea ((z1 * z2) * z3) = Rea (z1 * (z2 * z3)) by QUATERN2:16 .= Rea ((z2 * z3) * z1) by Th1 .= Rea (z2 * (z3 * z1)) by QUATERN2:16 .= Rea ((z3 * z1) * z2) by Th1 ; hence Rea ((z1 * z2) * z3) = Rea ((z3 * z1) * z2) ; ::_thesis: verum end; theorem Th32: :: QUATERN3:32 for z being quaternion number holds |.(z * z).| = |.((z *') * (z *')).| proof let z be quaternion number ; ::_thesis: |.(z * z).| = |.((z *') * (z *')).| |.((z *') * (z *')).| = |.(z *').| * |.(z *').| by QUATERNI:87 .= |.z.| * |.(z *').| by QUATERNI:73 .= |.z.| * |.z.| by QUATERNI:73 ; hence |.(z * z).| = |.((z *') * (z *')).| by QUATERNI:87; ::_thesis: verum end; theorem :: QUATERN3:33 for z being quaternion number holds |.((z *') * (z *')).| = |.z.| ^2 proof let z be quaternion number ; ::_thesis: |.((z *') * (z *')).| = |.z.| ^2 |.((z *') * (z *')).| = |.(z * z).| by Th32; hence |.((z *') * (z *')).| = |.z.| ^2 by QUATERNI:87; ::_thesis: verum end; theorem :: QUATERN3:34 for z1, z2, z3 being quaternion number holds |.((z1 * z2) * z3).| = (|.z1.| * |.z2.|) * |.z3.| proof let z1, z2, z3 be quaternion number ; ::_thesis: |.((z1 * z2) * z3).| = (|.z1.| * |.z2.|) * |.z3.| |.((z1 * z2) * z3).| = |.(z1 * (z2 * z3)).| by QUATERN2:16 .= |.z1.| * |.(z2 * z3).| by QUATERNI:87 .= |.z1.| * (|.z2.| * |.z3.|) by QUATERNI:87 .= (|.z1.| * |.z2.|) * |.z3.| ; hence |.((z1 * z2) * z3).| = (|.z1.| * |.z2.|) * |.z3.| ; ::_thesis: verum end; theorem :: QUATERN3:35 for z1, z2, z3 being quaternion number holds |.((z1 + z2) + z3).| <= (|.z1.| + |.z2.|) + |.z3.| proof let z1, z2, z3 be quaternion number ; ::_thesis: |.((z1 + z2) + z3).| <= (|.z1.| + |.z2.|) + |.z3.| |.((z1 + z2) + z3).| = |.(z1 + (z2 + z3)).| by QUATERN2:2; then |.((z1 + z2) + z3).| <= |.z1.| + |.(z2 + z3).| by QUATERNI:79; then A1: |.((z1 + z2) + z3).| - |.z1.| <= |.(z2 + z3).| by XREAL_1:20; |.(z2 + z3).| <= |.z2.| + |.z3.| by QUATERNI:79; then (|.((z1 + z2) + z3).| - |.z1.|) + |.(z2 + z3).| <= |.(z2 + z3).| + (|.z2.| + |.z3.|) by A1, XREAL_1:7; then |.((z1 + z2) + z3).| - |.z1.| <= (|.(z2 + z3).| + (|.z2.| + |.z3.|)) - |.(z2 + z3).| by XREAL_1:19; then |.((z1 + z2) + z3).| <= (|.z2.| + |.z3.|) + |.z1.| by XREAL_1:20; hence |.((z1 + z2) + z3).| <= (|.z1.| + |.z2.|) + |.z3.| ; ::_thesis: verum end; theorem :: QUATERN3:36 for z1, z2, z3 being quaternion number holds |.((z1 + z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.| proof let z1, z2, z3 be quaternion number ; ::_thesis: |.((z1 + z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.| |.((z1 + z2) - z3).| = |.(z1 + (z2 - z3)).| by QUATERN2:2; then |.((z1 + z2) - z3).| <= |.z1.| + |.(z2 - z3).| by QUATERNI:79; then A1: |.((z1 + z2) - z3).| - |.z1.| <= |.(z2 - z3).| by XREAL_1:20; |.(z2 - z3).| <= |.z2.| + |.z3.| by QUATERNI:80; then (|.((z1 + z2) - z3).| - |.z1.|) + |.(z2 - z3).| <= |.(z2 - z3).| + (|.z2.| + |.z3.|) by A1, XREAL_1:7; then |.((z1 + z2) - z3).| - |.z1.| <= (|.(z2 - z3).| + (|.z2.| + |.z3.|)) - |.(z2 - z3).| by XREAL_1:19; then |.((z1 + z2) - z3).| <= (|.z2.| + |.z3.|) + |.z1.| by XREAL_1:20; hence |.((z1 + z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.| ; ::_thesis: verum end; theorem :: QUATERN3:37 for z1, z2, z3 being quaternion number holds |.((z1 - z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.| proof let z1, z2, z3 be quaternion number ; ::_thesis: |.((z1 - z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.| ( |.((z1 - z2) - z3).| <= |.(z1 - z2).| + |.z3.| & |.(z1 - z2).| <= |.z1.| + |.z2.| ) by QUATERNI:80; then |.((z1 - z2) - z3).| + |.(z1 - z2).| <= (|.(z1 - z2).| + |.z3.|) + (|.z1.| + |.z2.|) by XREAL_1:7; then |.((z1 - z2) - z3).| <= ((|.(z1 - z2).| + |.z3.|) + (|.z1.| + |.z2.|)) - |.(z1 - z2).| by XREAL_1:19; hence |.((z1 - z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.| ; ::_thesis: verum end; theorem :: QUATERN3:38 for z1, z2 being quaternion number holds |.z1.| - |.z2.| <= (|.(z1 + z2).| + |.(z1 - z2).|) / 2 proof let z1, z2 be quaternion number ; ::_thesis: |.z1.| - |.z2.| <= (|.(z1 + z2).| + |.(z1 - z2).|) / 2 ( |.z1.| - |.z2.| <= |.(z1 + z2).| & |.z1.| - |.z2.| <= |.(z1 - z2).| ) by QUATERNI:81, QUATERNI:82; then (|.z1.| - |.z2.|) + (|.z1.| - |.z2.|) <= |.(z1 + z2).| + |.(z1 - z2).| by XREAL_1:7; then 2 * (|.z1.| - |.z2.|) <= |.(z1 + z2).| + |.(z1 - z2).| ; hence |.z1.| - |.z2.| <= (|.(z1 + z2).| + |.(z1 - z2).|) / 2 by XREAL_1:77; ::_thesis: verum end; theorem :: QUATERN3:39 for z1, z2 being quaternion number holds |.z1.| - |.z2.| <= (|.(z1 + z2).| + |.(z2 - z1).|) / 2 proof let z1, z2 be quaternion number ; ::_thesis: |.z1.| - |.z2.| <= (|.(z1 + z2).| + |.(z2 - z1).|) / 2 ( |.z1.| - |.z2.| <= |.(z1 + z2).| & |.z1.| - |.z2.| <= |.(z1 - z2).| ) by QUATERNI:81, QUATERNI:82; then (|.z1.| - |.z2.|) + (|.z1.| - |.z2.|) <= |.(z1 + z2).| + |.(z1 - z2).| by XREAL_1:7; then 2 * (|.z1.| - |.z2.|) <= |.(z1 + z2).| + |.(z2 - z1).| by QUATERNI:83; hence |.z1.| - |.z2.| <= (|.(z1 + z2).| + |.(z2 - z1).|) / 2 by XREAL_1:77; ::_thesis: verum end; theorem :: QUATERN3:40 for z1, z2 being quaternion number holds |.(|.z1.| - |.z2.|).| <= |.(z2 - z1).| proof let z1, z2 be quaternion number ; ::_thesis: |.(|.z1.| - |.z2.|).| <= |.(z2 - z1).| |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).| by QUATERNI:86; hence |.(|.z1.| - |.z2.|).| <= |.(z2 - z1).| by QUATERNI:83; ::_thesis: verum end; theorem :: QUATERN3:41 for z1, z2 being quaternion number holds |.(|.z1.| - |.z2.|).| <= |.z1.| + |.z2.| proof let z1, z2 be quaternion number ; ::_thesis: |.(|.z1.| - |.z2.|).| <= |.z1.| + |.z2.| ( |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).| & |.(z1 - z2).| <= |.z1.| + |.z2.| ) by QUATERNI:80, QUATERNI:86; then |.(|.z1.| - |.z2.|).| + |.(z1 - z2).| <= |.(z1 - z2).| + (|.z1.| + |.z2.|) by XREAL_1:7; then |.(|.z1.| - |.z2.|).| <= ((|.(z1 - z2).| + |.z1.|) + |.z2.|) - |.(z1 - z2).| by XREAL_1:19; hence |.(|.z1.| - |.z2.|).| <= |.z1.| + |.z2.| ; ::_thesis: verum end; theorem :: QUATERN3:42 for z1, z2, z being quaternion number holds |.z1.| - |.z2.| <= |.(z1 - z).| + |.(z - z2).| proof let z1, z2, z be quaternion number ; ::_thesis: |.z1.| - |.z2.| <= |.(z1 - z).| + |.(z - z2).| ( |.z1.| - |.z2.| <= |.(z1 - z2).| & |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).| ) by QUATERNI:82, QUATERNI:85; then (|.z1.| - |.z2.|) + |.(z1 - z2).| <= |.(z1 - z2).| + (|.(z1 - z).| + |.(z - z2).|) by XREAL_1:7; then |.z1.| - |.z2.| <= ((|.(z1 - z2).| + |.(z1 - z).|) + |.(z - z2).|) - |.(z1 - z2).| by XREAL_1:19; hence |.z1.| - |.z2.| <= |.(z1 - z).| + |.(z - z2).| ; ::_thesis: verum end; theorem :: QUATERN3:43 for z1, z2 being quaternion number st |.z1.| - |.z2.| <> 0 holds ((|.z1.| ^2) + (|.z2.| ^2)) - ((2 * |.z1.|) * |.z2.|) > 0 proof let z1, z2 be quaternion number ; ::_thesis: ( |.z1.| - |.z2.| <> 0 implies ((|.z1.| ^2) + (|.z2.| ^2)) - ((2 * |.z1.|) * |.z2.|) > 0 ) assume |.z1.| - |.z2.| <> 0 ; ::_thesis: ((|.z1.| ^2) + (|.z2.| ^2)) - ((2 * |.z1.|) * |.z2.|) > 0 then (|.z1.| - |.z2.|) ^2 > 0 by SQUARE_1:12; hence ((|.z1.| ^2) + (|.z2.| ^2)) - ((2 * |.z1.|) * |.z2.|) > 0 ; ::_thesis: verum end; theorem :: QUATERN3:44 for z1, z2 being quaternion number holds |.z1.| + |.z2.| >= (|.(z1 + z2).| + |.(z2 - z1).|) / 2 proof let z1, z2 be quaternion number ; ::_thesis: |.z1.| + |.z2.| >= (|.(z1 + z2).| + |.(z2 - z1).|) / 2 ( |.(z1 + z2).| <= |.z1.| + |.z2.| & |.(z1 - z2).| <= |.z1.| + |.z2.| ) by QUATERNI:79, QUATERNI:80; then |.(z1 + z2).| + |.(z1 - z2).| <= (|.z1.| + |.z2.|) + (|.z1.| + |.z2.|) by XREAL_1:7; then |.(z1 + z2).| + |.(z2 - z1).| <= 2 * (|.z1.| + |.z2.|) by QUATERNI:83; hence |.z1.| + |.z2.| >= (|.(z1 + z2).| + |.(z2 - z1).|) / 2 by XREAL_1:79; ::_thesis: verum end; theorem :: QUATERN3:45 for z1, z2 being quaternion number holds |.z1.| + |.z2.| >= (|.(z1 + z2).| + |.(z1 - z2).|) / 2 proof let z1, z2 be quaternion number ; ::_thesis: |.z1.| + |.z2.| >= (|.(z1 + z2).| + |.(z1 - z2).|) / 2 ( |.(z1 + z2).| <= |.z1.| + |.z2.| & |.(z1 - z2).| <= |.z1.| + |.z2.| ) by QUATERNI:79, QUATERNI:80; then |.(z1 + z2).| + |.(z1 - z2).| <= (|.z1.| + |.z2.|) + (|.z1.| + |.z2.|) by XREAL_1:7; then |.(z1 + z2).| + |.(z1 - z2).| <= 2 * (|.z1.| + |.z2.|) ; hence |.z1.| + |.z2.| >= (|.(z1 + z2).| + |.(z1 - z2).|) / 2 by XREAL_1:79; ::_thesis: verum end; theorem :: QUATERN3:46 for z1, z2 being quaternion number holds (z1 * z2) " = (z2 ") * (z1 ") proof let z1, z2 be quaternion number ; ::_thesis: (z1 * z2) " = (z2 ") * (z1 ") set z3 = z1 * z2; A1: ((((Rea (z2 ")) * (Im1 (z1 "))) + ((Im1 (z2 ")) * (Rea (z1 ")))) + ((Im2 (z2 ")) * (Im3 (z1 ")))) - ((Im3 (z2 ")) * (Im2 (z1 "))) = (((((Rea z2) / (|.z2.| ^2)) * (Im1 (z1 "))) + ((Im1 (z2 ")) * (Rea (z1 ")))) + ((Im2 (z2 ")) * (Im3 (z1 ")))) - ((Im3 (z2 ")) * (Im2 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im1 z1) / (|.z1.| ^2)))) + ((Im1 (z2 ")) * (Rea (z1 ")))) + ((Im2 (z2 ")) * (Im3 (z1 ")))) - ((Im3 (z2 ")) * (Im2 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im1 z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * (Rea (z1 ")))) + ((Im2 (z2 ")) * (Im3 (z1 ")))) - ((Im3 (z2 ")) * (Im2 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im1 z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((Im2 (z2 ")) * (Im3 (z1 ")))) - ((Im3 (z2 ")) * (Im2 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im1 z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * (Im3 (z1 ")))) - ((Im3 (z2 ")) * (Im2 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im1 z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im3 z1) / (|.z1.| ^2))))) - ((Im3 (z2 ")) * (Im2 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im1 z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im3 z1) / (|.z1.| ^2))))) - ((- ((Im3 z2) / (|.z2.| ^2))) * (Im2 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * ((- (Im1 z1)) / (|.z1.| ^2))) + ((- ((Im1 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im3 z1) / (|.z1.| ^2))))) - ((- ((Im3 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2)))) by QUATERN2:29 .= (((((Rea z2) * (- (Im1 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) + (((- (Im1 z2)) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im3 z1) / (|.z1.| ^2))))) - ((- ((Im3 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2)))) by XCMPLX_1:76 .= (((((Rea z2) * (- (Im1 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) + (((- (Im1 z2)) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) + (((Im2 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2)))) - ((- ((Im3 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2)))) by XCMPLX_1:76 .= (((((Rea z2) * (- (Im1 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) + (((- (Im1 z2)) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) + (((Im2 z2) * (Im3 z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) - (((Im3 z2) / (|.z2.| ^2)) * ((Im2 z1) / (|.z1.| ^2))) by XCMPLX_1:76 .= (((((Rea z2) * (- (Im1 z1))) + ((- (Im1 z2)) * (Rea z1))) + ((Im2 z2) * (Im3 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im3 z2) * (Im2 z1)) / ((|.z2.| ^2) * (|.z1.| ^2))) by XCMPLX_1:76 .= (((((Rea z2) * (- (Im1 z1))) + ((- (Im1 z2)) * (Rea z1))) + ((Im2 z2) * (Im3 z1))) - ((Im3 z2) * (Im2 z1))) / ((|.z2.| * |.z1.|) ^2) ; A2: ((((Rea (z2 ")) * (Im2 (z1 "))) + ((Im2 (z2 ")) * (Rea (z1 ")))) + ((Im3 (z2 ")) * (Im1 (z1 ")))) - ((Im1 (z2 ")) * (Im3 (z1 "))) = (((((Rea z2) / (|.z2.| ^2)) * (Im2 (z1 "))) + ((Im2 (z2 ")) * (Rea (z1 ")))) + ((Im3 (z2 ")) * (Im1 (z1 ")))) - ((Im1 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im2 z1) / (|.z1.| ^2)))) + ((Im2 (z2 ")) * (Rea (z1 ")))) + ((Im3 (z2 ")) * (Im1 (z1 ")))) - ((Im1 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im2 z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * (Rea (z1 ")))) + ((Im3 (z2 ")) * (Im1 (z1 ")))) - ((Im1 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im2 z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((Im3 (z2 ")) * (Im1 (z1 ")))) - ((Im1 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im2 z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * (Im1 (z1 ")))) - ((Im1 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im2 z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((Im1 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im2 z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (Im3 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im2 z1) / (|.z1.| ^2)))) + ((- ((Im2 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im3 z1) / (|.z1.| ^2)))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * ((- (Im2 z1)) / (|.z1.| ^2))) + (((- (Im2 z2)) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2)))) + (((Im3 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2)))) - (((Im1 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2))) .= (((((Rea z2) * (- (Im2 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) + (((- (Im2 z2)) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2)))) + (((Im3 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2)))) - (((Im1 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2))) by XCMPLX_1:76 .= (((((Rea z2) * (- (Im2 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) + (((- (Im2 z2)) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) + (((Im3 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2)))) - (((Im1 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2))) by XCMPLX_1:76 .= (((((Rea z2) * (- (Im2 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) + (((- (Im2 z2)) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) + (((Im3 z2) * (Im1 z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) - (((Im1 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2))) by XCMPLX_1:76 .= (((((Rea z2) * (- (Im2 z1))) + ((- (Im2 z2)) * (Rea z1))) + ((Im3 z2) * (Im1 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im1 z2) * (Im3 z1)) / ((|.z2.| ^2) * (|.z1.| ^2))) by XCMPLX_1:76 .= (((((Rea z2) * (- (Im2 z1))) + ((- (Im2 z2)) * (Rea z1))) + ((Im3 z2) * (Im1 z1))) - ((Im1 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2) ; A3: ((((Rea (z2 ")) * (Im3 (z1 "))) + ((Im3 (z2 ")) * (Rea (z1 ")))) + ((Im1 (z2 ")) * (Im2 (z1 ")))) - ((Im2 (z2 ")) * (Im1 (z1 "))) = (((((Rea z2) / (|.z2.| ^2)) * (Im3 (z1 "))) + ((Im3 (z2 ")) * (Rea (z1 ")))) + ((Im1 (z2 ")) * (Im2 (z1 ")))) - ((Im2 (z2 ")) * (Im1 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im3 z1) / (|.z1.| ^2)))) + ((Im3 (z2 ")) * (Rea (z1 ")))) + ((Im1 (z2 ")) * (Im2 (z1 ")))) - ((Im2 (z2 ")) * (Im1 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im3 z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * (Rea (z1 ")))) + ((Im1 (z2 ")) * (Im2 (z1 ")))) - ((Im2 (z2 ")) * (Im1 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im3 z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((Im1 (z2 ")) * (Im2 (z1 ")))) - ((Im2 (z2 ")) * (Im1 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im3 z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * (Im2 (z1 ")))) - ((Im2 (z2 ")) * (Im1 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im3 z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2))))) - ((Im2 (z2 ")) * (Im1 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im3 z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2))))) - ((- ((Im2 z2) / (|.z2.| ^2))) * (Im1 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * (- ((Im3 z1) / (|.z1.| ^2)))) + ((- ((Im3 z2) / (|.z2.| ^2))) * ((Rea z1) / (|.z1.| ^2)))) + ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2))))) - ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2)))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * ((- (Im3 z1)) / (|.z1.| ^2))) - (((Im3 z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2)))) + (((Im1 z2) / (|.z2.| ^2)) * ((Im2 z1) / (|.z1.| ^2)))) - (((Im2 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2))) .= (((((Rea z2) * (- (Im3 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im3 z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2)))) + (((Im1 z2) / (|.z2.| ^2)) * ((Im2 z1) / (|.z1.| ^2)))) - (((Im2 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2))) by XCMPLX_1:76 .= (((((Rea z2) * (- (Im3 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im3 z2) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) + (((Im1 z2) / (|.z2.| ^2)) * ((Im2 z1) / (|.z1.| ^2)))) - (((Im2 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2))) by XCMPLX_1:76 .= (((((Rea z2) * (- (Im3 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im3 z2) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) + (((Im1 z2) * (Im2 z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) - (((Im2 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2))) by XCMPLX_1:76 .= (((((Rea z2) * (- (Im3 z1))) - ((Im3 z2) * (Rea z1))) + ((Im1 z2) * (Im2 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im2 z2) * (Im1 z1)) / ((|.z2.| ^2) * (|.z1.| ^2))) by XCMPLX_1:76 .= (((((Rea z2) * (- (Im3 z1))) - ((Im3 z2) * (Rea z1))) + ((Im1 z2) * (Im2 z1))) - ((Im2 z2) * (Im1 z1))) / ((|.z2.| * |.z1.|) ^2) ; ((((Rea (z2 ")) * (Rea (z1 "))) - ((Im1 (z2 ")) * (Im1 (z1 ")))) - ((Im2 (z2 ")) * (Im2 (z1 ")))) - ((Im3 (z2 ")) * (Im3 (z1 "))) = (((((Rea z2) / (|.z2.| ^2)) * (Rea (z1 "))) - ((Im1 (z2 ")) * (Im1 (z1 ")))) - ((Im2 (z2 ")) * (Im2 (z1 ")))) - ((Im3 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2))) - ((Im1 (z2 ")) * (Im1 (z1 ")))) - ((Im2 (z2 ")) * (Im2 (z1 ")))) - ((Im3 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (Im1 (z1 ")))) - ((Im2 (z2 ")) * (Im2 (z1 ")))) - ((Im3 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((Im2 (z2 ")) * (Im2 (z1 ")))) - ((Im3 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((- ((Im2 z2) / (|.z2.| ^2))) * (Im2 (z1 ")))) - ((Im3 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2))))) - ((Im3 (z2 ")) * (Im3 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2))))) - ((- ((Im3 z2) / (|.z2.| ^2))) * (Im3 (z1 "))) by QUATERN2:29 .= (((((Rea z2) / (|.z2.| ^2)) * ((Rea z1) / (|.z1.| ^2))) - ((- ((Im1 z2) / (|.z2.| ^2))) * (- ((Im1 z1) / (|.z1.| ^2))))) - ((- ((Im2 z2) / (|.z2.| ^2))) * (- ((Im2 z1) / (|.z1.| ^2))))) - ((- ((Im3 z2) / (|.z2.| ^2))) * (- ((Im3 z1) / (|.z1.| ^2)))) by QUATERN2:29 .= (((((Rea z2) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im1 z2) / (|.z2.| ^2)) * ((Im1 z1) / (|.z1.| ^2)))) - (((Im2 z2) / (|.z2.| ^2)) * ((Im2 z1) / (|.z1.| ^2)))) - (((Im3 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2))) by XCMPLX_1:76 .= (((((Rea z2) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im1 z2) * (Im1 z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) - (((Im2 z2) / (|.z2.| ^2)) * ((Im2 z1) / (|.z1.| ^2)))) - (((Im3 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2))) by XCMPLX_1:76 .= (((((Rea z2) * (Rea z1)) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im1 z2) * (Im1 z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) - (((Im2 z2) * (Im2 z1)) / ((|.z2.| ^2) * (|.z1.| ^2)))) - (((Im3 z2) / (|.z2.| ^2)) * ((Im3 z1) / (|.z1.| ^2))) by XCMPLX_1:76 .= (((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) / ((|.z2.| ^2) * (|.z1.| ^2))) - (((Im3 z2) * (Im3 z1)) / ((|.z2.| ^2) * (|.z1.| ^2))) by XCMPLX_1:76 .= (((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) - ((Im3 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2) ; then A4: (z2 ") * (z1 ") = ((((((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) - ((Im3 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2)) + ((- ((((((Rea z2) * (Im1 z1)) + ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / ((|.z2.| * |.z1.|) ^2))) * )) + ((- ((((((Rea z2) * (Im2 z1)) + ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) + ((Im1 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2))) * )) + ((- ((((((Rea z2) * (Im3 z1)) + ((Im3 z2) * (Rea z1))) - ((Im1 z2) * (Im2 z1))) + ((Im2 z2) * (Im1 z1))) / ((|.z2.| * |.z1.|) ^2))) * ) by A1, A2, A3, QUATERNI:93 .= ((((((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) - ((Im3 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2)) + (- (((((((Rea z2) * (Im1 z1)) + ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / ((|.z2.| * |.z1.|) ^2)) * ))) + ((- ((((((Rea z2) * (Im2 z1)) + ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) + ((Im1 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2))) * )) + ((- ((((((Rea z2) * (Im3 z1)) + ((Im3 z2) * (Rea z1))) - ((Im1 z2) * (Im2 z1))) + ((Im2 z2) * (Im1 z1))) / ((|.z2.| * |.z1.|) ^2))) * ) by QUATERN2:9 .= ((((((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) - ((Im3 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2)) + (- (((((((Rea z2) * (Im1 z1)) + ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / ((|.z2.| * |.z1.|) ^2)) * ))) + (- (((((((Rea z2) * (Im2 z1)) + ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) + ((Im1 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2)) * ))) + ((- ((((((Rea z2) * (Im3 z1)) + ((Im3 z2) * (Rea z1))) - ((Im1 z2) * (Im2 z1))) + ((Im2 z2) * (Im1 z1))) / ((|.z2.| * |.z1.|) ^2))) * ) by QUATERN2:9 .= ((((((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) - ((Im3 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2)) - (((((((Rea z2) * (Im1 z1)) + ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / ((|.z2.| * |.z1.|) ^2)) * )) - (((((((Rea z2) * (Im2 z1)) + ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) + ((Im1 z2) * (Im3 z1))) / ((|.z2.| * |.z1.|) ^2)) * )) - (((((((Rea z2) * (Im3 z1)) + ((Im3 z2) * (Rea z1))) - ((Im1 z2) * (Im2 z1))) + ((Im2 z2) * (Im1 z1))) / ((|.z2.| * |.z1.|) ^2)) * ) by QUATERN2:9 ; (z1 * z2) " = ((((Rea (z1 * z2)) / (|.(z1 * z2).| ^2)) - (((Im1 (z1 * z2)) / (|.(z1 * z2).| ^2)) * )) - (((Im2 (z1 * z2)) / (|.(z1 * z2).| ^2)) * )) - (((Im3 (z1 * z2)) / (|.(z1 * z2).| ^2)) * ) by QUATERN2:28 .= ((((Rea (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) - (((Im1 (z1 * z2)) / (|.(z1 * z2).| ^2)) * )) - (((Im2 (z1 * z2)) / (|.(z1 * z2).| ^2)) * )) - (((Im3 (z1 * z2)) / (|.(z1 * z2).| ^2)) * ) by QUATERNI:87 .= ((((Rea (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) - (((Im1 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * )) - (((Im2 (z1 * z2)) / (|.(z1 * z2).| ^2)) * )) - (((Im3 (z1 * z2)) / (|.(z1 * z2).| ^2)) * ) by QUATERNI:87 .= ((((Rea (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) - (((Im1 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * )) - (((Im2 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * )) - (((Im3 (z1 * z2)) / (|.(z1 * z2).| ^2)) * ) by QUATERNI:87 .= ((((Rea (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) - (((Im1 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * )) - (((Im2 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * )) - (((Im3 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * ) by QUATERNI:87 .= ((((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) / ((|.z1.| * |.z2.|) ^2)) - (((Im1 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * )) - (((Im2 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * )) - (((Im3 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * ) by QUATERNI:97 .= ((((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) / ((|.z1.| * |.z2.|) ^2)) - (((((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))) / ((|.z1.| * |.z2.|) ^2)) * )) - (((Im2 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * )) - (((Im3 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * ) by QUATERNI:97 .= ((((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) / ((|.z1.| * |.z2.|) ^2)) - (((((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))) / ((|.z1.| * |.z2.|) ^2)) * )) - (((((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2))) / ((|.z1.| * |.z2.|) ^2)) * )) - (((Im3 (z1 * z2)) / ((|.z1.| * |.z2.|) ^2)) * ) by QUATERNI:97 .= ((((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) / ((|.z1.| * |.z2.|) ^2)) - (((((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))) / ((|.z1.| * |.z2.|) ^2)) * )) - (((((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2))) / ((|.z1.| * |.z2.|) ^2)) * )) - (((((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2))) / ((|.z1.| * |.z2.|) ^2)) * ) by QUATERNI:97 ; hence (z1 * z2) " = (z2 ") * (z1 ") by A4; ::_thesis: verum end; theorem :: QUATERN3:47 for z being quaternion number holds (z *') " = (z ") *' proof let z be quaternion number ; ::_thesis: (z *') " = (z ") *' Im1 ((z *') ") = - ((Im1 (z *')) / (|.(z *').| ^2)) by QUATERN2:29; then A1: Im1 ((z *') ") = - ((- (Im1 z)) / (|.(z *').| ^2)) by QUATERNI:44; Im2 ((z *') ") = - ((Im2 (z *')) / (|.(z *').| ^2)) by QUATERN2:29; then A2: Im2 ((z *') ") = - ((- (Im2 z)) / (|.(z *').| ^2)) by QUATERNI:44; Im2 ((z ") *') = - (Im2 (z ")) by QUATERNI:44; then Im2 ((z ") *') = - (- ((Im2 z) / (|.z.| ^2))) by QUATERN2:29; then A3: Im2 ((z ") *') = - (- ((Im2 z) / (|.(z *').| ^2))) by QUATERNI:73; Im1 ((z ") *') = - (Im1 (z ")) by QUATERNI:44; then Im1 ((z ") *') = - (- ((Im1 z) / (|.z.| ^2))) by QUATERN2:29; then A4: Im1 ((z ") *') = - (- ((Im1 z) / (|.(z *').| ^2))) by QUATERNI:73; Im3 ((z ") *') = - (Im3 (z ")) by QUATERNI:44; then Im3 ((z ") *') = - (- ((Im3 z) / (|.z.| ^2))) by QUATERN2:29; then A5: Im3 ((z ") *') = - (- ((Im3 z) / (|.(z *').| ^2))) by QUATERNI:73; Rea ((z ") *') = Rea (z ") by QUATERNI:44; then Rea ((z ") *') = (Rea z) / (|.z.| ^2) by QUATERN2:29; then A6: Rea ((z ") *') = (Rea z) / (|.(z *').| ^2) by QUATERNI:73; Im3 ((z *') ") = - ((Im3 (z *')) / (|.(z *').| ^2)) by QUATERN2:29; then A7: Im3 ((z *') ") = - ((- (Im3 z)) / (|.(z *').| ^2)) by QUATERNI:44; Rea ((z *') ") = (Rea (z *')) / (|.(z *').| ^2) by QUATERN2:29; then Rea ((z *') ") = (Rea z) / (|.(z *').| ^2) by QUATERNI:44; hence (z *') " = (z ") *' by A1, A2, A7, A6, A4, A3, A5, QUATERNI:25; ::_thesis: verum end; theorem :: QUATERN3:48 1q " = 1q proof A1: Im3 (1q ") = - ((Im3 1q) / (|.1q.| ^2)) by QUATERN2:29 .= 0 by QUATERNI:29 ; A2: Im2 (1q ") = - ((Im2 1q) / (|.1q.| ^2)) by QUATERN2:29 .= 0 by QUATERNI:29 ; A3: Im1 (1q ") = - ((Im1 1q) / (|.1q.| ^2)) by QUATERN2:29 .= 0 by QUATERNI:29 ; Rea (1q ") = (Rea 1q) / (|.1q.| ^2) by QUATERN2:29 .= 1 by QUATERNI:29, QUATERNI:68 ; then 1q " = [*1,0,0,0*] by A3, A2, A1, QUATERNI:24; hence 1q " = 1q by QUATERNI:24, QUATERNI:29; ::_thesis: verum end; theorem :: QUATERN3:49 for z1, z2 being quaternion number st |.z1.| = |.z2.| & |.z1.| <> 0 & z1 " = z2 " holds z1 = z2 proof let z1, z2 be quaternion number ; ::_thesis: ( |.z1.| = |.z2.| & |.z1.| <> 0 & z1 " = z2 " implies z1 = z2 ) assume that A1: |.z1.| = |.z2.| and A2: |.z1.| <> 0 and A3: z1 " = z2 " ; ::_thesis: z1 = z2 A4: |.z1.| ^2 <> 0 by A2, XCMPLX_1:6; Im3 (z1 ") = - ((Im3 z1) / (|.z1.| ^2)) by QUATERN2:29; then - ((Im3 z1) / (|.z1.| ^2)) = - ((Im3 z2) / (|.z2.| ^2)) by A3, QUATERN2:29; then A5: Im3 z1 = Im3 z2 by A1, A4, XCMPLX_1:53; Im2 (z1 ") = - ((Im2 z1) / (|.z1.| ^2)) by QUATERN2:29; then - ((Im2 z1) / (|.z1.| ^2)) = - ((Im2 z2) / (|.z2.| ^2)) by A3, QUATERN2:29; then A6: Im2 z1 = Im2 z2 by A1, A4, XCMPLX_1:53; Im1 (z1 ") = - ((Im1 z1) / (|.z1.| ^2)) by QUATERN2:29; then - ((Im1 z1) / (|.z1.| ^2)) = - ((Im1 z2) / (|.z2.| ^2)) by A3, QUATERN2:29; then A7: Im1 z1 = Im1 z2 by A1, A4, XCMPLX_1:53; Rea (z1 ") = (Rea z1) / (|.z1.| ^2) by QUATERN2:29; then (Rea z1) / (|.z1.| ^2) = (Rea z2) / (|.z2.| ^2) by A3, QUATERN2:29; then Rea z1 = Rea z2 by A1, A4, XCMPLX_1:53; hence z1 = z2 by A7, A6, A5, QUATERNI:25; ::_thesis: verum end; theorem :: QUATERN3:50 for z1, z2, z3, z4 being quaternion number holds (z1 - z2) * (z3 + z4) = (((z1 * z3) - (z2 * z3)) + (z1 * z4)) - (z2 * z4) proof let z1, z2, z3, z4 be quaternion number ; ::_thesis: (z1 - z2) * (z3 + z4) = (((z1 * z3) - (z2 * z3)) + (z1 * z4)) - (z2 * z4) (z1 - z2) * (z3 + z4) = ((z1 - z2) * z3) + ((z1 - z2) * z4) by QUATERN2:17 .= ((z1 * z3) - (z2 * z3)) + ((z1 - z2) * z4) by QUATERN2:23 .= ((z1 * z3) - (z2 * z3)) + ((z1 * z4) - (z2 * z4)) by QUATERN2:23 .= (((z1 * z3) - (z2 * z3)) + (z1 * z4)) - (z2 * z4) by QUATERN2:2 ; hence (z1 - z2) * (z3 + z4) = (((z1 * z3) - (z2 * z3)) + (z1 * z4)) - (z2 * z4) ; ::_thesis: verum end; theorem :: QUATERN3:51 for z1, z2, z3, z4 being quaternion number holds (z1 + z2) * (z3 + z4) = (((z1 * z3) + (z2 * z3)) + (z1 * z4)) + (z2 * z4) proof let z1, z2, z3, z4 be quaternion number ; ::_thesis: (z1 + z2) * (z3 + z4) = (((z1 * z3) + (z2 * z3)) + (z1 * z4)) + (z2 * z4) (z1 + z2) * (z3 + z4) = ((z1 + z2) * z3) + ((z1 + z2) * z4) by QUATERN2:17 .= ((z1 * z3) + (z2 * z3)) + ((z1 + z2) * z4) by QUATERN2:18 .= ((z1 * z3) + (z2 * z3)) + ((z1 * z4) + (z2 * z4)) by QUATERN2:18 .= (((z1 * z3) + (z2 * z3)) + (z1 * z4)) + (z2 * z4) by QUATERN2:2 ; hence (z1 + z2) * (z3 + z4) = (((z1 * z3) + (z2 * z3)) + (z1 * z4)) + (z2 * z4) ; ::_thesis: verum end; theorem Th52: :: QUATERN3:52 for z1, z2 being quaternion number holds - (z1 + z2) = (- z1) - z2 proof let z1, z2 be quaternion number ; ::_thesis: - (z1 + z2) = (- z1) - z2 A1: (- z1) - z2 = ((- 1q) * z1) - z2 by QUATERN2:19 .= ((- 1q) * z1) + ((- 1q) * z2) by QUATERN2:19 ; - (z1 + z2) = (- 1q) * (z1 + z2) by QUATERN2:19 .= ((- 1q) * z1) + ((- 1q) * z2) by QUATERN2:17 ; hence - (z1 + z2) = (- z1) - z2 by A1; ::_thesis: verum end; theorem Th53: :: QUATERN3:53 for z1, z2 being quaternion number holds - (z1 - z2) = (- z1) + z2 proof let z1, z2 be quaternion number ; ::_thesis: - (z1 - z2) = (- z1) + z2 - (z1 - z2) = (- 1q) * (z1 - z2) by QUATERN2:19 .= ((- 1q) * z1) - ((- 1q) * z2) by QUATERN2:24 .= ((- 1q) * z1) - (- z2) by QUATERN2:19 ; hence - (z1 - z2) = (- z1) + z2 by QUATERN2:19; ::_thesis: verum end; theorem Th54: :: QUATERN3:54 for z, z1, z2 being quaternion number holds z - (z1 + z2) = (z - z1) - z2 proof let z, z1, z2 be quaternion number ; ::_thesis: z - (z1 + z2) = (z - z1) - z2 A1: (z - z1) - z2 = (z + ((- 1q) * z1)) + (- z2) by QUATERN2:19 .= (z + ((- 1q) * z1)) + ((- 1q) * z2) by QUATERN2:19 ; - (z1 + z2) = (- 1q) * (z1 + z2) by QUATERN2:19 .= ((- 1q) * z1) + ((- 1q) * z2) by QUATERN2:17 ; hence z - (z1 + z2) = (z - z1) - z2 by A1, QUATERN2:2; ::_thesis: verum end; theorem Th55: :: QUATERN3:55 for z, z1, z2 being quaternion number holds z - (z1 - z2) = (z - z1) + z2 proof let z, z1, z2 be quaternion number ; ::_thesis: z - (z1 - z2) = (z - z1) + z2 - (z1 - z2) = (- 1q) * (z1 - z2) by QUATERN2:19 .= ((- 1q) * z1) - ((- 1q) * z2) by QUATERN2:24 ; then z - (z1 - z2) = z + (((- 1q) * z1) - (- z2)) by QUATERN2:19 .= (z + ((- 1q) * z1)) + z2 by QUATERN2:2 ; hence z - (z1 - z2) = (z - z1) + z2 by QUATERN2:19; ::_thesis: verum end; theorem :: QUATERN3:56 for z1, z2, z3, z4 being quaternion number holds (z1 + z2) * (z3 - z4) = (((z1 * z3) + (z2 * z3)) - (z1 * z4)) - (z2 * z4) proof let z1, z2, z3, z4 be quaternion number ; ::_thesis: (z1 + z2) * (z3 - z4) = (((z1 * z3) + (z2 * z3)) - (z1 * z4)) - (z2 * z4) (z1 + z2) * (z3 - z4) = ((z1 + z2) * z3) - ((z1 + z2) * z4) by QUATERN2:24 .= ((z1 * z3) + (z2 * z3)) - ((z1 + z2) * z4) by QUATERN2:18 .= ((z1 * z3) + (z2 * z3)) - ((z1 * z4) + (z2 * z4)) by QUATERN2:18 .= (((z1 * z3) + (z2 * z3)) - (z1 * z4)) - (z2 * z4) by Th54 ; hence (z1 + z2) * (z3 - z4) = (((z1 * z3) + (z2 * z3)) - (z1 * z4)) - (z2 * z4) ; ::_thesis: verum end; theorem Th57: :: QUATERN3:57 for z1, z2, z3, z4 being quaternion number holds (z1 - z2) * (z3 - z4) = (((z1 * z3) - (z2 * z3)) - (z1 * z4)) + (z2 * z4) proof let z1, z2, z3, z4 be quaternion number ; ::_thesis: (z1 - z2) * (z3 - z4) = (((z1 * z3) - (z2 * z3)) - (z1 * z4)) + (z2 * z4) (z1 - z2) * (z3 - z4) = ((z1 - z2) * z3) - ((z1 - z2) * z4) by QUATERN2:24 .= ((z1 * z3) - (z2 * z3)) - ((z1 - z2) * z4) by QUATERN2:23 .= ((z1 * z3) - (z2 * z3)) - ((z1 * z4) - (z2 * z4)) by QUATERN2:23 .= (((z1 * z3) - (z2 * z3)) - (z1 * z4)) + (z2 * z4) by Th55 ; hence (z1 - z2) * (z3 - z4) = (((z1 * z3) - (z2 * z3)) - (z1 * z4)) + (z2 * z4) ; ::_thesis: verum end; theorem :: QUATERN3:58 for z1, z2, z3 being quaternion number holds - ((z1 + z2) + z3) = ((- z1) - z2) - z3 proof let z1, z2, z3 be quaternion number ; ::_thesis: - ((z1 + z2) + z3) = ((- z1) - z2) - z3 - ((z1 + z2) + z3) = - (z1 + (z2 + z3)) by QUATERN2:2 .= (- z1) - (z2 + z3) by Th52 .= ((- z1) - z2) - z3 by Th54 ; hence - ((z1 + z2) + z3) = ((- z1) - z2) - z3 ; ::_thesis: verum end; theorem :: QUATERN3:59 for z1, z2, z3 being quaternion number holds - ((z1 - z2) - z3) = ((- z1) + z2) + z3 proof let z1, z2, z3 be quaternion number ; ::_thesis: - ((z1 - z2) - z3) = ((- z1) + z2) + z3 - ((z1 - z2) - z3) = (- (z1 - z2)) + z3 by Th53 .= ((- z1) + z2) + z3 by Th53 ; hence - ((z1 - z2) - z3) = ((- z1) + z2) + z3 ; ::_thesis: verum end; theorem :: QUATERN3:60 for z1, z2, z3 being quaternion number holds - ((z1 - z2) + z3) = ((- z1) + z2) - z3 proof let z1, z2, z3 be quaternion number ; ::_thesis: - ((z1 - z2) + z3) = ((- z1) + z2) - z3 - ((z1 - z2) + z3) = (- (z1 - z2)) - z3 by Th52 .= ((- z1) + z2) - z3 by Th53 ; hence - ((z1 - z2) + z3) = ((- z1) + z2) - z3 ; ::_thesis: verum end; theorem :: QUATERN3:61 for z1, z2, z3 being quaternion number holds - ((z1 + z2) - z3) = ((- z1) - z2) + z3 proof let z1, z2, z3 be quaternion number ; ::_thesis: - ((z1 + z2) - z3) = ((- z1) - z2) + z3 - ((z1 + z2) - z3) = (- (z1 + z2)) + z3 by Th53 .= ((- z1) - z2) + z3 by Th52 ; hence - ((z1 + z2) - z3) = ((- z1) - z2) + z3 ; ::_thesis: verum end; theorem :: QUATERN3:62 for z1, z, z2 being quaternion number st z1 + z = z2 + z holds z1 = z2 proof let z1, z, z2 be quaternion number ; ::_thesis: ( z1 + z = z2 + z implies z1 = z2 ) A1: ( Rea (z1 + z) = (Rea z1) + (Rea z) & Im1 (z1 + z) = (Im1 z1) + (Im1 z) ) by QUATERNI:36; A2: ( Im2 (z1 + z) = (Im2 z1) + (Im2 z) & Im3 (z1 + z) = (Im3 z1) + (Im3 z) ) by QUATERNI:36; A3: ( Im2 (z2 + z) = (Im2 z2) + (Im2 z) & Im3 (z2 + z) = (Im3 z2) + (Im3 z) ) by QUATERNI:36; A4: ( Rea (z2 + z) = (Rea z2) + (Rea z) & Im1 (z2 + z) = (Im1 z2) + (Im1 z) ) by QUATERNI:36; assume z1 + z = z2 + z ; ::_thesis: z1 = z2 hence z1 = z2 by A1, A2, A4, A3, QUATERNI:25; ::_thesis: verum end; theorem :: QUATERN3:63 for z1, z, z2 being quaternion number st z1 - z = z2 - z holds z1 = z2 proof let z1, z, z2 be quaternion number ; ::_thesis: ( z1 - z = z2 - z implies z1 = z2 ) A1: ( Rea (z1 - z) = (Rea z1) - (Rea z) & Im1 (z1 - z) = (Im1 z1) - (Im1 z) ) by QUATERNI:42; A2: ( Im2 (z1 - z) = (Im2 z1) - (Im2 z) & Im3 (z1 - z) = (Im3 z1) - (Im3 z) ) by QUATERNI:42; A3: ( Im2 (z2 - z) = (Im2 z2) - (Im2 z) & Im3 (z2 - z) = (Im3 z2) - (Im3 z) ) by QUATERNI:42; A4: ( Rea (z2 - z) = (Rea z2) - (Rea z) & Im1 (z2 - z) = (Im1 z2) - (Im1 z) ) by QUATERNI:42; assume z1 - z = z2 - z ; ::_thesis: z1 = z2 hence z1 = z2 by A1, A2, A4, A3, QUATERNI:25; ::_thesis: verum end; theorem :: QUATERN3:64 for z1, z2, z3, z4 being quaternion number holds ((z1 + z2) - z3) * z4 = ((z1 * z4) + (z2 * z4)) - (z3 * z4) proof let z1, z2, z3, z4 be quaternion number ; ::_thesis: ((z1 + z2) - z3) * z4 = ((z1 * z4) + (z2 * z4)) - (z3 * z4) ((z1 + z2) - z3) * z4 = ((z1 + z2) * z4) - (z3 * z4) by QUATERN2:23 .= ((z1 * z4) + (z2 * z4)) - (z3 * z4) by QUATERN2:18 ; hence ((z1 + z2) - z3) * z4 = ((z1 * z4) + (z2 * z4)) - (z3 * z4) ; ::_thesis: verum end; theorem :: QUATERN3:65 for z1, z2, z3, z4 being quaternion number holds ((z1 - z2) + z3) * z4 = ((z1 * z4) - (z2 * z4)) + (z3 * z4) proof let z1, z2, z3, z4 be quaternion number ; ::_thesis: ((z1 - z2) + z3) * z4 = ((z1 * z4) - (z2 * z4)) + (z3 * z4) ((z1 - z2) + z3) * z4 = ((z1 - z2) * z4) + (z3 * z4) by QUATERN2:18 .= ((z1 * z4) - (z2 * z4)) + (z3 * z4) by QUATERN2:23 ; hence ((z1 - z2) + z3) * z4 = ((z1 * z4) - (z2 * z4)) + (z3 * z4) ; ::_thesis: verum end; theorem :: QUATERN3:66 for z1, z2, z3, z4 being quaternion number holds ((z1 - z2) - z3) * z4 = ((z1 * z4) - (z2 * z4)) - (z3 * z4) proof let z1, z2, z3, z4 be quaternion number ; ::_thesis: ((z1 - z2) - z3) * z4 = ((z1 * z4) - (z2 * z4)) - (z3 * z4) ((z1 - z2) - z3) * z4 = ((z1 - z2) * z4) - (z3 * z4) by QUATERN2:23 .= ((z1 * z4) - (z2 * z4)) - (z3 * z4) by QUATERN2:23 ; hence ((z1 - z2) - z3) * z4 = ((z1 * z4) - (z2 * z4)) - (z3 * z4) ; ::_thesis: verum end; theorem :: QUATERN3:67 for z1, z2, z3, z4 being quaternion number holds ((z1 + z2) + z3) * z4 = ((z1 * z4) + (z2 * z4)) + (z3 * z4) proof let z1, z2, z3, z4 be quaternion number ; ::_thesis: ((z1 + z2) + z3) * z4 = ((z1 * z4) + (z2 * z4)) + (z3 * z4) ((z1 + z2) + z3) * z4 = ((z1 + z2) * z4) + (z3 * z4) by QUATERN2:18 .= ((z1 * z4) + (z2 * z4)) + (z3 * z4) by QUATERN2:18 ; hence ((z1 + z2) + z3) * z4 = ((z1 * z4) + (z2 * z4)) + (z3 * z4) ; ::_thesis: verum end; theorem :: QUATERN3:68 for z1, z2, z3 being quaternion number holds (z1 - z2) * z3 = (z2 - z1) * (- z3) proof let z1, z2, z3 be quaternion number ; ::_thesis: (z1 - z2) * z3 = (z2 - z1) * (- z3) (z2 - z1) * (- z3) = (z2 * (- z3)) - (z1 * (- z3)) by QUATERN2:23 .= (- (z2 * z3)) - (z1 * (- z3)) by QUATERN2:21 .= (- (z2 * z3)) - (- (z1 * z3)) by QUATERN2:21 .= (z1 * z3) - (z2 * z3) ; hence (z1 - z2) * z3 = (z2 - z1) * (- z3) by QUATERN2:23; ::_thesis: verum end; theorem :: QUATERN3:69 for z3, z1, z2 being quaternion number holds z3 * (z1 - z2) = (- z3) * (z2 - z1) proof let z3, z1, z2 be quaternion number ; ::_thesis: z3 * (z1 - z2) = (- z3) * (z2 - z1) (- z3) * (z2 - z1) = ((- z3) * z2) - ((- z3) * z1) by QUATERN2:24 .= (- (z3 * z2)) - ((- z3) * z1) by QUATERN2:20 .= (- (z3 * z2)) - (- (z3 * z1)) by QUATERN2:20 .= (z3 * z1) - (z3 * z2) ; hence z3 * (z1 - z2) = (- z3) * (z2 - z1) by QUATERN2:24; ::_thesis: verum end; theorem Th70: :: QUATERN3:70 for z1, z2, z3, z4 being quaternion number holds ((z1 - z2) - z3) + z4 = ((z4 - z3) - z2) + z1 proof let z1, z2, z3, z4 be quaternion number ; ::_thesis: ((z1 - z2) - z3) + z4 = ((z4 - z3) - z2) + z1 Im1 (((z1 - z2) - z3) + z4) = (Im1 ((z1 - z2) - z3)) + (Im1 z4) by QUATERNI:36; then Im1 (((z1 - z2) - z3) + z4) = ((Im1 (z1 - z2)) - (Im1 z3)) + (Im1 z4) by QUATERNI:42; then A1: Im1 (((z1 - z2) - z3) + z4) = (((Im1 z1) - (Im1 z2)) - (Im1 z3)) + (Im1 z4) by QUATERNI:42; Im2 (((z1 - z2) - z3) + z4) = (Im2 ((z1 - z2) - z3)) + (Im2 z4) by QUATERNI:36; then Im2 (((z1 - z2) - z3) + z4) = ((Im2 (z1 - z2)) - (Im2 z3)) + (Im2 z4) by QUATERNI:42; then A2: Im2 (((z1 - z2) - z3) + z4) = (((Im2 z1) - (Im2 z2)) - (Im2 z3)) + (Im2 z4) by QUATERNI:42; Im2 (((z4 - z3) - z2) + z1) = (Im2 ((z4 - z3) - z2)) + (Im2 z1) by QUATERNI:36; then Im2 (((z4 - z3) - z2) + z1) = ((Im2 (z4 - z3)) - (Im2 z2)) + (Im2 z1) by QUATERNI:42; then A3: Im2 (((z4 - z3) - z2) + z1) = (((Im2 z4) - (Im2 z3)) - (Im2 z2)) + (Im2 z1) by QUATERNI:42; Im1 (((z4 - z3) - z2) + z1) = (Im1 ((z4 - z3) - z2)) + (Im1 z1) by QUATERNI:36; then Im1 (((z4 - z3) - z2) + z1) = ((Im1 (z4 - z3)) - (Im1 z2)) + (Im1 z1) by QUATERNI:42; then A4: Im1 (((z4 - z3) - z2) + z1) = (((Im1 z4) - (Im1 z3)) - (Im1 z2)) + (Im1 z1) by QUATERNI:42; Im3 (((z4 - z3) - z2) + z1) = (Im3 ((z4 - z3) - z2)) + (Im3 z1) by QUATERNI:36; then Im3 (((z4 - z3) - z2) + z1) = ((Im3 (z4 - z3)) - (Im3 z2)) + (Im3 z1) by QUATERNI:42; then A5: Im3 (((z4 - z3) - z2) + z1) = (((Im3 z4) - (Im3 z3)) - (Im3 z2)) + (Im3 z1) by QUATERNI:42; Rea (((z4 - z3) - z2) + z1) = (Rea ((z4 - z3) - z2)) + (Rea z1) by QUATERNI:36; then Rea (((z4 - z3) - z2) + z1) = ((Rea (z4 - z3)) - (Rea z2)) + (Rea z1) by QUATERNI:42; then A6: Rea (((z4 - z3) - z2) + z1) = (((Rea z4) - (Rea z3)) - (Rea z2)) + (Rea z1) by QUATERNI:42; Im3 (((z1 - z2) - z3) + z4) = (Im3 ((z1 - z2) - z3)) + (Im3 z4) by QUATERNI:36; then Im3 (((z1 - z2) - z3) + z4) = ((Im3 (z1 - z2)) - (Im3 z3)) + (Im3 z4) by QUATERNI:42; then A7: Im3 (((z1 - z2) - z3) + z4) = (((Im3 z1) - (Im3 z2)) - (Im3 z3)) + (Im3 z4) by QUATERNI:42; Rea (((z1 - z2) - z3) + z4) = (Rea ((z1 - z2) - z3)) + (Rea z4) by QUATERNI:36; then Rea (((z1 - z2) - z3) + z4) = ((Rea (z1 - z2)) - (Rea z3)) + (Rea z4) by QUATERNI:42; then Rea (((z1 - z2) - z3) + z4) = (((Rea z1) - (Rea z2)) - (Rea z3)) + (Rea z4) by QUATERNI:42; hence ((z1 - z2) - z3) + z4 = ((z4 - z3) - z2) + z1 by A1, A2, A7, A6, A4, A3, A5, QUATERNI:25; ::_thesis: verum end; theorem :: QUATERN3:71 for z1, z2, z3, z4 being quaternion number holds (z1 - z2) * (z3 - z4) = (z2 - z1) * (z4 - z3) proof let z1, z2, z3, z4 be quaternion number ; ::_thesis: (z1 - z2) * (z3 - z4) = (z2 - z1) * (z4 - z3) (z2 - z1) * (z4 - z3) = ((z2 - z1) * z4) - ((z2 - z1) * z3) by QUATERN2:24 .= ((z2 * z4) - (z1 * z4)) - ((z2 - z1) * z3) by QUATERN2:23 .= ((z2 * z4) - (z1 * z4)) - ((z2 * z3) - (z1 * z3)) by QUATERN2:23 .= (((z2 * z4) - (z1 * z4)) - (z2 * z3)) + (z1 * z3) by Th55 .= (((z1 * z3) - (z2 * z3)) - (z1 * z4)) + (z2 * z4) by Th70 ; hence (z1 - z2) * (z3 - z4) = (z2 - z1) * (z4 - z3) by Th57; ::_thesis: verum end; theorem :: QUATERN3:72 for z, z1, z2 being quaternion number holds (z - z1) - z2 = (z - z2) - z1 proof let z, z1, z2 be quaternion number ; ::_thesis: (z - z1) - z2 = (z - z2) - z1 Im1 ((z - z1) - z2) = (Im1 (z - z1)) - (Im1 z2) by QUATERNI:42; then A1: Im1 ((z - z1) - z2) = ((Im1 z) - (Im1 z1)) - (Im1 z2) by QUATERNI:42; Im2 ((z - z1) - z2) = (Im2 (z - z1)) - (Im2 z2) by QUATERNI:42; then A2: Im2 ((z - z1) - z2) = ((Im2 z) - (Im2 z1)) - (Im2 z2) by QUATERNI:42; Im2 ((z - z2) - z1) = (Im2 (z - z2)) - (Im2 z1) by QUATERNI:42; then A3: Im2 ((z - z2) - z1) = ((Im2 z) - (Im2 z2)) - (Im2 z1) by QUATERNI:42; Im1 ((z - z2) - z1) = (Im1 (z - z2)) - (Im1 z1) by QUATERNI:42; then A4: Im1 ((z - z2) - z1) = ((Im1 z) - (Im1 z2)) - (Im1 z1) by QUATERNI:42; Im3 ((z - z2) - z1) = (Im3 (z - z2)) - (Im3 z1) by QUATERNI:42; then A5: Im3 ((z - z2) - z1) = ((Im3 z) - (Im3 z2)) - (Im3 z1) by QUATERNI:42; Rea ((z - z2) - z1) = (Rea (z - z2)) - (Rea z1) by QUATERNI:42; then A6: Rea ((z - z2) - z1) = ((Rea z) - (Rea z2)) - (Rea z1) by QUATERNI:42; Im3 ((z - z1) - z2) = (Im3 (z - z1)) - (Im3 z2) by QUATERNI:42; then A7: Im3 ((z - z1) - z2) = ((Im3 z) - (Im3 z1)) - (Im3 z2) by QUATERNI:42; Rea ((z - z1) - z2) = (Rea (z - z1)) - (Rea z2) by QUATERNI:42; then Rea ((z - z1) - z2) = ((Rea z) - (Rea z1)) - (Rea z2) by QUATERNI:42; hence (z - z1) - z2 = (z - z2) - z1 by A1, A2, A7, A6, A4, A3, A5, QUATERNI:25; ::_thesis: verum end; theorem :: QUATERN3:73 for z being quaternion number holds z " = [*((Rea z) / (|.z.| ^2)),(- ((Im1 z) / (|.z.| ^2))),(- ((Im2 z) / (|.z.| ^2))),(- ((Im3 z) / (|.z.| ^2)))*] proof let z be quaternion number ; ::_thesis: z " = [*((Rea z) / (|.z.| ^2)),(- ((Im1 z) / (|.z.| ^2))),(- ((Im2 z) / (|.z.| ^2))),(- ((Im3 z) / (|.z.| ^2)))*] z " = [*(Rea (z ")),(Im1 (z ")),(Im2 (z ")),(Im3 (z "))*] by QUATERNI:24 .= [*((Rea z) / (|.z.| ^2)),(Im1 (z ")),(Im2 (z ")),(Im3 (z "))*] by QUATERN2:29 .= [*((Rea z) / (|.z.| ^2)),(- ((Im1 z) / (|.z.| ^2))),(Im2 (z ")),(Im3 (z "))*] by QUATERN2:29 .= [*((Rea z) / (|.z.| ^2)),(- ((Im1 z) / (|.z.| ^2))),(- ((Im2 z) / (|.z.| ^2))),(Im3 (z "))*] by QUATERN2:29 .= [*((Rea z) / (|.z.| ^2)),(- ((Im1 z) / (|.z.| ^2))),(- ((Im2 z) / (|.z.| ^2))),(- ((Im3 z) / (|.z.| ^2)))*] by QUATERN2:29 ; hence z " = [*((Rea z) / (|.z.| ^2)),(- ((Im1 z) / (|.z.| ^2))),(- ((Im2 z) / (|.z.| ^2))),(- ((Im3 z) / (|.z.| ^2)))*] ; ::_thesis: verum end; theorem :: QUATERN3:74 for z1, z2 being quaternion number holds z1 / z2 = [*((((((Rea z2) * (Rea z1)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z2) * (Im2 z1))) + ((Im3 z2) * (Im3 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im1 z1)) - ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im2 z1)) + ((Im1 z2) * (Im3 z1))) - ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im3 z1)) - ((Im1 z2) * (Im2 z1))) + ((Im2 z2) * (Im1 z1))) - ((Im3 z2) * (Rea z1))) / (|.z2.| ^2))*] proof let z1, z2 be quaternion number ; ::_thesis: z1 / z2 = [*((((((Rea z2) * (Rea z1)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z2) * (Im2 z1))) + ((Im3 z2) * (Im3 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im1 z1)) - ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im2 z1)) + ((Im1 z2) * (Im3 z1))) - ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im3 z1)) - ((Im1 z2) * (Im2 z1))) + ((Im2 z2) * (Im1 z1))) - ((Im3 z2) * (Rea z1))) / (|.z2.| ^2))*] z1 / z2 = [*(Rea (z1 / z2)),(Im1 (z1 / z2)),(Im2 (z1 / z2)),(Im3 (z1 / z2))*] by QUATERNI:24 .= [*((((((Rea z2) * (Rea z1)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z2) * (Im2 z1))) + ((Im3 z2) * (Im3 z1))) / (|.z2.| ^2)),(Im1 (z1 / z2)),(Im2 (z1 / z2)),(Im3 (z1 / z2))*] by QUATERN2:30 .= [*((((((Rea z2) * (Rea z1)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z2) * (Im2 z1))) + ((Im3 z2) * (Im3 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im1 z1)) - ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / (|.z2.| ^2)),(Im2 (z1 / z2)),(Im3 (z1 / z2))*] by QUATERN2:30 .= [*((((((Rea z2) * (Rea z1)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z2) * (Im2 z1))) + ((Im3 z2) * (Im3 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im1 z1)) - ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im2 z1)) + ((Im1 z2) * (Im3 z1))) - ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) / (|.z2.| ^2)),(Im3 (z1 / z2))*] by QUATERN2:30 .= [*((((((Rea z2) * (Rea z1)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z2) * (Im2 z1))) + ((Im3 z2) * (Im3 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im1 z1)) - ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im2 z1)) + ((Im1 z2) * (Im3 z1))) - ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im3 z1)) - ((Im1 z2) * (Im2 z1))) + ((Im2 z2) * (Im1 z1))) - ((Im3 z2) * (Rea z1))) / (|.z2.| ^2))*] by QUATERN2:30 ; hence z1 / z2 = [*((((((Rea z2) * (Rea z1)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z2) * (Im2 z1))) + ((Im3 z2) * (Im3 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im1 z1)) - ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im2 z1)) + ((Im1 z2) * (Im3 z1))) - ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im3 z1)) - ((Im1 z2) * (Im2 z1))) + ((Im2 z2) * (Im1 z1))) - ((Im3 z2) * (Rea z1))) / (|.z2.| ^2))*] ; ::_thesis: verum end; Lm2: = [*0,1*] by ARYTM_0:def_5; theorem :: QUATERN3:75 " = - proof A1: Im3 ( ") = - ((Im3 ) / (|..| ^2)) by QUATERN2:29 .= 0 by QUATERNI:30 ; A2: Im2 ( ") = - ((Im2 ) / (|..| ^2)) by QUATERN2:29 .= 0 by QUATERNI:30 ; A3: Im1 ( ") = - ((Im1 ) / (|..| ^2)) by QUATERN2:29 .= - 1 by QUATERNI:30, QUATERNI:69 ; Rea ( ") = (Rea ) / (|..| ^2) by QUATERN2:29 .= 0 by QUATERNI:30 ; then " = [*(- 0),(- 1),(- 0),(- 0)*] by A3, A2, A1, QUATERNI:24 .= - [*0,1,0,0*] by QUATERN2:4 .= - by Lm2, QUATERNI:def_6 ; hence " = - ; ::_thesis: verum end; theorem :: QUATERN3:76 " = - proof A1: Im3 ( ") = - ((Im3 ) / (|..| ^2)) by QUATERN2:29 .= 0 by QUATERNI:31 ; A2: Im2 ( ") = - ((Im2 ) / (|..| ^2)) by QUATERN2:29 .= - 1 by QUATERNI:31, QUATERNI:70 ; A3: Im1 ( ") = - ((Im1 ) / (|..| ^2)) by QUATERN2:29 .= 0 by QUATERNI:31 ; Rea ( ") = (Rea ) / (|..| ^2) by QUATERN2:29 .= 0 by QUATERNI:31 ; then " = [*(- 0),(- 0),(- 1),(- 0)*] by A3, A2, A1, QUATERNI:24 .= - by QUATERN2:4 ; hence " = - ; ::_thesis: verum end; theorem :: QUATERN3:77 " = - proof A1: Im3 ( ") = - ((Im3 ) / (|..| ^2)) by QUATERN2:29 .= - 1 by QUATERNI:31, QUATERNI:71 ; A2: Im2 ( ") = - ((Im2 ) / (|..| ^2)) by QUATERN2:29 .= 0 by QUATERNI:31 ; A3: Im1 ( ") = - ((Im1 ) / (|..| ^2)) by QUATERN2:29 .= 0 by QUATERNI:31 ; Rea ( ") = (Rea ) / (|..| ^2) by QUATERN2:29 .= 0 by QUATERNI:31 ; then " = [*(- 0),(- 0),(- 0),(- 1)*] by A3, A2, A1, QUATERNI:24 .= - by QUATERN2:4 ; hence " = - ; ::_thesis: verum end; definition let z be quaternion number ; funcz ^2 -> set equals :: QUATERN3:def 1 z * z; correctness coherence z * z is set ; ; end; :: deftheorem defines ^2 QUATERN3:def_1_:_ for z being quaternion number holds z ^2 = z * z; registration let z be quaternion number ; clusterz ^2 -> quaternion ; coherence z ^2 is quaternion ; end; definition let z be Element of QUATERNION ; :: original: ^2 redefine funcz ^2 -> Element of QUATERNION ; correctness coherence z ^2 is Element of QUATERNION ; ; end; theorem Th78: :: QUATERN3:78 for z being quaternion number holds z ^2 = [*(((((Rea z) ^2) - ((Im1 z) ^2)) - ((Im2 z) ^2)) - ((Im3 z) ^2)),(2 * ((Rea z) * (Im1 z))),(2 * ((Rea z) * (Im2 z))),(2 * ((Rea z) * (Im3 z)))*] proof let z be quaternion number ; ::_thesis: z ^2 = [*(((((Rea z) ^2) - ((Im1 z) ^2)) - ((Im2 z) ^2)) - ((Im3 z) ^2)),(2 * ((Rea z) * (Im1 z))),(2 * ((Rea z) * (Im2 z))),(2 * ((Rea z) * (Im3 z)))*] z ^2 = [*(Rea (z ^2)),(Im1 (z ^2)),(Im2 (z ^2)),(Im3 (z ^2))*] by QUATERNI:24 .= [*(((((Rea z) ^2) - ((Im1 z) ^2)) - ((Im2 z) ^2)) - ((Im3 z) ^2)),(Im1 (z ^2)),(Im2 (z ^2)),(Im3 (z ^2))*] by QUATERNI:40 .= [*(((((Rea z) ^2) - ((Im1 z) ^2)) - ((Im2 z) ^2)) - ((Im3 z) ^2)),(2 * ((Rea z) * (Im1 z))),(Im2 (z ^2)),(Im3 (z ^2))*] by QUATERNI:40 .= [*(((((Rea z) ^2) - ((Im1 z) ^2)) - ((Im2 z) ^2)) - ((Im3 z) ^2)),(2 * ((Rea z) * (Im1 z))),(2 * ((Rea z) * (Im2 z))),(Im3 (z ^2))*] by QUATERNI:40 .= [*(((((Rea z) ^2) - ((Im1 z) ^2)) - ((Im2 z) ^2)) - ((Im3 z) ^2)),(2 * ((Rea z) * (Im1 z))),(2 * ((Rea z) * (Im2 z))),(2 * ((Rea z) * (Im3 z)))*] by QUATERNI:40 ; hence z ^2 = [*(((((Rea z) ^2) - ((Im1 z) ^2)) - ((Im2 z) ^2)) - ((Im3 z) ^2)),(2 * ((Rea z) * (Im1 z))),(2 * ((Rea z) * (Im2 z))),(2 * ((Rea z) * (Im3 z)))*] ; ::_thesis: verum end; theorem :: QUATERN3:79 0q ^2 = 0 proof A1: 0q = [*0,0*] by ARYTM_0:def_5 .= [*0,0,0,0*] by QUATERNI:91 ; then A2: ( Rea 0q = 0 & Im1 0q = 0 ) by QUATERNI:23; A3: ( Im2 0q = 0 & Im3 0q = 0 ) by A1, QUATERNI:23; 0q ^2 = [*(((((Rea 0q) ^2) - ((Im1 0q) ^2)) - ((Im2 0q) ^2)) - ((Im3 0q) ^2)),(2 * ((Rea 0q) * (Im1 0q))),(2 * ((Rea 0q) * (Im2 0q))),(2 * ((Rea 0q) * (Im3 0q)))*] by Th78 .= [*0,0*] by A2, A3, QUATERNI:91 .= 0 by ARYTM_0:def_5 ; hence 0q ^2 = 0 ; ::_thesis: verum end; theorem :: QUATERN3:80 1q ^2 = 1 proof A1: 1q = [*1,0*] by ARYTM_0:def_5 .= [*1,0,0,0*] by QUATERNI:91 ; then A2: ( Rea 1q = 1 & Im1 1q = 0 ) by QUATERNI:23; A3: ( Im2 1q = 0 & Im3 1q = 0 ) by A1, QUATERNI:23; 1q ^2 = [*(((((Rea 1q) ^2) - ((Im1 1q) ^2)) - ((Im2 1q) ^2)) - ((Im3 1q) ^2)),(2 * ((Rea 1q) * (Im1 1q))),(2 * ((Rea 1q) * (Im2 1q))),(2 * ((Rea 1q) * (Im3 1q)))*] by Th78 .= [*1,0*] by A2, A3, QUATERNI:91 .= 1 by ARYTM_0:def_5 ; hence 1q ^2 = 1 ; ::_thesis: verum end; theorem Th81: :: QUATERN3:81 for z being quaternion number holds z ^2 = (- z) ^2 proof let z be quaternion number ; ::_thesis: z ^2 = (- z) ^2 (- z) ^2 = [*(((((Rea (- z)) ^2) - ((Im1 (- z)) ^2)) - ((Im2 (- z)) ^2)) - ((Im3 (- z)) ^2)),(2 * ((Rea (- z)) * (Im1 (- z)))),(2 * ((Rea (- z)) * (Im2 (- z)))),(2 * ((Rea (- z)) * (Im3 (- z))))*] by Th78 .= [*(((((- (Rea z)) ^2) - ((Im1 (- z)) ^2)) - ((Im2 (- z)) ^2)) - ((Im3 (- z)) ^2)),(2 * ((Rea (- z)) * (Im1 (- z)))),(2 * ((Rea (- z)) * (Im2 (- z)))),(2 * ((Rea (- z)) * (Im3 (- z))))*] by QUATERNI:41 .= [*(((((- (Rea z)) ^2) - ((- (Im1 z)) ^2)) - ((Im2 (- z)) ^2)) - ((Im3 (- z)) ^2)),(2 * ((Rea (- z)) * (Im1 (- z)))),(2 * ((Rea (- z)) * (Im2 (- z)))),(2 * ((Rea (- z)) * (Im3 (- z))))*] by QUATERNI:41 .= [*(((((- (Rea z)) ^2) - ((- (Im1 z)) ^2)) - ((- (Im2 z)) ^2)) - ((Im3 (- z)) ^2)),(2 * ((Rea (- z)) * (Im1 (- z)))),(2 * ((Rea (- z)) * (Im2 (- z)))),(2 * ((Rea (- z)) * (Im3 (- z))))*] by QUATERNI:41 .= [*(((((- (Rea z)) ^2) - ((- (Im1 z)) ^2)) - ((- (Im2 z)) ^2)) - ((- (Im3 z)) ^2)),(2 * ((Rea (- z)) * (Im1 (- z)))),(2 * ((Rea (- z)) * (Im2 (- z)))),(2 * ((Rea (- z)) * (Im3 (- z))))*] by QUATERNI:41 .= [*(((((- (Rea z)) ^2) - ((- (Im1 z)) ^2)) - ((- (Im2 z)) ^2)) - ((- (Im3 z)) ^2)),(2 * ((- (Rea z)) * (Im1 (- z)))),(2 * ((Rea (- z)) * (Im2 (- z)))),(2 * ((Rea (- z)) * (Im3 (- z))))*] by QUATERNI:41 .= [*(((((- (Rea z)) ^2) - ((- (Im1 z)) ^2)) - ((- (Im2 z)) ^2)) - ((- (Im3 z)) ^2)),(2 * ((- (Rea z)) * (- (Im1 z)))),(2 * ((Rea (- z)) * (Im2 (- z)))),(2 * ((Rea (- z)) * (Im3 (- z))))*] by QUATERNI:41 .= [*(((((- (Rea z)) ^2) - ((- (Im1 z)) ^2)) - ((- (Im2 z)) ^2)) - ((- (Im3 z)) ^2)),(2 * ((- (Rea z)) * (- (Im1 z)))),(2 * ((- (Rea z)) * (Im2 (- z)))),(2 * ((Rea (- z)) * (Im3 (- z))))*] by QUATERNI:41 .= [*(((((- (Rea z)) ^2) - ((- (Im1 z)) ^2)) - ((- (Im2 z)) ^2)) - ((- (Im3 z)) ^2)),(2 * ((- (Rea z)) * (- (Im1 z)))),(2 * ((- (Rea z)) * (- (Im2 z)))),(2 * ((Rea (- z)) * (Im3 (- z))))*] by QUATERNI:41 .= [*(((((- (Rea z)) ^2) - ((- (Im1 z)) ^2)) - ((- (Im2 z)) ^2)) - ((- (Im3 z)) ^2)),(2 * ((- (Rea z)) * (- (Im1 z)))),(2 * ((- (Rea z)) * (- (Im2 z)))),(2 * ((- (Rea z)) * (Im3 (- z))))*] by QUATERNI:41 .= [*(((((- (Rea z)) ^2) - ((- (Im1 z)) ^2)) - ((- (Im2 z)) ^2)) - ((- (Im3 z)) ^2)),(2 * ((- (Rea z)) * (- (Im1 z)))),(2 * ((- (Rea z)) * (- (Im2 z)))),(2 * ((- (Rea z)) * (- (Im3 z))))*] by QUATERNI:41 .= [*(((((Rea z) ^2) - ((Im1 z) ^2)) - ((Im2 z) ^2)) - ((Im3 z) ^2)),(2 * ((Rea z) * (Im1 z))),(2 * ((Rea z) * (Im2 z))),(2 * ((Rea z) * (Im3 z)))*] ; hence z ^2 = (- z) ^2 by Th78; ::_thesis: verum end; definition let z be quaternion number ; funcz ^3 -> set equals :: QUATERN3:def 2 (z * z) * z; coherence (z * z) * z is set ; end; :: deftheorem defines ^3 QUATERN3:def_2_:_ for z being quaternion number holds z ^3 = (z * z) * z; registration let z be quaternion number ; clusterz ^3 -> quaternion ; coherence z ^3 is quaternion ; end; definition let z be Element of QUATERNION ; :: original: ^3 redefine funcz ^3 -> Element of QUATERNION ; correctness coherence z ^3 is Element of QUATERNION ; ; end; theorem :: QUATERN3:82 0q ^3 = 0 proof A1: 0q = [*0,0*] by ARYTM_0:def_5 .= [*0,0,0,0*] by QUATERNI:91 ; then A2: ( Rea 0q = 0 & Im1 0q = 0 ) by QUATERNI:23; A3: ( Im2 0q = 0 & Im3 0q = 0 ) by A1, QUATERNI:23; 0q ^2 = [*(((((Rea 0q) ^2) - ((Im1 0q) ^2)) - ((Im2 0q) ^2)) - ((Im3 0q) ^2)),(2 * ((Rea 0q) * (Im1 0q))),(2 * ((Rea 0q) * (Im2 0q))),(2 * ((Rea 0q) * (Im3 0q)))*] by Th78 .= [*0,0*] by A2, A3, QUATERNI:91 .= 0 by ARYTM_0:def_5 ; hence 0q ^3 = 0 ; ::_thesis: verum end; theorem :: QUATERN3:83 1q ^3 = 1 proof A1: 1q = [*1,0*] by ARYTM_0:def_5 .= [*1,0,0,0*] by QUATERNI:91 ; then A2: ( Rea 1q = 1 & Im1 1q = 0 ) by QUATERNI:23; A3: ( Im2 1q = 0 & Im3 1q = 0 ) by A1, QUATERNI:23; 1q ^2 = [*(((((Rea 1q) ^2) - ((Im1 1q) ^2)) - ((Im2 1q) ^2)) - ((Im3 1q) ^2)),(2 * ((Rea 1q) * (Im1 1q))),(2 * ((Rea 1q) * (Im2 1q))),(2 * ((Rea 1q) * (Im3 1q)))*] by Th78 .= [*1,0*] by A2, A3, QUATERNI:91 .= 1 by ARYTM_0:def_5 ; hence 1q ^3 = 1 ; ::_thesis: verum end; theorem :: QUATERN3:84 ^3 = - proof = [*0,1,0,0*] by Lm2, QUATERNI:def_6; then ( * ) * = [*((((0 * 0) - (1 * 1)) - (0 * 0)) - (0 * 0)),((((0 * 1) + (1 * 0)) + (0 * 0)) - (0 * 0)),((((0 * 0) + (0 * 0)) + (1 * 0)) - (0 * 1)),((((0 * 0) + (0 * 0)) + (1 * 0)) - (0 * 1))*] * [*0,1,0,0*] by QUATERNI:def_10 .= [*(((((- 1) * 0) - (0 * 1)) - (0 * 0)) - (0 * 0)),(((((- 1) * 1) + (0 * 0)) + (0 * 0)) - (0 * 0)),(((((- 1) * 0) + (0 * 0)) + (1 * 0)) - (0 * 0)),(((((- 1) * 0) + (0 * 0)) + (0 * 0)) - (0 * 1))*] by QUATERNI:def_10 .= - [*0,1,0,0*] by QUATERN2:4 ; hence ^3 = - by Lm2, QUATERNI:def_6; ::_thesis: verum end; theorem :: QUATERN3:85 ^3 = - proof ( * ) * = [*((((0 * 0) - (0 * 0)) - (1 * 1)) - (0 * 0)),((((0 * 0) + (0 * 0)) + (0 * 0)) - (0 * 1)),((((0 * 1) + (0 * 1)) + (0 * 0)) - (0 * 0)),((((0 * 0) + (0 * 0)) + (0 * 1)) - (1 * 0))*] * [*0,0,1,0*] by QUATERNI:def_10 .= [*(((((- 1) * 0) - (0 * 0)) - (0 * 1)) - (0 * 0)),(((((- 1) * 0) + (0 * 0)) + (0 * 0)) - (0 * 1)),(((((- 1) * 1) + (0 * 0)) + (0 * 0)) - (0 * 0)),(((((- 1) * 0) + (0 * 0)) + (0 * 1)) - (0 * 0))*] by QUATERNI:def_10 .= - [*0,0,1,0*] by QUATERN2:4 ; hence ^3 = - ; ::_thesis: verum end; theorem :: QUATERN3:86 ^3 = - proof ( * ) * = [*((((0 * 0) - (0 * 0)) - (0 * 0)) - (1 * 1)),((((0 * 0) + (0 * 0)) + (0 * 1)) - (1 * 0)),((((0 * 0) + (0 * 0)) + (0 * 1)) - (1 * 0)),((((0 * 1) + (1 * 0)) + (0 * 0)) - (0 * 0))*] * [*0,0,0,1*] by QUATERNI:def_10 .= [*(((((- 1) * 0) - (0 * 0)) - (0 * 0)) - (0 * 1)),(((((- 1) * 0) + (0 * 0)) + (0 * 1)) - (0 * 0)),(((((- 1) * 0) + (0 * 0)) + (0 * 0)) - (1 * 0)),(((((- 1) * 1) + (0 * 0)) + (0 * 0)) - (0 * 0))*] by QUATERNI:def_10 .= - [*0,0,0,1*] by QUATERN2:4 ; hence ^3 = - ; ::_thesis: verum end; theorem :: QUATERN3:87 (- 1q) ^2 = 1 proof 1q = [*1,0*] by ARYTM_0:def_5 .= [*1,0,0,0*] by QUATERNI:91 ; then A1: - 1q = [*(- 1),(- 0),(- 0),(- 0)*] by QUATERN2:4; then A2: ( Rea (- 1q) = - 1 & Im1 (- 1q) = 0 ) by QUATERNI:23; A3: ( Im2 (- 1q) = 0 & Im3 (- 1q) = 0 ) by A1, QUATERNI:23; (- 1q) ^2 = [*(((((Rea (- 1q)) ^2) - ((Im1 (- 1q)) ^2)) - ((Im2 (- 1q)) ^2)) - ((Im3 (- 1q)) ^2)),(2 * ((Rea (- 1q)) * (Im1 (- 1q)))),(2 * ((Rea (- 1q)) * (Im2 (- 1q)))),(2 * ((Rea (- 1q)) * (Im3 (- 1q))))*] by Th78 .= [*1,0*] by A2, A3, QUATERNI:91 .= 1 by ARYTM_0:def_5 ; hence (- 1q) ^2 = 1 ; ::_thesis: verum end; theorem :: QUATERN3:88 (- 1q) ^3 = - 1 proof A1: 1q = [*1,0*] by ARYTM_0:def_5 .= [*1,0,0,0*] by QUATERNI:91 ; then A2: - 1q = [*(- 1),(- 0),(- 0),(- 0)*] by QUATERN2:4; then A3: ( Rea (- 1q) = - 1 & Im1 (- 1q) = 0 ) by QUATERNI:23; A4: ( Im2 (- 1q) = 0 & Im3 (- 1q) = 0 ) by A2, QUATERNI:23; (- 1q) ^2 = [*(((((Rea (- 1q)) ^2) - ((Im1 (- 1q)) ^2)) - ((Im2 (- 1q)) ^2)) - ((Im3 (- 1q)) ^2)),(2 * ((Rea (- 1q)) * (Im1 (- 1q)))),(2 * ((Rea (- 1q)) * (Im2 (- 1q)))),(2 * ((Rea (- 1q)) * (Im3 (- 1q))))*] by Th78 .= [*1,0*] by A3, A4, QUATERNI:91 .= 1 by ARYTM_0:def_5 ; then (- 1q) ^3 = - 1q by QUATERN2:15 .= [*(- 1),(- 0),(- 0),(- 0)*] by A1, QUATERN2:4 .= [*(- 1),(- 0)*] by QUATERNI:91 .= - 1 by ARYTM_0:def_5 ; hence (- 1q) ^3 = - 1 ; ::_thesis: verum end; theorem :: QUATERN3:89 for z being quaternion number holds z ^3 = - ((- z) ^3) proof let z be quaternion number ; ::_thesis: z ^3 = - ((- z) ^3) A1: z ^3 = z * (z ^2) by QUATERN2:16; (- z) ^3 = (- z) * ((- z) ^2) by QUATERN2:16 .= (- z) * (z ^2) by Th81 .= ((- 1q) * z) * (z ^2) by QUATERN2:19 .= (- 1q) * (z * (z ^2)) by QUATERN2:16 .= - (z ^3) by A1, QUATERN2:19 ; hence z ^3 = - ((- z) ^3) ; ::_thesis: verum end;