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 − D G B − D = 0
Assertion sigaradd ⊢ φ → B − C G A − C − D − C G A − C = B − C G D − 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 − D G B − 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 − D G A - C - A − D = B − D G D − 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 − D G A - C - A − D = B − D G A − C − B − D G A − D
14 10 11 12 13 syl3anc ⊢ φ → B − D G A - C - A − D = B − D G A − C − B − D G A − D
15 8 14 eqtr3d ⊢ φ → B − D G D − C = B − D G A − C − B − D G A − D
16 1 sigarac ⊢ A − D ∈ ℂ ∧ B − D ∈ ℂ → A − D G B − D = − B − D G A − D
17 12 10 16 syl2anc ⊢ φ → A − D G B − D = − B − D G A − D
18 3 simprd ⊢ φ → A − D G B − D = 0
19 17 18 eqtr3d ⊢ φ → − B − D G A − D = 0
20 19 negeqd ⊢ φ → − − B − D G A − D = − 0
21 10 12 jca ⊢ φ → B − D ∈ ℂ ∧ A − D ∈ ℂ
22 1 21 sigarimcd ⊢ φ → B − D G A − D ∈ ℂ
23 22 negnegd ⊢ φ → − − B − D G A − D = B − D G A − D
24 neg0 ⊢ − 0 = 0
25 24 a1i ⊢ φ → − 0 = 0
26 20 23 25 3eqtr3d ⊢ φ → B − D G A − D = 0
27 26 oveq2d ⊢ φ → B − D G A − C − B − D G A − D = B − D G A − C − 0
28 10 11 jca ⊢ φ → B − D ∈ ℂ ∧ A − C ∈ ℂ
29 1 28 sigarimcd ⊢ φ → B − D G A − C ∈ ℂ
30 29 subid1d ⊢ φ → B − D G A − C − 0 = B − D G A − C
31 15 27 30 3eqtrd ⊢ φ → B − D G D − C = B − D G A − C
32 9 6 5 nnncan2d ⊢ φ → B - C - D − C = B − D
33 32 oveq1d ⊢ φ → B - C - D − C G A − C = B − D G A − 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 − C G A − C = B − C G A − C − D − C G A − C
37 34 11 35 36 syl3anc ⊢ φ → B - C - D − C G A − C = B − C G A − C − D − C G A − C
38 31 33 37 3eqtr2rd ⊢ φ → B − C G A − C − D − C G A − C = B − D G D − C
39 5 6 subcld ⊢ φ → C − D ∈ ℂ
40 1red ⊢ φ → 1 ∈ ℝ
41 40 renegcld ⊢ φ → − 1 ∈ ℝ
42 1 sigarls ⊢ B − D ∈ ℂ ∧ C − D ∈ ℂ ∧ − 1 ∈ ℝ → B − D G C − D ⁢ -1 = B − D G C − D ⁢ -1
43 10 39 41 42 syl3anc ⊢ φ → B − D G C − D ⁢ -1 = B − D G C − 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 − D G C − D ⁢ -1 = B − D G D − C
51 10 39 jca ⊢ φ → B − D ∈ ℂ ∧ C − D ∈ ℂ
52 1 51 sigarimcd ⊢ φ → B − D G C − D ∈ ℂ
53 52 mulm1d ⊢ φ → -1 ⁢ B − D G C − D = − B − D G C − D
54 52 46 mulcomd ⊢ φ → B − D G C − D ⁢ -1 = -1 ⁢ B − D G C − D
55 1 sigarac ⊢ C − D ∈ ℂ ∧ B − D ∈ ℂ → C − D G B − D = − B − D G C − D
56 39 10 55 syl2anc ⊢ φ → C − D G B − D = − B − D G C − D
57 53 54 56 3eqtr4d ⊢ φ → B − D G C − D ⁢ -1 = C − D G B − D
58 43 50 57 3eqtr3d ⊢ φ → B − D G D − C = C − D G B − D
59 1 sigarperm ⊢ C ∈ ℂ ∧ B ∈ ℂ ∧ D ∈ ℂ → C − D G B − D = B − C G D − C
60 5 9 6 59 syl3anc ⊢ φ → C − D G B − D = B − C G D − C
61 38 58 60 3eqtrd ⊢ φ → B − C G A − C − D − C G A − C = B − C G D − C