Theorem crut 6739

Description: The representation of complex numbers in terms of real and imaginary parts is unique. Proposition 10-1.3 of [Gleason] p. 130.

Assertion

Ref	Expression
crut	|- (((A e. RR /\ B e. RR) /\ (C e. RR /\ D e. RR)) -> ((A + (i x. B)) = (C + (i x. D)) <-> (A = C /\ B = D)))

Proof of Theorem crut

Step	Hyp	Ref	Expression
1		opreq1 3974	. . . 4 |- (A = if(A e. RR, A, 0) -> (A + (i x. B)) = (if(A e. RR, A, 0) + (i x. B)))
2	1	eqeq1d 1486	. . 3 |- (A = if(A e. RR, A, 0) -> ((A + (i x. B)) = (C + (i x. D)) <-> (if(A e. RR, A, 0) + (i x. B)) = (C + (i x. D))))
3		eqeq1 1484	. . . 4 |- (A = if(A e. RR, A, 0) -> (A = C <-> if(A e. RR, A, 0) = C))
4	3	anbi1d 619	. . 3 |- (A = if(A e. RR, A, 0) -> ((A = C /\ B = D) <-> (if(A e. RR, A, 0) = C /\ B = D)))
5	2, 4	bibi12d 631	. 2 |- (A = if(A e. RR, A, 0) -> (((A + (i x. B)) = (C + (i x. D)) <-> (A = C /\ B = D)) <-> ((if(A e. RR, A, 0) + (i x. B)) = (C + (i x. D)) <-> (if(A e. RR, A, 0) = C /\ B = D))))
6		opreq2 3975	. . . . 5 |- (B = if(B e. RR, B, 0) -> (i x. B) = (i x. if(B e. RR, B, 0)))
7	6	opreq2d 3982	. . . 4 |- (B = if(B e. RR, B, 0) -> (if(A e. RR, A, 0) + (i x. B)) = (if(A e. RR, A, 0) + (i x. if(B e. RR, B, 0))))
8	7	eqeq1d 1486	. . 3 |- (B = if(B e. RR, B, 0) -> ((if(A e. RR, A, 0) + (i x. B)) = (C + (i x. D)) <-> (if(A e. RR, A, 0) + (i x. if(B e. RR, B, 0))) = (C + (i x. D))))
9		eqeq1 1484	. . . 4 |- (B = if(B e. RR, B, 0) -> (B = D <-> if(B e. RR, B, 0) = D))
10	9	anbi2d 618	. . 3 |- (B = if(B e. RR, B, 0) -> ((if(A e. RR, A, 0) = C /\ B = D) <-> (if(A e. RR, A, 0) = C /\ if(B e. RR, B, 0) = D)))
11	8, 10	bibi12d 631	. 2 |- (B = if(B e. RR, B, 0) -> (((if(A e. RR, A, 0) + (i x. B)) = (C + (i x. D)) <-> (if(A e. RR, A, 0) = C /\ B = D)) <-> ((if(A e. RR, A, 0) + (i x. if(B e. RR, B, 0))) = (C + (i x. D)) <-> (if(A e. RR, A, 0) = C /\ if(B e. RR, B, 0) = D))))
12		opreq1 3974	. . . 4 |- (C = if(C e. RR, C, 0) -> (C + (i x. D)) = (if(C e. RR, C, 0) + (i x. D)))
13	12	eqeq2d 1489	. . 3 |- (C = if(C e. RR, C, 0) -> ((if(A e. RR, A, 0) + (i x. if(B e. RR, B, 0))) = (C + (i x. D)) <-> (if(A e. RR, A, 0) + (i x. if(B e. RR, B, 0))) = (if(C e. RR, C, 0) + (i x. D))))
14		eqeq2 1487	. . . 4 |- (C = if(C e. RR, C, 0) -> (if(A e. RR, A, 0) = C <-> if(A e. RR, A, 0) = if(C e. RR, C, 0)))
15	14	anbi1d 619	. . 3 |- (C = if(C e. RR, C, 0) -> ((if(A e. RR, A, 0) = C /\ if(B e. RR, B, 0) = D) <-> (if(A e. RR, A, 0) = if(C e. RR, C, 0) /\ if(B e. RR, B, 0) = D)))
16	13, 15	bibi12d 631	. 2 |- (C = if(C e. RR, C, 0) -> (((if(A e. RR, A, 0) + (i x. if(B e. RR, B, 0))) = (C + (i x. D)) <-> (if(A e. RR, A, 0) = C /\ if(B e. RR, B, 0) = D)) <-> ((if(A e. RR, A, 0) + (i x. if(B e. RR, B, 0))) = (if(C e. RR, C, 0) + (i x. D)) <-> (if(A e. RR, A, 0) = if(C e. RR, C, 0) /\ if(B e. RR, B, 0) = D))))
17		opreq2 3975	. . . . 5 |- (D = if(D e. RR, D, 0) -> (i x. D) = (i x. if(D e. RR, D, 0)))
18	17	opreq2d 3982	. . . 4 |- (D = if(D e. RR, D, 0) -> (if(C e. RR, C, 0) + (i x. D)) = (if(C e. RR, C, 0) + (i x. if(D e. RR, D, 0))))
19	18	eqeq2d 1489	. . 3 |- (D = if(D e. RR, D, 0) -> ((if(A e. RR, A, 0) + (i x. if(B e. RR, B, 0))) = (if(C e. RR, C, 0) + (i x. D)) <-> (if(A e. RR, A, 0) + (i x. if(B e. RR, B, 0))) = (if(C e. RR, C, 0) + (i x. if(D e. RR, D, 0)))))
20		eqeq2 1487	. . . 4 |- (D = if(D e. RR, D, 0) -> (if(B e. RR, B, 0) = D <-> if(B e. RR, B, 0) = if(D e. RR, D, 0)))
21	20	anbi2d 618	. . 3 |- (D = if(D e. RR, D, 0) -> ((if(A e. RR, A, 0) = if(C e. RR, C, 0) /\ if(B e. RR, B, 0) = D) <-> (if(A e. RR, A, 0) = if(C e. RR, C, 0) /\ if(B e. RR, B, 0) = if(D e. RR, D, 0))))
22	19, 21	bibi12d 631	. 2 |- (D = if(D e. RR, D, 0) -> (((if(A e. RR, A, 0) + (i x. if(B e. RR, B, 0))) = (if(C e. RR, C, 0) + (i x. D)) <-> (if(A e. RR, A, 0) = if(C e. RR, C, 0) /\ if(B e. RR, B, 0) = D)) <-> ((if(A e. RR, A, 0) + (i x. if(B e. RR, B, 0))) = (if(C e. RR, C, 0) + (i x. if(D e. RR, D, 0))) <-> (if(A e. RR, A, 0) = if(C e. RR, C, 0) /\ if(B e. RR, B, 0) = if(D e. RR, D, 0)))))
23		0re 5452	. . . 4 |- 0 e. RR
24	23	elimel 2398	. . 3 |- if(A e. RR, A, 0) e. RR
25	23	elimel 2398	. . 3 |- if(B e. RR, B, 0) e. RR
26	23	elimel 2398	. . 3 |- if(C e. RR, C, 0) e. RR
27	23	elimel 2398	. . 3 |- if(D e. RR, D, 0) e. RR
28	24, 25, 26, 27	cru 6738	. 2 |- ((if(A e. RR, A, 0) + (i x. if(B e. RR, B, 0))) = (if(C e. RR, C, 0) + (i x. if(D e. RR, D, 0))) <-> (if(A e. RR, A, 0) = if(C e. RR, C, 0) /\ if(B e. RR, B, 0) = if(D e. RR, D, 0)))
29	5, 11, 16, 22, 28	dedth4h 2393	1 |- (((A e. RR /\ B e. RR) /\ (C e. RR /\ D e. RR)) -> ((A + (i x. B)) = (C + (i x. D)) <-> (A = C /\ B = D)))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 958   e. wcel 960  ifcif 2365  (class class class)co 3969  RRcr 5245  0cc0 5246  ici 5248   + caddc 5249   x. cmul 5251

This theorem is referenced by:  creur 6743  creui 6744  rimul 6745  replimt 6762  crret 6770  crimt 6771  cj11t 6830  efieq 7450  sinperlem1 8681  efifolem7 8723  efif1lem3 8727  eff1i 8739

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-rep 2698  ax-sep 2708  ax-nul 2715  ax-pow 2748  ax-pr 2785  ax-un 2872  ax-inf2 4634

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 778  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-nel 1591  df-ral 1652  df-rex 1653  df-reu 1654  df-rab 1655  df-v 1815  df-sbc 1945  df-csb 2005  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-pss 2058  df-nul 2284  df-if 2366  df-pw