Metamath Proof Explorer

Theorem sigaraf

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

Ref Expression
Hypothesis sigar ⊢ G = x ∈ ℂ , y ∈ ℂ ⟼ ℑ ⁡ x ‾ ⁢ y
Assertion sigaraf ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + C G B = A G B + C G B

Proof

Step Hyp Ref Expression
1 sigar ⊢ G = x ∈ ℂ , y ∈ ℂ ⟼ ℑ ⁡ x ‾ ⁢ y
2 cjadd ⊢ A ∈ ℂ ∧ C ∈ ℂ → A + C ‾ = A ‾ + C ‾
3 2 oveq1d ⊢ A ∈ ℂ ∧ C ∈ ℂ → A + C ‾ ⁢ B = A ‾ + C ‾ ⁢ B
4 3 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + C ‾ ⁢ B = A ‾ + C ‾ ⁢ B
5 simp1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ∈ ℂ
6 5 cjcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ‾ ∈ ℂ
7 simp3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ∈ ℂ
8 7 cjcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ‾ ∈ ℂ
9 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B ∈ ℂ
10 6 8 9 adddird ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ‾ + C ‾ ⁢ B = A ‾ ⁢ B + C ‾ ⁢ B
11 4 10 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + C ‾ ⁢ B = A ‾ ⁢ B + C ‾ ⁢ B
12 11 fveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → ℑ ⁡ A + C ‾ ⁢ B = ℑ ⁡ A ‾ ⁢ B + C ‾ ⁢ B
13 6 9 mulcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ‾ ⁢ B ∈ ℂ
14 8 9 mulcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ‾ ⁢ B ∈ ℂ
15 13 14 imaddd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → ℑ ⁡ A ‾ ⁢ B + C ‾ ⁢ B = ℑ ⁡ A ‾ ⁢ B + ℑ ⁡ C ‾ ⁢ B
16 12 15 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → ℑ ⁡ A + C ‾ ⁢ B = ℑ ⁡ A ‾ ⁢ B + ℑ ⁡ C ‾ ⁢ B
17 5 7 addcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + C ∈ ℂ
18 1 sigarval ⊢ A + C ∈ ℂ ∧ B ∈ ℂ → A + C G B = ℑ ⁡ A + C ‾ ⁢ B
19 17 9 18 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + C G B = ℑ ⁡ A + C ‾ ⁢ B
20 1 sigarval ⊢ A ∈ ℂ ∧ B ∈ ℂ → A G B = ℑ ⁡ A ‾ ⁢ B
21 20 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A G B = ℑ ⁡ A ‾ ⁢ B
22 3simpc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B ∈ ℂ ∧ C ∈ ℂ
23 22 ancomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ∈ ℂ ∧ B ∈ ℂ
24 1 sigarval ⊢ C ∈ ℂ ∧ B ∈ ℂ → C G B = ℑ ⁡ C ‾ ⁢ B
25 23 24 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C G B = ℑ ⁡ C ‾ ⁢ B
26 21 25 oveq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A G B + C G B = ℑ ⁡ A ‾ ⁢ B + ℑ ⁡ C ‾ ⁢ B
27 16 19 26 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + C G B = A G B + C G B