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	$⊢ G = (x \in ℂ, y \in ℂ ⟼ ℑ (\overline{x} y))$
		sigarimcd.a	$⊢ φ \to (A \in ℂ \land B \in ℂ)$
		sigariz.a	$⊢ φ \to A G B = 0$
	Assertion	sigariz	$⊢ φ \to B G A = 0$

Proof

Step	Hyp	Ref	Expression
1		sigarimcd.sigar	$⊢ G = (x \in ℂ, y \in ℂ ⟼ ℑ (\overline{x} y))$
2		sigarimcd.a	$⊢ φ \to (A \in ℂ \land B \in ℂ)$
3		sigariz.a	$⊢ φ \to A G B = 0$
4	1	sigarac	$⊢ (A \in ℂ \land B \in ℂ) \to A G B = - (B G A)$
5	2 4	syl	$⊢ φ \to A G B = - (B G A)$
6	3 5	eqtr3d	$⊢ φ \to 0 = - (B G A)$
7	6	negeqd	$⊢ φ \to - 0 = - (- (B G A))$
8		neg0	$⊢ - 0 = 0$
9	8	a1i	$⊢ φ \to - 0 = 0$
10	2	ancomd	$⊢ φ \to (B \in ℂ \land A \in ℂ)$
11	1 10	sigarimcd	$⊢ φ \to B G A \in ℂ$
12	11	negnegd	$⊢ φ \to - (- (B G A)) = B G A$
13	7 9 12	3eqtr3rd	$⊢ φ \to B G A = 0$