Metamath Proof Explorer

Theorem sigaradd

Description: Subtracting (double) area of A D C from A B C yields the (double) area of D B C . (Contributed by Saveliy Skresanov, 23-Sep-2017)

Ref Expression
Hypotheses sharhght.sigar ⊢G=x∈ℂ,y∈ℂ⟼ℑ⁡x‾⁢y
sharhght.a ⊢φ→A∈ℂ∧B∈ℂ∧C∈ℂ
sharhght.b ⊢φ→D∈ℂ∧A−DGB−D=0
Assertion sigaradd ⊢φ→B−CGA−C−D−CGA−C=B−CGD−C

Proof

Step Hyp Ref Expression
1 sharhght.sigar ⊢G=x∈ℂ,y∈ℂ⟼ℑ⁡x‾⁢y
2 sharhght.a ⊢φ→A∈ℂ∧B∈ℂ∧C∈ℂ
3 sharhght.b ⊢φ→D∈ℂ∧A−DGB−D=0
4 2 simp1d ⊢φ→A∈ℂ
5 2 simp3d ⊢φ→C∈ℂ
6 3 simpld ⊢φ→D∈ℂ
7 4 5 6 nnncan1d ⊢φ→A-C-A−D=D−C
8 7 oveq2d ⊢φ→B−DGA-C-A−D=B−DGD−C
9 2 simp2d ⊢φ→B∈ℂ
10 9 6 subcld ⊢φ→B−D∈ℂ
11 4 5 subcld ⊢φ→A−C∈ℂ
12 4 6 subcld ⊢φ→A−D∈ℂ
13 1 sigarms ⊢B−D∈ℂ∧A−C∈ℂ∧A−D∈ℂ→B−DGA-C-A−D=B−DGA−C−B−DGA−D
14 10 11 12 13 syl3anc ⊢φ→B−DGA-C-A−D=B−DGA−C−B−DGA−D
15 8 14 eqtr3d ⊢φ→B−DGD−C=B−DGA−C−B−DGA−D
16 1 sigarac ⊢A−D∈ℂ∧B−D∈ℂ→A−DGB−D=−B−DGA−D
17 12 10 16 syl2anc ⊢φ→A−DGB−D=−B−DGA−D
18 3 simprd ⊢φ→A−DGB−D=0
19 17 18 eqtr3d ⊢φ→−B−DGA−D=0
20 19 negeqd ⊢φ→−−B−DGA−D=−0
21 10 12 jca ⊢φ→B−D∈ℂ∧A−D∈ℂ
22 1 21 sigarimcd ⊢φ→B−DGA−D∈ℂ
23 22 negnegd ⊢φ→−−B−DGA−D=B−DGA−D
24 neg0 ⊢−0=0
25 24 a1i ⊢φ→−0=0
26 20 23 25 3eqtr3d ⊢φ→B−DGA−D=0
27 26 oveq2d ⊢φ→B−DGA−C−B−DGA−D=B−DGA−C−0
28 10 11 jca ⊢φ→B−D∈ℂ∧A−C∈ℂ
29 1 28 sigarimcd ⊢φ→B−DGA−C∈ℂ
30 29 subid1d ⊢φ→B−DGA−C−0=B−DGA−C
31 15 27 30 3eqtrd ⊢φ→B−DGD−C=B−DGA−C
32 9 6 5 nnncan2d ⊢φ→B-C-D−C=B−D
33 32 oveq1d ⊢φ→B-C-D−CGA−C=B−DGA−C
34 9 5 subcld ⊢φ→B−C∈ℂ
35 6 5 subcld ⊢φ→D−C∈ℂ
36 1 sigarmf ⊢B−C∈ℂ∧A−C∈ℂ∧D−C∈ℂ→B-C-D−CGA−C=B−CGA−C−D−CGA−C
37 34 11 35 36 syl3anc ⊢φ→B-C-D−CGA−C=B−CGA−C−D−CGA−C
38 31 33 37 3eqtr2rd ⊢φ→B−CGA−C−D−CGA−C=B−DGD−C
39 5 6 subcld ⊢φ→C−D∈ℂ
40 1red ⊢φ→1∈ℝ
41 40 renegcld ⊢φ→−1∈ℝ
42 1 sigarls ⊢B−D∈ℂ∧C−D∈ℂ∧−1∈ℝ→B−DGC−D⁢-1=B−DGC−D⁢-1
43 10 39 41 42 syl3anc ⊢φ→B−DGC−D⁢-1=B−DGC−D⁢-1
44 39 mulm1d ⊢φ→-1⁢C−D=−C−D
45 1cnd ⊢φ→1∈ℂ
46 45 negcld ⊢φ→−1∈ℂ
47 46 39 mulcomd ⊢φ→-1⁢C−D=C−D⁢-1
48 5 6 negsubdi2d ⊢φ→−C−D=D−C
49 44 47 48 3eqtr3d ⊢φ→C−D⁢-1=D−C
50 49 oveq2d ⊢φ→B−DGC−D⁢-1=B−DGD−C
51 10 39 jca ⊢φ→B−D∈ℂ∧C−D∈ℂ
52 1 51 sigarimcd ⊢φ→B−DGC−D∈ℂ
53 52 mulm1d ⊢φ→-1⁢B−DGC−D=−B−DGC−D
54 52 46 mulcomd ⊢φ→B−DGC−D⁢-1=-1⁢B−DGC−D
55 1 sigarac ⊢C−D∈ℂ∧B−D∈ℂ→C−DGB−D=−B−DGC−D
56 39 10 55 syl2anc ⊢φ→C−DGB−D=−B−DGC−D
57 53 54 56 3eqtr4d ⊢φ→B−DGC−D⁢-1=C−DGB−D
58 43 50 57 3eqtr3d ⊢φ→B−DGD−C=C−DGB−D
59 1 sigarperm ⊢C∈ℂ∧B∈ℂ∧D∈ℂ→C−DGB−D=B−CGD−C
60 5 9 6 59 syl3anc ⊢φ→C−DGB−D=B−CGD−C
61 38 58 60 3eqtrd ⊢φ→B−CGA−C−D−CGA−C=B−CGD−C