Theorem sigarexp

Description: Expand the signed area formula by linearity. (Contributed by Saveliy Skresanov, 20-Sep-2017)

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

Proof

Step	Hyp	Ref	Expression
1		sigar	⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
2		simp2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ℂ )
3		simp3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐶 ∈ ℂ )
4	2 3	subcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 − 𝐶 ) ∈ ℂ )
5	1	sigarmf	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 − 𝐶 ) ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = ( ( 𝐴 𝐺 ( 𝐵 − 𝐶 ) ) − ( 𝐶 𝐺 ( 𝐵 − 𝐶 ) ) ) )
6	4 5	syld3an2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = ( ( 𝐴 𝐺 ( 𝐵 − 𝐶 ) ) − ( 𝐶 𝐺 ( 𝐵 − 𝐶 ) ) ) )
7	1	sigarms	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 𝐺 ( 𝐵 − 𝐶 ) ) = ( ( 𝐴 𝐺 𝐵 ) − ( 𝐴 𝐺 𝐶 ) ) )
8	7	oveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 𝐺 ( 𝐵 − 𝐶 ) ) − ( 𝐶 𝐺 ( 𝐵 − 𝐶 ) ) ) = ( ( ( 𝐴 𝐺 𝐵 ) − ( 𝐴 𝐺 𝐶 ) ) − ( 𝐶 𝐺 ( 𝐵 − 𝐶 ) ) ) )
9	1	sigarms	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 𝐺 ( 𝐵 − 𝐶 ) ) = ( ( 𝐶 𝐺 𝐵 ) − ( 𝐶 𝐺 𝐶 ) ) )
10	3 9	syld3an1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 𝐺 ( 𝐵 − 𝐶 ) ) = ( ( 𝐶 𝐺 𝐵 ) − ( 𝐶 𝐺 𝐶 ) ) )
11	1	sigarid	⊢ ( 𝐶 ∈ ℂ → ( 𝐶 𝐺 𝐶 ) = 0 )
12	3 11	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 𝐺 𝐶 ) = 0 )
13	12	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐶 𝐺 𝐵 ) − ( 𝐶 𝐺 𝐶 ) ) = ( ( 𝐶 𝐺 𝐵 ) − 0 ) )
14	1	sigarim	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐶 𝐺 𝐵 ) ∈ ℝ )
15	14	recnd	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐶 𝐺 𝐵 ) ∈ ℂ )
16	3 2 15	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 𝐺 𝐵 ) ∈ ℂ )
17	16	subid1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐶 𝐺 𝐵 ) − 0 ) = ( 𝐶 𝐺 𝐵 ) )
18	10 13 17	3eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 𝐺 ( 𝐵 − 𝐶 ) ) = ( 𝐶 𝐺 𝐵 ) )
19	18	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 𝐺 𝐵 ) − ( 𝐴 𝐺 𝐶 ) ) − ( 𝐶 𝐺 ( 𝐵 − 𝐶 ) ) ) = ( ( ( 𝐴 𝐺 𝐵 ) − ( 𝐴 𝐺 𝐶 ) ) − ( 𝐶 𝐺 𝐵 ) ) )
20	6 8 19	3eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = ( ( ( 𝐴 𝐺 𝐵 ) − ( 𝐴 𝐺 𝐶 ) ) − ( 𝐶 𝐺 𝐵 ) ) )