HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem cj11t 6773
Description: Complex conjugate is a one-to-one function.
Assertion
Ref Expression
cj11t |- ((A e. CC /\ B e. CC) -> ((*` A) = (*` B) <-> A = B))
Proof of Theorem cj11t
StepHypRef Expression
1 neg11t 5389 . . . . 5 |- (((Im` A) e. CC /\ (Im` B) e. CC) -> (-u(Im` A) = -u(Im` B) <-> (Im` A) = (Im` B)))
2 imclt 6697 . . . . . 6 |- (A e. CC -> (Im` A) e. RR)
32recnd 5295 . . . . 5 |- (A e. CC -> (Im` A) e. CC)
4 imclt 6697 . . . . . 6 |- (B e. CC -> (Im` B) e. RR)
54recnd 5295 . . . . 5 |- (B e. CC -> (Im` B) e. CC)
61, 3, 5syl2an 454 . . . 4 |- ((A e. CC /\ B e. CC) -> (-u(Im` A) = -u(Im` B) <-> (Im` A) = (Im` B)))
76anbi2d 615 . . 3 |- ((A e. CC /\ B e. CC) -> (((Re` A) = (Re` B) /\ -u(Im` A) = -u(Im` B)) <-> ((Re` A) = (Re` B) /\ (Im` A) = (Im` B))))
8 crut 6676 . . . 4 |- ((((Re` A) e. RR /\ -u(Im` A) e. RR) /\ ((Re` B) e. RR /\ -u(Im` B) e. RR)) -> (((Re` A) + (i x. -u(Im` A))) = ((Re` B) + (i x. -u(Im` B))) <-> ((Re` A) = (Re` B) /\ -u(Im` A) = -u(Im` B))))
9 reclt 6696 . . . . 5 |- (A e. CC -> (Re` A) e. RR)
10 renegclt 5417 . . . . . 6 |- ((Im` A) e. RR -> -u(Im` A) e. RR)
112, 10syl 10 . . . . 5 |- (A e. CC -> -u(Im` A) e. RR)
129, 11jca 288 . . . 4 |- (A e. CC -> ((Re` A) e. RR /\ -u(Im` A) e. RR))
13 reclt 6696 . . . . 5 |- (B e. CC -> (Re` B) e. RR)
14 renegclt 5417 . . . . . 6 |- ((Im` B) e. RR -> -u(Im` B) e. RR)
154, 14syl 10 . . . . 5 |- (B e. CC -> -u(Im` B) e. RR)
1613, 15jca 288 . . . 4 |- (B e. CC -> ((Re` B) e. RR /\ -u(Im` B) e. RR))
178, 12, 16syl2an 454 . . 3 |- ((A e. CC /\ B e. CC) -> (((Re` A) + (i x. -u(Im` A))) = ((Re` B) + (i x. -u(Im` B))) <-> ((Re` A) = (Re` B) /\ -u(Im` A) = -u(Im` B))))
18 crut 6676 . . . 4 |- ((((Re` A) e. RR /\ (Im` A) e. RR) /\ ((Re` B) e. RR /\ (Im` B) e. RR)) -> (((Re` A) + (i x. (Im` A))) = ((Re` B) + (i x. (Im` B))) <-> ((Re` A) = (Re` B) /\ (Im` A) = (Im` B))))
199, 2jca 288 . . . 4 |- (A e. CC -> ((Re` A) e. RR /\ (Im` A) e. RR))
2013, 4jca 288 . . . 4 |- (B e. CC -> ((Re` B) e. RR /\ (Im` B) e. RR))
2118, 19, 20syl2an 454 . . 3 |- ((A e. CC /\ B e. CC) -> (((Re` A) + (i x. (Im` A))) = ((Re` B) + (i x. (Im` B))) <-> ((Re` A) = (Re` B) /\ (Im` A) = (Im` B))))
227, 17, 213bitr4d 549 . 2 |- ((A e. CC /\ B e. CC) -> (((Re` A) + (i x. -u(Im` A))) = ((Re` B) + (i x. -u(Im` B))) <-> ((Re` A) + (i x. (Im` A))) = ((Re` B) + (i x. (Im` B)))))
23 negsubt 5362 . . . . 5 |- (((Re` A) e. CC /\ (i x. (Im` A)) e. CC) -> ((Re` A) + -u(i x. (Im` A))) = ((Re` A) - (i x. (Im` A))))
249recnd 5295 . . . . 5 |- (A e. CC -> (Re` A) e. CC)
25 axicn 5250 . . . . . . 7 |- i e. CC
26 axmulcl 5253 . . . . . . 7 |- ((i e. CC /\ (Im` A) e. CC) -> (i x. (Im` A)) e. CC)
2725, 26mpan 694 . . . . . 6 |- ((Im` A) e. CC -> (i x. (Im` A)) e. CC)
283, 27syl 10 . . . . 5 |- (A e. CC -> (i x. (Im` A)) e. CC)
2923, 24, 28sylanc 471 . . . 4 |- (A e. CC -> ((Re` A) + -u(i x. (Im` A))) = ((Re` A) - (i x. (Im` A))))
303, 25jctil 292 . . . . . 6 |- (A e. CC -> (i e. CC /\ (Im` A) e. CC))
31 mulneg2t 5432 . . . . . 6 |- ((i e. CC /\ (Im` A) e. CC) -> (i x. -u(Im` A)) = -u(i x. (Im` A)))
3230, 31syl 10 . . . . 5 |- (A e. CC -> (i x. -u(Im` A)) = -u(i x. (Im` A)))
3332opreq2d 3967 . . . 4 |- (A e. CC -> ((Re` A) + (i x. -u(Im` A))) = ((Re` A) + -u(i x. (Im` A))))
34 cjvalt 6703 . . . 4 |- (A e. CC -> (*` A) = ((Re` A) - (i x. (Im` A))))
3529, 33, 343eqtr4rd 1515 . . 3 |- (A e. CC -> (*` A) = ((Re` A) + (i x. -u(Im` A))))
36 negsubt 5362 . . . . 5 |- (((Re` B) e. CC /\ (i x. (Im` B)) e. CC) -> ((Re` B) + -u(i x. (Im` B))) = ((Re` B) - (i x. (Im` B))))
3713recnd 5295 . . . . 5 |- (B e. CC -> (Re` B) e. CC)
38 axmulcl 5253 . . . . . . 7 |- ((i e. CC /\ (Im` B) e. CC) -> (i x. (Im` B)) e. CC)
3925, 38mpan 694 . . . . . 6 |- ((Im` B) e. CC -> (i x. (Im` B)) e. CC)
405, 39syl 10 . . . . 5 |- (B e. CC -> (i x. (Im` B)) e. CC)
4136, 37, 40sylanc 471 . . . 4 |- (B e. CC -> ((Re` B) + -u(i x. (Im` B))) = ((Re` B) - (i x. (Im` B))))
425, 25jctil 292 . . . . . 6 |- (B e. CC -> (i e. CC /\ (Im` B) e. CC))
43 mulneg2t 5432 . . . . . 6 |- ((i e. CC /\ (Im` B) e. CC) -> (i x. -u(Im` B)) = -u(i x. (Im` B)))
4442, 43syl 10 . . . . 5 |- (B e. CC -> (i x. -u(Im` B)) = -u(i x. (Im` B)))
4544opreq2d 3967 . . . 4 |- (B e. CC -> ((Re` B) + (i x. -u(Im` B))) = ((Re` B) + -u(i x. (Im` B))))
46 cjvalt 6703 . . . 4 |- (B e. CC -> (*` B) = ((Re` B) - (i x. (Im` B))))
4741, 45, 463eqtr4rd 1515 . . 3 |- (B e. CC -> (*` B) = ((Re` B) + (i x. -u(Im` B))))
4835, 47eqeqan12d 1487 . 2 |- ((A e. CC /\ B e. CC) -> ((*` A) = (*` B) <-> ((Re` A) + (i x. -u(Im` A))) = ((Re` B) + (i x. -u(Im` B)))))
49 replimt 6700 . . 3 |- (A e. CC -> A = ((Re` A) + (i x. (Im` A))))
50 replimt 6700 . . 3 |- (B e. CC -> B = ((Re` B) + (i x. (Im` B))))
5149, 50eqeqan12d 1487 . 2 |- ((A e. CC /\ B e. CC) -> (A = B <-> ((Re` A) + (i x. (Im` A))) = ((Re` B) + (i x. (Im` B)))))
5222, 48, 513bitr4d 549 1 |- ((A e. CC /\ B e. CC) -> ((*` A) = (*` B) <-> A = B))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 954   e. wcel 956  ` cfv 3177  (class class class)co 3954  CCcc 5212  RRcr 5213  ici 5216   + caddc 5217   x. cmul 5219   - cmin 5272  -ucneg 5273  Recre 6686  Imcim 6687  *ccj 6688
This theorem is referenced by:  cjne0t 6774  hial2eq2t 8912  adjsymt 9699  cnvadj 9756  adj2t 9797
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-rep 2688  ax-sep 2698  ax-nul 2705  ax-pow 2737  ax-pr 2774  ax-un 2861  ax-inf2 4605
This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-nel 1585  df-ral 1646  df-rex 1647  df-reu 1648  df-rab 1649  df-v 1808  df-sbc 1938  df-csb 1998  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-pss 2051  df-nul 2277  df-if 2358  df-pw 2398  df-sn 2408  df-pr 2409  df-tp 2411  df-op 2412  df-uni 2499  df-int 2529  df-iun 2563  df-br 2615  df-opab 2662  df-tr 2676  df-eprel 2827  df-id 2830  df-po 2835  df-so 2845  df-fr 2912  df-we 2929  df-ord 2946  df-on 2947  df-lim 2948  df-suc 2949  df-om 3127  df-xp 3179  df-rel 3180  df-cnv