Metamath Proof Explorer


Theorem sigariz

Description: If signed area is zero, the signed area with swapped arguments is also zero. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017)

Ref Expression
Hypotheses sigarimcd.sigar 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
sigarimcd.a ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) )
sigariz.a ( 𝜑 → ( 𝐴 𝐺 𝐵 ) = 0 )
Assertion sigariz ( 𝜑 → ( 𝐵 𝐺 𝐴 ) = 0 )

Proof

Step Hyp Ref Expression
1 sigarimcd.sigar 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
2 sigarimcd.a ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) )
3 sigariz.a ( 𝜑 → ( 𝐴 𝐺 𝐵 ) = 0 )
4 1 sigarac ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 𝐺 𝐵 ) = - ( 𝐵 𝐺 𝐴 ) )
5 2 4 syl ( 𝜑 → ( 𝐴 𝐺 𝐵 ) = - ( 𝐵 𝐺 𝐴 ) )
6 3 5 eqtr3d ( 𝜑 → 0 = - ( 𝐵 𝐺 𝐴 ) )
7 6 negeqd ( 𝜑 → - 0 = - - ( 𝐵 𝐺 𝐴 ) )
8 neg0 - 0 = 0
9 8 a1i ( 𝜑 → - 0 = 0 )
10 2 ancomd ( 𝜑 → ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
11 1 10 sigarimcd ( 𝜑 → ( 𝐵 𝐺 𝐴 ) ∈ ℂ )
12 11 negnegd ( 𝜑 → - - ( 𝐵 𝐺 𝐴 ) = ( 𝐵 𝐺 𝐴 ) )
13 7 9 12 3eqtr3rd ( 𝜑 → ( 𝐵 𝐺 𝐴 ) = 0 )