Theorem cjval 7808

Description: Value of the conjugate of a complex number. The value is the real part minus _i times the imaginary part. Definition 10-3.2 of [Gleason] p. 132.

Assertion

Ref	Expression
cjval	|- (A e. CC -> (*` A) = ((Re` A) - (_i x. (Im` A))))

Proof of Theorem cjval

Step	Hyp	Ref	Expression
1		fveq2 4492	. . 3 |- (x = A -> (Re` x) = (Re` A))
2		fveq2 4492	. . . 4 |- (x = A -> (Im` x) = (Im` A))
3	2	opreq2d 4709	. . 3 |- (x = A -> (_i x. (Im` x)) = (_i x. (Im` A)))
4	1, 3	opreq12d 4711	. 2 |- (x = A -> ((Re` x) - (_i x. (Im` x))) = ((Re` A) - (_i x. (Im` A))))
5		df-cj 7798	. 2 |- * = {<.x, y>. | (x e. CC /\ y = ((Re` x) - (_i x. (Im` x))))}
6		oprex 4718	. 2 |- ((Re` A) - (_i x. (Im` A))) e. _V
7	4, 5, 6	fvopab4 4554	1 |- (A e. CC -> (*` A) = ((Re` A) - (_i x. (Im` A))))

Syntax hints:   -> wi 3   = wceq 1136   e. wcel 1138  ` cfv 3809  (class class class)co 4695  CCcc 6180  _ici 6184   x. cmul 6187   - cmin 6241  Recre 7792  Imcim 7793  *ccj 7794

This theorem is referenced by:  cjcl 7809  cjcji 7823  cjrebi 7826  recji 7827  imcji 7828  cjaddi 7833  cjmuli 7834  cjnegi 7842  addcji 7843  recj 7863  imcj 7864  cji 7872  cj11OLD 7876  cjcncf 8335

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-13 1149  ax-14 1150  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702  ax-sep 3253  ax-nul 3260  ax-pow 3296  ax-pr 3339  ax-un 3601

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-ex 1165  df-sb 1374  df-eu 1613  df-mo 1614  df-clab 1709  df-cleq 1714  df-clel 1717  df-ne 1856  df-rex 1944  df-v 2127  df-dif 2430  df-un 2433  df-in 2436  df-ss 2438  df-nul 2702  df-pw 2859  df-sn 2873  df-pr 2874  df-op 2877  df-uni 3000  df-br 3159  df-opab 3214  df-id 3401  df-xp 3811  df-rel 3812  df-cnv 3813  df-co 3814  df-dm 3815  df-rn 3816  df-res 3817  df-ima 3818  df-fun 3819  df-fv 3825  df-opr 4697  df-cj 7798

Copyright terms: Public domain