Theorem sigarid

Description: Signed area of a flat parallelogram is zero. (Contributed by Saveliy Skresanov, 20-Sep-2017)

	Ref	Expression
Hypothesis	sigar	⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
Assertion	sigarid	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 𝐺 𝐴 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		sigar	⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
2	1	sigarval	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝐴 𝐺 𝐴 ) = ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐴 ) ) )
3	2	anidms	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 𝐺 𝐴 ) = ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐴 ) ) )
4		cjcl	⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) ∈ ℂ )
5		id	⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
6	4 5	mulcomd	⊢ ( 𝐴 ∈ ℂ → ( ( ∗ ‘ 𝐴 ) · 𝐴 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
7		cjmulrcl	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℝ )
8	6 7	eqeltrd	⊢ ( 𝐴 ∈ ℂ → ( ( ∗ ‘ 𝐴 ) · 𝐴 ) ∈ ℝ )
9	8	reim0d	⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐴 ) ) = 0 )
10	3 9	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 𝐺 𝐴 ) = 0 )