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	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simplrl	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → 𝐶 ∈ ℝ )
2	1	recnd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → 𝐶 ∈ ℂ )
3		simplll	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → 𝐴 ∈ ℝ )
4	3	recnd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → 𝐴 ∈ ℂ )
5		simpr	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) )
6		ax-icn	⊢ i ∈ ℂ
7	6	a1i	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → i ∈ ℂ )
8		simpllr	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → 𝐵 ∈ ℝ )
9	8	recnd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → 𝐵 ∈ ℂ )
10	7 9	mulcld	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → ( i · 𝐵 ) ∈ ℂ )
11		simplrr	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → 𝐷 ∈ ℝ )
12	11	recnd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → 𝐷 ∈ ℂ )
13	7 12	mulcld	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → ( i · 𝐷 ) ∈ ℂ )
14	4 10 2 13	addsubeq4d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → ( ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ↔ ( 𝐶 − 𝐴 ) = ( ( i · 𝐵 ) − ( i · 𝐷 ) ) ) )
15	5 14	mpbid	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → ( 𝐶 − 𝐴 ) = ( ( i · 𝐵 ) − ( i · 𝐷 ) ) )
16	8 11	resubcld	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → ( 𝐵 − 𝐷 ) ∈ ℝ )
17	7 9 12	subdid	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → ( i · ( 𝐵 − 𝐷 ) ) = ( ( i · 𝐵 ) − ( i · 𝐷 ) ) )
18	17 15	eqtr4d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → ( i · ( 𝐵 − 𝐷 ) ) = ( 𝐶 − 𝐴 ) )
19	1 3	resubcld	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → ( 𝐶 − 𝐴 ) ∈ ℝ )
20	18 19	eqeltrd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → ( i · ( 𝐵 − 𝐷 ) ) ∈ ℝ )
21		rimul	⊢ ( ( ( 𝐵 − 𝐷 ) ∈ ℝ ∧ ( i · ( 𝐵 − 𝐷 ) ) ∈ ℝ ) → ( 𝐵 − 𝐷 ) = 0 )
22	16 20 21	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → ( 𝐵 − 𝐷 ) = 0 )
23	9 12 22	subeq0d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → 𝐵 = 𝐷 )
24	23	oveq2d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → ( i · 𝐵 ) = ( i · 𝐷 ) )
25	24	oveq1d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → ( ( i · 𝐵 ) − ( i · 𝐷 ) ) = ( ( i · 𝐷 ) − ( i · 𝐷 ) ) )
26	13	subidd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → ( ( i · 𝐷 ) − ( i · 𝐷 ) ) = 0 )
27	15 25 26	3eqtrd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → ( 𝐶 − 𝐴 ) = 0 )
28	2 4 27	subeq0d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → 𝐶 = 𝐴 )
29	28	eqcomd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → 𝐴 = 𝐶 )
30	29 23	jca	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
31	30	ex	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
32		oveq2	⊢ ( 𝐵 = 𝐷 → ( i · 𝐵 ) = ( i · 𝐷 ) )
33		oveq12	⊢ ( ( 𝐴 = 𝐶 ∧ ( i · 𝐵 ) = ( i · 𝐷 ) ) → ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) )
34	32 33	sylan2	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) )
35	31 34	impbid1	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 + ( i · 𝐵 ) ) = ( 𝐶 + ( i · 𝐷 ) ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )