Theorem sigarmf

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

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

Proof

Step	Hyp	Ref	Expression
1		sigar	⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
2		cjsub	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ∗ ‘ ( 𝐴 − 𝐶 ) ) = ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) )
3	2	oveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ∗ ‘ ( 𝐴 − 𝐶 ) ) · 𝐵 ) = ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · 𝐵 ) )
4	3	3adant2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ∗ ‘ ( 𝐴 − 𝐶 ) ) · 𝐵 ) = ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · 𝐵 ) )
5		simp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐴 ∈ ℂ )
6	5	cjcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ∗ ‘ 𝐴 ) ∈ ℂ )
7		simp3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐶 ∈ ℂ )
8	7	cjcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ∗ ‘ 𝐶 ) ∈ ℂ )
9		simp2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ℂ )
10	6 8 9	subdird	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · 𝐵 ) = ( ( ( ∗ ‘ 𝐴 ) · 𝐵 ) − ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ) )
11	4 10	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ∗ ‘ ( 𝐴 − 𝐶 ) ) · 𝐵 ) = ( ( ( ∗ ‘ 𝐴 ) · 𝐵 ) − ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ) )
12	11	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ℑ ‘ ( ( ∗ ‘ ( 𝐴 − 𝐶 ) ) · 𝐵 ) ) = ( ℑ ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐵 ) − ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ) ) )
13	6 9	mulcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ∈ ℂ )
14	8 9	mulcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ∈ ℂ )
15	13 14	imsubd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ℑ ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐵 ) − ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ) ) = ( ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) − ( ℑ ‘ ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ) ) )
16	12 15	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ℑ ‘ ( ( ∗ ‘ ( 𝐴 − 𝐶 ) ) · 𝐵 ) ) = ( ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) − ( ℑ ‘ ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ) ) )
17	5 7	subcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 − 𝐶 ) ∈ ℂ )
18	1	sigarval	⊢ ( ( ( 𝐴 − 𝐶 ) ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 − 𝐶 ) 𝐺 𝐵 ) = ( ℑ ‘ ( ( ∗ ‘ ( 𝐴 − 𝐶 ) ) · 𝐵 ) ) )
19	17 9 18	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐶 ) 𝐺 𝐵 ) = ( ℑ ‘ ( ( ∗ ‘ ( 𝐴 − 𝐶 ) ) · 𝐵 ) ) )
20	1	sigarval	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 𝐺 𝐵 ) = ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) )
21	20	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 𝐵 ) = ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) )
22		3simpc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
23	22	ancomd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) )
24	1	sigarval	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐶 𝐺 𝐵 ) = ( ℑ ‘ ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ) )
25	23 24	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 𝐺 𝐵 ) = ( ℑ ‘ ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ) )
26	21 25	oveq12d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 𝐺 𝐵 ) − ( 𝐶 𝐺 𝐵 ) ) = ( ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) − ( ℑ ‘ ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ) ) )
27	16 19 26	3eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐶 ) 𝐺 𝐵 ) = ( ( 𝐴 𝐺 𝐵 ) − ( 𝐶 𝐺 𝐵 ) ) )