:: 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 * ) = ((((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 * ) = 0 & Im3 (z1 * ) = x ) by A1, A2, A3, A4, Lm19, Th31; ::_thesis: verum end; definition let x be Real; let y be quaternion number ; consider y1, y2, y3, y4 being Element of REAL such that A1: y = [*y1,y2,y3,y4*] by Th7; funcx + y -> set means :Def19: :: QUATERNI:def 19 ex y1, y2, y3, y4 being Element of REAL st ( y = [*y1,y2,y3,y4*] & it = [*(x + y1),y2,y3,y4*] ); existence ex b1 being set ex y1, y2, y3, y4 being Element of REAL st ( y = [*y1,y2,y3,y4*] & b1 = [*(x + y1),y2,y3,y4*] ) proof take [*(x + y1),y2,y3,y4*] ; ::_thesis: ex y1, y2, y3, y4 being Element of REAL st ( y = [*y1,y2,y3,y4*] & [*(x + y1),y2,y3,y4*] = [*(x + y1),y2,y3,y4*] ) thus ex y1, y2, y3, y4 being Element of REAL st ( y = [*y1,y2,y3,y4*] & [*(x + y1),y2,y3,y4*] = [*(x + y1),y2,y3,y4*] ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being set st ex y1, y2, y3, y4 being Element of REAL st ( y = [*y1,y2,y3,y4*] & b1 = [*(x + y1),y2,y3,y4*] ) & ex y1, y2, y3, y4 being Element of REAL st ( y = [*y1,y2,y3,y4*] & b2 = [*(x + y1),y2,y3,y4*] ) holds b1 = b2 proof let c1, c2 be number ; ::_thesis: ( ex y1, y2, y3, y4 being Element of REAL st ( y = [*y1,y2,y3,y4*] & c1 = [*(x + y1),y2,y3,y4*] ) & ex y1, y2, y3, y4 being Element of REAL st ( y = [*y1,y2,y3,y4*] & c2 = [*(x + y1),y2,y3,y4*] ) implies c1 = c2 ) given y1, y2, y3, y4 being Real such that A2: y = [*y1,y2,y3,y4*] and A3: c1 = [*(x + y1),y2,y3,y4*] ; ::_thesis: ( for y1, y2, y3, y4 being Element of REAL holds ( not y = [*y1,y2,y3,y4*] or not c2 = [*(x + y1),y2,y3,y4*] ) or c1 = c2 ) given y19, y29, y39, y49 being Real such that A4: y = [*y19,y29,y39,y49*] and A5: c2 = [*(x + y19),y29,y39,y49*] ; ::_thesis: c1 = c2 A6: y1 = y19 by A2, A4, Th12; A7: y2 = y29 by A2, A4, Th12; y3 = y39 by A2, A4, Th12; hence c1 = c2 by A2, A3, A4, A5, A6, A7, Th12; ::_thesis: verum end; end; :: deftheorem Def19 defines + QUATERNI:def_19_:_ for x being Real for y being quaternion number for b3 being set holds ( b3 = x + y iff ex y1, y2, y3, y4 being Element of REAL st ( y = [*y1,y2,y3,y4*] & b3 = [*(x + y1),y2,y3,y4*] ) ); definition let x be Real; let y be quaternion number ; funcx - y -> set equals :: QUATERNI:def 20 x + (- y); coherence x + (- y) is set ; end; :: deftheorem defines - QUATERNI:def_20_:_ for x being Real for y being quaternion number holds x - y = x + (- y); definition let x be Real; let y be quaternion number ; consider y1, y2, y3, y4 being Element of REAL such that A1: y = [*y1,y2,y3,y4*] by Th7; funcx * y -> set means :Def21: :: QUATERNI:def 21 ex y1, y2, y3, y4 being Element of REAL st ( y = [*y1,y2,y3,y4*] & it = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ); existence ex b1 being set ex y1, y2, y3, y4 being Element of REAL st ( y = [*y1,y2,y3,y4*] & b1 = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) proof take [*(x * y1),(x * y2),(x * y3),(x * y4)*] ; ::_thesis: ex y1, y2, y3, y4 being Element of REAL st ( y = [*y1,y2,y3,y4*] & [*(x * y1),(x * y2),(x * y3),(x * y4)*] = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) thus ex y1, y2, y3, y4 being Element of REAL st ( y = [*y1,y2,y3,y4*] & [*(x * y1),(x * y2),(x * y3),(x * y4)*] = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being set st ex y1, y2, y3, y4 being Element of REAL st ( y = [*y1,y2,y3,y4*] & b1 = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) & ex y1, y2, y3, y4 being Element of REAL st ( y = [*y1,y2,y3,y4*] & b2 = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) holds b1 = b2 proof let c1, c2 be number ; ::_thesis: ( ex y1, y2, y3, y4 being Element of REAL st ( y = [*y1,y2,y3,y4*] & c1 = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) & ex y1, y2, y3, y4 being Element of REAL st ( y = [*y1,y2,y3,y4*] & c2 = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) implies c1 = c2 ) given y1, y2, y3, y4 being Real such that A2: y = [*y1,y2,y3,y4*] and A3: c1 = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ; ::_thesis: ( for y1, y2, y3, y4 being Element of REAL holds ( not y = [*y1,y2,y3,y4*] or not c2 = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) or c1 = c2 ) given y19, y29, y39, y49 being Real such that A4: y = [*y19,y29,y39,y49*] and A5: c2 = [*(x * y19),(x * y29),(x * y39),(x * y49)*] ; ::_thesis: c1 = c2 A6: y1 = y19 by A2, A4, Th12; A7: y2 = y29 by A2, A4, Th12; y3 = y39 by A2, A4, Th12; hence c1 = c2 by A2, A3, A4, A5, A6, A7, Th12; ::_thesis: verum end; end; :: deftheorem Def21 defines * QUATERNI:def_21_:_ for x being Real for y being quaternion number for b3 being set holds ( b3 = x * y iff ex y1, y2, y3, y4 being Element of REAL st ( y = [*y1,y2,y3,y4*] & b3 = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) ); registration let x be Real; let z9 be quaternion number ; clusterx + z9 -> quaternion ; coherence x + z9 is quaternion proof ex y1, y2, y3, y4 being Element of REAL st ( z9 = [*y1,y2,y3,y4*] & x + z9 = [*(x + y1),y2,y3,y4*] ) by Def19; hence x + z9 is quaternion ; ::_thesis: verum end; clusterx * z9 -> quaternion ; coherence x * z9 is quaternion proof ex y1, y2, y3, y4 being Element of REAL st ( z9 = [*y1,y2,y3,y4*] & x * z9 = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) by Def21; hence x * z9 in QUATERNION ; :: according to QUATERNI:def_2 ::_thesis: verum end; clusterx - z9 -> quaternion ; coherence x - z9 is quaternion ; end; Lm20: for x, y, z, w being Real holds [*x,y,z,w*] = ((x + (y * )) + (z * )) + (w * ) proof let x, y, z, w be Real; ::_thesis: [*x,y,z,w*] = ((x + (y * )) + (z * )) + (w * ) = [*0,1,0,0*] by Lm3, Lm4; then A1: y * = [*(y * 0),(y * 1),(y * 0),(y * 0)*] by Def21 .= [*0,y,0,0*] ; A2: z * = [*(z * 0),(z * 0),(z * 1),(y * 0)*] by Def21 .= [*0,0,z,0*] ; A3: w * = [*(w * 0),(w * 0),(w * 0),(w * 1)*] by Def21 .= [*0,0,0,w*] ; x + (y * ) = [*(x + 0),y,0,0*] by A1, Def19 .= [*x,y,0,0*] ; then (x + (y * )) + (z * ) = [*(x + 0),(y + 0),(0 + z),(0 + 0)*] by A2, Def7 .= [*x,y,z,0*] ; then ((x + (y * )) + (z * )) + (w * ) = [*(x + 0),(y + 0),(0 + z),(0 + w)*] by A3, Def7; hence [*x,y,z,w*] = ((x + (y * )) + (z * )) + (w * ) ; ::_thesis: verum end; definition let z1, z2 be quaternion number ; :: original: + redefine funcz1 + z2 -> Element of QUATERNION ; coherence z1 + z2 is Element of QUATERNION by Def2; end; Lm21: 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)) * ) z1 + z2 = [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*] by Lm14; hence z1 + z2 = ((((Rea z1) + (Rea z2)) + (((Im1 z1) + (Im1 z2)) * )) + (((Im2 z1) + (Im2 z2)) * )) + (((Im3 z1) + (Im3 z2)) * ) by Lm20; ::_thesis: verum end; theorem Th36: :: QUATERNI:36 for z1, z2 being quaternion number holds ( Rea (z1 + z2) = (Rea z1) + (Rea z2) & Im1 (z1 + z2) = (Im1 z1) + (Im1 z2) & Im2 (z1 + z2) = (Im2 z1) + (Im2 z2) & Im3 (z1 + z2) = (Im3 z1) + (Im3 z2) ) proof let z1, z2 be quaternion number ; ::_thesis: ( Rea (z1 + z2) = (Rea z1) + (Rea z2) & Im1 (z1 + z2) = (Im1 z1) + (Im1 z2) & Im2 (z1 + z2) = (Im2 z1) + (Im2 z2) & Im3 (z1 + z2) = (Im3 z1) + (Im3 z2) ) z1 + z2 = [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*] by Lm14; hence ( Rea (z1 + z2) = (Rea z1) + (Rea z2) & Im1 (z1 + z2) = (Im1 z1) + (Im1 z2) & Im2 (z1 + z2) = (Im2 z1) + (Im2 z2) & Im3 (z1 + z2) = (Im3 z1) + (Im3 z2) ) by Th23; ::_thesis: verum end; definition let z1, z2 be quaternion number ; :: original: * redefine funcz1 * z2 -> Element of QUATERNION ; coherence z1 * z2 is Element of QUATERNION by Def2; end; Lm22: 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))) * ) 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 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 Lm20; ::_thesis: verum end; theorem :: QUATERNI:37 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) * ) [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*] = z by Th24; hence z = (((Rea z) + ((Im1 z) * )) + ((Im2 z) * )) + ((Im3 z) * ) by Lm20; ::_thesis: verum end; Lm23: for c being quaternion number holds c + 0q = c proof let c be quaternion number ; ::_thesis: c + 0q = c A1: 0q = [*0,0*] by ARYTM_0:def_5 .= [*0,0,0,0*] by Lm4 ; consider x, y, w, z being Element of REAL such that A2: c = [*x,y,w,z*] by Th7; c + 0q = [*(x + 0),(y + 0),(w + 0),(z + 0)*] by A1, A2, Def7 .= [*x,y,w,z*] ; hence c + 0q = c by A2; ::_thesis: verum end; Lm24: ( 0 * = 0 & 0 * = 0 & 0 * = 0 ) proof set z1 = 0 ; set z2 = ; consider y1, y2, y3, y4 being Element of REAL such that A1: ( = [*y1,y2,y3,y4*] & 0 * = [*(0 * y1),(0 * y2),(0 * y3),(0 * y4)*] ) by Def21; A2: 0 * = [*0,0*] by A1, Lm4 .= 0 by ARYTM_0:def_5 ; consider y1, y2, y3, y4 being Element of REAL such that A3: ( = [*y1,y2,y3,y4*] & 0 * = [*(0 * y1),(0 * y2),(0 * y3),(0 * y4)*] ) by Def21; A4: 0 * = [*0,0*] by A3, Lm4 .= 0 by ARYTM_0:def_5 ; consider y1, y2, y3, y4 being Element of REAL such that A5: ( = [*y1,y2,y3,y4*] & 0 * = [*(0 * y1),(0 * y2),(0 * y3),(0 * y4)*] ) by Def21; 0 * = [*0,0*] by A5, Lm4 .= 0 by ARYTM_0:def_5 ; hence ( 0 * = 0 & 0 * = 0 & 0 * = 0 ) by A2, A4; ::_thesis: verum end; theorem :: QUATERNI:38 for z1, z2 being quaternion number st Im1 z1 = 0 & Im1 z2 = 0 & Im2 z1 = 0 & Im2 z2 = 0 & Im3 z1 = 0 & Im3 z2 = 0 holds ( Rea (z1 * z2) = (Rea z1) * (Rea z2) & Im1 (z1 * z2) = ((Im2 z1) * (Im3 z2)) - ((Im3 z1) * (Im2 z2)) & Im2 (z1 * z2) = ((Im3 z1) * (Im1 z2)) - ((Im1 z1) * (Im3 z2)) & Im3 (z1 * z2) = ((Im1 z1) * (Im2 z2)) - ((Im2 z1) * (Im1 z2)) ) proof let z1, z2 be quaternion number ; ::_thesis: ( Im1 z1 = 0 & Im1 z2 = 0 & Im2 z1 = 0 & Im2 z2 = 0 & Im3 z1 = 0 & Im3 z2 = 0 implies ( Rea (z1 * z2) = (Rea z1) * (Rea z2) & Im1 (z1 * z2) = ((Im2 z1) * (Im3 z2)) - ((Im3 z1) * (Im2 z2)) & Im2 (z1 * z2) = ((Im3 z1) * (Im1 z2)) - ((Im1 z1) * (Im3 z2)) & Im3 (z1 * z2) = ((Im1 z1) * (Im2 z2)) - ((Im2 z1) * (Im1 z2)) ) ) assume A1: ( Im1 z1 = 0 & Im1 z2 = 0 & Im2 z1 = 0 & Im2 z2 = 0 & Im3 z1 = 0 & Im3 z2 = 0 ) ; ::_thesis: ( Rea (z1 * z2) = (Rea z1) * (Rea z2) & Im1 (z1 * z2) = ((Im2 z1) * (Im3 z2)) - ((Im3 z1) * (Im2 z2)) & Im2 (z1 * z2) = ((Im3 z1) * (Im1 z2)) - ((Im1 z1) * (Im3 z2)) & Im3 (z1 * z2) = ((Im1 z1) * (Im2 z2)) - ((Im2 z1) * (Im1 z2)) ) A2: z1 * z2 = (((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) + ((((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))) * )) + ((((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2))) * )) + ((((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2))) * ) by Lm22 .= (((Rea z1) * (Rea z2)) + 0q) + 0q by Lm23, Lm24, A1 .= ((Rea z1) * (Rea z2)) + 0q by Lm23 ; consider y1, y2, y3, y4 being Element of REAL such that A3: ( 0q = [*y1,y2,y3,y4*] & ((Rea z1) * (Rea z2)) + 0q = [*(((Rea z1) * (Rea z2)) + y1),y2,y3,y4*] ) by Def19; ( y1 = 0 & y2 = 0 & y3 = 0 & y4 = 0 ) by Th12, A3, Lm7; then ((Rea z1) * (Rea z2)) + 0q = [*((Rea z1) * (Rea z2)),0*] by A3, Lm4; then ((Rea z1) * (Rea z2)) + 0q = (Rea z1) * (Rea z2) by ARYTM_0:def_5; hence ( Rea (z1 * z2) = (Rea z1) * (Rea z2) & Im1 (z1 * z2) = ((Im2 z1) * (Im3 z2)) - ((Im3 z1) * (Im2 z2)) & Im2 (z1 * z2) = ((Im3 z1) * (Im1 z2)) - ((Im1 z1) * (Im3 z2)) & Im3 (z1 * z2) = ((Im1 z1) * (Im2 z2)) - ((Im2 z1) * (Im1 z2)) ) by Lm19, A2, A1; ::_thesis: verum end; theorem :: QUATERNI:39 for z1, z2 being quaternion number st Rea z1 = 0 & Rea z2 = 0 holds ( Rea (z1 * z2) = ((- ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2)) & Im1 (z1 * z2) = ((Im2 z1) * (Im3 z2)) - ((Im3 z1) * (Im2 z2)) & Im2 (z1 * z2) = ((Im3 z1) * (Im1 z2)) - ((Im1 z1) * (Im3 z2)) & Im3 (z1 * z2) = ((Im1 z1) * (Im2 z2)) - ((Im2 z1) * (Im1 z2)) ) proof let z1, z2 be quaternion number ; ::_thesis: ( Rea z1 = 0 & Rea z2 = 0 implies ( Rea (z1 * z2) = ((- ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2)) & Im1 (z1 * z2) = ((Im2 z1) * (Im3 z2)) - ((Im3 z1) * (Im2 z2)) & Im2 (z1 * z2) = ((Im3 z1) * (Im1 z2)) - ((Im1 z1) * (Im3 z2)) & Im3 (z1 * z2) = ((Im1 z1) * (Im2 z2)) - ((Im2 z1) * (Im1 z2)) ) ) assume A1: ( Rea z1 = 0 & Rea z2 = 0 ) ; ::_thesis: ( Rea (z1 * z2) = ((- ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2)) & Im1 (z1 * z2) = ((Im2 z1) * (Im3 z2)) - ((Im3 z1) * (Im2 z2)) & Im2 (z1 * z2) = ((Im3 z1) * (Im1 z2)) - ((Im1 z1) * (Im3 z2)) & Im3 (z1 * z2) = ((Im1 z1) * (Im2 z2)) - ((Im2 z1) * (Im1 z2)) ) ( 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 Lm18; hence ( Rea (z1 * z2) = ((- ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2)) & Im1 (z1 * z2) = ((Im2 z1) * (Im3 z2)) - ((Im3 z1) * (Im2 z2)) & Im2 (z1 * z2) = ((Im3 z1) * (Im1 z2)) - ((Im1 z1) * (Im3 z2)) & Im3 (z1 * z2) = ((Im1 z1) * (Im2 z2)) - ((Im2 z1) * (Im1 z2)) ) by A1; ::_thesis: verum end; theorem :: QUATERNI:40 for z being quaternion number holds ( Rea (z * z) = ((((Rea z) ^2) - ((Im1 z) ^2)) - ((Im2 z) ^2)) - ((Im3 z) ^2) & Im1 (z * z) = 2 * ((Rea z) * (Im1 z)) & Im2 (z * z) = 2 * ((Rea z) * (Im2 z)) & Im3 (z * z) = 2 * ((Rea z) * (Im3 z)) ) proof let z be quaternion number ; ::_thesis: ( Rea (z * z) = ((((Rea z) ^2) - ((Im1 z) ^2)) - ((Im2 z) ^2)) - ((Im3 z) ^2) & Im1 (z * z) = 2 * ((Rea z) * (Im1 z)) & Im2 (z * z) = 2 * ((Rea z) * (Im2 z)) & Im3 (z * z) = 2 * ((Rea z) * (Im3 z)) ) ( Rea (z * z) = ((((Rea z) * (Rea z)) - ((Im1 z) * (Im1 z))) - ((Im2 z) * (Im2 z))) - ((Im3 z) * (Im3 z)) & Im1 (z * z) = ((((Rea z) * (Im1 z)) + ((Im1 z) * (Rea z))) + ((Im2 z) * (Im3 z))) - ((Im3 z) * (Im2 z)) & Im2 (z * z) = ((((Rea z) * (Im2 z)) + ((Im2 z) * (Rea z))) + ((Im3 z) * (Im1 z))) - ((Im1 z) * (Im3 z)) & Im3 (z * z) = ((((Rea z) * (Im3 z)) + ((Im3 z) * (Rea z))) + ((Im1 z) * (Im2 z))) - ((Im2 z) * (Im1 z)) ) by Lm18; hence ( Rea (z * z) = ((((Rea z) ^2) - ((Im1 z) ^2)) - ((Im2 z) ^2)) - ((Im3 z) ^2) & Im1 (z * z) = 2 * ((Rea z) * (Im1 z)) & Im2 (z * z) = 2 * ((Rea z) * (Im2 z)) & Im3 (z * z) = 2 * ((Rea z) * (Im3 z)) ) ; ::_thesis: verum end; definition let z be quaternion number ; :: original: - redefine func - z -> Element of QUATERNION ; coherence - z is Element of QUATERNION by Def2; end; Lm25: 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)) * ) set z9 = [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]; A1: [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] = (((- (Rea z)) + ((- (Im1 z)) * )) + ((- (Im2 z)) * )) + ((- (Im3 z)) * ) by Lm20; [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] + z = [*((Rea [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Rea z)),((Im1 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im1 z)),((Im2 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im2 z)),((Im3 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im3 z))*] by Lm14 .= [*((- (Rea z)) + (Rea z)),((Im1 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im1 z)),((Im2 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im2 z)),((Im3 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im3 z))*] by Th23 .= [*0,((- (Im1 z)) + (Im1 z)),((Im2 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im2 z)),((Im3 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im3 z))*] by Th23 .= [*0,0,((- (Im2 z)) + (Im2 z)),((Im3 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im3 z))*] by Th23 .= [*0,0,0,((- (Im3 z)) + (Im3 z))*] by Th23 .= 0 by Lm7 ; hence - z = (((- (Rea z)) + ((- (Im1 z)) * )) + ((- (Im2 z)) * )) + ((- (Im3 z)) * ) by A1, Def8; ::_thesis: verum end; theorem Th41: :: QUATERNI:41 for z being quaternion number holds ( Rea (- z) = - (Rea z) & Im1 (- z) = - (Im1 z) & Im2 (- z) = - (Im2 z) & Im3 (- z) = - (Im3 z) ) proof let z be quaternion number ; ::_thesis: ( Rea (- z) = - (Rea z) & Im1 (- z) = - (Im1 z) & Im2 (- z) = - (Im2 z) & Im3 (- z) = - (Im3 z) ) - z = (((- (Rea z)) + ((- (Im1 z)) * )) + ((- (Im2 z)) * )) + ((- (Im3 z)) * ) by Lm25; then - z = [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by Lm20; hence ( Rea (- z) = - (Rea z) & Im1 (- z) = - (Im1 z) & Im2 (- z) = - (Im2 z) & Im3 (- z) = - (Im3 z) ) by Th23; ::_thesis: verum end; definition let z1, z2 be quaternion number ; :: original: - redefine funcz1 - z2 -> Element of QUATERNION ; coherence z1 - z2 is Element of QUATERNION by Def2; end; Lm26: 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)) * ) z1 - z2 = ((((Rea z1) + (Rea (- z2))) + (((Im1 z1) + (Im1 (- z2))) * )) + (((Im2 z1) + (Im2 (- z2))) * )) + (((Im3 z1) + (Im3 (- z2))) * ) by Lm21 .= ((((Rea z1) + (- (Rea z2))) + (((Im1 z1) + (Im1 (- z2))) * )) + (((Im2 z1) + (Im2 (- z2))) * )) + (((Im3 z1) + (Im3 (- z2))) * ) by Th41 .= ((((Rea z1) + (- (Rea z2))) + (((Im1 z1) - (Im1 z2)) * )) + (((Im2 z1) + (Im2 (- z2))) * )) + (((Im3 z1) + (Im3 (- z2))) * ) by Th41 .= ((((Rea z1) + (- (Rea z2))) + (((Im1 z1) - (Im1 z2)) * )) + (((Im2 z1) + (- (Im2 z2))) * )) + (((Im3 z1) + (Im3 (- z2))) * ) by Th41 .= ((((Rea z1) - (Rea z2)) + (((Im1 z1) - (Im1 z2)) * )) + (((Im2 z1) - (Im2 z2)) * )) + (((Im3 z1) - (Im3 z2)) * ) by Th41 ; hence z1 - z2 = ((((Rea z1) - (Rea z2)) + (((Im1 z1) - (Im1 z2)) * )) + (((Im2 z1) - (Im2 z2)) * )) + (((Im3 z1) - (Im3 z2)) * ) ; ::_thesis: verum end; theorem Th42: :: QUATERNI:42 for z1, z2 being quaternion number holds ( Rea (z1 - z2) = (Rea z1) - (Rea z2) & Im1 (z1 - z2) = (Im1 z1) - (Im1 z2) & Im2 (z1 - z2) = (Im2 z1) - (Im2 z2) & Im3 (z1 - z2) = (Im3 z1) - (Im3 z2) ) proof let z1, z2 be quaternion number ; ::_thesis: ( Rea (z1 - z2) = (Rea z1) - (Rea z2) & Im1 (z1 - z2) = (Im1 z1) - (Im1 z2) & Im2 (z1 - z2) = (Im2 z1) - (Im2 z2) & Im3 (z1 - z2) = (Im3 z1) - (Im3 z2) ) z1 - z2 = ((((Rea z1) - (Rea z2)) + (((Im1 z1) - (Im1 z2)) * )) + (((Im2 z1) - (Im2 z2)) * )) + (((Im3 z1) - (Im3 z2)) * ) by Lm26; then z1 - z2 = [*((Rea z1) - (Rea z2)),((Im1 z1) - (Im1 z2)),((Im2 z1) - (Im2 z2)),((Im3 z1) - (Im3 z2))*] by Lm20; hence ( Rea (z1 - z2) = (Rea z1) - (Rea z2) & Im1 (z1 - z2) = (Im1 z1) - (Im1 z2) & Im2 (z1 - z2) = (Im2 z1) - (Im2 z2) & Im3 (z1 - z2) = (Im3 z1) - (Im3 z2) ) by Th23; ::_thesis: verum end; definition let z be quaternion number ; funcz *' -> quaternion number equals :: QUATERNI:def 22 (((Rea z) + ((- (Im1 z)) * )) + ((- (Im2 z)) * )) + ((- (Im3 z)) * ); coherence (((Rea z) + ((- (Im1 z)) * )) + ((- (Im2 z)) * )) + ((- (Im3 z)) * ) is quaternion number ; end; :: deftheorem defines *' QUATERNI:def_22_:_ for z being quaternion number holds z *' = (((Rea z) + ((- (Im1 z)) * )) + ((- (Im2 z)) * )) + ((- (Im3 z)) * ); definition let z be quaternion number ; :: original: *' redefine funcz *' -> Element of QUATERNION ; coherence z *' is Element of QUATERNION ; end; theorem Th43: :: QUATERNI:43 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))*] = [*0,1,0,0*] by Lm3, Lm4; then z *' = (((Rea z) + [*((- (Im1 z)) * 0),((- (Im1 z)) * 1),((- (Im1 z)) * 0),((- (Im1 z)) * 0)*]) + ((- (Im2 z)) * )) + ((- (Im3 z)) * ) by Def21 .= (((Rea z) + [*0,(- (Im1 z)),0,0*]) + [*((- (Im2 z)) * 0),((- (Im2 z)) * 0),((- (Im2 z)) * 1),((- (Im2 z)) * 0)*]) + ((- (Im3 z)) * ) by Def21 .= (((Rea z) + [*0,(- (Im1 z)),0,0*]) + [*0,0,(- (Im2 z)),0*]) + [*((- (Im3 z)) * 0),((- (Im3 z)) * 0),((- (Im3 z)) * 0),((- (Im3 z)) * 1)*] by Def21 .= ([*((Rea z) + 0),(- (Im1 z)),0,0*] + [*0,0,(- (Im2 z)),0*]) + [*0,0,0,(- (Im3 z))*] by Def19 .= [*((Rea z) + 0),((- (Im1 z)) + 0),(0 + (- (Im2 z))),(0 + 0)*] + [*0,0,0,(- (Im3 z))*] by Def7 .= [*((Rea z) + 0),((- (Im1 z)) + 0),((- (Im2 z)) + 0),(0 + (- (Im3 z)))*] by Def7 ; hence z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] ; ::_thesis: verum end; theorem :: QUATERNI:44 for z being quaternion number holds ( Rea (z *') = Rea z & Im1 (z *') = - (Im1 z) & Im2 (z *') = - (Im2 z) & Im3 (z *') = - (Im3 z) ) proof let z be quaternion number ; ::_thesis: ( Rea (z *') = Rea z & Im1 (z *') = - (Im1 z) & Im2 (z *') = - (Im2 z) & Im3 (z *') = - (Im3 z) ) z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by Lm20; hence ( Rea (z *') = Rea z & Im1 (z *') = - (Im1 z) & Im2 (z *') = - (Im2 z) & Im3 (z *') = - (Im3 z) ) by Th23; ::_thesis: verum end; theorem :: QUATERNI:45 for z being quaternion number st z = 0 holds z *' = 0 proof let z be quaternion number ; ::_thesis: ( z = 0 implies z *' = 0 ) assume A1: z = 0 ; ::_thesis: z *' = 0 then A2: Rea z = 0 by Lm7, Th23; A3: Im1 z = 0 by A1, Lm7, Th23; A4: Im2 z = 0 by A1, Lm7, Th23; Im3 z = 0 by A1, Lm7, Th23; hence z *' = 0 by A2, A3, A4, Lm7, Th43; ::_thesis: verum end; theorem :: QUATERNI:46 for z being quaternion number st z *' = 0 holds z = 0 proof let z be quaternion number ; ::_thesis: ( z *' = 0 implies z = 0 ) assume A1: z *' = 0 ; ::_thesis: z = 0 A2: z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by Th43; A3: Rea (z *') = 0 by A1, Lm7, Th23; A4: Im1 (z *') = 0 by A1, Lm7, Th23; A5: Im2 (z *') = 0 by A1, Lm7, Th23; A6: Im3 (z *') = 0 by A1, Lm7, Th23; A7: Rea (z *') = Rea z by A2, Th23; A8: Im1 (z *') = - (Im1 z) by A2, Th23; A9: Im2 (z *') = - (Im2 z) by A2, Th23; Im3 (z *') = - (Im3 z) by A2, Th23; hence z = 0 by A3, A4, A5, A6, A7, A8, A9, Th26; ::_thesis: verum end; theorem :: QUATERNI:47 1q *' = 1q proof [*1,0*] = [*1,0,0,0*] by Lm4; then A1: 1q = [*1,0,0,0*] by ARYTM_0:def_5; A2: Rea [*1,0,0,0*] = 1 by Th23; A3: Im1 [*1,0,0,0*] = 0 by Th23; A4: Im2 [*1,0,0,0*] = 0 by Th23; Im3 [*1,0,0,0*] = 0 by Th23; hence 1q *' = 1q by A1, A2, A3, A4, Th43; ::_thesis: verum end; theorem :: QUATERNI:48 ( Rea ( *') = 0 & Im1 ( *') = - 1 & Im2 ( *') = 0 & Im3 ( *') = 0 ) proof *' = [*0,(- 1),0,0*] by Th30, Th43; hence ( Rea ( *') = 0 & Im1 ( *') = - 1 & Im2 ( *') = 0 & Im3 ( *') = 0 ) by Th23; ::_thesis: verum end; theorem :: QUATERNI:49 ( Rea ( *') = 0 & Im1 ( *') = 0 & Im2 ( *') = - 1 & Im3 ( *') = 0 ) proof *' = [*0,0,(- 1),0*] by Th31, Th43; hence ( Rea ( *') = 0 & Im1 ( *') = 0 & Im2 ( *') = - 1 & Im3 ( *') = 0 ) by Th23; ::_thesis: verum end; theorem :: QUATERNI:50 ( Rea ( *') = 0 & Im1 ( *') = 0 & Im2 ( *') = 0 & Im3 ( *') = - 1 ) proof *' = [*0,0,0,(- 1)*] by Th31, Th43; hence ( Rea ( *') = 0 & Im1 ( *') = 0 & Im2 ( *') = 0 & Im3 ( *') = - 1 ) by Th23; ::_thesis: verum end; theorem :: QUATERNI:51 *' = - by Th30, Lm25; theorem :: QUATERNI:52 *' = - by Th31, Lm25; theorem :: QUATERNI:53 *' = - by Th31, Lm25; theorem :: QUATERNI:54 for z1, z2 being quaternion number holds (z1 + z2) *' = (z1 *') + (z2 *') proof let z1, z2 be quaternion number ; ::_thesis: (z1 + z2) *' = (z1 *') + (z2 *') A1: z1 *' = [*(Rea z1),(- (Im1 z1)),(- (Im2 z1)),(- (Im3 z1))*] by Th43; A2: z2 *' = [*(Rea z2),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*] by Th43; A3: (z1 + z2) *' = [*(Rea (z1 + z2)),(- (Im1 (z1 + z2))),(- (Im2 (z1 + z2))),(- (Im3 (z1 + z2)))*] by Th43; (z1 *') + (z2 *') = [*((Rea z1) + (Rea z2)),((- (Im1 z1)) + (- (Im1 z2))),((- (Im2 z1)) + (- (Im2 z2))),((- (Im3 z1)) + (- (Im3 z2)))*] by A1, A2, Def7 .= [*(Rea (z1 + z2)),(- ((Im1 z1) + (Im1 z2))),(- ((Im2 z1) + (Im2 z2))),(- ((Im3 z1) + (Im3 z2)))*] by Th36 .= [*(Rea (z1 + z2)),(- (Im1 (z1 + z2))),(- ((Im2 z1) + (Im2 z2))),(- ((Im3 z1) + (Im3 z2)))*] by Th36 .= [*(Rea (z1 + z2)),(- (Im1 (z1 + z2))),(- (Im2 (z1 + z2))),(- ((Im3 z1) + (Im3 z2)))*] by Th36 ; hence (z1 + z2) *' = (z1 *') + (z2 *') by A3, Th36; ::_thesis: verum end; theorem Th55: :: QUATERNI:55 for z being quaternion number holds (- z) *' = - (z *') proof let z be quaternion number ; ::_thesis: (- z) *' = - (z *') A1: z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by Th43; (- z) *' = [*(Rea (- z)),(- (Im1 (- z))),(- (Im2 (- z))),(- (Im3 (- z)))*] by Th43; then (- z) *' = [*(- (Rea z)),(- (Im1 (- z))),(- (Im2 (- z))),(- (Im3 (- z)))*] by Th41 .= [*(- (Rea z)),(- (- (Im1 z))),(- (Im2 (- z))),(- (Im3 (- z)))*] by Th41 .= [*(- (Rea z)),(Im1 z),(- (- (Im2 z))),(- (Im3 (- z)))*] by Th41 .= [*(- (Rea z)),(Im1 z),(Im2 z),(- (- (Im3 z)))*] by Th41 .= [*(- (Rea z)),(Im1 z),(Im2 z),(Im3 z)*] ; then (z *') + ((- z) *') = [*((Rea z) + (- (Rea z))),((- (Im1 z)) + (Im1 z)),((- (Im2 z)) + (Im2 z)),((- (Im3 z)) + (Im3 z))*] by A1, Def7 .= 0 by Lm7 ; hence (- z) *' = - (z *') by Def8; ::_thesis: verum end; theorem :: QUATERNI:56 for z1, z2 being quaternion number holds (z1 - z2) *' = (z1 *') - (z2 *') proof let z1, z2 be quaternion number ; ::_thesis: (z1 - z2) *' = (z1 *') - (z2 *') A1: z1 *' = [*(Rea z1),(- (Im1 z1)),(- (Im2 z1)),(- (Im3 z1))*] by Th43; A2: (- z2) *' = [*(Rea (- z2)),(- (Im1 (- z2))),(- (Im2 (- z2))),(- (Im3 (- z2)))*] by Th43; A3: (z1 - z2) *' = [*(Rea (z1 - z2)),(- (Im1 (z1 - z2))),(- (Im2 (z1 - z2))),(- (Im3 (z1 - z2)))*] by Th43; A4: (z1 *') - (z2 *') = (z1 *') + ((- z2) *') by Th55 .= [*((Rea z1) + (Rea (- z2))),((- (Im1 z1)) + (- (Im1 (- z2)))),((- (Im2 z1)) + (- (Im2 (- z2)))),((- (Im3 z1)) + (- (Im3 (- z2))))*] by A1, A2, Def7 .= [*((Rea z1) + (- (Rea z2))),((- (Im1 z1)) + (- (Im1 (- z2)))),((- (Im2 z1)) + (- (Im2 (- z2)))),((- (Im3 z1)) + (- (Im3 (- z2))))*] by Th41 .= [*((Rea z1) - (Rea z2)),((- (Im1 z1)) - (- (Im1 z2))),((- (Im2 z1)) + (- (Im2 (- z2)))),((- (Im3 z1)) + (- (Im3 (- z2))))*] by Th41 .= [*((Rea z1) - (Rea z2)),((- (Im1 z1)) + (Im1 z2)),((- (Im2 z1)) - (- (Im2 z2))),((- (Im3 z1)) + (- (Im3 (- z2))))*] by Th41 .= [*((Rea z1) - (Rea z2)),((- (Im1 z1)) + (Im1 z2)),((- (Im2 z1)) + (Im2 z2)),((- (Im3 z1)) - (- (Im3 z2)))*] by Th41 .= [*((Rea z1) - (Rea z2)),((- (Im1 z1)) + (Im1 z2)),((- (Im2 z1)) + (Im2 z2)),((- (Im3 z1)) + (Im3 z2))*] ; (z1 - z2) *' = [*((Rea z1) - (Rea z2)),(- (Im1 (z1 - z2))),(- (Im2 (z1 - z2))),(- (Im3 (z1 - z2)))*] by A3, Th42 .= [*((Rea z1) - (Rea z2)),(- ((Im1 z1) - (Im1 z2))),(- (Im2 (z1 - z2))),(- (Im3 (z1 - z2)))*] by Th42 .= [*((Rea z1) - (Rea z2)),((- (Im1 z1)) + (Im1 z2)),(- ((Im2 z1) - (Im2 z2))),(- (Im3 (z1 - z2)))*] by Th42 .= [*((Rea z1) - (Rea z2)),((- (Im1 z1)) + (Im1 z2)),((- (Im2 z1)) + (Im2 z2)),(- ((Im3 z1) - (Im3 z2)))*] by Th42 ; hence (z1 - z2) *' = (z1 *') - (z2 *') by A4; ::_thesis: verum end; theorem :: QUATERNI:57 for z1, z2 being quaternion number st (z1 * z2) *' = (z1 *') * (z2 *') holds (Im2 z1) * (Im3 z2) = (Im3 z1) * (Im2 z2) proof let z1, z2 be quaternion number ; ::_thesis: ( (z1 * z2) *' = (z1 *') * (z2 *') implies (Im2 z1) * (Im3 z2) = (Im3 z1) * (Im2 z2) ) assume A1: (z1 * z2) *' = (z1 *') * (z2 *') ; ::_thesis: (Im2 z1) * (Im3 z2) = (Im3 z1) * (Im2 z2) A2: z1 *' = [*(Rea z1),(- (Im1 z1)),(- (Im2 z1)),(- (Im3 z1))*] by Th43; A3: z2 *' = [*(Rea z2),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*] by Th43; A4: (z1 * z2) *' = [*(Rea (z1 * z2)),(- (Im1 (z1 * z2))),(- (Im2 (z1 * z2))),(- (Im3 (z1 * z2)))*] by Th43; A5: (z1 *') * (z2 *') = [*(((((Rea z1) * (Rea z2)) - ((- (Im1 z1)) * (- (Im1 z2)))) - ((- (Im2 z1)) * (- (Im2 z2)))) - ((- (Im3 z1)) * (- (Im3 z2)))),(((((Rea z1) * (- (Im1 z2))) + ((- (Im1 z1)) * (Rea z2))) + ((- (Im2 z1)) * (- (Im3 z2)))) - ((- (Im3 z1)) * (- (Im2 z2)))),(((((Rea z1) * (- (Im2 z2))) + ((Rea z2) * (- (Im2 z1)))) + ((- (Im1 z2)) * (- (Im3 z1)))) - ((- (Im3 z2)) * (- (Im1 z1)))),(((((Rea z1) * (- (Im3 z2))) + ((- (Im3 z1)) * (Rea z2))) + ((- (Im1 z1)) * (- (Im2 z2)))) - ((- (Im2 z1)) * (- (Im1 z2))))*] by A2, A3, Def10 .= [*(((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))),((((- ((Rea z1) * (Im1 z2))) - ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))),((((- ((Rea z1) * (Im2 z2))) - ((Rea z2) * (Im2 z1))) + ((Im1 z2) * (Im3 z1))) - ((Im3 z2) * (Im1 z1))),((((- ((Rea z1) * (Im3 z2))) - ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2)))*] ; A6: (z1 * z2) *' = [*(((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))),(- (Im1 (z1 * z2))),(- (Im2 (z1 * z2))),(- (Im3 (z1 * z2)))*] by A4, Lm18 .= [*(((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))),(- (((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)))),(- (Im2 (z1 * z2))),(- (Im3 (z1 * z2)))*] by Lm18 .= [*(((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))),(- (((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)))),(- (((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2)))),(- (Im3 (z1 * z2)))*] by Lm18 .= [*(((((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 Lm18 .= [*(((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))),((((- ((Rea z1) * (Im1 z2))) - ((Im1 z1) * (Rea z2))) - ((Im2 z1) * (Im3 z2))) + ((Im3 z1) * (Im2 z2))),((((- ((Rea z1) * (Im2 z2))) - ((Im2 z1) * (Rea z2))) - ((Im3 z1) * (Im1 z2))) + ((Im1 z1) * (Im3 z2))),((((- ((Rea z1) * (Im3 z2))) - ((Im3 z1) * (Rea z2))) - ((Im1 z1) * (Im2 z2))) + ((Im2 z1) * (Im1 z2)))*] ; A7: Im1 ((z1 *') * (z2 *')) = (((- ((Rea z1) * (Im1 z2))) - ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)) by A5, Th23; Im1 ((z1 * z2) *') = (((- ((Rea z1) * (Im1 z2))) - ((Im1 z1) * (Rea z2))) - ((Im2 z1) * (Im3 z2))) + ((Im3 z1) * (Im2 z2)) by A6, Th23; hence (Im2 z1) * (Im3 z2) = (Im3 z1) * (Im2 z2) by A1, A7; ::_thesis: verum end; theorem :: QUATERNI:58 for z being quaternion number st Im1 z = 0 & Im2 z = 0 & Im3 z = 0 holds z *' = z proof let z be quaternion number ; ::_thesis: ( Im1 z = 0 & Im2 z = 0 & Im3 z = 0 implies z *' = z ) assume that A1: Im1 z = 0 and A2: Im2 z = 0 and A3: Im3 z = 0 ; ::_thesis: z *' = z A4: z = [*(Rea z),0,0,0*] by A1, A2, A3, Th24 .= [*(Rea z),0*] by Lm4 .= Rea z by ARYTM_0:def_5 ; z *' = [*(Rea z),0,0,0*] by A1, A2, A3, Th43 .= [*(Rea z),0*] by Lm4 .= Rea z by ARYTM_0:def_5 ; hence z *' = z by A4; ::_thesis: verum end; theorem :: QUATERNI:59 for z being quaternion number st Rea z = 0 holds z *' = - z proof let z be quaternion number ; ::_thesis: ( Rea z = 0 implies z *' = - z ) assume A1: Rea z = 0 ; ::_thesis: z *' = - z - z = (((- (Rea z)) + ((- (Im1 z)) * )) + ((- (Im2 z)) * )) + ((- (Im3 z)) * ) by Lm25; hence z *' = - z by A1; ::_thesis: verum end; theorem :: QUATERNI:60 for z being quaternion number holds ( Rea (z * (z *')) = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) & Im1 (z * (z *')) = 0 & Im2 (z * (z *')) = 0 & Im3 (z * (z *')) = 0 ) proof let z be quaternion number ; ::_thesis: ( Rea (z * (z *')) = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) & Im1 (z * (z *')) = 0 & Im2 (z * (z *')) = 0 & Im3 (z * (z *')) = 0 ) A1: z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*] by Th24; z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by Th43; then z * (z *') = [*(((((Rea z) * (Rea z)) - ((Im1 z) * (- (Im1 z)))) - ((Im2 z) * (- (Im2 z)))) - ((Im3 z) * (- (Im3 z)))),(((((Rea z) * (- (Im1 z))) + ((Im1 z) * (Rea z))) + ((Im2 z) * (- (Im3 z)))) - ((Im3 z) * (- (Im2 z)))),(((((Rea z) * (- (Im2 z))) + ((Rea z) * (Im2 z))) + ((- (Im1 z)) * (Im3 z))) - ((- (Im3 z)) * (Im1 z))),(((((Rea z) * (- (Im3 z))) + ((Im3 z) * (Rea z))) + ((Im1 z) * (- (Im2 z)))) - ((Im2 z) * (- (Im1 z))))*] by A1, Def10 .= [*(((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)),0,0,0*] ; hence ( Rea (z * (z *')) = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) & Im1 (z * (z *')) = 0 & Im2 (z * (z *')) = 0 & Im3 (z * (z *')) = 0 ) by Th23; ::_thesis: verum end; theorem :: QUATERNI:61 for z being quaternion number holds ( Rea (z + (z *')) = 2 * (Rea z) & Im1 (z + (z *')) = 0 & Im2 (z + (z *')) = 0 & Im3 (z + (z *')) = 0 ) proof let z be quaternion number ; ::_thesis: ( Rea (z + (z *')) = 2 * (Rea z) & Im1 (z + (z *')) = 0 & Im2 (z + (z *')) = 0 & Im3 (z + (z *')) = 0 ) A1: z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*] by Th24; z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by Th43; then z + (z *') = [*((Rea z) + (Rea z)),((Im1 z) + (- (Im1 z))),((Im2 z) + (- (Im2 z))),((Im3 z) + (- (Im3 z)))*] by A1, Def7 .= [*(2 * (Rea z)),0,0,0*] ; hence ( Rea (z + (z *')) = 2 * (Rea z) & Im1 (z + (z *')) = 0 & Im2 (z + (z *')) = 0 & Im3 (z + (z *')) = 0 ) by Th23; ::_thesis: verum end; theorem Th62: :: QUATERNI:62 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 = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*] by Th24; set z9 = [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]; z + [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] = [*((Rea z) + (- (Rea z))),((Im1 z) + (- (Im1 z))),((Im2 z) + (- (Im2 z))),((Im3 z) + (- (Im3 z)))*] by A1, Def7 .= 0 by Lm7 ; hence - z = [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by Def8; ::_thesis: verum end; theorem :: QUATERNI:63 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))*] A1: z1 = [*(Rea z1),(Im1 z1),(Im2 z1),(Im3 z1)*] by Th24; A2: z2 = [*(Rea z2),(Im1 z2),(Im2 z2),(Im3 z2)*] by Th24; set z9 = [*(- (Rea z2)),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*]; z2 + [*(- (Rea z2)),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*] = [*((Rea z2) + (- (Rea z2))),((Im1 z2) + (- (Im1 z2))),((Im2 z2) + (- (Im2 z2))),((Im3 z2) + (- (Im3 z2)))*] by A2, Def7 .= 0 by Lm7 ; then - z2 = [*(- (Rea z2)),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*] by Def8; hence z1 - z2 = [*((Rea z1) - (Rea z2)),((Im1 z1) - (Im1 z2)),((Im2 z1) - (Im2 z2)),((Im3 z1) - (Im3 z2))*] by A1, Def7; ::_thesis: verum end; theorem :: QUATERNI:64 for z being quaternion number holds ( Rea (z - (z *')) = 0 & Im1 (z - (z *')) = 2 * (Im1 z) & Im2 (z - (z *')) = 2 * (Im2 z) & Im3 (z - (z *')) = 2 * (Im3 z) ) proof let z be quaternion number ; ::_thesis: ( Rea (z - (z *')) = 0 & Im1 (z - (z *')) = 2 * (Im1 z) & Im2 (z - (z *')) = 2 * (Im2 z) & Im3 (z - (z *')) = 2 * (Im3 z) ) A1: z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*] by Th24; A2: z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by Th43; A3: Im1 (z *') = - (Im1 z) by A2, Th23; A4: Im2 (z *') = - (Im2 z) by A2, Th23; A5: Im3 (z *') = - (Im3 z) by A2, Th23; set zz = z *' ; - (z *') = [*(- (Rea (z *'))),(- (Im1 (z *'))),(- (Im2 (z *'))),(- (Im3 (z *')))*] by Th62; then - (z *') = [*(- (Rea z)),(Im1 z),(Im2 z),(Im3 z)*] by A2, Th23, A3, A4, A5; then z - (z *') = [*((Rea z) + (- (Rea z))),((Im1 z) + (Im1 z)),((Im2 z) + (Im2 z)),((Im3 z) + (Im3 z))*] by A1, Def7 .= [*0,(2 * (Im1 z)),(2 * (Im2 z)),(2 * (Im3 z))*] ; hence ( Rea (z - (z *')) = 0 & Im1 (z - (z *')) = 2 * (Im1 z) & Im2 (z - (z *')) = 2 * (Im2 z) & Im3 (z - (z *')) = 2 * (Im3 z) ) by Th23; ::_thesis: verum end; definition let z be quaternion number ; func|.z.| -> real number equals :: QUATERNI:def 23 sqrt (((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)); coherence sqrt (((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)) is real number ; end; :: deftheorem defines |. QUATERNI:def_23_:_ for z being quaternion number holds |.z.| = sqrt (((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)); theorem Th65: :: QUATERNI:65 |.0q.| = 0 proof A1: Rea 0q = 0 by Lm7, Th23; A2: Im1 0q = 0 by Lm7, Th23; Im2 0q = 0 by Lm7, Th23; hence |.0q.| = 0 by A1, A2, Lm7, Th23, SQUARE_1:17; ::_thesis: verum end; theorem Th66: :: QUATERNI:66 for z being quaternion number st |.z.| = 0 holds z = 0 proof let z be quaternion number ; ::_thesis: ( |.z.| = 0 implies z = 0 ) assume A1: |.z.| = 0 ; ::_thesis: z = 0 A2: 0 <= (Rea z) ^2 by XREAL_1:63; A3: 0 <= (Im1 z) ^2 by XREAL_1:63; A4: 0 <= (Im2 z) ^2 by XREAL_1:63; 0 <= (Im3 z) ^2 by XREAL_1:63; then A5: 0 = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) by A1, A2, A3, A4, SQUARE_1:25; then A6: Rea z = 0 by Lm10; A7: Im1 z = 0 by A5, Lm10; A8: Im2 z = 0 by A5, Lm10; Im3 z = 0 by A5, Lm10; hence z = 0 by A6, A7, A8, Lm7, Th24; ::_thesis: verum end; theorem Th67: :: QUATERNI:67 for z being quaternion number holds 0 <= |.z.| proof let z be quaternion number ; ::_thesis: 0 <= |.z.| A1: 0 <= (Rea z) ^2 by XREAL_1:63; A2: 0 <= (Im1 z) ^2 by XREAL_1:63; A3: 0 <= (Im2 z) ^2 by XREAL_1:63; 0 <= (Im3 z) ^2 by XREAL_1:63; hence 0 <= |.z.| by A1, A2, A3, SQUARE_1:def_2; ::_thesis: verum end; theorem :: QUATERNI:68 |.1q.| = 1 proof A1: Rea 1q = 1 by Lm11, Th23; A2: Im1 1q = 0 by Lm11, Th23; Im2 1q = 0 by Lm11, Th23; hence |.1q.| = 1 by A1, A2, Lm11, Th23, SQUARE_1:18; ::_thesis: verum end; theorem :: QUATERNI:69 |..| = 1 by Th30, SQUARE_1:18; theorem :: QUATERNI:70 |..| = 1 by Th31, SQUARE_1:18; theorem :: QUATERNI:71 |..| = 1 by Th31, SQUARE_1:18; theorem Th72: :: QUATERNI:72 for z being quaternion number holds |.(- z).| = |.z.| proof let z be quaternion number ; ::_thesis: |.(- z).| = |.z.| A1: - z = [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by Th62; then A2: Rea (- z) = - (Rea z) by Th23; A3: Im1 (- z) = - (Im1 z) by A1, Th23; A4: Im2 (- z) = - (Im2 z) by A1, Th23; Im3 (- z) = - (Im3 z) by A1, Th23; hence |.(- z).| = |.z.| by A2, A3, A4; ::_thesis: verum end; theorem Th73: :: QUATERNI:73 for z being quaternion number holds |.(z *').| = |.z.| proof let z be quaternion number ; ::_thesis: |.(z *').| = |.z.| A1: z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by Th43; then A2: Im1 (z *') = - (Im1 z) by Th23; A3: Im2 (z *') = - (Im2 z) by A1, Th23; Im3 (z *') = - (Im3 z) by A1, Th23; hence |.(z *').| = |.z.| by A1, A2, A3, Th23; ::_thesis: verum end; theorem Th74: :: QUATERNI:74 for a, b, c, d being real number holds (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) >= 0 proof let a, b, c, d be real number ; ::_thesis: (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) >= 0 A1: a ^2 >= 0 by XREAL_1:63; A2: b ^2 >= 0 by XREAL_1:63; A3: c ^2 >= 0 by XREAL_1:63; d ^2 >= 0 by XREAL_1:63; hence (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) >= 0 by A1, A2, A3; ::_thesis: verum end; Lm27: for a, b, c, d being Element of REAL holds a ^2 <= (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) proof let a, b, c, d be Element of REAL ; ::_thesis: a ^2 <= (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) A1: 0 <= c ^2 by XREAL_1:63; A2: 0 <= d ^2 by XREAL_1:63; a ^2 <= (a ^2) + (b ^2) by XREAL_1:31, XREAL_1:63; then 0 + (a ^2) <= ((a ^2) + (b ^2)) + (c ^2) by A1, XREAL_1:7; hence a ^2 <= (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) by A2, XREAL_1:7; ::_thesis: verum end; Lm28: for a, b, c, d being real number holds c ^2 <= (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) proof let a, b, c, d be real number ; ::_thesis: c ^2 <= (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) A1: 0 <= b ^2 by XREAL_1:63; A2: 0 <= d ^2 by XREAL_1:63; c ^2 <= (a ^2) + (c ^2) by XREAL_1:31, XREAL_1:63; then 0 + (c ^2) <= ((a ^2) + (c ^2)) + (b ^2) by A1, XREAL_1:7; hence c ^2 <= (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) by A2, XREAL_1:7; ::_thesis: verum end; Lm29: for d, a, b, c being Element of REAL holds d ^2 <= (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) proof let d, a, b, c be Element of REAL ; ::_thesis: d ^2 <= (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) A1: 0 <= b ^2 by XREAL_1:63; A2: 0 <= c ^2 by XREAL_1:63; d ^2 <= (a ^2) + (d ^2) by XREAL_1:31, XREAL_1:63; then 0 + (d ^2) <= ((a ^2) + (d ^2)) + (c ^2) by A2, XREAL_1:7; then 0 + (d ^2) <= (b ^2) + (((a ^2) + (d ^2)) + (c ^2)) by A1, XREAL_1:7; hence d ^2 <= (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) ; ::_thesis: verum end; Lm30: for a, b being Element of REAL st a >= b ^2 holds sqrt a >= b proof let a, b be Element of REAL ; ::_thesis: ( a >= b ^2 implies sqrt a >= b ) assume A1: a >= b ^2 ; ::_thesis: sqrt a >= b b ^2 >= 0 by XREAL_1:63; then A2: sqrt a >= sqrt (b ^2) by A1, SQUARE_1:26; percases ( b >= 0 or b < 0 ) ; suppose b >= 0 ; ::_thesis: sqrt a >= b hence sqrt a >= b by A2, SQUARE_1:22; ::_thesis: verum end; supposeA3: b < 0 ; ::_thesis: sqrt a >= b then sqrt a >= - b by A2, SQUARE_1:23; hence sqrt a >= b by A3; ::_thesis: verum end; end; end; Lm31: for a1, a2, a3, a4, a5, a6, b1, b2, b3, b4, b5, b6 being real number st a1 >= b1 & a2 >= b2 & a3 >= b3 & a4 >= b4 & a5 >= b5 & a6 >= b6 holds ((((a1 + a2) + a3) + a4) + a5) + a6 >= ((((b1 + b2) + b3) + b4) + b5) + b6 proof let a1, a2, a3, a4, a5, a6, b1, b2, b3, b4, b5, b6 be real number ; ::_thesis: ( a1 >= b1 & a2 >= b2 & a3 >= b3 & a4 >= b4 & a5 >= b5 & a6 >= b6 implies ((((a1 + a2) + a3) + a4) + a5) + a6 >= ((((b1 + b2) + b3) + b4) + b5) + b6 ) assume that A1: a1 >= b1 and A2: a2 >= b2 and A3: a3 >= b3 and A4: a4 >= b4 and A5: a5 >= b5 and A6: a6 >= b6 ; ::_thesis: ((((a1 + a2) + a3) + a4) + a5) + a6 >= ((((b1 + b2) + b3) + b4) + b5) + b6 A7: a1 + a2 >= b1 + b2 by A1, A2, XREAL_1:7; A8: a3 + a4 >= b3 + b4 by A3, A4, XREAL_1:7; A9: a5 + a6 >= b5 + b6 by A5, A6, XREAL_1:7; (a1 + a2) + (a3 + a4) >= (b1 + b2) + (b3 + b4) by A7, A8, XREAL_1:7; then ((a1 + a2) + (a3 + a4)) + (a5 + a6) >= ((b1 + b2) + (b3 + b4)) + (b5 + b6) by A9, XREAL_1:7; hence ((((a1 + a2) + a3) + a4) + a5) + a6 >= ((((b1 + b2) + b3) + b4) + b5) + b6 ; ::_thesis: verum end; Lm32: for a, b being Element of REAL st a >= 0 & b >= 0 & a ^2 >= b ^2 holds a >= b proof let a, b be Element of REAL ; ::_thesis: ( a >= 0 & b >= 0 & a ^2 >= b ^2 implies a >= b ) assume that A1: a >= 0 and A2: b >= 0 and A3: a ^2 >= b ^2 ; ::_thesis: a >= b sqrt (a ^2) >= sqrt (b ^2) by A2, A3, SQUARE_1:26; then a >= sqrt (b ^2) by A1, SQUARE_1:22; hence a >= b by A1, SQUARE_1:22; ::_thesis: verum end; Lm33: for m1, m2, m4, m3, n1, n2, n3, n4 being real number holds ((sqrt ((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2))) + (sqrt ((((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2)))) ^2 = ((((((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2)) + (n1 ^2)) + (n2 ^2)) + (n3 ^2)) + (n4 ^2)) + (2 * (sqrt (((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2)) * ((((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2))))) proof let m1, m2, m4, m3, n1, n2, n3, n4 be real number ; ::_thesis: ((sqrt ((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2))) + (sqrt ((((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2)))) ^2 = ((((((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2)) + (n1 ^2)) + (n2 ^2)) + (n3 ^2)) + (n4 ^2)) + (2 * (sqrt (((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2)) * ((((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2))))) set a = (((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2); set b = (((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2); A1: (((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2) >= 0 by Th74; A2: (((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2) >= 0 by Th74; ((sqrt ((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2))) + (sqrt ((((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2)))) ^2 = (((sqrt ((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2))) ^2) + ((2 * (sqrt ((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2)))) * (sqrt ((((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2))))) + ((sqrt ((((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2))) ^2) .= (((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2)) + ((2 * (sqrt ((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2)))) * (sqrt ((((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2))))) + ((sqrt ((((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2))) ^2) by A1, SQUARE_1:def_2 .= (((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2)) + (2 * ((sqrt ((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2))) * (sqrt ((((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2)))))) + ((((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2)) by A2, SQUARE_1:def_2 .= (((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2)) + (2 * (sqrt (((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2)) * ((((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2)))))) + ((((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2)) by A1, A2, SQUARE_1:29 ; hence ((sqrt ((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2))) + (sqrt ((((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2)))) ^2 = ((((((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2)) + (n1 ^2)) + (n2 ^2)) + (n3 ^2)) + (n4 ^2)) + (2 * (sqrt (((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2)) * ((((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2))))) ; ::_thesis: verum end; Lm34: for m1, m2, m3, m4, n1, n2, n3, n4 being real number holds (sqrt (((((m1 + n1) ^2) + ((m2 + n2) ^2)) + ((m3 + n3) ^2)) + ((m4 + n4) ^2))) ^2 = ((((m1 + n1) ^2) + ((m2 + n2) ^2)) + ((m3 + n3) ^2)) + ((m4 + n4) ^2) proof let m1, m2, m3, m4, n1, n2, n3, n4 be real number ; ::_thesis: (sqrt (((((m1 + n1) ^2) + ((m2 + n2) ^2)) + ((m3 + n3) ^2)) + ((m4 + n4) ^2))) ^2 = ((((m1 + n1) ^2) + ((m2 + n2) ^2)) + ((m3 + n3) ^2)) + ((m4 + n4) ^2) ((((m1 + n1) ^2) + ((m2 + n2) ^2)) + ((m3 + n3) ^2)) + ((m4 + n4) ^2) >= 0 by Th74; hence (sqrt (((((m1 + n1) ^2) + ((m2 + n2) ^2)) + ((m3 + n3) ^2)) + ((m4 + n4) ^2))) ^2 = ((((m1 + n1) ^2) + ((m2 + n2) ^2)) + ((m3 + n3) ^2)) + ((m4 + n4) ^2) by SQUARE_1:def_2; ::_thesis: verum end; theorem :: QUATERNI:75 for z being quaternion number holds Rea z <= |.z.| proof let z be quaternion number ; ::_thesis: Rea z <= |.z.| 0 <= (Rea z) ^2 by XREAL_1:63; then A1: sqrt ((Rea z) ^2) <= sqrt (((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)) by Lm27, SQUARE_1:26; percases ( Rea z >= 0 or Rea z < 0 ) ; suppose Rea z >= 0 ; ::_thesis: Rea z <= |.z.| hence Rea z <= |.z.| by A1, SQUARE_1:22; ::_thesis: verum end; supposeA2: Rea z < 0 ; ::_thesis: Rea z <= |.z.| then - (Rea z) <= |.z.| by A1, SQUARE_1:23; hence Rea z <= |.z.| by A2; ::_thesis: verum end; end; end; theorem :: QUATERNI:76 for z being quaternion number holds Im1 z <= |.z.| proof let z be quaternion number ; ::_thesis: Im1 z <= |.z.| 0 <= (Im1 z) ^2 by XREAL_1:63; then A1: sqrt ((Im1 z) ^2) <= sqrt (((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)) by Lm27, SQUARE_1:26; percases ( Im1 z >= 0 or Im1 z < 0 ) ; suppose Im1 z >= 0 ; ::_thesis: Im1 z <= |.z.| hence Im1 z <= |.z.| by A1, SQUARE_1:22; ::_thesis: verum end; supposeA2: Im1 z < 0 ; ::_thesis: Im1 z <= |.z.| then - (Im1 z) <= |.z.| by A1, SQUARE_1:23; hence Im1 z <= |.z.| by A2; ::_thesis: verum end; end; end; theorem :: QUATERNI:77 for z being quaternion number holds Im2 z <= |.z.| proof let z be quaternion number ; ::_thesis: Im2 z <= |.z.| 0 <= (Im2 z) ^2 by XREAL_1:63; then A1: sqrt ((Im2 z) ^2) <= sqrt (((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)) by Lm28, SQUARE_1:26; percases ( Im2 z >= 0 or Im2 z < 0 ) ; suppose Im2 z >= 0 ; ::_thesis: Im2 z <= |.z.| hence Im2 z <= |.z.| by A1, SQUARE_1:22; ::_thesis: verum end; supposeA2: Im2 z < 0 ; ::_thesis: Im2 z <= |.z.| then - (Im2 z) <= |.z.| by A1, SQUARE_1:23; hence Im2 z <= |.z.| by A2; ::_thesis: verum end; end; end; theorem :: QUATERNI:78 for z being quaternion number holds Im3 z <= |.z.| proof let z be quaternion number ; ::_thesis: Im3 z <= |.z.| 0 <= (Im3 z) ^2 by XREAL_1:63; then A1: sqrt ((Im3 z) ^2) <= sqrt (((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)) by Lm29, SQUARE_1:26; percases ( Im3 z >= 0 or Im3 z < 0 ) ; suppose Im3 z >= 0 ; ::_thesis: Im3 z <= |.z.| hence Im3 z <= |.z.| by A1, SQUARE_1:22; ::_thesis: verum end; supposeA2: Im3 z < 0 ; ::_thesis: Im3 z <= |.z.| then - (Im3 z) <= |.z.| by A1, SQUARE_1:23; hence Im3 z <= |.z.| by A2; ::_thesis: verum end; end; end; theorem Th79: :: QUATERNI:79 for z1, z2 being quaternion number holds |.(z1 + z2).| <= |.z1.| + |.z2.| proof let z1, z2 be quaternion number ; ::_thesis: |.(z1 + z2).| <= |.z1.| + |.z2.| set m1 = Rea z1; set m2 = Im1 z1; set m3 = Im2 z1; set m4 = Im3 z1; set n1 = Rea z2; set n2 = Im1 z2; set n3 = Im2 z2; set n4 = Im3 z2; set a = ((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2); set b = ((((Rea z2) ^2) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2); A1: |.z1.| >= 0 by Th67; |.z2.| >= 0 by Th67; then A2: |.z1.| + |.z2.| >= 0 by A1; A3: ((sqrt (((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2))) + (sqrt (((((Rea z2) ^2) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2)))) ^2 = (((((((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2)) + ((Rea z2) ^2)) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2)) + (2 * (sqrt ((((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2)) * (((((Rea z2) ^2) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2))))) by Lm33; A4: (sqrt ((((((Rea z1) + (Rea z2)) ^2) + (((Im1 z1) + (Im1 z2)) ^2)) + (((Im2 z1) + (Im2 z2)) ^2)) + (((Im3 z1) + (Im3 z2)) ^2))) ^2 = (((((Rea z1) + (Rea z2)) ^2) + (((Im1 z1) + (Im1 z2)) ^2)) + (((Im2 z1) + (Im2 z2)) ^2)) + (((Im3 z1) + (Im3 z2)) ^2) by Lm34; A5: Rea (z1 + z2) = (Rea z1) + (Rea z2) by Th36; A6: Im1 (z1 + z2) = (Im1 z1) + (Im1 z2) by Th36; A7: Im2 (z1 + z2) = (Im2 z1) + (Im2 z2) by Th36; A8: Im3 (z1 + z2) = (Im3 z1) + (Im3 z2) by Th36; A9: (((Rea z1) * (Im1 z2)) ^2) + (((Im1 z1) * (Rea z2)) ^2) >= (2 * ((Rea z1) * (Im1 z2))) * ((Im1 z1) * (Rea z2)) by SERIES_3:6; A10: (((Rea z1) * (Im2 z2)) ^2) + (((Im2 z1) * (Rea z2)) ^2) >= (2 * ((Rea z1) * (Im2 z2))) * ((Im2 z1) * (Rea z2)) by SERIES_3:6; A11: (((Rea z1) * (Im3 z2)) ^2) + (((Im3 z1) * (Rea z2)) ^2) >= (2 * ((Rea z1) * (Im3 z2))) * ((Im3 z1) * (Rea z2)) by SERIES_3:6; A12: (((Im1 z1) * (Im2 z2)) ^2) + (((Im2 z1) * (Im1 z2)) ^2) >= (2 * ((Im1 z1) * (Im2 z2))) * ((Im2 z1) * (Im1 z2)) by SERIES_3:6; A13: (((Im1 z1) * (Im3 z2)) ^2) + (((Im3 z1) * (Im1 z2)) ^2) >= (2 * ((Im1 z1) * (Im3 z2))) * ((Im3 z1) * (Im1 z2)) by SERIES_3:6; A14: (((Im2 z1) * (Im3 z2)) ^2) + (((Im3 z1) * (Im2 z2)) ^2) >= (2 * ((Im2 z1) * (Im3 z2))) * ((Im3 z1) * (Im2 z2)) by SERIES_3:6; set a1 = ((Rea z1) * (Im1 z2)) ^2 ; set a2 = ((Im1 z1) * (Rea z2)) ^2 ; set a3 = ((Rea z1) * (Im2 z2)) ^2 ; set a4 = ((Im2 z1) * (Rea z2)) ^2 ; set a5 = ((Rea z1) * (Im3 z2)) ^2 ; set a6 = ((Im3 z1) * (Rea z2)) ^2 ; set a7 = ((Im1 z1) * (Im2 z2)) ^2 ; set a8 = ((Im2 z1) * (Im1 z2)) ^2 ; set a9 = ((Im1 z1) * (Im3 z2)) ^2 ; set a10 = ((Im3 z1) * (Im1 z2)) ^2 ; set a11 = ((Im2 z1) * (Im3 z2)) ^2 ; set a12 = ((Im3 z1) * (Im2 z2)) ^2 ; set b1 = (2 * ((Rea z1) * (Im1 z2))) * ((Im1 z1) * (Rea z2)); set b2 = (2 * ((Rea z1) * (Im2 z2))) * ((Im2 z1) * (Rea z2)); set b3 = (2 * ((Rea z1) * (Im3 z2))) * ((Im3 z1) * (Rea z2)); set b4 = (2 * ((Im1 z1) * (Im2 z2))) * ((Im2 z1) * (Im1 z2)); set b5 = (2 * ((Im1 z1) * (Im3 z2))) * ((Im3 z1) * (Im1 z2)); set b6 = (2 * ((Im2 z1) * (Im3 z2))) * ((Im3 z1) * (Im2 z2)); ((((((((Rea z1) * (Im1 z2)) ^2) + (((Im1 z1) * (Rea z2)) ^2)) + ((((Rea z1) * (Im2 z2)) ^2) + (((Im2 z1) * (Rea z2)) ^2))) + ((((Rea z1) * (Im3 z2)) ^2) + (((Im3 z1) * (Rea z2)) ^2))) + ((((Im1 z1) * (Im2 z2)) ^2) + (((Im2 z1) * (Im1 z2)) ^2))) + ((((Im1 z1) * (Im3 z2)) ^2) + (((Im3 z1) * (Im1 z2)) ^2))) + ((((Im2 z1) * (Im3 z2)) ^2) + (((Im3 z1) * (Im2 z2)) ^2)) >= ((((((2 * ((Rea z1) * (Im1 z2))) * ((Im1 z1) * (Rea z2))) + ((2 * ((Rea z1) * (Im2 z2))) * ((Im2 z1) * (Rea z2)))) + ((2 * ((Rea z1) * (Im3 z2))) * ((Im3 z1) * (Rea z2)))) + ((2 * ((Im1 z1) * (Im2 z2))) * ((Im2 z1) * (Im1 z2)))) + ((2 * ((Im1 z1) * (Im3 z2))) * ((Im3 z1) * (Im1 z2)))) + ((2 * ((Im2 z1) * (Im3 z2))) * ((Im3 z1) * (Im2 z2))) by A9, A10, A11, A12, A13, A14, Lm31; then ((((((((((((((Rea z1) * (Im1 z2)) ^2) + (((Im1 z1) * (Rea z2)) ^2)) + (((Rea z1) * (Im2 z2)) ^2)) + (((Im2 z1) * (Rea z2)) ^2)) + (((Rea z1) * (Im3 z2)) ^2)) + (((Im3 z1) * (Rea z2)) ^2)) + (((Im1 z1) * (Im2 z2)) ^2)) + (((Im2 z1) * (Im1 z2)) ^2)) + (((Im1 z1) * (Im3 z2)) ^2)) + (((Im3 z1) * (Im1 z2)) ^2)) + (((Im2 z1) * (Im3 z2)) ^2)) + (((Im3 z1) * (Im2 z2)) ^2)) + ((((((Rea z1) * (Rea z2)) ^2) + (((Im1 z1) * (Im1 z2)) ^2)) + (((Im2 z1) * (Im2 z2)) ^2)) + (((Im3 z1) * (Im3 z2)) ^2)) >= (((((((2 * ((Rea z1) * (Im1 z2))) * ((Im1 z1) * (Rea z2))) + ((2 * ((Rea z1) * (Im2 z2))) * ((Im2 z1) * (Rea z2)))) + ((2 * ((Rea z1) * (Im3 z2))) * ((Im3 z1) * (Rea z2)))) + ((2 * ((Im1 z1) * (Im2 z2))) * ((Im2 z1) * (Im1 z2)))) + ((2 * ((Im1 z1) * (Im3 z2))) * ((Im3 z1) * (Im1 z2)))) + ((2 * ((Im2 z1) * (Im3 z2))) * ((Im3 z1) * (Im2 z2)))) + ((((((Rea z1) * (Rea z2)) ^2) + (((Im1 z1) * (Im1 z2)) ^2)) + (((Im2 z1) * (Im2 z2)) ^2)) + (((Im3 z1) * (Im3 z2)) ^2)) by XREAL_1:6; then ((((((((((((((Rea z1) * (Im1 z2)) ^2) + (((Im1 z1) * (Rea z2)) ^2)) + (((Rea z1) * (Im2 z2)) ^2)) + (((Im2 z1) * (Rea z2)) ^2)) + (((Rea z1) * (Im3 z2)) ^2)) + (((Im3 z1) * (Rea z2)) ^2)) + (((Im1 z1) * (Im2 z2)) ^2)) + (((Im2 z1) * (Im1 z2)) ^2)) + (((Im1 z1) * (Im3 z2)) ^2)) + (((Im3 z1) * (Im1 z2)) ^2)) + (((Im2 z1) * (Im3 z2)) ^2)) + (((Im3 z1) * (Im2 z2)) ^2)) + ((((((Rea z1) * (Rea z2)) ^2) + (((Im1 z1) * (Im1 z2)) ^2)) + (((Im2 z1) * (Im2 z2)) ^2)) + (((Im3 z1) * (Im3 z2)) ^2)) >= (((((Rea z1) * (Rea z2)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z1) * (Im2 z2))) + ((Im3 z1) * (Im3 z2))) ^2 ; then sqrt ((((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2)) * (((((Rea z2) ^2) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2))) >= ((((Rea z1) * (Rea z2)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z1) * (Im2 z2))) + ((Im3 z1) * (Im3 z2)) by Lm30; then 2 * (sqrt ((((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2)) * (((((Rea z2) ^2) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2)))) >= 2 * (((((Rea z1) * (Rea z2)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z1) * (Im2 z2))) + ((Im3 z1) * (Im3 z2))) by XREAL_1:64; then ((((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2)) + (((((Rea z2) ^2) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2))) + (2 * (sqrt ((((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2)) * (((((Rea z2) ^2) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2))))) >= ((((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2)) + (((((Rea z2) ^2) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2))) + (2 * (((((Rea z1) * (Rea z2)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z1) * (Im2 z2))) + ((Im3 z1) * (Im3 z2)))) by XREAL_1:6; hence |.(z1 + z2).| <= |.z1.| + |.z2.| by A2, A3, A4, A5, A6, A7, A8, Lm32; ::_thesis: verum end; theorem Th80: :: QUATERNI:80 for z1, z2 being quaternion number holds |.(z1 - z2).| <= |.z1.| + |.z2.| proof let z1, z2 be quaternion number ; ::_thesis: |.(z1 - z2).| <= |.z1.| + |.z2.| |.(z1 - z2).| <= |.z1.| + |.(- z2).| by Th79; hence |.(z1 - z2).| <= |.z1.| + |.z2.| by Th72; ::_thesis: verum end; Lm35: for z1, z2 being quaternion number holds z1 = (z1 + z2) - z2 proof let z1, z2 be quaternion number ; ::_thesis: z1 = (z1 + z2) - z2 A1: z1 = [*(Rea z1),(Im1 z1),(Im2 z1),(Im3 z1)*] by Th24; A2: z2 = [*(Rea z2),(Im1 z2),(Im2 z2),(Im3 z2)*] by Th24; A3: - z2 = [*(- (Rea z2)),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*] by Th62; z1 + z2 = [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*] by A1, A2, Def7; then (z1 + z2) - z2 = [*(((Rea z1) + (Rea z2)) - (Rea z2)),(((Im1 z1) + (Im1 z2)) - (Im1 z2)),(((Im2 z1) + (Im2 z2)) - (Im2 z2)),(((Im3 z1) + (Im3 z2)) - (Im3 z2))*] by A3, Def7; hence z1 = (z1 + z2) - z2 by Th24; ::_thesis: verum end; Lm36: for z1, z2 being quaternion number holds z1 = (z1 - z2) + z2 proof let z1, z2 be quaternion number ; ::_thesis: z1 = (z1 - z2) + z2 A1: z1 = [*(Rea z1),(Im1 z1),(Im2 z1),(Im3 z1)*] by Th24; A2: z2 = [*(Rea z2),(Im1 z2),(Im2 z2),(Im3 z2)*] by Th24; - z2 = [*(- (Rea z2)),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*] by Th62; then z1 - z2 = [*((Rea z1) + (- (Rea z2))),((Im1 z1) + (- (Im1 z2))),((Im2 z1) + (- (Im2 z2))),((Im3 z1) + (- (Im3 z2)))*] by A1, Def7; then (z1 - z2) + z2 = [*(((Rea z1) + (- (Rea z2))) + (Rea z2)),(((Im1 z1) + (- (Im1 z2))) + (Im1 z2)),(((Im2 z1) + (- (Im2 z2))) + (Im2 z2)),(((Im3 z1) + (- (Im3 z2))) + (Im3 z2))*] by A2, Def7 .= [*(((Rea z1) + (Rea z2)) - (Rea z2)),(((Im1 z1) + (Im1 z2)) - (Im1 z2)),(((Im2 z1) + (Im2 z2)) - (Im2 z2)),(((Im3 z1) + (Im3 z2)) - (Im3 z2))*] ; hence z1 = (z1 - z2) + z2 by Th24; ::_thesis: verum end; Lm37: 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))*] A1: z1 = [*(Rea z1),(Im1 z1),(Im2 z1),(Im3 z1)*] by Th24; - z2 = [*(- (Rea z2)),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*] by Th62; hence z1 - z2 = [*((Rea z1) - (Rea z2)),((Im1 z1) - (Im1 z2)),((Im2 z1) - (Im2 z2)),((Im3 z1) - (Im3 z2))*] by A1, Def7; ::_thesis: verum end; Lm38: for z1, z2 being quaternion number holds z1 - z2 = - (z2 - z1) proof let z1, z2 be quaternion number ; ::_thesis: z1 - z2 = - (z2 - z1) A1: Rea (z2 - z1) = (Rea z2) - (Rea z1) by Th42; A2: Im1 (z2 - z1) = (Im1 z2) - (Im1 z1) by Th42; A3: Im2 (z2 - z1) = (Im2 z2) - (Im2 z1) by Th42; A4: Im3 (z2 - z1) = (Im3 z2) - (Im3 z1) by Th42; A5: Rea (- (z2 - z1)) = - ((Rea z2) - (Rea z1)) by A1, Th41; A6: Im1 (- (z2 - z1)) = - ((Im1 z2) - (Im1 z1)) by A2, Th41; A7: Im2 (- (z2 - z1)) = - ((Im2 z2) - (Im2 z1)) by A3, Th41; A8: Im3 (- (z2 - z1)) = - ((Im3 z2) - (Im3 z1)) by A4, Th41; A9: Rea (z1 - z2) = (Rea z1) - (Rea z2) by Th42; A10: Im1 (z1 - z2) = (Im1 z1) - (Im1 z2) by Th42; A11: Im2 (z1 - z2) = (Im2 z1) - (Im2 z2) by Th42; Im3 (z1 - z2) = (Im3 z1) - (Im3 z2) by Th42; hence z1 - z2 = - (z2 - z1) by Th25, A9, A10, A11, A5, A6, A7, A8; ::_thesis: verum end; Lm39: for z1, z2 being quaternion number st z1 - z2 = 0 holds z1 = z2 proof let z1, z2 be quaternion number ; ::_thesis: ( z1 - z2 = 0 implies z1 = z2 ) assume A1: z1 - z2 = 0 ; ::_thesis: z1 = z2 A2: Rea (z1 - z2) = (Rea z1) - (Rea z2) by Th42; A3: Im1 (z1 - z2) = (Im1 z1) - (Im1 z2) by Th42; A4: Im2 (z1 - z2) = (Im2 z1) - (Im2 z2) by Th42; A5: Im3 (z1 - z2) = (Im3 z1) - (Im3 z2) by Th42; A6: Rea (z1 - z2) = 0 by A1, Lm7, Th23; A7: Im1 (z1 - z2) = 0 by A1, Lm7, Th23; A8: Im2 (z1 - z2) = 0 by A1, Lm7, Th23; Im3 (z1 - z2) = 0 by A1, Lm7, Th23; hence z1 = z2 by A2, A3, A4, A5, A6, A7, A8, Th25; ::_thesis: verum end; theorem :: QUATERNI:81 for z1, z2 being quaternion number holds |.z1.| - |.z2.| <= |.(z1 + z2).| proof let z1, z2 be quaternion number ; ::_thesis: |.z1.| - |.z2.| <= |.(z1 + z2).| z1 = (z1 + z2) - z2 by Lm35; then |.z1.| <= |.(z1 + z2).| + |.z2.| by Th80; hence |.z1.| - |.z2.| <= |.(z1 + z2).| by XREAL_1:20; ::_thesis: verum end; theorem Th82: :: QUATERNI:82 for z1, z2 being quaternion number holds |.z1.| - |.z2.| <= |.(z1 - z2).| proof let z1, z2 be quaternion number ; ::_thesis: |.z1.| - |.z2.| <= |.(z1 - z2).| z1 = (z1 - z2) + z2 by Lm36; then |.z1.| <= |.(z1 - z2).| + |.z2.| by Th79; hence |.z1.| - |.z2.| <= |.(z1 - z2).| by XREAL_1:20; ::_thesis: verum end; theorem Th83: :: QUATERNI:83 for z1, z2 being quaternion number holds |.(z1 - z2).| = |.(z2 - z1).| proof let z1, z2 be quaternion number ; ::_thesis: |.(z1 - z2).| = |.(z2 - z1).| thus |.(z1 - z2).| = |.(- (z2 - z1)).| by Lm38 .= |.(z2 - z1).| by Th72 ; ::_thesis: verum end; theorem :: QUATERNI:84 for z1, z2 being quaternion number holds ( |.(z1 - z2).| = 0 iff z1 = z2 ) proof let z1, z2 be quaternion number ; ::_thesis: ( |.(z1 - z2).| = 0 iff z1 = z2 ) thus ( |.(z1 - z2).| = 0 implies z1 = z2 ) by Lm39, Th66; ::_thesis: ( z1 = z2 implies |.(z1 - z2).| = 0 ) assume z1 = z2 ; ::_thesis: |.(z1 - z2).| = 0 then z1 - z2 = [*((Rea z1) - (Rea z1)),((Im1 z1) - (Im1 z1)),((Im2 z1) - (Im2 z1)),((Im3 z1) - (Im3 z1))*] by Lm37 .= 0 by Lm7 ; hence |.(z1 - z2).| = 0 by Th65; ::_thesis: verum end; Lm40: for z, z1, z2 being quaternion number holds z1 - z2 = (z1 - z) + (z - z2) proof let z, z1, z2 be quaternion number ; ::_thesis: z1 - z2 = (z1 - z) + (z - z2) A1: Rea ((z1 - z) + (z - z2)) = (Rea (z1 - z)) + (Rea (z - z2)) by Lm13 .= (Rea (z1 - z)) + ((Rea z) - (Rea z2)) by Th42 .= ((Rea z1) - (Rea z)) + ((Rea z) - (Rea z2)) by Th42 .= (Rea z1) - (Rea z2) .= Rea (z1 - z2) by Th42 ; A2: Im1 ((z1 - z) + (z - z2)) = (Im1 (z1 - z)) + (Im1 (z - z2)) by Lm13 .= (Im1 (z1 - z)) + ((Im1 z) - (Im1 z2)) by Th42 .= ((Im1 z1) - (Im1 z)) + ((Im1 z) - (Im1 z2)) by Th42 .= (Im1 z1) - (Im1 z2) .= Im1 (z1 - z2) by Th42 ; A3: Im2 ((z1 - z) + (z - z2)) = (Im2 (z1 - z)) + (Im2 (z - z2)) by Lm13 .= (Im2 (z1 - z)) + ((Im2 z) - (Im2 z2)) by Th42 .= ((Im2 z1) - (Im2 z)) + ((Im2 z) - (Im2 z2)) by Th42 .= (Im2 z1) - (Im2 z2) .= Im2 (z1 - z2) by Th42 ; Im3 ((z1 - z) + (z - z2)) = (Im3 (z1 - z)) + (Im3 (z - z2)) by Lm13 .= (Im3 (z1 - z)) + ((Im3 z) - (Im3 z2)) by Th42 .= ((Im3 z1) - (Im3 z)) + ((Im3 z) - (Im3 z2)) by Th42 .= (Im3 z1) - (Im3 z2) .= Im3 (z1 - z2) by Th42 ; hence z1 - z2 = (z1 - z) + (z - z2) by A1, A2, A3, Th25; ::_thesis: verum end; theorem :: QUATERNI:85 for z1, z2, z being quaternion number holds |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).| proof let z1, z2, z be quaternion number ; ::_thesis: |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).| |.(z1 - z2).| = |.((z1 - z) + (z - z2)).| by Lm40; hence |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).| by Th79; ::_thesis: verum end; theorem :: QUATERNI:86 for z1, z2 being quaternion number holds |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).| proof let z1, z2 be quaternion number ; ::_thesis: |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).| |.z2.| - |.z1.| <= |.(z2 - z1).| by Th82; then - (|.z1.| - |.z2.|) <= |.(z1 - z2).| by Th83; then A1: - |.(z1 - z2).| <= - (- (|.z1.| - |.z2.|)) by XREAL_1:24; |.z1.| - |.z2.| <= |.(z1 - z2).| by Th82; hence |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).| by A1, ABSVALUE:5; ::_thesis: verum end; theorem Th87: :: QUATERNI:87 for z1, z2 being quaternion number holds |.(z1 * z2).| = |.z1.| * |.z2.| proof let z1, z2 be quaternion number ; ::_thesis: |.(z1 * z2).| = |.z1.| * |.z2.| set m1 = Rea z1; set m2 = Im1 z1; set m3 = Im2 z1; set m4 = Im3 z1; set n1 = Rea z2; set n2 = Im1 z2; set n3 = Im2 z2; set n4 = Im3 z2; A1: Rea (z1 * z2) = ((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2)) by Lm18; A2: Im1 (z1 * z2) = ((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)) by Lm18; A3: Im2 (z1 * z2) = ((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2)) by Lm18; A4: Im3 (z1 * z2) = ((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2)) by Lm18; set b1 = ((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2)); set b2 = ((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)); set b3 = ((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2)); set b4 = ((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2)); A5: ((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2) >= 0 by Th74; A6: ((((Rea z2) ^2) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2) >= 0 by Th74; sqrt (((((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) ^2) + ((((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))) ^2)) + ((((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2))) ^2)) + ((((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2))) ^2)) = sqrt ((((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2)) * (((((Rea z2) ^2) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2))) ; hence |.(z1 * z2).| = |.z1.| * |.z2.| by A1, A2, A3, A4, A5, A6, SQUARE_1:29; ::_thesis: verum end; theorem :: QUATERNI:88 for z being quaternion number holds |.(z * z).| = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) proof let z be quaternion number ; ::_thesis: |.(z * z).| = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) A1: ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) >= 0 by Th74; |.z.| * |.z.| = (sqrt (((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2))) ^2 .= ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) by A1, SQUARE_1:def_2 ; hence |.(z * z).| = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) by Th87; ::_thesis: verum end; theorem :: QUATERNI:89 for z being quaternion number holds |.(z * z).| = |.(z * (z *')).| proof let z be quaternion number ; ::_thesis: |.(z * z).| = |.(z * (z *')).| thus |.(z * z).| = |.z.| * |.z.| by Th87 .= |.z.| * |.(z *').| by Th73 .= |.(z * (z *')).| by Th87 ; ::_thesis: verum end; theorem :: QUATERNI:90 for z being quaternion number st z is real holds ( Rea z = z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) proof let z be quaternion number ; ::_thesis: ( z is real implies ( Rea z = z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) ) assume z is real ; ::_thesis: ( Rea z = z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) then z in REAL by XREAL_0:def_1; hence ( Rea z = z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) by Lm19; ::_thesis: verum end; theorem :: QUATERNI:91 for x, y being Element of REAL holds [*x,y,0,0*] = [*x,y*] by Lm4; theorem :: QUATERNI:92 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)) * ) by Lm21; theorem :: QUATERNI:93 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))) * ) by Lm22; theorem :: QUATERNI:94 for z being quaternion number holds - z = (((- (Rea z)) + ((- (Im1 z)) * )) + ((- (Im2 z)) * )) + ((- (Im3 z)) * ) by Lm25; theorem :: QUATERNI:95 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)) * ) by Lm26; theorem :: QUATERNI:96 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 ) by Lm10; theorem :: QUATERNI:97 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)) ) by Lm18;