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 e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
	sigarimcd.a	|- ( ph -> ( A e. CC /\ B e. CC ) )
	sigariz.a	|- ( ph -> ( A G B ) = 0 )
Assertion	sigariz	|- ( ph -> ( B G A ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		sigarimcd.sigar	|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
2		sigarimcd.a	|- ( ph -> ( A e. CC /\ B e. CC ) )
3		sigariz.a	|- ( ph -> ( A G B ) = 0 )
4	1	sigarac	|- ( ( A e. CC /\ B e. CC ) -> ( A G B ) = -u ( B G A ) )
5	2 4	syl	|- ( ph -> ( A G B ) = -u ( B G A ) )
6	3 5	eqtr3d	|- ( ph -> 0 = -u ( B G A ) )
7	6	negeqd	|- ( ph -> -u 0 = -u -u ( B G A ) )
8		neg0	|- -u 0 = 0
9	8	a1i	|- ( ph -> -u 0 = 0 )
10	2	ancomd	|- ( ph -> ( B e. CC /\ A e. CC ) )
11	1 10	sigarimcd	|- ( ph -> ( B G A ) e. CC )
12	11	negnegd	|- ( ph -> -u -u ( B G A ) = ( B G A ) )
13	7 9 12	3eqtr3rd	|- ( ph -> ( B G A ) = 0 )