Theorem replimt 6692

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

Assertion

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

Proof of Theorem replimt

Step	Hyp	Ref	Expression
1		eqid 1468	. . . . . 6 |- (Im` A) = (Im` A)
2		imclt 6689	. . . . . . 7 |- (A e. CC -> (Im` A) e. RR)
3		opreq2 3954	. . . . . . . . . . . . 13 |- (y = (Im` A) -> (i x. y) = (i x. (Im` A)))
4	3	opreq2d 3961	. . . . . . . . . . . 12 |- (y = (Im` A) -> (x + (i x. y)) = (x + (i x. (Im` A))))
5	4	eqeq2d 1478	. . . . . . . . . . 11 |- (y = (Im` A) -> (A = (x + (i x. y)) <-> A = (x + (i x. (Im` A)))))
6	5	rexbidv 1656	. . . . . . . . . 10 |- (y = (Im` A) -> (E.x e. RR A = (x + (i x. y)) <-> E.x e. RR A = (x + (i x. (Im` A)))))
7		eqeq2 1476	. . . . . . . . . 10 |- (y = (Im` A) -> ((Im` A) = y <-> (Im` A) = (Im` A)))
8	6, 7	bibi12d 627	. . . . . . . . 9 |- (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 610	. . . . . . . 8 |- (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		reuuni1 2872	. . . . . . . . . . 11 |- ((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))
11		creui 6674	. . . . . . . . . . 11 |- (A e. CC -> E!y e. RR E.x e. RR A = (x + (i x. y)))
12	10, 11	sylan2 451	. . . . . . . . . 10 |- ((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		imvalt 6687	. . . . . . . . . . . 12 |- (A e. CC -> (Im` A) = U.{y e. RR | E.x e. RR A = (x + (i x. y))})
14	13	eqeq1d 1475	. . . . . . . . . . 11 |- (A e. CC -> ((Im` A) = y <-> U.{y e. RR | E.x e. RR A = (x + (i x. y))} = y))
15	14	adantl 388	. . . . . . . . . 10 |- ((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 529	. . . . . . . . 9 |- ((y e. RR /\ A e. CC) -> (E.x e. RR A = (x + (i x. y)) <-> (Im` A) = y))
17	16	ex 373	. . . . . . . 8 |- (y e. RR -> (A e. CC -> (E.x e. RR A = (x + (i x. y)) <-> (Im` A) = y)))
18	9, 17	vtoclga 1843	. . . . . . 7 |- ((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 49	. . . . . 6 |- (A e. CC -> (E.x e. RR A = (x + (i x. (Im` A))) <-> (Im` A) = (Im` A)))
20	1, 19	mpbiri 194	. . . . 5 |- (A e. CC -> E.x e. RR A = (x + (i x. (Im` A))))
21		df-rex 1642	. . . . 5 |- (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 198	. . . 4 |- (A e. CC -> E.x(x e. RR /\ A = (x + (i x. (Im` A)))))
23		eqid 1468	. . . . . 6 |- (Re` A) = (Re` A)
24		reclt 6688	. . . . . . 7 |- (A e. CC -> (Re` A) e. RR)
25		opreq1 3953	. . . . . . . . . . . 12 |- (x = (Re` A) -> (x + (i x. y)) = ((Re` A) + (i x. y)))
26	25	eqeq2d 1478	. . . . . . . . . . 11 |- (x = (Re` A) -> (A = (x + (i x. y)) <-> A = ((Re` A) + (i x. y))))
27	26	rexbidv 1656	. . . . . . . . . 10 |- (x = (Re` A) -> (E.y e. RR A = (x + (i x. y)) <-> E.y e. RR A = ((Re` A) + (i x. y))))
28		eqeq2 1476	. . . . . . . . . 10 |- (x = (Re` A) -> ((Re` A) = x <-> (Re` A) = (Re` A)))
29	27, 28	bibi12d 627	. . . . . . . . 9 |- (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 610	. . . . . . . 8 |- (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		reuuni1 2872	. . . . . . . . . . 11 |- ((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))
32		creur 6673	. . . . . . . . . . 11 |- (A e. CC -> E!x e. RR E.y e. RR A = (x + (i x. y)))
33	31, 32	sylan2 451	. . . . . . . . . 10 |- ((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		revalt 6686	. . . . . . . . . . . 12 |- (A e. CC -> (Re` A) = U.{x e. RR | E.y e. RR A = (x + (i x. y))})
35	34	eqeq1d 1475	. . . . . . . . . . 11 |- (A e. CC -> ((Re` A) = x <-> U.{x e. RR | E.y e. RR A = (x + (i x. y))} = x))
36	35	adantl 388	. . . . . . . . . 10 |- ((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 529	. . . . . . . . 9 |- ((x e. RR /\ A e. CC) -> (E.y e. RR A = (x + (i x. y)) <-> (Re` A) = x))
38	37	ex 373	. . . . . . . 8 |- (x e. RR -> (A e. CC -> (E.y e. RR A = (x + (i x. y)) <-> (Re` A) = x)))
39	30, 38	vtoclga 1843	. . . . . . 7 |- ((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 49	. . . . . 6 |- (A e. CC -> (E.y e. RR A = ((Re` A) + (i x. y)) <-> (Re` A) = (Re` A)))
41	23, 40	mpbiri 194	. . . . 5 |- (A e. CC -> E.y e. RR A = ((Re` A) + (i x. y)))
42		df-rex 1642	. . . . 5 |- (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 198	. . . 4 |- (A e. CC -> E.y(y e. RR /\ A = ((Re` A) + (i x. y))))
44	22, 43	jca 288	. . 3 |- (A e. CC -> (E.x(x e. RR /\ A = (x + (i x. (Im` A)))) /\ E.y(y e. RR /\ A = ((Re` A) + (i x. y)))))
45		an4 505	. . . . 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)))))
46	45	2exbii 1048	. . . 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)))))
47		eeanv 1318	. . . 4 |- (