Metamath Proof Explorer

Theorem sigarls

Description: Signed area is linear by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017)

Ref Expression
Hypothesis sigar 
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
Assertion sigarls 
|- ( ( A e. CC /\ B e. CC /\ C e. RR ) -> ( A G ( B x. C ) ) = ( ( A G B ) x. C ) )

Proof

Step Hyp Ref Expression
1 sigar 
 |-  G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
2 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. RR ) -> A e. CC )
3 2 cjcld 
 |-  ( ( A e. CC /\ B e. CC /\ C e. RR ) -> ( * ` A ) e. CC )
4 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. RR ) -> B e. CC )
5 simpr 
 |-  ( ( B e. CC /\ C e. RR ) -> C e. RR )
6 5 recnd 
 |-  ( ( B e. CC /\ C e. RR ) -> C e. CC )
7 6 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. RR ) -> C e. CC )
8 3 4 7 mulassd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. RR ) -> ( ( ( * ` A ) x. B ) x. C ) = ( ( * ` A ) x. ( B x. C ) ) )
9 8 fveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. RR ) -> ( Im ` ( ( ( * ` A ) x. B ) x. C ) ) = ( Im ` ( ( * ` A ) x. ( B x. C ) ) ) )
10 simp3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. RR ) -> C e. RR )
11 3 4 mulcld 
 |-  ( ( A e. CC /\ B e. CC /\ C e. RR ) -> ( ( * ` A ) x. B ) e. CC )
12 10 11 immul2d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. RR ) -> ( Im ` ( C x. ( ( * ` A ) x. B ) ) ) = ( C x. ( Im ` ( ( * ` A ) x. B ) ) ) )
13 11 7 mulcomd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. RR ) -> ( ( ( * ` A ) x. B ) x. C ) = ( C x. ( ( * ` A ) x. B ) ) )
14 13 fveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. RR ) -> ( Im ` ( ( ( * ` A ) x. B ) x. C ) ) = ( Im ` ( C x. ( ( * ` A ) x. B ) ) ) )
15 imcl 
 |-  ( ( ( * ` A ) x. B ) e. CC -> ( Im ` ( ( * ` A ) x. B ) ) e. RR )
16 15 recnd 
 |-  ( ( ( * ` A ) x. B ) e. CC -> ( Im ` ( ( * ` A ) x. B ) ) e. CC )
17 11 16 syl 
 |-  ( ( A e. CC /\ B e. CC /\ C e. RR ) -> ( Im ` ( ( * ` A ) x. B ) ) e. CC )
18 17 7 mulcomd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. RR ) -> ( ( Im ` ( ( * ` A ) x. B ) ) x. C ) = ( C x. ( Im ` ( ( * ` A ) x. B ) ) ) )
19 12 14 18 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. RR ) -> ( Im ` ( ( ( * ` A ) x. B ) x. C ) ) = ( ( Im ` ( ( * ` A ) x. B ) ) x. C ) )
20 9 19 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. RR ) -> ( Im ` ( ( * ` A ) x. ( B x. C ) ) ) = ( ( Im ` ( ( * ` A ) x. B ) ) x. C ) )
21 simpl 
 |-  ( ( B e. CC /\ C e. RR ) -> B e. CC )
22 21 6 mulcld 
 |-  ( ( B e. CC /\ C e. RR ) -> ( B x. C ) e. CC )
23 22 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. RR ) -> ( B x. C ) e. CC )
24 1 sigarval 
 |-  ( ( A e. CC /\ ( B x. C ) e. CC ) -> ( A G ( B x. C ) ) = ( Im ` ( ( * ` A ) x. ( B x. C ) ) ) )
25 2 23 24 syl2anc 
 |-  ( ( A e. CC /\ B e. CC /\ C e. RR ) -> ( A G ( B x. C ) ) = ( Im ` ( ( * ` A ) x. ( B x. C ) ) ) )
26 1 sigarval 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A G B ) = ( Im ` ( ( * ` A ) x. B ) ) )
27 26 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. RR ) -> ( A G B ) = ( Im ` ( ( * ` A ) x. B ) ) )
28 27 oveq1d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. RR ) -> ( ( A G B ) x. C ) = ( ( Im ` ( ( * ` A ) x. B ) ) x. C ) )
29 20 25 28 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. RR ) -> ( A G ( B x. C ) ) = ( ( A G B ) x. C ) )