Theorem cjvalt 6646

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
cjvalt	|- (A e. CC -> (*` A) = ((Re` A) - (i x. (Im` A))))

Proof of Theorem cjvalt

Step	Hyp	Ref	Expression
1		fveq2 3663	. . 3 |- (x = A -> (Re` x) = (Re` A))
2		fveq2 3663	. . . 4 |- (x = A -> (Im` x) = (Im` A))
3	2	opreq2d 3915	. . 3 |- (x = A -> (i x. (Im` x)) = (i x. (Im` A)))
4	1, 3	opreq12d 3917	. 2 |- (x = A -> ((Re` x) - (i x. (Im` x))) = ((Re` A) - (i x. (Im` A))))
5		df-cj 6635	. 2 |- * = {<.x, y>. | (x e. CC /\ y = ((Re` x) - (i x. (Im` x))))}
6		oprex 3922	. 2 |- ((Re` A) - (i x. (Im` A))) e. V
7	4, 5, 6	fvopab4 3719	1 |- (A e. CC -> (*` A) = ((Re` A) - (i x. (Im` A))))

Syntax hints:   -> wi 3   = wceq 1099   e. wcel 1105  ` cfv 3145  (class class class)co 3902  CCcc 5155  ici 5159   x. cmul 5162   - cmin 5215  Recre 6629  Imcim 6630  *ccj 6631

This theorem is referenced by:  cjclt 6647  cjcj 6664  cjreb 6667  recj 6668  imcj 6669  cjadd 6674  cjmul 6675  cjneg 6683  addcj 6684  recjt 6704  imcjt 6705  cji 6713  cj11t 6716  cjcncf 7164

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-sep 2671  ax-nul 2678  ax-pow 2710  ax-pr 2747  ax-un 2830

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-rex 1626  df-v 1787  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-nul 2252  df-pw 2373  df-sn 2383  df-pr 2384  df-op 2387  df-uni 2472  df-br 2588  df-opab 2635  df-id 2797  df-xp 3147  df-rel 3148  df-cnv 3149  df-co 3150  df-dm 3151  df-rn 3152  df-res 3153  df-ima 3154  df-fun 3155  df-fv 3161  df-opr 3904  df-cj 6635

Copyright terms: Public domain