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