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∈ℂ→AGB−C=AGB−AGC

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∈ℂ→AGB−C=−B−CGA
7 2 5 6 syl2anc ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→AGB−C=−B−CGA
8 1 sigarmf ⊢B∈ℂ∧A∈ℂ∧C∈ℂ→B−CGA=BGA−CGA
9 8 negeqd ⊢B∈ℂ∧A∈ℂ∧C∈ℂ→−B−CGA=−BGA−CGA
10 9 3com12 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→−B−CGA=−BGA−CGA
11 3simpa ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A∈ℂ∧B∈ℂ
12 11 ancomd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B∈ℂ∧A∈ℂ
13 1 sigarim ⊢B∈ℂ∧A∈ℂ→BGA∈ℝ
14 12 13 syl ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→BGA∈ℝ
15 14 recnd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→BGA∈ℂ
16 3simpb ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A∈ℂ∧C∈ℂ
17 16 ancomd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→C∈ℂ∧A∈ℂ
18 1 sigarim ⊢C∈ℂ∧A∈ℂ→CGA∈ℝ
19 17 18 syl ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→CGA∈ℝ
20 19 recnd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→CGA∈ℂ
21 negsubdi ⊢BGA∈ℂ∧CGA∈ℂ→−BGA−CGA=-BGA+CGA
22 simpl ⊢BGA∈ℂ∧CGA∈ℂ→BGA∈ℂ
23 22 negcld ⊢BGA∈ℂ∧CGA∈ℂ→−BGA∈ℂ
24 simpr ⊢BGA∈ℂ∧CGA∈ℂ→CGA∈ℂ
25 23 24 subnegd ⊢BGA∈ℂ∧CGA∈ℂ→-BGA-−CGA=-BGA+CGA
26 21 25 eqtr4d ⊢BGA∈ℂ∧CGA∈ℂ→−BGA−CGA=-BGA-−CGA
27 15 20 26 syl2anc ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→−BGA−CGA=-BGA-−CGA
28 10 27 eqtrd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→−B−CGA=-BGA-−CGA
29 1 sigarac ⊢A∈ℂ∧B∈ℂ→AGB=−BGA
30 2 3 29 syl2anc ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→AGB=−BGA
31 30 eqcomd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→−BGA=AGB
32 1 sigarac ⊢A∈ℂ∧C∈ℂ→AGC=−CGA
33 2 4 32 syl2anc ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→AGC=−CGA
34 33 eqcomd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→−CGA=AGC
35 31 34 oveq12d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→-BGA-−CGA=AGB−AGC
36 7 28 35 3eqtrd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→AGB−C=AGB−AGC