:: QUATERNI semantic presentation
begin
definition
func QUATERNION -> set equals :: QUATERNI:def 1
((Funcs (4,REAL)) \ { x where x is Element of Funcs (4,REAL) : ( x . 2 = 0 & x . 3 = 0 ) } ) \/ COMPLEX;
coherence
((Funcs (4,REAL)) \ { x where x is Element of Funcs (4,REAL) : ( x . 2 = 0 & x . 3 = 0 ) } ) \/ COMPLEX is set ;
end;
:: deftheorem defines QUATERNION QUATERNI:def_1_:_
QUATERNION = ((Funcs (4,REAL)) \ { x where x is Element of Funcs (4,REAL) : ( x . 2 = 0 & x . 3 = 0 ) } ) \/ COMPLEX;
definition
let x be number ;
attrx is quaternion means :Def2: :: QUATERNI:def 2
x in QUATERNION ;
end;
:: deftheorem Def2 defines quaternion QUATERNI:def_2_:_
for x being number holds
( x is quaternion iff x in QUATERNION );
registration
cluster QUATERNION -> non empty ;
coherence
not QUATERNION is empty ;
end;
definition
let x, y, w, z, a, b, c, d be set ;
func(x,y,w,z) --> (a,b,c,d) -> set equals :: QUATERNI:def 3
((x,y) --> (a,b)) +* ((w,z) --> (c,d));
coherence
((x,y) --> (a,b)) +* ((w,z) --> (c,d)) is set ;
end;
:: deftheorem defines --> QUATERNI:def_3_:_
for x, y, w, z, a, b, c, d being set holds (x,y,w,z) --> (a,b,c,d) = ((x,y) --> (a,b)) +* ((w,z) --> (c,d));
registration
let x, y, w, z, a, b, c, d be set ;
cluster(x,y,w,z) --> (a,b,c,d) -> Relation-like Function-like ;
coherence
( (x,y,w,z) --> (a,b,c,d) is Function-like & (x,y,w,z) --> (a,b,c,d) is Relation-like ) ;
end;
theorem Th1: :: QUATERNI:1
for x, y, w, z, a, b, c, d being set holds dom ((x,y,w,z) --> (a,b,c,d)) = {x,y,w,z}
proof
let x, y, w, z, a, b, c, d be set ; ::_thesis: dom ((x,y,w,z) --> (a,b,c,d)) = {x,y,w,z}
set f = (x,y) --> (a,b);
set g = (w,z) --> (c,d);
A1: dom ((x,y) --> (a,b)) = {x,y} by FUNCT_4:62;
dom ((w,z) --> (c,d)) = {w,z} by FUNCT_4:62;
then (dom ((x,y) --> (a,b))) \/ (dom ((w,z) --> (c,d))) = {x,y,w,z} by A1, ENUMSET1:5;
hence dom ((x,y,w,z) --> (a,b,c,d)) = {x,y,w,z} by FUNCT_4:def_1; ::_thesis: verum
end;
theorem Th2: :: QUATERNI:2
for x, y, w, z, a, b, c, d being set holds rng ((x,y,w,z) --> (a,b,c,d)) c= {a,b,c,d}
proof
let x, y, w, z, a, b, c, d be set ; ::_thesis: rng ((x,y,w,z) --> (a,b,c,d)) c= {a,b,c,d}
set f = (x,y) --> (a,b);
set g = (w,z) --> (c,d);
set h = ((x,y) --> (a,b)) +* ((w,z) --> (c,d));
A1: rng ((x,y) --> (a,b)) c= {a,b} by FUNCT_4:62;
rng ((w,z) --> (c,d)) c= {c,d} by FUNCT_4:62;
then (rng ((x,y) --> (a,b))) \/ (rng ((w,z) --> (c,d))) c= {a,b} \/ {c,d} by A1, XBOOLE_1:13;
then A2: (rng ((x,y) --> (a,b))) \/ (rng ((w,z) --> (c,d))) c= {a,b,c,d} by ENUMSET1:5;
rng (((x,y) --> (a,b)) +* ((w,z) --> (c,d))) c= (rng ((x,y) --> (a,b))) \/ (rng ((w,z) --> (c,d))) by FUNCT_4:17;
hence rng ((x,y,w,z) --> (a,b,c,d)) c= {a,b,c,d} by A2, XBOOLE_1:1; ::_thesis: verum
end;
Lm1: 0 ,1,2,3 are_mutually_different
by ZFMISC_1:def_6;
theorem Th3: :: QUATERNI:3
for x, y, w, z, a, b, c, d being set st x,y,w,z are_mutually_different holds
( ((x,y,w,z) --> (a,b,c,d)) . x = a & ((x,y,w,z) --> (a,b,c,d)) . y = b & ((x,y,w,z) --> (a,b,c,d)) . w = c & ((x,y,w,z) --> (a,b,c,d)) . z = d )
proof
let x, y, w, z, a, b, c, d be set ; ::_thesis: ( x,y,w,z are_mutually_different implies ( ((x,y,w,z) --> (a,b,c,d)) . x = a & ((x,y,w,z) --> (a,b,c,d)) . y = b & ((x,y,w,z) --> (a,b,c,d)) . w = c & ((x,y,w,z) --> (a,b,c,d)) . z = d ) )
assume A1: x,y,w,z are_mutually_different ; ::_thesis: ( ((x,y,w,z) --> (a,b,c,d)) . x = a & ((x,y,w,z) --> (a,b,c,d)) . y = b & ((x,y,w,z) --> (a,b,c,d)) . w = c & ((x,y,w,z) --> (a,b,c,d)) . z = d )
then A2: x <> w by ZFMISC_1:def_6;
A3: x <> z by A1, ZFMISC_1:def_6;
A4: y <> w by A1, ZFMISC_1:def_6;
A5: y <> z by A1, ZFMISC_1:def_6;
A6: x <> y by A1, ZFMISC_1:def_6;
A7: w <> z by A1, ZFMISC_1:def_6;
set f = (x,y) --> (a,b);
set g = (w,z) --> (c,d);
A8: ((x,y) --> (a,b)) . x = a by A6, FUNCT_4:63;
A9: ((x,y) --> (a,b)) . y = b by FUNCT_4:63;
A10: ((w,z) --> (c,d)) . w = c by A7, FUNCT_4:63;
A11: ((w,z) --> (c,d)) . z = d by FUNCT_4:63;
A12: dom ((w,z) --> (c,d)) = {w,z} by FUNCT_4:62;
then A13: not x in dom ((w,z) --> (c,d)) by A2, A3, TARSKI:def_2;
A14: not y in dom ((w,z) --> (c,d)) by A4, A5, A12, TARSKI:def_2;
A15: w in dom ((w,z) --> (c,d)) by A12, TARSKI:def_2;
z in dom ((w,z) --> (c,d)) by A12, TARSKI:def_2;
hence ( ((x,y,w,z) --> (a,b,c,d)) . x = a & ((x,y,w,z) --> (a,b,c,d)) . y = b & ((x,y,w,z) --> (a,b,c,d)) . w = c & ((x,y,w,z) --> (a,b,c,d)) . z = d ) by A8, A9, A10, A11, A13, A14, A15, FUNCT_4:11, FUNCT_4:13; ::_thesis: verum
end;
Lm2: for x, y, w, z, a, b, c, d being set st x,y,w,z are_mutually_different holds
{a,b,c,d} c= rng ((x,y,w,z) --> (a,b,c,d))
proof
let x, y, w, z, a, b, c, d be set ; ::_thesis: ( x,y,w,z are_mutually_different implies {a,b,c,d} c= rng ((x,y,w,z) --> (a,b,c,d)) )
set h = (x,y,w,z) --> (a,b,c,d);
assume A1: x,y,w,z are_mutually_different ; ::_thesis: {a,b,c,d} c= rng ((x,y,w,z) --> (a,b,c,d))
let y1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not y1 in {a,b,c,d} or y1 in rng ((x,y,w,z) --> (a,b,c,d)) )
assume y1 in {a,b,c,d} ; ::_thesis: y1 in rng ((x,y,w,z) --> (a,b,c,d))
then A2: ( y1 = a or y1 = b or y1 = c or y1 = d ) by ENUMSET1:def_2;
A3: dom ((x,y,w,z) --> (a,b,c,d)) = {x,y,w,z} by Th1;
A4: ( ((x,y,w,z) --> (a,b,c,d)) . x = y1 or ((x,y,w,z) --> (a,b,c,d)) . y = y1 or ((x,y,w,z) --> (a,b,c,d)) . w = y1 or ((x,y,w,z) --> (a,b,c,d)) . z = y1 ) by A1, A2, Th3;
A5: x in dom ((x,y,w,z) --> (a,b,c,d)) by A3, ENUMSET1:def_2;
A6: y in dom ((x,y,w,z) --> (a,b,c,d)) by A3, ENUMSET1:def_2;
A7: w in dom ((x,y,w,z) --> (a,b,c,d)) by A3, ENUMSET1:def_2;
z in dom ((x,y,w,z) --> (a,b,c,d)) by A3, ENUMSET1:def_2;
hence y1 in rng ((x,y,w,z) --> (a,b,c,d)) by A4, A5, A6, A7, FUNCT_1:def_3; ::_thesis: verum
end;
theorem :: QUATERNI:4
for x, y, w, z, a, b, c, d being set st x,y,w,z are_mutually_different holds
rng ((x,y,w,z) --> (a,b,c,d)) = {a,b,c,d}
proof
let x, y, w, z, a, b, c, d be set ; ::_thesis: ( x,y,w,z are_mutually_different implies rng ((x,y,w,z) --> (a,b,c,d)) = {a,b,c,d} )
set h = (x,y,w,z) --> (a,b,c,d);
assume A1: x,y,w,z are_mutually_different ; ::_thesis: rng ((x,y,w,z) --> (a,b,c,d)) = {a,b,c,d}
A2: rng ((x,y,w,z) --> (a,b,c,d)) c= {a,b,c,d} by Th2;
{a,b,c,d} c= rng ((x,y,w,z) --> (a,b,c,d)) by A1, Lm2;
hence rng ((x,y,w,z) --> (a,b,c,d)) = {a,b,c,d} by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: QUATERNI:5
for x1, x2, x3, x4, X being set holds
( {x1,x2,x3,x4} c= X iff ( x1 in X & x2 in X & x3 in X & x4 in X ) )
proof
let x1, x2, x3, x4, X be set ; ::_thesis: ( {x1,x2,x3,x4} c= X iff ( x1 in X & x2 in X & x3 in X & x4 in X ) )
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; ::_thesis: ( x1 in X & x2 in X & x3 in X & x4 in X implies {x1,x2,x3,x4} c= X )
assume that
A4: x1 in X and
A5: x2 in X and
A6: x3 in X and
A7: x4 in X ; ::_thesis: {x1,x2,x3,x4} c= X
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {x1,x2,x3,x4} or z in X )
assume z in {x1,x2,x3,x4} ; ::_thesis: z in X
hence z in X by A4, A5, A6, A7, ENUMSET1:def_2; ::_thesis: verum
end;
definition
let A be non empty set ;
let x, y, w, z be set ;
let a, b, c, d be Element of A;
:: original: -->
redefine func(x,y,w,z) --> (a,b,c,d) -> Function of {x,y,w,z},A;
coherence
(x,y,w,z) --> (a,b,c,d) is Function of {x,y,w,z},A
proof
set f = (x,y) --> (a,b);
set g = (w,z) --> (c,d);
set h = (x,y,w,z) --> (a,b,c,d);
A1: rng ((x,y,w,z) --> (a,b,c,d)) c= (rng ((x,y) --> (a,b))) \/ (rng ((w,z) --> (c,d))) by FUNCT_4:17;
A2: dom ((x,y,w,z) --> (a,b,c,d)) = {x,y,w,z} by Th1;
rng ((x,y,w,z) --> (a,b,c,d)) c= A by A1, XBOOLE_1:1;
hence (x,y,w,z) --> (a,b,c,d) is Function of {x,y,w,z},A by A2, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
end;
definition
func -> set equals :: QUATERNI:def 4
(0,1,2,3) --> (0,0,1,0);
coherence
(0,1,2,3) --> (0,0,1,0) is set ;
func -> set equals :: QUATERNI:def 5
(0,1,2,3) --> (0,0,0,1);
coherence
(0,1,2,3) --> (0,0,0,1) is set ;
end;
:: deftheorem defines QUATERNI:def_4_:_
= (0,1,2,3) --> (0,0,1,0);
:: deftheorem defines QUATERNI:def_5_:_
= (0,1,2,3) --> (0,0,0,1);
Lm3: * = [*0,1*]
by ARYTM_0:def_5;
registration
cluster ** -> quaternion ;
coherence
** is quaternion
proof
thus ** in QUATERNION by Lm3, XBOOLE_0:def_3; :: according to QUATERNI:def_2 ::_thesis: verum
end;
cluster -> quaternion ;
coherence
is quaternion
proof
set X = { x where x is Element of Funcs (4,REAL) : ( x . 2 = 0 & x . 3 = 0 ) } ;
A1: now__::_thesis:_not__in__{__x_where_x_is_Element_of_Funcs_(4,REAL)_:_(_x_._2_=_0_&_x_._3_=_0_)__}_
assume in { x where x is Element of Funcs (4,REAL) : ( x . 2 = 0 & x . 3 = 0 ) } ; ::_thesis: contradiction
then ex x being Element of Funcs (4,REAL) st
( = x & x . 2 = 0 & x . 3 = 0 ) ;
hence contradiction by Lm1, Th3; ::_thesis: verum
end;
reconsider z = 0 , j = 0 , w = 1, m = 0 as Element of REAL ;
= (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 where x is Element of Funcs (4,REAL) : ( x . 2 = 0 & x . 3 = 0 ) } by A1, XBOOLE_0:def_5;
hence in QUATERNION by XBOOLE_0:def_3; :: according to QUATERNI:def_2 ::_thesis: verum
end;
cluster -> quaternion ;
coherence
is quaternion
proof
set X = { x where x is Element of Funcs (4,REAL) : ( x . 2 = 0 & x . 3 = 0 ) } ;
A2: now__::_thesis:_not__in__{__x_where_x_is_Element_of_Funcs_(4,REAL)_:_(_x_._2_=_0_&_x_._3_=_0_)__}_
assume in { x where x is Element of Funcs (4,REAL) : ( x . 2 = 0 & x . 3 = 0 ) } ; ::_thesis: contradiction
then ex x being Element of Funcs (4,REAL) st
( = x & x . 2 = 0 & x . 3 = 0 ) ;
hence contradiction by Lm1, Th3; ::_thesis: verum
end;
reconsider z = 0 , j = 0 , w = 0 , m = 1 as Element of REAL ;
= (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 where x is Element of Funcs (4,REAL) : ( x . 2 = 0 & x . 3 = 0 ) } by A2, XBOOLE_0:def_5;
hence in QUATERNION by XBOOLE_0:def_3; :: according to QUATERNI:def_2 ::_thesis: verum
end;
end;
registration
cluster quaternion for set ;
existence
ex b1 being number st b1 is quaternion
proof
take ; ::_thesis: is quaternion
thus is quaternion ; ::_thesis: verum
end;
end;
registration
cluster -> quaternion for Element of QUATERNION ;
coherence
for b1 being Element of QUATERNION holds b1 is quaternion by Def2;
end;
definition
let x, y, w, z be real number ;
func[*x,y,w,z*] -> Element of QUATERNION means :Def6: :: QUATERNI:def 6
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
for b1 being Element of QUATERNION holds verum ;
existence
( ( w = 0 & z = 0 implies ex b1 being Element of QUATERNION ex x9, y9 being Element of REAL st
( x9 = x & y9 = y & b1 = [*x9,y9*] ) ) & ( ( not w = 0 or not z = 0 ) implies ex b1 being Element of QUATERNION st b1 = (0,1,2,3) --> (x,y,w,z) ) )
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 ex x9, y9 being Element of REAL st
( x9 = x & y9 = y & t = [*x9,y9*] ) ) ::_thesis: ( ( not w = 0 or not z = 0 ) implies ex b1 being Element of QUATERNION st b1 = (0,1,2,3) --> (x,y,w,z) )
proof
assume that
w = 0 and
z = 0 ; ::_thesis: ex t being Element of QUATERNION ex x9, y9 being Element of REAL st
( x9 = x & y9 = y & t = [*x9,y9*] )
set t = [*x9,y9*];
reconsider t = [*x9,y9*] as Element of QUATERNION by XBOOLE_0:def_3;
take t ; ::_thesis: ex x9, y9 being Element of REAL st
( x9 = x & y9 = y & t = [*x9,y9*] )
take x9 ; ::_thesis: ex y9 being Element of REAL st
( x9 = x & y9 = y & t = [*x9,y9*] )
take y9 ; ::_thesis: ( x9 = x & y9 = y & t = [*x9,y9*] )
thus ( x9 = x & y9 = y & t = [*x9,y9*] ) ; ::_thesis: verum
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) ) ::_thesis: verum
proof
assume A1: ( w <> 0 or z <> 0 ) ; ::_thesis: ex t being Element of QUATERNION st t = (0,1,2,3) --> (x,y,w,z)
A2: (0,1,2,3) --> (x9,y9,w9,z9) in Funcs (4,REAL) by CARD_1:52, FUNCT_2:8;
now__::_thesis:_not_(0,1,2,3)_-->_(x9,y9,w9,z9)_in__{__r_where_r_is_Element_of_Funcs_(4,REAL)_:_(_r_._2_=_0_&_r_._3_=_0_)__}_
assume (0,1,2,3) --> (x9,y9,w9,z9) in { r where r is Element of Funcs (4,REAL) : ( r . 2 = 0 & r . 3 = 0 ) } ; ::_thesis: contradiction
then ex r being Element of Funcs (4,REAL) st
( (0,1,2,3) --> (x9,y9,w9,z9) = r & r . 2 = 0 & r . 3 = 0 ) ;
hence contradiction by A1, Lm1, Th3; ::_thesis: verum
end;
then (0,1,2,3) --> (x9,y9,w9,z9) 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 = (0,1,2,3) --> (x9,y9,w9,z9) as Element of QUATERNION by XBOOLE_0:def_3;
take e ; ::_thesis: e = (0,1,2,3) --> (x,y,w,z)
thus e = (0,1,2,3) --> (x,y,w,z) ; ::_thesis: verum
end;
end;
uniqueness
for b1, b2 being Element of QUATERNION holds
( ( w = 0 & z = 0 & ex x9, y9 being Element of REAL st
( x9 = x & y9 = y & b1 = [*x9,y9*] ) & ex x9, y9 being Element of REAL st
( x9 = x & y9 = y & b2 = [*x9,y9*] ) implies b1 = b2 ) & ( ( not w = 0 or not z = 0 ) & b1 = (0,1,2,3) --> (x,y,w,z) & b2 = (0,1,2,3) --> (x,y,w,z) implies b1 = b2 ) ) ;
end;
:: deftheorem Def6 defines [* QUATERNI:def_6_:_
for x, y, w, z being real number
for b5 being Element of QUATERNION holds
( ( w = 0 & z = 0 implies ( b5 = [*x,y,w,z*] iff ex x9, y9 being Element of REAL st
( x9 = x & y9 = y & b5 = [*x9,y9*] ) ) ) & ( ( not w = 0 or not z = 0 ) implies ( b5 = [*x,y,w,z*] iff b5 = (0,1,2,3) --> (x,y,w,z) ) ) );
Lm4: for x, y being Element of REAL holds [*x,y,0,0*] = [*x,y*]
proof
let x, y be Element of REAL ; ::_thesis: [*x,y,0,0*] = [*x,y*]
ex x9, y9 being Element of REAL st
( x9 = x & y9 = y & [*x,y,0,0*] = [*x9,y9*] ) by Def6;
hence [*x,y,0,0*] = [*x,y*] ; ::_thesis: verum
end;
theorem Th6: :: QUATERNI:6
for a, b, c, d, e, i, j, k being set
for g being Function st a <> b & c <> d & dom g = {a,b,c,d} & g . a = e & g . b = i & g . c = j & g . d = k holds
g = (a,b,c,d) --> (e,i,j,k)
proof
let a, b, c, d, e, i, j, k be set ; ::_thesis: for g being Function st a <> b & c <> d & dom g = {a,b,c,d} & g . a = e & g . b = i & g . c = j & g . d = k holds
g = (a,b,c,d) --> (e,i,j,k)
let h be Function; ::_thesis: ( a <> b & c <> d & dom h = {a,b,c,d} & h . a = e & h . b = i & h . c = j & h . d = k implies h = (a,b,c,d) --> (e,i,j,k) )
assume that
A1: a <> b and
A2: c <> d and
A3: dom h = {a,b,c,d} and
A4: h . a = e and
A5: h . b = i and
A6: h . c = j and
A7: h . d = k ; ::_thesis: h = (a,b,c,d) --> (e,i,j,k)
set f = (a,b) --> (e,i);
set g = (c,d) --> (j,k);
A8: dom ((a,b) --> (e,i)) = {a,b} by FUNCT_4:62;
A9: dom ((c,d) --> (j,k)) = {c,d} by FUNCT_4:62;
then A10: dom h = (dom ((a,b) --> (e,i))) \/ (dom ((c,d) --> (j,k))) by A3, A8, ENUMSET1:5;
now__::_thesis:_for_x_being_set_st_x_in_(dom_((a,b)_-->_(e,i)))_\/_(dom_((c,d)_-->_(j,k)))_holds_
(_(_x_in_dom_((c,d)_-->_(j,k))_implies_h_._x_=_((c,d)_-->_(j,k))_._x_)_&_(_not_x_in_dom_((c,d)_-->_(j,k))_implies_h_._x_=_((a,b)_-->_(e,i))_._x_)_)
let x be set ; ::_thesis: ( x in (dom ((a,b) --> (e,i))) \/ (dom ((c,d) --> (j,k))) implies ( ( x in dom ((c,d) --> (j,k)) implies h . x = ((c,d) --> (j,k)) . x ) & ( not x in dom ((c,d) --> (j,k)) implies h . x = ((a,b) --> (e,i)) . x ) ) )
assume A11: x in (dom ((a,b) --> (e,i))) \/ (dom ((c,d) --> (j,k))) ; ::_thesis: ( ( x in dom ((c,d) --> (j,k)) implies h . x = ((c,d) --> (j,k)) . x ) & ( not x in dom ((c,d) --> (j,k)) implies h . x = ((a,b) --> (e,i)) . x ) )
thus ( x in dom ((c,d) --> (j,k)) implies h . x = ((c,d) --> (j,k)) . x ) ::_thesis: ( not x in dom ((c,d) --> (j,k)) implies h . x = ((a,b) --> (e,i)) . x )
proof
assume A12: x in dom ((c,d) --> (j,k)) ; ::_thesis: h . x = ((c,d) --> (j,k)) . x
percases ( x = c or x = d ) by A9, A12, TARSKI:def_2;
suppose x = c ; ::_thesis: h . x = ((c,d) --> (j,k)) . x
hence h . x = ((c,d) --> (j,k)) . x by A2, A6, FUNCT_4:63; ::_thesis: verum
end;
suppose x = d ; ::_thesis: h . x = ((c,d) --> (j,k)) . x
hence h . x = ((c,d) --> (j,k)) . x by A7, FUNCT_4:63; ::_thesis: verum
end;
end;
end;
thus ( not x in dom ((c,d) --> (j,k)) implies h . x = ((a,b) --> (e,i)) . x ) ::_thesis: verum
proof
assume not x in dom ((c,d) --> (j,k)) ; ::_thesis: h . x = ((a,b) --> (e,i)) . x
then A13: x in dom ((a,b) --> (e,i)) by A11, XBOOLE_0:def_3;
percases ( x = a or x = b ) by A8, A13, TARSKI:def_2;
suppose x = a ; ::_thesis: h . x = ((a,b) --> (e,i)) . x
hence h . x = ((a,b) --> (e,i)) . x by A1, A4, FUNCT_4:63; ::_thesis: verum
end;
suppose x = b ; ::_thesis: h . x = ((a,b) --> (e,i)) . x
hence h . x = ((a,b) --> (e,i)) . x by A5, FUNCT_4:63; ::_thesis: verum
end;
end;
end;
end;
hence h = (a,b,c,d) --> (e,i,j,k) by A10, FUNCT_4:def_1; ::_thesis: verum
end;
theorem Th7: :: QUATERNI:7
for g being quaternion number ex r, s, t, u being Element of REAL st g = [*r,s,t,u*]
proof
let g be quaternion number ; ::_thesis: ex r, s, t, u being Element of REAL st g = [*r,s,t,u*]
A1: g in QUATERNION by Def2;
percases ( g in COMPLEX or not g in COMPLEX ) ;
suppose g in COMPLEX ; ::_thesis: ex r, s, t, u being Element of REAL st g = [*r,s,t,u*]
then consider r, s being Element of REAL such that
A2: g = [*r,s*] by ARYTM_0:9;
take r ; ::_thesis: ex s, t, u being Element of REAL st g = [*r,s,t,u*]
take s ; ::_thesis: ex t, u being Element of REAL st g = [*r,s,t,u*]
take 0 ; ::_thesis: ex u being Element of REAL st g = [*r,s,0,u*]
take 0 ; ::_thesis: g = [*r,s,0,0*]
thus g = [*r,s,0,0*] by A2, Def6, A1; ::_thesis: verum
end;
suppose not g in COMPLEX ; ::_thesis: ex r, s, t, u being Element of REAL st g = [*r,s,t,u*]
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, Th6, CARD_1:52;
take r ; ::_thesis: ex s, t, u being Element of REAL st g = [*r,s,t,u*]
take s ; ::_thesis: ex t, u being Element of REAL st g = [*r,s,t,u*]
take t ; ::_thesis: ex u being Element of REAL st g = [*r,s,t,u*]
take u ; ::_thesis: g = [*r,s,t,u*]
now__::_thesis:_(_t_=_0_implies_not_u_=_0_)
assume that
A15: t = 0 and
A16: u = 0 ; ::_thesis: contradiction
A17: ((0,1,2,3) --> (r,s,t,u)) . 2 = 0 by A15, Lm1, Th3;
((0,1,2,3) --> (r,s,t,u)) . 3 = 0 by A16, Lm1, Th3;
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; ::_thesis: verum
end;
hence g = [*r,s,t,u*] by A14, Def6; ::_thesis: verum
end;
end;
end;
theorem Th8: :: QUATERNI:8
for a, c, x, w, b, d, y, z being set st a,c,x,w are_mutually_different holds
(a,c,x,w) --> (b,d,y,z) = {[a,b],[c,d],[x,y],[w,z]}
proof
let a, c, x, w, b, d, y, z be set ; ::_thesis: ( a,c,x,w are_mutually_different implies (a,c,x,w) --> (b,d,y,z) = {[a,b],[c,d],[x,y],[w,z]} )
assume A1: a,c,x,w are_mutually_different ; ::_thesis: (a,c,x,w) --> (b,d,y,z) = {[a,b],[c,d],[x,y],[w,z]}
then A2: a <> c by ZFMISC_1:def_6;
A3: a <> x by A1, ZFMISC_1:def_6;
A4: a <> w by A1, ZFMISC_1:def_6;
A5: c <> x by A1, ZFMISC_1:def_6;
A6: c <> w by A1, ZFMISC_1:def_6;
A7: x <> w by A1, ZFMISC_1:def_6;
set m = (a,c) --> (b,d);
set n = (x,w) --> (y,z);
A8: dom ((a,c) --> (b,d)) = {a,c} by FUNCT_4:62;
A9: dom ((x,w) --> (y,z)) = {x,w} by FUNCT_4:62;
A10: not a in {x,w} by A3, A4, TARSKI:def_2;
not c in {x,w} by A5, A6, TARSKI:def_2;
then (a,c,x,w) --> (b,d,y,z) = ((a,c) --> (b,d)) \/ ((x,w) --> (y,z)) by A8, A9, A10, FUNCT_4:31, ZFMISC_1:51
.= {[a,b],[c,d]} \/ ((x,w) --> (y,z)) by A2, FUNCT_4:67
.= {[a,b],[c,d]} \/ {[x,y],[w,z]} by A7, FUNCT_4:67
.= {[a,b],[c,d],[x,y],[w,z]} by ENUMSET1:5 ;
hence (a,c,x,w) --> (b,d,y,z) = {[a,b],[c,d],[x,y],[w,z]} ; ::_thesis: verum
end;
Lm5: for x, y, z being set st [x,y] = {z} holds
( z = {x} & x = y )
proof
let x, y, z be set ; ::_thesis: ( [x,y] = {z} implies ( z = {x} & x = y ) )
assume A1: [x,y] = {z} ; ::_thesis: ( z = {x} & x = y )
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; ::_thesis: x = y
{x,y} = z by A2, TARSKI:def_1;
hence x = y by A3, ZFMISC_1:5; ::_thesis: verum
end;
theorem Th9: :: QUATERNI:9
for A being Subset of RAT+ st ex t being Element of RAT+ st
( t in A & t <> {} ) & ( for r, s being Element of RAT+ st r in A & s <=' r holds
s in A ) holds
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+; ::_thesis: ( ex t being Element of RAT+ st
( t in A & t <> {} ) & ( for r, s being Element of RAT+ st r in A & s <=' r holds
s in A ) implies 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 ) )
given t being Element of RAT+ such that A1: t in A and
A2: t <> {} ; ::_thesis: ( ex r, s being Element of RAT+ st
( r in A & s <=' r & not s in A ) or 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 ) )
assume A3: for r, s being Element of RAT+ st r in A & s <=' r holds
s in A ; ::_thesis: 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 )
consider x being Element of RAT+ such that
A4: t = x + x by ARYTM_3:60;
consider y being Element of RAT+ such that
A5: x = y + y by ARYTM_3:60;
consider w being Element of RAT+ such that
A6: y = w + w by ARYTM_3:60;
take {} ; ::_thesis: ex r2, r3, r4, r5 being Element of RAT+ st
( {} in A & r2 in A & r3 in A & r4 in A & r5 in A & {} <> r2 & {} <> r3 & {} <> r4 & {} <> r5 & r2 <> r3 & r2 <> r4 & r2 <> r5 & r3 <> r4 & r3 <> r5 & r4 <> r5 )
take w ; ::_thesis: ex r3, r4, r5 being Element of RAT+ st
( {} in A & w in A & r3 in A & r4 in A & r5 in A & {} <> w & {} <> r3 & {} <> r4 & {} <> r5 & w <> r3 & w <> r4 & w <> r5 & r3 <> r4 & r3 <> r5 & r4 <> r5 )
take y ; ::_thesis: ex r4, r5 being Element of RAT+ st
( {} in A & w in A & y in A & r4 in A & r5 in A & {} <> w & {} <> y & {} <> r4 & {} <> r5 & w <> y & w <> r4 & w <> r5 & y <> r4 & y <> r5 & r4 <> r5 )
take x ; ::_thesis: ex r5 being Element of RAT+ st
( {} in A & w in A & y in A & x in A & r5 in A & {} <> w & {} <> y & {} <> x & {} <> r5 & w <> y & w <> x & w <> r5 & y <> x & y <> r5 & x <> r5 )
take t ; ::_thesis: ( {} in A & w in A & y in A & x in A & t in A & {} <> w & {} <> y & {} <> x & {} <> t & w <> y & w <> x & w <> t & y <> x & y <> t & x <> t )
A7: {} <=' t by ARYTM_3:64;
A8: x <=' t by A4, ARYTM_3:def_13;
A9: y <=' x by A5, ARYTM_3:def_13;
A10: w <=' y by A6, ARYTM_3:def_13;
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; ::_thesis: ( {} <> w & {} <> y & {} <> x & {} <> t & w <> y & w <> x & w <> t & y <> x & y <> t & x <> t )
A12: {} <> x by A2, A4, ARYTM_3:50;
then A13: {} <> y by A5, ARYTM_3:50;
A14: x <> t
proof
assume x = t ; ::_thesis: contradiction
then t + {} = t + t by A4, ARYTM_3:50;
hence contradiction by A2, ARYTM_3:62; ::_thesis: verum
end;
A15: y <> x
proof
assume y = x ; ::_thesis: contradiction
then x + {} = x + x by A5, ARYTM_3:50;
hence contradiction by A12, ARYTM_3:62; ::_thesis: verum
end;
w <> y
proof
assume w = y ; ::_thesis: contradiction
then y + {} = y + y by A6, ARYTM_3:50;
hence contradiction by A13, ARYTM_3:62; ::_thesis: verum
end;
hence ( {} <> w & {} <> y & {} <> x & {} <> t & w <> y & w <> x & w <> t & y <> x & y <> t & x <> t ) by A2, A4, A5, A6, A8, A9, A10, A11, A14, A15, ARYTM_3:50, ARYTM_3:66; ::_thesis: verum
end;
Lm6: for a, b, c, d being Element of REAL holds not (0,1,2,3) --> (a,b,c,d) in REAL
proof
let a, b, c, d be Element of REAL ; ::_thesis: not (0,1,2,3) --> (a,b,c,d) in REAL
set f = (0,1,2,3) --> (a,b,c,d);
A1: (0,1,2,3) --> (a,b,c,d) = {[0,a],[1,b],[2,c],[3,d]} by Lm1, Th8;
now__::_thesis:_not_(0,1,2,3)_-->_(a,b,c,d)_in__{__[i,j]_where_i,_j_is_Element_of_NAT_:_(_i,j_are_relative_prime_&_j_<>_{}_)__}_
assume (0,1,2,3) --> (a,b,c,d) in { [i,j] where i, j is Element of NAT : ( i,j are_relative_prime & j <> {} ) } ; ::_thesis: contradiction
then consider i, j being Element of NAT such that
A2: (0,1,2,3) --> (a,b,c,d) = [i,j] and
i,j are_relative_prime and
j <> {} ;
A3: {i} in (0,1,2,3) --> (a,b,c,d) by A2, TARSKI:def_2;
A4: {i,j} in (0,1,2,3) --> (a,b,c,d) by A2, TARSKI:def_2;
A5: now__::_thesis:_not_i_=_j
assume i = j ; ::_thesis: contradiction
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; ::_thesis: verum
end;
percases ( ( {i} = [0,a] & {i,j} = [0,a] ) or ( {i} = [0,a] & {i,j} = [1,b] ) or ( {i} = [0,a] & {i,j} = [2,c] ) or ( {i} = [0,a] & {i,j} = [3,d] ) or ( {i} = [1,b] & {i,j} = [0,a] ) or ( {i} = [1,b] & {i,j} = [1,b] ) or ( {i} = [1,b] & {i,j} = [2,c] ) or ( {i} = [1,b] & {i,j} = [3,d] ) or ( {i} = [2,c] & {i,j} = [0,a] ) or ( {i} = [2,c] & {i,j} = [1,b] ) or ( {i} = [2,c] & {i,j} = [2,c] ) or ( {i} = [2,c] & {i,j} = [3,d] ) or ( {i} = [3,d] & {i,j} = [0,a] ) or ( {i} = [3,d] & {i,j} = [1,b] ) or ( {i} = [3,d] & {i,j} = [2,c] ) or ( {i} = [3,d] & {i,j} = [3,d] ) ) by A1, A3, A4, ENUMSET1:def_2;
suppose ( {i} = [0,a] & {i,j} = [0,a] ) ; ::_thesis: contradiction
hence contradiction by A5, ZFMISC_1:5; ::_thesis: verum
end;
supposethat A10: {i} = [0,a] and
A11: {i,j} = [1,b] ; ::_thesis: contradiction
A12: i = {0} by A10, Lm5;
i in [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, TARSKI:def_2;
hence contradiction by A12, TARSKI:def_1; ::_thesis: verum
end;
supposethat A13: {i} = [0,a] and
A14: {i,j} = [2,c] ; ::_thesis: contradiction
A15: i = {0} by A13, Lm5;
i in [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, TARSKI:def_2;
hence contradiction by A15, TARSKI:def_1; ::_thesis: verum
end;
supposethat A16: {i} = [0,a] and
A17: {i,j} = [3,d] ; ::_thesis: contradiction
A18: i = {0} by A16, Lm5;
i in [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, TARSKI:def_2;
hence contradiction by A18, TARSKI:def_1; ::_thesis: verum
end;
supposethat A19: {i} = [1,b] and
A20: {i,j} = [0,a] ; ::_thesis: contradiction
A21: i = {1} by A19, Lm5;
i in [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, TARSKI:def_2;
hence contradiction by A21, TARSKI:def_1; ::_thesis: verum
end;
suppose ( {i} = [1,b] & {i,j} = [1,b] ) ; ::_thesis: contradiction
hence contradiction by A5, ZFMISC_1:5; ::_thesis: verum
end;
supposethat A22: {i} = [1,b] and
A23: {i,j} = [2,c] ; ::_thesis: contradiction
A24: i = {1} by A22, Lm5;
i in [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, TARSKI:def_2;
hence contradiction by A24, TARSKI:def_1; ::_thesis: verum
end;
supposethat A25: {i} = [1,b] and
A26: {i,j} = [3,d] ; ::_thesis: contradiction
A27: i = {1} by A25, Lm5;
i in [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, TARSKI:def_2;
hence contradiction by A27, TARSKI:def_1; ::_thesis: verum
end;
supposethat A28: {i} = [2,c] and
A29: {i,j} = [0,a] ; ::_thesis: contradiction
A30: i = {2} by A28, Lm5;
i in [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, TARSKI:def_2;
hence contradiction by A30, TARSKI:def_1; ::_thesis: verum
end;
supposethat A31: {i} = [2,c] and
A32: {i,j} = [1,b] ; ::_thesis: contradiction
A33: i = {2} by A31, Lm5;
i in [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, TARSKI:def_2;
hence contradiction by A33, TARSKI:def_1; ::_thesis: verum
end;
suppose ( {i} = [2,c] & {i,j} = [2,c] ) ; ::_thesis: contradiction
hence contradiction by A5, ZFMISC_1:5; ::_thesis: verum
end;
supposethat A34: {i} = [2,c] and
A35: {i,j} = [3,d] ; ::_thesis: contradiction
A36: i = {2} by A34, Lm5;
i in [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, TARSKI:def_2;
hence contradiction by A36, TARSKI:def_1; ::_thesis: verum
end;
supposethat A37: {i} = [3,d] and
A38: {i,j} = [0,a] ; ::_thesis: contradiction
A39: i = {3} by A37, Lm5;
i in [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, TARSKI:def_2;
hence contradiction by A39, TARSKI:def_1; ::_thesis: verum
end;
supposethat A40: {i} = [3,d] and
A41: {i,j} = [1,b] ; ::_thesis: contradiction
A42: i = {3} by A40, Lm5;
i in [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, TARSKI:def_2;
hence contradiction by A42, TARSKI:def_1; ::_thesis: verum
end;
supposethat A43: {i} = [3,d] and
A44: {i,j} = [2,c] ; ::_thesis: contradiction
A45: i = {3} by A43, Lm5;
i in [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, TARSKI:def_2;
hence contradiction by A45, TARSKI:def_1; ::_thesis: verum
end;
suppose ( {i} = [3,d] & {i,j} = [3,d] ) ; ::_thesis: contradiction
hence contradiction by A5, ZFMISC_1:5; ::_thesis: verum
end;
end;
end;
then A46: not (0,1,2,3) --> (a,b,c,d) in { [i,j] where i, j is Element of NAT : ( i,j are_relative_prime & j <> {} ) } \ { [k,1] where k is Element of NAT : verum } ;
now__::_thesis:_not_(0,1,2,3)_-->_(a,b,c,d)_in_omega
assume (0,1,2,3) --> (a,b,c,d) in omega ; ::_thesis: contradiction
then {} in (0,1,2,3) --> (a,b,c,d) by ORDINAL3:8;
hence contradiction by A1, ENUMSET1:def_2; ::_thesis: verum
end;
then A47: not (0,1,2,3) --> (a,b,c,d) 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 ) ) } ;
for x, y, z, w being set holds not {[0,x],[1,y],[2,z],[3,w]} in { 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 ) ) }
proof
given x, y, z, w being set such that A48: {[0,x],[1,y],[2,z],[3,w]} in { 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 ) ) } ; ::_thesis: contradiction
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, Th9;
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; ::_thesis: verum
end;
then not (0,1,2,3) --> (a,b,c,d) in DEDEKIND_CUTS by A1, ARYTM_2:def_1;
then A70: not (0,1,2,3) --> (a,b,c,d) in REAL+ by A47, ARYTM_2:def_2, XBOOLE_0:def_3;
now__::_thesis:_not_(0,1,2,3)_-->_(a,b,c,d)_in_[:{{}},REAL+:]
assume (0,1,2,3) --> (a,b,c,d) in [:{{}},REAL+:] ; ::_thesis: contradiction
then consider x, y being set such that
A71: x in {{}} and
y in REAL+ and
A72: (0,1,2,3) --> (a,b,c,d) = [x,y] by ZFMISC_1:84;
A73: x = 0 by A71, TARSKI:def_1;
(0,1,2,3) --> (a,b,c,d) = {[0,a],[1,b],[2,c],[3,d]} by Lm1, Th8;
then A74: [1,b] in (0,1,2,3) --> (a,b,c,d) by ENUMSET1:def_2;
percases ( {{1,b},{1}} = {0} or {{1,b},{1}} = {0,y} ) by A72, A73, A74, TARSKI:def_2;
suppose {{1,b},{1}} = {0} ; ::_thesis: contradiction
then 0 in {{1,b},{1}} by TARSKI:def_1;
hence contradiction by TARSKI:def_2; ::_thesis: verum
end;
suppose {{1,b},{1}} = {0,y} ; ::_thesis: contradiction
then 0 in {{1,b},{1}} by TARSKI:def_2;
hence contradiction by TARSKI:def_2; ::_thesis: verum
end;
end;
end;
hence not (0,1,2,3) --> (a,b,c,d) in REAL by A70, NUMBERS:def_1, XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th10: :: QUATERNI:10
for a, b, c, d being Element of REAL holds not (0,1,2,3) --> (a,b,c,d) in COMPLEX
proof
let a, b, c, d be Element of REAL ; ::_thesis: not (0,1,2,3) --> (a,b,c,d) in COMPLEX
set f = (0,1,2,3) --> (a,b,c,d);
A1: not (0,1,2,3) --> (a,b,c,d) in REAL by Lm6;
not (0,1,2,3) --> (a,b,c,d) in Funcs ({0,1},REAL)
proof
assume (0,1,2,3) --> (a,b,c,d) in Funcs ({0,1},REAL) ; ::_thesis: contradiction
then dom ((0,1,2,3) --> (a,b,c,d)) = {0,1} by FUNCT_2:92;
then {0,1,2,3} c= {0,1} by Th1;
then {0,1} \/ {2,3} c= {0,1} by ENUMSET1:5;
hence contradiction by XBOOLE_1:11, ZFMISC_1:22; ::_thesis: verum
end;
then not (0,1,2,3) --> (a,b,c,d) in (Funcs ({0,1},REAL)) \ { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } ;
hence not (0,1,2,3) --> (a,b,c,d) in COMPLEX by A1, NUMBERS:def_2, XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th11: :: QUATERNI:11
for a, b, c, d, x, y, z, w, x9, y9, z9, w9 being set st a,b,c,d are_mutually_different & (a,b,c,d) --> (x,y,z,w) = (a,b,c,d) --> (x9,y9,z9,w9) holds
( x = x9 & y = y9 & z = z9 & w = w9 )
proof
let a, b, c, d, x, y, z, w, x9, y9, z9, w9 be set ; ::_thesis: ( a,b,c,d are_mutually_different & (a,b,c,d) --> (x,y,z,w) = (a,b,c,d) --> (x9,y9,z9,w9) implies ( x = x9 & y = y9 & z = z9 & w = w9 ) )
assume that
A1: a,b,c,d are_mutually_different and
A2: (a,b,c,d) --> (x,y,z,w) = (a,b,c,d) --> (x9,y9,z9,w9) ; ::_thesis: ( x = x9 & y = y9 & z = z9 & w = w9 )
A3: x = ((a,b,c,d) --> (x,y,z,w)) . a by A1, Th3
.= x9 by A1, A2, Th3 ;
A4: y = ((a,b,c,d) --> (x,y,z,w)) . b by A1, Th3
.= y9 by A1, A2, Th3 ;
A5: z = ((a,b,c,d) --> (x,y,z,w)) . c by A1, Th3
.= z9 by A1, A2, Th3 ;
w = ((a,b,c,d) --> (x,y,z,w)) . d by A1, Th3
.= w9 by A1, A2, Th3 ;
hence ( x = x9 & y = y9 & z = z9 & w = w9 ) by A3, A4, A5; ::_thesis: verum
end;
theorem Th12: :: QUATERNI:12
for x1, x2, x3, x4, y1, y2, y3, y4 being Element of 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 Element of REAL ; ::_thesis: ( [*x1,x2,x3,x4*] = [*y1,y2,y3,y4*] implies ( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 ) )
assume A1: [*x1,x2,x3,x4*] = [*y1,y2,y3,y4*] ; ::_thesis: ( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 )
percases ( ( x3 = 0 & x4 = 0 ) or x3 <> 0 or x4 <> 0 ) ;
supposeA2: ( x3 = 0 & x4 = 0 ) ; ::_thesis: ( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 )
then A3: [*x1,x2,x3,x4*] = [*x1,x2*] by Lm4;
A4: now__::_thesis:_(_not_y3_<>_0_&_not_y4_<>_0_)
assume ( y3 <> 0 or y4 <> 0 ) ; ::_thesis: contradiction
then [*x1,x2*] = (0,1,2,3) --> (y1,y2,y3,y4) by A1, A3, Def6;
hence contradiction by Th10; ::_thesis: verum
end;
then [*y1,y2,y3,y4*] = [*y1,y2*] by Lm4;
hence ( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 ) by A1, A2, A3, A4, ARYTM_0:10; ::_thesis: verum
end;
suppose ( x3 <> 0 or x4 <> 0 ) ; ::_thesis: ( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 )
then A5: [*y1,y2,y3,y4*] = (0,1,2,3) --> (x1,x2,x3,x4) by A1, Def6;
now__::_thesis:_(_y3_=_0_implies_not_y4_=_0_)
assume that
A6: y3 = 0 and
A7: y4 = 0 ; ::_thesis: contradiction
[*y1,y2,y3,y4*] = [*y1,y2*] by A6, A7, Lm4;
hence contradiction by A5, Th10; ::_thesis: verum
end;
then [*y1,y2,y3,y4*] = (0,1,2,3) --> (y1,y2,y3,y4) by Def6;
hence ( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 ) by A5, Lm1, Th11; ::_thesis: verum
end;
end;
end;
definition
let x, y be quaternion number ;
consider x1, x2, x3, x4 being Element of REAL such that
A1: x = [*x1,x2,x3,x4*] by Th7;
consider y1, y2, y3, y4 being Element of REAL such that
A2: y = [*y1,y2,y3,y4*] by Th7;
funcx + y -> set means :Def7: :: QUATERNI:def 7
ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & it = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] );
existence
ex b1 being set ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b1 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] )
proof
take [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ; ::_thesis: ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] )
thus ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b1 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) & ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b2 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) holds
b1 = b2
proof
let c1, c2 be number ; ::_thesis: ( ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & c1 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) & ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & c2 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) implies c1 = c2 )
given x1, x2, x3, x4, y1, y2, y3, y4 being Element of 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)*] ; ::_thesis: ( for x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL holds
( not x = [*x1,x2,x3,x4*] or not y = [*y1,y2,y3,y4*] or not c2 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) or c1 = c2 )
given x19, x29, x39, x49, y19, y29, y39, y49 being Element of 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)*] ; ::_thesis: c1 = c2
A9: x1 = x19 by A3, A6, Th12;
A10: x2 = x29 by A3, A6, Th12;
A11: x3 = x39 by A3, A6, Th12;
A12: x4 = x49 by A3, A6, Th12;
A13: y1 = y19 by A4, A7, Th12;
A14: y2 = y29 by A4, A7, Th12;
y3 = y39 by A4, A7, Th12;
hence c1 = c2 by A4, A5, A7, A8, A9, A10, A11, A12, A13, A14, Th12; ::_thesis: verum
end;
commutativity
for b1 being set
for x, y being quaternion number st ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b1 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) holds
ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( y = [*x1,x2,x3,x4*] & x = [*y1,y2,y3,y4*] & b1 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) ;
end;
:: deftheorem Def7 defines + QUATERNI:def_7_:_
for x, y being quaternion number
for b3 being set holds
( b3 = x + y iff ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b3 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) );
Lm7: 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 Def6;
hence 0 = [*0,0,0,0*] by ARYTM_0:def_5; ::_thesis: verum
end;
definition
let z be quaternion number ;
consider v, w, x, y being Element of REAL such that
A1: z = [*v,w,x,y*] by Th7;
func - z -> quaternion number means :Def8: :: QUATERNI:def 8
z + it = 0 ;
existence
ex b1 being quaternion number st z + b1 = 0
proof
reconsider z9 = [*(- v),(- w),(- x),(- y)*] as quaternion number ;
take z9 ; ::_thesis: z + z9 = 0
A2: 0 = v + (- v) ;
A3: 0 = w + (- w) ;
A4: 0 = x + (- x) ;
0 = y + (- y) ;
hence z + z9 = 0 by A1, A2, A3, A4, Def7, Lm7; ::_thesis: verum
end;
uniqueness
for b1, b2 being quaternion number st z + b1 = 0 & z + b2 = 0 holds
b1 = b2
proof
let c1, c2 be quaternion number ; ::_thesis: ( z + c1 = 0 & z + c2 = 0 implies c1 = c2 )
assume that
A5: z + c1 = 0 and
A6: z + c2 = 0 ; ::_thesis: c1 = c2
consider x1, x2, x3, x4, y1, y2, y3, y4 being Element of 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, Def7;
consider x19, x29, x39, x49, y19, y29, y39, y49 being Element of 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, Def7;
A13: x1 = x19 by A7, A10, Th12;
A14: x2 = x29 by A7, A10, Th12;
A15: x3 = x39 by A7, A10, Th12;
A16: x4 = x49 by A7, A10, Th12;
A17: x1 + y1 = 0 by A9, Lm7, Th12;
A18: x1 + y19 = 0 by A12, A13, Lm7, Th12;
A19: x2 + y2 = 0 by A9, Lm7, Th12;
A20: x2 + y29 = 0 by A12, A14, Lm7, Th12;
A21: x3 + y3 = 0 by A9, Lm7, Th12;
A22: x3 + y39 = 0 by A12, A15, Lm7, Th12;
A23: x4 + y4 = 0 by A9, Lm7, Th12;
x4 + y49 = 0 by A12, A16, Lm7, Th12;
hence c1 = c2 by A8, A11, A17, A18, A19, A20, A21, A22, A23; ::_thesis: verum
end;
involutiveness
for b1, b2 being quaternion number st b2 + b1 = 0 holds
b1 + b2 = 0 ;
end;
:: deftheorem Def8 defines - QUATERNI:def_8_:_
for z, b2 being quaternion number holds
( b2 = - z iff z + b2 = 0 );
definition
let x, y be quaternion number ;
funcx - y -> set equals :: QUATERNI:def 9
x + (- y);
coherence
x + (- y) is set ;
end;
:: deftheorem defines - QUATERNI:def_9_:_
for x, y being quaternion number holds x - y = x + (- y);
definition
let x, y be quaternion number ;
consider x1, x2, x3, x4 being Element of REAL such that
A1: x = [*x1,x2,x3,x4*] by Th7;
consider y1, y2, y3, y4 being Element of REAL such that
A2: y = [*y1,y2,y3,y4*] by Th7;
funcx * y -> set means :Def10: :: QUATERNI:def 10
ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of 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
ex b1 being set ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b1 = [*((((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))*] )
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))*] ; ::_thesis: ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & [*((((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))*] = [*((((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 ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & [*((((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))*] = [*((((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 A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b1 = [*((((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))*] ) & ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b2 = [*((((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))*] ) holds
b1 = b2
proof
let c1, c2 be number ; ::_thesis: ( ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & 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))*] ) & ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & c2 = [*((((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))*] ) implies c1 = c2 )
given x1, x2, x3, x4, y1, y2, y3, y4 being Element of 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))*] ; ::_thesis: ( for x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL holds
( not x = [*x1,x2,x3,x4*] or not y = [*y1,y2,y3,y4*] or not c2 = [*((((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))*] ) or c1 = c2 )
given x19, x29, x39, x49, y19, y29, y39, y49 being Element of 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))*] ; ::_thesis: c1 = c2
A9: x1 = x19 by A3, A6, Th12;
A10: x2 = x29 by A3, A6, Th12;
A11: x3 = x39 by A3, A6, Th12;
A12: x4 = x49 by A3, A6, Th12;
A13: y1 = y19 by A4, A7, Th12;
A14: y2 = y29 by A4, A7, Th12;
A15: y3 = y39 by A4, A7, Th12;
y4 = y49 by A4, A7, Th12;
hence c1 = c2 by A5, A8, A9, A10, A11, A12, A13, A14, A15; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines * QUATERNI:def_10_:_
for x, y being quaternion number
for b3 being set holds
( b3 = x * y iff ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b3 = [*((((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))*] ) );
registration
let z, z9 be quaternion number ;
clusterz + z9 -> quaternion ;
coherence
z + z9 is quaternion
proof
ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( z = [*x1,x2,x3,x4*] & z9 = [*y1,y2,y3,y4*] & z + z9 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) by Def7;
hence z + z9 is quaternion ; ::_thesis: verum
end;
clusterz * z9 -> quaternion ;
coherence
z * z9 is quaternion
proof
ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of 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 Def10;
hence z * z9 in QUATERNION ; :: according to QUATERNI:def_2 ::_thesis: verum
end;
end;
definition
:: original:
redefine func -> Element of QUATERNION equals :: QUATERNI:def 11
[*0,0,1,0*];
coherence
is Element of QUATERNION by Def2;
compatibility
for b1 being Element of QUATERNION holds
( b1 = iff b1 = [*0,0,1,0*] ) by Def6;
:: original:
redefine func -> Element of QUATERNION equals :: QUATERNI:def 12
[*0,0,0,1*];
coherence
is Element of QUATERNION by Def2;
compatibility
for b1 being Element of QUATERNION holds
( b1 = iff b1 = [*0,0,0,1*] ) by Def6;
end;
:: deftheorem defines QUATERNI:def_11_:_
= [*0,0,1,0*];
:: deftheorem defines QUATERNI:def_12_:_
= [*0,0,0,1*];
theorem :: QUATERNI:13
** * ** = - 1
proof
** = [*0,1,0,0*] by Lm3, Lm4;
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 Def10
.= [*(- 1),0,0,0*] ;
- 1 = [*(- 1),0*] by ARYTM_0:def_5;
hence ** * ** = - 1 by A1, Lm4; ::_thesis: verum
end;
theorem :: QUATERNI:14
* = - 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 Def10
.= [*(- 1),0,0,0*] ;
[*(- 1),0,0,0*] = [*(- 1),0*] by Lm4;
hence * = - 1 by A1, ARYTM_0:def_5; ::_thesis: verum
end;
theorem :: QUATERNI:15
* = - 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 Def10
.= [*(- 1),0,0,0*] ;
- 1 = [*(- 1),0*] by ARYTM_0:def_5;
hence * = - 1 by A1, Lm4; ::_thesis: verum
end;
theorem :: QUATERNI:16
** * =
proof
** = [*0,1,0,0*] by Lm3, Lm4;
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 Def10
.= [*0,0,0,1*] ;
hence ** * = ; ::_thesis: verum
end;
theorem :: QUATERNI:17
* = **
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 Def10
.= [*0,1,0,0*] ;
hence * = ** by Lm3, Lm4; ::_thesis: verum
end;
theorem :: QUATERNI:18
* ** =
proof
** = [*0,1,0,0*] by Lm3, Lm4;
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 Def10
.= [*0,0,1,0*] ;
hence * ** = ; ::_thesis: verum
end;
theorem :: QUATERNI:19
** * = - ( * **)
proof
A1: ** = [*0,1,0,0*] by Lm3, Lm4;
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 Def10
.= [*0,0,0,1*] ;
* ** = [*((((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, Def10
.= [*0,0,0,(- 1)*] ;
then (** * ) + ( * **) = [*(0 + 0),(0 + 0),(0 + 0),(1 + (- 1))*] by A2, Def7
.= 0 by Lm7 ;
hence ** * = - ( * **) by Def8; ::_thesis: verum
end;
theorem :: QUATERNI:20
* = - ( * )
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 Def10
.= [*0,1,0,0*] ;
* = [*((((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 Def10
.= [*0,(- 1),0,0*] ;
then ( * ) + ( * ) = [*(0 + 0),(0 + 0),(0 + 0),(1 + (- 1))*] by A1, Def7
.= 0 by Lm7 ;
hence * = - ( * ) by Def8; ::_thesis: verum
end;
theorem :: QUATERNI:21
* ** = - (** * )
proof
A1: ** = [*0,1,0,0*] by Lm3, Lm4;
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 Def10
.= [*0,0,1,0*] ;
** * = [*((((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, Def10
.= [*0,0,(- 1),0*] ;
then ( * **) + (** * ) = [*(0 + 0),(0 + 0),(1 + (- 1)),(0 + 0)*] by A2, Def7
.= 0 by Lm7 ;
hence * ** = - (** * ) by Def8; ::_thesis: verum
end;
definition
let z be quaternion number ;
func Rea z -> set means :Def13: :: QUATERNI:def 13
ex z9 being complex number 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
( ( z in COMPLEX implies ex b1 being set ex z9 being complex number st
( z = z9 & b1 = Re z9 ) ) & ( not z in COMPLEX implies ex b1 being set ex f being Function of 4,REAL st
( z = f & b1 = f . 0 ) ) )
proof
thus ( z in COMPLEX implies ex IT being set ex z9 being complex number st
( z = z9 & IT = Re z9 ) ) ::_thesis: ( not z in COMPLEX implies ex b1 being set ex f being Function of 4,REAL st
( z = f & b1 = f . 0 ) )
proof
assume z in COMPLEX ; ::_thesis: ex IT being set ex z9 being complex number st
( z = z9 & IT = Re z9 )
then consider r, s being Element of REAL such that
A1: z = [*r,s*] by ARYTM_0:9;
set z9 = [*r,s*];
take Re [*r,s*] ; ::_thesis: ex z9 being complex number st
( z = z9 & Re [*r,s*] = Re z9 )
take [*r,s*] ; ::_thesis: ( z = [*r,s*] & Re [*r,s*] = Re [*r,s*] )
thus ( z = [*r,s*] & Re [*r,s*] = Re [*r,s*] ) by A1; ::_thesis: verum
end;
assume A2: not z in COMPLEX ; ::_thesis: ex b1 being set ex f being Function of 4,REAL st
( z = f & b1 = f . 0 )
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 ; ::_thesis: ex f being Function of 4,REAL st
( z = f & f . 0 = f . 0 )
take f ; ::_thesis: ( z = f & f . 0 = f . 0 )
thus ( z = f & f . 0 = f . 0 ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being set holds
( ( z in COMPLEX & ex z9 being complex number st
( z = z9 & b1 = Re z9 ) & ex z9 being complex number st
( z = z9 & b2 = Re z9 ) implies b1 = b2 ) & ( not z in COMPLEX & ex f being Function of 4,REAL st
( z = f & b1 = f . 0 ) & ex f being Function of 4,REAL st
( z = f & b2 = f . 0 ) implies b1 = b2 ) ) ;
consistency
for b1 being set holds verum ;
func Im1 z -> set means :Def14: :: QUATERNI:def 14
ex z9 being complex number 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
( ( z in COMPLEX implies ex b1 being set ex z9 being complex number st
( z = z9 & b1 = Im z9 ) ) & ( not z in COMPLEX implies ex b1 being set ex f being Function of 4,REAL st
( z = f & b1 = f . 1 ) ) )
proof
thus ( z in COMPLEX implies ex IT being set ex z9 being complex number st
( z = z9 & IT = Im z9 ) ) ::_thesis: ( not z in COMPLEX implies ex b1 being set ex f being Function of 4,REAL st
( z = f & b1 = f . 1 ) )
proof
assume z in COMPLEX ; ::_thesis: ex IT being set ex z9 being complex number st
( z = z9 & IT = Im z9 )
then consider r, s being Element of REAL such that
A3: z = [*r,s*] by ARYTM_0:9;
set z9 = [*r,s*];
take Im [*r,s*] ; ::_thesis: ex z9 being complex number st
( z = z9 & Im [*r,s*] = Im z9 )
take [*r,s*] ; ::_thesis: ( z = [*r,s*] & Im [*r,s*] = Im [*r,s*] )
thus ( z = [*r,s*] & Im [*r,s*] = Im [*r,s*] ) by A3; ::_thesis: verum
end;
assume A4: not z in COMPLEX ; ::_thesis: ex b1 being set ex f being Function of 4,REAL st
( z = f & b1 = f . 1 )
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 ; ::_thesis: ex f being Function of 4,REAL st
( z = f & f . 1 = f . 1 )
take f ; ::_thesis: ( z = f & f . 1 = f . 1 )
thus ( z = f & f . 1 = f . 1 ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being set holds
( ( z in COMPLEX & ex z9 being complex number st
( z = z9 & b1 = Im z9 ) & ex z9 being complex number st
( z = z9 & b2 = Im z9 ) implies b1 = b2 ) & ( not z in COMPLEX & ex f being Function of 4,REAL st
( z = f & b1 = f . 1 ) & ex f being Function of 4,REAL st
( z = f & b2 = f . 1 ) implies b1 = b2 ) ) ;
consistency
for b1 being set holds verum ;
func Im2 z -> set means :Def15: :: QUATERNI:def 15
it = 0 if z in COMPLEX
otherwise ex f being Function of 4,REAL st
( z = f & it = f . 2 );
existence
( ( z in COMPLEX implies ex b1 being set st b1 = 0 ) & ( not z in COMPLEX implies ex b1 being set ex f being Function of 4,REAL st
( z = f & b1 = f . 2 ) ) )
proof
thus ( z in COMPLEX implies ex IT being set st IT = 0 ) ; ::_thesis: ( not z in COMPLEX implies ex b1 being set ex f being Function of 4,REAL st
( z = f & b1 = f . 2 ) )
assume A5: not z in COMPLEX ; ::_thesis: ex b1 being set ex f being Function of 4,REAL st
( z = f & b1 = f . 2 )
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 ; ::_thesis: ex f being Function of 4,REAL st
( z = f & f . 2 = f . 2 )
take f ; ::_thesis: ( z = f & f . 2 = f . 2 )
thus ( z = f & f . 2 = f . 2 ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being set holds
( ( z in COMPLEX & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( not z in COMPLEX & ex f being Function of 4,REAL st
( z = f & b1 = f . 2 ) & ex f being Function of 4,REAL st
( z = f & b2 = f . 2 ) implies b1 = b2 ) ) ;
consistency
for b1 being set holds verum ;
func Im3 z -> set means :Def16: :: QUATERNI:def 16
it = 0 if z in COMPLEX
otherwise ex f being Function of 4,REAL st
( z = f & it = f . 3 );
existence
( ( z in COMPLEX implies ex b1 being set st b1 = 0 ) & ( not z in COMPLEX implies ex b1 being set ex f being Function of 4,REAL st
( z = f & b1 = f . 3 ) ) )
proof
thus ( z in COMPLEX implies ex IT being set st IT = 0 ) ; ::_thesis: ( not z in COMPLEX implies ex b1 being set ex f being Function of 4,REAL st
( z = f & b1 = f . 3 ) )
assume A6: not z in COMPLEX ; ::_thesis: ex b1 being set ex f being Function of 4,REAL st
( z = f & b1 = f . 3 )
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 ; ::_thesis: ex f being Function of 4,REAL st
( z = f & f . 3 = f . 3 )
take f ; ::_thesis: ( z = f & f . 3 = f . 3 )
thus ( z = f & f . 3 = f . 3 ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being set holds
( ( z in COMPLEX & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( not z in COMPLEX & ex f being Function of 4,REAL st
( z = f & b1 = f . 3 ) & ex f being Function of 4,REAL st
( z = f & b2 = f . 3 ) implies b1 = b2 ) ) ;
consistency
for b1 being set holds verum ;
end;
:: deftheorem Def13 defines Rea QUATERNI:def_13_:_
for z being quaternion number
for b2 being set holds
( ( z in COMPLEX implies ( b2 = Rea z iff ex z9 being complex number st
( z = z9 & b2 = Re z9 ) ) ) & ( not z in COMPLEX implies ( b2 = Rea z iff ex f being Function of 4,REAL st
( z = f & b2 = f . 0 ) ) ) );
:: deftheorem Def14 defines Im1 QUATERNI:def_14_:_
for z being quaternion number
for b2 being set holds
( ( z in COMPLEX implies ( b2 = Im1 z iff ex z9 being complex number st
( z = z9 & b2 = Im z9 ) ) ) & ( not z in COMPLEX implies ( b2 = Im1 z iff ex f being Function of 4,REAL st
( z = f & b2 = f . 1 ) ) ) );
:: deftheorem Def15 defines Im2 QUATERNI:def_15_:_
for z being quaternion number
for b2 being set holds
( ( z in COMPLEX implies ( b2 = Im2 z iff b2 = 0 ) ) & ( not z in COMPLEX implies ( b2 = Im2 z iff ex f being Function of 4,REAL st
( z = f & b2 = f . 2 ) ) ) );
:: deftheorem Def16 defines Im3 QUATERNI:def_16_:_
for z being quaternion number
for b2 being set holds
( ( z in COMPLEX implies ( b2 = Im3 z iff b2 = 0 ) ) & ( not z in COMPLEX implies ( b2 = Im3 z iff ex f being Function of 4,REAL st
( z = f & b2 = f . 3 ) ) ) );
registration
let z be quaternion number ;
cluster Rea z -> real ;
coherence
Rea z is real
proof
percases ( z in COMPLEX or not z in COMPLEX ) ;
suppose z in COMPLEX ; ::_thesis: Rea z is real
then ex z9 being complex number st
( z = z9 & Rea z = Re z9 ) by Def13;
hence Rea z is real ; ::_thesis: verum
end;
suppose not z in COMPLEX ; ::_thesis: Rea z is real
then ex f being Function of 4,REAL st
( z = f & Rea z = f . 0 ) by Def13;
hence Rea z is real ; ::_thesis: verum
end;
end;
end;
cluster Im1 z -> real ;
coherence
Im1 z is real
proof
percases ( z in COMPLEX or not z in COMPLEX ) ;
suppose z in COMPLEX ; ::_thesis: Im1 z is real
then ex z9 being complex number st
( z = z9 & Im1 z = Im z9 ) by Def14;
hence Im1 z is real ; ::_thesis: verum
end;
suppose not z in COMPLEX ; ::_thesis: Im1 z is real
then ex f being Function of 4,REAL st
( z = f & Im1 z = f . 1 ) by Def14;
hence Im1 z is real ; ::_thesis: verum
end;
end;
end;
cluster Im2 z -> real ;
coherence
Im2 z is real
proof
percases ( z in COMPLEX or not z in COMPLEX ) ;
suppose z in COMPLEX ; ::_thesis: Im2 z is real
hence Im2 z is real by Def15; ::_thesis: verum
end;
suppose not z in COMPLEX ; ::_thesis: Im2 z is real
then ex f being Function of 4,REAL st
( z = f & Im2 z = f . 2 ) by Def15;
hence Im2 z is real ; ::_thesis: verum
end;
end;
end;
cluster Im3 z -> real ;
coherence
Im3 z is real
proof
percases ( z in COMPLEX or not z in COMPLEX ) ;
suppose z in COMPLEX ; ::_thesis: Im3 z is real
hence Im3 z is real by Def16; ::_thesis: verum
end;
suppose not z in COMPLEX ; ::_thesis: Im3 z is real
then ex f being Function of 4,REAL st
( z = f & Im3 z = f . 3 ) by Def16;
hence Im3 z is real ; ::_thesis: verum
end;
end;
end;
end;
definition
let z be quaternion number ;
:: original: Rea
redefine func Rea z -> Real;
coherence
Rea z is Real by XREAL_0:def_1;
:: original: Im1
redefine func Im1 z -> Real;
coherence
Im1 z is Real by XREAL_0:def_1;
:: original: Im2
redefine func Im2 z -> Real;
coherence
Im2 z is Real by XREAL_0:def_1;
:: original: Im3
redefine func Im3 z -> Real;
coherence
Im3 z is Real by XREAL_0:def_1;
end;
theorem Th22: :: QUATERNI:22
for f being Function of 4,REAL ex a, b, c, d being Element of REAL st f = (0,1,2,3) --> (a,b,c,d)
proof
let f be Function of 4,REAL; ::_thesis: ex a, b, c, d being Element of REAL st f = (0,1,2,3) --> (a,b,c,d)
reconsider a = f . 0, b = f . 1, c = f . 2, d = f . 3 as Element of REAL ;
take a ; ::_thesis: ex b, c, d being Element of REAL st f = (0,1,2,3) --> (a,b,c,d)
take b ; ::_thesis: ex c, d being Element of REAL st f = (0,1,2,3) --> (a,b,c,d)
take c ; ::_thesis: ex d being Element of REAL st f = (0,1,2,3) --> (a,b,c,d)
take d ; ::_thesis: f = (0,1,2,3) --> (a,b,c,d)
dom f = {0,1,2,3} by CARD_1:52, FUNCT_2:def_1;
hence f = (0,1,2,3) --> (a,b,c,d) by Th6; ::_thesis: verum
end;
Lm8: for a, b being Element of REAL holds
( Re [*a,b*] = a & Im [*a,b*] = b )
proof
let a, b be Element of REAL ; ::_thesis: ( Re [*a,b*] = a & Im [*a,b*] = b )
reconsider a9 = a, b9 = b as Element of REAL ;
thus Re [*a,b*] = a ::_thesis: Im [*a,b*] = b
proof
percases ( b = 0 or b <> 0 ) ;
suppose b = 0 ; ::_thesis: Re [*a,b*] = a
then [*a,b*] = a by ARYTM_0:def_5;
hence Re [*a,b*] = a by COMPLEX1:def_1; ::_thesis: verum
end;
suppose b <> 0 ; ::_thesis: Re [*a,b*] = a
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;
A2: not [*a,b*] in REAL by A1, ARYTM_0:8;
f . 0 = a by A1, FUNCT_4:63;
hence Re [*a,b*] = a by A2, COMPLEX1:def_1; ::_thesis: verum
end;
end;
end;
percases ( b = 0 or b <> 0 ) ;
supposeA3: b = 0 ; ::_thesis: Im [*a,b*] = b
then [*a,b*] = a by ARYTM_0:def_5;
hence Im [*a,b*] = b by A3, COMPLEX1:def_2; ::_thesis: verum
end;
suppose b <> 0 ; ::_thesis: Im [*a,b*] = b
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;
A5: not [*a,b*] in REAL by A4, ARYTM_0:8;
f . 1 = b by A4, FUNCT_4:63;
hence Im [*a,b*] = b by A5, COMPLEX1:def_2; ::_thesis: verum
end;
end;
end;
Lm9: for z being complex number holds [*(Re z),(Im z)*] = z
proof
let z be complex number ; ::_thesis: [*(Re z),(Im z)*] = z
A1: z in COMPLEX by XCMPLX_0:def_2;
percases ( z in REAL or not z in REAL ) ;
supposeA2: z in REAL ; ::_thesis: [*(Re z),(Im z)*] = z
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 ;
::_thesis: verum
end;
supposeA3: not z in REAL ; ::_thesis: [*(Re z),(Im z)*] = z
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 [*(Re z),(Im z)*] = z by A6, A7, A8, ARYTM_0:def_5; ::_thesis: verum
end;
end;
end;
theorem Th23: :: QUATERNI:23
for a, b, c, d being Element of REAL holds
( 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
let a, b, c, d be Element of REAL ; ::_thesis: ( Rea [*a,b,c,d*] = a & Im1 [*a,b,c,d*] = b & Im2 [*a,b,c,d*] = c & Im3 [*a,b,c,d*] = d )
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of REAL ;
thus Rea [*a,b,c,d*] = a ::_thesis: ( Im1 [*a,b,c,d*] = b & Im2 [*a,b,c,d*] = c & Im3 [*a,b,c,d*] = d )
proof
percases ( ( c = 0 & d = 0 ) or c <> 0 or d <> 0 ) ;
suppose ( c = 0 & d = 0 ) ; ::_thesis: Rea [*a,b,c,d*] = a
then A1: [*a,b,c,d*] = [*a,b*] by Lm4;
Re [*a,b*] = a by Lm8;
hence Rea [*a,b,c,d*] = a by A1, Def13; ::_thesis: verum
end;
suppose ( c <> 0 or d <> 0 ) ; ::_thesis: Rea [*a,b,c,d*] = a
then A2: [*a,b,c,d*] = (0,1,2,3) --> (a9,b9,c9,d9) by Def6;
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, Th10;
f . 0 = a by A2, Lm1, Th3;
hence Rea [*a,b,c,d*] = a by A3, Def13; ::_thesis: verum
end;
end;
end;
thus Im1 [*a,b,c,d*] = b ::_thesis: ( Im2 [*a,b,c,d*] = c & Im3 [*a,b,c,d*] = d )
proof
percases ( ( c = 0 & d = 0 ) or c <> 0 or d <> 0 ) ;
suppose ( c = 0 & d = 0 ) ; ::_thesis: Im1 [*a,b,c,d*] = b
then A4: [*a,b,c,d*] = [*a,b*] by Lm4;
Im [*a,b*] = b by Lm8;
hence Im1 [*a,b,c,d*] = b by A4, Def14; ::_thesis: verum
end;
suppose ( c <> 0 or d <> 0 ) ; ::_thesis: Im1 [*a,b,c,d*] = b
then A5: [*a,b,c,d*] = (0,1,2,3) --> (a9,b9,c9,d9) by Def6;
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, Th10;
f . 1 = b by A5, Lm1, Th3;
hence Im1 [*a,b,c,d*] = b by A6, Def14; ::_thesis: verum
end;
end;
end;
thus Im2 [*a,b,c,d*] = c ::_thesis: Im3 [*a,b,c,d*] = d
proof
percases ( ( c = 0 & d = 0 ) or c <> 0 or d <> 0 ) ;
supposeA7: ( c = 0 & d = 0 ) ; ::_thesis: Im2 [*a,b,c,d*] = c
then [*a,b,c,d*] = [*a,b*] by Lm4;
hence Im2 [*a,b,c,d*] = c by A7, Def15; ::_thesis: verum
end;
suppose ( c <> 0 or d <> 0 ) ; ::_thesis: Im2 [*a,b,c,d*] = c
then A8: [*a,b,c,d*] = (0,1,2,3) --> (a9,b9,c9,d9) by Def6;
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, Th10;
f . 2 = c by A8, Lm1, Th3;
hence Im2 [*a,b,c,d*] = c by A9, Def15; ::_thesis: verum
end;
end;
end;
percases ( ( c = 0 & d = 0 ) or c <> 0 or d <> 0 ) ;
supposeA10: ( c = 0 & d = 0 ) ; ::_thesis: Im3 [*a,b,c,d*] = d
then [*a,b,c,d*] = [*a,b*] by Lm4;
hence Im3 [*a,b,c,d*] = d by A10, Def16; ::_thesis: verum
end;
suppose ( c <> 0 or d <> 0 ) ; ::_thesis: Im3 [*a,b,c,d*] = d
then A11: [*a,b,c,d*] = (0,1,2,3) --> (a9,b9,c9,d9) by Def6;
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, Th10;
f . 3 = d by A11, Lm1, Th3;
hence Im3 [*a,b,c,d*] = d by A12, Def16; ::_thesis: verum
end;
end;
end;
theorem Th24: :: QUATERNI:24
for z being quaternion number holds z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*]
proof
let z be quaternion number ; ::_thesis: z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*]
A1: z in QUATERNION by Def2;
percases ( z in COMPLEX or not z in COMPLEX ) ;
supposeA2: z in COMPLEX ; ::_thesis: z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*]
then A3: Im2 z = 0 by Def15;
A4: Im3 z = 0 by A2, Def16;
A5: ex z9 being complex number st
( z = z9 & Rea z = Re z9 ) by A2, Def13;
consider z9 being complex number such that
A6: z = z9 and
A7: Im1 z = Im z9 by A2, Def14;
[*(Rea z),(Im1 z)*] = z9 by A5, A6, A7, Lm9;
hence z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*] by A3, A4, A6, Lm4; ::_thesis: verum
end;
supposeA8: not z in COMPLEX ; ::_thesis: z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*]
then A9: ex f being Function of 4,REAL st
( z = f & Im1 z = f . 1 ) by Def14;
A10: ex f being Function of 4,REAL st
( z = f & Rea z = f . 0 ) by A8, Def13;
A11: ex f being Function of 4,REAL st
( z = f & Im2 z = f . 2 ) by A8, Def15;
A12: ex f being Function of 4,REAL st
( z = f & Im3 z = f . 3 ) by A8, Def16;
consider a, b, c, d being Element of REAL such that
A13: z = (0,1,2,3) --> (a,b,c,d) by A9, Th22;
A14: Rea z = a by A10, A13, Lm1, Th3;
A15: Im1 z = b by A9, A13, Lm1, Th3;
A16: Im2 z = c by A11, A13, Lm1, Th3;
A17: Im3 z = d by A12, A13, Lm1, Th3;
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 A18: 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 A13, CARD_1:52, FUNCT_2:8;
( f . 2 <> 0 or f . 3 <> 0 ) by A18;
then ( c <> 0 or d <> 0 ) by A13, Lm1, Th3;
hence z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*] by A13, A14, A15, A16, A17, Def6; ::_thesis: verum
end;
end;
end;
theorem Th25: :: QUATERNI:25
for z1, z2 being quaternion number st Rea z1 = Rea z2 & Im1 z1 = Im1 z2 & Im2 z1 = Im2 z2 & Im3 z1 = Im3 z2 holds
z1 = z2
proof
let z1, z2 be quaternion number ; ::_thesis: ( Rea z1 = Rea z2 & Im1 z1 = Im1 z2 & Im2 z1 = Im2 z2 & Im3 z1 = Im3 z2 implies z1 = z2 )
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 ; ::_thesis: z1 = z2
thus z1 = [*(Rea z2),(Im1 z2),(Im2 z2),(Im3 z2)*] by A1, A2, A3, A4, Th24
.= z2 by Th24 ; ::_thesis: verum
end;
definition
func 0q -> quaternion number equals :: QUATERNI:def 17
0 ;
coherence
0 is quaternion number by Lm7;
func 1q -> quaternion number equals :: QUATERNI:def 18
1;
coherence
1 is quaternion number
proof
[*1,0,0,0*] = [*1,0*] by Lm4;
hence 1 is quaternion number by ARYTM_0:def_5; ::_thesis: verum
end;
end;
:: deftheorem defines 0q QUATERNI:def_17_:_
0q = 0 ;
:: deftheorem defines 1q QUATERNI:def_18_:_
1q = 1;
Lm10: for a, b, c, d being real number 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 number ; ::_thesis: ( (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) = 0 implies ( a = 0 & b = 0 & c = 0 & d = 0 ) )
assume A1: (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) = 0 ; ::_thesis: ( a = 0 & b = 0 & c = 0 & d = 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 ) ; ::_thesis: contradiction
percases ( a <> 0 or b <> 0 or c <> 0 or d <> 0 ) by A6;
suppose a <> 0 ; ::_thesis: contradiction
then 0 < (a ^2) + (b ^2) by A3, SQUARE_1:12, XREAL_1:34;
hence contradiction by A1, A4, A5; ::_thesis: verum
end;
suppose b <> 0 ; ::_thesis: contradiction
then 0 < (a ^2) + (b ^2) by A2, SQUARE_1:12, XREAL_1:34;
hence contradiction by A1, A4, A5; ::_thesis: verum
end;
suppose c <> 0 ; ::_thesis: contradiction
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; ::_thesis: verum
end;
suppose d <> 0 ; ::_thesis: contradiction
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; ::_thesis: verum
end;
end;
end;
theorem Th26: :: QUATERNI:26
for z being quaternion number st Rea z = 0 & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 holds
z = 0q
proof
let z be quaternion number ; ::_thesis: ( Rea z = 0 & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 implies z = 0q )
assume that
A1: Rea z = 0 and
A2: Im1 z = 0 and
A3: Im2 z = 0 and
A4: Im3 z = 0 ; ::_thesis: z = 0q
A5: Rea z = Rea [*0,0,0,0*] by A1, Th23;
A6: Im1 z = Im1 [*0,0,0,0*] by A2, Th23;
A7: Im2 z = Im2 [*0,0,0,0*] by A3, Th23;
Im3 z = Im3 [*0,0,0,0*] by A4, Th23;
hence z = 0q by A5, A6, A7, Lm7, Th25; ::_thesis: verum
end;
theorem :: QUATERNI:27
for z being quaternion number st z = 0 holds
((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) = 0
proof
let z be quaternion number ; ::_thesis: ( z = 0 implies ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) = 0 )
assume A1: z = 0 ; ::_thesis: ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) = 0
then A2: Rea z = 0 by Lm7, Th23;
A3: Im1 z = 0 by A1, Lm7, Th23;
Im2 z = 0 by A1, Lm7, Th23;
hence ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) = 0 by A1, A2, A3, Lm7, Th23; ::_thesis: verum
end;
theorem :: QUATERNI:28
for z being quaternion number st ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) = 0 holds
z = 0q
proof
let z be quaternion number ; ::_thesis: ( ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) = 0 implies z = 0q )
assume A1: ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) = 0 ; ::_thesis: z = 0q
then A2: Rea z = 0 by Lm10;
A3: Im1 z = 0 by A1, Lm10;
A4: Im2 z = 0 by A1, Lm10;
Im3 z = 0 by A1, Lm10;
hence z = 0q by A2, A3, A4, Th26; ::_thesis: verum
end;
Lm11: [*1,0,0,0*] = 1
proof
[*1,0,0,0*] = [*1,0*] by Lm4;
hence [*1,0,0,0*] = 1 by ARYTM_0:def_5; ::_thesis: verum
end;
theorem :: QUATERNI:29
( Rea 1q = 1 & Im1 1q = 0 & Im2 1q = 0 & Im3 1q = 0 ) by Lm11, Th23;
theorem Th30: :: QUATERNI:30
( Rea ** = 0 & Im1 ** = 1 & Im2 ** = 0 & Im3 ** = 0 )
proof
[*0,1*] = [*0,1,0,0*] by Lm4;
hence ( Rea ** = 0 & Im1 ** = 1 & Im2 ** = 0 & Im3 ** = 0 ) by Lm3, Th23; ::_thesis: verum
end;
theorem Th31: :: QUATERNI:31
( Rea = 0 & Im1 = 0 & Im2 = 1 & Im3 = 0 & Rea = 0 & Im1 = 0 & Im2 = 0 & Im3 = 1 ) by Th23;
Lm12: for m, n, x, y, z being quaternion number 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 number ; ::_thesis: ( z = ((m + n) + x) + y implies ( 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) ) )
assume A1: z = ((m + n) + x) + y ; ::_thesis: ( 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) )
consider m1, m2, m3, m4, n1, n2, n3, n4 being Element of 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 Def7;
consider x1, x2, x3, x4, y1, y2, y3, y4 being Element of 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 Def7;
A7: Rea m = m1 by A2, Th23;
A8: Rea n = n1 by A3, Th23;
A9: Rea x = x1 by A5, Th23;
A10: Rea y = y1 by A6, Th23;
A11: Im1 m = m2 by A2, Th23;
A12: Im1 n = n2 by A3, Th23;
A13: Im1 x = x2 by A5, Th23;
A14: Im1 y = y2 by A6, Th23;
A15: Im2 m = m3 by A2, Th23;
A16: Im2 n = n3 by A3, Th23;
A17: Im2 x = x3 by A5, Th23;
A18: Im2 y = y3 by A6, Th23;
A19: Im3 m = m4 by A2, Th23;
A20: Im3 n = n4 by A3, Th23;
A21: Im3 x = x4 by A5, Th23;
A22: Im3 y = y4 by A6, Th23;
(m + n) + x = [*((m1 + n1) + x1),((m2 + n2) + x2),((m3 + n3) + x3),((m4 + n4) + x4)*] by A4, A5, Def7;
then z = [*(((m1 + n1) + x1) + y1),(((m2 + n2) + x2) + y2),(((m3 + n3) + x3) + y3),(((m4 + n4) + x4) + y4)*] by A1, A6, Def7;
hence ( 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) ) by A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, A22, Th23; ::_thesis: verum
end;
Lm13: for x, y, z being quaternion number 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 number ; ::_thesis: ( z = x + y implies ( Rea z = (Rea x) + (Rea y) & Im1 z = (Im1 x) + (Im1 y) & Im2 z = (Im2 x) + (Im2 y) & Im3 z = (Im3 x) + (Im3 y) ) )
assume A1: z = x + y ; ::_thesis: ( Rea z = (Rea x) + (Rea y) & Im1 z = (Im1 x) + (Im1 y) & Im2 z = (Im2 x) + (Im2 y) & Im3 z = (Im3 x) + (Im3 y) )
consider x1, x2, x3, x4, y1, y2, y3, y4 being Element of 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 Def7;
A5: Rea x = x1 by A2, Th23;
A6: Rea y = y1 by A3, Th23;
A7: Im1 x = x2 by A2, Th23;
A8: Im1 y = y2 by A3, Th23;
A9: Im2 x = x3 by A2, Th23;
A10: Im2 y = y3 by A3, Th23;
A11: Im3 x = x4 by A2, Th23;
Im3 y = y4 by A3, Th23;
hence ( Rea z = (Rea x) + (Rea y) & Im1 z = (Im1 x) + (Im1 y) & Im2 z = (Im2 x) + (Im2 y) & Im3 z = (Im3 x) + (Im3 y) ) by A1, A4, A5, A6, A7, A8, A9, A10, A11, Th23; ::_thesis: verum
end;
Lm14: for z1, z2 being quaternion number holds z1 + z2 = [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*]
proof
let z1, z2 be quaternion number ; ::_thesis: z1 + z2 = [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*]
set z = [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*];
reconsider z9 = z1 + z2 as quaternion number ;
A1: Rea [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*] = (Rea z1) + (Rea z2) by Th23
.= Rea z9 by Lm13 ;
A2: Im1 [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*] = (Im1 z1) + (Im1 z2) by Th23
.= Im1 z9 by Lm13 ;
A3: Im2 [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*] = (Im2 z1) + (Im2 z2) by Th23
.= Im2 z9 by Lm13 ;
Im3 [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*] = (Im3 z1) + (Im3 z2) by Th23
.= Im3 z9 by Lm13 ;
hence z1 + z2 = [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*] by A1, A2, A3, Th25; ::_thesis: verum
end;
Lm15: for x, y, z being quaternion number 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 number ; ::_thesis: ( z = x * y implies ( 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)) ) )
assume A1: z = x * y ; ::_thesis: ( 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)) )
consider x1, x2, x3, x4, y1, y2, y3, y4 being Element of 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 Def10;
A5: Rea x = x1 by A2, Th23;
A6: Rea y = y1 by A3, Th23;
A7: Im1 x = x2 by A2, Th23;
A8: Im1 y = y2 by A3, Th23;
A9: Im2 x = x3 by A2, Th23;
A10: Im2 y = y3 by A3, Th23;
A11: Im3 x = x4 by A2, Th23;
Im3 y = y4 by A3, Th23;
hence ( 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)) ) by A1, A4, A5, A6, A7, A8, A9, A10, A11, Th23; ::_thesis: verum
end;
Lm16: for z1, z2, z3, z4 being quaternion number holds ((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
let z1, z2, z3, z4 be quaternion number ; ::_thesis: ((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))*]
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 number ;
A1: Rea [*((((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))*] = (((Rea z1) + (Rea z2)) + (Rea z3)) + (Rea z4) by Th23
.= Rea z9 by Lm12 ;
A2: Im1 [*((((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))*] = (((Im1 z1) + (Im1 z2)) + (Im1 z3)) + (Im1 z4) by Th23
.= Im1 z9 by Lm12 ;
A3: Im2 [*((((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))*] = (((Im2 z1) + (Im2 z2)) + (Im2 z3)) + (Im2 z4) by Th23
.= Im2 z9 by Lm12 ;
Im3 [*((((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))*] = (((Im3 z1) + (Im3 z2)) + (Im3 z3)) + (Im3 z4) by Th23
.= Im3 z9 by Lm12 ;
hence ((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 A1, A2, A3, Th25; ::_thesis: verum
end;
Lm17: for z1, z2 being quaternion number holds 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
let z1, z2 be quaternion number ; ::_thesis: 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)))*]
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 number ;
A1: Rea [*(((((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)))*] = ((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2)) by Th23
.= Rea z9 by Lm15 ;
A2: Im1 [*(((((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)))*] = ((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)) by Th23
.= Im1 z9 by Lm15 ;
A3: Im2 [*(((((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)))*] = ((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2)) by Th23
.= Im2 z9 by Lm15 ;
Im3 [*(((((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)))*] = ((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2)) by Th23
.= Im3 z9 by Lm15 ;
hence 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 A1, A2, A3, Th25; ::_thesis: verum
end;
Lm18: for z1, z2 being quaternion number holds
( 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
let z1, z2 be quaternion number ; ::_thesis: ( 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)) )
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 Lm17;
hence ( 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 Th23; ::_thesis: verum
end;
theorem :: QUATERNI:32
for z1, z2, z3, z4 being quaternion number holds
( 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
let z1, z2, z3, z4 be quaternion number ; ::_thesis: ( 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) )
((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 Lm16;
hence ( 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) ) by Th23; ::_thesis: verum
end;
Lm19: for z being quaternion number
for x being Real st z = x holds
( Rea z = x & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 )
proof
let z be quaternion number ; ::_thesis: for x being Real st z = x holds
( Rea z = x & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 )
let x be Real; ::_thesis: ( z = x implies ( Rea z = x & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) )
assume A1: z = x ; ::_thesis: ( Rea z = x & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 )
A2: x = [*x,0*] by ARYTM_0:def_5;
[*x,0*] = [*x,0,0,0*] by Lm4;
hence ( Rea z = x & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) by A1, A2, Th23; ::_thesis: verum
end;
theorem :: QUATERNI:33
for z1 being quaternion number
for x being Real st z1 = x holds
( Rea (z1 * **) = 0 & Im1 (z1 * **) = x & Im2 (z1 * **) = 0 & Im3 (z1 * **) = 0 )
proof
let z1 be quaternion number ; ::_thesis: for x being Real st z1 = x holds
( Rea (z1 * **) = 0 & Im1 (z1 * **) = x & Im2 (z1 * **) = 0 & Im3 (z1 * **) = 0 )
let x be Real; ::_thesis: ( z1 = x implies ( Rea (z1 * **) = 0 & Im1 (z1 * **) = x & Im2 (z1 * **) = 0 & Im3 (z1 * **) = 0 ) )
assume A1: z1 = x ; ::_thesis: ( Rea (z1 * **) = 0 & Im1 (z1 * **) = x & Im2 (z1 * **) = 0 & Im3 (z1 * **) = 0 )
A2: Rea (z1 * **) = ((((Rea z1) * (Rea **)) - ((Im1 z1) * (Im1 **))) - ((Im2 z1) * (Im2 **))) - ((Im3 z1) * (Im3 **)) by Lm18;
A3: Im1 (z1 * **) = ((((Rea z1) * (Im1 **)) + ((Im1 z1) * (Rea **))) + ((Im2 z1) * (Im3 **))) - ((Im3 z1) * (Im2 **)) by Lm18;
A4: Im2 (z1 * **) = ((((Rea z1) * (Im2 **)) + ((Im2 z1) * (Rea **))) + ((Im3 z1) * (Im1 **))) - ((Im1 z1) * (Im3 **)) by Lm18;
Im3 (z1 * **) = ((((Rea z1) * (Im3 **)) + ((Im3 z1) * (Rea **))) + ((Im1 z1) * (Im2 **))) - ((Im2 z1) * (Im1 **)) by Lm18;
hence ( Rea (z1 * **) = 0 & Im1 (z1 * **) = x & Im2 (z1 * **) = 0 & Im3 (z1 * **) = 0 ) by A1, A2, A3, A4, Lm19, Th30; ::_thesis: verum
end;
theorem :: QUATERNI:34
for z1 being quaternion number
for x being Real st z1 = x holds
( Rea (z1 * ) = 0 & Im1 (z1 * ) = 0 & Im2 (z1 * ) = x & Im3 (z1 * ) = 0 )
proof
let z1 be quaternion number ; ::_thesis: for x being Real st z1 = x holds
( Rea (z1 * ) = 0 & Im1 (z1 * ) = 0 & Im2 (z1 * ) = x & Im3 (z1 * ) = 0 )
let x be Real; ::_thesis: ( z1 = x implies ( Rea (z1 * ) = 0 & Im1 (z1 * ) = 0 & Im2 (z1 * ) = x & Im3 (z1 * ) = 0 ) )
assume A1: z1 = x ; ::_thesis: ( Rea (z1 * ) = 0 & Im1 (z1 * ) = 0 & Im2 (z1 * ) = x & Im3 (z1 * ) = 0 )
A2: Rea (z1 * ) = ((((Rea z1) * (Rea )) - ((Im1 z1) * (Im1 ))) - ((Im2 z1) * (Im2 ))) - ((Im3 z1) * (Im3 )) by Lm18;
A3: Im1 (z1 * ) = ((((Rea z1) * (Im1 )) + ((Im1 z1) * (Rea ))) + ((Im2 z1) * (Im3 ))) - ((Im3 z1) * (Im2 )) by Lm18;
A4: Im2 (z1 * ) = ((((Rea z1) * (Im2 )) + ((Im2 z1) * (Rea ))) + ((Im3 z1) * (Im1 ))) - ((Im1 z1) * (Im3 )) by Lm18;
Im3 (z1 * ) = ((((Rea z1) * (Im3 )) + ((Im3 z1) * (Rea ))) + ((Im1 z1) * (Im2 ))) - ((Im2 z1) * (Im1 )) by Lm18;
hence ( Rea (z1 * ) = 0 & Im1 (z1 * ) = 0 & Im2 (z1 * ) = x & Im3 (z1 * ) = 0 ) by A1, A2, A3, A4, Lm19, Th31; ::_thesis: verum
end;
theorem :: QUATERNI:35
for z1 being quaternion number
for x being Real st z1 = x holds
( Rea (z1 * ) = 0 & Im1 (z1 * ) = 0 & Im2 (z1 * ) = 0 & Im3 (z1 * ) = x )
proof
let z1 be quaternion number ; ::_thesis: for x being Real st z1 = x holds
( Rea (z1 * ) = 0 & Im1 (z1 * ) = 0 & Im2 (z1 * ) = 0 & Im3 (z1 * ) = x )
let x be Real; ::_thesis: ( z1 = x implies ( Rea (z1 * ) = 0 & Im1 (z1 * ) = 0 & Im2 (z1 * ) = 0 & Im3 (z1 * ) = x ) )
assume A1: z1 = x ; ::_thesis: ( Rea (z1 * ) = 0 & Im1 (z1 * ) = 0 & Im2 (z1 * ) = 0 & Im3 (z1 * ) = x )
A2: Rea (z1 * ) = ((((Rea z1) * (Rea )) - ((Im1 z1) * (Im1 ))) - ((Im2 z1) * (Im2 ))) - ((Im3 z1) * (Im3 )) by Lm18;
A3: Im1 (z1 * *