Metamath Proof Explorer

Theorem sigaras

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

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

Proof

Step Hyp Ref Expression
1 sigar ⊢ G = x ∈ ℂ , y ∈ ℂ ⟼ ℑ ⁡ x ‾ ⁢ y
2 simp1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ∈ ℂ
3 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B ∈ ℂ
4 simp3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ∈ ℂ
5 3 4 addcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B + C ∈ ℂ
6 1 sigarac ⊢ A ∈ ℂ ∧ B + C ∈ ℂ → A G B + C = − B + C G A
7 2 5 6 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A G B + C = − B + C G A
8 1 sigaraf ⊢ B ∈ ℂ ∧ A ∈ ℂ ∧ C ∈ ℂ → B + C G A = B G A + C G A
9 8 negeqd ⊢ B ∈ ℂ ∧ A ∈ ℂ ∧ C ∈ ℂ → − B + C G A = − B G A + C G A
10 9 3com12 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → − B + C G A = − B G A + C G A
11 3simpa ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ∈ ℂ ∧ B ∈ ℂ
12 11 ancomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B ∈ ℂ ∧ A ∈ ℂ
13 1 sigarim ⊢ B ∈ ℂ ∧ A ∈ ℂ → B G A ∈ ℝ
14 12 13 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B G A ∈ ℝ
15 14 recnd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B G A ∈ ℂ
16 3simpb ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ∈ ℂ ∧ C ∈ ℂ
17 16 ancomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ∈ ℂ ∧ A ∈ ℂ
18 1 sigarim ⊢ C ∈ ℂ ∧ A ∈ ℂ → C G A ∈ ℝ
19 17 18 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C G A ∈ ℝ
20 19 recnd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C G A ∈ ℂ
21 15 20 negdid ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → − B G A + C G A = - B G A + − C G A
22 10 21 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → − B + C G A = - B G A + − C G A
23 1 sigarac ⊢ A ∈ ℂ ∧ B ∈ ℂ → A G B = − B G A
24 2 3 23 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A G B = − B G A
25 24 eqcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → − B G A = A G B
26 1 sigarac ⊢ A ∈ ℂ ∧ C ∈ ℂ → A G C = − C G A
27 2 4 26 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A G C = − C G A
28 27 eqcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → − C G A = A G C
29 25 28 oveq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → - B G A + − C G A = A G B + A G C
30 7 22 29 3eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A G B + C = A G B + A G C