let z be quaternion number ; :: thesis: z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*]
A1:
z in QUATERNION
by Def2;
per cases
( z in COMPLEX or not z in COMPLEX )
;
suppose A2:
z in COMPLEX
;
:: thesis: z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*]then A3:
(
Im2 z = 0 &
Im3 z = 0 )
by Def15, Def16;
consider z' being
complex number such that A4:
z = z'
and A5:
Rea z = Re z'
by A2, Def13;
consider z' being
complex number such that A6:
z = z'
and A7:
Im1 z = Im z'
by A2, Def14;
[*(Rea z),(Im1 z)*] = z'
by A4, A5, A6, A7, Lm7;
hence
z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*]
by A3, A6, Def6';
:: thesis: verum end; suppose A8:
not
z in COMPLEX
;
:: thesis: z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*]then consider f being
Function of 4,
REAL such that A9:
z = f
and A10:
Im1 z = f . 1
by Def14;
consider f being
Function of 4,
REAL such that A11:
z = f
and A12:
Rea z = f . 0
by A8, Def13;
consider f being
Function of 4,
REAL such that A13:
z = f
and A14:
Im2 z = f . 2
by A8, Def15;
consider f being
Function of 4,
REAL such that A15:
z = f
and A16:
Im3 z = f . 3
by A8, Def16;
consider a,
b,
c,
d being
Element of
REAL such that A17:
z = 0 ,1,2,3
--> a,
b,
c,
d
by A9, Th22;
A18:
Rea z = a
by A11, A12, A17, Lm1, Th3;
A19:
Im1 z = b
by A9, A10, A17, Lm1, Th3;
A20:
Im2 z = c
by A13, A14, A17, Lm1, Th3;
A21:
Im3 z = d
by A15, A16, A17, 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 A22:
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 A17, CARD_1:90, FUNCT_2:11;
(
f . 2
<> 0 or
f . 3
<> 0 )
by A22;
then
(
c <> 0 or
d <> 0 )
by A17, Lm1, Th3;
hence
z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*]
by A17, A18, A19, A20, A21, Def6;
:: thesis: verum end;