Metamath Proof Explorer

Theorem recan

Description: Cancellation law involving the real part of a complex number. (Contributed by NM, 12-May-2005)

Ref Expression
Assertion recan ⊢ A ∈ ℂ ∧ B ∈ ℂ → ∀ x ∈ ℂ ℜ ⁡ x ⁢ A = ℜ ⁡ x ⁢ B ↔ A = B

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 fvoveq1 ⊢ x = 1 → ℜ ⁡ x ⁢ A = ℜ ⁡ 1 ⁢ A
3 fvoveq1 ⊢ x = 1 → ℜ ⁡ x ⁢ B = ℜ ⁡ 1 ⁢ B
4 2 3 eqeq12d ⊢ x = 1 → ℜ ⁡ x ⁢ A = ℜ ⁡ x ⁢ B ↔ ℜ ⁡ 1 ⁢ A = ℜ ⁡ 1 ⁢ B
5 4 rspcv ⊢ 1 ∈ ℂ → ∀ x ∈ ℂ ℜ ⁡ x ⁢ A = ℜ ⁡ x ⁢ B → ℜ ⁡ 1 ⁢ A = ℜ ⁡ 1 ⁢ B
6 1 5 ax-mp ⊢ ∀ x ∈ ℂ ℜ ⁡ x ⁢ A = ℜ ⁡ x ⁢ B → ℜ ⁡ 1 ⁢ A = ℜ ⁡ 1 ⁢ B
7 negicn ⊢ − i ∈ ℂ
8 fvoveq1 ⊢ x = − i → ℜ ⁡ x ⁢ A = ℜ ⁡ − i ⁢ A
9 fvoveq1 ⊢ x = − i → ℜ ⁡ x ⁢ B = ℜ ⁡ − i ⁢ B
10 8 9 eqeq12d ⊢ x = − i → ℜ ⁡ x ⁢ A = ℜ ⁡ x ⁢ B ↔ ℜ ⁡ − i ⁢ A = ℜ ⁡ − i ⁢ B
11 10 rspcv ⊢ − i ∈ ℂ → ∀ x ∈ ℂ ℜ ⁡ x ⁢ A = ℜ ⁡ x ⁢ B → ℜ ⁡ − i ⁢ A = ℜ ⁡ − i ⁢ B
12 7 11 ax-mp ⊢ ∀ x ∈ ℂ ℜ ⁡ x ⁢ A = ℜ ⁡ x ⁢ B → ℜ ⁡ − i ⁢ A = ℜ ⁡ − i ⁢ B
13 12 oveq2d ⊢ ∀ x ∈ ℂ ℜ ⁡ x ⁢ A = ℜ ⁡ x ⁢ B → i ⁢ ℜ ⁡ − i ⁢ A = i ⁢ ℜ ⁡ − i ⁢ B
14 6 13 oveq12d ⊢ ∀ x ∈ ℂ ℜ ⁡ x ⁢ A = ℜ ⁡ x ⁢ B → ℜ ⁡ 1 ⁢ A + i ⁢ ℜ ⁡ − i ⁢ A = ℜ ⁡ 1 ⁢ B + i ⁢ ℜ ⁡ − i ⁢ B
15 replim ⊢ A ∈ ℂ → A = ℜ ⁡ A + i ⁢ ℑ ⁡ A
16 mullid ⊢ A ∈ ℂ → 1 ⁢ A = A
17 16 eqcomd ⊢ A ∈ ℂ → A = 1 ⁢ A
18 17 fveq2d ⊢ A ∈ ℂ → ℜ ⁡ A = ℜ ⁡ 1 ⁢ A
19 imre ⊢ A ∈ ℂ → ℑ ⁡ A = ℜ ⁡ − i ⁢ A
20 19 oveq2d ⊢ A ∈ ℂ → i ⁢ ℑ ⁡ A = i ⁢ ℜ ⁡ − i ⁢ A
21 18 20 oveq12d ⊢ A ∈ ℂ → ℜ ⁡ A + i ⁢ ℑ ⁡ A = ℜ ⁡ 1 ⁢ A + i ⁢ ℜ ⁡ − i ⁢ A
22 15 21 eqtrd ⊢ A ∈ ℂ → A = ℜ ⁡ 1 ⁢ A + i ⁢ ℜ ⁡ − i ⁢ A
23 replim ⊢ B ∈ ℂ → B = ℜ ⁡ B + i ⁢ ℑ ⁡ B
24 mullid ⊢ B ∈ ℂ → 1 ⁢ B = B
25 24 eqcomd ⊢ B ∈ ℂ → B = 1 ⁢ B
26 25 fveq2d ⊢ B ∈ ℂ → ℜ ⁡ B = ℜ ⁡ 1 ⁢ B
27 imre ⊢ B ∈ ℂ → ℑ ⁡ B = ℜ ⁡ − i ⁢ B
28 27 oveq2d ⊢ B ∈ ℂ → i ⁢ ℑ ⁡ B = i ⁢ ℜ ⁡ − i ⁢ B
29 26 28 oveq12d ⊢ B ∈ ℂ → ℜ ⁡ B + i ⁢ ℑ ⁡ B = ℜ ⁡ 1 ⁢ B + i ⁢ ℜ ⁡ − i ⁢ B
30 23 29 eqtrd ⊢ B ∈ ℂ → B = ℜ ⁡ 1 ⁢ B + i ⁢ ℜ ⁡ − i ⁢ B
31 22 30 eqeqan12d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A = B ↔ ℜ ⁡ 1 ⁢ A + i ⁢ ℜ ⁡ − i ⁢ A = ℜ ⁡ 1 ⁢ B + i ⁢ ℜ ⁡ − i ⁢ B
32 14 31 imbitrrid ⊢ A ∈ ℂ ∧ B ∈ ℂ → ∀ x ∈ ℂ ℜ ⁡ x ⁢ A = ℜ ⁡ x ⁢ B → A = B
33 oveq2 ⊢ A = B → x ⁢ A = x ⁢ B
34 33 fveq2d ⊢ A = B → ℜ ⁡ x ⁢ A = ℜ ⁡ x ⁢ B
35 34 ralrimivw ⊢ A = B → ∀ x ∈ ℂ ℜ ⁡ x ⁢ A = ℜ ⁡ x ⁢ B
36 32 35 impbid1 ⊢ A ∈ ℂ ∧ B ∈ ℂ → ∀ x ∈ ℂ ℜ ⁡ x ⁢ A = ℜ ⁡ x ⁢ B ↔ A = B