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 )