Metamath Proof Explorer

Theorem sigaras

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

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

Proof

Step Hyp Ref Expression
1 sigar ⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
2 simp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐴 ∈ ℂ )
3 simp2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ℂ )
4 simp3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐶 ∈ ℂ )
5 3 4 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 + 𝐶 ) ∈ ℂ )
6 1 sigarac ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 + 𝐶 ) ∈ ℂ ) → ( 𝐴 𝐺 ( 𝐵 + 𝐶 ) ) = - ( ( 𝐵 + 𝐶 ) 𝐺 𝐴 ) )
7 2 5 6 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 ( 𝐵 + 𝐶 ) ) = - ( ( 𝐵 + 𝐶 ) 𝐺 𝐴 ) )
8 1 sigaraf ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 + 𝐶 ) 𝐺 𝐴 ) = ( ( 𝐵 𝐺 𝐴 ) + ( 𝐶 𝐺 𝐴 ) ) )
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 15 20 negdid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → - ( ( 𝐵 𝐺 𝐴 ) + ( 𝐶 𝐺 𝐴 ) ) = ( - ( 𝐵 𝐺 𝐴 ) + - ( 𝐶 𝐺 𝐴 ) ) )
22 10 21 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → - ( ( 𝐵 + 𝐶 ) 𝐺 𝐴 ) = ( - ( 𝐵 𝐺 𝐴 ) + - ( 𝐶 𝐺 𝐴 ) ) )
23 1 sigarac ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 𝐺 𝐵 ) = - ( 𝐵 𝐺 𝐴 ) )
24 2 3 23 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 𝐵 ) = - ( 𝐵 𝐺 𝐴 ) )
25 24 eqcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → - ( 𝐵 𝐺 𝐴 ) = ( 𝐴 𝐺 𝐵 ) )
26 1 sigarac ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 𝐶 ) = - ( 𝐶 𝐺 𝐴 ) )
27 2 4 26 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 𝐶 ) = - ( 𝐶 𝐺 𝐴 ) )
28 27 eqcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → - ( 𝐶 𝐺 𝐴 ) = ( 𝐴 𝐺 𝐶 ) )
29 25 28 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( - ( 𝐵 𝐺 𝐴 ) + - ( 𝐶 𝐺 𝐴 ) ) = ( ( 𝐴 𝐺 𝐵 ) + ( 𝐴 𝐺 𝐶 ) ) )
30 7 22 29 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 𝐺 𝐵 ) + ( 𝐴 𝐺 𝐶 ) ) )