:: Cayley-Dickson Construction
:: by Artur Korni{\l}owicz
::
:: Copyright (c) 2012-2021 Association of Mizar Users

theorem Th1: :: CAYLDICK:1
for a, b, c, d being Real holds ((a + b) ^2) + ((c + d) ^2) <= ((sqrt ((a ^2) + (c ^2))) + (sqrt ((b ^2) + (d ^2)))) ^2
proof end;

registration
let X be non trivial RealNormSpace;
let x be non zero Element of X;
coherence
proof end;
end;

registration
let c be non zero Complex;
cluster c ^2 -> non zero ;
coherence
not c ^2 is zero
by XCMPLX_1:6;
end;

registration
let x be non empty set ;
coherence
proof end;
end;

registration
existence
ex b1 being XFinSequence st b1 is non-empty
proof end;
end;

registration
let f, g be non-empty XFinSequence;
cluster f ^ g -> non-empty ;
coherence
f ^ g is non-empty
proof end;
end;

registration
let x, y be non empty set ;
cluster <%x,y%> -> non-empty ;
coherence
<%x,y%> is non-empty
;
end;

theorem :: CAYLDICK:2
for u, x being set st <%u%> = <%x%> holds
u = x
proof end;

theorem Th3: :: CAYLDICK:3
for u, v, x, y being set st <%u,v%> = <%x,y%> holds
( u = x & v = y )
proof end;

theorem :: CAYLDICK:4
for x, X being set st x in X holds
<%x%> in product <%X%>
proof end;

theorem :: CAYLDICK:5
for z, X being set st z in product <%X%> holds
ex x being set st
( x in X & z = <%x%> )
proof end;

theorem Th6: :: CAYLDICK:6
for x, y, X, Y being set st x in X & y in Y holds
<%x,y%> in product <%X,Y%>
proof end;

theorem Th7: :: CAYLDICK:7
for z, X, Y being set st z in product <%X,Y%> holds
ex x, y being set st
( x in X & y in Y & z = <%x,y%> )
proof end;

definition
let D be set ;
func binop D -> BinOp of D equals :: CAYLDICK:def 1
[:D,D:] --> the Element of D;
coherence
[:D,D:] --> the Element of D is BinOp of D
proof end;
end;

:: deftheorem defines binop CAYLDICK:def 1 :
for D being set holds binop D = [:D,D:] --> the Element of D;

registration
let D be set ;
coherence
( binop D is associative & binop D is commutative )
proof end;
end;

registration
let D be set ;
cluster Relation-like [:D,D:] -defined D -valued Function-like V14([:D,D:]) V18([:D,D:],D) commutative associative for Element of bool [:[:D,D:],D:];
existence
ex b1 being BinOp of D st
( b1 is associative & b1 is commutative )
proof end;
end;

definition
attr c1 is strict ;
struct ConjNormAlgStr -> Normed_AlgebraStr ;
aggr ConjNormAlgStr(# carrier, multF, addF, Mult, OneF, ZeroF, normF, conjugateF #) -> ConjNormAlgStr ;
sel conjugateF c1 -> Function of the carrier of c1, the carrier of c1;
end;

registration
existence
ex b1 being ConjNormAlgStr st
( not b1 is trivial & b1 is strict )
proof end;
end;

definition
let N be non empty ConjNormAlgStr ;
let a be Element of N;
func a *' -> Element of N equals :: CAYLDICK:def 2
the conjugateF of N . a;
coherence
the conjugateF of N . a is Element of N
;
end;

:: deftheorem defines *' CAYLDICK:def 2 :
for N being non empty ConjNormAlgStr
for a being Element of N holds a *' = the conjugateF of N . a;

definition
let N be non empty ConjNormAlgStr ;
let a be Element of N;
attr a is well-conjugated means :Def3: :: CAYLDICK:def 3
(a *') * a = () * (1. N) if not a is zero
otherwise a *' is zero ;
consistency
verum
;
end;

:: deftheorem Def3 defines well-conjugated CAYLDICK:def 3 :
for N being non empty ConjNormAlgStr
for a being Element of N holds
( ( not a is zero implies ( a is well-conjugated iff (a *') * a = () * (1. N) ) ) & ( a is zero implies ( a is well-conjugated iff a *' is zero ) ) );

definition
let N be non empty ConjNormAlgStr ;
attr N is well-conjugated means :Def4: :: CAYLDICK:def 4
for a being Element of N holds a is well-conjugated ;
attr N is add-conjugative means :Def5: :: CAYLDICK:def 5
for a, b being Element of N holds (a + b) *' = (a *') + (b *');
attr N is norm-conjugative means :Def6: :: CAYLDICK:def 6
for a being Element of N holds ||.(a *').|| = ;
attr N is scalar-conjugative means :Def7: :: CAYLDICK:def 7
for r being Real
for a being Element of N holds r * (a *') = (r * a) *' ;
end;

:: deftheorem Def4 defines well-conjugated CAYLDICK:def 4 :
for N being non empty ConjNormAlgStr holds
( N is well-conjugated iff for a being Element of N holds a is well-conjugated );

:: deftheorem Def5 defines add-conjugative CAYLDICK:def 5 :
for N being non empty ConjNormAlgStr holds
( N is add-conjugative iff for a, b being Element of N holds (a + b) *' = (a *') + (b *') );

:: deftheorem Def6 defines norm-conjugative CAYLDICK:def 6 :
for N being non empty ConjNormAlgStr holds
( N is norm-conjugative iff for a being Element of N holds ||.(a *').|| = );

:: deftheorem Def7 defines scalar-conjugative CAYLDICK:def 7 :
for N being non empty ConjNormAlgStr holds
( N is scalar-conjugative iff for r being Real
for a being Element of N holds r * (a *') = (r * a) *' );

registration
let D be real-membered set ;
let a, m be BinOp of D;
let M be Function of [:REAL,D:],D;
let O, Z be Element of D;
let n be Function of D,REAL;
let c be Function of D,D;
cluster ConjNormAlgStr(# D,m,a,M,O,Z,n,c #) -> real-membered ;
coherence
ConjNormAlgStr(# D,m,a,M,O,Z,n,c #) is real-membered
;
end;

registration
let D be set ;
let a be associative BinOp of D;
let m be BinOp of D;
let M be Function of [:REAL,D:],D;
let O, Z be Element of D;
let n be Function of D,REAL;
let c be Function of D,D;
cluster ConjNormAlgStr(# D,m,a,M,O,Z,n,c #) -> add-associative ;
coherence
by BINOP_1:def 3;
end;

registration
let D be set ;
let a be commutative BinOp of D;
let m be BinOp of D;
let M be Function of [:REAL,D:],D;
let O, Z be Element of D;
let n be Function of D,REAL;
let c be Function of D,D;
cluster ConjNormAlgStr(# D,m,a,M,O,Z,n,c #) -> Abelian ;
coherence
ConjNormAlgStr(# D,m,a,M,O,Z,n,c #) is Abelian
by BINOP_1:def 2;
end;

registration
let D be set ;
let a be BinOp of D;
let m be associative BinOp of D;
let M be Function of [:REAL,D:],D;
let O, Z be Element of D;
let n be Function of D,REAL;
let c be Function of D,D;
cluster ConjNormAlgStr(# D,m,a,M,O,Z,n,c #) -> associative ;
coherence
ConjNormAlgStr(# D,m,a,M,O,Z,n,c #) is associative
by BINOP_1:def 3;
end;

registration
let D be set ;
let a be BinOp of D;
let m be commutative BinOp of D;
let M be Function of [:REAL,D:],D;
let O, Z be Element of D;
let n be Function of D,REAL;
let c be Function of D,D;
cluster ConjNormAlgStr(# D,m,a,M,O,Z,n,c #) -> commutative ;
coherence
ConjNormAlgStr(# D,m,a,M,O,Z,n,c #) is commutative
by BINOP_1:def 2;
end;

definition
func N_Real -> strict ConjNormAlgStr equals :: CAYLDICK:def 8
coherence
ConjNormAlgStr(# REAL,multreal,addreal,multreal,(In (1,REAL)),(In (0,REAL)),absreal,() #) is strict ConjNormAlgStr
;
end;

:: deftheorem defines N_Real CAYLDICK:def 8 :
N_Real = ConjNormAlgStr(# REAL,multreal,addreal,multreal,(In (1,REAL)),(In (0,REAL)),absreal,() #);

registration
coherence ;
end;

registration
let a, b be Element of N_Real;
let r, s be Real;
identify a + b with r + s when a = r, b = s;
compatibility
( a = r & b = s implies a + b = r + s )
by BINOP_2:def 9;
identify a * b with r * s when a = r, b = s;
compatibility
( a = r & b = s implies a * b = r * s )
by BINOP_2:def 11;
end;

registration
coherence
for b1 being non empty Abelian addMagma st b1 is right_add-cancelable holds
proof end;
coherence
for b1 being non empty Abelian addMagma st b1 is left_add-cancelable holds
proof end;
coherence
for b1 being non empty Abelian addLoopStr st b1 is left_complementable holds
b1 is right_complementable
proof end;
coherence
for b1 being non empty Abelian commutative doubleLoopStr st b1 is left-distributive holds
b1 is right-distributive
proof end;
coherence
for b1 being non empty Abelian commutative doubleLoopStr st b1 is right-distributive holds
b1 is left-distributive
proof end;
coherence
for b1 being non empty commutative multLoopStr_0 st b1 is almost_left_invertible holds
b1 is almost_right_invertible
proof end;
coherence
for b1 being non empty commutative multLoopStr_0 st b1 is almost_right_invertible holds
b1 is almost_left_invertible
proof end;
coherence
for b1 being non empty commutative multLoopStr_0 st b1 is almost_right_cancelable holds
b1 is almost_left_cancelable
proof end;
coherence
for b1 being non empty commutative multLoopStr_0 st b1 is almost_left_cancelable holds
b1 is almost_right_cancelable
proof end;
coherence
for b1 being non empty commutative multMagma st b1 is right_mult-cancelable holds
b1 is left_mult-cancelable
proof end;
coherence
for b1 being non empty commutative multMagma st b1 is left_mult-cancelable holds
b1 is right_mult-cancelable
proof end;
end;

registration
coherence
proof end;
end;

registration
let a be Element of N_Real;
let r be Real;
identify - a with - r when a = r;
compatibility
( a = r implies - a = - r )
proof end;
end;

registration
let a, b be Element of N_Real;
let r, s be Real;
identify a - b with r - s when a = r, b = s;
compatibility
( a = r & b = s implies a - b = r - s )
;
end;

registration
let a be Element of N_Real;
let r, s be Real;
identify r * a with r * s when a = s;
compatibility
( a = s implies r * a = r * s )
by BINOP_2:def 11;
end;

registration
let a be Element of N_Real;
identify with |.a.|;
compatibility by EUCLID:def 2;
end;

theorem Th8: :: CAYLDICK:8
for a being Element of N_Real holds a * a = ^2
proof end;

registration
let a be Element of N_Real;
reduce a *' to a;
reducibility
a *' = a
;
end;

registration
coherence
proof end;
end;

registration
existence
ex b1 being non empty ConjNormAlgStr st
( b1 is strict & not b1 is degenerated & b1 is real-membered & b1 is reflexive & b1 is discerning & b1 is zeroed & b1 is complementable & b1 is add-associative & b1 is Abelian & b1 is associative & b1 is commutative & b1 is distributive & b1 is well-unital & b1 is add-cancelable & b1 is vector-associative & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital & b1 is Banach_Algebra-like_1 & b1 is Banach_Algebra-like_2 & b1 is Banach_Algebra-like_3 & b1 is well-conjugated & b1 is add-conjugative & b1 is norm-conjugative & b1 is scalar-conjugative & b1 is almost_left_invertible & b1 is almost_left_cancelable & b1 is RealNormSpace-like )
proof end;
end;

registration
coherence
( not 0. N_Real is left_invertible & not 0. N_Real is right_invertible )
;
end;

registration
let a be non zero Element of N_Real;
let r be Real;
identify / a with r " when a = r;
compatibility
( a = r implies / a = r " )
proof end;
end;

registration
let X be non trivial discerning ConjNormAlgStr ;
let x be non zero Element of X;
cluster -> non zero ;
coherence
not is zero
proof end;
end;

registration
cluster non zero -> non empty non zero for Element of the carrier of N_Real;
coherence
for b1 being non zero Element of N_Real holds not b1 is empty
proof end;
end;

registration
cluster non zero -> non zero mult-cancelable for Element of the carrier of N_Real;
coherence
for b1 being non zero Element of N_Real holds b1 is mult-cancelable
proof end;
end;

registration
let N be non empty well-conjugated ConjNormAlgStr ;
cluster -> well-conjugated for Element of the carrier of N;
coherence
for b1 being Element of N holds b1 is well-conjugated
by Def4;
end;

registration
let N be non empty well-conjugated ConjNormAlgStr ;
let a be zero Element of N;
cluster a *' -> zero ;
coherence
a *' is zero
by Def3;
end;

registration
let N be non empty well-conjugated ConjNormAlgStr ;
reduce (0. N) *' to 0. N;
reducibility
(0. N) *' = 0. N
by STRUCT_0:def 12;
end;

registration
let N be non degenerated right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning left-distributive well-conjugated ConjNormAlgStr ;
let a be non zero Element of N;
cluster a *' -> non zero ;
coherence
not a *' is zero
proof end;
end;

theorem Th9: :: CAYLDICK:9
for N being non empty ConjNormAlgStr st N is add-associative & N is right_zeroed & N is right_complementable & N is well-conjugated & N is reflexive & N is scalar-distributive & N is scalar-unital & N is vector-distributive & N is left-distributive holds
for a being Element of N holds (a *') * a = () * (1. N)
proof end;

registration end;

Lm1: for N being non empty ConjNormAlgStr st ( N is left_unital or N is right_unital ) & N is Banach_Algebra-like_2 & N is almost_right_cancelable & N is well-conjugated & N is scalar-unital holds
(1. N) *' = 1. N

proof end;

registration
let N be non empty almost_right_cancelable scalar-unital left_unital Banach_Algebra-like_2 well-conjugated ConjNormAlgStr ;
reduce (1. N) *' to 1. N;
reducibility
(1. N) *' = 1. N
by Lm1;
end;

registration
let N be non empty almost_right_cancelable scalar-unital right_unital Banach_Algebra-like_2 well-conjugated ConjNormAlgStr ;
reduce (1. N) *' to 1. N;
reducibility
(1. N) *' = 1. N
by Lm1;
end;

theorem Th10: :: CAYLDICK:10
for N being non empty ConjNormAlgStr
for a being Element of N st N is well-conjugated & N is reflexive & N is discerning & N is RealNormSpace-like & N is vector-distributive & N is scalar-distributive & N is scalar-associative & N is scalar-unital & N is Abelian & N is add-associative & N is right_zeroed & N is right_complementable & N is associative & N is distributive & N is well-unital & not N is degenerated & N is almost_left_invertible holds
(- a) *' = - (a *')
proof end;

theorem :: CAYLDICK:11
for N being non empty ConjNormAlgStr
for a, b being Element of N st N is well-conjugated & N is reflexive & N is discerning & N is RealNormSpace-like & N is vector-distributive & N is scalar-distributive & N is scalar-associative & N is scalar-unital & N is Abelian & N is add-associative & N is right_zeroed & N is right_complementable & N is associative & N is distributive & N is well-unital & not N is degenerated & N is almost_left_invertible & N is add-conjugative holds
(a - b) *' = (a *') - (b *')
proof end;

definition
let N be non empty ConjNormAlgStr ;
func Cayley-Dickson N -> strict ConjNormAlgStr means :Def9: :: CAYLDICK:def 9
( the carrier of it = product <% the carrier of N, the carrier of N%> & the ZeroF of it = <%(0. N),(0. N)%> & the OneF of it = <%(1. N),(0. N)%> & ( for a1, a2, b1, b2 being Element of N holds
( the addF of it . (<%a1,b1%>,<%a2,b2%>) = <%(a1 + a2),(b1 + b2)%> & the multF of it . (<%a1,b1%>,<%a2,b2%>) = <%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%> ) ) & ( for r being Real
for a, b being Element of N holds the Mult of it . (r,<%a,b%>) = <%(r * a),(r * b)%> ) & ( for a, b being Element of N holds
( the normF of it . <%a,b%> = sqrt (() + ()) & the conjugateF of it . <%a,b%> = <%(a *'),(- b)%> ) ) );
existence
ex b1 being strict ConjNormAlgStr st
( the carrier of b1 = product <% the carrier of N, the carrier of N%> & the ZeroF of b1 = <%(0. N),(0. N)%> & the OneF of b1 = <%(1. N),(0. N)%> & ( for a1, a2, b1, b2 being Element of N holds
( the addF of b1 . (<%a1,b1%>,<%a2,b2%>) = <%(a1 + a2),(b1 + b2)%> & the multF of b1 . (<%a1,b1%>,<%a2,b2%>) = <%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%> ) ) & ( for r being Real
for a, b being Element of N holds the Mult of b1 . (r,<%a,b%>) = <%(r * a),(r * b)%> ) & ( for a, b being Element of N holds
( the normF of b1 . <%a,b%> = sqrt (() + ()) & the conjugateF of b1 . <%a,b%> = <%(a *'),(- b)%> ) ) )
proof end;
uniqueness
for b1, b2 being strict ConjNormAlgStr st the carrier of b1 = product <% the carrier of N, the carrier of N%> & the ZeroF of b1 = <%(0. N),(0. N)%> & the OneF of b1 = <%(1. N),(0. N)%> & ( for a1, a2, b1, b2 being Element of N holds
( the addF of b1 . (<%a1,b1%>,<%a2,b2%>) = <%(a1 + a2),(b1 + b2)%> & the multF of b1 . (<%a1,b1%>,<%a2,b2%>) = <%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%> ) ) & ( for r being Real
for a, b being Element of N holds the Mult of b1 . (r,<%a,b%>) = <%(r * a),(r * b)%> ) & ( for a, b being Element of N holds
( the normF of b1 . <%a,b%> = sqrt (() + ()) & the conjugateF of b1 . <%a,b%> = <%(a *'),(- b)%> ) ) & the carrier of b2 = product <% the carrier of N, the carrier of N%> & the ZeroF of b2 = <%(0. N),(0. N)%> & the OneF of b2 = <%(1. N),(0. N)%> & ( for a1, a2, b1, b2 being Element of N holds
( the addF of b2 . (<%a1,b1%>,<%a2,b2%>) = <%(a1 + a2),(b1 + b2)%> & the multF of b2 . (<%a1,b1%>,<%a2,b2%>) = <%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%> ) ) & ( for r being Real
for a, b being Element of N holds the Mult of b2 . (r,<%a,b%>) = <%(r * a),(r * b)%> ) & ( for a, b being Element of N holds
( the normF of b2 . <%a,b%> = sqrt (() + ()) & the conjugateF of b2 . <%a,b%> = <%(a *'),(- b)%> ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines Cayley-Dickson CAYLDICK:def 9 :
for N being non empty ConjNormAlgStr
for b2 being strict ConjNormAlgStr holds
( b2 = Cayley-Dickson N iff ( the carrier of b2 = product <% the carrier of N, the carrier of N%> & the ZeroF of b2 = <%(0. N),(0. N)%> & the OneF of b2 = <%(1. N),(0. N)%> & ( for a1, a2, b1, b2 being Element of N holds
( the addF of b2 . (<%a1,b1%>,<%a2,b2%>) = <%(a1 + a2),(b1 + b2)%> & the multF of b2 . (<%a1,b1%>,<%a2,b2%>) = <%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%> ) ) & ( for r being Real
for a, b being Element of N holds the Mult of b2 . (r,<%a,b%>) = <%(r * a),(r * b)%> ) & ( for a, b being Element of N holds
( the normF of b2 . <%a,b%> = sqrt (() + ()) & the conjugateF of b2 . <%a,b%> = <%(a *'),(- b)%> ) ) ) );

registration
let N be non empty ConjNormAlgStr ;
coherence
not Cayley-Dickson N is empty
proof end;
end;

theorem Th12: :: CAYLDICK:12
for N being non empty ConjNormAlgStr
for c being Element of () ex a, b being Element of N st c = <%a,b%>
proof end;

theorem Th13: :: CAYLDICK:13
for N being non empty ConjNormAlgStr
for c being Element of () ex a1, b1, a2, b2 being Element of N st c = <%<%a1,b1%>,<%a2,b2%>%>
proof end;

definition
let N be non empty ConjNormAlgStr ;
let a, b be Element of N;
:: original: <%
redefine func <%a,b%> -> Element of ();
coherence
<%a,b%> is Element of ()
proof end;
end;

registration
let N be non empty ConjNormAlgStr ;
let a, b be zero Element of N;
cluster <%a,b%> -> zero for Element of ();
coherence
for b1 being Element of () st b1 = <%a,b%> holds
b1 is zero
proof end;
end;

registration
let N be non empty non degenerated ConjNormAlgStr ;
let a be non zero Element of N;
let b be Element of N;
cluster <%a,b%> -> non zero for Element of ();
coherence
for b1 being Element of () st b1 = <%a,b%> holds
not b1 is zero
proof end;
end;

registration
let N be non empty reflexive ConjNormAlgStr ;
coherence
proof end;
end;

registration
let N be non empty discerning ConjNormAlgStr ;
coherence
proof end;
end;

theorem Th14: :: CAYLDICK:14
for N being non empty ConjNormAlgStr
for a, b being Element of N st a is left_complementable & b is left_complementable holds
<%a,b%> is left_complementable
proof end;

theorem Th15: :: CAYLDICK:15
for N being non empty ConjNormAlgStr
for a, b being Element of N st <%a,b%> is left_complementable holds
( a is left_complementable & b is left_complementable )
proof end;

theorem Th16: :: CAYLDICK:16
for N being non empty ConjNormAlgStr
for a, b being Element of N st a is right_complementable & b is right_complementable holds
<%a,b%> is right_complementable
proof end;

theorem Th17: :: CAYLDICK:17
for N being non empty ConjNormAlgStr
for a, b being Element of N st <%a,b%> is right_complementable holds
( a is right_complementable & b is right_complementable )
proof end;

theorem :: CAYLDICK:18
for N being non empty ConjNormAlgStr
for a, b being Element of N st a is complementable & b is complementable holds
<%a,b%> is complementable by ;

theorem :: CAYLDICK:19
for N being non empty ConjNormAlgStr
for a, b being Element of N st <%a,b%> is complementable holds
( a is complementable & b is complementable ) by ;

theorem Th20: :: CAYLDICK:20
for N being non empty ConjNormAlgStr
for a, b being Element of N st a is left_add-cancelable & b is left_add-cancelable holds
proof end;

theorem Th21: :: CAYLDICK:21
for N being non empty ConjNormAlgStr
for a, b being Element of N st <%a,b%> is left_add-cancelable holds
proof end;

theorem Th22: :: CAYLDICK:22
for N being non empty ConjNormAlgStr
for a, b being Element of N st a is right_add-cancelable & b is right_add-cancelable holds
proof end;

theorem Th23: :: CAYLDICK:23
for N being non empty ConjNormAlgStr
for a, b being Element of N st <%a,b%> is right_add-cancelable holds
proof end;

theorem :: CAYLDICK:24
for N being non empty ConjNormAlgStr
for a, b being Element of N st a is add-cancelable & b is add-cancelable holds

theorem :: CAYLDICK:25
for N being non empty ConjNormAlgStr
for a, b being Element of N st <%a,b%> is add-cancelable holds

theorem :: CAYLDICK:26
for N being non empty ConjNormAlgStr
for a, b being Element of N st <%a,b%> is left_complementable & <%a,b%> is right_add-cancelable holds
- <%a,b%> = <%(- a),(- b)%>
proof end;

registration
let N be non empty add-associative ConjNormAlgStr ;
coherence
proof end;
end;

registration
let N be non empty right_zeroed ConjNormAlgStr ;
coherence
proof end;
end;

registration
let N be non empty left_zeroed ConjNormAlgStr ;
coherence
proof end;
end;

registration
let N be non empty right_complementable ConjNormAlgStr ;
coherence
proof end;
end;

registration
let N be non empty left_complementable ConjNormAlgStr ;
coherence
proof end;
end;

registration
let N be non empty Abelian ConjNormAlgStr ;
coherence
proof end;
end;

theorem Th27: :: CAYLDICK:27
for N being non empty ConjNormAlgStr
for a, b being Element of N st N is add-associative & N is right_zeroed & N is right_complementable holds
- <%a,b%> = <%(- a),(- b)%>
proof end;

theorem Th28: :: CAYLDICK:28
for N being non empty ConjNormAlgStr
for a1, a2, b1, b2 being Element of N st N is add-associative & N is right_zeroed & N is right_complementable holds
<%a1,b1%> - <%a2,b2%> = <%(a1 - a2),(b1 - b2)%>
proof end;

registration end;

registration
let N be non empty non degenerated ConjNormAlgStr ;
coherence
proof end;
end;

registration end;

registration end;

registration end;

registration end;

registration end;

registration end;

registration
let N be non empty vector-distributive ConjNormAlgStr ;
coherence
proof end;
end;

registration end;

registration
let N be non empty scalar-distributive ConjNormAlgStr ;
coherence
proof end;
end;

registration
let N be non empty scalar-associative ConjNormAlgStr ;
coherence
proof end;
end;

registration
let N be non empty scalar-unital ConjNormAlgStr ;
coherence
proof end;
end;

registration
let N be non empty reflexive Banach_Algebra-like_2 ConjNormAlgStr ;
coherence
proof end;
end;

registration end;

theorem :: CAYLDICK:29
for N being non degenerated right_complementable almost_right_cancelable almost_left_invertible Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative discerning reflexive RealNormSpace-like well-unital distributive associative Banach_Algebra-like_2 Banach_Algebra-like_3 well-conjugated add-conjugative ConjNormAlgStr
for a, b being Element of N st ( not a is zero or not b is zero ) & <%a,b%> is right_mult-cancelable & <%a,b%> is left_invertible holds
/ <%a,b%> = <%((1 / (() + ())) * (a *')),((1 / (() + ())) * (- b))%>
proof end;

registration end;

registration
coherence
proof end;
end;

set z = 0. N_Real;

set j = 1. N_Real;

set ZJ = <%(),()%>;

set ZZ = <%(),()%>;

set JZ = <%(),()%>;

set ZM = <%(),(- ())%>;

set MZ = <%(- ()),()%>;

Lm2: <%(),()%> * <%(),()%> = <%((() * ()) - ((() *') * ())),((() * ()) + ((() *') * ()))%> by Def9
.= <%(),((() *') * ())%> ;

::i*j = k in quaternions
theorem Th30: :: CAYLDICK:30
<%<%(),()%>,<%(),()%>%> * <%<%(),()%>,<%(),()%>%> = <%<%(),()%>,<%(),()%>%>
proof end;

::j*i = -k in quaternions
theorem Th31: :: CAYLDICK:31
<%<%(),()%>,<%(),()%>%> * <%<%(),()%>,<%(),()%>%> = <%<%(),()%>,<%(),(- ())%>%>
proof end;

registration
coherence
proof end;
end;

set ZZZZ = <%<%(),()%>,<%(),()%>%>;

set JZZZ = <%<%(),()%>,<%(),()%>%>;

set ZJZZ = <%<%(),()%>,<%(),()%>%>;

set ZZJZ = <%<%(),()%>,<%(),()%>%>;

set ZZZJ = <%<%(),()%>,<%(),()%>%>;

Lm3: <%(),()%> *' = <%(() *'),(- ())%>
by Def9;

::e1*e2 = e3 in octonions
theorem Th32: :: CAYLDICK:32
<%<%<%(),()%>,<%(),()%>%>,<%<%(),()%>,<%(),()%>%>%> * <%<%<%(),()%>,<%(),()%>%>,<%<%(),()%>,<%(),()%>%>%> = <%<%<%(),()%>,<%(),()%>%>,<%<%(),()%>,<%(),()%>%>%>
proof end;

::e2*e1 = -e3 in octonions
theorem Th33: :: CAYLDICK:33
<%<%<%(),()%>,<%(),()%>%>,<%<%(),()%>,<%(),()%>%>%> * <%<%<%(),()%>,<%(),()%>%>,<%<%(),()%>,<%(),()%>%>%> = <%<%<%(),()%>,<%(),(- ())%>%>,<%<%(),()%>,<%(),()%>%>%>
proof end;

::(e1*e2)*e5 = -e6 in octonions
theorem Th34: :: CAYLDICK:34
(<%<%<%(),()%>,<%(),()%>%>,<%<%(),()%>,<%(),()%>%>%> * <%<%<%(),()%>,<%(),()%>%>,<%<%(),()%>,<%(),()%>%>%>) * <%<%<%(),()%>,<%(),()%>%>,<%<%(),()%>,<%(),()%>%>%> = <%<%<%(),()%>,<%(),()%>%>,<%<%(),()%>,<%(- ()),()%>%>%>
proof end;

::e1*(e2*e5) = e6 in octonions
theorem Th35: :: CAYLDICK:35
<%<%<%(),()%>,<%(),()%>%>,<%<%(),()%>,<%(),()%>%>%> * (<%<%<%(),()%>,<%(),()%>%>,<%<%(),()%>,<%(),()%>%>%> * <%<%<%(),()%>,<%(),()%>%>,<%<%(),()%>,<%(),()%>%>%>) = <%<%<%(),()%>,<%(),()%>%>,<%<%(),()%>,<%(),()%>%>%>
proof end;

registration
coherence
proof end;
end;