Metamath Proof Explorer


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 )