:: Cayley-Dickson Construction
:: by Artur Korni{\l}owicz
::
:: Received August 6, 2012
:: 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;

cluster ||.x.|| -> positive ;

coherence
||.x.|| is positive

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 ;

cluster <%x%> -> non-empty ;

coherence
<%x%> is non-empty

proof end;

end;

registration

cluster Relation-like non-empty NAT -defined Function-like V25() V32() countable V65() for set ;

existence
ex b₁ being XFinSequence st b₁ 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 ;

cluster binop D -> commutative associative ;

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 b₁ being BinOp of D st
( b₁ is associative & b₁ is commutative )

proof end;

end;

definition

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

end;

registration

cluster non trivial strict for ConjNormAlgStr ;

existence
ex b₁ being ConjNormAlgStr st
( not b₁ is trivial & b₁ 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 = (||.a.|| ^2) * (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 = (||.a.|| ^2) * (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 *').|| = ||.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 *').|| = ||.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
ConjNormAlgStr(# D,m,a,M,O,Z,n,c #) is add-associative 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
ConjNormAlgStr(# REAL,multreal,addreal,multreal,(In (1,REAL)),(In (0,REAL)),absreal,(id REAL) #);

coherence
ConjNormAlgStr(# REAL,multreal,addreal,multreal,(In (1,REAL)),(In (0,REAL)),absreal,(id REAL) #) 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,(id REAL) #);

registration

cluster N_Real -> non degenerated Abelian add-associative associative commutative real-membered strict ;

coherence
( not N_Real is degenerated & N_Real is real-membered & N_Real is add-associative & N_Real is Abelian & N_Real is associative & N_Real is commutative ) ;

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

cluster non empty right_add-cancelable Abelian -> non empty left_add-cancelable Abelian for addMagma ;

coherence
for b₁ being non empty Abelian addMagma st b₁ is right_add-cancelable holds
b₁ is left_add-cancelable

proof end;

cluster non empty left_add-cancelable Abelian -> non empty right_add-cancelable Abelian for addMagma ;

coherence
for b₁ being non empty Abelian addMagma st b₁ is left_add-cancelable holds
b₁ is right_add-cancelable

proof end;

cluster non empty left_complementable Abelian -> non empty right_complementable Abelian for addLoopStr ;

coherence
for b₁ being non empty Abelian addLoopStr st b₁ is left_complementable holds
b₁ is right_complementable

proof end;

cluster non empty Abelian left-distributive commutative -> non empty Abelian right-distributive commutative for doubleLoopStr ;

coherence
for b₁ being non empty Abelian commutative doubleLoopStr st b₁ is left-distributive holds
b₁ is right-distributive

proof end;

cluster non empty Abelian right-distributive commutative -> non empty Abelian left-distributive commutative for doubleLoopStr ;

coherence
for b₁ being non empty Abelian commutative doubleLoopStr st b₁ is right-distributive holds
b₁ is left-distributive

proof end;

cluster non empty almost_left_invertible commutative -> non empty almost_right_invertible commutative for multLoopStr_0 ;

coherence
for b₁ being non empty commutative multLoopStr_0 st b₁ is almost_left_invertible holds
b₁ is almost_right_invertible

proof end;

cluster non empty almost_right_invertible commutative -> non empty almost_left_invertible commutative for multLoopStr_0 ;

coherence
for b₁ being non empty commutative multLoopStr_0 st b₁ is almost_right_invertible holds
b₁ is almost_left_invertible

proof end;

cluster non empty almost_right_cancelable commutative -> non empty almost_left_cancelable commutative for multLoopStr_0 ;

coherence
for b₁ being non empty commutative multLoopStr_0 st b₁ is almost_right_cancelable holds
b₁ is almost_left_cancelable

proof end;

cluster non empty almost_left_cancelable commutative -> non empty almost_right_cancelable commutative for multLoopStr_0 ;

coherence
for b₁ being non empty commutative multLoopStr_0 st b₁ is almost_left_cancelable holds
b₁ is almost_right_cancelable

proof end;

cluster non empty right_mult-cancelable commutative -> non empty left_mult-cancelable commutative for multMagma ;

coherence
for b₁ being non empty commutative multMagma st b₁ is right_mult-cancelable holds
b₁ is left_mult-cancelable

proof end;

cluster non empty left_mult-cancelable commutative -> non empty right_mult-cancelable commutative for multMagma ;

coherence
for b₁ being non empty commutative multMagma st b₁ is left_mult-cancelable holds
b₁ is right_mult-cancelable

proof end;

end;

registration

cluster N_Real -> right_add-cancelable right_complementable strict ;

coherence
( N_Real is right_complementable & N_Real is right_add-cancelable )

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 ||.a.|| with |.a.|;

compatibility
||.a.|| = |.a.| by EUCLID:def 2;

end;

theorem Th8: :: CAYLDICK:8

for a being Element of N_Real holds a * a = ||.a.|| ^2

proof end;

registration

let a be Element of N_Real;

reduce a *' to a;

reducibility
a *' = a ;

end;

registration

cluster N_Real -> almost_left_cancelable almost_left_invertible right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative discerning reflexive RealNormSpace-like right-distributive well-unital Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 strict well-conjugated add-conjugative norm-conjugative scalar-conjugative ;

coherence
( N_Real is reflexive & N_Real is discerning & N_Real is well-unital & N_Real is RealNormSpace-like & N_Real is right_zeroed & N_Real is right-distributive & N_Real is vector-associative & N_Real is vector-distributive & N_Real is scalar-distributive & N_Real is scalar-associative & N_Real is scalar-unital & N_Real is Banach_Algebra-like_1 & N_Real is Banach_Algebra-like_2 & N_Real is Banach_Algebra-like_3 & N_Real is almost_left_invertible & N_Real is almost_left_cancelable & N_Real is well-conjugated & N_Real is add-conjugative & N_Real is norm-conjugative & N_Real is scalar-conjugative )

proof end;

end;

registration

cluster non empty non degenerated add-cancelable complementable almost_left_cancelable almost_left_invertible Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital zeroed vector-associative discerning reflexive RealNormSpace-like well-unital distributive associative commutative Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 real-membered strict well-conjugated add-conjugative norm-conjugative scalar-conjugative for ConjNormAlgStr ;

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

proof end;

end;

registration

cluster 0. N_Real -> non left_invertible non right_invertible ;

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 ||.x.|| -> non zero ;

coherence
not ||.x.|| is zero

proof end;

end;

registration

cluster non zero -> non empty non zero for Element of the carrier of N_Real;

coherence
for b₁ being non zero Element of N_Real holds not b₁ is empty

proof end;

end;

registration

cluster non zero -> non zero mult-cancelable for Element of the carrier of N_Real;

coherence
for b₁ being non zero Element of N_Real holds b₁ 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 b₁ being Element of N holds b₁ 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 = (||.a.|| ^2) * (1. N)

proof end;

registration

let N be non degenerated right_complementable almost_right_cancelable almost_left_invertible add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive well-unital distributive associative commutative well-conjugated norm-conjugative ConjNormAlgStr ;
let a be Element of N;

reduce (a *') *' to a;

reducibility
(a *') *' = a

proof end;

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 ((||.a.|| ^2) + (||.b.|| ^2)) & the conjugateF of it . <%a,b%> = <%(a *'),(- b)%> ) ) );

existence
ex b₁ being strict ConjNormAlgStr st
( the carrier of b₁ = product <% the carrier of N, the carrier of N%> & the ZeroF of b₁ = <%(0. N),(0. N)%> & the OneF of b₁ = <%(1. N),(0. N)%> & ( for a1, a2, b1, b2 being Element of N holds
( the addF of b₁ . (<%a1,b1%>,<%a2,b2%>) = <%(a1 + a2),(b1 + b2)%> & the multF of b₁ . (<%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 b₁ . (r,<%a,b%>) = <%(r * a),(r * b)%> ) & ( for a, b being Element of N holds
( the normF of b₁ . <%a,b%> = sqrt ((||.a.|| ^2) + (||.b.|| ^2)) & the conjugateF of b₁ . <%a,b%> = <%(a *'),(- b)%> ) ) )

proof end;

uniqueness
for b₁, b₂ being strict ConjNormAlgStr st the carrier of b₁ = product <% the carrier of N, the carrier of N%> & the ZeroF of b₁ = <%(0. N),(0. N)%> & the OneF of b₁ = <%(1. N),(0. N)%> & ( for a1, a2, b1, b2 being Element of N holds
( the addF of b₁ . (<%a1,b1%>,<%a2,b2%>) = <%(a1 + a2),(b1 + b2)%> & the multF of b₁ . (<%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 b₁ . (r,<%a,b%>) = <%(r * a),(r * b)%> ) & ( for a, b being Element of N holds
( the normF of b₁ . <%a,b%> = sqrt ((||.a.|| ^2) + (||.b.|| ^2)) & the conjugateF of b₁ . <%a,b%> = <%(a *'),(- b)%> ) ) & the carrier of b₂ = product <% the carrier of N, the carrier of N%> & the ZeroF of b₂ = <%(0. N),(0. N)%> & the OneF of b₂ = <%(1. N),(0. N)%> & ( for a1, a2, b1, b2 being Element of N holds
( the addF of b₂ . (<%a1,b1%>,<%a2,b2%>) = <%(a1 + a2),(b1 + b2)%> & the multF of b₂ . (<%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 b₂ . (r,<%a,b%>) = <%(r * a),(r * b)%> ) & ( for a, b being Element of N holds
( the normF of b₂ . <%a,b%> = sqrt ((||.a.|| ^2) + (||.b.|| ^2)) & the conjugateF of b₂ . <%a,b%> = <%(a *'),(- b)%> ) ) holds
b₁ = b₂

proof end;

end;

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

registration

let N be non empty ConjNormAlgStr ;

cluster Cayley-Dickson N -> non empty strict ;

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 (Cayley-Dickson N) 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 (Cayley-Dickson (Cayley-Dickson N)) 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 (Cayley-Dickson N);
coherence
<%a,b%> is Element of (Cayley-Dickson N)

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 (Cayley-Dickson N);

coherence
for b₁ being Element of (Cayley-Dickson N) st b₁ = <%a,b%> holds
b₁ 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 (Cayley-Dickson N);

coherence
for b₁ being Element of (Cayley-Dickson N) st b₁ = <%a,b%> holds
not b₁ is zero

proof end;

end;

registration

let N be non empty reflexive ConjNormAlgStr ;

cluster Cayley-Dickson N -> reflexive strict ;

coherence
Cayley-Dickson N is reflexive

proof end;

end;

registration

let N be non empty discerning ConjNormAlgStr ;

cluster Cayley-Dickson N -> discerning strict ;

coherence
Cayley-Dickson N is discerning

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 Th14, Th16;

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 Th15, Th17;

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
<%a,b%> is left_add-cancelable

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
( a is left_add-cancelable & b is left_add-cancelable )

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
<%a,b%> is right_add-cancelable

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
( a is right_add-cancelable & b is right_add-cancelable )

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
<%a,b%> is add-cancelable by Th20, Th22;

theorem :: CAYLDICK:25

for N being non empty ConjNormAlgStr
for a, b being Element of N st <%a,b%> is add-cancelable holds
( a is add-cancelable & b is add-cancelable ) by Th21, Th23;

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 ;

cluster Cayley-Dickson N -> add-associative strict ;

coherence
Cayley-Dickson N is add-associative

proof end;

end;

registration

let N be non empty right_zeroed ConjNormAlgStr ;

cluster Cayley-Dickson N -> right_zeroed strict ;

coherence
Cayley-Dickson N is right_zeroed

proof end;

end;

registration

let N be non empty left_zeroed ConjNormAlgStr ;

cluster Cayley-Dickson N -> left_zeroed strict ;

coherence
Cayley-Dickson N is left_zeroed

proof end;

end;

registration

let N be non empty right_complementable ConjNormAlgStr ;

cluster Cayley-Dickson N -> right_complementable strict ;

coherence
Cayley-Dickson N is right_complementable

proof end;

end;

registration

let N be non empty left_complementable ConjNormAlgStr ;

cluster Cayley-Dickson N -> left_complementable strict ;

coherence
Cayley-Dickson N is left_complementable

proof end;

end;

registration

let N be non empty Abelian ConjNormAlgStr ;

cluster Cayley-Dickson N -> Abelian strict ;

coherence
Cayley-Dickson N is Abelian

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

let N be non empty right_complementable almost_right_cancelable add-associative right_zeroed scalar-unital well-unital distributive Banach_Algebra-like_2 well-conjugated ConjNormAlgStr ;

cluster Cayley-Dickson N -> well-unital strict ;

coherence
Cayley-Dickson N is well-unital

proof end;

end;

registration

let N be non empty non degenerated ConjNormAlgStr ;

cluster Cayley-Dickson N -> non degenerated strict ;

coherence
not Cayley-Dickson N is degenerated

proof end;

end;

registration

let N be non empty right_complementable Abelian add-associative right_zeroed add-conjugative ConjNormAlgStr ;

cluster Cayley-Dickson N -> strict add-conjugative ;

coherence
Cayley-Dickson N is add-conjugative

proof end;

end;

registration

let N be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like norm-conjugative ConjNormAlgStr ;

cluster Cayley-Dickson N -> strict norm-conjugative ;

coherence
Cayley-Dickson N is norm-conjugative

proof end;

end;

registration

let N be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital scalar-conjugative ConjNormAlgStr ;

cluster Cayley-Dickson N -> strict scalar-conjugative ;

coherence
Cayley-Dickson N is scalar-conjugative

proof end;

end;

registration

let N be non empty right_complementable Abelian add-associative right_zeroed distributive ConjNormAlgStr ;

cluster Cayley-Dickson N -> left-distributive strict ;

coherence
Cayley-Dickson N is left-distributive

proof end;

end;

registration

let N be non empty right_complementable Abelian add-associative right_zeroed distributive add-conjugative ConjNormAlgStr ;

cluster Cayley-Dickson N -> right-distributive strict ;

coherence
Cayley-Dickson N is right-distributive

proof end;

end;

registration

let N be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ConjNormAlgStr ;

cluster Cayley-Dickson N -> RealNormSpace-like strict ;

coherence
Cayley-Dickson N is RealNormSpace-like

proof end;

end;

registration

let N be non empty vector-distributive ConjNormAlgStr ;

cluster Cayley-Dickson N -> vector-distributive strict ;

coherence
Cayley-Dickson N is vector-distributive

proof end;

end;

registration

let N be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative Banach_Algebra-like_3 ConjNormAlgStr ;

cluster Cayley-Dickson N -> vector-associative strict ;

coherence
Cayley-Dickson N is vector-associative

proof end;

end;

registration

let N be non empty scalar-distributive ConjNormAlgStr ;

cluster Cayley-Dickson N -> scalar-distributive strict ;

coherence
Cayley-Dickson N is scalar-distributive

proof end;

end;

registration

let N be non empty scalar-associative ConjNormAlgStr ;

cluster Cayley-Dickson N -> scalar-associative strict ;

coherence
Cayley-Dickson N is scalar-associative

proof end;

end;

registration

let N be non empty scalar-unital ConjNormAlgStr ;

cluster Cayley-Dickson N -> scalar-unital strict ;

coherence
Cayley-Dickson N is scalar-unital

proof end;

end;

registration

let N be non empty reflexive Banach_Algebra-like_2 ConjNormAlgStr ;

cluster Cayley-Dickson N -> Banach_Algebra-like_2 strict ;

coherence
Cayley-Dickson N is Banach_Algebra-like_2

proof end;

end;

registration

let N be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative Banach_Algebra-like_3 scalar-conjugative ConjNormAlgStr ;

cluster Cayley-Dickson N -> Banach_Algebra-like_3 strict ;

coherence
Cayley-Dickson N is Banach_Algebra-like_3

proof end;

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.|| ^2) + (||.b.|| ^2))) * (a *')),((1 / ((||.a.|| ^2) + (||.b.|| ^2))) * (- b))%>

proof end;

registration

let N be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-unital discerning reflexive distributive well-conjugated ConjNormAlgStr ;

cluster Cayley-Dickson N -> strict well-conjugated ;

coherence
Cayley-Dickson N is well-conjugated

proof end;

end;

registration

cluster Cayley-Dickson N_Real -> associative commutative strict ;

coherence
( Cayley-Dickson N_Real is associative & Cayley-Dickson N_Real is commutative )

proof end;

end;

set z = 0. N_Real;

set j = 1. N_Real;

set ZJ = <%(0. N_Real),(1. N_Real)%>;

set ZZ = <%(0. N_Real),(0. N_Real)%>;

set JZ = <%(1. N_Real),(0. N_Real)%>;

set ZM = <%(0. N_Real),(- (1. N_Real))%>;

set MZ = <%(- (1. N_Real)),(0. N_Real)%>;

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

::i*j = k in quaternions

theorem Th30: :: CAYLDICK:30

<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%> * <%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%> = <%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(1. N_Real)%>%>

proof end;

::j*i = -k in quaternions

theorem Th31: :: CAYLDICK:31

<%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%> * <%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%> = <%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(- (1. N_Real))%>%>

proof end;

registration

cluster Cayley-Dickson (Cayley-Dickson N_Real) -> associative non commutative strict ;

coherence
( Cayley-Dickson (Cayley-Dickson N_Real) is associative & not Cayley-Dickson (Cayley-Dickson N_Real) is commutative )

proof end;

end;

set ZZZZ = <%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>;

set JZZZ = <%<%(1. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>;

set ZJZZ = <%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>;

set ZZJZ = <%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%>;

set ZZZJ = <%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(1. N_Real)%>%>;

Lm3: <%(0. N_Real),(1. N_Real)%> *' = <%((0. N_Real) *'),(- (1. N_Real))%>
by Def9;

::e1*e2 = e3 in octonions

theorem Th32: :: CAYLDICK:32

<%<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> * <%<%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> = <%<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(1. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%>

proof end;

::e2*e1 = -e3 in octonions

theorem Th33: :: CAYLDICK:33

<%<%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> * <%<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> = <%<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(- (1. N_Real))%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%>

proof end;

::(e1*e2)*e5 = -e6 in octonions

theorem Th34: :: CAYLDICK:34

(<%<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> * <%<%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%>) * <%<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> = <%<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(- (1. N_Real)),(0. N_Real)%>%>%>

proof end;

::e1*(e2*e5) = e6 in octonions

theorem Th35: :: CAYLDICK:35

<%<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> * (<%<%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> * <%<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%>) = <%<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%>%>

proof end;

registration

cluster Cayley-Dickson (Cayley-Dickson (Cayley-Dickson N_Real)) -> non associative non commutative strict ;

coherence
( not Cayley-Dickson (Cayley-Dickson (Cayley-Dickson N_Real)) is associative & not Cayley-Dickson (Cayley-Dickson (Cayley-Dickson N_Real)) is commutative )

proof end;

end;