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−CGB=AGB−CGB

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−CGB=ℑ⁡A−C‾⁢B
19 17 9 18 syl2anc ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−CGB=ℑ⁡A−C‾⁢B
20 1 sigarval ⊢A∈ℂ∧B∈ℂ→AGB=ℑ⁡A‾⁢B
21 20 3adant3 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→AGB=ℑ⁡A‾⁢B
22 3simpc ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B∈ℂ∧C∈ℂ
23 22 ancomd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→C∈ℂ∧B∈ℂ
24 1 sigarval ⊢C∈ℂ∧B∈ℂ→CGB=ℑ⁡C‾⁢B
25 23 24 syl ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→CGB=ℑ⁡C‾⁢B
26 21 25 oveq12d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→AGB−CGB=ℑ⁡A‾⁢B−ℑ⁡C‾⁢B
27 16 19 26 3eqtr4d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−CGB=AGB−CGB