:: Inner Products, Group, Ring of Quaternion Numbers
:: by Fuguo Ge
::
:: Received March 18, 2008
:: Copyright (c) 2008-2021 Association of Mizar Users


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

Lm2: for a, b, c, d being Real holds (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) >= 0
by QUATERNI:74;

Lm3: for a, b, c, d being Real st (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) = 0 holds
( a = 0 & b = 0 & c = 0 & d = 0 )
by QUATERNI:96;

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

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

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

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

theorem Th2: :: QUATERN2:2
for c1, c2, c3 being Quaternion holds (c1 + c2) + c3 = c1 + (c2 + c3)
proof end;

theorem Th3: :: QUATERN2:3
for c being Quaternion holds c + 0q = c
proof end;

theorem Th4: :: QUATERN2:4
for x1, x2, x3, x4 being 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 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 holds (c1 - c2) + c3 = (c1 + c3) - c2 by Th2;

theorem Th7: :: QUATERN2:7
for c1, c2 being Quaternion holds c1 = (c1 + c2) - c2
proof end;

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

theorem Th9: :: QUATERN2:9
for c being Quaternion
for x1 being Real holds (- x1) * c = - (x1 * c)
proof end;

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

Lm4: for r being Quaternion st |.r.| = 0 holds
r = 0
by QUATERNI:66;

theorem Th10: :: QUATERN2:10
for r being Quaternion st r <> 0 holds
|.r.| > 0
proof end;

theorem Th11: :: QUATERN2:11
0q = [*0,0,0,0*]
proof end;

theorem :: QUATERN2:12
for r being Quaternion holds 0q * r = 0
proof end;

theorem :: QUATERN2:13
for r being Quaternion holds r * 0q = 0
proof end;

theorem Th14: :: QUATERN2:14
for c being Quaternion holds c * 1q = c
proof end;

theorem Th15: :: QUATERN2:15
for c being Quaternion holds 1q * c = c
proof end;

theorem Th16: :: QUATERN2:16
for c1, c2, c3 being Quaternion holds (c1 * c2) * c3 = c1 * (c2 * c3)
proof end;

theorem Th17: :: QUATERN2:17
for c1, c2, c3 being Quaternion holds c1 * (c2 + c3) = (c1 * c2) + (c1 * c3)
proof end;

theorem Th18: :: QUATERN2:18
for c1, c2, c3 being Quaternion holds (c1 + c2) * c3 = (c1 * c3) + (c2 * c3)
proof end;

theorem Th19: :: QUATERN2:19
for c being Quaternion holds - c = (- 1q) * c
proof end;

theorem Th20: :: QUATERN2:20
for c1, c2 being Quaternion holds (- c1) * c2 = - (c1 * c2)
proof end;

theorem Th21: :: QUATERN2:21
for c1, c2 being Quaternion holds c1 * (- c2) = - (c1 * c2)
proof end;

theorem Th22: :: QUATERN2:22
for c1, c2 being Quaternion holds (- c1) * (- c2) = c1 * c2
proof end;

theorem Th23: :: QUATERN2:23
for c1, c2, c3 being Quaternion holds (c1 - c2) * c3 = (c1 * c3) - (c2 * c3)
proof end;

theorem Th24: :: QUATERN2:24
for c1, c2, c3 being Quaternion holds c1 * (c2 - c3) = (c1 * c2) - (c1 * c3)
proof end;

theorem Th25: :: QUATERN2:25
for x1, x2, x3, x4 being Real holds [*x1,x2,x3,x4*] *' = [*x1,(- x2),(- x3),(- x4)*]
proof end;

theorem :: QUATERN2:26
for c being Quaternion holds (c *') *' = c
proof end;

definition
let q, r be Quaternion;
consider q0, q1, q2, q3 being Element of REAL such that
A1: q = [*q0,q1,q2,q3*] by Lm1;
consider r0, r1, r2, r3 being Element of REAL such that
A2: r = [*r0,r1,r2,r3*] by Lm1;
func q / r -> Number 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 Number 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 Number 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
for b3 being Number 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;
cluster q / r -> quaternion ;
coherence
q / r is quaternion
proof end;
end;

definition
let q, r be Quaternion;
:: original: /
redefine func q / r -> Element of QUATERNION ;
coherence
q / r is Element of QUATERNION by QUATERNI:def 2;
end;

theorem :: QUATERN2:27
for q, r being Quaternion 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>)
proof end;

definition
let c be Quaternion;
func c " -> Quaternion equals :: QUATERN2:def 2
1q / c;
coherence
1q / c is Quaternion ;
end;

:: deftheorem defines " QUATERN2:def 2 :
for c being Quaternion holds c " = 1q / c;

definition
let r be Quaternion;
:: original: "
redefine func r " -> Element of QUATERNION ;
coherence
r " is Element of QUATERNION ;
end;

theorem :: QUATERN2:28
for r being Quaternion holds r " = ((((Rea r) / (|.r.| ^2)) - (((Im1 r) / (|.r.| ^2)) * <i>)) - (((Im2 r) / (|.r.| ^2)) * <j>)) - (((Im3 r) / (|.r.| ^2)) * <k>)
proof end;

theorem :: QUATERN2:29
for r being Quaternion holds
( Rea (r ") = (Rea r) / (|.r.| ^2) & Im1 (r ") = - ((Im1 r) / (|.r.| ^2)) & Im2 (r ") = - ((Im2 r) / (|.r.| ^2)) & Im3 (r ") = - ((Im3 r) / (|.r.| ^2)) )
proof end;

theorem :: QUATERN2:30
for q, r being Quaternion holds
( Rea (q / r) = (((((Rea r) * (Rea q)) + ((Im1 q) * (Im1 r))) + ((Im2 r) * (Im2 q))) + ((Im3 r) * (Im3 q))) / (|.r.| ^2) & Im1 (q / r) = (((((Rea r) * (Im1 q)) - ((Im1 r) * (Rea q))) - ((Im2 r) * (Im3 q))) + ((Im3 r) * (Im2 q))) / (|.r.| ^2) & Im2 (q / r) = (((((Rea r) * (Im2 q)) + ((Im1 r) * (Im3 q))) - ((Im2 r) * (Rea q))) - ((Im3 r) * (Im1 q))) / (|.r.| ^2) & Im3 (q / r) = (((((Rea r) * (Im3 q)) - ((Im1 r) * (Im2 q))) + ((Im2 r) * (Im1 q))) - ((Im3 r) * (Rea q))) / (|.r.| ^2) )
proof end;

Lm5: 0 in REAL
by XREAL_0:def 1;

theorem Th31: :: QUATERN2:31
for r being Quaternion st r <> 0 holds
r * (r ") = 1
proof end;

theorem :: QUATERN2:32
for r being Quaternion st r <> 0 holds
(r ") * r = 1
proof end;

theorem Th33: :: QUATERN2:33
for c being Quaternion st c <> 0q holds
c / c = 1q
proof end;

theorem :: QUATERN2:34
for c being Quaternion holds (- c) " = - (c ")
proof end;

definition
func compquaternion -> UnOp of QUATERNION means :: QUATERN2:def 3
 for c being Element of QUATERNION holds it . c = - c;
existence
ex b1 being UnOp of QUATERNION st
for c being Element of QUATERNION holds b1 . c = - c from FUNCT_2:sch 4();
uniqueness
for b1, b2 being UnOp of QUATERNION st ( for c being Element of QUATERNION holds b1 . c = - c ) & ( for c being Element of QUATERNION holds b2 . c = - c ) holds
b1 = b2 from BINOP_2:sch 1();
func addquaternion -> BinOp of QUATERNION means :Def4: :: QUATERN2:def 4
 for c1, c2 being Element of QUATERNION holds it . (c1,c2) = c1 + c2;
existence
ex b1 being BinOp of QUATERNION st
for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 + c2 from BINOP_1:sch 4();
uniqueness
for b1, b2 being BinOp of QUATERNION st ( for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 + c2 ) & ( for c1, c2 being Element of QUATERNION holds b2 . (c1,c2) = c1 + c2 ) holds
b1 = b2 from BINOP_2:sch 2();
func diffquaternion -> BinOp of QUATERNION means :: QUATERN2:def 5
 for c1, c2 being Element of QUATERNION holds it . (c1,c2) = c1 - c2;
existence
ex b1 being BinOp of QUATERNION st
for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 - c2 from BINOP_1:sch 4();
uniqueness
for b1, b2 being BinOp of QUATERNION st ( for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 - c2 ) & ( for c1, c2 being Element of QUATERNION holds b2 . (c1,c2) = c1 - c2 ) holds
b1 = b2 from BINOP_2:sch 2();
func multquaternion -> BinOp of QUATERNION means :Def6: :: QUATERN2:def 6
 for c1, c2 being Element of QUATERNION holds it . (c1,c2) = c1 * c2;
existence
ex b1 being BinOp of QUATERNION st
for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 * c2 from BINOP_1:sch 4();
uniqueness
for b1, b2 being BinOp of QUATERNION st ( for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 * c2 ) & ( for c1, c2 being Element of QUATERNION holds b2 . (c1,c2) = c1 * c2 ) holds
b1 = b2 from BINOP_2:sch 2();
func divquaternion -> BinOp of QUATERNION means :: QUATERN2:def 7
 for c1, c2 being Element of QUATERNION holds it . (c1,c2) = c1 / c2;
existence
ex b1 being BinOp of QUATERNION st
for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 / c2 from BINOP_1:sch 4();
uniqueness
for b1, b2 being BinOp of QUATERNION st ( for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 / c2 ) & ( for c1, c2 being Element of QUATERNION holds b2 . (c1,c2) = c1 / c2 ) holds
b1 = b2 from BINOP_2:sch 2();
func invquaternion -> UnOp of QUATERNION means :: QUATERN2:def 8
 for c being Element of QUATERNION holds it . c = c " ;
existence
ex b1 being UnOp of QUATERNION st
for c being Element of QUATERNION holds b1 . c = c " from FUNCT_2:sch 4();
uniqueness
for b1, b2 being UnOp of QUATERNION st ( for c being Element of QUATERNION holds b1 . c = c " ) & ( for c being Element of QUATERNION holds b2 . c = c " ) holds
b1 = b2 from BINOP_2:sch 1();
end;

:: deftheorem defines compquaternion QUATERN2:def 3 :
for b1 being UnOp of QUATERNION holds
( b1 = compquaternion iff for c being Element of QUATERNION holds b1 . c = - c );

:: deftheorem Def4 defines addquaternion QUATERN2:def 4 :
for b1 being BinOp of QUATERNION holds
( b1 = addquaternion iff for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 + c2 );

:: deftheorem defines diffquaternion QUATERN2:def 5 :
for b1 being BinOp of QUATERNION holds
( b1 = diffquaternion iff for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 - c2 );

:: deftheorem Def6 defines multquaternion QUATERN2:def 6 :
for b1 being BinOp of QUATERNION holds
( b1 = multquaternion iff for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 * c2 );

:: deftheorem defines divquaternion QUATERN2:def 7 :
for b1 being BinOp of QUATERNION holds
( b1 = divquaternion iff for c1, c2 being Element of QUATERNION holds b1 . (c1,c2) = c1 / c2 );

:: deftheorem defines invquaternion QUATERN2:def 8 :
for b1 being UnOp of QUATERNION holds
( b1 = invquaternion iff for c being Element of QUATERNION holds b1 . c = c " );

definition
func G_Quaternion -> strict addLoopStr means :Def9: :: QUATERN2:def 9
( the carrier of it = QUATERNION & the addF of it = addquaternion & 0. it = 0q );
existence
ex b1 being strict addLoopStr st
( the carrier of b1 = QUATERNION & the addF of b1 = addquaternion & 0. b1 = 0q )
proof end;
uniqueness
for b1, b2 being strict addLoopStr st the carrier of b1 = QUATERNION & the addF of b1 = addquaternion & 0. b1 = 0q & the carrier of b2 = QUATERNION & the addF of b2 = addquaternion & 0. b2 = 0q holds
b1 = b2 ;
end;

:: deftheorem Def9 defines G_Quaternion QUATERN2:def 9 :
for b1 being strict addLoopStr holds
( b1 = G_Quaternion iff ( the carrier of b1 = QUATERNION & the addF of b1 = addquaternion & 0. b1 = 0q ) );

registration
cluster G_Quaternion -> non empty strict ;
coherence
not G_Quaternion is empty by Def9;
end;

registration
cluster -> quaternion for Element of the carrier of G_Quaternion;
coherence
for b1 being Element of G_Quaternion holds b1 is quaternion
proof end;
end;

registration
let x, y be Element of G_Quaternion;
let a, b be Quaternion;
identify x + y with a + b when x = a, y = b;
compatibility
( x = a & y = b implies x + y = a + b )
proof end;
end;

theorem Th35: :: QUATERN2:35
0. G_Quaternion = 0q by Def9;

registration
cluster G_Quaternion -> strict right_complementable Abelian add-associative right_zeroed ;
coherence
( G_Quaternion is Abelian & G_Quaternion is add-associative & G_Quaternion is right_zeroed & G_Quaternion is right_complementable )
proof end;
end;

registration
let x be Element of G_Quaternion;
let a be Quaternion;
identify - x with - a when x = a;
compatibility
( x = a implies - x = - a )
proof end;
end;

registration
let x, y be Element of G_Quaternion;
let a, b be Quaternion;
identify x - y with a - b when x = a, y = b;
compatibility
( x = a & y = b implies x - y = a - b ) ;
end;

theorem :: QUATERN2:36
for x, y, z being Element of G_Quaternion holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. G_Quaternion) = x ) by RLVECT_1:def 3, RLVECT_1:def 4;

definition
func R_Quaternion -> strict doubleLoopStr means :Def10: :: QUATERN2:def 10
( the carrier of it = QUATERNION & the addF of it = addquaternion & the multF of it = multquaternion & 1. it = 1q & 0. it = 0q );
existence
ex b1 being strict doubleLoopStr st
( the carrier of b1 = QUATERNION & the addF of b1 = addquaternion & the multF of b1 = multquaternion & 1. b1 = 1q & 0. b1 = 0q )
proof end;
uniqueness
for b1, b2 being strict doubleLoopStr st the carrier of b1 = QUATERNION & the addF of b1 = addquaternion & the multF of b1 = multquaternion & 1. b1 = 1q & 0. b1 = 0q & the carrier of b2 = QUATERNION & the addF of b2 = addquaternion & the multF of b2 = multquaternion & 1. b2 = 1q & 0. b2 = 0q holds
b1 = b2 ;
end;

:: deftheorem Def10 defines R_Quaternion QUATERN2:def 10 :
for b1 being strict doubleLoopStr holds
( b1 = R_Quaternion iff ( the carrier of b1 = QUATERNION & the addF of b1 = addquaternion & the multF of b1 = multquaternion & 1. b1 = 1q & 0. b1 = 0q ) );

registration
cluster R_Quaternion -> non empty strict ;
coherence
not R_Quaternion is empty by Def10;
end;

registration
cluster -> quaternion for Element of the carrier of R_Quaternion;
coherence
for b1 being Element of R_Quaternion holds b1 is quaternion
proof end;
end;

registration
let a, b be Quaternion;
let x, y be Element of R_Quaternion;
identify x + y with a + b when x = a, y = b;
compatibility
( x = a & y = b implies x + y = a + b )
proof end;
identify x * y with a * b when x = a, y = b;
compatibility
( x = a & y = b implies x * y = a * b )
proof end;
end;

registration
cluster R_Quaternion -> strict well-unital ;
coherence
R_Quaternion is well-unital
proof end;
end;

theorem :: QUATERN2:37
1. R_Quaternion = 1q by Def10;

theorem :: QUATERN2:38
1_ R_Quaternion = 1q by Def10;

theorem Th39: :: QUATERN2:39
0. R_Quaternion = 0q by Def10;

registration
cluster R_Quaternion -> non degenerated right_complementable almost_right_invertible strict Abelian add-associative right_zeroed right_unital distributive left_unital associative ;
coherence
( R_Quaternion is add-associative & R_Quaternion is right_zeroed & R_Quaternion is right_complementable & R_Quaternion is Abelian & R_Quaternion is associative & R_Quaternion is left_unital & R_Quaternion is right_unital & R_Quaternion is distributive & R_Quaternion is almost_right_invertible & not R_Quaternion is degenerated )
proof end;
end;

registration
let x be Element of R_Quaternion;
let a be Quaternion;
identify - x with - a when x = a;
compatibility
( x = a implies - x = - a )
proof end;
end;

registration
let x, y be Element of R_Quaternion;
let a, b be Quaternion;
identify x - y with a - b when x = a, y = b;
compatibility
( x = a & y = b implies x - y = a - b ) ;
end;

definition
let z be Element of R_Quaternion;
:: original: *'
redefine func z *' -> Element of R_Quaternion;
coherence
z *' is Element of R_Quaternion by Def10;
end;

theorem :: QUATERN2:40
for z being Element of R_Quaternion holds - z = (- (1_ R_Quaternion)) * z
proof end;

theorem :: QUATERN2:41
(0. R_Quaternion) *' = 0. R_Quaternion
proof end;

theorem :: QUATERN2:42
for z being Element of R_Quaternion st z *' = 0. R_Quaternion holds
z = 0. R_Quaternion
proof end;

theorem :: QUATERN2:43
(1. R_Quaternion) *' = 1. R_Quaternion
proof end;

theorem :: QUATERN2:44
|.(0. R_Quaternion).| = 0 by Def10, QUATERNI:65;

theorem :: QUATERN2:45
for z being Element of R_Quaternion st |.z.| = 0 holds
z = 0. R_Quaternion by Th39, QUATERNI:66;

theorem :: QUATERN2:46
|.(1. R_Quaternion).| = 1 by Def10, QUATERNI:68;

theorem :: QUATERN2:47
(1. R_Quaternion) " = 1. R_Quaternion
proof end;

definition
let x, y be Quaternion;
func x .|. y -> Element of QUATERNION equals :: QUATERN2:def 11
x * (y *');
coherence
x * (y *') is Element of QUATERNION ;
end;

:: deftheorem defines .|. QUATERN2:def 11 :
for x, y being Quaternion holds x .|. y = x * (y *');

theorem Th48: :: QUATERN2:48
for c1, c2 being Quaternion holds c1 .|. c2 = [*(((((Rea c1) * (Rea c2)) + ((Im1 c1) * (Im1 c2))) + ((Im2 c1) * (Im2 c2))) + ((Im3 c1) * (Im3 c2))),(((((Rea c1) * (- (Im1 c2))) + ((Im1 c1) * (Rea c2))) - ((Im2 c1) * (Im3 c2))) + ((Im3 c1) * (Im2 c2))),(((((Rea c1) * (- (Im2 c2))) + ((Rea c2) * (Im2 c1))) - ((Im1 c2) * (Im3 c1))) + ((Im3 c2) * (Im1 c1))),(((((Rea c1) * (- (Im3 c2))) + ((Im3 c1) * (Rea c2))) - ((Im1 c1) * (Im2 c2))) + ((Im2 c1) * (Im1 c2)))*]
proof end;

theorem Th49: :: QUATERN2:49
for c being Quaternion holds c .|. c = |.c.| ^2
proof end;

theorem :: QUATERN2:50
for c being Quaternion holds
( Rea (c .|. c) = |.c.| ^2 & Im1 (c .|. c) = 0 & Im2 (c .|. c) = 0 & Im2 (c .|. c) = 0 )
proof end;

theorem :: QUATERN2:51
for c1, c2 being Quaternion holds |.(c1 .|. c2).| = |.c1.| * |.c2.|
proof end;

theorem :: QUATERN2:52
for c being Quaternion st c .|. c = 0 holds
c = 0
proof end;

theorem :: QUATERN2:53
for c1, c2, c3 being Quaternion holds (c1 + c2) .|. c3 = (c1 .|. c3) + (c2 .|. c3) by Th18;

theorem :: QUATERN2:54
for c1, c2, c3 being Quaternion holds c1 .|. (c2 + c3) = (c1 .|. c2) + (c1 .|. c3)
proof end;

theorem :: QUATERN2:55
for c1, c2 being Quaternion holds (- c1) .|. c2 = - (c1 .|. c2) by Th20;

theorem :: QUATERN2:56
for c1, c2 being Quaternion holds - (c1 .|. c2) = c1 .|. (- c2)
proof end;

theorem :: QUATERN2:57
for c1, c2 being Quaternion holds (- c1) .|. (- c2) = c1 .|. c2
proof end;

theorem :: QUATERN2:58
for c1, c2, c3 being Quaternion holds (c1 - c2) .|. c3 = (c1 .|. c3) - (c2 .|. c3) by Th23;

theorem :: QUATERN2:59
for c1, c2, c3 being Quaternion holds c1 .|. (c2 - c3) = (c1 .|. c2) - (c1 .|. c3)
proof end;

theorem :: QUATERN2:60
for c1, c2 being Quaternion holds (c1 + c2) .|. (c1 + c2) = (((c1 .|. c1) + (c1 .|. c2)) + (c2 .|. c1)) + (c2 .|. c2)
proof end;

theorem :: QUATERN2:61
for c1, c2 being Quaternion holds (c1 - c2) .|. (c1 - c2) = (((c1 .|. c1) - (c1 .|. c2)) - (c2 .|. c1)) + (c2 .|. c2)
proof end;