This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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