sigarval

Description: Define the signed area by treating complex numbers as vectors with two components. (Contributed by Saveliy Skresanov, 19-Sep-2017)

		Ref	Expression
	Hypothesis	sigar	$⊢ G = (x \in ℂ, y \in ℂ ⟼ ℑ (\overline{x} y))$
	Assertion	sigarval	$⊢ (A \in ℂ \land B \in ℂ) \to A G B = ℑ (\overline{A} B)$

Step	Hyp	Ref	Expression
1		sigar	$⊢ G = (x \in ℂ, y \in ℂ ⟼ ℑ (\overline{x} y))$
2		simpl	$⊢ (x = A \land y = B) \to x = A$
3	2	fveq2d	$⊢ (x = A \land y = B) \to \overline{x} = \overline{A}$
4		simpr	$⊢ (x = A \land y = B) \to y = B$
5	3 4	oveq12d	$⊢ (x = A \land y = B) \to \overline{x} y = \overline{A} B$
6	5	fveq2d	$⊢ (x = A \land y = B) \to ℑ (\overline{x} y) = ℑ (\overline{A} B)$
7		fvex	$⊢ ℑ (\overline{A} B) \in V$
8	6 1 7	ovmpoa	$⊢ (A \in ℂ \land B \in ℂ) \to A G B = ℑ (\overline{A} B)$

Metamath Proof Explorer