:: The Quaternion Numbers
:: by Xiquan Liang and Fuguo Ge
::
:: Received November 14, 2006
:: Copyright (c) 2006-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 NUMBERS, XBOOLE_0, FUNCT_2, SUBSET_1, FUNCT_1, CARD_1, ORDINAL1,
FUNCOP_1, RELAT_1, TARSKI, ZFMISC_1, XCMPLX_0, ARYTM_0, XREAL_0, ARYTM_3,
ARYTM_2, ARYTM_1, COMPLEX1, REAL_1, SQUARE_1, XXREAL_0, QUATERNI,
FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ARYTM_3, NUMBERS, RELAT_1,
FUNCT_1, FUNCT_2, FUNCT_4, ENUMSET1, COMPLEX1, ARYTM_0, ZFMISC_1,
ARYTM_2, XCMPLX_0, XREAL_0, REAL_1, SQUARE_1, XXREAL_0, RELSET_1;
constructors ENUMSET1, FUNCT_4, ARYTM_1, ARYTM_0, REAL_1, SQUARE_1, COMPLEX1,
VALUED_1, RELSET_1;
registrations XBOOLE_0, ORDINAL1, FUNCT_4, NUMBERS, XXREAL_0, XREAL_0,
SQUARE_1, MEMBERED, VALUED_0, RELSET_1, FUNCT_7;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions TARSKI;
equalities SQUARE_1, TARSKI, ARYTM_3, XCMPLX_0, ORDINAL1, FUNCT_4;
expansions ARYTM_3, ZFMISC_1;
theorems FUNCT_2, XBOOLE_0, TARSKI, NUMBERS, ENUMSET1, FUNCT_4, XBOOLE_1,
FUNCT_1, ZFMISC_1, RELSET_1, COMPLEX1, ARYTM_2, ARYTM_0, SQUARE_1,
XREAL_0, CARD_1, XCMPLX_0, XREAL_1, ARYTM_3, ORDINAL3, ABSVALUE,
SERIES_3, XTUPLE_0;
begin
reserve a,b,c,d,x,y,w,z,x1,x2,x3,x4 , X for set;
reserve A for non empty set;
definition
func QUATERNION -> set equals
Funcs(4,REAL) \ { x where x is Element of Funcs(4,REAL):
x.2 = 0 & x.3 = 0} \/ COMPLEX;
coherence;
end;
definition
let x be Number;
attr x is quaternion means
:Def2:
x in QUATERNION;
end;
registration
cluster QUATERNION -> non empty;
coherence;
end;
registration
cluster quaternion for Number;
existence
proof
take the Element of QUATERNION;
thus thesis;
end;
end;
definition
mode Quaternion is quaternion Number;
end;
::$CD
::$CT 4
Lm1: 0,1,2,3 are_mutually_distinct;
theorem
{x1,x2,x3,x4} c= X iff x1 in X & x2 in X & x3 in X & x4 in X
proof
A1: x1 in {x1,x2,x3,x4} by ENUMSET1:def 2;
A2: x2 in {x1,x2,x3,x4} by ENUMSET1:def 2;
A3: x3 in {x1,x2,x3,x4} by ENUMSET1:def 2;
x4 in {x1,x2,x3,x4} by ENUMSET1:def 2;
hence {x1,x2,x3,x4} c= X implies x1 in X & x2 in X & x3 in X & x4 in X
by A1,A2,A3;
assume that
A4: x1 in X and
A5: x2 in X and
A6: x3 in X and
A7: x4 in X;
let z be object;
assume z in {x1,x2,x3,x4};
hence thesis by A4,A5,A6,A7,ENUMSET1:def 2;
end;
definition
let A,x,y,w,z;
let a,b,c,d be Element of A;
redefine func (x,y,w,z) --> (a,b,c,d) -> Function of {x,y,w,z},A; :: redefines --> (FUNCT_4, definition)
coherence
proof
set f=(x,y) --> (a,b),g=(w,z) --> (c,d),h = (x,y,w,z) --> (a,b,c,d);
A1: rng h c= rng f \/ rng g by FUNCT_4:17;
A2: dom h = {x,y,w,z} by FUNCT_4:137;
rng h c= A by A1,XBOOLE_1:1;
hence thesis by A2,FUNCT_2:def 1,RELSET_1:4;
end;
end;
definition
func <j> -> Number equals
(0,1,2,3) --> (0,0,1,0);
coherence;
func <k> -> Number equals
(0,1,2,3) --> (0,0,0,1);
coherence;
end;
reconsider jj=1, zz = 0 as Element of REAL by XREAL_0:def 1;
Lm2: <i> = [*zz,jj*] by ARYTM_0:def 5;
registration
cluster <i> -> quaternion;
coherence by Lm2,XBOOLE_0:def 3;
cluster <j> -> quaternion;
coherence
proof
set X = { x where x is Element of Funcs(4,REAL): x.2=0 & x.3=0};
A1: now
assume <j> in X;
then ex x being Element of Funcs(4,REAL) st <j> = x & x.2=0 & x.3=0;
hence contradiction by FUNCT_4:140;
end;
reconsider z=0,j=0,w=1,m=0 as Element of REAL by XREAL_0:def 1;
<j> = (0,1,2,3) --> (z,j,w,m);
then <j> in Funcs(4,REAL) by CARD_1:52,FUNCT_2:8;
then <j> in Funcs(4,REAL) \ X by A1,XBOOLE_0:def 5;
hence <j> in QUATERNION by XBOOLE_0:def 3;
end;
cluster <k> -> quaternion;
coherence
proof
set X = { x where x is Element of Funcs(4,REAL): x.2=0 & x.3=0};
A2: now
assume <k> in X;
then ex x being Element of Funcs(4,REAL) st <k> = x & x.2=0 & x.3=0;
hence contradiction by FUNCT_4:139;
end;
reconsider z=0,j=0,w=0,m=1 as Element of REAL by XREAL_0:def 1;
<k> = (0,1,2,3) --> (z,j,w,m);
then <k> in Funcs(4,REAL) by CARD_1:52,FUNCT_2:8;
then <k> in Funcs(4,REAL) \ X by A2,XBOOLE_0:def 5;
hence <k> in QUATERNION by XBOOLE_0:def 3;
end;
end;
registration
cluster -> quaternion for Element of QUATERNION;
coherence;
end;
definition
let x,y,w,z be Real;
func [*x,y,w,z*] -> Element of QUATERNION means
:Def5:
ex x9, y9 being Element of REAL st
x9 = x & y9 = y & it = [*x9,y9*] if w=0 & z=0
otherwise it = (0,1,2,3) --> (x,y,w,z);
consistency;
existence
proof
reconsider x9 = x, y9 = y, w9 = w, z9 = z as Element of REAL
by XREAL_0:def 1;
thus w = 0 & z = 0 implies ex t being Element of QUATERNION st
ex x9, y9 being Element of REAL st
x9 = x & y9 = y & t = [*x9,y9*]
proof
assume that w = 0 and z = 0;
set t = [*x9,y9*];
reconsider t as Element of QUATERNION by XBOOLE_0:def 3;
take t;
take x9, y9;
thus thesis;
end;
set e = (0,1,2,3) --> (x9,y9,w9,z9);
thus w <> 0 or z <> 0 implies
ex t being Element of QUATERNION st t = (0,1,2,3) --> (x,y,w,z)
proof
assume
A1: w <> 0 or z <> 0;
A2: e in Funcs(4,REAL) by CARD_1:52,FUNCT_2:8;
now
assume e in {r where r is Element of Funcs(4,REAL): r.2=0 & r.3=0};
then ex r being Element of Funcs(4,REAL) st e = r & r.2=0 & r.3=0;
hence contradiction by A1,FUNCT_4:139,140;
end;
then e in Funcs(4,REAL)
\ { r where r is Element of Funcs(4,REAL): r.2=0 & r.3 = 0}
by A2,XBOOLE_0:def 5;
then reconsider e as Element of QUATERNION by XBOOLE_0:def 3;
take e;
thus thesis;
end;
end;
uniqueness;
end;
Lm3: for x,y being Element of REAL holds [*x,y,0,0*] = [*x,y*]
proof
let x,y be Element of REAL;
ex x9, y9 being Element of REAL st ( x9 = x)&( y9 = y)&( [*x
,y,0,0*] = [*x9,y9*]) by Def5;
hence thesis;
end;
::$CT
theorem Th2:
for g being Quaternion
ex r,s,t,u being Real st g = [*r,s,t,u*]
proof
let g be Quaternion;
A1:g in QUATERNION by Def2;
per cases;
suppose g in COMPLEX;
then consider r,s being Element of REAL such that
A2: g = [*r,s*] by ARYTM_0:9;
take r,s,0,0;
thus thesis by A2,Def5,A1;
end;
suppose not g in COMPLEX;
then
A3: g in Funcs(4,REAL) \ { x where x is Element of Funcs(4,REAL):
x.2=0 & x.3=0} by A1,XBOOLE_0:def 3;
then consider f being Function such that
A4: g = f and
A5: dom f = 4 and
A6: rng f c= REAL by FUNCT_2:def 2;
A7: 0 in 4 by CARD_1:52,ENUMSET1:def 2;
A8: 1 in 4 by CARD_1:52,ENUMSET1:def 2;
A9: 2 in 4 by CARD_1:52,ENUMSET1:def 2;
A10: 3 in 4 by CARD_1:52,ENUMSET1:def 2;
A11: f.0 in rng f by A5,A7,FUNCT_1:3;
A12: f.1 in rng f by A5,A8,FUNCT_1:3;
A13: f.2 in rng f by A5,A9,FUNCT_1:3;
f.3 in rng f by A5,A10,FUNCT_1:3;
then reconsider
r = f.0, s = f.1, t=f.2, u=f.3 as Element of REAL by A6,A11,A12,A13;
A14: g = (0,1,2,3)-->(r,s,t,u) by A4,A5,FUNCT_4:144,CARD_1:52;
take r,s,t,u;
now
assume that
A15: t=0 and
A16: u=0;
A17: (0,1,2,3)-->(r,s,t,u).2 = 0 by A15,FUNCT_4:140;
(0,1,2,3)-->(r,s,t,u).3 = 0 by A16,FUNCT_4:139;
then g in { x where x is Element of Funcs(4,REAL):
x.2=0 & x.3=0} by A3,A14,A17;
hence contradiction by A3,XBOOLE_0:def 5;
end;
hence thesis by A14,Def5;
end;
end;
reserve i,j,k for Element of NAT;
reserve a,b,c,d for Real;
reserve y,r,s,x,t,w for Element of RAT+;
::$CT
Lm4: for x,y,z being object st [x,y] = {z} holds z = {x} & x = y
proof
let x,y,z be object;
assume
A1: [x,y] = {z};
then
A2: {x,y} in {z} by TARSKI:def 2;
{x} in {z} by A1,TARSKI:def 2;
hence
A3: z = {x} by TARSKI:def 1;
{x,y} = z by A2,TARSKI:def 1;
hence thesis by A3,ZFMISC_1:5;
end;
theorem Th3:
for A being Subset of RAT+ st (ex t st t in A & t <> {}) &
for r,s st r in A & s <=' r holds s in A
ex r1,r2,r3,r4,r5 being Element of RAT+ st
r1 in A & r2 in A & r3 in A & r4 in A & r5 in A &
r1 <> r2 & r1 <> r3 & r1<>r4 & r1 <> r5 & r2<> r3 & r2<> r4 &
r2<> r5& r3 <> r4 & r3 <> r5 & r4 <> r5
proof
let A be Subset of RAT+;
given t such that
A1: t in A and
A2: t <> {};
assume
A3: for r,s st r in A & s <=' r holds s in A;
consider x such that
A4: t = x+x by ARYTM_3:60;
consider y such that
A5: x = y+y by ARYTM_3:60;
consider w such that
A6: y = w+w by ARYTM_3:60;
take {},w,y,x,t;
A7: {} <=' t by ARYTM_3:64;
A8: x <=' t by A4;
A9: y <=' x by A5;
A10: w<=' y by A6;
A11: y <=' t by A8,A9,ARYTM_3:67;
w <=' x by A9,A10,ARYTM_3:67;
hence {} in A & w in A & y in A & x in A & t in A by A1,A3,A7,A8,A9,
ARYTM_3:67;
A12: {} <> x by A2,A4,ARYTM_3:50;
then
A13: {} <> y by A5,ARYTM_3:50;
A14: x <> t
proof
assume x = t;
then t+{} = t+t by A4,ARYTM_3:50;
hence contradiction by A2,ARYTM_3:62;
end;
A15: y <> x
proof
assume y = x;
then x+{} = x+x by A5,ARYTM_3:50;
hence contradiction by A12,ARYTM_3:62;
end;
w <> y
proof
assume w = y;
then y+{} = y+y by A6,ARYTM_3:50;
hence contradiction by A13,ARYTM_3:62;
end;
hence thesis by A2,A4,A5,A6,A8,A9,A10,A11,A14,A15,ARYTM_3:50,66;
end;
Lm5: not (0,1,2,3) --> (a,b,c,d) in REAL
proof
set f = (0,1,2,3)-->(a,b,c,d);
A1: f = {[0,a],[1,b],[2,c],[3,d]} by Lm1,FUNCT_4:145;
now
assume f in {[i,j]: i,j are_coprime & j <> {}};
then consider i,j such that
A2: f = [i,j] and i,j are_coprime and j<> {};
A3: {i} in f by A2,TARSKI:def 2;
A4: {i,j} in f by A2,TARSKI:def 2;
A5: now
assume i = j;
then {i} = {i,j} by ENUMSET1:29;
then
A6: [i,j] = {{i}} by ENUMSET1:29;
then
A7: [0,a] in {{i}} by A1,A2,ENUMSET1:def 2;
A8: [1,b] in {{i}} by A1,A2,A6,ENUMSET1:def 2;
A9: [0,a] = {i} by A7,TARSKI:def 1;
[1,b] = {i} by A8,TARSKI:def 1;
hence contradiction by A9,XTUPLE_0:1;
end;
per cases by A1,A3,A4,ENUMSET1:def 2;
suppose {i} = [0,a] & {i,j} = [0,a];
hence contradiction by A5,ZFMISC_1:5;
end;
suppose that
A10: {i} = [0,a] and
A11: {i,j} = [1,b];
A12: i = {0} by A10,Lm4;
i in {{1},{1,b}} by A11,TARSKI:def 2;
then i = {1,b} or i = {1} by TARSKI:def 2;
then 1 in i by TARSKI:def 1,def 2;
hence contradiction by A12,TARSKI:def 1;
end;
suppose that
A13: {i} = [0,a] and
A14: {i,j} = [2,c];
A15: i = {0} by A13,Lm4;
i in {{2},{2,c}} by A14,TARSKI:def 2;
then i = {2,c} or i = {2} by TARSKI:def 2;
then 2 in i by TARSKI:def 1,def 2;
hence contradiction by A15,TARSKI:def 1;
end;
suppose that
A16: {i} = [0,a] and
A17: {i,j} = [3,d];
A18: i = {0} by A16,Lm4;
i in {{3},{3,d}} by A17,TARSKI:def 2;
then i = {3,d} or i = {3} by TARSKI:def 2;
then 3 in i by TARSKI:def 1,def 2;
hence contradiction by A18,TARSKI:def 1;
end;
suppose that
A19: {i} = [1,b] and
A20: {i,j} = [0,a];
A21: i = {1} by A19,Lm4;
i in {{0},{0,a}} by A20,TARSKI:def 2;
then i = {0,a} or i = {0} by TARSKI:def 2;
then 0 in i by TARSKI:def 1,def 2;
hence contradiction by A21,TARSKI:def 1;
end;
suppose {i} = [1,b] & {i,j} = [1,b];
hence contradiction by A5,ZFMISC_1:5;
end;
suppose that
A22: {i} = [1,b] and
A23: {i,j} = [2,c];
A24: i = {1} by A22,Lm4;
i in {{2},{2,c}} by A23,TARSKI:def 2;
then i = {2,c} or i = {2} by TARSKI:def 2;
then 2 in i by TARSKI:def 1,def 2;
hence contradiction by A24,TARSKI:def 1;
end;
suppose that
A25: {i} = [1,b] and
A26: {i,j} = [3,d];
A27: i = {1} by A25,Lm4;
i in {{3},{3,d}} by A26,TARSKI:def 2;
then i = {3,d} or i = {3} by TARSKI:def 2;
then 3 in i by TARSKI:def 1,def 2;
hence contradiction by A27,TARSKI:def 1;
end;
suppose that
A28: {i} = [2,c] and
A29: {i,j} = [0,a];
A30: i = {2} by A28,Lm4;
i in {{0},{0,a}} by A29,TARSKI:def 2;
then i = {0,a} or i = {0} by TARSKI:def 2;
then 0 in i by TARSKI:def 1,def 2;
hence contradiction by A30,TARSKI:def 1;
end;
suppose that
A31: {i} = [2,c] and
A32: {i,j} = [1,b];
A33: i = {2} by A31,Lm4;
i in {{1},{1,b}} by A32,TARSKI:def 2;
then i = {1,b} or i = {1} by TARSKI:def 2;
then 1 in i by TARSKI:def 1,def 2;
hence contradiction by A33,TARSKI:def 1;
end;
suppose {i} = [2,c] & {i,j} = [2,c];
hence contradiction by A5,ZFMISC_1:5;
end;
suppose that
A34: {i} = [2,c] and
A35: {i,j} = [3,d];
A36: i = {2} by A34,Lm4;
i in {{3},{3,d}} by A35,TARSKI:def 2;
then i = {3,d} or i = {3} by TARSKI:def 2;
then 3 in i by TARSKI:def 1,def 2;
hence contradiction by A36,TARSKI:def 1;
end;
suppose that
A37: {i} = [3,d] and
A38: {i,j} = [0,a];
A39: i = {3} by A37,Lm4;
i in {{0},{0,a}} by A38,TARSKI:def 2;
then i = {0,a} or i = {0} by TARSKI:def 2;
then 0 in i by TARSKI:def 1,def 2;
hence contradiction by A39,TARSKI:def 1;
end;
suppose that
A40: {i} = [3,d] and
A41: {i,j} = [1,b];
A42: i = {3} by A40,Lm4;
i in {{1},{1,b}} by A41,TARSKI:def 2;
then i = {1,b} or i = {1} by TARSKI:def 2;
then 1 in i by TARSKI:def 1,def 2;
hence contradiction by A42,TARSKI:def 1;
end;
suppose that
A43: {i} = [3,d] and
A44: {i,j} = [2,c];
A45: i = {3} by A43,Lm4;
i in {{2},{2,c}} by A44,TARSKI:def 2;
then i = {2,c} or i = {2} by TARSKI:def 2;
then 2 in i by TARSKI:def 1,def 2;
hence contradiction by A45,TARSKI:def 1;
end;
suppose {i} = [3,d] & {i,j} = [3,d];
hence contradiction by A5,ZFMISC_1:5;
end;
end;
then
A46: not f in {[i,j]: i,j are_coprime & j <> {}} \
the set of all [k,1];
now
assume f in omega;
then f is non empty ordinal;
then {} in f by ORDINAL3:8;
hence contradiction by A1,ENUMSET1:def 2;
end;
then
A47: not f in RAT+ by A46,XBOOLE_0:def 3;
set IR = { A where A is Subset of RAT+:
for r being Element of RAT+ st r in A holds
(for s being Element of RAT+ st s <=' r holds s in A) &
ex s being Element of RAT+ st s in A & r < s};
not ex x,y,z,w being object st {[0,x],[1,y],[2,z],[3,w]} in IR
proof
given x,y,z,w being object such that
A48: {[0,x],[1,y],[2,z],[3,w]} in IR;
consider A being Subset of RAT+ such that
A49: {[0,x],[1,y],[2,z],[3,w]} = A and
A50: for r being Element of RAT+ st r in A holds
(for s being Element of RAT+ st s <=' r holds s in A) &
ex s being Element of RAT+ st s in A & r < s by A48;
A51: [0,x] in A by A49,ENUMSET1:def 2;
for r,s being Element of RAT+ st r in A & s <=' r holds s in A by A50;
then consider r1,r2,r3,r4,r5 being Element of RAT+ such that
A52: r1 in A and
A53: r2 in A and
A54: r3 in A and
A55: r4 in A and
A56: r5 in A and
A57: r1 <> r2 and
A58: r1 <> r3 and
A59: r1<>r4 and
A60: r1 <> r5 and
A61: r2<> r3 and
A62: r2<> r4 and
A63: r2<> r5 and
A64: r3 <> r4 and
A65: r3 <> r5 and
A66: r4 <> r5 by A51,Th3;
A67: r1 = [0,x] or r1 = [1,y] or r1 = [2,z] or r1 = [3,w]
by A49,A52,ENUMSET1:def 2;
A68: r2 = [0,x] or r2 = [1,y] or r2 = [2,z] or r2 = [3,w]
by A49,A53,ENUMSET1:def 2;
A69: r3 = [0,x] or r3 = [1,y] or r3 = [2,z] or r3 = [3,w]
by A49,A54,ENUMSET1:def 2;
r4 = [0,x] or r4 = [1,y] or r4 = [2,z] or r4 = [3,w]
by A49,A55,ENUMSET1:def 2;
hence contradiction by A49,A56,A57,A58,A59,A60,A61,A62,A63,A64,A65,A66,A67
,A68,A69,ENUMSET1:def 2;
end;
then not f in DEDEKIND_CUTS by A1,ARYTM_2:def 1;
then
A70: not f in REAL+ by A47,ARYTM_2:def 2,XBOOLE_0:def 3;
now
assume f in [:{{}},REAL+:];
then consider x,y being object such that
A71: x in {{}} and y in REAL+ and
A72: f = [x,y] by ZFMISC_1:84;
A73: x = 0 by A71,TARSKI:def 1;
f = {[0,a],[1,b],[2,c],[3,d]} by Lm1,FUNCT_4:145;
then
A74: [1,b] in f by ENUMSET1:def 2;
per cases by A72,A73,A74,TARSKI:def 2;
suppose {{1,b},{1}} = {0};
then 0 in {{1,b},{1}} by TARSKI:def 1;
hence contradiction by TARSKI:def 2;
end;
suppose {{1,b},{1}} = {0,y};
then 0 in {{1,b},{1}} by TARSKI:def 2;
hence contradiction by TARSKI:def 2;
end;
end;
hence thesis by A70,NUMBERS:def 1,XBOOLE_0:def 3;
end;
theorem Th4:
not (0,1,2,3) --> (a,b,c,d) in COMPLEX
proof
set f = (0,1,2,3)-->(a,b,c,d);
A1: not f in REAL by Lm5;
not f in Funcs({0,1},REAL)
proof
assume f in Funcs({0,1},REAL);
then dom f = {0,1} by FUNCT_2:92;
then {0,1,2,3} c= {0,1} by FUNCT_4:137;
then {0,1} \/ {2,3} c= {0,1} by ENUMSET1:5;
hence contradiction by XBOOLE_1:11,ZFMISC_1:22;
end;
then not f in Funcs({0,1},REAL)\
{ x where x is Element of Funcs({0,1},REAL): x.1 = 0};
hence thesis by A1,NUMBERS:def 2,XBOOLE_0:def 3;
end;
::$CT
theorem Th5:
for x1,x2,x3,x4,y1,y2,y3,y4 being Real st [*x1,x2,x3,x4*]
= [*y1,y2,y3,y4*] holds x1 = y1 & x2 = y2 & x3=y3 & x4=y4
proof
let x1,x2,x3,x4,y1,y2,y3,y4 be Real such that
A1: [*x1,x2,x3,x4*] = [*y1,y2,y3,y4*];
reconsider xx1=x1, xx2=x2, yy1=y1, yy2=y2 as Element of REAL
by XREAL_0:def 1;
per cases;
suppose
A2: x3=0 & x4=0;
then
A3: [*x1,x2,x3,x4*] = [*xx1,xx2*] by Lm3;
A4: now
assume y3<>0 or y4<>0;
then [*xx1,xx2*] = (0,1,2,3) --> (y1,y2,y3,y4) by A1,A3,Def5;
hence contradiction by Th4;
end;
then [*y1,y2,y3,y4*] = [*yy1,yy2*] by Lm3;
hence thesis by A1,A2,A3,A4,ARYTM_0:10;
end;
suppose x3<>0 or x4<>0;
then
A5: [*y1,y2,y3,y4*] = (0,1,2,3) --> (x1,x2,x3,x4) by A1,Def5;
now
assume that
A6: y3=0 and
A7: y4=0;
[*y1,y2,y3,y4*] = [*yy1,yy2*] by A6,A7,Lm3;
hence contradiction by A5,Th4;
end;
then [*y1,y2,y3,y4*] = (0,1,2,3) --> (y1,y2,y3,y4) by Def5;
hence thesis by A5,Lm1,FUNCT_4:146;
end;
end;
definition
let x,y be Quaternion;
consider x1,x2,x3,x4 being Real such that
A1: x = [*x1,x2,x3,x4*] by Th2;
consider y1,y2,y3,y4 being Real such that
A2: y = [*y1,y2,y3,y4*] by Th2;
func x + y -> Number means
:Def6:
ex x1,x2,x3,x4,y1,y2,y3,y4 being Real st
x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] &
it = [*x1+y1,x2+y2,x3+y3,x4+y4*];
existence
proof
take [*x1+y1,x2+y2,x3+y3,x4+y4*];
thus thesis by A1,A2;
end;
uniqueness
proof
let c1,c2 be Number;
given x1,x2,x3,x4,y1,y2,y3,y4 being Real such that
A3: x = [*x1,x2,x3,x4*] and
A4: y = [*y1,y2,y3,y4*] and
A5: c1 = [*x1+y1,x2+y2,x3+y3,x4+y4*];
given x19,x29,x39,x49,y19,y29,y39,y49 being Real such that
A6: x = [*x19,x29,x39,x49*] and
A7: y = [*y19,y29,y39,y49*] and
A8: c2 = [*x19+y19,x29+y29,x39+y39,x49+y49*];
A9: x1 = x19 by A3,A6,Th5;
A10: x2 = x29 by A3,A6,Th5;
A11: x3=x39 by A3,A6,Th5;
A12: x4=x49 by A3,A6,Th5;
A13: y1 = y19 by A4,A7,Th5;
A14: y2 = y29 by A4,A7,Th5;
y3=y39 by A4,A7,Th5;
hence thesis by A4,A5,A7,A8,A9,A10,A11,A12,A13,A14,Th5;
end;
commutativity;
end;
Lm6: 0 = [*0,0,0,0*]
proof
ex x9, y9 being Element of REAL st ( x9 = 0)&( y9 = 0)&( [*0
,0,0,0*] = [*x9,y9*]) by Def5;
hence thesis by ARYTM_0:def 5;
end;
definition
let z be Quaternion;
consider v,w,x,y being Real such that
A1: z = [*v,w,x,y*] by Th2;
func - z -> Quaternion means
:Def7:
z + it = 0;
existence
proof
reconsider z9 = [*- v, - w, - x, - y*] as Quaternion;
take z9;
A2: 0 =v+ -v;
A3: 0 = w+ -w;
A4: 0 = x+ -x;
0 = y+ -y;
hence thesis by A1,A2,A3,A4,Def6,Lm6;
end;
uniqueness
proof
let c1,c2 be Quaternion such that
A5: z + c1 = 0 and
A6: z + c2 = 0;
consider x1,x2,x3,x4,y1,y2,y3,y4 being Real such that
A7: z = [*x1,x2,x3,x4*] and
A8: c1 = [*y1,y2,y3,y4*] and
A9: 0 = [*x1+y1,x2+y2,x3+y3,x4+y4*] by A5,Def6;
consider x19,x29,x39,x49,y19,y29,y39,y49 being Real such that
A10: z = [*x19,x29,x39,x49*] and
A11: c2 = [*y19,y29,y39,y49*] and
A12: 0 = [*x19+y19,x29+y29,x39+y39,x49+y49*] by A6,Def6;
A13: x1 = x19 by A7,A10,Th5;
A14: x2 = x29 by A7,A10,Th5;
A15: x3 = x39 by A7,A10,Th5;
A16: x4 = x49 by A7,A10,Th5;
A17: x1+y1 = 0 by A9,Lm6,Th5;
A18: x1+y19 = 0 by A12,A13,Lm6,Th5;
A19: x2+y2 = 0 by A9,Lm6,Th5;
A20: x2+y29 = 0 by A12,A14,Lm6,Th5;
A21: x3+y3 = 0 by A9,Lm6,Th5;
A22: x3+y39 = 0 by A12,A15,Lm6,Th5;
A23: x4+y4 = 0 by A9,Lm6,Th5;
x4+y49 = 0 by A12,A16,Lm6,Th5;
hence thesis by A8,A11,A17,A18,A19,A20,A21,A22,A23;
end;
involutiveness;
end;
definition
let x,y be Quaternion;
func x-y -> Number equals
x + - y;
coherence;
end;
definition
let x,y be Quaternion;
consider x1,x2,x3,x4 being Real such that
A1: x = [*x1,x2,x3,x4*] by Th2;
consider y1,y2,y3,y4 being Real such that
A2: y = [*y1,y2,y3,y4*] by Th2;
func x*y -> Number means
:Def9:
ex x1,x2,x3,x4,y1,y2,y3,y4 being Real st
x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & it = [* x1*y1-x2*y2-x3*y3-x4*y4,
x1*y2+x2*y1+x3*y4-x4*y3, x1*y3+y1*x3+y2*x4-y4*x2,
x1*y4+x4*y1+x2*y3-x3*y2 *];
existence
proof
take [* x1*y1-x2*y2-x3*y3-x4*y4, x1*y2+x2*y1+x3*y4-x4*y3,
x1*y3+y1*x3+y2*x4-y4*x2, x1*y4+x4*y1+x2*y3-x3*y2 *];
thus thesis by A1,A2;
end;
uniqueness
proof
let c1,c2 be Number;
given x1,x2,x3,x4,y1,y2,y3,y4 being Real such that
A3: x = [*x1,x2,x3,x4*] and
A4: y = [*y1,y2,y3,y4*] and
A5: c1 = [* x1*y1-x2*y2-x3*y3-x4*y4, x1*y2+x2*y1+x3*y4-x4*y3,
x1*y3+y1*x3+y2*x4-y4*x2, x1*y4+x4*y1+x2*y3-x3*y2 *];
given x19,x29,x39,x49,y19,y29,y39,y49 being Real such that
A6: x = [*x19,x29,x39,x49*] and
A7: y = [*y19,y29,y39,y49*] and
A8: c2 = [* x19*y19-x29*y29-x39*y39-x49*y49, x19*y29+x29*y19+x39*y49-x49*y39,
x19*y39+y19*x39+y29*x49-y49*x29, x19*y49+x49*y19+x29*y39-x39*y29 *];
A9: x1 = x19 by A3,A6,Th5;
A10: x2 = x29 by A3,A6,Th5;
A11: x3 = x39 by A3,A6,Th5;
A12: x4 = x49 by A3,A6,Th5;
A13: y1 = y19 by A4,A7,Th5;
A14: y2 = y29 by A4,A7,Th5;
A15: y3 = y39 by A4,A7,Th5;
y4 = y49 by A4,A7,Th5;
hence thesis by A5,A8,A9,A10,A11,A12,A13,A14,A15;
end;
end;
registration
let z,z9 be Quaternion;
cluster z + z9 -> quaternion;
coherence
proof
ex x1,x2,x3,x4,y1,y2,y3,y4 being Real st
z = [*x1,x2,x3,x4*] & z9 = [*y1,y2,y3,y4*] &
z + z9 = [*x1+y1,x2+y2,x3+y3,x4+y4*] by Def6;
hence thesis;
end;
cluster z*z9 -> quaternion;
coherence
proof
ex x1,x2,x3,x4,y1,y2,y3,y4 being Real st
z = [*x1,x2,x3,x4*] & z9 = [*y1,y2,y3,y4*] &
z*z9 = [* x1*y1-x2*y2-x3*y3-x4*y4, x1*y2+x2*y1+x3*y4-x4*y3,
x1*y3+y1*x3+y2*x4-y4*x2, x1*y4+x4*y1+x2*y3-x3*y2 *] by Def9;
hence z*z9 in QUATERNION;
end;
end;
definition
redefine func <j> -> Element of QUATERNION equals :: redefines <j> (QUATERNI, definition)
[*0,0,1,0*];
coherence by Def2;
compatibility by Def5;
redefine func <k> -> Element of QUATERNION equals :: redefines <k> (QUATERNI, definition)
[*0,0,0,1*];
coherence by Def2;
compatibility by Def5;
end;
theorem
<i> * <i> = -1
proof
<i> = [*zz,jj,zz,zz*] by Lm2,Lm3; then
A1: <i> * <i> = [* 0*0-1*1-0*0-0*0, 0*1+1*0+0*0-0*0,
0*0+0*0+1*0-0*1, 0*0+0*0+1*0-0*1 *] by Def9
.= [*-1,0,0,0*];
-1 = [*-jj,zz*] by ARYTM_0:def 5;
hence thesis by A1,Lm3;
end;
theorem
<j> * <j> = -1
proof
A1: <j> * <j> = [* 0*0-0*0-1*1-0*0, 0*0+0*0+0*0-0*1,
0*1+0*1+0*0-0*0, 0*0+0*0+0*1-1*0 *] by Def9
.= [*-1,0,0,0*];
[*-1,0,0,0*] = [*-jj,zz*] by Lm3;
hence thesis by A1,ARYTM_0:def 5;
end;
theorem
<k> * <k> = -1
proof
A1: <k> * <k> = [* 0*0-0*0-0*0-1*1, 0*0+0*0+0*1-1*0,
0*0+0*0+0*1-1*0, 0*1+1*0+0*0-0*0 *] by Def9
.= [*-1,0,0,0*];
-1 = [*-jj,zz*] by ARYTM_0:def 5;
hence thesis by A1,Lm3;
end;
theorem
<i> * <j> = <k>
proof
<i> = [*0,1,0,0*] by Lm2,Lm3;
then <i> * <j> = [* 0*0-1*0-0*1-0*0, 0*0+1*0+0*0-0*1,
0*1+0*0+0*0-0*1, 0*0+0*0+1*1-0*0 *] by Def9
.= [*0,0,0,1*];
hence thesis;
end;
theorem
<j> * <k> = <i>
proof
<j> * <k> = [* 0*0-0*0-1*0-0*1, 0*0+0*0+1*1-0*0,
0*0+0*1+0*0-1*0, 0*1+0*0+0*0-1*0 *] by Def9
.= [*0,1,0,0*];
hence thesis by Lm2,Lm3;
end;
theorem
<k> * <i> = <j>
proof
<i> = [*0,1,0,0*] by Lm2,Lm3;
then <k> * <i> = [* 0*0-0*1-0*0-1*0, 0*1+0*0+0*0-1*0,
0*0+0*0+1*1-0*0, 0*0+1*0+0*0-0*1 *] by Def9
.= [*0,0,1,0*];
hence thesis;
end;
theorem
<i> * <j> = - <j> * <i>
proof
A1: <i> = [*zz,jj,zz,zz*] by Lm2,Lm3;
then
A2: <i> * <j> = [* 0*0-1*0-0*1-0*0, 0*0+1*0+0*0-0*1,
0*1+0*0+0*0-0*1, 0*0+0*0+1*1-0*0 *] by Def9
.= [*zz,zz,zz,jj*];
<j> * <i> = [* 0*0-0*1-1*0-0*0, 0*1+0*0+1*0-0*0,
0*0+0*1+1*0-0*0, 0*0+0*0+0*0-1*1 *] by A1,Def9
.= [*zz,zz,zz,-jj*];
then <i> * <j> + <j> * <i> = [*0+0,0+0,0+0,1+ -1*] by A2,Def6
.= 0 by Lm6;
hence thesis by Def7;
end;
theorem
<j> * <k> = - <k> * <j>
proof
A1: <j> * <k> = [* 0*0-0*0-1*0-0*1, 0*0+0*0+1*1-0*0,
0*0+0*1+0*0-1*0, 0*1+0*0+0*0-1*0 *] by Def9
.= [*zz,jj,zz,zz*];
<k> * <j> = [* 0*0-0*0-0*1-1*0, 0*0+0*0+0*0-1*1,
0*1+0*0+0*1-0*0, 0*0+1*0+0*1-0*0 *] by Def9
.= [*zz,-jj,zz,zz*];
then <j> * <k> + <k> * <j> = [*0+0,0+0,0+0,1+ -1*] by A1,Def6
.= 0 by Lm6;
hence thesis by Def7;
end;
theorem
<k> * <i> = - <i> * <k>
proof
A1: <i> = [*zz,jj,zz,zz*] by Lm2,Lm3;
then
A2: <k> * <i> = [* 0*0-0*1-0*0-1*0, 0*1+0*0+0*0-1*0,
0*0+0*0+1*1-0*0, 0*0+1*0+0*0-0*1 *] by Def9
.= [*zz,zz,jj,zz*];
<i> * <k> = [* 0*0-1*0-0*0-0*1, 0*0+1*0+0*1-0*0,
0*0+0*0+0*1-1*1, 0*1+0*0+1*0-0*0 *] by A1,Def9
.= [*zz,zz,-jj,zz*];
then <k> * <i> + <i> * <k> = [*0+0,0+0,1+ -1,0+0*] by A2,Def6
.= 0 by Lm6;
hence thesis by Def7;
end;
definition
let z be Quaternion;
func Rea z -> Number means
:Def12:
ex z9 being Complex st z=z9 & it = Re z9 if z in COMPLEX otherwise
ex f being Function of 4,REAL st z = f & it = f.0;
existence
proof
thus z in COMPLEX implies ex IT being Number,
z9 being Complex st z=z9 & IT = Re z9
proof
assume z in COMPLEX;
then consider r,s being Element of REAL such that
A1: z = [*r,s*] by ARYTM_0:9;
set z9=[*r,s*];
take Re z9,z9;
thus thesis by A1;
end;
assume
A2: not z in COMPLEX;
z in QUATERNION by Def2;
then z in Funcs(4,REAL) \ { x where x is Element of Funcs(4,REAL):
x.2=0 & x.3=0} by A2,XBOOLE_0:def 3;
then reconsider f = z as Function of 4, REAL by FUNCT_2:66;
take f.0, f;
thus thesis;
end;
uniqueness;
consistency;
func Im1 z -> Number means
:Def13:
ex z9 being Complex st z=z9 & it = Im z9 if z in COMPLEX otherwise
ex f being Function of 4,REAL st z = f & it = f.1;
existence
proof
thus z in COMPLEX implies ex IT being Number,
z9 being Complex st z=z9 & IT = Im z9
proof
assume z in COMPLEX;
then consider r,s being Element of REAL such that
A3: z = [*r,s*] by ARYTM_0:9;
set z9=[*r,s*];
take Im z9,z9;
thus thesis by A3;
end;
assume
A4: not z in COMPLEX;
z in QUATERNION by Def2;
then z in Funcs(4,REAL) \ { x where x is Element of Funcs(4,REAL):
x.2=0 & x.3=0} by A4,XBOOLE_0:def 3;
then reconsider f = z as Function of 4, REAL by FUNCT_2:66;
take f.1, f;
thus thesis;
end;
uniqueness;
consistency;
func Im2 z -> Number means
:Def14:
it = 0 if z in COMPLEX otherwise
ex f being Function of 4,REAL st z = f & it = f.2;
existence
proof
thus z in COMPLEX implies ex IT being Number st IT = 0;
assume
A5: not z in COMPLEX;
z in QUATERNION by Def2;
then z in Funcs(4,REAL) \ { x where x is Element of Funcs(4,REAL):
x.2=0 & x.3=0} by A5,XBOOLE_0:def 3;
then reconsider f = z as Function of 4, REAL by FUNCT_2:66;
take f.2, f;
thus thesis;
end;
uniqueness;
consistency;
func Im3 z -> Number means
:Def15:
it = 0 if z in COMPLEX otherwise
ex f being Function of 4,REAL st z = f & it = f.3;
existence
proof
thus z in COMPLEX implies ex IT being Number st IT = 0;
assume
A6: not z in COMPLEX;
z in QUATERNION by Def2;
then z in Funcs(4,REAL) \ { x where x is Element of Funcs(4,REAL):
x.2=0 & x.3=0} by A6,XBOOLE_0:def 3;
then reconsider f = z as Function of 4, REAL by FUNCT_2:66;
take f.3, f;
thus thesis;
end;
uniqueness;
consistency;
end;
registration
let z be Quaternion;
cluster Rea z -> real;
coherence
proof
per cases;
suppose z in COMPLEX;
then ex z9 being Complex st ( z = z9)&( Rea z = Re z9) by Def12;
hence thesis;
end;
suppose not z in COMPLEX;
then ex f being Function of 4,REAL st ( z = f)&( Rea z = f.0) by Def12;
hence thesis;
end;
end;
cluster Im1 z -> real;
coherence
proof
per cases;
suppose z in COMPLEX;
then ex z9 being Complex st ( z = z9)&( Im1 z = Im z9) by Def13;
hence thesis;
end;
suppose not z in COMPLEX;
then ex f being Function of 4,REAL st ( z = f)&( Im1 z = f.1) by Def13;
hence thesis;
end;
end;
cluster Im2 z -> real;
coherence
proof
per cases;
suppose z in COMPLEX;
hence thesis by Def14;
end;
suppose not z in COMPLEX;
then ex f being Function of 4,REAL st ( z = f)&( Im2 z = f.2) by Def14;
hence thesis;
end;
end;
cluster Im3 z -> real;
coherence
proof
per cases;
suppose z in COMPLEX;
hence thesis by Def15;
end;
suppose not z in COMPLEX;
then ex f being Function of 4,REAL st ( z = f)&( Im3 z = f.3) by Def15;
hence thesis;
end;
end;
end;
theorem Th15:
for f being Function of 4,REAL ex a,b,c,d st f = (0,1,2,3)-->(a,b,c,d)
proof
let f be Function of 4,REAL;
reconsider a = f.0, b = f.1, c = f.2, d = f.3 as Element of REAL
by XREAL_0:def 1;
take a,b,c,d;
dom f = {0,1,2,3} by CARD_1:52,FUNCT_2:def 1;
hence thesis by FUNCT_4:144;
end;
Lm7: for a,b being Element of REAL holds Re [*a,b*] = a & Im [*a,b*] = b
proof let a,b be Element of REAL;
reconsider a9 =a, b9 = b as Element of REAL;
thus Re [*a,b*] = a proof per cases;
suppose b = 0;
then [*a,b*] = a by ARYTM_0:def 5;
hence thesis by COMPLEX1:def 1;
end;
suppose b <> 0;
then
A1: [*a,b*] = (0,1)-->(a9,b9) by ARYTM_0:def 5;
then reconsider f = [*a,b*] as Function of 2, REAL by CARD_1:50;
not [*a,b*] in REAL by A1,ARYTM_0:8; then
a2: not [*a,b*] is real by XREAL_0:def 1;
f.0 = a by A1,FUNCT_4:63;
hence thesis by a2,COMPLEX1:def 1;
end;
end;
per cases;
suppose
A3: b = 0;
then [*a,b*] = a by ARYTM_0:def 5;
hence thesis by A3,COMPLEX1:def 2;
end;
suppose b <> 0;
then
A4: [*a,b*] = (0,1)-->(a9,b9) by ARYTM_0:def 5;
then reconsider f = [*a,b*] as Function of 2, REAL by CARD_1:50;
not [*a,b*] in REAL by A4,ARYTM_0:8; then
a5: not [*a,b*] is real by XREAL_0:def 1;
f.1 = b by A4,FUNCT_4:63;
hence thesis by a5,COMPLEX1:def 2;
end;
end;
Lm8: for z being Complex holds [*Re z, Im z*] = z
proof
let z be Complex;
A1: z in COMPLEX by XCMPLX_0:def 2;
per cases;
suppose
A2: z in REAL;
then Im z = 0 by COMPLEX1:def 2;
hence [*Re z, Im z*] = Re z by ARYTM_0:def 5
.= z by A2,COMPLEX1:def 1;
end;
suppose
A3: not z in REAL; then
a3: not z is real by XREAL_0:def 1;
then
A4: ex f being Function of 2,REAL st ( z = f)&( Im z = f.1) by COMPLEX1:def 2;
A5: ex f being Function of 2,REAL st ( z = f)&( Re z = f.0) by a3,
COMPLEX1:def 1;
consider a,b being Element of REAL such that
A6: z = (0,1)-->(a,b) by A4,COMPLEX1:2;
A7: Re z = a by A5,A6,FUNCT_4:63;
A8: Im z = b by A4,A6,FUNCT_4:63;
z in Funcs(2,REAL) \ { x where x is Element of Funcs(2,REAL): x.1 = 0 }
by A1,A3,CARD_1:50,NUMBERS:def 2,XBOOLE_0:def 3;
then
A9: not z in { x where x is Element of Funcs(2,REAL): x.1 = 0}
by XBOOLE_0:def 5;
reconsider f = z as Element of Funcs(2,REAL) by A6,CARD_1:50,FUNCT_2:8;
f.1 <> 0 by A9;
then b <> 0 by A6,FUNCT_4:63;
hence thesis by A6,A7,A8,ARYTM_0:def 5;
end;
end;
theorem Th16:
Rea [*a,b,c,d*] = a & Im1 [*a,b,c,d*] = b &
Im2 [*a,b,c,d*] = c & Im3 [*a,b,c,d*] = d
proof
reconsider aa = a, bb = b, c9 = c, d9 = d as Element of REAL
by XREAL_0:def 1;
thus Rea [*a,b,c,d*] = a
proof
per cases;
suppose c = 0 & d=0;
then
A1: [*a,b,c,d*] = [*aa,bb*] by Lm3;
Re [*aa,bb*] =a by Lm7;
hence thesis by A1,Def12;
end;
suppose c <> 0 or d<>0;
then
A2: [*a,b,c,d*] = (0,1,2,3)-->(aa,bb,c9,d9) by Def5;
then reconsider f = [*a,b,c,d*] as Function of 4, REAL by CARD_1:52;
A3: not [*a,b,c,d*] in COMPLEX by A2,Th4;
f.0 = a by A2,FUNCT_4:142;
hence thesis by A3,Def12;
end;
end;
thus Im1 [*a,b,c,d*] = b
proof
per cases;
suppose c = 0 & d = 0;
then
A4: [*a,b,c,d*] = [*aa,bb*] by Lm3;
Im [*aa,bb*] = b by Lm7;
hence thesis by A4,Def13;
end;
suppose c <> 0 or d <> 0;
then
A5: [*a,b,c,d*] = (0,1,2,3) --> (aa,bb,c9,d9) by Def5;
then reconsider f = [*a,b,c,d*] as Function of 4, REAL by CARD_1:52;
A6: not [*a,b,c,d*] in COMPLEX by A5,Th4;
f.1 = b by A5,FUNCT_4:141;
hence thesis by A6,Def13;
end;
end;
thus Im2 [*a,b,c,d*] = c
proof
per cases;
suppose
A7: c = 0 & d = 0;
then [*a,b,c,d*] = [*aa,bb*] by Lm3;
hence thesis by A7,Def14;
end;
suppose c <> 0 or d <> 0;
then
A8: [*a,b,c,d*] = (0,1,2,3) --> (aa,bb,c9,d9) by Def5;
then reconsider f = [*a,b,c,d*] as Function of 4, REAL by CARD_1:52;
A9: not [*a,b,c,d*] in COMPLEX by A8,Th4;
f.2 = c by A8,FUNCT_4:140;
hence thesis by A9,Def14;
end;
end;
per cases;
suppose
A10: c = 0 & d = 0;
then [*a,b,c,d*] = [*aa,bb*] by Lm3;
hence thesis by A10,Def15;
end;
suppose c <> 0 or d <> 0;
then
A11: [*a,b,c,d*] = (0,1,2,3) --> (aa,bb,c9,d9) by Def5;
then reconsider f = [*a,b,c,d*] as Function of 4, REAL by CARD_1:52;
A12: not [*a,b,c,d*] in COMPLEX by A11,Th4;
f.3 = d by A11,FUNCT_4:139;
hence thesis by A12,Def15;
end;
end;
reserve z,z1,z2,z3,z4 for Quaternion;
theorem Th17:
z = [*Rea z, Im1 z, Im2 z, Im3 z*]
proof
A1: z in QUATERNION by Def2;
per cases;
suppose
A2: z in COMPLEX;
then
A3: Im2 z = 0 by Def14;
A4: Im3 z = 0 by A2,Def15;
A5: ex z9 being Complex st ( z = z9)&( Rea z = Re z9) by A2,Def12;
consider z9 being Complex such that
A6: z = z9 and
A7: Im1 z = Im z9 by A2,Def13;
reconsider Rz = Rea z, Imz = Im1 z as Element of REAL by XREAL_0:def 1;
[*Rz, Imz*] = z9 by A5,A6,A7,Lm8;
hence thesis by A3,A4,A6,Lm3;
end;
suppose
A8: not z in COMPLEX;
then
A9: ex f being Function of 4,REAL st ( z = f)&( Im1 z = f.1) by Def13;
A10: ex f being Function of 4,REAL st ( z = f)&( Rea z = f.0) by A8,Def12;
A11: ex f being Function of 4,REAL st ( z = f)&( Im2 z = f.2) by A8,Def14;
A12: ex f being Function of 4,REAL st ( z = f)&( Im3 z = f.3) by A8,Def15;
consider a,b,c,d being Real such that
A13: z = (0,1,2,3)-->(a,b,c,d) by A9,Th15;
reconsider a,b,c,d as Element of REAL by XREAL_0:def 1;
A14: z = (0,1,2,3)-->(a,b,c,d) by A13;
A15: Rea z = a by A10,A14,FUNCT_4:142;
A16: Im1 z = b by A9,A14,FUNCT_4:141;
A17: Im2 z = c by A11,A14,FUNCT_4:140;
A18: Im3 z = d by A12,A14,FUNCT_4:139;
z in Funcs(4,REAL) \ { x where x is Element of Funcs(4,REAL):
x.2 = 0 & x.3 = 0} by A1,A8,XBOOLE_0:def 3;
then
A19: not z in { x where x is Element of Funcs(4,REAL):
x.2 = 0 & x.3 = 0} by XBOOLE_0:def 5;
reconsider f = z as Element of Funcs(4,REAL) by A14,CARD_1:52,FUNCT_2:8;
f.2 <> 0 or f.3 <> 0 by A19;
then c <> 0 or d <> 0 by A14,FUNCT_4:139,140;
hence thesis by A14,A15,A16,A17,A18,Def5;
end;
end;
theorem Th18:
Rea z1 = Rea z2 & Im1 z1 = Im1 z2 & Im2 z1 = Im2 z2 &
Im3 z1 = Im3 z2 implies z1 = z2
proof
assume that
A1: Rea z1 = Rea z2 and
A2: Im1 z1 = Im1 z2 and
A3: Im2 z1 = Im2 z2 and
A4: Im3 z1 = Im3 z2;
thus z1 = [*Rea z2,Im1 z2,Im2 z2,Im3 z2*] by A1,A2,A3,A4,Th17
.= z2 by Th17;
end;
definition
func 0q -> Quaternion equals
0;
coherence by Lm6;
func 1q -> Quaternion equals
1;
coherence
proof
[*1,0,0,0*] = [*jj,zz*] by Lm3;
hence thesis by ARYTM_0:def 5;
end;
end;
Lm9: for a, b, c, d being Real st a^2 + b^2 + c^2 + d^2 = 0 holds
a = 0 & b = 0 & c = 0 & d = 0
proof
let a, b, c, d be Real;
assume
A1: a^2 + b^2 + c^2 + d^2 = 0;
A2: 0 <= a^2 by XREAL_1:63;
A3: 0 <= b^2 by XREAL_1:63;
A4: 0 <= c^2 by XREAL_1:63;
A5: 0 <= d^2 by XREAL_1:63;
assume
A6: a <> 0 or b <> 0 or c <> 0 or d <> 0;
per cases by A6;
suppose a <> 0;
then 0 < a^2 + b^2 by A3,SQUARE_1:12,XREAL_1:34;
hence contradiction by A1,A4,A5;
end;
suppose b <> 0;
then 0 < a^2 + b^2 by A2,SQUARE_1:12,XREAL_1:34;
hence contradiction by A1,A4,A5;
end;
suppose c <> 0;
then 0 < c^2 + d^2 by A5,SQUARE_1:12,XREAL_1:34;
then 0 < (a^2 + b^2) + (c^2 + d^2) by A2,A3;
hence contradiction by A1;
end;
suppose d <> 0;
then 0 < c^2 + d^2 by A4,SQUARE_1:12,XREAL_1:34;
then 0 < (a^2 + b^2) + (c^2 + d^2) by A2,A3;
hence contradiction by A1;
end;
end;
theorem Th19:
Rea z = 0 & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 implies z = 0q
proof
assume that
A1: Rea z = 0 and
A2: Im1 z = 0 and
A3: Im2 z = 0 and
A4: Im3 z = 0;
A5: Rea z = Rea [*0,0,0,0*] by A1,Th16;
A6: Im1 z = Im1 [*0,0,0,0*] by A2,Th16;
A7: Im2 z = Im2 [*0,0,0,0*] by A3,Th16;
Im3 z = Im3 [*0,0,0,0*] by A4,Th16;
hence thesis by A5,A6,A7,Lm6,Th18;
end;
theorem
z = 0 implies (Rea z)^2 + (Im1 z)^2 +(Im2 z)^2 + (Im3 z)^2 = 0
proof
assume
A1: z = 0; then
A2: Rea z = 0 by Lm6,Th16;
A3: Im1 z = 0 by A1,Lm6,Th16;
Im2 z = 0 by A1,Lm6,Th16;
hence thesis by A1,A2,A3,Lm6,Th16;
end;
theorem
(Rea z)^2 + (Im1 z)^2 +(Im2 z)^2 + (Im3 z)^2 = 0 implies z = 0q
proof
assume
A1: (Rea z)^2 + (Im1 z)^2 +(Im2 z)^2 + (Im3 z)^2 = 0;
then
A2: Rea z = 0 by Lm9;
A3: Im1 z = 0 by A1,Lm9;
A4: Im2 z = 0 by A1,Lm9;
Im3 z = 0 by A1,Lm9;
hence thesis by A2,A3,A4,Th19;
end;
Lm10: [*jj,zz,zz,zz*] = 1
proof
[*1,0,0,0*] = [*jj,zz*] by Lm3;
hence thesis by ARYTM_0:def 5;
end;
theorem
Rea (1q) = 1 & Im1(1q) = 0 & Im2 (1q) = 0 & Im3 (1q) = 0
by Lm10,Th16;
theorem Th23:
Rea <i> = 0 & Im1 <i> = 1 & Im2 <i> = 0 & Im3 <i> = 0
proof
[*zz,jj*] = [*0,1,0,0*] by Lm3;
hence thesis by Lm2,Th16;
end;
theorem Th24:
Rea <j> = 0 & Im1 <j> = 0 & Im2 <j> = 1 & Im3 <j> = 0 &
Rea <k> = 0 & Im1 <k> = 0 & Im2 <k> = 0 & Im3 <k> = 1
by Th16;
Lm11: for m,n,x,y,z being Quaternion st z = m + n + x + y
holds Rea z = Rea m +Rea n +Rea x + Rea y &
Im1 z = Im1 m + Im1 n + Im1 x + Im1 y &
Im2 z = Im2 m + Im2 n + Im2 x + Im2 y & Im3 z = Im3 m + Im3 n + Im3 x + Im3 y
proof
let m,n,x,y,z be Quaternion such that
A1: z = m + n + x + y;
consider m1,m2,m3,m4,n1,n2,n3,n4 being Real such that
A2: m = [*m1,m2,m3,m4*] and
A3: n = [*n1,n2,n3,n4*] and
A4: m + n = [*m1+n1, m2+n2, m3+n3, m4+n4*] by Def6;
consider x1,x2,x3,x4,y1,y2,y3,y4 being Real such that
A5: x = [*x1,x2,x3,x4*] and
A6: y = [*y1,y2,y3,y4*] and
x + y = [*x1+y1, x2+y2, x3+y3, x4+y4*] by Def6;
A7: Rea m = m1 by A2,Th16;
A8: Rea n = n1 by A3,Th16;
A9: Rea x = x1 by A5,Th16;
A10: Rea y = y1 by A6,Th16;
A11: Im1 m = m2 by A2,Th16;
A12: Im1 n = n2 by A3,Th16;
A13: Im1 x = x2 by A5,Th16;
A14: Im1 y = y2 by A6,Th16;
A15: Im2 m = m3 by A2,Th16;
A16: Im2 n = n3 by A3,Th16;
A17: Im2 x = x3 by A5,Th16;
A18: Im2 y = y3 by A6,Th16;
A19: Im3 m = m4 by A2,Th16;
A20: Im3 n = n4 by A3,Th16;
A21: Im3 x = x4 by A5,Th16;
A22: Im3 y = y4 by A6,Th16;
m+n+x =[*m1+n1+x1, m2+n2+x2, m3+n3+x3, m4+n4+x4*] by A4,A5,Def6;
then z = [*m1+n1+x1+y1, m2+n2+x2+y2,
m3+n3+x3+y3, m4+n4+x4+y4*] by A1,A6,Def6;
hence thesis by A7,A8,A9,A10,A11,A12,A13,A14,A15,A16,A17,A18,A19,A20,A21,A22
,Th16;
end;
Lm12: for x,y,z being Quaternion st z = x + y
holds Rea z = Rea x + Rea y & Im1 z = Im1 x + Im1 y &
Im2 z = Im2 x + Im2 y & Im3 z = Im3 x + Im3 y
proof
let x,y,z be Quaternion such that
A1: z = x + y;
consider x1,x2,x3,x4,y1,y2,y3,y4 being Real such that
A2: x = [*x1,x2,x3,x4*] and
A3: y = [*y1,y2,y3,y4*] and
A4: x + y = [*x1+y1, x2+y2, x3+y3, x4+y4*] by Def6;
A5: Rea x = x1 by A2,Th16;
A6: Rea y = y1 by A3,Th16;
A7: Im1 x = x2 by A2,Th16;
A8: Im1 y = y2 by A3,Th16;
A9: Im2 x = x3 by A2,Th16;
A10: Im2 y = y3 by A3,Th16;
A11: Im3 x = x4 by A2,Th16;
Im3 y = y4 by A3,Th16;
hence thesis by A1,A4,A5,A6,A7,A8,A9,A10,A11,Th16;
end;
Lm13: z1 + z2 = [* Rea z1 + Rea z2, Im1 z1 + Im1 z2,
Im2 z1 + Im2 z2, Im3 z1 + Im3 z2 *]
proof
set z = [* Rea z1 + Rea z2, Im1 z1 + Im1 z2,
Im2 z1 + Im2 z2, Im3 z1 + Im3 z2 *];
reconsider z9 = z1 + z2 as Quaternion;
A1: Rea z = Rea z1 + Rea z2 by Th16
.= Rea z9 by Lm12;
A2: Im1 z = Im1 z1 + Im1 z2 by Th16
.= Im1 z9 by Lm12;
A3: Im2 z = Im2 z1 + Im2 z2 by Th16
.= Im2 z9 by Lm12;
Im3 z = Im3 z1 + Im3 z2 by Th16
.= Im3 z9 by Lm12;
hence thesis by A1,A2,A3,Th18;
end;
Lm14: for x,y,z being Quaternion st z = x * y
holds Rea z = Rea x * Rea y - Im1 x * Im1 y - Im2 x * Im2 y - Im3 x * Im3 y &
Im1 z = Rea x * Im1 y + Im1 x * Rea y + Im2 x * Im3 y - Im3 x * Im2 y &
Im2 z = Rea x * Im2 y + Im2 x * Rea y + Im3 x * Im1 y - Im1 x * Im3 y &
Im3 z = Rea x * Im3 y + Im3 x * Rea y + Im1 x * Im2 y - Im2 x * Im1 y
proof
let x,y,z be Quaternion such that
A1: z = x * y;
consider x1,x2,x3,x4,y1,y2,y3,y4 being Real such that
A2: x = [*x1,x2,x3,x4*] and
A3: y = [*y1,y2,y3,y4*] and
A4: x * y = [* x1*y1-x2*y2-x3*y3-x4*y4, x1*y2+x2*y1+x3*y4-x4*y3,
x1*y3+y1*x3+y2*x4-y4*x2, x1*y4+x4*y1+x2*y3-x3*y2 *] by Def9;
A5: Rea x = x1 by A2,Th16;
A6: Rea y = y1 by A3,Th16;
A7: Im1 x = x2 by A2,Th16;
A8: Im1 y = y2 by A3,Th16;
A9: Im2 x = x3 by A2,Th16;
A10: Im2 y = y3 by A3,Th16;
A11: Im3 x = x4 by A2,Th16;
Im3 y = y4 by A3,Th16;
hence thesis by A1,A4,A5,A6,A7,A8,A9,A10,A11,Th16;
end;
Lm15: z1 + z2 + z3 + z4 = [* Rea z1 + Rea z2 + Rea z3 + Rea z4,
Im1 z1 + Im1 z2 + Im1 z3 + Im1 z4, Im2 z1 + Im2 z2 + Im2 z3 + Im2 z4,
Im3 z1 + Im3 z2 + Im3 z3 + Im3 z4 *]
proof
set z = [* Rea z1 + Rea z2 + Rea z3 + Rea z4,
Im1 z1 + Im1 z2 + Im1 z3 + Im1 z4, Im2 z1 + Im2 z2 + Im2 z3 + Im2 z4,
Im3 z1 + Im3 z2 + Im3 z3 + Im3 z4 *];
reconsider z9 = z1 + z2 + z3 + z4 as Quaternion;
A1: Rea z = Rea z1 + Rea z2 + Rea z3 + Rea z4 by Th16
.= Rea z9 by Lm11;
A2: Im1 z = Im1 z1 + Im1 z2 + Im1 z3 + Im1 z4 by Th16
.= Im1 z9 by Lm11;
A3: Im2 z = Im2 z1 + Im2 z2 + Im2 z3 + Im2 z4 by Th16
.= Im2 z9 by Lm11;
Im3 z = Im3 z1 + Im3 z2 + Im3 z3 + Im3 z4 by Th16
.= Im3 z9 by Lm11;
hence thesis by A1,A2,A3,Th18;
end;
Lm16: z1 * z2 =
[*Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2,
Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2,
Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2,
Rea z1 * Im3 z2 + Im3 z1 * Rea z2 + Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2 *]
proof
set z =
[*Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2,
Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2,
Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2,
Rea z1 * Im3 z2 + Im3 z1 * Rea z2 + Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2 *];
reconsider z9 = z1 * z2 as Quaternion;
A1: Rea z = Rea z1 * Rea z2 - Im1 z1 * Im1 z2 -
Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2 by Th16
.= Rea z9 by Lm14;
A2: Im1 z = Rea z1 * Im1 z2 + Im1 z1 * Rea z2 +
Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2 by Th16
.= Im1 z9 by Lm14;
A3: Im2 z = Rea z1 * Im2 z2 + Im2 z1 * Rea z2 +
Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2 by Th16
.= Im2 z9 by Lm14;
Im3 z = Rea z1 * Im3 z2 + Im3 z1 * Rea z2 +
Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2 by Th16
.= Im3 z9 by Lm14;
hence thesis by A1,A2,A3,Th18;
end;
Lm17: Rea (z1 * z2) =
Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2 &
Im1 (z1 * z2) =
Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2 &
Im2 (z1 * z2) =
Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2 &
Im3 (z1 * z2) =
Rea z1 * Im3 z2 + Im3 z1 * Rea z2 + Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2
proof
z1 * z2 =
[*Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2,
Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2,
Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2,
Rea z1 * Im3 z2 + Im3 z1 * Rea z2 + Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2 *]
by Lm16;
hence thesis by Th16;
end;
theorem
Rea (z1 + z2 + z3 + z4) = Rea z1 + Rea z2 + Rea z3 + Rea z4 &
Im1 (z1 + z2 + z3 + z4) = Im1 z1 + Im1 z2 + Im1 z3 + Im1 z4 &
Im2 (z1 + z2 + z3 + z4) = Im2 z1 + Im2 z2 + Im2 z3 + Im2 z4 &
Im3 (z1 + z2 + z3 + z4) = Im3 z1 + Im3 z2 + Im3 z3 + Im3 z4
proof
(z1 + z2 + z3 + z4) = [* Rea z1 + Rea z2 + Rea z3 + Rea z4,
Im1 z1 + Im1 z2 + Im1 z3 + Im1 z4, Im2 z1 + Im2 z2 + Im2 z3 + Im2 z4,
Im3 z1 + Im3 z2 + Im3 z3 + Im3 z4*] by Lm15;
hence thesis by Th16;
end;
reserve x for Real;
Lm18: z = x implies Rea z = x & Im1 z = 0 & Im2 z = 0 & Im3 z = 0
proof
assume
A1: z = x;
reconsider xx=x, zz=0 as Element of REAL by XREAL_0:def 1;
A2: x = [*xx,zz*] by ARYTM_0:def 5;
[*xx,zz*] = [*x,0,0,0*] by Lm3;
hence thesis by A1,A2,Th16;
end;
theorem
z1 = x implies Rea (z1*<i>) = 0 &
Im1 (z1*<i>) = x & Im2 (z1*<i>) = 0 & Im3 (z1*<i>) = 0
proof
assume
A1: z1 = x;
A2: Rea (z1 * <i>) = Rea z1 * Rea <i> - Im1 z1 * Im1 <i> - Im2 z1 * Im2 <i>
- Im3 z1 * Im3 <i> by Lm17;
A3: Im1 (z1 * <i>) = Rea z1 * Im1 <i> + Im1 z1 * Rea <i> + Im2 z1 * Im3 <i>
- Im3 z1 * Im2 <i> by Lm17;
A4: Im2 (z1 * <i>) = Rea z1 * Im2 <i> + Im2 z1 * Rea <i> + Im3 z1 * Im1 <i>
- Im1 z1 * Im3 <i> by Lm17;
Im3 (z1 * <i>) = Rea z1 * Im3 <i> + Im3 z1 * Rea <i> + Im1 z1 * Im2 <i>
- Im2 z1 * Im1 <i> by Lm17;
hence thesis by A1,A2,A3,A4,Lm18,Th23;
end;
theorem
z1 = x implies Rea (z1*<j>) = 0 &
Im1 (z1*<j>) = 0 & Im2 (z1*<j>) = x & Im3 (z1*<j>) = 0
proof
assume
A1: z1 = x;
A2: Rea (z1 * <j>) = Rea z1 * Rea <j> - Im1 z1 * Im1 <j> - Im2 z1 * Im2 <j>
- Im3 z1 * Im3 <j> by Lm17;
A3: Im1 (z1 * <j>) = Rea z1 * Im1 <j> + Im1 z1 * Rea <j> + Im2 z1 * Im3 <j>
- Im3 z1 * Im2 <j> by Lm17;
A4: Im2 (z1 * <j>) = Rea z1 * Im2 <j> + Im2 z1 * Rea <j> + Im3 z1 * Im1 <j>
- Im1 z1 * Im3 <j> by Lm17;
Im3 (z1 * <j>) = Rea z1 * Im3 <j> + Im3 z1 * Rea <j> + Im1 z1 * Im2 <j>
- Im2 z1 * Im1 <j> by Lm17;
hence thesis by A1,A2,A3,A4,Lm18,Th24;
end;
theorem
z1 = x implies Rea (z1*<k>) = 0 &
Im1 (z1*<k>) = 0 & Im2 (z1*<k>) = 0 & Im3 (z1*<k>) = x
proof
assume
A1: z1 = x;
A2: Rea (z1 * <k>) = Rea z1 * Rea <k> - Im1 z1 * Im1 <k> - Im2 z1 * Im2 <k>
- Im3 z1 * Im3 <k> by Lm17;
A3: Im1 (z1 * <k>) = Rea z1 * Im1 <k> + Im1 z1 * Rea <k> + Im2 z1 * Im3 <k>
- Im3 z1 * Im2 <k> by Lm17;
A4: Im2 (z1 * <k>) = Rea z1 * Im2 <k> + Im2 z1 * Rea <k> + Im3 z1 * Im1 <k>
- Im1 z1 * Im3 <k> by Lm17;
Im3 (z1 * <k>) = Rea z1 * Im3 <k> + Im3 z1 * Rea <k> + Im1 z1 * Im2 <k>
- Im2 z1 * Im1 <k> by Lm17;
hence thesis by A1,A2,A3,A4,Lm18,Th24;
end;
definition
let x be Real, y be Quaternion;
consider y1,y2,y3,y4 being Real such that
A1: y = [*y1,y2,y3,y4*] by Th2;
func x + y -> Number means
:Def18:
ex y1,y2,y3,y4 being Real st y = [*y1,y2,y3,y4*] &
it = [*x+y1,y2,y3,y4*];
existence
proof
take [*x+y1,y2,y3,y4*];
thus thesis by A1;
end;
uniqueness
proof
let c1,c2 be Number;
given y1,y2,y3,y4 being Real such that
A2: y = [*y1,y2,y3,y4*] and
A3: c1 = [*x+y1,y2,y3,y4*];
given y19,y29,y39,y49 being Real such that
A4: y = [*y19,y29,y39,y49*] and
A5: c2 = [*x+y19,y29,y39,y49*];
A6: y1 = y19 by A2,A4,Th5;
A7: y2 = y29 by A2,A4,Th5;
y3 = y39 by A2,A4,Th5;
hence thesis by A2,A3,A4,A5,A6,A7,Th5;
end;
end;
definition
let x be Real, y be Quaternion;
func x - y -> Number equals
x + -y;
coherence;
end;
definition
let x be Real, y be Quaternion;
consider y1,y2,y3,y4 being Real such that
A1: y = [*y1,y2,y3,y4*] by Th2;
func x * y -> Number means
:Def20:
ex y1,y2,y3,y4 being Real st y = [*y1,y2,y3,y4*] &
it = [*x*y1,x*y2,x*y3,x*y4*];
existence
proof
take [*x*y1,x*y2,x*y3,x*y4*];
thus thesis by A1;
end;
uniqueness
proof
let c1,c2 be Number;
given y1,y2,y3,y4 being Real such that
A2: y = [*y1,y2,y3,y4*] and
A3: c1 = [*x*y1,x*y2,x*y3,x*y4*];
given y19,y29,y39,y49 being Real such that
A4: y = [*y19,y29,y39,y49*] and
A5: c2 = [*x*y19,x*y29,x*y39,x*y49*];
A6: y1 = y19 by A2,A4,Th5;
A7: y2 = y29 by A2,A4,Th5;
y3 = y39 by A2,A4,Th5;
hence thesis by A2,A3,A4,A5,A6,A7,Th5;
end;
end;
registration
let x be Real,z9 be Quaternion;
cluster x+z9 -> quaternion;
coherence
proof
ex y1,y2,y3,y4 being Real st z9 = [*y1,y2,y3,y4*] &
x+z9 = [*x+y1,y2,y3,y4*] by Def18;
hence thesis;
end;
cluster x*z9 -> quaternion;
coherence
proof
ex y1,y2,y3,y4 being Real st z9 = [*y1,y2,y3,y4*] &
x*z9 = [*x*y1,x*y2,x*y3,x*y4*] by Def20;
hence x*z9 in QUATERNION;
end;
cluster x-z9 -> quaternion;
coherence;
end;
Lm19: for x,y,z,w being Real
holds [*x,y,z,w*] = x + y*<i> + z*<j> + w*<k>
proof
let x,y,z,w be Real;
<i> = [*zz,jj,zz,zz*] by Lm2,Lm3; then
A1: y*<i> = [*y*0,y*1,y*0,y*0*] by Def20
.= [*0,y,0,0*];
A2: z*<j> = [*z*0,z*0,z*1,y*0*] by Def20
.= [*0,0,z,0*];
A3: w*<k> = [*w*0,w*0,w*0,w*1*] by Def20
.= [*0,0,0,w*];
x + y* <i> = [*x+0,y,0,0*] by A1,Def18
.= [*x,y,0,0*];
then x + y*<i> + z*<j> = [*x+0,y+0,0+z,0+0*] by A2,Def6
.= [*x,y,z,0*];
then x + y*<i> + z*<j> + w*<k> = [*x+0,y+0,0+z,0+w*] by A3,Def6;
hence thesis;
end;
definition
let z1,z2 be Quaternion;
redefine func z1 + z2 -> Element of QUATERNION; :: redefines + (QUATERNI, definition)
coherence by Def2;
end;
Lm20: z1+z2 = Rea z1 + Rea z2 + (Im1 z1 + Im1 z2)*<i> +
(Im2 z1 + Im2 z2)*<j> + (Im3 z1 + Im3 z2)*<k>
proof
z1 + z2 = [* Rea z1 + Rea z2, Im1 z1 + Im1 z2,
Im2 z1 + Im2 z2, Im3 z1 + Im3 z2 *] by Lm13;
hence thesis by Lm19;
end;
theorem Th29:
Rea (z1 + z2) = Rea z1 + Rea z2 & Im1(z1 + z2) = Im1 z1 + Im1 z2 &
Im2 (z1 + z2) = Im2 z1 + Im2 z2 & Im3(z1 + z2) = Im3 z1 + Im3 z2
proof
(z1 + z2) = [* Rea z1 + Rea z2, Im1 z1 + Im1 z2,
Im2 z1 + Im2 z2, Im3 z1 + Im3 z2*] by Lm13;
hence thesis by Th16;
end;
definition
let z1,z2 be Quaternion;
redefine func z1 * z2 -> Element of QUATERNION; :: redefines * (QUATERNI, definition)
coherence by Def2;
end;
Lm21: z1*z2 =
(Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2) +
(Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2)*<i> +
(Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2) *<j> +
(Rea z1 * Im3 z2 + Im3 z1 * Rea z2 + Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2)*<k>
proof
z1 * z2 =
[* Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2,
Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2,
Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1* Im1 z2 - Im1 z1* Im3 z2,
Rea z1 * Im3 z2 + Im3 z1 * Rea z2 + Im1 z1 * Im2 z2 - Im2 z1* Im1 z2 *]
by Lm16;
hence thesis by Lm19;
end;
theorem
z = Rea z+(Im1 z)*<i> + (Im2 z)*<j> + (Im3 z)*<k>
proof
[*Rea z, Im1 z, Im2 z, Im3 z*] = z by Th17;
hence thesis by Lm19;
end;
Lm22: for c be Quaternion holds c + 0q = c
proof
let c be Quaternion;
A1: 0q = [*In(0,REAL),In(0,REAL)*] by ARYTM_0:def 5
.= [*0,0,0,0*] by Lm3;
consider x,y,w,z be Real such that
A2: c = [*x,y,w,z*] by Th2;
c + 0q = [* x+0,y+0,w+0,z+0 *] by A1,A2,Def6
.= [*x,y,w,z*];
hence thesis by A2;
end;
Lm23: 0*<i> = 0 & 0*<j> = 0 & 0*<k> = 0
proof
set z1 = 0, z2 = <i>;
consider y1,y2,y3,y4 being Real such that
A1: <i> = [*y1,y2,y3,y4*] &
z1*z2 = [*z1*y1,z1*y2,z1*y3,z1*y4*] by Def20;
A2: z1*z2 = [*In(0,REAL),In(0,REAL)*] by A1,Lm3 .= 0 by ARYTM_0:def 5;
consider y1,y2,y3,y4 being Real such that
A3: <j> = [*y1,y2,y3,y4*] &
z1*<j> = [*z1*y1,z1*y2,z1*y3,z1*y4*] by Def20;
A4: z1*<j> = [*In(0,REAL),In(0,REAL)*] by A3,Lm3 .= 0 by ARYTM_0:def 5;
consider y1,y2,y3,y4 being Real such that
A5: <k> = [*y1,y2,y3,y4*] &
z1*<k> = [*z1*y1,z1*y2,z1*y3,z1*y4*] by Def20;
z1*<k> = [*In(0,REAL),In(0,REAL)*] by A5,Lm3 .= 0 by ARYTM_0:def 5;
hence thesis by A2,A4;
end;
theorem
Im1 z1 = 0 & Im1 z2 = 0 & Im2 z1 = 0 & Im2 z2 = 0 &
Im3 z1 = 0 & Im3 z2 = 0 implies Rea(z1*z2) = Rea z1 * Rea z2 &
Im1(z1*z2) = Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2 &
Im2(z1*z2) = Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2 &
Im3(z1*z2) = Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2
proof
assume A1: Im1 z1 = 0 & Im1 z2 = 0 & Im2 z1 = 0 & Im2 z2 = 0 &
Im3 z1 = 0 & Im3 z2 = 0;
A2: z1*z2 =
(Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2) +
(Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2)*<i> +
(Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2)*<j> +
(Rea z1 * Im3 z2 + Im3 z1 * Rea z2 + Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2)*<k>
by Lm21
.= Rea z1 * Rea z2 + 0q + 0q by Lm22,Lm23,A1
.= (Rea z1 * Rea z2) + 0q by Lm22;
consider y1,y2,y3,y4 being Real such that
A3: 0q = [*y1,y2,y3,y4*] &
(Rea z1 * Rea z2) + 0q = [*(Rea z1 * Rea z2)+y1,y2,y3,y4*] by Def18;
reconsider RR = Rea z1 * Rea z2, zz = 0 as Element of REAL
by XREAL_0:def 1;
y1 = 0 & y2 = 0 & y3 = 0 & y4 = 0 by Th5,A3,Lm6; then
(Rea z1 * Rea z2) + 0q = [*RR,zz*] by A3,Lm3; then
(Rea z1 * Rea z2) + 0q = Rea z1 * Rea z2 by ARYTM_0:def 5;
hence thesis by Lm18,A2,A1;
end;
theorem
Rea z1 = 0 & Rea z2 = 0 implies
Rea(z1*z2) = - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2 &
Im1(z1*z2) = Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2 &
Im2(z1*z2) = Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2 &
Im3(z1*z2) = Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2
proof
assume A1: Rea z1 = 0 & Rea z2 = 0;
Rea (z1 * z2) =
Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2 &
Im1 (z1 * z2) =
Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2 &
Im2 (z1 * z2) =
Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2 &
Im3 (z1 * z2) =
Rea z1 * Im3 z2 + Im3 z1 * Rea z2 + Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2
by Lm17;
hence thesis by A1;
end;
theorem
Rea(z*z) = (Rea z)^2 - (Im1 z)^2 - (Im2 z)^2 - (Im3 z)^2 &
Im1(z*z) = 2*(Rea z * Im1 z) & Im2(z*z) = 2*( Rea z * Im2 z) &
Im3(z*z) = 2*(Rea z * Im3 z)
proof
Rea (z * z) =
Rea z * Rea z - Im1 z * Im1 z - Im2 z * Im2 z - Im3 z * Im3 z &
Im1 (z * z) =
Rea z * Im1 z + Im1 z * Rea z + Im2 z * Im3 z - Im3 z * Im2 z &
Im2 (z * z) =
Rea z * Im2 z + Im2 z * Rea z + Im3 z * Im1 z - Im1 z * Im3 z &
Im3 (z * z) =
Rea z * Im3 z + Im3 z * Rea z + Im1 z * Im2 z - Im2 z * Im1 z by Lm17;
hence thesis;
end;
definition
let z be Quaternion;
redefine func -z -> Element of QUATERNION; :: redefines - (QUATERNI, definition)
coherence by Def2;
end;
Lm24: -z = -Rea z + (-Im1 z)*<i> + (-Im2 z)*<j> + (-Im3 z)*<k>
proof
set z9 = [* -Rea z, -Im1 z, -Im2 z, -Im3 z *];
A1: z9 = -Rea z+(-Im1 z)*<i> + (-Im2 z)*<j> + (-Im3 z)*<k> by Lm19;
z9 + z =
[* Rea z9 + Rea z, Im1 z9 + Im1 z, Im2 z9 + Im2 z,Im3 z9 + Im3 z*] by Lm13
.= [* -Rea z + Rea z, Im1 z9 + Im1 z,Im2 z9 + Im2 z,Im3 z9 + Im3 z *]
by Th16
.= [* 0, - Im1 z + Im1 z,Im2 z9 + Im2 z,Im3 z9 + Im3 z *] by Th16
.= [* 0, 0,- Im2 z + Im2 z,Im3 z9 + Im3 z *] by Th16
.= [* 0, 0,0,-Im3 z + Im3 z *] by Th16
.= 0 by Lm6;
hence thesis by A1,Def7;
end;
theorem Th34:
Rea(-z) = -(Rea z) & Im1(-z) = -(Im1 z) & Im2(-z) = -(Im2 z) &
Im3(-z) = -(Im3 z)
proof
-z = -Rea z + (-Im1 z)*<i> + (-Im2 z)*<j> + (-Im3 z)*<k> by Lm24; then
-z = [*-Rea z,-Im1 z,-Im2 z,-Im3 z*] by Lm19;
hence thesis by Th16;
end;
definition
let z1,z2 be Quaternion;
redefine func z1 - z2 -> Element of QUATERNION; :: redefines - (QUATERNI, definition)
coherence by Def2;
end;
Lm25: z1 - z2 = Rea z1 - Rea z2 + (Im1 z1 - Im1 z2)*<i> +
(Im2 z1 - Im2 z2)*<j> + (Im3 z1 - Im3 z2)*<k>
proof
z1 - z2 = Rea z1 + Rea (-z2) + (Im1 z1 + Im1 (-z2))*<i> +
(Im2 z1 + Im2 (-z2))*<j> + (Im3 z1 + Im3 (-z2))*<k> by Lm20
.= Rea z1 + -Rea z2 + (Im1 z1 + Im1 (-z2))*<i> +
(Im2 z1 + Im2 (-z2))*<j> + (Im3 z1 + Im3 (-z2))*<k> by Th34
.= Rea z1 + -Rea z2 + (Im1 z1 - Im1 z2)*<i> +
(Im2 z1 + Im2 (-z2))*<j> + (Im3 z1 + Im3 (-z2))*<k> by Th34
.= Rea z1 + -Rea z2 + (Im1 z1 - Im1 z2)*<i> +
(Im2 z1 + -Im2 z2)*<j> + (Im3 z1 + Im3 (-z2))*<k> by Th34
.= (Rea z1 - Rea z2) + (Im1 z1 - Im1 z2)*<i> +
(Im2 z1 - Im2 z2)*<j> + (Im3 z1 - Im3 z2)*<k> by Th34;
hence thesis;
end;
theorem Th35:
Rea(z1 - z2) = Rea z1 - Rea z2 & Im1(z1 - z2) = Im1 z1 - Im1 z2 &
Im2(z1 - z2) = Im2 z1 - Im2 z2 & Im3(z1 - z2) = Im3 z1 - Im3 z2
proof
z1 - z2 = Rea z1 - Rea z2 + (Im1 z1 - Im1 z2)*<i> +
(Im2 z1 - Im2 z2)*<j> + (Im3 z1 - Im3 z2)*<k> by Lm25; then
z1 - z2 = [*Rea z1 - Rea z2, Im1 z1 - Im1 z2,
Im2 z1 - Im2 z2, Im3 z1 - Im3 z2*] by Lm19;
hence thesis by Th16;
end;
definition
let z be Quaternion;
func z*' -> Quaternion equals
Rea z + (-Im1 z)*<i> + (-Im2 z)*<j> + (-Im3 z)*<k>;
coherence;
end;
definition
let z be Quaternion;
redefine func z*' -> Element of QUATERNION; :: redefines *' (QUATERNI, definition)
coherence;
end;
theorem Th36:
z*' = [*Rea z, -Im1 z, -Im2 z, -Im3 z*]
proof
<i> = [*zz,jj,zz,zz*] by Lm2,Lm3;
then z*'= Rea z + [*(-Im1 z)*0,(-Im1 z) *1,(-Im1 z) *0,(-Im1 z) *0 *]
+ (-Im2 z)*<j> + (-Im3 z)*<k> by Def20
.= Rea z + [*0,-Im1 z,0,0 *] +
[*(-Im2 z)*0,(-Im2 z)*0,(-Im2 z)*1,(-Im2 z)*0*] + (-Im3 z)*<k> by Def20
.= Rea z + [*0,-Im1 z,0,0 *] + [*0,0,(-Im2 z),0*] +
[*(-Im3 z)*0,(-Im3 z)*0,(-Im3 z)*0,(-Im3 z)*1*] by Def20
.= [*Rea z+0,-Im1 z,0,0 *] + [*0,0,(-Im2 z),0*]
+ [*0,0,0,(-Im3 z)*] by Def18
.= [*Rea z+0,-Im1 z+0,0+(-Im2 z),0+0*] + [*0,0,0,(-Im3 z)*] by Def6
.= [*Rea z+0,-Im1 z+0,-Im2 z+0,0+(-Im3 z)*] by Def6;
hence thesis;
end;
theorem
Rea (z*') = Rea z & Im1 (z*') = -Im1 z &
Im2 (z*') = -Im2 z & Im3 (z*') = -Im3 z
proof
z*' = [*Rea z, -Im1 z, -Im2 z, -Im3 z*] by Lm19;
hence thesis by Th16;
end;
theorem
z = 0 implies z*' = 0
proof
assume
A1: z = 0; then
A2: Rea z = 0 by Lm6,Th16;
A3: Im1 z = 0 by A1,Lm6,Th16;
A4: Im2 z = 0 by A1,Lm6,Th16;
Im3 z = 0 by A1,Lm6,Th16;
hence thesis by A2,A3,A4,Lm6,Th36;
end;
theorem
z*' = 0 implies z = 0
proof
assume
A1: z*' = 0;
A2: z*' = [*Rea z, -Im1 z, -Im2 z, -Im3 z*] by Th36;
A3: Rea z*' = 0 by A1,Lm6,Th16;
A4: Im1 z*' = 0 by A1,Lm6,Th16;
A5: Im2 z*'= 0 by A1,Lm6,Th16;
A6: Im3 z*' = 0 by A1,Lm6,Th16;
A7: Rea z*' = Rea z by A2,Th16;
A8: Im1 z*' = -Im1 z by A2,Th16;
A9: Im2 z*'= -Im2 z by A2,Th16;
Im3 z*' = -Im3 z by A2,Th16;
hence thesis by A3,A4,A5,A6,A7,A8,A9,Th19;
end;
theorem
1q*' = 1q
proof
[*jj,zz*] = [*1,0,0,0*] by Lm3; then
A1: 1q= [*1,0,0,0*] by ARYTM_0:def 5;
A2: Rea [*jj,zz,zz,zz*] = 1 by Th16;
A3: Im1 [*jj,zz,zz,zz*] = 0 by Th16;
A4: Im2 [*jj,zz,zz,zz*] = 0 by Th16;
Im3 [*jj,zz,zz,zz*] = 0 by Th16;
hence thesis by A1,A2,A3,A4,Th36;
end;
theorem
Rea (<i>*') = 0 & Im1 (<i>*') = -1 & Im2 (<i>*') = 0 & Im3 (<i>*') = 0
proof
<i>*' = [*zz, -jj, zz, zz*] by Th23,Th36;
hence thesis by Th16;
end;
theorem
Rea (<j>*') = 0 & Im1 (<j>*') = 0 & Im2 (<j>*') = -1 & Im3 (<j>*') = 0
proof
<j>*' = [*zz,zz,-jj,zz*] by Th24,Th36;
hence thesis by Th16;
end;
theorem
Rea (<k>*') = 0 & Im1 (<k>*') = 0 & Im2 (<k>*') = 0 & Im3 (<k>*') = -1
proof
<k>*' = [*zz,zz,zz,-jj*] by Th24,Th36;
hence thesis by Th16;
end;
theorem
<i>*' = -<i> by Th23,Lm24;
theorem
<j>*' = -<j> by Th24,Lm24;
theorem
<k>*' = -<k> by Th24,Lm24;
theorem
(z1 + z2)*' = z1*' + z2*'
proof
A1: z1*' = [*Rea z1, -Im1 z1, -Im2 z1, -Im3 z1*] by Th36;
A2: z2*' = [*Rea z2, -Im1 z2, -Im2 z2, -Im3 z2*] by Th36;
A3: (z1+z2)*' = [*Rea (z1+z2), -Im1 (z1+z2), -Im2 (z1+z2), -Im3 (z1+z2)*]
by Th36;
z1*' + z2*' = [* Rea z1 + Rea z2, - Im1 z1 + - Im1 z2,
- Im2 z1 + - Im2 z2, - Im3 z1 + - Im3 z2*] by A1,A2,Def6
.= [* Rea (z1 + z2), - (Im1 z1 + Im1 z2),
- (Im2 z1 + Im2 z2), - (Im3 z1 + Im3 z2)*] by Th29
.= [* Rea (z1 + z2), - Im1 (z1 + z2),
- (Im2 z1 + Im2 z2), - (Im3 z1 + Im3 z2)*] by Th29
.= [* Rea (z1 + z2), - Im1 (z1 + z2),
- Im2 (z1+z2), - (Im3 z1 + Im3 z2)*] by Th29;
hence thesis by A3,Th29;
end;
theorem Th48:
(-z)*' = -(z*')
proof
A1: z*' = [*Rea z, -Im1 z, -Im2 z, -Im3 z*] by Th36;
(-z)*' = [*Rea (-z), -Im1 (-z), -Im2 (-z), -Im3 (-z)*] by Th36;
then (-z)*' = [*-Rea z, -Im1 (-z), -Im2 (-z), -Im3 (-z)*] by Th34
.= [*-Rea z, - - Im1 z, -Im2 (-z), -Im3 (-z)*] by Th34
.= [*-Rea z, Im1 z, - - Im2 z, -Im3 (-z)*] by Th34
.= [*-Rea z, Im1 z, Im2 z, - -Im3 z*] by Th34
.= [*-Rea z, Im1 z, Im2 z, Im3 z*];
then z*' + (-z)*' = [*Rea z+ -Rea z, -Im1 z+ Im1 z,
-Im2 z+ Im2 z, -Im3 z+Im3 z*] by A1,Def6 .= 0 by Lm6;
hence thesis by Def7;
end;
theorem
(z1 - z2)*' = z1*' - z2*'
proof
A1: z1*' = [*Rea z1, -Im1 z1, -Im2 z1, -Im3 z1*] by Th36;
A2: (-z2)*' = [*Rea (-z2), -Im1 (-z2), -Im2 (-z2), -Im3 (-z2)*] by Th36;
A3: (z1-z2)*' = [*Rea (z1-z2), -Im1 (z1-z2), -Im2 (z1-z2), -Im3 (z1-z2)*]
by Th36;
A4: z1*' - z2*' = z1*' + (- z2)*' by Th48
.= [*Rea z1+Rea (-z2), -Im1 z1+ -Im1(-z2),
-Im2 z1+ - Im2 (-z2), -Im3 z1+ - Im3 (-z2)*] by A1,A2,Def6
.= [*Rea z1+- Rea z2, -Im1 z1+ -Im1(-z2),
-Im2 z1+ - Im2 (-z2), -Im3 z1+ - Im3 (-z2)*] by Th34
.= [*Rea z1- Rea z2, -Im1 z1- - Im1 z2,
-Im2 z1+ - Im2 (-z2), -Im3 z1+ - Im3 (-z2)*] by Th34
.= [*Rea z1- Rea z2, -Im1 z1+ Im1 z2,
-Im2 z1 - - Im2 z2, -Im3 z1+ - Im3 (-z2)*] by Th34
.= [*Rea z1- Rea z2, -Im1 z1+ Im1 z2,
-Im2 z1 + Im2 z2, -Im3 z1 - -Im3 z2*] by Th34
.= [*Rea z1- Rea z2, -Im1 z1+ Im1 z2, -Im2 z1 + Im2 z2, -Im3 z1 +Im3 z2*];
(z1-z2)*' = [*Rea z1-Rea z2, -Im1 (z1-z2), -Im2 (z1-z2), -Im3 (z1-z2)*]
by A3,Th35
.= [*Rea z1-Rea z2, -(Im1 z1- Im1 z2), -Im2 (z1-z2), -Im3 (z1-z2)*]
by Th35
.= [*Rea z1-Rea z2, -Im1 z1+ Im1 z2,
-(Im2 z1- Im2 z2), -Im3 (z1-z2)*] by Th35
.= [*Rea z1-Rea z2, -Im1 z1+ Im1 z2,
-Im2 z1+ Im2 z2, -(Im3 z1- Im3 z2)*] by Th35;
hence thesis by A4;
end;
theorem
(z1*z2)*' = z1*' * z2*' implies (Im2 z1 * Im3 z2) = (Im3 z1)*(Im2 z2)
proof
assume
A1: (z1*z2)*' = z1*' * z2*';
A2: z1*' = [*Rea z1, -Im1 z1, -Im2 z1, -Im3 z1*] by Th36;
A3: z2*' = [*Rea z2, -Im1 z2, -Im2 z2, -Im3 z2*] by Th36;
A4: (z1*z2)*' = [*Rea (z1*z2), -Im1 (z1*z2), -Im2 (z1*z2), -Im3 (z1*z2)*]
by Th36;
A5: z1*' * z2*' = [*(Rea z1)*(Rea z2) - (- Im1 z1)*(- Im1 z2) -
(- Im2 z1)*(- Im2 z2) - (-Im3 z1)*(-Im3 z2),
(Rea z1)*(- Im1 z2) + (- Im1 z1)*(Rea z2) +
(- Im2 z1)*(-Im3 z2) - (-Im3 z1)*(- Im2 z2),
(Rea z1)*(- Im2 z2) + (Rea z2)*(- Im2 z1) +
(- Im1 z2)*(-Im3 z1) - (-Im3 z2)*(- Im1 z1),
(Rea z1)*(-Im3 z2) + (-Im3 z1)*(Rea z2) +
(- Im1 z1)*(- Im2 z2) - (- Im2 z1)*(- Im1 z2) *] by A2,A3,Def9
.= [*(Rea z1)*(Rea z2) - (Im1 z1)*(Im1 z2) -
(Im2 z1)*(Im2 z2) - (Im3 z1)*(Im3 z2),
-(Rea z1)*( Im1 z2) - ( Im1 z1)*(Rea z2) +
(Im2 z1)*(Im3 z2) - (Im3 z1)*(Im2 z2),
-(Rea z1)*(Im2 z2) - (Rea z2)*(Im2 z1) +
(Im1 z2)*(Im3 z1) - (Im3 z2)*(Im1 z1),
-(Rea z1)*(Im3 z2) - (Im3 z1)*(Rea z2) +
(Im1 z1)*(Im2 z2) - (Im2 z1)*(Im1 z2) *];
A6: (z1*z2)*' =
[*Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2,
-Im1 (z1*z2), -Im2 (z1*z2), -Im3 (z1*z2)*] by A4,Lm17
.=[*Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2,
-(Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2),
-Im2 (z1*z2), -Im3 (z1*z2)*] by Lm17
.=[*Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2,
-(Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2),
-(Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2),
-Im3 (z1*z2)*] by Lm17
.=[*Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2,
-(Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2),
-(Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2),
-(Rea z1 * Im3 z2 + Im3 z1 * Rea z2 + Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2)*]
by Lm17
.=[*Rea z1 * Rea z2 - (Im1 z1 * Im1 z2) -
(Im2 z1 * Im2 z2) - (Im3 z1 * Im3 z2),
-(Rea z1 * Im1 z2) - (Im1 z1 * Rea z2) -
(Im2 z1 * Im3 z2) + (Im3 z1 * Im2 z2),
-(Rea z1 * Im2 z2) - (Im2 z1 * Rea z2) -
(Im3 z1 * Im1 z2) + (Im1 z1 * Im3 z2),
-(Rea z1 * Im3 z2) - (Im3 z1 * Rea z2) -
(Im1 z1 * Im2 z2) + (Im2 z1 * Im1 z2)*];
A7: Im1 (z1*' * z2*') = -(Rea z1)*( Im1 z2) - ( Im1 z1)*(Rea z2) +
(Im2 z1)*(Im3 z2) - (Im3 z1)*(Im2 z2) by A5,Th16;
Im1(z1*z2)*' = -(Rea z1 * Im1 z2) - (Im1 z1 * Rea z2) -
(Im2 z1 * Im3 z2) + (Im3 z1 * Im2 z2) by A6,Th16;
hence thesis by A1,A7;
end;
theorem
Im1 z = 0 & Im2 z = 0 & Im3 z = 0 implies z*' = z
proof
assume that
A1: Im1 z = 0 and
A2: Im2 z = 0 and
A3: Im3 z = 0;
reconsider Rz = Rea z, zz = 0 as Element of REAL by XREAL_0:def 1;
A4: z = [*Rea z,0,0,0*] by A1,A2,A3,Th17
.= [*Rz,zz*] by Lm3
.= Rea z by ARYTM_0:def 5;
z*' = [*Rea z, 0,0,0*] by A1,A2,A3,Th36
.= [*Rz, zz*] by Lm3
.= Rea z by ARYTM_0:def 5;
hence thesis by A4;
end;
theorem
Rea z = 0 implies z*' = -z
proof
assume A1: Rea z = 0;
-z = -Rea z + (-Im1 z)*<i> + (-Im2 z)*<j> + (-Im3 z)*<k> by Lm24;
hence thesis by A1;
end;
theorem
Rea(z*z*') = (Rea z)^2+(Im1 z)^2+(Im2 z)^2+(Im3 z)^2 &
Im1(z*z*') = 0 & Im2(z*z*') = 0 & Im3(z*z*') = 0
proof
A1: z = [*Rea z, Im1 z, Im2 z, Im3 z*] by Th17;
z*' = [*Rea z, -Im1 z, -Im2 z, -Im3 z*] by Th36;
then z*z*' = [* Rea z*Rea z-(Im1 z)*(-Im1 z)-Im2 z*(-Im2 z)-(Im3 z)*(-Im3
z), Rea z*(-Im1 z)+Im1 z*Rea z+Im2 z*(-Im3 z)-(Im3 z)*(-Im2 z),
Rea z*(-Im2 z)+Rea z*Im2 z+(-Im1 z)*(Im3 z)-(-Im3 z)*Im1 z,
Rea z*(-Im3 z)+(Im3 z)*Rea z+Im1 z*(-Im2 z)-Im2 z*(-Im1 z) *] by A1,Def9
.= [* (Rea z)^2+(Im1 z)^2+(Im2 z)^2+(Im3 z)^2,0,0,0 *];
hence thesis by Th16;
end;
theorem
Rea(z + z*') = 2*Rea z & Im1(z + z*') = 0 &
Im2(z + z*') = 0 & Im3(z + z*') = 0
proof
A1: z = [*Rea z, Im1 z, Im2 z, Im3 z*] by Th17;
z*' = [*Rea z, -Im1 z, -Im2 z, -Im3 z*] by Th36;
then z + z*' = [*Rea z+Rea z, Im1 z+ -Im1 z, Im2 z+ -Im2 z, Im3 z+ -Im3 z*]
by A1,Def6
.=[*2*Rea z,0,0,0*];
hence thesis by Th16;
end;
theorem Th55:
-z = [*-Rea z, -Im1 z, -Im2 z, -Im3 z*]
proof
A1: z = [*Rea z, Im1 z, Im2 z, Im3 z*] by Th17;
set z9 = [*-Rea z, -Im1 z, -Im2 z, -Im3 z*];
z + z9 = [*Rea z+ -Rea z, Im1 z+ -Im1 z, Im2 z+ -Im2 z, Im3 z+ -Im3 z*]
by A1,Def6
.= 0 by Lm6;
hence thesis by Def7;
end;
theorem
z1 - z2 =
[*Rea z1 - Rea z2, Im1 z1 - Im1 z2, Im2 z1 - Im2 z2, Im3 z1 - Im3 z2*]
proof
A1: z1 = [*Rea z1, Im1 z1, Im2 z1, Im3 z1*] by Th17;
A2: z2 = [*Rea z2, Im1 z2, Im2 z2, Im3 z2*] by Th17;
set z9 = [*-Rea z2, -Im1 z2, -Im2 z2, -Im3 z2*];
z2 + z9 = [*Rea z2+ -Rea z2, Im1 z2+ -Im1 z2,
Im2 z2+ -Im2 z2, Im3 z2+ -Im3 z2*] by A2,Def6
.= 0 by Lm6;
then -z2 = [*-Rea z2, -Im1 z2, -Im2 z2, -Im3 z2*] by Def7;
hence thesis by A1,Def6;
end;
theorem
Rea(z - z*') = 0 & Im1(z - z*') = 2*Im1 z &
Im2(z - z*') = 2*Im2 z & Im3(z - z*') = 2*Im3 z
proof
A1: z = [*Rea z, Im1 z, Im2 z, Im3 z*] by Th17;
A2: z*' = [*Rea z, -Im1 z, -Im2 z, -Im3 z*] by Th36;
A3: Im1 z*' = - Im1 z by A2,Th16;
A4: Im2 z*' = - Im2 z by A2,Th16;
A5: Im3 z*' = - Im3 z by A2,Th16;
set zz = z*';
-zz = [*-Rea zz, -Im1 zz, -Im2 zz, -Im3 zz*] by Th55;
then -zz = [*-Rea z,Im1 z,Im2 z,Im3 z*] by A2,Th16,A3,A4,A5;
then z - zz = [*Rea z+ (-Rea z), Im1 z + Im1 z, Im2 z + Im2 z, Im3 z +Im3
z *] by A1,Def6
.= [*0, 2* Im1 z, 2* Im2 z,2* Im3 z*];
hence thesis by Th16;
end;
definition let z;
func |.z.| -> Real equals
sqrt ((Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z)^2);
coherence;
end;
theorem Th58:
|.0q.| = 0
proof
A1: Rea 0q = 0 by Lm6,Th16;
A2: Im1 0q = 0 by Lm6,Th16;
Im2 0q = 0 by Lm6,Th16;
hence thesis by A1,A2,Lm6,Th16,SQUARE_1:17;
end;
theorem Th59:
|.z.| = 0 implies z = 0
proof
assume
A1: |.z.| = 0;
A2: 0 <= (Rea z)^2 by XREAL_1:63;
A3: 0 <= (Im1 z)^2 by XREAL_1:63;
A4: 0 <= (Im2 z)^2 by XREAL_1:63;
0 <= (Im3 z)^2 by XREAL_1:63; then
A5: 0 = (Rea z)^2+(Im1 z)^2+ (Im2 z)^2 + (Im3 z)^2
by A1,A2,A3,A4,SQUARE_1:25; then
A6: Rea z = 0 by Lm9;
A7: Im1 z = 0 by A5,Lm9;
A8: Im2 z = 0 by A5,Lm9;
Im3 z = 0 by A5,Lm9;
hence thesis by A6,A7,A8,Lm6,Th17;
end;
theorem Th60:
0 <= |.z.|
proof
A1: 0 <= (Rea z)^2 by XREAL_1:63;
A2: 0 <= (Im1 z)^2 by XREAL_1:63;
A3: 0 <= (Im2 z)^2 by XREAL_1:63;
0 <= (Im3 z)^2 by XREAL_1:63;
hence thesis by A1,A2,A3,SQUARE_1:def 2;
end;
theorem
|.1q.| = 1
proof
A1: Rea 1q =jj by Lm10,Th16;
A2: Im1 1q = zz by Lm10,Th16;
Im2 1q = zz by Lm10,Th16;
hence thesis by A1,A2,Lm10,Th16,SQUARE_1:18;
end;
theorem
|.<i>.| = 1 by Th23;
theorem
|.<j>.| = 1 by Th24;
theorem
|.<k>.| = 1 by Th24;
theorem Th65:
|.-z.| = |.z.|
proof
A1: -z = [*-Rea z, -Im1 z, -Im2 z, -Im3 z*] by Th55;
then
A2: Rea -z = - Rea z by Th16;
A3: Im1 -z = - Im1 z by A1,Th16;
A4: Im2 -z = - Im2 z by A1,Th16;
Im3 -z = - Im3 z by A1,Th16;
hence thesis by A2,A3,A4;
end;
theorem Th66:
|.z*'.| = |.z.|
proof
A1: z*' = [*Rea z, -Im1 z, -Im2 z, -Im3 z*] by Th36; then
A2: Im1 z*' = - Im1 z by Th16;
A3: Im2 z*' = - Im2 z by A1,Th16;
Im3 z*' = - Im3 z by A1,Th16;
hence thesis by A1,A2,A3,Th16;
end;
theorem Th67:
for a,b,c,d being Real holds a^2 + b^2 + c^2 + d^2 >= 0
proof
let a,b,c,d be Real;
A1: a^2 >= 0 by XREAL_1:63;
A2: b^2>= 0 by XREAL_1:63;
A3: c^2 >= 0 by XREAL_1:63;
d^2 >= 0 by XREAL_1:63;
hence thesis by A1,A2,A3;
end;
Lm26: a^2 <= a^2 + b^2 + c^2 + d^2
proof
A1: 0 <= c^2 by XREAL_1:63;
A2: 0<= d^2 by XREAL_1:63;
a^2 <= a^2 + b^2 by XREAL_1:31,63;
then 0+a^2 <= (a^2 + b^2) + c^2 by A1,XREAL_1:7;
hence thesis by A2,XREAL_1:7;
end;
Lm27: for a, b, c, d being Real holds c^2 <= a^2 + b^2 + c^2 + d^2
proof
let a, b, c, d be Real;
A1: 0 <= b^2 by XREAL_1:63;
A2: 0 <= d^2 by XREAL_1:63;
c^2 <= a^2 + c^2 by XREAL_1:31,63;
then 0+c^2 <= (a^2 + c^2) + b^2 by A1,XREAL_1:7;
hence thesis by A2,XREAL_1:7;
end;
Lm28: d^2 <= a^2 + b^2 + c^2 + d^2
proof
A1: 0 <= b^2 by XREAL_1:63;
A2: 0 <= c^2 by XREAL_1:63;
d^2 <= a^2 + d^2 by XREAL_1:31,63;
then 0+d^2 <= (a^2 + d^2) + c^2 by A2,XREAL_1:7;
then 0+ d^2 <= b^2 + (a^2 + d^2 + c^2) by A1,XREAL_1:7;
hence thesis;
end;
Lm29: a >= b^2 implies sqrt a >= b
proof
assume
A1: a >= b^2;
b^2 >= 0 by XREAL_1:63; then
A2: sqrt a >= sqrt b^2 by A1,SQUARE_1:26;
per cases;
suppose b >= 0;
hence thesis by A2,SQUARE_1:22;
end;
suppose
A3: b < 0;
then sqrt a >= -b by A2,SQUARE_1:23;
hence thesis by A3;
end;
end;
Lm30: for a1,a2,a3,a4,a5,a6,b1,b2,b3,b4,b5,b6 being Real st
a1 >= b1 & a2 >= b2 & a3 >= b3 & a4 >= b4 & a5 >= b5 & a6 >= b6 holds
a1 + a2 + a3 + a4 + a5 + a6 >= b1 + b2 + b3 + b4 + b5 + b6
proof
let a1,a2,a3,a4,a5,a6,b1,b2,b3,b4,b5,b6 be Real;
assume that
A1: a1 >= b1 and
A2: a2 >= b2 and
A3: a3 >= b3 and
A4: a4 >= b4 and
A5: a5 >= b5 and
A6: a6 >= b6;
A7: a1+a2>=b1+b2 by A1,A2,XREAL_1:7;
A8: a3+a4 >= b3+b4 by A3,A4,XREAL_1:7;
A9: a5+a6 >= b5+b6 by A5,A6,XREAL_1:7;
(a1+a2)+(a3+a4)>=(b1+b2) + (b3+b4) by A7,A8,XREAL_1:7;
then (a1+a2)+(a3+a4)+(a5+a6)>=(b1+b2) + (b3+b4)+(b5+b6) by A9,XREAL_1:7;
hence thesis;
end;
Lm31: a>=0 & b>=0 & a^2 >= b^2 implies a >= b
proof
assume that
A1: a>=0 and
A2: b>=0 and
A3: a^2 >= b^2;
sqrt a^2 >= sqrt b^2 by A2,A3,SQUARE_1:26;
then a >= sqrt b^2 by A1,SQUARE_1:22;
hence thesis by A1,SQUARE_1:22;
end;
Lm32: for m1,m2,m4,m3,n1,n2,n3,n4 being Real holds
(sqrt (m1^2 + m2^2 + m3^2 + m4^2)+sqrt (n1^2 + n2^2 + n3^2 + n4^2))^2
= (m1^2 + m2^2 + m3^2 + m4^2 + n1^2 + n2^2 + n3^2 + n4^2)+
2*sqrt((m1^2 + m2^2 + m3^2 + m4^2) * (n1^2 + n2^2 + n3^2 + n4^2))
proof
let m1,m2,m4,m3,n1,n2,n3,n4 be Real;
set a = m1^2 + m2^2 + m3^2 + m4^2, b = n1^2 + n2^2 + n3^2 + n4^2;
A1: a >= 0 by Th67;
A2: b>= 0 by Th67;
(sqrt a + sqrt b)^2 = (sqrt a)^2 + 2*(sqrt a)*(sqrt b) + (sqrt b)^2
.= a + 2*(sqrt a)*(sqrt b) + (sqrt b)^2 by A1,SQUARE_1:def 2
.= a + 2*((sqrt a)*(sqrt b)) + b by A2,SQUARE_1:def 2
.= a + 2*sqrt (a* b) + b by A1,A2,SQUARE_1:29;
hence thesis;
end;
Lm33: for m1,m2,m3,m4,n1,n2,n3,n4 being Real holds
(sqrt ((m1 + n1)^2 + (m2+n2)^2 + (m3+n3)^2 + (m4 +n4)^2))^2
= (m1+n1)^2+(m2+n2)^2+(m3+n3)^2+(m4+n4)^2
proof
let m1,m2,m3,m4,n1,n2,n3,n4 be Real;
(m1+n1)^2+(m2+n2)^2+(m3+n3)^2+(m4+n4)^2 >= 0 by Th67;
hence thesis by SQUARE_1:def 2;
end;
theorem
Rea z <= |.z.|
proof
0 <= (Rea z)^2 by XREAL_1:63; then
A1: sqrt ((Rea z)^2) <= sqrt ((Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z )^2)
by Lm26,SQUARE_1:26;
per cases;
suppose Rea z >= 0;
hence thesis by A1,SQUARE_1:22;
end;
suppose
A2: Rea z < 0;
then - Rea z <= |.z.| by A1,SQUARE_1:23;
hence thesis by A2;
end;
end;
theorem
Im1 z <= |.z.|
proof
0 <= (Im1 z)^2 by XREAL_1:63;
then
A1: sqrt ((Im1 z)^2) <= sqrt ((Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z )^2)
by Lm26,SQUARE_1:26;
per cases;
suppose Im1 z >= 0;
hence thesis by A1,SQUARE_1:22;
end;
suppose
A2: Im1 z < 0;
then -Im1 z <= |.z.| by A1,SQUARE_1:23;
hence thesis by A2;
end;
end;
theorem
Im2 z <= |.z.|
proof
0 <= (Im2 z)^2 by XREAL_1:63;
then
A1: sqrt ((Im2 z)^2) <= sqrt ((Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z )^2)
by Lm27,SQUARE_1:26;
per cases;
suppose Im2 z >= 0;
hence thesis by A1,SQUARE_1:22;
end;
suppose
A2: Im2 z < 0;
then -Im2 z <= |.z.| by A1,SQUARE_1:23;
hence thesis by A2;
end;
end;
theorem
Im3 z <= |.z.|
proof
0<= (Im3 z)^2 by XREAL_1:63; then
A1: sqrt ((Im3 z)^2) <= sqrt ((Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z )^2)
by Lm28,SQUARE_1:26;
per cases;
suppose Im3 z >= 0;
hence thesis by A1,SQUARE_1:22;
end;
suppose
A2: Im3 z < 0;
then -Im3 z <= |.z.| by A1,SQUARE_1:23;
hence thesis by A2;
end;
end;
theorem Th72:
|.z1 + z2.| <= |.z1.| + |.z2.|
proof
set m1 = Rea z1, m2 = Im1 z1, m3 = Im2 z1, m4 = Im3 z1,
n1 = Rea z2, n2 = Im1 z2, n3 = Im2 z2, n4 = Im3 z2, a = m1^2+m2^2+m3^2+m4^2,
b = n1^2 +n2^2 + n3^2 + n4^2;
A1: |.z1.| >= 0 by Th60;
|.z2.| >= 0 by Th60; then
A2: |.z1.| + |.z2.| >= 0 by A1;
A3: (sqrt (m1^2 + m2^2 + m3^2 + m4^2)+sqrt (n1^2 + n2^2 + n3^2 + n4^2))^2
= (m1^2 + m2^2 + m3^2 + m4^2 + n1^2 + n2^2 + n3^2 + n4^2)+
2*sqrt((m1^2 + m2^2 + m3^2 + m4^2) * (n1^2 + n2^2 + n3^2 + n4^2)) by Lm32;
A4: (sqrt ((m1 + n1)^2 + ( m2+n2)^2 + (m3+n3)^2 + (m4 +n4)^2))^2
= (m1+n1)^2+(m2+n2)^2+(m3+n3)^2+(m4+n4)^2 by Lm33;
A5: Rea (z1+z2) = Rea z1 + Rea z2 by Th29;
A6: Im1 (z1+z2) = Im1 z1 + Im1 z2 by Th29;
A7: Im2 (z1+z2) = Im2 z1 + Im2 z2 by Th29;
A8: Im3 (z1+z2) = Im3 z1 + Im3 z2 by Th29;
A9: (m1*n2)^2 + (m2*n1)^2 >= 2*(m1*n2)*(m2*n1) by SERIES_3:6;
A10: (m1*n3)^2 + (m3*n1)^2 >= 2*(m1*n3)*(m3*n1) by SERIES_3:6;
A11: (m1*n4)^2 + (m4*n1)^2 >= 2*(m1*n4)*(m4*n1) by SERIES_3:6;
A12: (m2*n3)^2 + (m3*n2)^2 >= 2*(m2*n3)*(m3*n2) by SERIES_3:6;
A13: (m2*n4)^2 + (m4*n2)^2 >= 2*(m2*n4)*(m4*n2) by SERIES_3:6;
A14: (m3*n4)^2 + (m4*n3)^2 >= 2*(m3*n4)*(m4*n3) by SERIES_3:6;
set a1= (m1*n2)^2, a2= (m2*n1)^2, a3=(m1*n3)^2,a4= (m3*n1)^2,
a5= (m1*n4)^2, a6= (m4*n1)^2, a7= (m2*n3)^2, a8= (m3*n2)^2,
a9 =(m2*n4)^2, a10= (m4*n2)^2, a11= (m3*n4)^2,a12= (m4*n3)^2,
b1= 2*(m1*n2)*(m2*n1), b2= 2*(m1*n3)*(m3*n1),
b3 = 2*(m1*n4)*(m4*n1), b4= 2*(m2*n3)*(m3*n2),
b5= 2*(m2*n4)*(m4*n2), b6 =2*(m3*n4)*(m4*n3);
((a1 + a2) + (a3 + a4) + (a5 + a6)+(a7 + a8) + (a9 + a10) + (a11 + a12)) >=
b1 + b2 + b3 + b4 + b5 + b6 by A9,A10,A11,A12,A13,A14,Lm30;
then (a1 + a2 + a3 + a4 + a5 + a6+a7 + a8 + a9 + a10 + a11 + a12)
+((m1*n1)^2+(m2*n2)^2+(m3*n3)^2+(m4*n4)^2) >= (b1 + b2 + b3 + b4 + b5 + b6)
+((m1*n1)^2+(m2*n2)^2+(m3*n3)^2+(m4*n4)^2) by XREAL_1:6;
then (a1 + a2 + a3 + a4 + a5 + a6+a7 + a8 + a9 + a10 + a11 + a12 )
+((m1*n1)^2+(m2*n2)^2+(m3*n3)^2+(m4*n4)^2) >= (m1*n1+m2*n2+m3*n3+m4*n4)^2;
then sqrt ((m1^2+m2^2+m3^2+m4^2)*(n1^2+n2^2+n3^2+n4^2)) >=
m1*n1+m2*n2+m3*n3+m4*n4 by Lm29;
then 2*sqrt ((m1^2+m2^2+m3^2+m4^2)*(n1^2+n2^2+n3^2+n4^2)) >=
2*(m1*n1+m2*n2+m3*n3+m4*n4) by XREAL_1:64;
then (a+b)+2*sqrt ((m1^2+m2^2+m3^2+m4^2)*(n1^2+n2^2+n3^2+n4^2)) >=
(a+b)+2*(m1*n1+m2*n2+m3*n3+m4*n4) by XREAL_1:6;
hence thesis by A2,A3,A4,A5,A6,A7,A8,Lm31;
end;
theorem Th73:
|.z1 - z2.| <= |.z1.| + |.z2.|
proof
|.z1 - z2.| <= |.z1.| + |.-z2.| by Th72;
hence thesis by Th65;
end;
Lm34: z1 = z1+z2-z2
proof
A1: z1 = [*Rea z1, Im1 z1, Im2 z1, Im3 z1*] by Th17;
A2: z2 = [*Rea z2, Im1 z2, Im2 z2, Im3 z2*] by Th17;
A3: -z2 = [*-Rea z2, -Im1 z2, -Im2 z2, -Im3 z2*] by Th55;
z1 + z2 = [*Rea z1+ Rea z2, Im1 z1+ Im1 z2,
Im2 z1+ Im2 z2, Im3 z1+ Im3 z2*] by A1,A2,Def6;
then z1+z2-z2 = [*Rea z1+ Rea z2 -Rea z2, Im1 z1+ Im1 z2-Im1 z2,
Im2 z1+ Im2 z2-Im2 z2, Im3 z1+ Im3 z2-Im3 z2*] by A3,Def6;
hence thesis by Th17;
end;
Lm35: z1 = z1-z2+z2
proof
A1: z1 = [*Rea z1, Im1 z1, Im2 z1, Im3 z1*] by Th17;
A2: z2 = [*Rea z2, Im1 z2, Im2 z2, Im3 z2*] by Th17;
-z2 = [*-Rea z2, -Im1 z2, -Im2 z2, -Im3 z2*] by Th55;
then z1 - z2 = [*Rea z1+ -Rea z2, Im1 z1+ -Im1 z2,
Im2 z1+ -Im2 z2, Im3 z1+ -Im3 z2*] by A1,Def6;
then z1-z2+z2 = [*Rea z1+ -Rea z2 +Rea z2, Im1 z1+ -Im1 z2+ Im1 z2,
Im2 z1+ -Im2 z2+ Im2 z2, Im3 z1+ -Im3 z2+ Im3 z2*] by A2,Def6
.= [*Rea z1+ Rea z2 -Rea z2, Im1 z1+ Im1 z2-Im1 z2,
Im2 z1+ Im2 z2-Im2 z2, Im3 z1+ Im3 z2-Im3 z2*];
hence thesis by Th17;
end;
Lm36: z1-z2 = [*Rea z1-Rea z2, Im1 z1-Im1 z2, Im2 z1-Im2 z2, Im3 z1-Im3 z2*]
proof
A1: z1 = [*Rea z1, Im1 z1, Im2 z1, Im3 z1*] by Th17;
-z2 = [*-Rea z2, -Im1 z2, -Im2 z2, -Im3 z2*] by Th55;
hence thesis by A1,Def6;
end;
Lm37: z1-z2 = -(z2 - z1)
proof
A1: Rea (z2 - z1) = Rea z2 - Rea z1 by Th35;
A2: Im1 (z2 - z1) = Im1 z2 - Im1 z1 by Th35;
A3: Im2 (z2 - z1) = Im2 z2 - Im2 z1 by Th35;
A4: Im3 (z2 - z1) = Im3 z2 - Im3 z1 by Th35;
A5: Rea (-(z2 - z1)) = -(Rea z2 - Rea z1) by A1,Th34;
A6: Im1 (-(z2 - z1)) = -(Im1 z2 - Im1 z1) by A2,Th34;
A7: Im2 (-(z2 - z1)) = -(Im2 z2 - Im2 z1) by A3,Th34;
A8: Im3 (-(z2 - z1)) = -(Im3 z2 - Im3 z1) by A4,Th34;
A9: Rea (z1 - z2) = Rea z1 - Rea z2 by Th35;
A10: Im1 (z1 - z2) = Im1 z1 - Im1 z2 by Th35;
A11: Im2 (z1 - z2) = Im2 z1 - Im2 z2 by Th35;
Im3 (z1 - z2) = Im3 z1 - Im3 z2 by Th35;
hence thesis by Th18,A9,A10,A11,A5,A6,A7,A8;
end;
Lm38: z1 - z2 = 0 implies z1 = z2
proof
assume
A1: z1 - z2 = 0;
A2: Rea (z1 - z2) = Rea z1 - Rea z2 by Th35;
A3: Im1 (z1 - z2) = Im1 z1 - Im1 z2 by Th35;
A4: Im2 (z1 - z2) = Im2 z1 - Im2 z2 by Th35;
A5: Im3 (z1 - z2) = Im3 z1 - Im3 z2 by Th35;
A6: Rea (z1 - z2) = 0 by A1,Lm6,Th16;
A7: Im1 (z1 - z2) = 0 by A1,Lm6,Th16;
A8: Im2 (z1 - z2) = 0 by A1,Lm6,Th16;
Im3 (z1 - z2) = 0 by A1,Lm6,Th16;
hence thesis by A2,A3,A4,A5,A6,A7,A8,Th18;
end;
theorem
|.z1.| - |.z2.| <= |.z1 + z2.|
proof z1 = z1 + z2 - z2 by Lm34;
then |.z1.| <= |.z1 + z2.| + |.z2.| by Th73;
hence thesis by XREAL_1:20;
end;
theorem Th75:
|.z1.| - |.z2.| <= |.z1 - z2.|
proof z1 = z1 - z2 + z2 by Lm35;
then |.z1.| <= |.z1 - z2.| + |.z2.| by Th72;
hence thesis by XREAL_1:20;
end;
theorem Th76:
|.z1 - z2.| = |.z2 - z1.|
proof
thus |.z1 - z2.| = |.-(z2 - z1).| by Lm37
.= |.z2 - z1.| by Th65;
end;
theorem
|.z1 - z2.| = 0 iff z1 = z2
proof
thus |.z1 - z2.| = 0 implies z1 = z2 by Lm38,Th59;
assume z1 = z2; then
z1 - z2 = [*Rea z1-Rea z1, Im1 z1-Im1 z1, Im2 z1-Im2 z1, Im3 z1-Im3 z1*]
by Lm36
.= 0 by Lm6;
hence thesis by Th58;
end;
Lm39: for z,z1,z2 being Quaternion holds z1-z2 = (z1 - z) + (z - z2)
proof
let z,z1,z2 be Quaternion;
A1: Rea ((z1 - z) + (z - z2)) = Rea (z1 - z) + Rea (z - z2) by Lm12
.= Rea (z1 - z) + (Rea z - Rea z2) by Th35
.= (Rea z1 - Rea z) + (Rea z - Rea z2) by Th35
.= Rea z1 - Rea z2
.= Rea (z1 - z2) by Th35;
A2: Im1 ((z1 - z) + (z - z2)) = Im1 (z1 - z) + Im1 (z - z2) by Lm12
.= Im1 (z1 - z) + (Im1 z - Im1 z2) by Th35
.= (Im1 z1 - Im1 z) + (Im1 z - Im1 z2) by Th35
.= Im1 z1 - Im1 z2
.= Im1 (z1 - z2) by Th35;
A3: Im2 ((z1 - z) + (z - z2)) = Im2 (z1 - z) + Im2 (z - z2) by Lm12
.= Im2 (z1 - z) + (Im2 z - Im2 z2) by Th35
.= (Im2 z1 - Im2 z) + (Im2 z - Im2 z2) by Th35
.= Im2 z1 - Im2 z2
.= Im2 (z1 - z2) by Th35;
Im3 ((z1 - z) + (z - z2)) = Im3 (z1 - z) + Im3 (z - z2) by Lm12
.= Im3 (z1 - z) + (Im3 z - Im3 z2) by Th35
.= (Im3 z1 - Im3 z) + (Im3 z - Im3 z2) by Th35
.= Im3 z1 - Im3 z2
.= Im3 (z1 - z2) by Th35;
hence thesis by A1,A2,A3,Th18;
end;
theorem
|.z1 - z2.| <= |.z1 - z.| + |.z - z2.|
proof
|.z1 - z2.| = |.(z1 - z) + (z - z2).| by Lm39;
hence thesis by Th72;
end;
theorem
|.|.z1.| - |.z2.|.| <= |.z1 - z2.|
proof
|.z2.| - |.z1.| <= |.z2 - z1.| by Th75;
then -(|.z1.| - |.z2.|) <= |.z1 - z2.| by Th76; then
A1: -|.z1 - z2.| <= --(|.z1.| - |.z2.|) by XREAL_1:24;
|.z1.| - |.z2.| <= |.z1 - z2.| by Th75;
hence thesis by A1,ABSVALUE:5;
end;
theorem Th80:
|.z1*z2.| = |.z1.|*|.z2.|
proof
set m1 = Rea z1, m2 = Im1 z1, m3 = Im2 z1, m4 = Im3 z1,
n1 = Rea z2, n2 = Im1 z2, n3 = Im2 z2, n4 = Im3 z2;
A1: Rea (z1 * z2) = m1*n1 - m2*n2 - m3*n3 - m4*n4 by Lm17;
A2: Im1 (z1 * z2) = m1*n2 + m2*n1 + m3*n4 - m4*n3 by Lm17;
A3: Im2 (z1 * z2) = m1*n3 + m3*n1 + m4*n2 - m2*n4 by Lm17;
A4: Im3 (z1 * z2) = m1*n4 + m4*n1 + m2*n3 - m3*n2 by Lm17;
set b1=m1*n1 - m2*n2 - m3*n3 - m4*n4, b2 = m1*n2 + m2*n1 + m3*n4 - m4*n3,
b3 = m1*n3 + m3*n1 + m4*n2 - m2*n4, b4 = m1*n4 + m4*n1 + m2*n3 - m3*n2;
A5: (m1^2 + m2^2 + m3^2 + m4^2)>=0 by Th67;
A6: (n1^2 + n2^2 + n3^2 + n4^2) >= 0 by Th67;
sqrt(b1^2 +b2^2 +b3^2 +b4^2)
=sqrt((m1^2 + m2^2 + m3^2 + m4^2) * (n1^2 + n2^2 + n3^2 + n4^2));
hence thesis by A1,A2,A3,A4,A5,A6,SQUARE_1:29;
end;
theorem
|.z*z.| = (Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z)^2
proof
A1: (Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z)^2 >= 0 by Th67;
|.z.| * |.z.| =(sqrt ((Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z)^2))^2
.= (Rea z)^2 + (Im1 z)^2 + (Im2 z)^2 + (Im3 z)^2 by A1,SQUARE_1:def 2;
hence thesis by Th80;
end;
theorem
|.z*z.| = |.z*z*'.|
proof
thus |.z*z.| = |.z.|*|.z.| by Th80
.= |.z.|*|.z*'.| by Th66
.= |.z*z*'.| by Th80;
end;
theorem
z is real implies Rea z = z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0
by Lm18;
theorem
for x,y being Element of REAL holds [*x,y,0,0*] = [*x,y*] by Lm3;
theorem
z1+z2 = Rea z1 + Rea z2 + (Im1 z1 + Im1 z2)*<i> +
(Im2 z1 + Im2 z2)*<j> + (Im3 z1 + Im3 z2)*<k> by Lm20;
theorem
z1*z2 =
(Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2) +
(Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2)*<i> +
(Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2)*<j> +
(Rea z1 * Im3 z2 + Im3 z1 * Rea z2 + Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2)*<k>
by Lm21;
theorem
-z = -Rea z + (-Im1 z)*<i> + (-Im2 z)*<j> + (-Im3 z)*<k> by Lm24;
theorem
z1 - z2 = Rea z1 - Rea z2 + (Im1 z1 - Im1 z2)*<i> +
(Im2 z1 - Im2 z2)*<j> + (Im3 z1 - Im3 z2)*<k> by Lm25;
theorem
for a, b, c, d being Real st a^2 + b^2 + c^2 + d^2 = 0 holds
a = 0 & b = 0 & c = 0 & d = 0 by Lm9;
theorem
Rea (z1 * z2) =
Rea z1 * Rea z2 - Im1 z1 * Im1 z2 - Im2 z1 * Im2 z2 - Im3 z1 * Im3 z2 &
Im1 (z1 * z2) =
Rea z1 * Im1 z2 + Im1 z1 * Rea z2 + Im2 z1 * Im3 z2 - Im3 z1 * Im2 z2 &
Im2 (z1 * z2) =
Rea z1 * Im2 z2 + Im2 z1 * Rea z2 + Im3 z1 * Im1 z2 - Im1 z1 * Im3 z2 &
Im3 (z1 * z2) =
Rea z1 * Im3 z2 + Im3 z1 * Rea z2 + Im1 z1 * Im2 z2 - Im2 z1 * Im1 z2
by Lm17;