Theorem replimt 4798

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

Assertion

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

Proof of Theorem replimt

Step	Hyp	Ref	Expression
1		cleqid 1102	. . . . . 6 |- (Im` A) = (Im` A)
2		imclt 4797	. . . . . . 7 |- (A e. CC -> (Im` A) e. RR)
3		opreq1 3006	. . . . . . . . . . . . 13 |- (y = (Im` A) -> (y x. i) = ((Im` A) x. i))
4	3	opreq2d 3013	. . . . . . . . . . . 12 |- (y = (Im` A) -> (x + (y x. i)) = (x + ((Im` A) x. i)))
5	4	cleq2d 1112	. . . . . . . . . . 11 |- (y = (Im` A) -> (A = (x + (y x. i)) <-> A = (x + ((Im` A) x. i))))
6	5	birexdv 1220	. . . . . . . . . 10 |- (y = (Im` A) -> (E.x e. RR A = (x + (y x. i)) <-> E.x e. RR A = (x + ((Im` A) x. i))))
7		cleq2 1110	. . . . . . . . . 10 |- (y = (Im` A) -> ((Im` A) = y <-> (Im` A) = (Im` A)))
8	6, 7	bibi12d 477	. . . . . . . . 9 |- (y = (Im` A) -> ((E.x e. RR A = (x + (y x. i)) <-> (Im` A) = y) <-> (E.x e. RR A = (x + ((Im` A) x. i)) <-> (Im` A) = (Im` A))))
9	8	imbi2d 464	. . . . . . . 8 |- (y = (Im` A) -> ((A e. CC -> (E.x e. RR A = (x + (y x. i)) <-> (Im` A) = y)) <-> (A e. CC -> (E.x e. RR A = (x + ((Im` A) x. i)) <-> (Im` A) = (Im` A)))))
10		reuuni1 1955	. . . . . . . . . . 11 |- ((y e. RR /\ E!y e. RR E.x e. RR A = (x + (y x. i))) -> (E.x e. RR A = (x + (y x. i)) <-> U.{y e. RR | E.x e. RR A = (x + (y x. i))} = y))
11		creui 4533	. . . . . . . . . . 11 |- (A e. CC -> E!y e. RR E.x e. RR A = (x + (y x. i)))
12	10, 11	sylan2 346	. . . . . . . . . 10 |- ((y e. RR /\ A e. CC) -> (E.x e. RR A = (x + (y x. i)) <-> U.{y e. RR | E.x e. RR A = (x + (y x. i))} = y))
13		imvalt 4795	. . . . . . . . . . . 12 |- (A e. CC -> (Im` A) = U.{y e. RR | E.x e. RR A = (x + (y x. i))})
14	13	cleq1d 1109	. . . . . . . . . . 11 |- (A e. CC -> ((Im` A) = y <-> U.{y e. RR | E.x e. RR A = (x + (y x. i))} = y))
15	14	adantl 305	. . . . . . . . . 10 |- ((y e. RR /\ A e. CC) -> ((Im` A) = y <-> U.{y e. RR | E.x e. RR A = (x + (y x. i))} = y))
16	12, 15	bitr4d 409	. . . . . . . . 9 |- ((y e. RR /\ A e. CC) -> (E.x e. RR A = (x + (y x. i)) <-> (Im` A) = y))
17	16	exp 291	. . . . . . . 8 |- (y e. RR -> (A e. CC -> (E.x e. RR A = (x + (y x. i)) <-> (Im` A) = y)))
18	9, 17	vtoclga 1387	. . . . . . 7 |- ((Im` A) e. RR -> (A e. CC -> (E.x e. RR A = (x + ((Im` A) x. i)) <-> (Im` A) = (Im` A))))
19	2, 18	mpcom 49	. . . . . 6 |- (A e. CC -> (E.x e. RR A = (x + ((Im` A) x. i)) <-> (Im` A) = (Im` A)))
20	1, 19	mpbiri 169	. . . . 5 |- (A e. CC -> E.x e. RR A = (x + ((Im` A) x. i)))
21		df-rex 1206	. . . . 5 |- (E.x e. RR A = (x + ((Im` A) x. i)) <-> E.x(x e. RR /\ A = (x + ((Im` A) x. i))))
22	20, 21	sylib 173	. . . 4 |- (A e. CC -> E.x(x e. RR /\ A = (x + ((Im` A) x. i))))
23		cleqid 1102	. . . . . 6 |- (Re` A) = (Re` A)
24		reclt 4796	. . . . . . 7 |- (A e. CC -> (Re` A) e. RR)
25		opreq1 3006	. . . . . . . . . . . 12 |- (x = (Re` A) -> (x + (y x. i)) = ((Re` A) + (y x. i)))
26	25	cleq2d 1112	. . . . . . . . . . 11 |- (x = (Re` A) -> (A = (x + (y x. i)) <-> A = ((Re` A) + (y x. i))))
27	26	birexdv 1220	. . . . . . . . . 10 |- (x = (Re` A) -> (E.y e. RR A = (x + (y x. i)) <-> E.y e. RR A = ((Re` A) + (y x. i))))
28		cleq2 1110	. . . . . . . . . 10 |- (x = (Re` A) -> ((Re` A) = x <-> (Re` A) = (Re` A)))
29	27, 28	bibi12d 477	. . . . . . . . 9 |- (x = (Re` A) -> ((E.y e. RR A = (x + (y x. i)) <-> (Re` A) = x) <-> (E.y e. RR A = ((Re` A) + (y x. i)) <-> (Re` A) = (Re` A))))
30	29	imbi2d 464	. . . . . . . 8 |- (x = (Re` A) -> ((A e. CC -> (E.y e. RR A = (x + (y x. i)) <-> (Re` A) = x)) <-> (A e. CC -> (E.y e. RR A = ((Re` A) + (y x. i)) <-> (Re` A) = (Re` A)))))
31		reuuni1 1955	. . . . . . . . . . 11 |- ((x e. RR /\ E!x e. RR E.y e. RR A = (x + (y x. i))) -> (E.y e. RR A = (x + (y x. i)) <-> U.{x e. RR | E.y e. RR A = (x + (y x. i))} = x))
32		creur 4532	. . . . . . . . . . 11 |- (A e. CC -> E!x e. RR E.y e. RR A = (x + (y x. i)))
33	31, 32	sylan2 346	. . . . . . . . . 10 |- ((x e. RR /\ A e. CC) -> (E.y e. RR A = (x + (y x. i)) <-> U.{x e. RR | E.y e. RR A = (x + (y x. i))} = x))
34		revalt 4794	. . . . . . . . . . . 12 |- (A e. CC -> (Re` A) = U.{x e. RR | E.y e. RR A = (x + (y x. i))})
35	34	cleq1d 1109	. . . . . . . . . . 11 |- (A e. CC -> ((Re` A) = x <-> U.{x e. RR | E.y e. RR A = (x + (y x. i))} = x))
36	35	adantl 305	. . . . . . . . . 10 |- ((x e. RR /\ A e. CC) -> ((Re` A) = x <-> U.{x e. RR | E.y e. RR A = (x + (y x. i))} = x))
37	33, 36	bitr4d 409	. . . . . . . . 9 |- ((x e. RR /\ A e. CC) -> (E.y e. RR A = (x + (y x. i)) <-> (Re` A) = x))
38	37	exp 291	. . . . . . . 8 |- (x e. RR -> (A e. CC -> (E.y e. RR A = (x + (y x. i)) <-> (Re` A) = x)))
39	30, 38	vtoclga 1387	. . . . . . 7 |- ((Re` A) e. RR -> (A e. CC -> (E.y e. RR A = ((Re` A) + (y x. i)) <-> (Re` A) = (Re` A))))
40	24, 39	mpcom 49	. . . . . 6 |- (A e. CC -> (E.y e. RR A = ((Re` A) + (y x. i)) <-> (Re` A) = (Re` A)))
41	23, 40	mpbiri 169	. . . . 5 |- (A e. CC -> E.y e. RR A = ((Re` A) + (y x. i)))
42		df-rex 1206	. . . . 5 |- (E.y e. RR A = ((Re` A) + (y x. i)) <-> E.y(y e. RR /\ A = ((Re` A) + (y x. i))))
43	41, 42	sylib 173	. . . 4 |- (A e. CC -> E.y(y e. RR /\ A = ((Re` A) + (y x. i))))
44	22, 43	jca 236	. . 3 |- (A e. CC -> (E.x(x e. RR /\ A = (x + ((Im` A) x. i))) /\ E.y(y e. RR /\ A = ((Re` A) + (y x. i)))))
45		an4 388	. . . . 5 |- (((x e. RR /\ y e. RR) /\ (A = (x + ((Im` A) x. i)) /\ A = ((Re` A) + (y x. i)))) <-> ((x e. RR /\ A = (x + ((Im` A) x. i))) /\ (y e. RR /\ A = ((Re` A) + (y x. i)))))
46	45	bi2ex 734	. . . 4 |- (E.xE.y((x e. RR /\ y e. RR) /\ (A = (x + ((Im` A) x. i)) /\ A = ((Re` A) + (y x. i)))) <-> E.xE.y((x e. RR /\ A = (x + ((Im` A) x. i))) /\ (y e. RR /\ A = ((Re` A) + (y x. i)))))
47		eeanv 980	. . . 4 |- (E.xE.y((x e. RR /\ A = (x + ((Im` A) x. i))) /\ (y e. RR /\ A = ((Re` A) + (y x. i)))) <-> (E.x(x e. RR