Theorem sigarid

Description: Signed area of a flat parallelogram is zero. (Contributed by Saveliy Skresanov, 20-Sep-2017)

	Ref	Expression
Hypothesis	sigar	$$⊢G=\left(x\in ℂ,y\in ℂ⟼\Im \left(\bar{x}y\right)\right)$$
Assertion	sigarid	$$⊢A\in ℂ\to AGA=0$$

Proof

Step	Hyp	Ref	Expression
1		sigar	$$⊢G=\left(x\in ℂ,y\in ℂ⟼\Im \left(\bar{x}y\right)\right)$$
2	1	sigarval	$$⊢\left(A\in ℂ\wedge A\in ℂ\right)\to AGA=\Im \left(\bar{A}A\right)$$
3	2	anidms	$$⊢A\in ℂ\to AGA=\Im \left(\bar{A}A\right)$$
4		cjcl	$$⊢A\in ℂ\to \bar{A}\in ℂ$$
5		id	$$⊢A\in ℂ\to A\in ℂ$$
6	4 5	mulcomd	$$⊢A\in ℂ\to \bar{A}A=A\bar{A}$$
7		cjmulrcl	$$⊢A\in ℂ\to A\bar{A}\in ℝ$$
8	6 7	eqeltrd	$$⊢A\in ℂ\to \bar{A}A\in ℝ$$
9	8	reim0d	$$⊢A\in ℂ\to \Im \left(\bar{A}A\right)=0$$
10	3 9	eqtrd	$$⊢A\in ℂ\to AGA=0$$