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 ⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
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 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 𝐺 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 𝐺 𝐵 ) · 𝐶 ) )