Theorem replim 7806

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		an4 561	. . . . 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)))))
2	1	2exbii 1237	. . . 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)))))
3		eeanv 1545	. . . 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)))))
4	2, 3	bitri 189	. . 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)))))
5		eqid 1721	. . . . 5 |- (Im` A) = (Im` A)
6		imcl 7803	. . . . . 6 |- (A e. CC -> (Im` A) e. RR)
7		opreq2 4701	. . . . . . . . . . . 12 |- (y = (Im` A) -> (_i x. y) = (_i x. (Im` A)))
8	7	opreq2d 4709	. . . . . . . . . . 11 |- (y = (Im` A) -> (x + (_i x. y)) = (x + (_i x. (Im` A))))
9	8	eqeq2d 1732	. . . . . . . . . 10 |- (y = (Im` A) -> (A = (x + (_i x. y)) <-> A = (x + (_i x. (Im` A)))))
10	9	rexbidv 1958	. . . . . . . . 9 |- (y = (Im` A) -> (E.x e. RR A = (x + (_i x. y)) <-> E.x e. RR A = (x + (_i x. (Im` A)))))
11		eqeq2 1730	. . . . . . . . 9 |- (y = (Im` A) -> ((Im` A) = y <-> (Im` A) = (Im` A)))
12	10, 11	bibi12d 688	. . . . . . . 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))))
13	12	imbi2d 671	. . . . . . 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)))))
14		reuuni1 3619	. . . . . . . . . 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))
15		creui 7788	. . . . . . . . . 10 |- (A e. CC -> E!y e. RR E.x e. RR A = (x + (_i x. y)))
16	14, 15	sylan2 498	. . . . . . . . 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))
17		imval 7801	. . . . . . . . . . 11 |- (A e. CC -> (Im` A) = U.{y e. RR | E.x e. RR A = (x + (_i x. y))})
18	17	eqeq1d 1729	. . . . . . . . . 10 |- (A e. CC -> ((Im` A) = y <-> U.{y e. RR | E.x e. RR A = (x + (_i x. y))} = y))
19	18	adantl 422	. . . . . . . . 9 |- ((y e. RR /\ A e. CC) -> ((Im` A) = y <-> U.{y e. RR | E.x e. RR A = (x + (_i x. y))} = y))
20	16, 19	bitr4d 587	. . . . . . . 8 |- ((y e. RR /\ A e. CC) -> (E.x e. RR A = (x + (_i x. y)) <-> (Im` A) = y))
21	20	ex 400	. . . . . . 7 |- (y e. RR -> (A e. CC -> (E.x e. RR A = (x + (_i x. y)) <-> (Im` A) = y)))
22	13, 21	vtoclga 2185	. . . . . 6 |- ((Im` A) e. RR -> (A e. CC -> (E.x e. RR A = (x + (_i x. (Im` A))) <-> (Im` A) = (Im` A))))
23	6, 22	mpcom 60	. . . . 5 |- (A e. CC -> (E.x e. RR A = (x + (_i x. (Im` A))) <-> (Im` A) = (Im` A)))
24	5, 23	mpbiri 210	. . . 4 |- (A e. CC -> E.x e. RR A = (x + (_i x. (Im` A))))
25		df-rex 1944	. . . 4 |- (E.x e. RR A = (x + (_i x. (Im` A))) <-> E.x(x e. RR /\ A = (x + (_i x. (Im` A)))))
26	24, 25	sylib 214	. . 3 |- (A e. CC -> E.x(x e. RR /\ A = (x + (_i x. (Im` A)))))
27		eqid 1721	. . . . 5 |- (Re` A) = (Re` A)
28		recl 7802	. . . . . 6 |- (A e. CC -> (Re` A) e. RR)
29		opreq1 4700	. . . . . . . . . . 11 |- (x = (Re` A) -> (x + (_i x. y)) = ((Re` A) + (_i x. y)))
30	29	eqeq2d 1732	. . . . . . . . . 10 |- (x = (Re` A) -> (A = (x + (_i x. y)) <-> A = ((Re` A) + (_i x. y))))
31	30	rexbidv 1958	. . . . . . . . 9 |- (x = (Re` A) -> (E.y e. RR A = (x + (_i x. y)) <-> E.y e. RR A = ((Re` A) + (_i x. y))))
32		eqeq2 1730	. . . . . . . . 9 |- (x = (Re` A) -> ((Re` A) = x <-> (Re` A) = (Re` A)))
33	31, 32	bibi12d 688	. . . . . . . 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))))
34	33	imbi2d 671	. . . . . . 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)))))
35		reuuni1 3619	. . . . . . . . . 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))
36		creur 7787	. . . . . . . . . 10 |- (A e. CC -> E!x e. RR E.y e. RR A = (x + (_i x. y)))
37	35, 36	sylan2 498	. . . . . . . . 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))
38		reval 7800	. . . . . . . . . . 11 |- (A e. CC -> (Re` A) = U.{x e. RR | E.y e. RR A = (x + (_i x. y))})
39	38	eqeq1d 1729	. . . . . . . . . 10 |- (A e. CC -> ((Re` A) = x <-> U.{x e. RR | E.y e. RR A = (x + (_i x. y))} = x))
40	39	adantl 422	. . . . . . . . 9 |- ((x e. RR /\ A e. CC) -> ((Re` A) = x <-> U.{x e. RR | E.y e. RR A = (x + (_i x. y))} = x))
41	37, 40	bitr4d 587	. . . . . . . 8 |- ((x e. RR /\ A e. CC) -> (E.y e. RR A = (x + (_i x. y)) <-> (Re` A) = x))
42	41	ex 400	. . . . . . 7 |- (x e. RR -> (A e. CC -> (E.y e. RR A = (x + (_i x. y)) <-> (Re` A) = x)))
43	34, 42	vtoclga 2185	. . . . . 6 |- ((Re` A) e. RR -> (A e. CC -> (E.y e. RR A = ((Re` A) + (_i x. y)) <-> (Re` A) = (Re` A))))
44	28, 43	mpcom 60	. . . . 5 |- (A e. CC -> (E.y e. RR A = ((Re` A) + (_i x. y)) <-> (Re` A) = (Re` A)))
45	27, 44	mpbiri 210	. . . 4 |- (A e. CC -> E.y e. RR A = ((Re` A) + (_i x. y)))
46		df-rex 1944	. . . 4 |- (E.y e. RR A = ((Re` A) + (_i x. y)) <-> E.y(y e. RR /\ A = ((Re` A) + (_i x. y))))
47	45, 46	sylib 214	. . 3 |- (A e. CC -> E.y(y e. RR /\ A = ((Re` A) + (_i x. y))))
48	4, 26, 47	sylanbrc 524	. 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 456	. . . . 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	6	a1d 15	. . . . . . . . . . . . 13 |- (A e. CC -> (x e. RR -> (Im` A) e. RR))
51	50	ancld 320	. . . . . . . . . . . 12 |- (A e. CC -> (x e. RR -> (x e. RR /\ (Im` A) e. RR)))
52	28	a1d 15	. . . . . . . . . . . . 13 |- (A e. CC -> (y e. RR -> (Re` A) e. RR))
53	52	ancrd 321	. . . . . . . . . . . 12 |- (A e. CC -> (y e. RR -> ((Re` A) e. RR /\ y e. RR)))
54	51, 53	anim12d 614	. . . . . . . . . . 11 |- (A e. CC -> ((x e. RR /\ y e. RR) -> ((x e. RR /\ (Im` A) e. RR) /\ ((Re` A) e. RR /\ y e. RR))))
55	54	imp 375	. . . . . . . . . 10 |- ((A e. CC /\ (x e. RR /\ y e. RR)) -> ((x e. RR /\ (Im` A) e. RR) /\ ((Re` A) e. RR /\ y e. RR)))
56		cru 7783	. . . . . . . . . 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)))
57	55, 56	syl 12	. . . . . . . . 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)))
58		eqtr2 1742	. . . . . . . . 9 |- ((A = (x + (_i x. (Im` A))) /\ A = ((Re` A) + (_i x. y))) -> (x + (_i x. (Im` A))) = ((Re` A) + (_i x. y)))
59	57, 58	syl5bi 224	. . . . . . . 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 420	. . . . . . 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	pm3.26d 346	. . . . . 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 4708	. . . . 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 1762	. . . 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 400	. . 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 1514	. 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 29	1 |- (A e. CC -> A = ((Re` A) + (_i x. (Im` A))))

Syntax hints:   -> wi 3   <-> wb 162   /\ wa 239   = wceq 1136   e. wcel 1138  E.wex 1164  E.wrex 1940  E!wreu 1941  {crab 1942  U.cuni 2999  ` cfv 3809  (class class class)co 4695  CCcc 6180  RRcr 6181  _ici 6184   + caddc 6185   x. cmul 6187  Recre 7792  Imcim 7793

This theorem is referenced by:  replimi 7813  crre 7814  crim 7815  imre 7818  reim0 7819  reim0b 7820  rereb 7821  mulre 7822  recj 7863  imcj 7864  cj11OLD 7876  recan 7952  caucvg3ai 8219  caucvg3lem 8221  efeul 8509  absef 8544  absefib 8545  efieq1re 8546  efifolem7 9877  eff1lem 9892  eff1i 9893

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-rep 3243  ax-sep 3253  ax-nul 3260  ax-pow 3296  ax-pr 3339  ax-un 3601  ax-inf2 5540

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-3or 856  df-3an 857  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-nel 1857  df-ral 1943  df-rex 1944  df-reu 1945  df-rab 1946  df-v 2127  df-sbc 2287  df-csb 2374  df-dif 2430  df-un 2433  df-in 2436  df-ss 2438  df-pss 2440  df-nul 2702  df-if 2807  df-pw 2859  df-sn 2873  df-pr 2874  df-tp 2876  df-op 2877  df-uni 3000  df-int 3037  df-iun 3079  df-br 3159  df-opab 3214  df-tr 3230  df-eprel 3398  df-id 3401  df-po 3406  df-so 3419  df-fr 3440  df-we 3459  df-ord 3475  df-on 3476  df-lim 3477  df-suc 3478  df-om 3761  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-fn 3820  df-f 3821  df-f1 3822  df-fo 3823  df-f1o 3824  df-fv 3825  df-opr 4697  df-oprab 4698  df-mpt 4817  df-1st 4831  df-2nd 4832  df-iota 4900  df-rdg 4951  df-1o 4988  df-oadd 4990  df-omul 4991  df-er 5129  df-ec 5131  df-qs 5134  df-en 5238  df-dom 5239  df-sdom 5240  df-undef 5367  df-riota 5371  df-ni 5948  df-pli 5949  df-mi 5950  df-lti 5951  df-plpq 5983  df-mpq 5984  df-enq 5985  df-nq 5986  df-plq 5987  df-mq 5988  df-rq 5989  df-ltq 5990  df-1q 5991  df-np 6034  df-1p 6035  df-plp 6036  df-mp 6037  df-ltp 6038  df-plpr 6112  df-mpr 6113  df-enr 6114  df-nr 6115  df-plr 6116  df-mr 6117  df-ltr 6118  df-0r 6119  df-1r 6120  df-m1r 6121  df-c 6188  df-0 6189  df-1 6190  df-i 6191  df-r 6192  df-plus 6193  df-mul 6194  df-lt 6195  df-sub 6307  df-neg 6309  df-pnf 6450  df-mnf 6451  df-xr 6452  df-ltxr 6453  df-le 6454  df-div 6688  df-re 7796  df-im 7797

Copyright terms: Public domain