let x, y be Real; for z being Complex
for v being Element of (REAL-NS 2) st z = x + (y * <i>) & v = <*x,y*> holds
|.z.| = ||.v.||
let z be Complex; for v being Element of (REAL-NS 2) st z = x + (y * <i>) & v = <*x,y*> holds
|.z.| = ||.v.||
let v be Element of (REAL-NS 2); ( z = x + (y * <i>) & v = <*x,y*> implies |.z.| = ||.v.|| )
assume that
A1:
z = x + (y * <i>)
and
A2:
v = <*x,y*>
; |.z.| = ||.v.||
A3:
Im z = y
by A1, COMPLEX1:12;
( x in REAL & y in REAL )
by XREAL_0:def 1;
then reconsider xx = <*x,y*> as Element of REAL 2 by FINSEQ_2:101;
A4:
( |.xx.| = ||.v.|| & Re z = x )
by A1, A2, COMPLEX1:12, REAL_NS1:1;
reconsider xx1 = xx as Point of (TOP-REAL 2) by EUCLID:22;
xx1 `2 = y
by FINSEQ_1:44;
then A5:
(sqr xx) . 2 = y ^2
by VALUED_1:11;
xx1 `1 = x
by FINSEQ_1:44;
then
( len (sqr xx) = 2 & (sqr xx) . 1 = x ^2 )
by CARD_1:def 7, VALUED_1:11;
then
sqr xx = <*(x ^2),(y ^2)*>
by A5, FINSEQ_1:44;
hence
|.z.| = ||.v.||
by A4, A3, RVSUM_1:77; verum