Metamath Proof Explorer

Theorem 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 e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
Assertion sigarval 
|- ( ( A e. CC /\ B e. CC ) -> ( A G B ) = ( Im ` ( ( * ` A ) x. B ) ) )

Proof

Step Hyp Ref Expression
1 sigar 
 |-  G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
2 simpl 
 |-  ( ( x = A /\ y = B ) -> x = A )
3 2 fveq2d 
 |-  ( ( x = A /\ y = B ) -> ( * ` x ) = ( * ` A ) )
4 simpr 
 |-  ( ( x = A /\ y = B ) -> y = B )
5 3 4 oveq12d 
 |-  ( ( x = A /\ y = B ) -> ( ( * ` x ) x. y ) = ( ( * ` A ) x. B ) )
6 5 fveq2d 
 |-  ( ( x = A /\ y = B ) -> ( Im ` ( ( * ` x ) x. y ) ) = ( Im ` ( ( * ` A ) x. B ) ) )
7 fvex 
 |-  ( Im ` ( ( * ` A ) x. B ) ) e. _V
8 6 1 7 ovmpoa 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A G B ) = ( Im ` ( ( * ` A ) x. B ) ) )