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 ⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
sharhght.a ⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
sharhght.b ⊢ ( 𝜑 → ( 𝐷 ∈ ℂ ∧ ( ( 𝐴 − 𝐷 ) 𝐺 ( 𝐵 − 𝐷 ) ) = 0 ) )
Assertion sigaradd ( 𝜑 → ( ( ( 𝐵 − 𝐶 ) 𝐺 ( 𝐴 − 𝐶 ) ) − ( ( 𝐷 − 𝐶 ) 𝐺 ( 𝐴 − 𝐶 ) ) ) = ( ( 𝐵 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 sharhght.sigar ⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
2 sharhght.a ⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
3 sharhght.b ⊢ ( 𝜑 → ( 𝐷 ∈ ℂ ∧ ( ( 𝐴 − 𝐷 ) 𝐺 ( 𝐵 − 𝐷 ) ) = 0 ) )
4 2 simp1d ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
5 2 simp3d ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
6 3 simpld ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
7 4 5 6 nnncan1d ⊢ ( 𝜑 → ( ( 𝐴 − 𝐶 ) − ( 𝐴 − 𝐷 ) ) = ( 𝐷 − 𝐶 ) )
8 7 oveq2d ⊢ ( 𝜑 → ( ( 𝐵 − 𝐷 ) 𝐺 ( ( 𝐴 − 𝐶 ) − ( 𝐴 − 𝐷 ) ) ) = ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐷 − 𝐶 ) ) )
9 2 simp2d ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
10 9 6 subcld ⊢ ( 𝜑 → ( 𝐵 − 𝐷 ) ∈ ℂ )
11 4 5 subcld ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) ∈ ℂ )
12 4 6 subcld ⊢ ( 𝜑 → ( 𝐴 − 𝐷 ) ∈ ℂ )
13 1 sigarms ⊢ ( ( ( 𝐵 − 𝐷 ) ∈ ℂ ∧ ( 𝐴 − 𝐶 ) ∈ ℂ ∧ ( 𝐴 − 𝐷 ) ∈ ℂ ) → ( ( 𝐵 − 𝐷 ) 𝐺 ( ( 𝐴 − 𝐶 ) − ( 𝐴 − 𝐷 ) ) ) = ( ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐴 − 𝐶 ) ) − ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐴 − 𝐷 ) ) ) )
14 10 11 12 13 syl3anc ⊢ ( 𝜑 → ( ( 𝐵 − 𝐷 ) 𝐺 ( ( 𝐴 − 𝐶 ) − ( 𝐴 − 𝐷 ) ) ) = ( ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐴 − 𝐶 ) ) − ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐴 − 𝐷 ) ) ) )
15 8 14 eqtr3d ⊢ ( 𝜑 → ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐷 − 𝐶 ) ) = ( ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐴 − 𝐶 ) ) − ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐴 − 𝐷 ) ) ) )
16 1 sigarac ⊢ ( ( ( 𝐴 − 𝐷 ) ∈ ℂ ∧ ( 𝐵 − 𝐷 ) ∈ ℂ ) → ( ( 𝐴 − 𝐷 ) 𝐺 ( 𝐵 − 𝐷 ) ) = - ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐴 − 𝐷 ) ) )
17 12 10 16 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 − 𝐷 ) 𝐺 ( 𝐵 − 𝐷 ) ) = - ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐴 − 𝐷 ) ) )
18 3 simprd ⊢ ( 𝜑 → ( ( 𝐴 − 𝐷 ) 𝐺 ( 𝐵 − 𝐷 ) ) = 0 )
19 17 18 eqtr3d ⊢ ( 𝜑 → - ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐴 − 𝐷 ) ) = 0 )
20 19 negeqd ⊢ ( 𝜑 → - - ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐴 − 𝐷 ) ) = - 0 )
21 10 12 jca ⊢ ( 𝜑 → ( ( 𝐵 − 𝐷 ) ∈ ℂ ∧ ( 𝐴 − 𝐷 ) ∈ ℂ ) )
22 1 21 sigarimcd ⊢ ( 𝜑 → ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐴 − 𝐷 ) ) ∈ ℂ )
23 22 negnegd ⊢ ( 𝜑 → - - ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐴 − 𝐷 ) ) = ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐴 − 𝐷 ) ) )
24 neg0 ⊢ - 0 = 0
25 24 a1i ⊢ ( 𝜑 → - 0 = 0 )
26 20 23 25 3eqtr3d ⊢ ( 𝜑 → ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐴 − 𝐷 ) ) = 0 )
27 26 oveq2d ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐴 − 𝐶 ) ) − ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐴 − 𝐷 ) ) ) = ( ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐴 − 𝐶 ) ) − 0 ) )
28 10 11 jca ⊢ ( 𝜑 → ( ( 𝐵 − 𝐷 ) ∈ ℂ ∧ ( 𝐴 − 𝐶 ) ∈ ℂ ) )
29 1 28 sigarimcd ⊢ ( 𝜑 → ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐴 − 𝐶 ) ) ∈ ℂ )
30 29 subid1d ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐴 − 𝐶 ) ) − 0 ) = ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐴 − 𝐶 ) ) )
31 15 27 30 3eqtrd ⊢ ( 𝜑 → ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐷 − 𝐶 ) ) = ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐴 − 𝐶 ) ) )
32 9 6 5 nnncan2d ⊢ ( 𝜑 → ( ( 𝐵 − 𝐶 ) − ( 𝐷 − 𝐶 ) ) = ( 𝐵 − 𝐷 ) )
33 32 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝐶 ) − ( 𝐷 − 𝐶 ) ) 𝐺 ( 𝐴 − 𝐶 ) ) = ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐴 − 𝐶 ) ) )
34 9 5 subcld ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) ∈ ℂ )
35 6 5 subcld ⊢ ( 𝜑 → ( 𝐷 − 𝐶 ) ∈ ℂ )
36 1 sigarmf ⊢ ( ( ( 𝐵 − 𝐶 ) ∈ ℂ ∧ ( 𝐴 − 𝐶 ) ∈ ℂ ∧ ( 𝐷 − 𝐶 ) ∈ ℂ ) → ( ( ( 𝐵 − 𝐶 ) − ( 𝐷 − 𝐶 ) ) 𝐺 ( 𝐴 − 𝐶 ) ) = ( ( ( 𝐵 − 𝐶 ) 𝐺 ( 𝐴 − 𝐶 ) ) − ( ( 𝐷 − 𝐶 ) 𝐺 ( 𝐴 − 𝐶 ) ) ) )
37 34 11 35 36 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝐶 ) − ( 𝐷 − 𝐶 ) ) 𝐺 ( 𝐴 − 𝐶 ) ) = ( ( ( 𝐵 − 𝐶 ) 𝐺 ( 𝐴 − 𝐶 ) ) − ( ( 𝐷 − 𝐶 ) 𝐺 ( 𝐴 − 𝐶 ) ) ) )
38 31 33 37 3eqtr2rd ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝐶 ) 𝐺 ( 𝐴 − 𝐶 ) ) − ( ( 𝐷 − 𝐶 ) 𝐺 ( 𝐴 − 𝐶 ) ) ) = ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐷 − 𝐶 ) ) )
39 5 6 subcld ⊢ ( 𝜑 → ( 𝐶 − 𝐷 ) ∈ ℂ )
40 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
41 40 renegcld ⊢ ( 𝜑 → - 1 ∈ ℝ )
42 1 sigarls ⊢ ( ( ( 𝐵 − 𝐷 ) ∈ ℂ ∧ ( 𝐶 − 𝐷 ) ∈ ℂ ∧ - 1 ∈ ℝ ) → ( ( 𝐵 − 𝐷 ) 𝐺 ( ( 𝐶 − 𝐷 ) · - 1 ) ) = ( ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐶 − 𝐷 ) ) · - 1 ) )
43 10 39 41 42 syl3anc ⊢ ( 𝜑 → ( ( 𝐵 − 𝐷 ) 𝐺 ( ( 𝐶 − 𝐷 ) · - 1 ) ) = ( ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐶 − 𝐷 ) ) · - 1 ) )
44 39 mulm1d ⊢ ( 𝜑 → ( - 1 · ( 𝐶 − 𝐷 ) ) = - ( 𝐶 − 𝐷 ) )
45 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
46 45 negcld ⊢ ( 𝜑 → - 1 ∈ ℂ )
47 46 39 mulcomd ⊢ ( 𝜑 → ( - 1 · ( 𝐶 − 𝐷 ) ) = ( ( 𝐶 − 𝐷 ) · - 1 ) )
48 5 6 negsubdi2d ⊢ ( 𝜑 → - ( 𝐶 − 𝐷 ) = ( 𝐷 − 𝐶 ) )
49 44 47 48 3eqtr3d ⊢ ( 𝜑 → ( ( 𝐶 − 𝐷 ) · - 1 ) = ( 𝐷 − 𝐶 ) )
50 49 oveq2d ⊢ ( 𝜑 → ( ( 𝐵 − 𝐷 ) 𝐺 ( ( 𝐶 − 𝐷 ) · - 1 ) ) = ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐷 − 𝐶 ) ) )
51 10 39 jca ⊢ ( 𝜑 → ( ( 𝐵 − 𝐷 ) ∈ ℂ ∧ ( 𝐶 − 𝐷 ) ∈ ℂ ) )
52 1 51 sigarimcd ⊢ ( 𝜑 → ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐶 − 𝐷 ) ) ∈ ℂ )
53 52 mulm1d ⊢ ( 𝜑 → ( - 1 · ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐶 − 𝐷 ) ) ) = - ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐶 − 𝐷 ) ) )
54 52 46 mulcomd ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐶 − 𝐷 ) ) · - 1 ) = ( - 1 · ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐶 − 𝐷 ) ) ) )
55 1 sigarac ⊢ ( ( ( 𝐶 − 𝐷 ) ∈ ℂ ∧ ( 𝐵 − 𝐷 ) ∈ ℂ ) → ( ( 𝐶 − 𝐷 ) 𝐺 ( 𝐵 − 𝐷 ) ) = - ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐶 − 𝐷 ) ) )
56 39 10 55 syl2anc ⊢ ( 𝜑 → ( ( 𝐶 − 𝐷 ) 𝐺 ( 𝐵 − 𝐷 ) ) = - ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐶 − 𝐷 ) ) )
57 53 54 56 3eqtr4d ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐶 − 𝐷 ) ) · - 1 ) = ( ( 𝐶 − 𝐷 ) 𝐺 ( 𝐵 − 𝐷 ) ) )
58 43 50 57 3eqtr3d ⊢ ( 𝜑 → ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐷 − 𝐶 ) ) = ( ( 𝐶 − 𝐷 ) 𝐺 ( 𝐵 − 𝐷 ) ) )
59 1 sigarperm ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( 𝐶 − 𝐷 ) 𝐺 ( 𝐵 − 𝐷 ) ) = ( ( 𝐵 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) )
60 5 9 6 59 syl3anc ⊢ ( 𝜑 → ( ( 𝐶 − 𝐷 ) 𝐺 ( 𝐵 − 𝐷 ) ) = ( ( 𝐵 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) )
61 38 58 60 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝐶 ) 𝐺 ( 𝐴 − 𝐶 ) ) − ( ( 𝐷 − 𝐶 ) 𝐺 ( 𝐴 − 𝐶 ) ) ) = ( ( 𝐵 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) )