Metamath Proof Explorer

Theorem sigarexp

Description: Expand the signed area formula by linearity. (Contributed by Saveliy Skresanov, 20-Sep-2017)

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

Proof

Step Hyp Ref Expression
1 sigar ⊢ G = x ∈ ℂ , y ∈ ℂ ⟼ ℑ ⁡ x ‾ ⁢ y
2 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B ∈ ℂ
3 simp3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ∈ ℂ
4 2 3 subcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B − C ∈ ℂ
5 1 sigarmf ⊢ A ∈ ℂ ∧ B − C ∈ ℂ ∧ C ∈ ℂ → A − C G B − C = A G B − C − C G B − C
6 4 5 syld3an2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − C G B − C = A G B − C − C G B − C
7 1 sigarms ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A G B − C = A G B − A G C
8 7 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A G B − C − C G B − C = A G B - A G C - C G B − C
9 1 sigarms ⊢ C ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C G B − C = C G B − C G C
10 3 9 syld3an1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C G B − C = C G B − C G C
11 1 sigarid ⊢ C ∈ ℂ → C G C = 0
12 3 11 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C G C = 0
13 12 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C G B − C G C = C G B − 0
14 1 sigarim ⊢ C ∈ ℂ ∧ B ∈ ℂ → C G B ∈ ℝ
15 14 recnd ⊢ C ∈ ℂ ∧ B ∈ ℂ → C G B ∈ ℂ
16 3 2 15 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C G B ∈ ℂ
17 16 subid1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C G B − 0 = C G B
18 10 13 17 3eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C G B − C = C G B
19 18 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A G B - A G C - C G B − C = A G B - A G C - C G B
20 6 8 19 3eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − C G B − C = A G B - A G C - C G B