Metamath Proof Explorer

Theorem sigarms

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

Ref Expression
Hypothesis sigar ⊢ G = x ∈ ℂ , y ∈ ℂ ⟼ ℑ ⁡ x ‾ ⁢ y
Assertion sigarms ⊢ 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 subcld ⊢ 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 sigarmf ⊢ 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 negsubdi ⊢ B G A ∈ ℂ ∧ C G A ∈ ℂ → − B G A − C G A = - B G A + C G A
22 simpl ⊢ B G A ∈ ℂ ∧ C G A ∈ ℂ → B G A ∈ ℂ
23 22 negcld ⊢ B G A ∈ ℂ ∧ C G A ∈ ℂ → − B G A ∈ ℂ
24 simpr ⊢ B G A ∈ ℂ ∧ C G A ∈ ℂ → C G A ∈ ℂ
25 23 24 subnegd ⊢ B G A ∈ ℂ ∧ C G A ∈ ℂ → - B G A - − C G A = - B G A + C G A
26 21 25 eqtr4d ⊢ B G A ∈ ℂ ∧ C G A ∈ ℂ → − B G A − C G A = - B G A - − C G A
27 15 20 26 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → − B G A − C G A = - B G A - − C G A
28 10 27 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → − B − C G A = - B G A - − C G A
29 1 sigarac ⊢ A ∈ ℂ ∧ B ∈ ℂ → A G B = − B G A
30 2 3 29 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A G B = − B G A
31 30 eqcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → − B G A = A G B
32 1 sigarac ⊢ A ∈ ℂ ∧ C ∈ ℂ → A G C = − C G A
33 2 4 32 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A G C = − C G A
34 33 eqcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → − C G A = A G C
35 31 34 oveq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → - B G A - − C G A = A G B − A G C
36 7 28 35 3eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A G B − C = A G B − A G C