Theorem sigarls

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

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

Proof

Step	Hyp	Ref	Expression
1		sigar	⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
2		simp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℂ )
3	2	cjcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → ( ∗ ‘ 𝐴 ) ∈ ℂ )
4		simp2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
5		simpr	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
6	5	recnd	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℂ )
7	6	3adant1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℂ )
8	3 4 7	mulassd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → ( ( ( ∗ ‘ 𝐴 ) · 𝐵 ) · 𝐶 ) = ( ( ∗ ‘ 𝐴 ) · ( 𝐵 · 𝐶 ) ) )
9	8	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → ( ℑ ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐵 ) · 𝐶 ) ) = ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · ( 𝐵 · 𝐶 ) ) ) )
10		simp3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
11	3 4	mulcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ∈ ℂ )
12	10 11	immul2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → ( ℑ ‘ ( 𝐶 · ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) ) = ( 𝐶 · ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) ) )
13	11 7	mulcomd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → ( ( ( ∗ ‘ 𝐴 ) · 𝐵 ) · 𝐶 ) = ( 𝐶 · ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) )
14	13	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → ( ℑ ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐵 ) · 𝐶 ) ) = ( ℑ ‘ ( 𝐶 · ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) ) )
15		imcl	⊢ ( ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ∈ ℂ → ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) ∈ ℝ )
16	15	recnd	⊢ ( ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ∈ ℂ → ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) ∈ ℂ )
17	11 16	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) ∈ ℂ )
18	17 7	mulcomd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → ( ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) · 𝐶 ) = ( 𝐶 · ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) ) )
19	12 14 18	3eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → ( ℑ ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐵 ) · 𝐶 ) ) = ( ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) · 𝐶 ) )
20	9 19	eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · ( 𝐵 · 𝐶 ) ) ) = ( ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) · 𝐶 ) )
21		simpl	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
22	21 6	mulcld	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
23	22	3adant1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
24	1	sigarval	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 · 𝐶 ) ∈ ℂ ) → ( 𝐴 𝐺 ( 𝐵 · 𝐶 ) ) = ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · ( 𝐵 · 𝐶 ) ) ) )
25	2 23 24	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 𝐺 ( 𝐵 · 𝐶 ) ) = ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · ( 𝐵 · 𝐶 ) ) ) )
26	1	sigarval	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 𝐺 𝐵 ) = ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) )
27	26	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 𝐺 𝐵 ) = ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) )
28	27	oveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 𝐺 𝐵 ) · 𝐶 ) = ( ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) · 𝐶 ) )
29	20 25 28	3eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 𝐺 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 𝐺 𝐵 ) · 𝐶 ) )