:: Cayley-Dickson Construction
:: by Artur Korni{\l}owicz
::
:: Received August 6, 2012
:: Copyright (c) 2012-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, ALGSTR_0, STRUCT_0, CARD_1, ZFMISC_1, SUBSET_1,
ARYTM_3, RLVECT_1, SUPINF_2, ARYTM_1, RELAT_1, MESFUNC1, FUNCT_1,
VECTSP_1, NORMSP_0, AFINSQ_1, NUMBERS, BINOP_2, NORMSP_1, CARD_3,
FINSEQ_1, ORDINAL4, SQUARE_1, LOPBAN_2, BINOP_1, EUCLID, MEMBERED,
FUNCOP_1, XCMPLX_0, COMPLEX1, LATTICES, FUNCSDOM, XXREAL_0, RELAT_2,
METRIC_1, VALUED_0, ALGSTR_1, CAYLDICK, FUNCT_7, REAL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1,
FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, CARD_3,
XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, BINOP_2, MEMBERED, COMPLEX1,
AFINSQ_1, STRUCT_0, ALGSTR_0, ALGSTR_1, TOPMETR, RLVECT_1, GROUP_1,
VECTSP_1, FUNCSDOM, NORMSP_0, NORMSP_1, EUCLID, LOPBAN_2;
constructors BINARITH, NAT_D, AFINSQ_1, SQUARE_1, BINOP_2, EUCLID, LOPBAN_2,
TOPMETR, ALGSTR_1;
registrations RELSET_1, NUMBERS, XREAL_0, STRUCT_0, ALGSTR_0, MEMBERED,
VECTSP_1, NORMSP_0, AFINSQ_1, CARD_3, XXREAL_0, LOPBAN_2, ZFMISC_1,
FUNCT_2, XBOOLE_0, TOPMETR, BINOP_2, RELAT_1, FUNCT_1, SQUARE_1,
NORMSP_1, COMPLEX1, TOPREALC, RLVECT_1, ALGSTR_1, GROEB_2, ORDINAL1;
requirements NUMERALS, SUBSET, ARITHM, BOOLE, REAL;
definitions FUNCT_1, BINOP_1, STRUCT_0, ALGSTR_0, ALGSTR_1, GROUP_1, RLVECT_1,
VECTSP_1, FUNCSDOM, NORMSP_0, NORMSP_1, LOPBAN_2;
equalities BINOP_1, AFINSQ_1, SQUARE_1, STRUCT_0, ALGSTR_0, RLVECT_1,
NORMSP_0, ORDINAL1;
expansions STRUCT_0, ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1, LOPBAN_2, TOPMETR;
theorems CARD_3, TARSKI, AFINSQ_1, CARD_1, RELAT_1, XBOOLE_0, RLVECT_1,
ALGSTR_0, VECTSP_1, XREAL_0, FUNCT_2, ZFMISC_1, BINOP_1, BINOP_2,
FUNCOP_1, XCMPLX_1, EUCLID, COMPLEX1, STRUCT_0, LOPBAN_2, NORMSP_0,
SQUARE_1, ALGSTR_1, NORMSP_1, XCMPLX_0, VECTSP_2, FUNCSDOM, XREAL_1,
XXREAL_0;
schemes FUNCT_2, BINOP_1;
begin :: Preliminaries
reserve u,v,x,y,z,X,Y for set;
reserve r,s for Real;
theorem Th1:
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
let a,b,c,d be Real;
set A = a^2+c^2, B = b^2+d^2, C1 = sqrt(A), C2 = sqrt(B);
A1: 0 <= C1 & 0 <= C2 by SQUARE_1:def 2;
A2: C1^2 = A & C2^2 = B by SQUARE_1:def 2;
A3: a^2+2*a*b+b^2 + (c^2+2*c*d+d^2) = a^2+c^2+b^2+d^2+(2*a*b+2*c*d);
A4: A+2*C1*C2+B = A+B+2*C1*C2;
A5: 2*a*b+2*c*d = 2*(a*b+c*d);
A6: 2*(C1*C2) = 2*C1*C2;
(a*d-c*b)^2 = (a*d)^2+(c*b)^2-2*(a*d)*(c*b);
then
A7: 0+2*(a*d)*(c*b) <=
(a*d)^2+(c*b)^2-2*(a*d)*(c*b)+2*(a*d)*(c*b) by XREAL_1:6;
A8: A*B = (sqrt(A*B))^2 by SQUARE_1:def 2;
a^2*b^2+c^2*d^2+(2*a*b*c*d) <= a^2*b^2+c^2*d^2+(c^2*b^2+a^2*d^2)
by A7,XREAL_1:6;
then
A9: (a*b+c*d)^2 <= A*B;
C1*C2 = sqrt(A*B) by SQUARE_1:29;
then a*b+c*d <= C1*C2 by A1,A8,A9,SQUARE_1:16;
then 2*a*b+2*c*d <= 2*C1*C2 by A5,A6,XREAL_1:64;
hence thesis by A2,A3,A4,XREAL_1:6;
end;
registration
let X be non trivial RealNormSpace;
let x be non zero Element of X;
cluster ||.x.|| -> positive;
coherence
proof
x <> 0.X;
then 0 <> ||.x.|| by NORMSP_0:def 5;
hence thesis;
end;
end;
registration
let c be non zero Complex;
cluster c^2 -> non zero;
coherence by XCMPLX_1:6;
end;
registration
let x be non empty set;
cluster <% x %> -> non-empty;
coherence
proof
let y be object;
assume y in dom <%x%>;
then y in 1 by AFINSQ_1:def 4;
then y = 0 by CARD_1:49,TARSKI:def 1;
hence thesis;
end;
end;
registration
cluster non-empty for XFinSequence;
existence
proof
take <%the non empty set%>;
thus thesis;
end;
end;
registration
let f,g be non-empty XFinSequence;
cluster f^g -> non-empty;
coherence
proof
A1: rng(f^g) = rng f \/ rng g by AFINSQ_1:26;
not {} in rng f & not {} in rng g by RELAT_1:def 9;
then not {} in rng (f^g) by A1,XBOOLE_0:def 3;
hence thesis by RELAT_1:def 9;
end;
end;
registration
let x,y be non empty set;
cluster <% x,y %> -> non-empty;
coherence;
end;
theorem
<%u%> = <%x%> implies u = x
proof
<%u%>.0 = u & <%x%>.0 = x;
hence thesis;
end;
theorem Th3:
<%u,v%> = <%x,y%> implies u = x & v = y
proof
<%u,v%>.0 = u & <%u,v%>.1 = v & <%x,y%>.0 = x & <%x,y%>.1 = y;
hence thesis;
end;
theorem
x in X implies <%x%> in product <%X%>
proof
set f = <%X%>;
set g = <%x%>;
assume
A1: x in X;
A2: len f = 1 by AFINSQ_1:34;
A3: len g = dom g;
now
let a be object;
assume a in dom f;
then a = 0 by A2,CARD_1:49,TARSKI:def 1;
hence g.a in f.a by A1;
end;
hence thesis by A2,A3,CARD_3:9,AFINSQ_1:34;
end;
theorem
z in product <%X%> implies ex x st x in X & z = <%x%>
proof
assume z in product <%X%>;
then consider f being Function such that
A1: z = f and
A2: dom f = dom <%X%> and
A3: for x being object st x in dom <%X%> holds f.x in <%X%>.x by CARD_3:def 5;
reconsider f as XFinSequence by A2,AFINSQ_1:5;
take f.0;
A4: 0 in {0} by TARSKI:def 1;
A5: <%X%>.0 = X;
len <%X%> = 1 by AFINSQ_1:34;
then len f = 1 by A2;
hence thesis by A5,A4,A1,A2,A3,AFINSQ_1:34,CARD_1:49;
end;
theorem Th6:
x in X & y in Y implies <%x,y%> in product <%X,Y%>
proof
set f = <%X,Y%>;
set g = <%x,y%>;
assume
A1: x in X & y in Y;
A2: len f = 2 by AFINSQ_1:38;
A3: len g = dom g;
now
let a be object;
assume a in dom f;
then a = 0 or a = 1 by A2,TARSKI:def 2,CARD_1:50;
hence g.a in f.a by A1;
end;
hence thesis by A2,A3,CARD_3:9,AFINSQ_1:38;
end;
theorem Th7:
z in product <%X,Y%> implies ex x,y st x in X & y in Y & z = <%x,y%>
proof
assume z in product <%X,Y%>;
then consider f being Function such that
A1: z = f and
A2: dom f = dom <%X,Y%> and
A3: for x being object st x in dom <%X,Y%> holds f.x in <%X,Y%>.x
by CARD_3:def 5;
reconsider f as XFinSequence by A2,AFINSQ_1:5;
take f.0, f.1;
A4: 0 in {0,1} & 1 in {0,1} by TARSKI:def 2;
A5: <%X,Y%>.0 = X & <%X,Y%>.1 = Y;
len <%X,Y%> = 2 by AFINSQ_1:38;
then len f = 2 by A2;
hence thesis by A5,A4,A1,A2,A3,AFINSQ_1:38,CARD_1:50;
end;
definition
let D be set;
func binop(D) -> BinOp of D equals
[:D,D:] --> the Element of D;
coherence
proof
per cases;
suppose D is non empty;
then reconsider D as non empty set;
[:D,D:] --> the Element of D is BinOp of D;
hence thesis;
end;
suppose D is empty;
hence thesis;
end;
end;
end;
registration
let D be set;
cluster binop(D) -> associative commutative;
coherence
proof
set f = binop(D);
thus f is associative
proof
let a,b,c be Element of D;
per cases;
suppose
A1: D is non empty;
hence f.(a,f.(b,c)) = the Element of D by ZFMISC_1:87,FUNCOP_1:7
.= f.(f.(a,b),c) by A1,ZFMISC_1:87,FUNCOP_1:7;
end;
suppose
A2: D is empty;
hence f.(a,f.(b,c)) = {}
.= f.(f.(a,b),c) by A2;
end;
end;
let a,b be Element of D;
per cases;
suppose
A3: D is non empty;
hence f.(a,b) = the Element of D by ZFMISC_1:87,FUNCOP_1:7
.= f.(b,a) by A3,ZFMISC_1:87,FUNCOP_1:7;
end;
suppose
A4: D is empty;
hence f.(a,b) = {}
.= f.(b,a) by A4;
end;
end;
end;
registration
let D be set;
cluster associative commutative for BinOp of D;
existence
proof
take binop(D);
thus thesis;
end;
end;
begin :: Conjunctive normed spaces
definition
struct (Normed_AlgebraStr) ConjNormAlgStr
(# carrier -> set,
multF,addF -> BinOp of the carrier,
Mult -> Function of [:REAL,the carrier:],the carrier,
OneF,ZeroF -> Element of the carrier,
normF -> Function of the carrier,REAL,
conjugateF -> Function of the carrier,the carrier #);
end;
registration
cluster non trivial strict for ConjNormAlgStr;
existence
proof
set A = the non trivial set;
take ConjNormAlgStr (# A,the BinOp of A,the BinOp of A,
the Function of [:REAL,A:],A, the Element of A,the Element of A,
the Function of A,REAL, the Function of A,A #);
thus thesis;
end;
end;
reserve N for non empty ConjNormAlgStr;
reserve a,a1,a2,b,b1,b2 for Element of N;
definition
let N be non empty ConjNormAlgStr;
let a be Element of N;
func a *' -> Element of N equals
(the conjugateF of N).a;
coherence;
end;
definition
let N be non empty ConjNormAlgStr, a be Element of N;
attr a is well-conjugated means :Def3:
a*' * a = ||.a.||^2 * 1.N if a is non zero
otherwise a*' is zero;
consistency;
end;
definition
let N be non empty ConjNormAlgStr;
attr N is well-conjugated means :Def4:
for a being Element of N holds a is well-conjugated;
attr N is add-conjugative means :Def5:
for a,b being Element of N holds (a+b)*' = a*'+b*';
attr N is norm-conjugative means :Def6:
for a being Element of N holds ||.a*'.|| = ||.a.||;
attr N is scalar-conjugative means :Def7:
for r being Real, a being Element of N holds r*(a*') = (r*a)*';
end;
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;
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
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
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 by BINOP_1:def 2;
end;
definition
func N_Real -> strict ConjNormAlgStr equals
ConjNormAlgStr (# REAL,multreal,addreal,multreal,In(1,REAL),
In(0,REAL),absreal,id REAL #);
coherence;
end;
registration
cluster N_Real -> non degenerated real-membered add-associative Abelian
associative commutative;
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 by BINOP_2:def 9;
identify a*b with r*s when a = r, b = s;
compatibility by BINOP_2:def 11;
end;
registration
cluster right_add-cancelable -> left_add-cancelable
for Abelian non empty addMagma;
coherence
proof
let M be Abelian non empty addMagma;
assume
A1: M is right_add-cancelable;
let x,y,z be Element of M;
assume x+y = x+z;
hence thesis by A1,ALGSTR_0:def 4;
end;
cluster left_add-cancelable -> right_add-cancelable
for Abelian non empty addMagma;
coherence
proof
let M be Abelian non empty addMagma such that
A2: M is left_add-cancelable;
let x,y,z be Element of M;
assume y+x = z+x;
hence thesis by A2,ALGSTR_0:def 3;
end;
cluster left_complementable -> right_complementable
for Abelian non empty addLoopStr;
coherence
proof
let M be Abelian non empty addLoopStr such that
A3: M is left_complementable;
let x be Element of M;
ex y being Element of M st y+x = 0.M by A3,ALGSTR_0:def 10;
hence x is right_complementable;
end;
cluster left-distributive -> right-distributive
for Abelian commutative non empty doubleLoopStr;
coherence
proof
let M be Abelian commutative non empty doubleLoopStr such that
A4: M is left-distributive;
let x,y,z be Element of M;
thus x*(y+z) = x*y+x*z by A4;
end;
cluster right-distributive -> left-distributive
for Abelian commutative non empty doubleLoopStr;
coherence
proof
let M be Abelian commutative non empty doubleLoopStr such that
A5: M is right-distributive;
let x,y,z be Element of M;
thus (y+z)*x = y*x+z*x by A5;
end;
cluster almost_left_invertible -> almost_right_invertible
for commutative non empty multLoopStr_0;
coherence
proof
let M be commutative non empty multLoopStr_0 such that
A6: M is almost_left_invertible;
let x be Element of M;
assume x <> 0.M;
then consider y being Element of M such that
A7: y*x = 1.M by A6;
take y;
thus thesis by A7;
end;
cluster almost_right_invertible -> almost_left_invertible
for commutative non empty multLoopStr_0;
coherence
proof
let M be commutative non empty multLoopStr_0 such that
A8: M is almost_right_invertible;
let x be Element of M;
assume x <> 0.M;
then consider y being Element of M such that
A9: x*y = 1.M by A8,ALGSTR_0:def 28;
take y;
thus thesis by A9;
end;
cluster almost_right_cancelable -> almost_left_cancelable
for commutative non empty multLoopStr_0;
coherence
proof
let M be commutative non empty multLoopStr_0 such that
A10: M is almost_right_cancelable;
let x be Element of M;
assume
A11: x <> 0.M;
let y,z be Element of M;
assume x*y = x*z;
hence thesis by A10,A11,ALGSTR_0:def 21;
end;
cluster almost_left_cancelable -> almost_right_cancelable
for commutative non empty multLoopStr_0;
coherence
proof
let M be commutative non empty multLoopStr_0 such that
A12: M is almost_left_cancelable;
let x be Element of M;
assume
A13: x <> 0.M;
let y,z be Element of M;
assume y*x = z*x;
hence thesis by A12,A13,ALGSTR_0:def 20;
end;
cluster right_mult-cancelable -> left_mult-cancelable
for commutative non empty multMagma;
coherence
proof
let M be commutative non empty multMagma such that
A14: M is right_mult-cancelable;
let x,y,z be Element of M;
assume x*y = x*z;
hence thesis by A14,ALGSTR_0:def 21;
end;
cluster left_mult-cancelable -> right_mult-cancelable
for commutative non empty multMagma;
coherence
proof
let M be commutative non empty multMagma such that
A15: M is left_mult-cancelable;
let x,y,z be Element of M;
assume y*x = z*x;
hence thesis by A15,ALGSTR_0:def 20;
end;
end;
registration
cluster N_Real -> right_complementable right_add-cancelable;
coherence
proof
thus N_Real is right_complementable
proof
let a be Element of N_Real;
reconsider b = -(a qua Real) as Element of N_Real
by XREAL_0:def 1;
take b;
thus thesis;
end;
let a be Element of N_Real;
thus for b,c being Element of N_Real st b+a = c+a holds b = c;
end;
end;
registration
let a be Element of N_Real;
let r be Real;
identify -a with -r when a = r;
compatibility
proof
assume
A1: a = r;
reconsider b = -r as Element of N_Real by XREAL_0:def 1;
b+a = 0.N_Real by A1;
hence thesis by ALGSTR_0:def 13;
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;
end;
registration
let a be Element of N_Real;
let r,s be Real;
identify r*a with r*s when a = s;
compatibility by BINOP_2:def 11;
end;
registration
let a be Element of N_Real;
identify ||.a.|| with |.a.|;
compatibility by EUCLID:def 2;
end;
theorem Th8:
for a being Element of N_Real holds a*a = ||.a.||^2
proof
let a be Element of N_Real;
reconsider x = a as Element of REAL;
thus a*a = x^2
.= ||.a.||^2 by COMPLEX1:75;
end;
registration
let a be Element of N_Real;
reduce a*' to a;
reducibility;
end;
registration
cluster N_Real -> reflexive discerning well-unital RealNormSpace-like
right_zeroed right-distributive
vector-associative
vector-distributive scalar-distributive scalar-associative scalar-unital
Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3
almost_left_invertible almost_left_cancelable
well-conjugated add-conjugative norm-conjugative scalar-conjugative;
coherence
proof
thus ||.0.N_Real.|| = 0;
thus for a being Element of N_Real st ||.a.|| = 0 holds a = 0.N_Real;
thus for a being Element of N_Real holds a*1.N_Real = a & 1.N_Real*a = a;
thus for a,b being Element of N_Real, r holds
||.r*a.|| = |.r.| * ||.a.|| & ||.a+b.|| <= ||.a.|| + ||.b.||
by COMPLEX1:56,65;
thus for a being Element of N_Real holds a+0.N_Real = a;
thus for a,b,c being Element of N_Real holds a*(b+c) = a*b+a*c;
thus for a,b being Element of N_Real for r holds r*(a*b) = (r*a)*b;
thus for r for a,b being Element of N_Real holds r*(a+b) = r*a+r*b;
thus for r,s for a being Element of N_Real holds (r+s)*a = r*a+s*a;
thus for r,s for a being Element of N_Real holds (r*s)*a = r*(s*a);
thus for a being Element of N_Real holds 1 * a = a;
thus for a,b being Element of N_Real holds ||.a*b.|| <= ||.a.|| * ||.b.||
by COMPLEX1:65;
thus ||.1.N_Real.|| = 1 by COMPLEX1:43;
thus for r for a,b being Element of N_Real holds r*(a*b)=a*(r*b);
thus for a being Element of N_Real st a <> 0.N_Real
ex b be Element of N_Real st b*a = 1.N_Real
proof
let a be Element of N_Real such that
A1: a <> 0.N_Real;
reconsider b = a qua Real" as Element of N_Real by XREAL_0:def 1;
take b;
thus thesis by A1,XCMPLX_0:def 7;
end;
thus for a being Element of N_Real st a <> 0.N_Real holds
a is left_mult-cancelable
by XCMPLX_1:5;
thus N_Real is well-conjugated
proof
let a be Element of N_Real;
per cases;
case a is non zero;
thus a*'*a = ||.a.||^2*1.N_Real by Th8;
end;
case a is zero;
hence a*' = 0.N_Real;
end;
end;
thus for a,b being Element of N_Real holds (a+b)*' = a*'+b*';
thus for a being Element of N_Real holds ||.a*'.|| = ||.a.||;
thus for r for a being Element of N_Real holds r*(a*') = (r*a)*';
end;
end;
registration
cluster strict non degenerated real-membered reflexive discerning
zeroed complementable add-associative Abelian
associative commutative distributive well-unital add-cancelable
vector-associative
vector-distributive scalar-distributive scalar-associative scalar-unital
Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3
well-conjugated add-conjugative norm-conjugative scalar-conjugative
almost_left_invertible almost_left_cancelable RealNormSpace-like
for non empty ConjNormAlgStr;
existence
proof
take N_Real;
thus thesis;
end;
end;
registration
cluster 0.N_Real -> non left_invertible non right_invertible;
coherence;
end;
registration
let a be non zero Element of N_Real;
let r be Real;
identify a" with r" when a = r;
compatibility
proof
assume
A1: a = r;
reconsider b = r" as Element of N_Real by XREAL_0:def 1;
A2: a <> 0.N_Real;
then b*a = 1.N_Real by A1,XCMPLX_0:def 7;
hence thesis by A2,VECTSP_2:def 2;
end;
end;
registration
let X be discerning non trivial ConjNormAlgStr;
let x be non zero Element of X;
cluster ||.x.|| -> non zero;
coherence
proof
x <> 0.X;
hence thesis by NORMSP_0:def 5;
end;
end;
registration
cluster -> non empty for non zero Element of N_Real;
coherence
proof
let a be non zero Element of N_Real;
0.N_Real = 0;
hence thesis;
end;
end;
registration
cluster -> mult-cancelable for non zero Element of N_Real;
coherence
proof
let x be non zero Element of N_Real;
thus x is right_mult-cancelable
by XCMPLX_1:5;
let y,z be Element of N_Real;
thus thesis by XCMPLX_1:5;
end;
end;
registration
let N be well-conjugated non empty ConjNormAlgStr;
cluster -> well-conjugated for Element of N;
coherence by Def4;
end;
registration
let N be well-conjugated non empty ConjNormAlgStr;
let a be zero Element of N;
cluster a*' -> zero;
coherence by Def3;
end;
registration
let N be well-conjugated non empty ConjNormAlgStr;
reduce 0.N *' to 0.N;
reducibility by STRUCT_0:def 12;
end;
registration
let N be well-conjugated discerning
add-associative right_zeroed right_complementable left-distributive
scalar-distributive scalar-associative scalar-unital vector-distributive
non degenerated ConjNormAlgStr;
let a be non zero Element of N;
cluster a*' -> non zero;
coherence
proof
assume a*' is zero;
then
A1: a*' = 0.N;
a*' * a = ||.a.||^2 * 1.N by Def3;
hence thesis by A1,RLVECT_1:11;
end;
end;
theorem Th9:
N is add-associative right_zeroed right_complementable well-conjugated
reflexive scalar-distributive scalar-unital vector-distributive
left-distributive
implies for a holds a*' * a = ||.a.||^2 * 1.N
proof
assume that
A1: N is add-associative right_zeroed right_complementable and
A2: N is well-conjugated and
A3: N is reflexive and
A4: N is scalar-distributive scalar-unital vector-distributive
left-distributive;
let a;
per cases;
suppose a is non zero;
hence a*' * a = ||.a.||^2 * 1.N by A2,Def3;
end;
suppose
A5: a is zero;
then
A6: a = 0.N & a*' = 0.N by A2;
A7: ||.a.||^2 = 0 by A3,A5;
0 * 1.N = 0.N by A1,A4,RLVECT_1:10;
hence thesis by A1,A6,A4,A7;
end;
end;
registration
let N be well-conjugated reflexive discerning
add-associative right_zeroed right_complementable almost_right_cancelable
associative commutative well-unital almost_left_invertible distributive
scalar-distributive scalar-associative scalar-unital vector-distributive
norm-conjugative non degenerated ConjNormAlgStr;
let a be Element of N;
reduce a*'*' to a;
reducibility
proof
per cases;
suppose
A1: a is non zero;
then
A2: a*' * a = ||.a.||^2 * 1.N by Def3;
A3: a*'*' * a*' = ||.a*'.||^2 * 1.N by A1,Def3;
A4: ||.a*'.|| = ||.a.|| by Def6;
a*' <> 0.N by A1;
hence thesis by A2,A3,A4,ALGSTR_0:def 21,def 37;
end;
suppose a is zero;
then a = 0.N;
hence thesis;
end;
end;
end;
Lm1:
(N is left_unital or N is right_unital) &
N is Banach_Algebra-like_2 almost_right_cancelable well-conjugated
scalar-unital implies (1.N)*' = 1.N
proof
assume that
A1: N is left_unital or N is right_unital and
A2: N is Banach_Algebra-like_2 and
A3: N is almost_right_cancelable and
A4: N is well-conjugated and
A5: N is scalar-unital;
per cases;
suppose
A6: 1.N is non zero;
then
A7: 1.N <> 0.N;
A8: ||.1.N.|| = 1 by A2;
(1.N)*' * 1.N = ||.1.N.||^2 * 1.N by A4,A6,Def3
.= 1.N by A8,A5
.= 1.N * 1.N by A1;
hence thesis by A3,A7,ALGSTR_0:def 21;
end;
suppose 1.N is zero;
then 1.N = 0.N*' by A4;
hence thesis by A4;
end;
end;
registration
let N be left_unital Banach_Algebra-like_2 almost_right_cancelable
well-conjugated scalar-unital non empty ConjNormAlgStr;
reduce (1.N)*' to 1.N;
reducibility by Lm1;
end;
registration
let N be right_unital Banach_Algebra-like_2 almost_right_cancelable
well-conjugated scalar-unital non empty ConjNormAlgStr;
reduce (1.N)*' to 1.N;
reducibility by Lm1;
end;
theorem Th10:
N is well-conjugated reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable associative
distributive well-unital non degenerated almost_left_invertible
implies (-a)*' = -(a*')
proof
assume that
A1: N is well-conjugated and
A2: N is reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable and
A3: N is associative and
A4: N is distributive and
A5: N is well-unital and
A6: N is non degenerated almost_left_invertible;
per cases;
suppose
A7: a is non zero;
then
A8: a*' * a = ||.a.||^2 * 1.N by A1,Def3;
A9: (-a)*' * -a = ||.-a.||^2 * 1.N by A1,A2,A6,A7,Def3;
A10: ||.-a.|| = ||.a.|| by A2,NORMSP_1:2;
A11: a <> 0.N by A7;
A12: a*/a = 1.N by A2,A3,A4,A5,A6,A11,VECTSP_2:9;
then
A13: (-a) * -/a = 1.N by A2,A4,VECTSP_1:10;
A14: a * -/a = -1.N by A2,A4,A12,VECTSP_1:8;
thus (-a)*' = (-a)*' * 1.N by A5
.= (-a)*' * (-a) * -/a by A13,A3
.= a*' * (a * -/a) by A8,A9,A10,A3
.= -(a*') by A2,A14,A4,A5,VECTSP_2:28;
end;
suppose a is zero;
then
A15: a = 0.N & a*' = 0.N by A1;
-0.N = 0.N by A2;
hence thesis by A15;
end;
end;
theorem
N is well-conjugated reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable associative
distributive well-unital non degenerated almost_left_invertible
add-conjugative
implies (a-b)*' = a*' - b*'
proof
assume that
A1: N is well-conjugated reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable associative
distributive well-unital non degenerated almost_left_invertible;
assume N is add-conjugative;
hence (a-b)*' = a*'+(-b)*'
.= a*'-b*' by A1,Th10;
end;
begin :: Cayley-Dickson construction
definition
let N be non empty ConjNormAlgStr;
func Cayley-Dickson(N) -> strict ConjNormAlgStr means :Def9:
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, 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
proof
set A = the carrier of N;
set C = product <%A,A%>;
defpred A[Element of C,Element of C,set] means
ex a1,a2,b1,b2 being Element of N st
$1 = <%a1,b1%> & $2 = <%a2,b2%> & $3 = <%a1+a2,b1+b2%>;
A1: for x,y being Element of C ex z being Element of C st A[x,y,z]
proof
let a,b be Element of C;
consider a1,b1 being set such that
A2: a1 in A & b1 in A and
A3: a = <%a1,b1%> by Th7;
consider a2,b2 being set such that
A4: a2 in A & b2 in A and
A5: b = <%a2,b2%> by Th7;
reconsider a1,a2,b1,b2 as Element of A by A2,A4;
take c = <%a1+a2,b1+b2%>;
thus c is Element of C by Th6;
thus thesis by A3,A5;
end;
consider add being Function of [:C,C:],C such that
A6: for x,y being Element of C holds A[x,y,add.(x,y)] from BINOP_1:sch 3(A1);
defpred M[Element of C,Element of C,set] means
ex a1,a2,b1,b2 being Element of N st
$1 = <%a1,b1%> & $2 = <%a2,b2%> & $3 = <%a1*a2-b2*'*b1,b2*a1+b1*a2*'%>;
A7: for x,y being Element of C ex z being Element of C st M[x,y,z]
proof
let a,b be Element of C;
consider a1,b1 being set such that
A8: a1 in A & b1 in A and
A9: a = <%a1,b1%> by Th7;
consider a2,b2 being set such that
A10: a2 in A & b2 in A and
A11: b = <%a2,b2%> by Th7;
reconsider a1,a2,b1,b2 as Element of A by A8,A10;
take z = <%a1*a2-b2*'*b1,b2*a1+b1*a2*'%>;
thus z is Element of C by Th6;
thus thesis by A9,A11;
end;
consider mult being Function of [:C,C:],C such that
A12: for x,y being Element of C holds M[x,y,mult.(x,y)] from BINOP_1:sch 3(A7);
defpred MU[Element of REAL,Element of C,set] means
ex a,b being Element of N st $2 = <%a,b%> & $3 = <%$1*a,$1*b%>;
A13: for x being Element of REAL,y being Element of C ex z being Element of C
st MU[x,y,z]
proof
let r be Element of REAL, c be Element of C;
consider a,b being set such that
A14: a in A & b in A and
A15: c = <%a,b%> by Th7;
reconsider a,b as Element of A by A14;
take z = <%r*a,r*b%>;
thus z is Element of C by Th6;
thus thesis by A15;
end;
consider MU being Function of [:REAL,C:],C such that
A16: for x being Element of REAL, y being Element of C holds MU[x,y,MU.(x,y)]
from BINOP_1:sch 3(A13);
defpred N[Element of C,set] means
ex a,b being Element of N st $1 = <%a,b%> &
$2 = sqrt (||.a.||^2 + ||.b.||^2);
A17: for x being Element of C ex y being Element of REAL st N[x,y]
proof
let c be Element of C;
consider a,b being set such that
A18: a in A & b in A and
A19: c = <%a,b%> by Th7;
reconsider a,b as Element of A by A18;
take sqrt (||.a.||^2 + ||.b.||^2);
thus thesis by A19,XREAL_0:def 1,TARSKI:1;
end;
consider norm being Function of C,REAL such that
A20: for x being Element of C holds N[x,norm.x] from FUNCT_2:sch 3(A17);
defpred C[Element of C,set] means
ex a,b being Element of N st $1 = <%a,b%> & $2 = <%a*',-b%>;
A21: for x being Element of C ex y being Element of C st C[x,y]
proof
let c be Element of C;
consider a,b being set such that
A22: a in A & b in A and
A23: c = <%a,b%> by Th7;
reconsider a,b as Element of A by A22;
take <%a*',-b%>;
thus thesis by A23,Th6;
end;
consider conj being Function of C,C such that
A24: for x being Element of C holds C[x,conj.x] from FUNCT_2:sch 3(A21);
reconsider Z = <%0.N,0.N%>, O = <%1.N,0.N%> as Element of C by Th6;
take X = ConjNormAlgStr(#C,mult,add,MU,O,Z,norm,conj#);
thus the carrier of X = C & the ZeroF of X = <% 0.N,0.N %> &
the OneF of X = <% 1.N,0.N %>;
hereby
let a1,a2,b1,b2 be Element of N;
reconsider a = <%a1,b1%>, b = <%a2,b2%> as Element of C by Th6;
consider x1,x2,y1,y2 being Element of N such that
A25: a = <%x1,y1%> & b = <%x2,y2%> and
A26: add.(a,b) = <%x1+x2,y1+y2%> by A6;
a1 = x1 & a2 = x2 & b1 = y1 & b2 = y2 by A25,Th3;
hence (the addF of X).(<%a1,b1%>,<%a2,b2%>) = <%a1+a2,b1+b2%> by A26;
consider x1,x2,y1,y2 being Element of N such that
A27: a = <%x1,y1%> & b = <%x2,y2%> and
A28: mult.(a,b) = <%x1*x2-y2*'*y1,y2*x1+y1*x2*'%> by A12;
a1 = x1 & a2 = x2 & b1 = y1 & b2 = y2 by A27,Th3;
hence (the multF of X).(<%a1,b1%>,<%a2,b2%>) =
<%a1*a2-b2*'*b1,b2*a1+b1*a2*'%> by A28;
end;
hereby
let r be Real, a,b being Element of N;
reconsider c = <%a,b%> as Element of C by Th6;
r in REAL by XREAL_0:def 1;
then consider x,y being Element of N such that
A29: c = <%x,y%> and
A30: MU.(r,c) = <%r*x,r*y%> by A16;
a = x & b = y by A29,Th3;
hence (the Mult of X).(r,<%a,b%>) = <%r*a,r*b%> by A30;
end;
hereby
let a,b be Element of N;
reconsider c = <%a,b%> as Element of C by Th6;
consider x,y being Element of N such that
A31: c = <%x,y%> and
A32: norm.c = sqrt (||.x.||^2 + ||.y.||^2) by A20;
a = x & b = y by A31,Th3;
hence (the normF of X).<%a,b%> = sqrt (||.a.||^2 + ||.b.||^2) by A32;
consider x,y being Element of N such that
A33: c = <%x,y%> and
A34: conj.c = <%x*',-y%> by A24;
a = x & b = y by A33,Th3;
hence (the conjugateF of X).<%a,b%> = <%a*',-b%> by A34;
end;
end;
uniqueness
proof
let X,Y be strict ConjNormAlgStr such that
A35: the carrier of X = product <% the carrier of N,the carrier of N %> and
A36: the ZeroF of X = <% 0.N,0.N %> and
A37: the OneF of X = <% 1.N,0.N %> and
A38: for a1,a2,b1,b2 being Element of N holds
(the addF of X).(<%a1,b1%>,<%a2,b2%>) = <%a1+a2,b1+b2%> &
(the multF of X).(<%a1,b1%>,<%a2,b2%>) = <%a1*a2-b2*'*b1,b2*a1+b1*a2*'%>
and
A39: for r being Real, a,b being Element of N holds
(the Mult of X).(r,<%a,b%>) = <%r*a,r*b%>
and
A40: for a,b being Element of N holds
(the normF of X).<%a,b%> = sqrt (||.a.||^2 + ||.b.||^2) &
(the conjugateF of X).<%a,b%> = <%a*',-b%>
and
A41: the carrier of Y = product <% the carrier of N,the carrier of N %> and
A42: the ZeroF of Y = <% 0.N,0.N %> and
A43: the OneF of Y = <% 1.N,0.N %> and
A44: for a1,a2,b1,b2 being Element of N holds
(the addF of Y).(<%a1,b1%>,<%a2,b2%>) = <%a1+a2,b1+b2%> &
(the multF of Y).(<%a1,b1%>,<%a2,b2%>) = <%a1*a2-b2*'*b1,b2*a1+b1*a2*'%>
and
A45: for r being Real, a,b being Element of N holds
(the Mult of Y).(r,<%a,b%>) = <%r*a,r*b%>
and
A46: for a,b being Element of N holds
(the normF of Y).<%a,b%> = sqrt (||.a.||^2 + ||.b.||^2) &
(the conjugateF of Y).<%a,b%> = <%a*',-b%>;
A47: the addF of X = the addF of Y
proof
dom the addF of X = [:the carrier of X,the carrier of X:]
by A35,FUNCT_2:def 1;
hence dom the addF of X = dom the addF of Y by A35,A41,FUNCT_2:def 1;
let z be object;
assume z in dom the addF of X;
then consider z1,z2 being object such that
A48: z1 in the carrier of X and
A49: z2 in the carrier of X and
A50: z = [z1,z2] by ZFMISC_1:def 2;
consider a1,b1 being set such that
A51: a1 in the carrier of N & b1 in the carrier of N and
A52: z1 = <%a1,b1%> by A35,A48,Th7;
consider a2,b2 being set such that
A53: a2 in the carrier of N & b2 in the carrier of N and
A54: z2 = <%a2,b2%> by A35,A49,Th7;
reconsider a1,a2,b1,b2 as Element of N by A51,A53;
thus (the addF of X).z = (the addF of X).(z1,z2) by A50
.= <%a1+a2,b1+b2%> by A52,A54,A38
.= (the addF of Y).(z1,z2) by A52,A54,A44
.= (the addF of Y).z by A50;
end;
A55: the multF of X = the multF of Y
proof
dom the multF of X = [:the carrier of X,the carrier of X:]
by A35,FUNCT_2:def 1;
hence dom the multF of X = dom the multF of Y by A35,A41,FUNCT_2:def 1;
let z be object;
assume z in dom the multF of X;
then consider z1,z2 being object such that
A56: z1 in the carrier of X and
A57: z2 in the carrier of X and
A58: z = [z1,z2] by ZFMISC_1:def 2;
consider a1,b1 being set such that
A59: a1 in the carrier of N & b1 in the carrier of N and
A60: z1 = <%a1,b1%> by A35,A56,Th7;
consider a2,b2 being set such that
A61: a2 in the carrier of N & b2 in the carrier of N and
A62: z2 = <%a2,b2%> by A35,A57,Th7;
reconsider a1,a2,b1,b2 as Element of N by A59,A61;
thus (the multF of X).z = (the multF of X).(z1,z2) by A58
.= <%a1*a2-b2*'*b1,b2*a1+b1*a2*'%> by A60,A62,A38
.= (the multF of Y).(z1,z2) by A60,A62,A44
.= (the multF of Y).z by A58;
end;
A63: the Mult of X = the Mult of Y
proof
dom the Mult of X = [:REAL,the carrier of X:] by A35,FUNCT_2:def 1;
hence dom the Mult of X = dom the Mult of Y by A35,A41,FUNCT_2:def 1;
let z be object;
assume z in dom the Mult of X;
then consider z1,z2 being object such that
A64: z1 in REAL and
A65: z2 in the carrier of X and
A66: z = [z1,z2] by ZFMISC_1:def 2;
consider a,b being set such that
A67: a in the carrier of N & b in the carrier of N and
A68: z2 = <%a,b%> by A35,A65,Th7;
reconsider z1 as Element of REAL by A64;
reconsider a,b as Element of N by A67;
thus (the Mult of X).z = (the Mult of X).(z1,z2) by A66
.= <%z1*a,z1*b%> by A68,A39
.= (the Mult of Y).(z1,z2) by A68,A45
.= (the Mult of Y).z by A66;
end;
A69: the normF of X = the normF of Y
proof
dom the normF of X = the carrier of X by FUNCT_2:def 1;
hence dom the normF of X = dom the normF of Y by A35,A41,FUNCT_2:def 1;
let z be object;
assume z in dom the normF of X;
then consider a,b being set such that
A70: a in the carrier of N & b in the carrier of N and
A71: z = <%a,b%> by A35,Th7;
reconsider a,b as Element of N by A70;
thus (the normF of X).z = sqrt (||.a.||^2 + ||.b.||^2) by A71,A40
.= (the normF of Y).z by A71,A46;
end;
the conjugateF of X = the conjugateF of Y
proof
dom the conjugateF of X = the carrier of X by A35,FUNCT_2:def 1;
hence dom the conjugateF of X = dom the conjugateF of Y
by A35,A41,FUNCT_2:def 1;
let z be object;
assume z in dom the conjugateF of X;
then consider a,b being set such that
A72: a in the carrier of N & b in the carrier of N and
A73: z = <%a,b%> by A35,Th7;
reconsider a,b as Element of N by A72;
thus (the conjugateF of X).z = <%a*',-b%> by A73,A40
.= (the conjugateF of Y).z by A73,A46;
end;
hence thesis by A35,A36,A37,A41,A42,A43,A47,A55,A63,A69;
end;
end;
reserve c,c1,c2 for Element of Cayley-Dickson(N);
registration
let N be non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> non empty;
coherence
proof
product <%the carrier of N,the carrier of N%> is non empty;
hence the carrier of Cayley-Dickson(N) is non empty by Def9;
end;
end;
theorem Th12:
ex a,b being Element of N st c = <%a,b%>
proof
set C = Cayley-Dickson(N);
the carrier of C = product <% the carrier of N,the carrier of N %> by Def9;
then ex a,b being set st a in the carrier of N & b in the carrier of N
& c = <%a,b%> by Th7;
hence thesis;
end;
theorem Th13:
for c being Element of Cayley-Dickson(Cayley-Dickson(N))
ex a1,b1,a2,b2 st c = <%<%a1,b1%>,<%a2,b2%>%>
proof
let c be Element of Cayley-Dickson(Cayley-Dickson(N));
consider a,b being Element of Cayley-Dickson(N) such that
A1: c = <%a,b%> by Th12;
consider a1,b1 being Element of N such that
A2: a = <%a1,b1%> by Th12;
consider a2,b2 being Element of N such that
A3: b = <%a2,b2%> by Th12;
take a1,b1,a2,b2;
thus c = <%<%a1,b1%>,<%a2,b2%>%> by A1,A2,A3;
end;
definition
let N,a,b;
redefine func <% a,b %> -> Element of Cayley-Dickson(N); :: redefines <% (AFINSQ_1, definition)
coherence
proof
<%a,b%> in product <%the carrier of N,the carrier of N%> by Th6;
hence thesis by Def9;
end;
end;
registration
let N;
let a,b be zero Element of N;
cluster <% a,b %> -> zero for Element of Cayley-Dickson(N);
coherence
proof
A1: a = 0.N & b = 0.N by STRUCT_0:def 12;
0.Cayley-Dickson(N) = <%0.N,0.N%> by Def9;
hence thesis by A1;
end;
end;
registration
let N be non degenerated non empty 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
proof
set C = Cayley-Dickson(N);
now
assume <%a,b%> is zero;
then
A1: <%a,b%> = 0.C;
0.C = <%0.N,0.N%> by Def9;
hence contradiction by A1,Th3;
end;
hence thesis;
end;
end;
registration
let N be reflexive non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> reflexive;
coherence
proof
set C = Cayley-Dickson(N);
0.C = <%0.N,0.N%> by Def9;
hence ||.0.C.|| = sqrt (||.0.N.||^2 + ||.0.N.||^2) by Def9
.= 0;
end;
end;
registration
let N be discerning non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> discerning;
coherence
proof
set C = Cayley-Dickson(N);
let a be Element of C such that
A1: ||.a.|| = 0;
consider a1,b1 being Element of N such that
A2: a = <%a1,b1%> by Th12;
||.a.|| = sqrt (||.a1.||^2 + ||.b1.||^2) by A2,Def9;
then ||.a1.|| = 0 & ||.b1.|| = 0 by A1,SQUARE_1:24;
then a1 = 0.N & b1 = 0.N by NORMSP_0:def 5;
hence a = 0.C by A2,Def9;
end;
end;
theorem Th14:
a is left_complementable & b is left_complementable implies
<%a,b%> is left_complementable
proof
given x being Element of N such that
A1: x+a = 0.N;
given y being Element of N such that
A2: y+b = 0.N;
take <%x,y%>;
thus <%x,y%>+<%a,b%> = <%x+a,y+b%> by Def9
.= 0.Cayley-Dickson(N) by A1,A2,Def9;
end;
theorem Th15:
<%a,b%> is left_complementable implies
a is left_complementable & b is left_complementable
proof
set C = Cayley-Dickson(N);
given x being Element of C such that
A1: x+<%a,b%> = 0.C;
consider x1,x2 being Element of N such that
A2: x = <%x1,x2%> by Th12;
A3: 0.C = <%0.N,0.N%> by Def9;
A4: <%x1,x2%>+<%a,b%> = <%x1+a,x2+b%> by Def9;
hereby
take x1;
thus x1+a = 0.N by A1,A2,A3,A4,Th3;
end;
take x2;
thus x2+b = 0.N by A1,A2,A3,A4,Th3;
end;
theorem Th16:
a is right_complementable & b is right_complementable implies
<%a,b%> is right_complementable
proof
given x being Element of N such that
A1: a+x = 0.N;
given y being Element of N such that
A2: b+y = 0.N;
take <%x,y%>;
thus <%a,b%>+<%x,y%> = <%a+x,b+y%> by Def9
.= 0.Cayley-Dickson(N) by A1,A2,Def9;
end;
theorem Th17:
<%a,b%> is right_complementable implies
a is right_complementable & b is right_complementable
proof
set C = Cayley-Dickson(N);
given x being Element of C such that
A1: <%a,b%>+x = 0.C;
consider x1,x2 being Element of N such that
A2: x = <%x1,x2%> by Th12;
A3: 0.C = <%0.N,0.N%> by Def9;
A4: <%a,b%>+<%x1,x2%> = <%a+x1,b+x2%> by Def9;
hereby
take x1;
thus a+x1 = 0.N by A1,A2,A3,A4,Th3;
end;
take x2;
thus b+x2 = 0.N by A1,A2,A3,A4,Th3;
end;
theorem
a is complementable & b is complementable implies <%a,b%> is complementable
by Th14,Th16;
theorem
<%a,b%> is complementable implies a is complementable & b is complementable
by Th15,Th17;
theorem Th20:
a is left_add-cancelable & b is left_add-cancelable implies
<%a,b%> is left_add-cancelable
proof
assume
A1: a is left_add-cancelable & b is left_add-cancelable;
let y,z be Element of Cayley-Dickson(N) such that
A2: <%a,b%>+y = <%a,b%>+z;
consider y1,y2 being Element of N such that
A3: y = <%y1,y2%> by Th12;
consider z1,z2 being Element of N such that
A4: z = <%z1,z2%> by Th12;
<%a,b%>+<%y1,y2%> = <%a+y1,b+y2%> & <%a,b%>+<%z1,z2%> = <%a+z1,b+z2%>
by Def9;
then a+y1 = a+z1 & b+y2 = b+z2 by A2,A3,A4,Th3;
then y1 = z1 & y2 = z2 by A1;
hence y = z by A3,A4;
end;
theorem Th21:
<%a,b%> is left_add-cancelable implies
a is left_add-cancelable & b is left_add-cancelable
proof
assume
A1: <%a,b%> is left_add-cancelable;
hereby
let y,z be Element of N such that
A2: a+y = a+z;
<%a,b%>+<%y,0.N%> = <%a+y,b+0.N%> by Def9
.= <%a,b%>+<%z,0.N%> by A2,Def9;
then <%y,0.N%> = <%z,0.N%> by A1;
hence y = z by Th3;
end;
let y,z be Element of N such that
A3: b+y = b+z;
<%a,b%>+<%0.N,y%> = <%a+0.N,b+y%> by Def9
.= <%a,b%>+<%0.N,z%> by A3,Def9;
then <%0.N,y%> = <%0.N,z%> by A1;
hence y = z by Th3;
end;
theorem Th22:
a is right_add-cancelable & b is right_add-cancelable implies
<%a,b%> is right_add-cancelable
proof
assume
A1: a is right_add-cancelable & b is right_add-cancelable;
let y,z be Element of Cayley-Dickson(N) such that
A2: y+<%a,b%> = z+<%a,b%>;
consider y1,y2 being Element of N such that
A3: y = <%y1,y2%> by Th12;
consider z1,z2 being Element of N such that
A4: z = <%z1,z2%> by Th12;
<%y1,y2%>+<%a,b%> = <%y1+a,y2+b%> & <%z1,z2%>+<%a,b%> = <%z1+a,z2+b%>
by Def9;
then y1+a = z1+a & y2+b = z2+b by A2,A3,A4,Th3;
then y1 = z1 & y2 = z2 by A1;
hence y = z by A3,A4;
end;
theorem Th23:
<%a,b%> is right_add-cancelable implies
a is right_add-cancelable & b is right_add-cancelable
proof
assume
A1: <%a,b%> is right_add-cancelable;
hereby
let y,z be Element of N such that
A2: y+a = z+a;
<%y,0.N%>+<%a,b%> = <%y+a,0.N+b%> by Def9
.= <%z,0.N%>+<%a,b%> by A2,Def9;
then <%y,0.N%> = <%z,0.N%> by A1;
hence y = z by Th3;
end;
let y,z be Element of N such that
A3: y+b = z+b;
<%0.N,y%>+<%a,b%> = <%0.N+a,y+b%> by Def9
.= <%0.N,z%>+<%a,b%> by A3,Def9;
then <%0.N,y%> = <%0.N,z%> by A1;
hence y = z by Th3;
end;
theorem
a is add-cancelable & b is add-cancelable implies <%a,b%> is add-cancelable
by Th20,Th22;
theorem
<%a,b%> is add-cancelable implies a is add-cancelable & b is add-cancelable
by Th21,Th23;
theorem
<% a,b %> is left_complementable right_add-cancelable implies
- <% a,b %> = <% -a,-b %>
proof
assume
A1: <%a,b%> is left_complementable right_add-cancelable;
then a is left_complementable & b is left_complementable &
a is right_add-cancelable & b is right_add-cancelable by Th15,Th23;
then
A2: -a+a = 0.N & -b+b = 0.N by ALGSTR_0:def 13;
<%-a,-b%> + <%a,b%> = <%-a+a,-b+b%> by Def9
.= 0.Cayley-Dickson(N) by A2,Def9;
hence thesis by A1,ALGSTR_0:def 13;
end;
registration
let N be add-associative non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> add-associative;
coherence
proof
set C = Cayley-Dickson(N);
set f = the addF of C;
let a,b,c be Element of C;
consider a1,b1 being Element of N such that
A1: a = <%a1,b1%> by Th12;
consider a2,b2 being Element of N such that
A2: b = <%a2,b2%> by Th12;
consider a3,b3 being Element of N such that
A3: c = <%a3,b3%> by Th12;
A4: a1+a2+a3 = a1+(a2+a3) & b1+b2+b3 = b1+(b2+b3) by RLVECT_1:def 3;
A5: f.(b,c) = <%a2+a3,b2+b3%> by A2,A3,Def9;
f.(a,b) = <%a1+a2,b1+b2%> by A1,A2,Def9;
hence (a+b)+c = <% a1+a2+a3,b1+b2+b3 %> by A3,Def9
.= a+(b+c) by A1,A4,A5,Def9;
end;
end;
registration
let N be right_zeroed non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> right_zeroed;
coherence
proof
set C = Cayley-Dickson(N);
let a be Element of C;
consider a1,b1 being Element of N such that
A1: a = <%a1,b1%> by Th12;
A2: 0.C = <%0.N,0.N%> by Def9;
a1+0.N = a1 & b1+0.N = b1 by RLVECT_1:def 4;
hence thesis by A1,A2,Def9;
end;
end;
registration
let N be left_zeroed non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> left_zeroed;
coherence
proof
set C = Cayley-Dickson(N);
let a be Element of C;
consider a1,b1 being Element of N such that
A1: a = <%a1,b1%> by Th12;
A2: 0.C = <%0.N,0.N%> by Def9;
0.N+a1 = a1 & 0.N+b1 = b1 by ALGSTR_1:def 2;
hence thesis by A1,A2,Def9;
end;
end;
registration
let N be right_complementable non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> right_complementable;
coherence
proof
set C = Cayley-Dickson(N);
let a be Element of C;
consider a1,b1 being Element of N such that
A1: a = <%a1,b1%> by Th12;
consider a2 being Element of N such that
A2: a1+a2 = 0.N by ALGSTR_0:def 11;
consider b2 being Element of N such that
A3: b1+b2 = 0.N by ALGSTR_0:def 11;
take <%a2,b2%>;
0.C = <%0.N,0.N%> by Def9;
hence thesis by A1,A2,A3,Def9;
end;
end;
registration
let N be left_complementable non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> left_complementable;
coherence
proof
set C = Cayley-Dickson(N);
let a be Element of C;
consider a1,b1 being Element of N such that
A1: a = <%a1,b1%> by Th12;
consider a2 being Element of N such that
A2: a2+a1 = 0.N by ALGSTR_0:def 10;
consider b2 being Element of N such that
A3: b2+b1 = 0.N by ALGSTR_0:def 10;
take <%a2,b2%>;
0.C = <%0.N,0.N%> by Def9;
hence thesis by A1,A2,A3,Def9;
end;
end;
registration
let N be Abelian non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> Abelian;
coherence
proof
set C = Cayley-Dickson(N);
let a,b be Element of C;
consider a1,b1 being Element of N such that
A1: a = <%a1,b1%> by Th12;
consider a2,b2 being Element of N such that
A2: b = <%a2,b2%> by Th12;
(the addF of C).(a,b) = <%a1+a2,b1+b2%> by A1,A2,Def9;
hence thesis by A1,A2,Def9;
end;
end;
theorem Th27:
N is add-associative right_zeroed right_complementable implies
- <% a,b %> = <% -a,-b %>
proof
assume
A1: N is add-associative right_zeroed right_complementable;
then
A2: a+-a = 0.N & b+-b = 0.N by RLVECT_1:def 10;
<%a,b%> + <%-a,-b%> = <%a+-a,b+-b%> by Def9
.= 0.Cayley-Dickson(N) by A2,Def9;
hence thesis by A1,RLVECT_1:def 10;
end;
theorem Th28:
N is add-associative right_zeroed right_complementable implies
<% a1,b1 %> - <% a2,b2 %> = <% a1-a2,b1-b2 %>
proof
assume N is add-associative right_zeroed right_complementable;
hence <%a1,b1%> - <%a2,b2%> = <%a1,b1%>+<%-a2,-b2%> by Th27
.= <%a1-a2,b1-b2%> by Def9;
end;
registration
let N be well-unital add-associative right_zeroed right_complementable
distributive Banach_Algebra-like_2 well-conjugated scalar-unital
almost_right_cancelable non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> well-unital;
coherence
proof
set C = Cayley-Dickson(N);
let a be Element of C;
consider a1,b1 being Element of N such that
A1: a = <%a1,b1%> by Th12;
A3: 1.C = <%1.N,0.N%> by Def9;
then
A4: a*1.C = <%a1*1.N-0.N*'*b1,0.N*a1+b1*(1.N)*'%> by A1,Def9;
1.C*a = <%1.N*a1-b1*'*0.N,b1*1.N+0.N*a1*'%> by A1,A3,Def9;
hence thesis by A1,A4;
end;
end;
registration
let N be non degenerated non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> non degenerated;
coherence
proof
set C = Cayley-Dickson(N);
0.C = <%0.N,0.N%> & 1.C = <%1.N,0.N%> by Def9;
hence 0.C <> 1.C;
end;
end;
registration
let N be add-conjugative add-associative right_zeroed right_complementable
Abelian non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> add-conjugative;
coherence
proof
let a,b be Element of Cayley-Dickson(N);
consider a1,a2 being Element of N such that
A1: a = <%a1,a2%> by Th12;
consider b1,b2 being Element of N such that
A2: b = <%b1,b2%> by Th12;
A3: (a1+b1)*' = a1*'+b1*' by Def5;
A4: a*' = <%a1*',-a2%> & b*' = <%b1*',-b2%> by A1,A2,Def9;
A5: -(a2+b2) = -a2-b2 by RLVECT_1:30;
a+b = <%a1+b1,a2+b2%> by A1,A2,Def9;
hence (a+b)*' = <%(a1+b1)*',-(a2+b2)%> by Def9
.= a*'+b*' by A3,A4,A5,Def9;
end;
end;
registration
let N be norm-conjugative reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable
non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> norm-conjugative;
coherence
proof
let a be Element of Cayley-Dickson(N);
consider a1,a2 being Element of N such that
A1: a = <%a1,a2%> by Th12;
A2: ||.a1*'.|| = ||.a1.|| by Def6;
A3: ||.-a2.|| = ||.a2.|| by NORMSP_1:2;
a*' = <%a1*',-a2%> by A1,Def9;
hence ||.a*'.|| = sqrt(||.a1*'.||^2+||.-a2.||^2) by Def9
.= ||.a.|| by A1,A2,A3,Def9;
end;
end;
registration
let N be scalar-conjugative
add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> scalar-conjugative;
coherence
proof
let r;
let a be Element of Cayley-Dickson(N);
consider a1,a2 being Element of N such that
A1: a = <%a1,a2%> by Th12;
A2: r*-a2 = -r*a2 by RLVECT_1:25;
r*a = <%r*a1,r*a2%> by A1,Def9;
then
A3: (r*a)*' = <%(r*a1)*',-(r*a2)%> by Def9;
A4: r*a1*' = (r*a1)*' by Def7;
a*' = <%a1*',-a2%> by A1,Def9;
hence (r*a)*' = r*a*' by A2,A3,A4,Def9;
end;
end;
registration
let N be distributive add-associative right_zeroed right_complementable
Abelian non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> left-distributive;
coherence
proof
let a,b,c be Element of Cayley-Dickson(N);
consider a1,a2 being Element of N such that
A1: a = <%a1,a2%> by Th12;
consider b1,b2 being Element of N such that
A2: b = <%b1,b2%> by Th12;
consider c1,c2 being Element of N such that
A3: c = <%c1,c2%> by Th12;
A4: b+c = <%b1+c1,b2+c2%> by A2,A3,Def9;
A5: b*a = <%b1*a1-a2*'*b2,a2*b1+b2*a1*'%> by A1,A2,Def9;
A6: c*a = <%c1*a1-a2*'*c2,a2*c1+c2*a1*'%> by A1,A3,Def9;
A7: (b1+c1)*a1 = b1*a1+c1*a1 by VECTSP_1:def 3;
A8: a2*(b1+c1) = a2*b1+a2*c1 by VECTSP_1:def 2;
a2*'*(b2+c2) = a2*'*b2+a2*'*c2 by VECTSP_1:def 2;
then
A9: (b1+c1)*a1-a2*'*(b2+c2) = b1*a1+c1*a1-a2*'*b2-a2*'*c2 by A7,RLVECT_1:27
.= b1*a1-a2*'*b2+c1*a1-a2*'*c2 by RLVECT_1:28
.= b1*a1-a2*'*b2+(c1*a1-a2*'*c2) by RLVECT_1:28;
(b2+c2)*a1*' = b2*a1*'+c2*a1*' by VECTSP_1:def 3;
then
A10: a2*(b1+c1)+(b2+c2)*a1*' = a2*b1+a2*c1+b2*a1*'+c2*a1*' by A8,RLVECT_1:def 3
.= a2*b1+b2*a1*'+a2*c1+c2*a1*' by RLVECT_1:def 3
.= a2*b1+b2*a1*'+(a2*c1+c2*a1*') by RLVECT_1:def 3;
thus (b+c)*a = <%(b1+c1)*a1-a2*'*(b2+c2),a2*(b1+c1)+(b2+c2)*a1*'%>
by A1,A4,Def9
.= b*a+c*a by A5,A6,A9,A10,Def9;
end;
end;
registration
let N be distributive add-associative right_zeroed right_complementable
add-conjugative Abelian non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> right-distributive;
coherence
proof
let a,b,c be Element of Cayley-Dickson(N);
consider a1,a2 being Element of N such that
A1: a = <%a1,a2%> by Th12;
consider b1,b2 being Element of N such that
A2: b = <%b1,b2%> by Th12;
consider c1,c2 being Element of N such that
A3: c = <%c1,c2%> by Th12;
A4: a1*(b1+c1) = a1*b1+a1*c1 by VECTSP_1:def 2;
A5: (b2+c2)*a1 = b2*a1+c2*a1 by VECTSP_1:def 3;
(b2+c2)*' = b2*'+c2*' by Def5;
then (b2+c2)*'*a2 = b2*'*a2+c2*'*a2 by VECTSP_1:def 3;
then
A6: a1*(b1+c1)-(b2+c2)*'*a2 = a1*b1+a1*c1-b2*'*a2-c2*'*a2 by A4,RLVECT_1:27
.= a1*b1-b2*'*a2+a1*c1-c2*'*a2 by RLVECT_1:def 3
.= a1*b1-b2*'*a2+(a1*c1-c2*'*a2) by RLVECT_1:def 3;
(b1+c1)*' = b1*'+c1*' by Def5;
then a2*(b1+c1)*' = a2*b1*'+a2*c1*' by VECTSP_1:def 2;
then
A7: (b2+c2)*a1+a2*(b1+c1)*' = b2*a1+c2*a1+a2*b1*'+a2*c1*' by A5,RLVECT_1:def 3
.= b2*a1+a2*b1*'+c2*a1+a2*c1*' by RLVECT_1:def 3
.= b2*a1+a2*b1*'+(c2*a1+a2*c1*') by RLVECT_1:def 3;
A8: a*b = <%a1*b1-b2*'*a2,b2*a1+a2*b1*'%> by A1,A2,Def9;
A9: a*c = <%a1*c1-c2*'*a2,c2*a1+a2*c1*'%> by A1,A3,Def9;
b+c = <%b1+c1,b2+c2%> by A2,A3,Def9;
hence a*(b+c) = <%a1*(b1+c1)-(b2+c2)*'*a2,(b2+c2)*a1+a2*(b1+c1)*'%>
by A1,Def9
.= a*b+a*c by A6,A7,A8,A9,Def9;
end;
end;
registration
let N be reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable
non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> RealNormSpace-like;
coherence
proof
let c1,c2 be Element of Cayley-Dickson(N);
let r;
consider a1,b1 being Element of N such that
A1: c1 = <%a1,b1%> by Th12;
A2: r*c1 = <%r*a1,r*b1%> by A1,Def9;
A3: ||.r*a1.|| = |.r.|*||.a1.|| & ||.r*b1.|| = |.r.|*||.b1.||
by NORMSP_1:def 1;
thus ||.r*c1.|| = sqrt(||.r*a1.||^2+||.r*b1.||^2) by A2,Def9
.= sqrt(|.r.|^2*(||.a1.||^2+||.b1.||^2)) by A3
.= |.r.| * sqrt(||.a1.||^2+||.b1.||^2) by SQUARE_1:54
.= |.r.| * ||.c1.|| by A1,Def9;
consider a2,b2 being Element of N such that
A4: c2 = <%a2,b2%> by Th12;
set A1 = ||.a1.||, A2 = ||.a2.||, B1 = ||.b1.||, B2 = ||.b2.||,
C1 = ||.c1.||, C2 = ||.c2.||;
||.a1+a2.|| <= A1+A2 & ||.b1+b2.|| <= B1+B2 by NORMSP_1:def 1;
then ||.a1+a2.||^2 <= (A1+A2)^2 & ||.b1+b2.||^2 <= (B1+B2)^2 by XREAL_1:66;
then
A5: ||.a1+a2.||^2+||.b1+b2.||^2 <= (A1+A2)^2+(B1+B2)^2 by XREAL_1:7;
c1+c2 = <%a1+a2,b1+b2%> by A1,A4,Def9;
then
A6: ||.c1+c2.|| = sqrt(||.a1+a2.||^2+||.b1+b2.||^2) by Def9;
A7: C1 = sqrt(A1^2+B1^2) & C2 = sqrt(A2^2+B2^2) by A1,A4,Def9;
then 0 <= C1 & 0 <= C2 by SQUARE_1:def 2;
then
A8: C1+C2 = sqrt(C1+C2)^2 by SQUARE_1:def 2;
(A1+A2)^2+(B1+B2)^2 <= (C1+C2)^2 by A7,Th1;
then ||.a1+a2.||^2+||.b1+b2.||^2 <= (C1+C2)^2 by A5,XXREAL_0:2;
hence thesis by A6,A8,SQUARE_1:26;
end;
end;
registration
let N be vector-distributive non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> vector-distributive;
coherence
proof
let r;
let c1,c2 be Element of Cayley-Dickson(N);
consider a1,b1 being Element of N such that
A1: c1 = <%a1,b1%> by Th12;
consider a2,b2 being Element of N such that
A2: c2 = <%a2,b2%> by Th12;
A3: r*(a1+a2) = r*a1+r*a2 & r*(b1+b2) = r*b1+r*b2 by RLVECT_1:def 5;
A4: r*<%a1,b1%> = <%r*a1,r*b1%> & r*<%a2,b2%> = <%r*a2,r*b2%> by Def9;
c1+c2 = <%a1+a2,b1+b2%> by A1,A2,Def9;
hence r*(c1+c2) = <%r*(a1+a2),r*(b1+b2)%> by Def9
.= r*c1 + r*c2 by A1,A2,A3,A4,Def9;
end;
end;
registration
let N be vector-associative Banach_Algebra-like_3
add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> vector-associative;
coherence
proof
let c1,c2 be Element of Cayley-Dickson(N);
let r;
consider a1,b1 being Element of N such that
A1: c1 = <%a1,b1%> by Th12;
consider a2,b2 being Element of N such that
A2: c2 = <%a2,b2%> by Th12;
A3: c1*c2 = <%a1*a2-b2*'*b1,b2*a1+b1*a2*'%> by A1,A2,Def9;
A4: r*(a1*a2) = r*a1*a2 by FUNCSDOM:def 9;
r*(b2*'*b1) = b2*'*(r*b1) by LOPBAN_2:def 11;
then
A5: r*(a1*a2-b2*'*b1) = r*a1*a2-b2*'*(r*b1) by A4,RLVECT_1:34;
A6: r*(b2*a1) = b2*(r*a1) by LOPBAN_2:def 11;
r*(b1*a2*') = r*b1*a2*' by FUNCSDOM:def 9;
then
A7: r*(b2*a1+b1*a2*') = b2*(r*a1)+r*b1*a2*' by A6,RLVECT_1:def 5;
r*c1 = <%r*a1,r*b1%> by A1,Def9;
hence r*c1*c2 = <%r*a1*a2-b2*'*(r*b1),b2*(r*a1)+r*b1*a2*'%> by A2,Def9
.= r*(c1*c2) by A3,A5,A7,Def9;
end;
end;
registration
let N be scalar-distributive non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> scalar-distributive;
coherence
proof
let r,s;
let c be Element of Cayley-Dickson(N);
consider a,b being Element of N such that
A1: c = <%a,b%> by Th12;
A2: (r+s)*a = r*a+s*a & (r+s)*b = r*b+s*b by RLVECT_1:def 6;
A3: r*<%a,b%> = <%r*a,r*b%> & s*<%a,b%> = <%s*a,s*b%> by Def9;
thus (r+s)*c = <%(r+s)*a,(r+s)*b%> by A1,Def9
.= r*c + s*c by A1,A2,A3,Def9;
end;
end;
registration
let N be scalar-associative non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> scalar-associative;
coherence
proof
let r,s;
let c be Element of Cayley-Dickson(N);
consider a,b being Element of N such that
A1: c = <%a,b%> by Th12;
A2: r*s*a = r*(s*a) & r*s*b = r*(s*b) by RLVECT_1:def 7;
thus r*s*c = <%r*s*a,r*s*b%> by A1,Def9
.= r*<%s*a,s*b%> by A2,Def9
.= r*(s*c) by A1,Def9;
end;
end;
registration
let N be scalar-unital non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> scalar-unital;
coherence
proof
let c be Element of Cayley-Dickson(N);
consider a,b being Element of N such that
A1: c = <%a,b%> by Th12;
1*a = a & 1*b = b by RLVECT_1:def 8;
hence thesis by A1,Def9;
end;
end;
registration
let N be reflexive Banach_Algebra-like_2 non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> Banach_Algebra-like_2;
coherence
proof
set C = Cayley-Dickson(N);
A1: ||.1.N.|| = 1 by LOPBAN_2:def 10;
1.C = <%1.N,0.N%> by Def9;
hence ||.1.C.|| = sqrt(||.1.N.||^2+||.0.N.||^2) by Def9
.= 1 by A1;
end;
end;
registration
let N be Banach_Algebra-like_3
add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
vector-associative scalar-conjugative non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> Banach_Algebra-like_3;
coherence
proof
set C = Cayley-Dickson(N);
let r;
let a,b be Element of C;
consider a1,b1 being Element of N such that
A1: a = <%a1,b1%> by Th12;
consider a2,b2 being Element of N such that
A2: b = <%a2,b2%> by Th12;
A3: r*b = <%r*a2,r*b2%> by A2,Def9;
A4: a*b = <%a1*a2-b2*'*b1,b2*a1+b1*a2*'%> by A1,A2,Def9;
A5: a*(r*b) = <%a1*(r*a2)-(r*b2)*'*b1,(r*b2)*a1+b1*(r*a2)*'%> by A1,A3,Def9;
r*b2*' = (r*b2)*' by Def7;
then
A6: r*(b2*'*b1) = (r*b2)*'*b1 by FUNCSDOM:def 9;
A7: r*(a1*a2-b2*'*b1) = r*(a1*a2)-r*(b2*'*b1) by RLVECT_1:34
.= a1*(r*a2)-(r*b2)*'*b1 by A6,LOPBAN_2:def 11;
A8: r*b2*a1 = r*(b2*a1) by FUNCSDOM:def 9;
r*a2*' = (r*a2)*' by Def7;
then b1*(r*a2)*' = r*(b1*a2*') by LOPBAN_2:def 11;
then r*b2*a1+b1*(r*a2)*' = r*(b2*a1+b1*a2*') by A8,RLVECT_1:def 5;
hence thesis by A4,A5,A7,Def9;
end;
end;
theorem
for N being almost_left_invertible associative add-associative
right_zeroed right_complementable well-unital distributive Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
vector-associative reflexive discerning RealNormSpace-like
almost_right_cancelable
well-conjugated add-conjugative Banach_Algebra-like_2
Banach_Algebra-like_3 non degenerated ConjNormAlgStr
for a,b being Element of N st (a is non zero or b is non zero) &
<%a,b%> is right_mult-cancelable left_invertible holds
/<%a,b%> = <%1/(||.a.||^2+||.b.||^2) * a*' , 1/(||.a.||^2+||.b.||^2) * -b%>
proof
let N be almost_left_invertible associative add-associative
right_zeroed right_complementable well-unital distributive Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
vector-associative reflexive discerning RealNormSpace-like
almost_right_cancelable
well-conjugated add-conjugative Banach_Algebra-like_2
Banach_Algebra-like_3 non degenerated ConjNormAlgStr;
let a,b be Element of N such that
A1: a is non zero or b is non zero and
A2: <%a,b%> is right_mult-cancelable left_invertible;
set C = Cayley-Dickson(N);
set m = 1/(||.a.||^2+||.b.||^2);
A3: b*'*-b = -b*'*b by VECTSP_1:8;
A4: a*'*a = ||.a.||^2 * 1.N by Th9;
A5: b*'*b = ||.b.||^2 * 1.N by Th9;
b*'*(m*-b) = m*(b*'*-b) by LOPBAN_2:def 11;
then
A6: m*a*'*a-b*'*(m*-b) = m*a*'*a--m*(b*'*b) by A3,RLVECT_1:25
.= m*a*'*a+m*(b*'*b)
.= m*(a*'*a)+m*(b*'*b) by FUNCSDOM:def 9
.= m*(a*'*a+b*'*b) by RLVECT_1:def 5
.= m*((||.a.||^2+||.b.||^2) * 1.N) by A4,A5,RLVECT_1:def 6
.= m*(||.a.||^2+||.b.||^2) * 1.N by RLVECT_1:def 7
.= 1 * 1.N by A1,XCMPLX_1:106
.= 1.N by RLVECT_1:def 8;
(m*-b)*a*' = m*((-b)*a*') by FUNCSDOM:def 9
.= (-b)*(m*a*') by LOPBAN_2:def 11
.= -b*(m*a*') by VECTSP_1:9;
then
A7: b*(m*a*')+(m*-b)*a*' = 0.N by RLVECT_1:def 10;
<%m*a*',m*-b%> * <%a,b%> = <%m*a*'*a-b*'*(m*-b),b*(m*a*')+(m*-b)*a*'%>
by Def9
.= 1.C by A6,A7,Def9;
hence thesis by A2,ALGSTR_0:def 30;
end;
registration
let N be add-associative right_zeroed right_complementable distributive
scalar-distributive scalar-unital vector-distributive
discerning reflexive well-conjugated non empty ConjNormAlgStr;
cluster Cayley-Dickson(N) -> well-conjugated;
coherence
proof
set C = Cayley-Dickson(N);
let c be Element of C;
consider a,b being Element of N such that
A1: c = <%a,b%> by Th12;
A2: 0.C = <%0.N,0.N%> by Def9;
A3: c*' = <%a*',-b%> by A1,Def9;
A4: ||.c.|| = sqrt(||.a.||^2+||.b.||^2) by A1,Def9;
per cases;
case c is non zero;
A5: 1.C = <%1.N,0.N%> by Def9;
A6: a*'*a = ||.a.||^2 * 1.N & b*'*b = ||.b.||^2 * 1.N by Th9;
A7: a*'*a-b*'*-b = a*'*a--b*'*b by VECTSP_1:8
.= a*'*a+b*'*b
.= (||.a.||^2+||.b.||^2) * 1.N by A6,RLVECT_1:def 6
.= ||.c.||^2*1.N by A4,SQUARE_1:def 2;
b+-b = 0.N by RLVECT_1:def 10;
then b*a*'+(-b)*a*' = 0.N*a*' by VECTSP_1:def 3
.= ||.c.||^2*0.N;
then c*' * c = <%||.c.||^2*1.N,||.c.||^2*0.N%> by A1,A3,A7,Def9
.= ||.c.||^2 * 1.C by A5,Def9;
hence thesis;
end;
case c is zero;
then c = 0.C;
then
A8: a = 0.N & b = 0.N by A1,A2,Th3;
||.c*'.|| = 0 by A3,A8;
hence c*' = 0.C by NORMSP_0:def 5;
end;
end;
end;
registration
cluster Cayley-Dickson(N_Real) -> associative commutative;
coherence
proof
thus Cayley-Dickson(N_Real) is associative
proof
let x,y,z be Element of Cayley-Dickson(N_Real);
consider x1,x2 being Element of N_Real such that
A1: x = <%x1,x2%> by Th12;
consider y1,y2 being Element of N_Real such that
A2: y = <%y1,y2%> by Th12;
consider z1,z2 being Element of N_Real such that
A3: z = <%z1,z2%> by Th12;
set a1 = x1*y1-y2*'*x2, b1 = x1*y2+y1*'*x2,
a2 = y1*z1-z2*'*y2, b2 = y1*z2+z1*'*y2;
A4: y*z = <%y1*z1-z2*'*y2,y1*z2+z1*'*y2%> by A2,A3,Def9;
x*y = <%x1*y1-y2*'*x2,x1*y2+y1*'*x2%> by A1,A2,Def9;
hence x*y*z = <%a1*z1-z2*'*b1,a1*z2+z1*'*b1%> by A3,Def9
.= <%x1*a2-b2*'*x2,x1*b2+a2*'*x2%>
.= x*(y*z) by A1,A4,Def9;
end;
let x,y be Element of Cayley-Dickson(N_Real);
consider x1,x2 being Element of N_Real such that
A5: x = <%x1,x2%> by Th12;
consider y1,y2 being Element of N_Real such that
A6: y = <%y1,y2%> by Th12;
thus x*y = <%x1*y1-y2*'*x2,x1*y2+y1*'*x2%> by A5,A6,Def9
.= <%y1*x1-x2*'*y2,y1*x2+x1*'*y2%>
.= y*x by A5,A6,Def9;
end;
end;
set z = 0.N_Real, j = 1.N_Real;
set ZJ = <%z,j%>, ZZ = <%z,z%>, JZ = <%j,z%>, ZM = <%z,-j%>, MZ = <%-j,z%>;
Lm2: ZJ*JZ = <%z*j-z*'*j,z*z+j*'*j%> by Def9
.= <%z,j*'*j%>;
::i*j = k in quaternions
theorem Th30:
<% <%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
thus <%ZZ,ZJ%> = <%ZJ*ZZ-JZ*'*ZZ,ZJ*JZ+ZZ*'*ZZ%> by Lm2
.= <%ZJ,ZZ%> * <%ZZ,JZ%> by Def9;
end;
::j*i = -k in quaternions
theorem Th31:
<% <%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
ZJ*' = <%z*',-j%> by Def9;
then ZJ*'*JZ = <%z*j-z*'*-j,z*z+j*'*-j%> by Def9;
hence <%ZZ,ZM%> = <%ZZ*ZJ-ZZ*'*JZ,ZZ*ZZ+ZJ*'*JZ%>
.= <%ZZ,JZ%> * <%ZJ,ZZ%> by Def9;
end;
registration
cluster Cayley-Dickson(Cayley-Dickson(N_Real)) ->
associative non commutative;
coherence
proof
thus Cayley-Dickson(Cayley-Dickson(N_Real)) is associative
proof
let a,b,c be Element of Cayley-Dickson(Cayley-Dickson(N_Real));
consider a1,b1,a2,b2 being Element of N_Real such that
A1: a = <%<%a1,b1%>,<%a2,b2%>%> by Th13;
consider a3,b3,a4,b4 being Element of N_Real such that
A2: b = <%<%a3,b3%>,<%a4,b4%>%> by Th13;
consider a5,b5,a6,b6 being Element of N_Real such that
A3: c = <%<%a5,b5%>,<%a6,b6%>%> by Th13;
set x1 = <%a1,b1%>*<%a3,b3%>-<%a4,b4%>*'*<%a2,b2%>;
set x2 = <%a1,b1%>*<%a4,b4%>+<%a3,b3%>*'*<%a2,b2%>;
set x3 = <%a3,b3%>*<%a5,b5%>-<%a6,b6%>*'*<%a4,b4%>;
set x4 = <%a3,b3%>*<%a6,b6%>+<%a5,b5%>*'*<%a4,b4%>;
set x11 = a1*a3-b3*'*b1-(a4*'*a2-b2*'*-b4);
set x12 = a1*b3+a3*'*b1-(a4*'*b2+a2*'*-b4);
set x21 = a1*a4-b4*'*b1+(a3*'*a2-b2*'*-b3);
set x22 = a1*b4+a4*'*b1+(a3*'*b2+a2*'*-b3);
set x31 = a3*a5-b5*'*b3-(a6*'*a4-b4*'*-b6);
set x32 = a3*b5+a5*'*b3-(a6*'*b4+a4*'*-b6);
set x41 = a3*a6-b6*'*b3+(a5*'*a4-b4*'*-b5);
set x42 = a3*b6+a6*'*b3+(a5*'*b4+a4*'*-b5);
A4: <%a1,b1%>*<%a3,b3%> = <%a1*a3-b3*'*b1,a1*b3+a3*'*b1%> by Def9;
A5: <%a4,b4%>*' = <%a4*',-b4%> by Def9;
A6: <%a4*',-b4%>*<%a2,b2%> = <%a4*'*a2-b2*'*-b4,a4*'*b2+a2*'*-b4%> by Def9;
A7: x1 = <%x11,x12%> by A4,A5,A6,Th28;
A8: <%a1,b1%>*<%a4,b4%> = <%a1*a4-b4*'*b1,a1*b4+a4*'*b1%> by Def9;
A9: <%a3,b3%>*' = <%a3*',-b3%> by Def9;
A10: <%a3*',-b3%>*<%a2,b2%> = <%a3*'*a2-b2*'*-b3,a3*'*b2+a2*'*-b3%> by Def9;
A11: x2 = <%x21,x22%> by A8,A9,A10,Def9;
A12: <%a3,b3%>*<%a5,b5%> = <%a3*a5-b5*'*b3,a3*b5+a5*'*b3%> by Def9;
A13: <%a6,b6%>*' = <%a6*',-b6%> by Def9;
A14: <%a6*',-b6%>*<%a4,b4%> = <%a6*'*a4-b4*'*-b6,a6*'*b4+a4*'*-b6%> by Def9;
A15: x3 = <%x31,x32%> by A12,A13,A14,Th28;
A16: <%a3,b3%>*<%a6,b6%> = <%a3*a6-b6*'*b3,a3*b6+a6*'*b3%> by Def9;
A17: <%a5,b5%>*' = <%a5*',-b5%> by Def9;
A18: <%a5*',-b5%>*<%a4,b4%> = <%a5*'*a4-b4*'*-b5,a5*'*b4+a4*'*-b5%> by Def9;
A19: x4 = <%x41,x42%> by A16,A17,A18,Def9;
A20: <%a1,b1%>*x3 = <%a1*x31-x32*'*b1,a1*x32+x31*'*b1%> by A15,Def9;
x4*' = <%x41*',-x42%> by A19,Def9;
then
A21: x4*'*<%a2,b2%> = <%x41*'*a2-b2*'*-x42,x41*'*b2+a2*'*-x42%> by Def9;
A22: x1*<%a5,b5%> = <%x11*a5-b5*'*x12,x11*b5+a5*'*x12%> by A7,Def9;
<%a6,b6%>*'*x2 = <%a6*'*x21-x22*'*-b6,a6*'*x22+x21*'*-b6%> by A11,A13,
Def9;
then
A23: x1*<%a5,b5%>-<%a6,b6%>*'*x2 =
<%x11*a5-b5*'*x12-(a6*'*x21-x22*'*-b6),
x11*b5+a5*'*x12-(a6*'*x22+x21*'*-b6)%> by A22,Th28
.= <%a1*x31-x32*'*b1-(x41*'*a2-b2*'*-x42),
a1*x32+x31*'*b1-(x41*'*b2+a2*'*-x42)%>
.= <%a1,b1%>*x3-x4*'*<%a2,b2%> by A20,A21,Th28;
A24: <%a1,b1%>*x4 = <%a1*x41-x42*'*b1,a1*x42+x41*'*b1%> by A19,Def9;
x3*' = <%x31*',-x32%> by A15,Def9;
then
A25: x3*'*<%a2,b2%> = <%x31*'*a2-b2*'*-x32,x31*'*b2+a2*'*-x32%> by Def9;
A26: x1*<%a6,b6%> = <%x11*a6-b6*'*x12,x11*b6+a6*'*x12%> by A7,Def9;
<%a5,b5%>*'*x2 = <%a5*'*x21-x22*'*-b5,a5*'*x22+x21*'*-b5%> by A17,A11,
Def9;
then
A27: x1*<%a6,b6%>+<%a5,b5%>*'*x2 =
<%x11*a6-b6*'*x12+(a5*'*x21-x22*'*-b5),
x11*b6+a6*'*x12+(a5*'*x22+x21*'*-b5)%> by A26,Def9
.= <%a1*x41-x42*'*b1+(x31*'*a2-b2*'*-x32),
a1*x42+x41*'*b1+(x31*'*b2+a2*'*-x32)%>
.= <%a1,b1%>*x4+x3*'*<%a2,b2%> by A24,A25,Def9;
A28: b*c = <%x3,x4%> by A2,A3,Def9;
a*b = <%x1,x2%> by A1,A2,Def9;
hence a*b*c = <%x1*<%a5,b5%>-<%a6,b6%>*'*x2,x1*<%a6,b6%>+<%a5,b5%>*'*x2%>
by A3,Def9
.= a*(b*c) by A1,A28,A23,A27,Def9;
end;
take <%ZJ,ZZ%>, <%ZZ,JZ%>;
ZJ <> ZM by Th3;
hence thesis by Th30,Th31,Th3;
end;
end;
set ZZZZ = <%ZZ,ZZ%>, JZZZ = <%JZ,ZZ%>, ZJZZ = <%ZJ,ZZ%>, ZZJZ = <%ZZ,JZ%>,
ZZZJ = <%ZZ,ZJ%>;
Lm3: ZJ*' = <%z*',-j%> by Def9;
::e1*e2 = e3 in octonions
theorem Th32:
<%<%<%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
A1: ZJZZ*ZZJZ-ZZZZ*'*ZZZZ = <%ZJ*ZZ-JZ*'*ZZ,ZJ*JZ+ZZ*'*ZZ%> by Def9
.= <%ZZ,ZJ*JZ%>
.= ZZZJ by Lm2;
ZZZZ*ZJZZ+ZZZZ*ZZJZ*' = ZZZZ;
hence thesis by A1,Def9;
end;
::e2*e1 = -e3 in octonions
theorem Th33:
<%<%<%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
A1: JZ*ZJ*' = <%j*z*'-(-j)*'*z,(-j)*j+z*z*'*'%> by Lm3,Def9
.= <%z,-j%>;
A2: ZZJZ*ZJZZ-ZZZZ*'*ZZZZ = <%ZZ*ZJ-ZZ*'*JZ,ZZ*ZZ+JZ*ZJ*'%> by Def9
.= <%ZZ,ZM%> by A1;
ZZZZ*ZZJZ+ZZZZ*ZJZZ*' = ZZZZ;
hence <%ZZJZ,ZZZZ%> * <%ZJZZ,ZZZZ%> = <%<%ZZ,ZM%>,ZZZZ%> by A2,Def9;
end;
::(e1*e2)*e5 = -e6 in octonions
theorem Th34:
<%<%<%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
set a1 = ZJZZ*ZZJZ-ZZZZ*'*ZZZZ, b1 = ZZZZ*ZJZZ+ZZZZ*ZZJZ*';
A1: ZJ*ZJ = <%z*z-j*'*j,z*j+z*'*j%> by Def9
.= <%-j,z%>;
a1 = <%ZJ*ZZ-JZ*'*ZZ,ZJ*JZ+ZZ*'*ZZ%> by Def9
.= <%ZZ,ZJ*JZ%>
.= ZZZJ by Lm2;
then
A2: ZJZZ*a1 = <%ZJ*ZZ-ZJ*'*ZZ,ZJ*ZJ+ZZ*ZZ*'%> by Def9
.= <%ZZ,ZJ*ZJ%>;
<%ZJZZ,ZZZZ%> * <%ZZJZ,ZZZZ%> = <%a1,b1%> by Def9;
hence <%ZJZZ,ZZZZ%> * <%ZZJZ,ZZZZ%> * <%ZZZZ,ZJZZ%>
= <%a1*ZZZZ-ZJZZ*'*b1,ZJZZ*a1+b1*ZZZZ*'%> by Def9
.= <%ZZZZ,ZJZZ*a1%>
.= <%ZZZZ,<%ZZ,MZ%>%> by A1,A2;
end;
::e1*(e2*e5) = e6 in octonions
theorem Th35:
<%<%<%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
set a1 = ZZJZ*ZZZZ-ZJZZ*'*ZZZZ, b1 = ZJZZ*ZZJZ+ZZZZ*ZZZZ*';
A1: ZJ*ZJ*' = <%z*z-(-j)*'*j,(-j)*z+j*z*'%> by Lm3,Def9;
A2: JZ*ZJ = <%j*z-j*'*z,j*j+z*z*'%> by Def9;
b1 = <%ZJ*ZZ-JZ*'*ZZ,JZ*ZJ+ZZ*ZZ*'%> by Def9
.= <%ZZ,JZ*ZJ%>;
then
A3: b1*ZJZZ = <%ZZ*ZJ-ZZ*'*ZJ,ZZ*ZZ+ZJ*ZJ*'%> by A2,Def9
.= <%ZZ,JZ%> by A1;
<%ZZJZ,ZZZZ%> * <%ZZZZ,ZJZZ%> = <%a1,b1%> by Def9;
hence <%ZJZZ,ZZZZ%> * (<%ZZJZ,ZZZZ%> * <%ZZZZ,ZJZZ%>)
= <%ZJZZ*a1-b1*'*ZZZZ,b1*ZJZZ+ZZZZ*a1*'%> by Def9
.= <%ZZZZ,b1*ZJZZ%>
.= <%ZZZZ,ZZJZ%> by A3;
end;
registration
cluster Cayley-Dickson(Cayley-Dickson(Cayley-Dickson(N_Real)))
-> non associative non commutative;
coherence
proof
thus Cayley-Dickson(Cayley-Dickson(Cayley-Dickson(N_Real)))
is non associative
proof
take <%ZJZZ,ZZZZ%>, <%ZZJZ,ZZZZ%>, <%ZZZZ,ZJZZ%>;
<%-j,z%> <> JZ by Th3;
then <%ZZ,<%-j,z%>%> <> ZZJZ by Th3;
hence thesis by Th34,Th35,Th3;
end;
take <%ZJZZ,ZZZZ%>, <%ZZJZ,ZZZZ%>;
ZJ <> <%z,-j%> by Th3;
then <%ZZ,<%z,-j%>%> <> ZZZJ by Th3;
hence thesis by Th32,Th33,Th3;
end;
end;