Metamath Proof Explorer

Theorem sigarmf

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

Ref Expression
Hypothesis sigar ⊢ G = x ∈ ℂ , y ∈ ℂ ⟼ ℑ ⁡ x ‾ ⁢ y
Assertion sigarmf ⊢ 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 cjsub ⊢ 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 subdird ⊢ 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 imsubd ⊢ 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 subcld ⊢ 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