Metamath Proof Explorer


Theorem sigarls

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

Ref Expression
Hypothesis sigar G = x , y x y
Assertion sigarls A B C A G B C = A G B C

Proof

Step Hyp Ref Expression
1 sigar G = x , y x y
2 simp1 A B C A
3 2 cjcld A B C A
4 simp2 A B C B
5 simpr B C C
6 5 recnd B C C
7 6 3adant1 A B C C
8 3 4 7 mulassd A B C A B C = A B C
9 8 fveq2d A B C A B C = A B C
10 simp3 A B C C
11 3 4 mulcld A B C A B
12 10 11 immul2d A B C C A B = C A B
13 11 7 mulcomd A B C A B C = C A B
14 13 fveq2d A B C A B C = C A B
15 imcl A B A B
16 15 recnd A B A B
17 11 16 syl A B C A B
18 17 7 mulcomd A B C A B C = C A B
19 12 14 18 3eqtr4d A B C A B C = A B C
20 9 19 eqtr3d A B C A B C = A B C
21 simpl B C B
22 21 6 mulcld B C B C
23 22 3adant1 A B C B C
24 1 sigarval A B C A G B C = A B C
25 2 23 24 syl2anc A B C A G B C = A B C
26 1 sigarval A B A G B = A B
27 26 3adant3 A B C A G B = A B
28 27 oveq1d A B C A G B C = A B C
29 20 25 28 3eqtr4d A B C A G B C = A G B C