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