# Metamath Proof Explorer

## Theorem cru

Description: The representation of complex numbers in terms of real and imaginary parts is unique. Proposition 10-1.3 of Gleason p. 130. (Contributed by NM, 9-May-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion cru ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\to \left({A}+\mathrm{i}{B}={C}+\mathrm{i}{D}↔\left({A}={C}\wedge {B}={D}\right)\right)$

### Proof

Step Hyp Ref Expression
1 simplrl ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to {C}\in ℝ$
2 1 recnd ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to {C}\in ℂ$
3 simplll ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to {A}\in ℝ$
4 3 recnd ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to {A}\in ℂ$
5 simpr ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}$
6 ax-icn ${⊢}\mathrm{i}\in ℂ$
7 6 a1i ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to \mathrm{i}\in ℂ$
8 simpllr ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to {B}\in ℝ$
9 8 recnd ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to {B}\in ℂ$
10 7 9 mulcld ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to \mathrm{i}{B}\in ℂ$
11 simplrr ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to {D}\in ℝ$
12 11 recnd ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to {D}\in ℂ$
13 7 12 mulcld ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to \mathrm{i}{D}\in ℂ$
14 4 10 2 13 addsubeq4d ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to \left({A}+\mathrm{i}{B}={C}+\mathrm{i}{D}↔{C}-{A}=\mathrm{i}{B}-\mathrm{i}{D}\right)$
15 5 14 mpbid ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to {C}-{A}=\mathrm{i}{B}-\mathrm{i}{D}$
16 8 11 resubcld ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to {B}-{D}\in ℝ$
17 7 9 12 subdid ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to \mathrm{i}\left({B}-{D}\right)=\mathrm{i}{B}-\mathrm{i}{D}$
18 17 15 eqtr4d ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to \mathrm{i}\left({B}-{D}\right)={C}-{A}$
19 1 3 resubcld ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to {C}-{A}\in ℝ$
20 18 19 eqeltrd ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to \mathrm{i}\left({B}-{D}\right)\in ℝ$
21 rimul ${⊢}\left({B}-{D}\in ℝ\wedge \mathrm{i}\left({B}-{D}\right)\in ℝ\right)\to {B}-{D}=0$
22 16 20 21 syl2anc ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to {B}-{D}=0$
23 9 12 22 subeq0d ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to {B}={D}$
24 23 oveq2d ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to \mathrm{i}{B}=\mathrm{i}{D}$
25 24 oveq1d ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to \mathrm{i}{B}-\mathrm{i}{D}=\mathrm{i}{D}-\mathrm{i}{D}$
26 13 subidd ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to \mathrm{i}{D}-\mathrm{i}{D}=0$
27 15 25 26 3eqtrd ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to {C}-{A}=0$
28 2 4 27 subeq0d ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to {C}={A}$
29 28 eqcomd ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to {A}={C}$
30 29 23 jca ${⊢}\left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\wedge {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\right)\to \left({A}={C}\wedge {B}={D}\right)$
31 30 ex ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\to \left({A}+\mathrm{i}{B}={C}+\mathrm{i}{D}\to \left({A}={C}\wedge {B}={D}\right)\right)$
32 oveq2 ${⊢}{B}={D}\to \mathrm{i}{B}=\mathrm{i}{D}$
33 oveq12 ${⊢}\left({A}={C}\wedge \mathrm{i}{B}=\mathrm{i}{D}\right)\to {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}$
34 32 33 sylan2 ${⊢}\left({A}={C}\wedge {B}={D}\right)\to {A}+\mathrm{i}{B}={C}+\mathrm{i}{D}$
35 31 34 impbid1 ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\to \left({A}+\mathrm{i}{B}={C}+\mathrm{i}{D}↔\left({A}={C}\wedge {B}={D}\right)\right)$