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 ( 𝜑 → ( ( ( 𝐵𝐶 ) 𝐺 ( 𝐴𝐶 ) ) − ( ( 𝐷𝐶 ) 𝐺 ( 𝐴𝐶 ) ) ) = ( ( 𝐵𝐶 ) 𝐺 ( 𝐷𝐶 ) ) )