sigarac

Description: Signed area is anticommutative. (Contributed by Saveliy Skresanov, 19-Sep-2017)

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

Proof

Step	Hyp	Ref	Expression
1		sigar	$⊢ G = (x \in ℂ, y \in ℂ ⟼ ℑ (\overline{x} y))$
2	1	sigarval	$⊢ (A \in ℂ \land B \in ℂ) \to A G B = ℑ (\overline{A} B)$
3		cjcl	$⊢ B \in ℂ \to \overline{B} \in ℂ$
4	3	adantl	$⊢ (A \in ℂ \land B \in ℂ) \to \overline{B} \in ℂ$
5		simpl	$⊢ (A \in ℂ \land B \in ℂ) \to A \in ℂ$
6	4 5	cjmuld	$⊢ (A \in ℂ \land B \in ℂ) \to \overline{\overline{B} A} = \overline{\overline{B}} \overline{A}$
7		simpr	$⊢ (A \in ℂ \land B \in ℂ) \to B \in ℂ$
8	7	cjcjd	$⊢ (A \in ℂ \land B \in ℂ) \to \overline{\overline{B}} = B$
9	8	oveq1d	$⊢ (A \in ℂ \land B \in ℂ) \to \overline{\overline{B}} \overline{A} = B \overline{A}$
10	5	cjcld	$⊢ (A \in ℂ \land B \in ℂ) \to \overline{A} \in ℂ$
11	7 10	mulcomd	$⊢ (A \in ℂ \land B \in ℂ) \to B \overline{A} = \overline{A} B$
12	6 9 11	3eqtrrd	$⊢ (A \in ℂ \land B \in ℂ) \to \overline{A} B = \overline{\overline{B} A}$
13	12	fveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to ℑ (\overline{A} B) = ℑ (\overline{\overline{B} A})$
14	4 5	mulcld	$⊢ (A \in ℂ \land B \in ℂ) \to \overline{B} A \in ℂ$
15	14	imcjd	$⊢ (A \in ℂ \land B \in ℂ) \to ℑ (\overline{\overline{B} A}) = - ℑ (\overline{B} A)$
16	2 13 15	3eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to A G B = - ℑ (\overline{B} A)$
17	1	sigarval	$⊢ (B \in ℂ \land A \in ℂ) \to B G A = ℑ (\overline{B} A)$
18	17	ancoms	$⊢ (A \in ℂ \land B \in ℂ) \to B G A = ℑ (\overline{B} A)$
19	18	negeqd	$⊢ (A \in ℂ \land B \in ℂ) \to - (B G A) = - ℑ (\overline{B} A)$
20	16 19	eqtr4d	$⊢ (A \in ℂ \land B \in ℂ) \to A G B = - (B G A)$

Metamath Proof Explorer

Theorem sigarac

Proof