Theorem replim 8511

Description: Reconstruct a complex number from its real and imaginary parts.

Assertion

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

Proof of Theorem replim

Step	Hyp	Ref	Expression
1		eqid 2170	. . . . 5 |- (Im` A) = (Im` A)
2		imcl 8508	. . . . . 6 |- (A e. CC -> (Im` A) e. RR)
3		opreq2 5026	. . . . . . . . . . . 12 |- (y = (Im` A) -> (_i x. y) = (_i x. (Im` A)))
4	3	opreq2d 5033	. . . . . . . . . . 11 |- (y = (Im` A) -> (x + (_i x. y)) = (x + (_i x. (Im` A))))
5	4	eqeq2d 2181	. . . . . . . . . 10 |- (y = (Im` A) -> (A = (x + (_i x. y)) <-> A = (x + (_i x. (Im` A)))))
6	5	rexbidv 2404	. . . . . . . . 9 |- (y = (Im` A) -> (E.x e. RR A = (x + (_i x. y)) <-> E.x e. RR A = (x + (_i x. (Im` A)))))
7		eqeq2 2179	. . . . . . . . 9 |- (y = (Im` A) -> ((Im` A) = y <-> (Im` A) = (Im` A)))
8	6, 7	bibi12d 385	. . . . . . . 8 |- (y = (Im` A) -> ((E.x e. RR A = (x + (_i x. y)) <-> (Im` A) = y) <-> (E.x e. RR A = (x + (_i x. (Im` A))) <-> (Im` A) = (Im` A))))
9	8	imbi2d 380	. . . . . . 7 |- (y = (Im` A) -> ((A e. CC -> (E.x e. RR A = (x + (_i x. y)) <-> (Im` A) = y)) <-> (A e. CC -> (E.x e. RR A = (x + (_i x. (Im` A))) <-> (Im` A) = (Im` A)))))
10		creui 8493	. . . . . . . . . 10 |- (A e. CC -> E!y e. RR E.x e. RR A = (x + (_i x. y)))
11		reuuni1 3978	. . . . . . . . . 10 |- ((y e. RR /\ E!y e. RR E.x e. RR A = (x + (_i x. y))) -> (E.x e. RR A = (x + (_i x. y)) <-> U.{y e. RR | E.x e. RR A = (x + (_i x. y))} = y))
12	10, 11	sylan2 696	. . . . . . . . 9 |- ((y e. RR /\ A e. CC) -> (E.x e. RR A = (x + (_i x. y)) <-> U.{y e. RR | E.x e. RR A = (x + (_i x. y))} = y))
13		imval 8506	. . . . . . . . . . 11 |- (A e. CC -> (Im` A) = U.{y e. RR | E.x e. RR A = (x + (_i x. y))})
14	13	eqeq1d 2178	. . . . . . . . . 10 |- (A e. CC -> ((Im` A) = y <-> U.{y e. RR | E.x e. RR A = (x + (_i x. y))} = y))
15	14	adantl 544	. . . . . . . . 9 |- ((y e. RR /\ A e. CC) -> ((Im` A) = y <-> U.{y e. RR | E.x e. RR A = (x + (_i x. y))} = y))
16	12, 15	bitr4d 315	. . . . . . . 8 |- ((y e. RR /\ A e. CC) -> (E.x e. RR A = (x + (_i x. y)) <-> (Im` A) = y))
17	16	ex 494	. . . . . . 7 |- (y e. RR -> (A e. CC -> (E.x e. RR A = (x + (_i x. y)) <-> (Im` A) = y)))
18	9, 17	vtoclga 2624	. . . . . 6 |- ((Im` A) e. RR -> (A e. CC -> (E.x e. RR A = (x + (_i x. (Im` A))) <-> (Im` A) = (Im` A))))
19	2, 18	mpcom 105	. . . . 5 |- (A e. CC -> (E.x e. RR A = (x + (_i x. (Im` A))) <-> (Im` A) = (Im` A)))
20	1, 19	mpbiri 260	. . . 4 |- (A e. CC -> E.x e. RR A = (x + (_i x. (Im` A))))
21		df-rex 2390	. . . 4 |- (E.x e. RR A = (x + (_i x. (Im` A))) <-> E.x(x e. RR /\ A = (x + (_i x. (Im` A)))))
22	20, 21	sylib 263	. . 3 |- (A e. CC -> E.x(x e. RR /\ A = (x + (_i x. (Im` A)))))
23		eqid 2170	. . . . 5 |- (Re` A) = (Re` A)
24		recl 8507	. . . . . 6 |- (A e. CC -> (Re` A) e. RR)
25		opreq1 5025	. . . . . . . . . . 11 |- (x = (Re` A) -> (x + (_i x. y)) = ((Re` A) + (_i x. y)))
26	25	eqeq2d 2181	. . . . . . . . . 10 |- (x = (Re` A) -> (A = (x + (_i x. y)) <-> A = ((Re` A) + (_i x. y))))
27	26	rexbidv 2404	. . . . . . . . 9 |- (x = (Re` A) -> (E.y e. RR A = (x + (_i x. y)) <-> E.y e. RR A = ((Re` A) + (_i x. y))))
28		eqeq2 2179	. . . . . . . . 9 |- (x = (Re` A) -> ((Re` A) = x <-> (Re` A) = (Re` A)))
29	27, 28	bibi12d 385	. . . . . . . 8 |- (x = (Re` A) -> ((E.y e. RR A = (x + (_i x. y)) <-> (Re` A) = x) <-> (E.y e. RR A = ((Re` A) + (_i x. y)) <-> (Re` A) = (Re` A))))
30	29	imbi2d 380	. . . . . . 7 |- (x = (Re` A) -> ((A e. CC -> (E.y e. RR A = (x + (_i x. y)) <-> (Re` A) = x)) <-> (A e. CC -> (E.y e. RR A = ((Re` A) + (_i x. y)) <-> (Re` A) = (Re` A)))))
31		creur 8492	. . . . . . . . . 10 |- (A e. CC -> E!x e. RR E.y e. RR A = (x + (_i x. y)))
32		reuuni1 3978	. . . . . . . . . 10 |- ((x e. RR /\ E!x e. RR E.y e. RR A = (x + (_i x. y))) -> (E.y e. RR A = (x + (_i x. y)) <-> U.{x e. RR | E.y e. RR A = (x + (_i x. y))} = x))
33	31, 32	sylan2 696	. . . . . . . . 9 |- ((x e. RR /\ A e. CC) -> (E.y e. RR A = (x + (_i x. y)) <-> U.{x e. RR | E.y e. RR A = (x + (_i x. y))} = x))
34		reval 8505	. . . . . . . . . . 11 |- (A e. CC -> (Re` A) = U.{x e. RR | E.y e. RR A = (x + (_i x. y))})
35	34	eqeq1d 2178	. . . . . . . . . 10 |- (A e. CC -> ((Re` A) = x <-> U.{x e. RR | E.y e. RR A = (x + (_i x. y))} = x))
36	35	adantl 544	. . . . . . . . 9 |- ((x e. RR /\ A e. CC) -> ((Re` A) = x <-> U.{x e. RR | E.y e. RR A = (x + (_i x. y))} = x))
37	33, 36	bitr4d 315	. . . . . . . 8 |- ((x e. RR /\ A e. CC) -> (E.y e. RR A = (x + (_i x. y)) <-> (Re` A) = x))
38	37	ex 494	. . . . . . 7 |- (x e. RR -> (A e. CC -> (E.y e. RR A = (x + (_i x. y)) <-> (Re` A) = x)))
39	30, 38	vtoclga 2624	. . . . . 6 |- ((Re` A) e. RR -> (A e. CC -> (E.y e. RR A = ((Re` A) + (_i x. y)) <-> (Re` A) = (Re` A))))
40	24, 39	mpcom 105	. . . . 5 |- (A e. CC -> (E.y e. RR A = ((Re` A) + (_i x. y)) <-> (Re` A) = (Re` A)))
41	23, 40	mpbiri 260	. . . 4 |- (A e. CC -> E.y e. RR A = ((Re` A) + (_i x. y)))
42		df-rex 2390	. . . 4 |- (E.y e. RR A = ((Re` A) + (_i x. y)) <-> E.y(y e. RR /\ A = ((Re` A) + (_i x. y))))
43	41, 42	sylib 263	. . 3 |- (A e. CC -> E.y(y e. RR /\ A = ((Re` A) + (_i x. y))))
44		an4 939	. . . . 5 |- (((x e. RR /\ y e. RR) /\ (A = (x + (_i x. (Im` A))) /\ A = ((Re` A) + (_i x. y)))) <-> ((x e. RR /\ A = (x + (_i x. (Im` A)))) /\ (y e. RR /\ A = ((Re` A) + (_i x. y)))))
45	44	2exbii 1717	. . . 4 |- (E.xE.y((x e. RR /\ y e. RR) /\ (A = (x + (_i x. (Im` A))) /\ A = ((Re` A) + (_i x. y)))) <-> E.xE.y((x e. RR /\ A = (x + (_i x. (Im` A)))) /\ (y e. RR /\ A = ((Re` A) + (_i x. y)))))
46		eeanv 2003	. . . 4 |- (E.xE.y((x e. RR /\ A = (x + (_i x. (Im` A)))) /\ (y e. RR /\ A = ((Re` A) + (_i x. y)))) <-> (E.x(x e. RR /\ A = (x + (_i x. (Im` A)))) /\ E.y(y e. RR /\ A = ((Re` A) + (_i x. y)))))
47	45, 46	bitri 306	. . 3 |- (E.xE.y((x e. RR /\ y e. RR) /\ (A = (x + (_i x. (Im` A))) /\ A = ((Re` A) + (_i x. y)))) <-> (E.x(x e. RR /\ A = (x + (_i x. (Im` A)))) /\ E.y(y e. RR /\ A = ((Re` A) + (_i x. y)))))
48	22, 43, 47	sylanbrc 760	. 2 |- (A e. CC -> E.xE.y((x e. RR /\ y e. RR) /\ (A = (x + (_i x. (Im` A))) /\ A = ((Re` A) + (_i x. y)))))
49		simprrl 877	. . . . 5 |- ((A e. CC /\ ((x e. RR /\ y e. RR) /\ (A = (x + (_i x. (Im` A))) /\ A = ((Re` A) + (_i x. y))))) -> A = (x + (_i x. (Im` A))))
50		eqtr2 2188	. . . . . . . . 9 |- ((A = (x + (_i x. (Im` A))) /\ A = ((Re` A) + (_i x. y))) -> (x + (_i x. (Im` A))) = ((Re` A) + (_i x. y)))
51	2	a1d 18	. . . . . . . . . . . . 13 |- (A e. CC -> (x e. RR -> (Im` A) e. RR))
52	51	ancld 609	. . . . . . . . . . . 12 |- (A e. CC -> (x e. RR -> (x e. RR /\ (Im` A) e. RR)))
53	24	a1d 18	. . . . . . . . . . . . 13 |- (A e. CC -> (y e. RR -> (Re` A) e. RR))
54	53	ancrd 611	. . . . . . . . . . . 12 |- (A e. CC -> (y e. RR -> ((Re` A) e. RR /\ y e. RR)))
55	52, 54	anim12d 629	. . . . . . . . . . 11 |- (A e. CC -> ((x e. RR /\ y e. RR) -> ((x e. RR /\ (Im` A) e. RR) /\ ((Re` A) e. RR /\ y e. RR))))
56	55	imp 489	. . . . . . . . . 10 |- ((A e. CC /\ (x e. RR /\ y e. RR)) -> ((x e. RR /\ (Im` A) e. RR) /\ ((Re` A) e. RR /\ y e. RR)))
57		cru 8488	. . . . . . . . . 10 |- (((x e. RR /\ (Im` A) e. RR) /\ ((Re` A) e. RR /\ y e. RR)) -> ((x + (_i x. (Im` A))) = ((Re` A) + (_i x. y)) <-> (x = (Re` A) /\ (Im` A) = y)))
58	56, 57	syl 13	. . . . . . . . 9 |- ((A e. CC /\ (x e. RR /\ y e. RR)) -> ((x + (_i x. (Im` A))) = ((Re` A) + (_i x. y)) <-> (x = (Re` A) /\ (Im` A) = y)))
59	50, 58	syl5ib 274	. . . . . . . 8 |- ((A e. CC /\ (x e. RR /\ y e. RR)) -> ((A = (x + (_i x. (Im` A))) /\ A = ((Re` A) + (_i x. y))) -> (x = (Re` A) /\ (Im` A) = y)))
60	59	impr 688	. . . . . . 7 |- ((A e. CC /\ ((x e. RR /\ y e. RR) /\ (A = (x + (_i x. (Im` A))) /\ A = ((Re` A) + (_i x. y))))) -> (x = (Re` A) /\ (Im` A) = y))
61	60	simpld 536	. . . . . 6 |- ((A e. CC /\ ((x e. RR /\ y e. RR) /\ (A = (x + (_i x. (Im` A))) /\ A = ((Re` A) + (_i x. y))))) -> x = (Re` A))
62	61	opreq1d 5032	. . . . 5 |- ((A e. CC /\ ((x e. RR /\ y e. RR) /\ (A = (x + (_i x. (Im` A))) /\ A = ((Re` A) + (_i x. y))))) -> (x + (_i x. (Im` A))) = ((Re` A) + (_i x. (Im` A))))
63	49, 62	eqtrd 2202	. . . 4 |- ((A e. CC /\ ((x e. RR /\ y e. RR) /\ (A = (x + (_i x. (Im` A))) /\ A = ((Re` A) + (_i x. y))))) -> A = ((Re` A) + (_i x. (Im` A))))
64	63	ex 494	. . 3 |- (A e. CC -> (((x e. RR /\ y e. RR) /\ (A = (x + (_i x. (Im` A))) /\ A = ((Re` A) + (_i x. y)))) -> A = ((Re` A) + (_i x. (Im` A)))))
65	64	19.23advv 1974	. 2 |- (A e. CC -> (E.xE.y((x e. RR /\ y e. RR) /\ (A = (x + (_i x. (Im` A))) /\ A = ((Re` A) + (_i x. y)))) -> A = ((Re` A) + (_i x. (Im` A)))))
66	48, 65	mpd 11	1 |- (A e. CC -> A = ((Re` A) + (_i x. (Im` A))))

Syntax hints:   -> wi 3   <-> wb 231   /\ wa 433   = wceq 1615   e. wcel 1617  E.wex 1644  E.wrex 2386  E!wreu 2387  {crab 2388  U.cuni 3398  ` cfv 4163  (class class class)co 5020  CCcc 6827  RRcr 6828  _ici 6831   + caddc 6832   x. cmul 6834  Recre 8497  Imcim 8498

This theorem is referenced by:  replimi 8518  crre 8519  crim 8520  imre 8523  reim0 8524  reim0b 8525  rereb 8526  mulre 8527  recj 8568  imcj 8569  cj11OLD 8581  recan 8658  caucvg3ai 8936  caucvg3lem 8938  efeul 9230  absef 9265  absefib 9266  efieq1re 9267  efifolem7 11109  eff1lem 11124  eff1i 11125

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-rep 3628  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961  ax-cnex 6885  ax-resscn 6886  ax-1cn 6887  ax-icn 6888  ax-addcl 6889  ax-addrcl 6890  ax-mulcl 6891  ax-mulrcl 6892  ax-mulcom 6893  ax-addass 6894  ax-mulass 6895  ax-distr 6896  ax-i2m1 6897  ax-1ne0 6898  ax-1rid 6899  ax-rnegex 6900  ax-rrecex 6901  ax-cnre 6902  ax-pre-lttri 6903  ax-pre-lttrn 6904  ax-pre-ltadd 6905  ax-pre-mulgt0 6906

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3or 1131  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-nel 2298  df-ral 2389  df-rex 2390  df-reu 2391  df-rab 2392  df-v 2571  df-sbc 2731  df-csb 2806  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-nul 3115  df-if 3213  df-pw 3261  df-sn 3274  df-pr 3275  df-op 3278  df-uni 3399  df-br 3540  df-opab 3598  df-id 3779  df-po 3784  df-so 3796  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-f 4175  df-f1 4176  df-fo 4177  df-f1o 4178  df-fv 4179  df-opr 5022  df-oprab 5023  df-mpt 5138  df-iota 5259  df-er 5519  df-en 5631  df-dom 5632  df-sdom 5633  df-undef 5769  df-riota 5773  df-pnf 6948  df-mnf 6949  df-xr 6950  df-ltxr 6951  df-le 6952  df-sub 7111  df-neg 7113  df-div 7325  df-re 8501  df-im 8502

Copyright terms: Public domain