Theorem sigarms

Description: Signed area is additive (with respect to subtraction) by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017)

	Ref	Expression
Hypothesis	sigar	⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
Assertion	sigarms	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 ( 𝐵 − 𝐶 ) ) = ( ( 𝐴 𝐺 𝐵 ) − ( 𝐴 𝐺 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sigar	⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
2		simp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐴 ∈ ℂ )
3		simp2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ℂ )
4		simp3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐶 ∈ ℂ )
5	3 4	subcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 − 𝐶 ) ∈ ℂ )
6	1	sigarac	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 − 𝐶 ) ∈ ℂ ) → ( 𝐴 𝐺 ( 𝐵 − 𝐶 ) ) = - ( ( 𝐵 − 𝐶 ) 𝐺 𝐴 ) )
7	2 5 6	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 ( 𝐵 − 𝐶 ) ) = - ( ( 𝐵 − 𝐶 ) 𝐺 𝐴 ) )
8	1	sigarmf	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 − 𝐶 ) 𝐺 𝐴 ) = ( ( 𝐵 𝐺 𝐴 ) − ( 𝐶 𝐺 𝐴 ) ) )
9	8	negeqd	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → - ( ( 𝐵 − 𝐶 ) 𝐺 𝐴 ) = - ( ( 𝐵 𝐺 𝐴 ) − ( 𝐶 𝐺 𝐴 ) ) )
10	9	3com12	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → - ( ( 𝐵 − 𝐶 ) 𝐺 𝐴 ) = - ( ( 𝐵 𝐺 𝐴 ) − ( 𝐶 𝐺 𝐴 ) ) )
11		3simpa	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) )
12	11	ancomd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
13	1	sigarim	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝐵 𝐺 𝐴 ) ∈ ℝ )
14	12 13	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 𝐺 𝐴 ) ∈ ℝ )
15	14	recnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 𝐺 𝐴 ) ∈ ℂ )
16		3simpb	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
17	16	ancomd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
18	1	sigarim	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝐶 𝐺 𝐴 ) ∈ ℝ )
19	17 18	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 𝐺 𝐴 ) ∈ ℝ )
20	19	recnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 𝐺 𝐴 ) ∈ ℂ )
21		negsubdi	⊢ ( ( ( 𝐵 𝐺 𝐴 ) ∈ ℂ ∧ ( 𝐶 𝐺 𝐴 ) ∈ ℂ ) → - ( ( 𝐵 𝐺 𝐴 ) − ( 𝐶 𝐺 𝐴 ) ) = ( - ( 𝐵 𝐺 𝐴 ) + ( 𝐶 𝐺 𝐴 ) ) )
22		simpl	⊢ ( ( ( 𝐵 𝐺 𝐴 ) ∈ ℂ ∧ ( 𝐶 𝐺 𝐴 ) ∈ ℂ ) → ( 𝐵 𝐺 𝐴 ) ∈ ℂ )
23	22	negcld	⊢ ( ( ( 𝐵 𝐺 𝐴 ) ∈ ℂ ∧ ( 𝐶 𝐺 𝐴 ) ∈ ℂ ) → - ( 𝐵 𝐺 𝐴 ) ∈ ℂ )
24		simpr	⊢ ( ( ( 𝐵 𝐺 𝐴 ) ∈ ℂ ∧ ( 𝐶 𝐺 𝐴 ) ∈ ℂ ) → ( 𝐶 𝐺 𝐴 ) ∈ ℂ )
25	23 24	subnegd	⊢ ( ( ( 𝐵 𝐺 𝐴 ) ∈ ℂ ∧ ( 𝐶 𝐺 𝐴 ) ∈ ℂ ) → ( - ( 𝐵 𝐺 𝐴 ) − - ( 𝐶 𝐺 𝐴 ) ) = ( - ( 𝐵 𝐺 𝐴 ) + ( 𝐶 𝐺 𝐴 ) ) )
26	21 25	eqtr4d	⊢ ( ( ( 𝐵 𝐺 𝐴 ) ∈ ℂ ∧ ( 𝐶 𝐺 𝐴 ) ∈ ℂ ) → - ( ( 𝐵 𝐺 𝐴 ) − ( 𝐶 𝐺 𝐴 ) ) = ( - ( 𝐵 𝐺 𝐴 ) − - ( 𝐶 𝐺 𝐴 ) ) )
27	15 20 26	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → - ( ( 𝐵 𝐺 𝐴 ) − ( 𝐶 𝐺 𝐴 ) ) = ( - ( 𝐵 𝐺 𝐴 ) − - ( 𝐶 𝐺 𝐴 ) ) )
28	10 27	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → - ( ( 𝐵 − 𝐶 ) 𝐺 𝐴 ) = ( - ( 𝐵 𝐺 𝐴 ) − - ( 𝐶 𝐺 𝐴 ) ) )
29	1	sigarac	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 𝐺 𝐵 ) = - ( 𝐵 𝐺 𝐴 ) )
30	2 3 29	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 𝐵 ) = - ( 𝐵 𝐺 𝐴 ) )
31	30	eqcomd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → - ( 𝐵 𝐺 𝐴 ) = ( 𝐴 𝐺 𝐵 ) )
32	1	sigarac	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 𝐶 ) = - ( 𝐶 𝐺 𝐴 ) )
33	2 4 32	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 𝐶 ) = - ( 𝐶 𝐺 𝐴 ) )
34	33	eqcomd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → - ( 𝐶 𝐺 𝐴 ) = ( 𝐴 𝐺 𝐶 ) )
35	31 34	oveq12d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( - ( 𝐵 𝐺 𝐴 ) − - ( 𝐶 𝐺 𝐴 ) ) = ( ( 𝐴 𝐺 𝐵 ) − ( 𝐴 𝐺 𝐶 ) ) )
36	7 28 35	3eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 ( 𝐵 − 𝐶 ) ) = ( ( 𝐴 𝐺 𝐵 ) − ( 𝐴 𝐺 𝐶 ) ) )