Metamath Proof Explorer

Theorem sigarmf

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

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

Proof

Step Hyp Ref Expression
1 sigar ⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
2 cjsub ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ∗ ‘ ( 𝐴 − 𝐶 ) ) = ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) )
3 2 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ∗ ‘ ( 𝐴 − 𝐶 ) ) · 𝐵 ) = ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · 𝐵 ) )
4 3 3adant2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ∗ ‘ ( 𝐴 − 𝐶 ) ) · 𝐵 ) = ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · 𝐵 ) )
5 simp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐴 ∈ ℂ )
6 5 cjcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ∗ ‘ 𝐴 ) ∈ ℂ )
7 simp3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐶 ∈ ℂ )
8 7 cjcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ∗ ‘ 𝐶 ) ∈ ℂ )
9 simp2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ℂ )
10 6 8 9 subdird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · 𝐵 ) = ( ( ( ∗ ‘ 𝐴 ) · 𝐵 ) − ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ) )
11 4 10 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ∗ ‘ ( 𝐴 − 𝐶 ) ) · 𝐵 ) = ( ( ( ∗ ‘ 𝐴 ) · 𝐵 ) − ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ) )
12 11 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ℑ ‘ ( ( ∗ ‘ ( 𝐴 − 𝐶 ) ) · 𝐵 ) ) = ( ℑ ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐵 ) − ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ) ) )
13 6 9 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ∈ ℂ )
14 8 9 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ∈ ℂ )
15 13 14 imsubd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ℑ ‘ ( ( ( ∗ ‘ 𝐴 ) · 𝐵 ) − ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ) ) = ( ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) − ( ℑ ‘ ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ) ) )
16 12 15 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ℑ ‘ ( ( ∗ ‘ ( 𝐴 − 𝐶 ) ) · 𝐵 ) ) = ( ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) − ( ℑ ‘ ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ) ) )
17 5 7 subcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 − 𝐶 ) ∈ ℂ )
18 1 sigarval ⊢ ( ( ( 𝐴 − 𝐶 ) ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 − 𝐶 ) 𝐺 𝐵 ) = ( ℑ ‘ ( ( ∗ ‘ ( 𝐴 − 𝐶 ) ) · 𝐵 ) ) )
19 17 9 18 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐶 ) 𝐺 𝐵 ) = ( ℑ ‘ ( ( ∗ ‘ ( 𝐴 − 𝐶 ) ) · 𝐵 ) ) )
20 1 sigarval ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 𝐺 𝐵 ) = ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) )
21 20 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 𝐵 ) = ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) )
22 3simpc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
23 22 ancomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) )
24 1 sigarval ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐶 𝐺 𝐵 ) = ( ℑ ‘ ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ) )
25 23 24 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 𝐺 𝐵 ) = ( ℑ ‘ ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ) )
26 21 25 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 𝐺 𝐵 ) − ( 𝐶 𝐺 𝐵 ) ) = ( ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) − ( ℑ ‘ ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ) ) )
27 16 19 26 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐶 ) 𝐺 𝐵 ) = ( ( 𝐴 𝐺 𝐵 ) − ( 𝐶 𝐺 𝐵 ) ) )