:: QUATERN2 semantic presentation

QUA7: for g being quaternion number ex r, s, t, u being Element of REAL st g = [*r,s,t,u*]
proof end;

Lm4: for a, b, c, d being real number holds (((a ^2 ) + (b ^2 )) + (c ^2 )) + (d ^2 ) >= 0
proof end;

Lm2: for a, b, c, d being real number st (((a ^2 ) + (b ^2 )) + (c ^2 )) + (d ^2 ) = 0 holds
( a = 0 & b = 0 & c = 0 & d = 0 )
proof end;

Lm5: for a, b, c, d being real number st (((a ^2 ) + (b ^2 )) + (c ^2 )) + (d ^2 ) = 0 holds
( a = 0 & b = 0 & c = 0 & d = 0 )
proof end;

definition
:: original: 0q
redefine func 0q -> Element of QUATERNION ;
coherence
0q is Element of QUATERNION by QUATERNI:def 2;
end;

definition
:: original: 1q
redefine func 1q -> Element of QUATERNION ;
coherence
1q is Element of QUATERNION by QUATERNI:def 2;
end;

theorem Th35: :: QUATERN2:1
for x, y, z, w being Real holds [*x,y,z,w*] = ((x + (y * <i> )) + (z * <j> )) + (w * <k> )
proof end;

theorem Th5: :: QUATERN2:2
for c1, c2, c3 being quaternion number holds (c1 + c2) + c3 = c1 + (c2 + c3)
proof end;

theorem Th6: :: QUATERN2:3
for c being quaternion number holds c + 0q = c
proof end;

theorem Thc1: :: QUATERN2:4
for x1, x2, x3, x4 being Element of REAL holds - [*x1,x2,x3,x4*] = [*(- x1),(- x2),(- x3),(- x4)*]
proof end;

theorem :: QUATERN2:5
for x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL holds [*x1,x2,x3,x4*] - [*y1,y2,y3,y4*] = [*(x1 - y1),(x2 - y2),(x3 - y3),(x4 - y4)*]
proof end;

theorem :: QUATERN2:6
for c1, c2, c3 being quaternion number holds (c1 - c2) + c3 = (c1 + c3) - c2 by Th5;

theorem Thz1: :: QUATERN2:7
for c1, c2 being quaternion number holds c1 = (c1 + c2) - c2
proof end;

theorem :: QUATERN2:8
for c1, c2 being quaternion number holds c1 = (c1 - c2) + c2
proof end;

theorem Th38: :: QUATERN2:9
for c being quaternion number
for x1 being Element of REAL holds (- x1) * c = - (x1 * c)
proof end;

definition
let q be quaternion number ;
:: original: |.
redefine func |.q.| -> Element of REAL ;
coherence
|.q.| is Element of REAL ;
end;

definition
:: original: <i>
redefine func <i> -> Element of QUATERNION ;
coherence
<i> is Element of QUATERNION by QUATERNI:def 2;
end;

Lm3: for r being quaternion number st r <> 0 holds
|.r.| <> 0
proof end;

theorem Th40: :: QUATERN2:10
for r being quaternion number st r <> 0 holds
|.r.| > 0
proof end;

theorem :: QUATERN2:11
for q, c being quaternion number st q = 0 holds
q * c = 0
proof end;

theorem :: QUATERN2:12
for q, c being quaternion number st q = 0 holds
c * q = 0
proof end;

theorem Th1: :: QUATERN2:13
for c being quaternion number holds c * 1q = c
proof end;

theorem Th2: :: QUATERN2:14
for c being quaternion number holds 1q * c = c
proof end;

theorem Th9: :: QUATERN2:15
for c1, c2, c3 being quaternion number holds (c1 * c2) * c3 = c1 * (c2 * c3)
proof end;

theorem Th10: :: QUATERN2:16
for c1, c2, c3 being quaternion number holds c1 * (c2 + c3) = (c1 * c2) + (c1 * c3)
proof end;

theorem Th11: :: QUATERN2:17
for c1, c2, c3 being quaternion number holds (c1 + c2) * c3 = (c1 * c3) + (c2 * c3)
proof end;

theorem Th12: :: QUATERN2:18
for c being quaternion number holds - c = (- 1q ) * c
proof end;

theorem Thd3: :: QUATERN2:19
for c1, c2 being quaternion number holds (- c1) * c2 = - (c1 * c2)
proof end;

theorem Thd4a: :: QUATERN2:20
for c1, c2 being quaternion number holds c1 * (- c2) = - (c1 * c2)
proof end;

theorem Thd5: :: QUATERN2:21
for c1, c2 being quaternion number holds (- c1) * (- c2) = c1 * c2
proof end;

theorem Thd6: :: QUATERN2:22
for c1, c2, c3 being quaternion number holds (c1 - c2) * c3 = (c1 * c3) - (c2 * c3)
proof end;

theorem Thd7: :: QUATERN2:23
for c1, c2, c3 being quaternion number holds c1 * (c2 - c3) = (c1 * c2) - (c1 * c3)
proof end;

theorem Thd3a: :: QUATERN2:24
for x1, x2, x3, x4 being Element of REAL holds [*x1,x2,x3,x4*] *' = [*x1,(- x2),(- x3),(- x4)*]
proof end;

theorem :: QUATERN2:25
for c being quaternion number holds (c *' ) *' = c
proof end;

definition
let q, r be quaternion number ;
consider q0, q1, q2, q3 being Element of REAL such that
A1: q = [*q0,q1,q2,q3*] by QUA7;
consider r0, r1, r2, r3 being Element of REAL such that
A2: r = [*r0,r1,r2,r3*] by QUA7;
func q / r -> set means :Def1: :: QUATERN2:def 1
 ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st
( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & it = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2 )),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2 )),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2 )),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2 ))*] );
existence
ex b1 being set ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st
( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & b1 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2 )),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2 )),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2 )),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2 ))*] )
proof end;
uniqueness
for b1, b2 being set st ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st
( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & b1 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2 )),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2 )),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2 )),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2 ))*] ) & ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st
( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & b2 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2 )),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2 )),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2 )),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2 ))*] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines / QUATERN2:def 1 :
for q, r being quaternion number
for b3 being set holds
( b3 = q / r iff ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st
( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & b3 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2 )),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2 )),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2 )),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2 ))*] ) );

registration
let q, r be quaternion number ;
cluster q / r -> quaternion ;
coherence
q / r is quaternion
proof end;
end;

definition
let q, r be quaternion number ;
:: original: /
redefine func q / r -> Element of QUATERNION equals :: QUATERN2:def 2
((((((((Rea r) * (Rea q)) + ((Im1 q) * (Im1 r))) + ((Im2 r) * (Im2 q))) + ((Im3 r) * (Im3 q))) / (|.r.| ^2 )) + (((((((Rea r) * (Im1 q)) - ((Im1 r) * (Rea q))) - ((Im2 r) * (Im3 q))) + ((Im3 r) * (Im2 q))) / (|.r.| ^2 )) * <i> )) + (((((((Rea r) * (Im2 q)) + ((Im1 r) * (Im3 q))) - ((Im2 r) * (Rea q))) - ((Im3 r) * (Im1 q))) / (|.r.| ^2 )) * <j> )) + (((((((Rea r) * (Im3 q)) - ((Im1 r) * (Im2 q))) + ((Im2 r) * (Im1 q))) - ((Im3 r) * (Rea q))) / (|.r.| ^2 )) * <k> );
coherence
q / r is Element of QUATERNION by QUATERNI:def 2;
compatibility
for b1 being Element of QUATERNION holds
( b1 = q / r iff b1 = ((((((((Rea r) * (Rea q)) + ((Im1 q) * (Im1 r))) + ((Im2 r) * (Im2 q))) + ((Im3 r) * (Im3 q))) / (|.r.| ^2 )) + (((((((Rea r) * (Im1 q)) - ((Im1 r) * (Rea q))) - ((Im2 r) * (Im3 q))) + ((Im3 r) * (Im2 q))) / (|.r.| ^2 )) * <i> )) + (((((((Rea r) * (Im2 q)) + ((Im1 r) * (Im3 q))) - ((Im2 r) * (Rea q))) - ((Im3 r) * (Im1 q))) / (|.r.| ^2 )) * <j> )) + (((((((Rea r) * (Im3 q)) - ((Im1 r) * (Im2 q))) + ((Im2 r) * (Im1 q))) - ((Im3 r) * (Rea q))) / (|.r.| ^2 )) * <k> ) )
proof end;
end;

:: deftheorem defines / QUATERN2:def 2 :
for q, r being quaternion number holds q / r = ((((((((Rea r) * (Rea q)) + ((Im1 q) * (Im1 r))) + ((Im2 r) * (Im2 q))) + ((Im3 r) * (Im3 q))) / (|.r.| ^2 )) + (((((((Rea r) * (Im1 q)) - ((Im1 r) * (Rea q))) - ((Im2 r) * (Im3 q))) + ((Im3 r) * (Im2 q))) / (|.r.| ^2 )) * <i> )) + (((((((Rea r) * (Im2 q)) + ((Im1 r) * (Im3 q))) - ((Im2 r) * (Rea q))) - ((Im3 r) * (Im1 q))) / (|.r.| ^2 )) * <j> )) + (((((((Rea r) * (Im3 q)) - ((Im1 r) * (Im2 q))) + ((Im2 r) * (Im1 q))) - ((Im3 r) * (Rea q))) / (|.r.| ^2 )) * <k> );

definition
let c be quaternion number ;
func c " -> quaternion number equals :: QUATERN2:def 3
1q / c;
coherence
1q / c is quaternion number ;
end;

:: deftheorem defines " QUATERN2:def 3 :
for c being quaternion number holds c " = 1q / c;

definition
let r be quaternion number ;
:: original: "
redefine func r " -> Element of QUATERNION equals :: QUATERN2:def 4
((((Rea r) / (|.r.| ^2 )) - (((Im1 r) / (|.r.| ^2 )) * <i> )) - (((Im2 r) / (|.r.| ^2 )) * <j> )) - (((Im3 r) / (|.r.| ^2 )) * <k> );
coherence
r " is Element of QUATERNION ;
compatibility
for b1 being Element of QUATERNION holds
( b1 = r " iff b1 = ((((Rea