:: The Quaternion Numbers
:: by Xiquan Liang and Fuguo Ge
::
:: Received November 14, 2006
:: Copyright (c) 2006-2021 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;
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 -> Number equals
(0,1,2,3) --> (0,0,1,0);
coherence;
func -> 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: * = [*zz,jj*] by ARYTM_0:def 5;
registration
cluster ** -> quaternion;
coherence by Lm2,XBOOLE_0:def 3;
cluster -> quaternion;
coherence
proof
set X = { x where x is Element of Funcs(4,REAL): x.2=0 & x.3=0};
A1: now
assume in X;
then ex x being Element of Funcs(4,REAL) st = 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;
= (0,1,2,3) --> (z,j,w,m);
then in Funcs(4,REAL) by CARD_1:52,FUNCT_2:8;
then in Funcs(4,REAL) \ X by A1,XBOOLE_0:def 5;
hence in QUATERNION by XBOOLE_0:def 3;
end;
cluster -> quaternion;
coherence
proof
set X = { x where x is Element of Funcs(4,REAL): x.2=0 & x.3=0};
A2: now
assume in X;
then ex x being Element of Funcs(4,REAL) st = 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;
= (0,1,2,3) --> (z,j,w,m);
then in Funcs(4,REAL) by CARD_1:52,FUNCT_2:8;
then in Funcs(4,REAL) \ X by A2,XBOOLE_0:def 5;
hence 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 -> Element of QUATERNION equals
[*0,0,1,0*];
coherence by Def2;
compatibility by Def5;
redefine func -> Element of QUATERNION equals
[*0,0,0,1*];
coherence by Def2;
compatibility by Def5;
end;
theorem
** * ** = -1
proof
** = [*zz,jj,zz,zz*] by Lm2,Lm3; then
A1: ** * ** = [* 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
* = -1
proof
A1: * = [* 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
* = -1
proof
A1: * = [* 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
** * =
proof
** = [*0,1,0,0*] by Lm2,Lm3;
then ** * = [* 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
* = **
proof
* = [* 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
* ** =
proof
** = [*0,1,0,0*] by Lm2,Lm3;
then * ** = [* 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
** * = - * **
proof
A1: ** = [*zz,jj,zz,zz*] by Lm2,Lm3;
then
A2: ** * = [* 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*];
* ** = [* 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 ** * + * ** = [*0+0,0+0,0+0,1+ -1*] by A2,Def6
.= 0 by Lm6;
hence thesis by Def7;
end;
theorem
* = - *
proof
A1: * = [* 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*];
* = [* 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 * + * = [*0+0,0+0,0+0,1+ -1*] by A1,Def6
.= 0 by Lm6;
hence thesis by Def7;
end;
theorem
* ** = - ** *
proof
A1: ** = [*zz,jj,zz,zz*] by Lm2,Lm3;
then
A2: * ** = [* 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*];
** * = [* 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 * ** + ** * = [*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 ** = 0 & Im1 ** = 1 & Im2 ** = 0 & Im3 ** = 0
proof
[*zz,jj*] = [*0,1,0,0*] by Lm3;
hence thesis by Lm2,Th16;
end;
theorem Th24:
Rea = 0 & Im1 = 0 & Im2 = 1 & Im3 = 0 &
Rea = 0 & Im1 = 0 & Im2 = 0 & Im3 = 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***) = 0 &
Im1 (z1***) = x & Im2 (z1***) = 0 & Im3 (z1***) = 0
proof
assume
A1: z1 = x;
A2: Rea (z1 * **) = Rea z1 * Rea ** - Im1 z1 * Im1 ** - Im2 z1 * Im2 **
- Im3 z1 * Im3 ** by Lm17;
A3: Im1 (z1 * **) = Rea z1 * Im1 ** + Im1 z1 * Rea ** + Im2 z1 * Im3 **
- Im3 z1 * Im2 ** by Lm17;
A4: Im2 (z1 * **) = Rea z1 * Im2 ** + Im2 z1 * Rea ** + Im3 z1 * Im1 **
- Im1 z1 * Im3 ** by Lm17;
Im3 (z1 * **) = Rea z1 * Im3 ** + Im3 z1 * Rea ** + Im1 z1 * Im2 **
- Im2 z1 * Im1 ** by Lm17;
hence thesis by A1,A2,A3,A4,Lm18,Th23;
end;
theorem
z1 = x implies Rea (z1*) = 0 &
Im1 (z1*) = 0 & Im2 (z1*) = x & Im3 (z1*) = 0
proof
assume
A1: z1 = x;
A2: Rea (z1 * ) = Rea z1 * Rea - Im1 z1 * Im1 - Im2 z1 * Im2
- Im3 z1 * Im3 by Lm17;
A3: Im1 (z1 * ) = Rea z1 * Im1 + Im1 z1 * Rea + Im2 z1 * Im3
- Im3 z1 * Im2 by Lm17;
A4: Im2 (z1 * ) = Rea z1 * Im2 + Im2 z1 * Rea + Im3 z1 * Im1
- Im1 z1 * Im3 by Lm17;
Im3 (z1 * ) = Rea z1 * Im3 + Im3 z1 * Rea + Im1 z1 * Im2
- Im2 z1 * Im1 by Lm17;
hence thesis by A1,A2,A3,A4,Lm18,Th24;
end;
theorem
z1 = x implies Rea (z1*) = 0 &
Im1 (z1*) = 0 & Im2 (z1*) = 0 & Im3 (z1*) = x
proof
assume
A1: z1 = x;
A2: Rea (z1 * ) = Rea z1 * Rea - Im1 z1 * Im1 - Im2 z1 * Im2
- Im3 z1 * Im3 by Lm17;
A3: Im1 (z1 * ) = Rea z1 * Im1 + Im1 z1 * Rea + Im2 z1 * Im3
- Im3 z1 * Im2 by Lm17;
A4: Im2 (z1 * ) = Rea z1 * Im2 + Im2 z1 * Rea + Im3 z1 * Im1
- Im1 z1 * Im3 by Lm17;
Im3 (z1 * ) = Rea z1 * Im3 + Im3 z1 * Rea + Im1 z1 * Im2
- Im2 z1 * Im1 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*** + z* + w*
proof
let x,y,z,w be Real;
** = [*zz,jj,zz,zz*] by Lm2,Lm3; then
A1: y*** = [*y*0,y*1,y*0,y*0*] by Def20
.= [*0,y,0,0*];
A2: z* = [*z*0,z*0,z*1,y*0*] by Def20
.= [*0,0,z,0*];
A3: w* = [*w*0,w*0,w*0,w*1*] by Def20
.= [*0,0,0,w*];
x + y* ** = [*x+0,y,0,0*] by A1,Def18
.= [*x,y,0,0*];
then x + y*** + z* = [*x+0,y+0,0+z,0+0*] by A2,Def6
.= [*x,y,z,0*];
then x + y*** + z* + w* = [*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;
coherence by Def2;
end;
Lm20: z1+z2 = Rea z1 + Rea z2 + (Im1 z1 + Im1 z2)*** +
(Im2 z1 + Im2 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 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;
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)*** +
(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
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)*** + (Im2 z)* + (Im3 z)*
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*** = 0 & 0* = 0 & 0* = 0
proof
set z1 = 0, z2 = **;
consider y1,y2,y3,y4 being Real such that
A1: ** = [*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: = [*y1,y2,y3,y4*] &
z1* = [*z1*y1,z1*y2,z1*y3,z1*y4*] by Def20;
A4: z1* = [*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: = [*y1,y2,y3,y4*] &
z1* = [*z1*y1,z1*y2,z1*y3,z1*y4*] by Def20;
z1* = [*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)*** +
(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 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;
coherence by Def2;
end;
Lm24: -z = -Rea z + (-Im1 z)*** + (-Im2 z)* + (-Im3 z)*
proof
set z9 = [* -Rea z, -Im1 z, -Im2 z, -Im3 z *];
A1: z9 = -Rea z+(-Im1 z)*** + (-Im2 z)* + (-Im3 z)* 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)*** + (-Im2 z)* + (-Im3 z)* 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;
coherence by Def2;
end;
Lm25: z1 - z2 = Rea z1 - Rea z2 + (Im1 z1 - Im1 z2)*** +
(Im2 z1 - Im2 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 Lm20
.= 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;
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)*** +
(Im2 z1 - Im2 z2)* + (Im3 z1 - Im3 z2)* 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)*** + (-Im2 z)* + (-Im3 z)*;
coherence;
end;
definition
let z be Quaternion;
redefine func z*' -> Element of QUATERNION;
coherence;
end;
theorem Th36:
z*' = [*Rea z, -Im1 z, -Im2 z, -Im3 z*]
proof
** = [*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)* + (-Im3 z)* by Def20
.= Rea z + [*0,-Im1 z,0,0 *] +
[*(-Im2 z)*0,(-Im2 z)*0,(-Im2 z)*1,(-Im2 z)*0*] + (-Im3 z)* 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 (***') = 0 & Im1 (***') = -1 & Im2 (***') = 0 & Im3 (***') = 0
proof
***' = [*zz, -jj, zz, zz*] by Th23,Th36;
hence thesis by Th16;
end;
theorem
Rea (*') = 0 & Im1 (*') = 0 & Im2 (*') = -1 & Im3 (*') = 0
proof
*' = [*zz,zz,-jj,zz*] by Th24,Th36;
hence thesis by Th16;
end;
theorem
Rea (*