Metamath Proof Explorer


Theorem sigaraf

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

Ref Expression
Hypothesis sigar G = x , y x y
Assertion sigaraf 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 cjadd 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 adddird 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 imaddd 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 addcld 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