Metamath Proof Explorer

Theorem sigarac

Description: Signed area is anticommutative. (Contributed by Saveliy Skresanov, 19-Sep-2017)

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

Proof

Step Hyp Ref Expression
1 sigar ⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
2 1 sigarval ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 𝐺 𝐵 ) = ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) )
3 cjcl ⊢ ( 𝐵 ∈ ℂ → ( ∗ ‘ 𝐵 ) ∈ ℂ )
4 3 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ 𝐵 ) ∈ ℂ )
5 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ )
6 4 5 cjmuld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( ( ∗ ‘ 𝐵 ) · 𝐴 ) ) = ( ( ∗ ‘ ( ∗ ‘ 𝐵 ) ) · ( ∗ ‘ 𝐴 ) ) )
7 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
8 7 cjcjd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( ∗ ‘ 𝐵 ) ) = 𝐵 )
9 8 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ∗ ‘ ( ∗ ‘ 𝐵 ) ) · ( ∗ ‘ 𝐴 ) ) = ( 𝐵 · ( ∗ ‘ 𝐴 ) ) )
10 5 cjcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ 𝐴 ) ∈ ℂ )
11 7 10 mulcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 · ( ∗ ‘ 𝐴 ) ) = ( ( ∗ ‘ 𝐴 ) · 𝐵 ) )
12 6 9 11 3eqtrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ∗ ‘ 𝐴 ) · 𝐵 ) = ( ∗ ‘ ( ( ∗ ‘ 𝐵 ) · 𝐴 ) ) )
13 12 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) = ( ℑ ‘ ( ∗ ‘ ( ( ∗ ‘ 𝐵 ) · 𝐴 ) ) ) )
14 4 5 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ∗ ‘ 𝐵 ) · 𝐴 ) ∈ ℂ )
15 14 imcjd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ ( ∗ ‘ ( ( ∗ ‘ 𝐵 ) · 𝐴 ) ) ) = - ( ℑ ‘ ( ( ∗ ‘ 𝐵 ) · 𝐴 ) ) )
16 2 13 15 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 𝐺 𝐵 ) = - ( ℑ ‘ ( ( ∗ ‘ 𝐵 ) · 𝐴 ) ) )
17 1 sigarval ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝐵 𝐺 𝐴 ) = ( ℑ ‘ ( ( ∗ ‘ 𝐵 ) · 𝐴 ) ) )
18 17 ancoms ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 𝐺 𝐴 ) = ( ℑ ‘ ( ( ∗ ‘ 𝐵 ) · 𝐴 ) ) )
19 18 negeqd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - ( 𝐵 𝐺 𝐴 ) = - ( ℑ ‘ ( ( ∗ ‘ 𝐵 ) · 𝐴 ) ) )
20 16 19 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 𝐺 𝐵 ) = - ( 𝐵 𝐺 𝐴 ) )