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

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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∀ 𝑥 ∈ ℂ ( ℜ ‘ ( 𝑥 · 𝐴 ) ) = ( ℜ ‘ ( 𝑥 · 𝐵 ) ) ↔ 𝐴 = 𝐵 ) )

Proof

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