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 ∈ ℂ , y ∈ ℂ ⟼ ℑ ⁡ x ‾ ⁢ y
Assertion sigarls ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℝ → A G B ⁢ C = A G B ⁢ C

Proof

Step Hyp Ref Expression
1 sigar ⊢ G = x ∈ ℂ , y ∈ ℂ ⟼ ℑ ⁡ x ‾ ⁢ y
2 simp1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℝ → A ∈ ℂ
3 2 cjcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℝ → A ‾ ∈ ℂ
4 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℝ → B ∈ ℂ
5 simpr ⊢ B ∈ ℂ ∧ C ∈ ℝ → C ∈ ℝ
6 5 recnd ⊢ B ∈ ℂ ∧ C ∈ ℝ → C ∈ ℂ
7 6 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℝ → C ∈ ℂ
8 3 4 7 mulassd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℝ → A ‾ ⁢ B ⁢ C = A ‾ ⁢ B ⁢ C
9 8 fveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℝ → ℑ ⁡ A ‾ ⁢ B ⁢ C = ℑ ⁡ A ‾ ⁢ B ⁢ C
10 simp3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℝ → C ∈ ℝ
11 3 4 mulcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℝ → A ‾ ⁢ B ∈ ℂ
12 10 11 immul2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℝ → ℑ ⁡ C ⁢ A ‾ ⁢ B = C ⁢ ℑ ⁡ A ‾ ⁢ B
13 11 7 mulcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℝ → A ‾ ⁢ B ⁢ C = C ⁢ A ‾ ⁢ B
14 13 fveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℝ → ℑ ⁡ A ‾ ⁢ B ⁢ C = ℑ ⁡ C ⁢ A ‾ ⁢ B
15 imcl ⊢ A ‾ ⁢ B ∈ ℂ → ℑ ⁡ A ‾ ⁢ B ∈ ℝ
16 15 recnd ⊢ A ‾ ⁢ B ∈ ℂ → ℑ ⁡ A ‾ ⁢ B ∈ ℂ
17 11 16 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℝ → ℑ ⁡ A ‾ ⁢ B ∈ ℂ
18 17 7 mulcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℝ → ℑ ⁡ A ‾ ⁢ B ⁢ C = C ⁢ ℑ ⁡ A ‾ ⁢ B
19 12 14 18 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℝ → ℑ ⁡ A ‾ ⁢ B ⁢ C = ℑ ⁡ A ‾ ⁢ B ⁢ C
20 9 19 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℝ → ℑ ⁡ A ‾ ⁢ B ⁢ C = ℑ ⁡ A ‾ ⁢ B ⁢ C
21 simpl ⊢ B ∈ ℂ ∧ C ∈ ℝ → B ∈ ℂ
22 21 6 mulcld ⊢ B ∈ ℂ ∧ C ∈ ℝ → B ⁢ C ∈ ℂ
23 22 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℝ → B ⁢ C ∈ ℂ
24 1 sigarval ⊢ A ∈ ℂ ∧ B ⁢ C ∈ ℂ → A G B ⁢ C = ℑ ⁡ A ‾ ⁢ B ⁢ C
25 2 23 24 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℝ → A G B ⁢ C = ℑ ⁡ A ‾ ⁢ B ⁢ C
26 1 sigarval ⊢ A ∈ ℂ ∧ B ∈ ℂ → A G B = ℑ ⁡ A ‾ ⁢ B
27 26 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℝ → A G B = ℑ ⁡ A ‾ ⁢ B
28 27 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℝ → A G B ⁢ C = ℑ ⁡ A ‾ ⁢ B ⁢ C
29 20 25 28 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℝ → A G B ⁢ C = A G B ⁢ C