Metamath Proof Explorer

Theorem sigarms

Description: Signed area is additive (with respect to subtraction) by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017)

Ref Expression
Hypothesis sigar ⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
Assertion sigarms ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 ( 𝐵 − 𝐶 ) ) = ( ( 𝐴 𝐺 𝐵 ) − ( 𝐴 𝐺 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 sigar ⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
2 simp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐴 ∈ ℂ )
3 simp2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ℂ )
4 simp3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐶 ∈ ℂ )
5 3 4 subcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 − 𝐶 ) ∈ ℂ )
6 1 sigarac ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 − 𝐶 ) ∈ ℂ ) → ( 𝐴 𝐺 ( 𝐵 − 𝐶 ) ) = - ( ( 𝐵 − 𝐶 ) 𝐺 𝐴 ) )
7 2 5 6 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 ( 𝐵 − 𝐶 ) ) = - ( ( 𝐵 − 𝐶 ) 𝐺 𝐴 ) )
8 1 sigarmf ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 − 𝐶 ) 𝐺 𝐴 ) = ( ( 𝐵 𝐺 𝐴 ) − ( 𝐶 𝐺 𝐴 ) ) )
9 8 negeqd ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → - ( ( 𝐵 − 𝐶 ) 𝐺 𝐴 ) = - ( ( 𝐵 𝐺 𝐴 ) − ( 𝐶 𝐺 𝐴 ) ) )
10 9 3com12 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → - ( ( 𝐵 − 𝐶 ) 𝐺 𝐴 ) = - ( ( 𝐵 𝐺 𝐴 ) − ( 𝐶 𝐺 𝐴 ) ) )
11 3simpa ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) )
12 11 ancomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
13 1 sigarim ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝐵 𝐺 𝐴 ) ∈ ℝ )
14 12 13 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 𝐺 𝐴 ) ∈ ℝ )
15 14 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 𝐺 𝐴 ) ∈ ℂ )
16 3simpb ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
17 16 ancomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
18 1 sigarim ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝐶 𝐺 𝐴 ) ∈ ℝ )
19 17 18 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 𝐺 𝐴 ) ∈ ℝ )
20 19 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 𝐺 𝐴 ) ∈ ℂ )
21 negsubdi ⊢ ( ( ( 𝐵 𝐺 𝐴 ) ∈ ℂ ∧ ( 𝐶 𝐺 𝐴 ) ∈ ℂ ) → - ( ( 𝐵 𝐺 𝐴 ) − ( 𝐶 𝐺 𝐴 ) ) = ( - ( 𝐵 𝐺 𝐴 ) + ( 𝐶 𝐺 𝐴 ) ) )
22 simpl ⊢ ( ( ( 𝐵 𝐺 𝐴 ) ∈ ℂ ∧ ( 𝐶 𝐺 𝐴 ) ∈ ℂ ) → ( 𝐵 𝐺 𝐴 ) ∈ ℂ )
23 22 negcld ⊢ ( ( ( 𝐵 𝐺 𝐴 ) ∈ ℂ ∧ ( 𝐶 𝐺 𝐴 ) ∈ ℂ ) → - ( 𝐵 𝐺 𝐴 ) ∈ ℂ )
24 simpr ⊢ ( ( ( 𝐵 𝐺 𝐴 ) ∈ ℂ ∧ ( 𝐶 𝐺 𝐴 ) ∈ ℂ ) → ( 𝐶 𝐺 𝐴 ) ∈ ℂ )
25 23 24 subnegd ⊢ ( ( ( 𝐵 𝐺 𝐴 ) ∈ ℂ ∧ ( 𝐶 𝐺 𝐴 ) ∈ ℂ ) → ( - ( 𝐵 𝐺 𝐴 ) − - ( 𝐶 𝐺 𝐴 ) ) = ( - ( 𝐵 𝐺 𝐴 ) + ( 𝐶 𝐺 𝐴 ) ) )
26 21 25 eqtr4d ⊢ ( ( ( 𝐵 𝐺 𝐴 ) ∈ ℂ ∧ ( 𝐶 𝐺 𝐴 ) ∈ ℂ ) → - ( ( 𝐵 𝐺 𝐴 ) − ( 𝐶 𝐺 𝐴 ) ) = ( - ( 𝐵 𝐺 𝐴 ) − - ( 𝐶 𝐺 𝐴 ) ) )
27 15 20 26 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → - ( ( 𝐵 𝐺 𝐴 ) − ( 𝐶 𝐺 𝐴 ) ) = ( - ( 𝐵 𝐺 𝐴 ) − - ( 𝐶 𝐺 𝐴 ) ) )
28 10 27 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → - ( ( 𝐵 − 𝐶 ) 𝐺 𝐴 ) = ( - ( 𝐵 𝐺 𝐴 ) − - ( 𝐶 𝐺 𝐴 ) ) )
29 1 sigarac ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 𝐺 𝐵 ) = - ( 𝐵 𝐺 𝐴 ) )
30 2 3 29 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 𝐵 ) = - ( 𝐵 𝐺 𝐴 ) )
31 30 eqcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → - ( 𝐵 𝐺 𝐴 ) = ( 𝐴 𝐺 𝐵 ) )
32 1 sigarac ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 𝐶 ) = - ( 𝐶 𝐺 𝐴 ) )
33 2 4 32 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 𝐶 ) = - ( 𝐶 𝐺 𝐴 ) )
34 33 eqcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → - ( 𝐶 𝐺 𝐴 ) = ( 𝐴 𝐺 𝐶 ) )
35 31 34 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( - ( 𝐵 𝐺 𝐴 ) − - ( 𝐶 𝐺 𝐴 ) ) = ( ( 𝐴 𝐺 𝐵 ) − ( 𝐴 𝐺 𝐶 ) ) )
36 7 28 35 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 ( 𝐵 − 𝐶 ) ) = ( ( 𝐴 𝐺 𝐵 ) − ( 𝐴 𝐺 𝐶 ) ) )