Metamath Proof Explorer

Theorem sigaraf

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

Ref Expression
Hypothesis sigar ⊢G=x∈ℂ,y∈ℂ⟼ℑ⁡x‾⁢y
Assertion sigaraf ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A+CGB=AGB+CGB

Proof

Step Hyp Ref Expression
1 sigar ⊢G=x∈ℂ,y∈ℂ⟼ℑ⁡x‾⁢y
2 cjadd ⊢A∈ℂ∧C∈ℂ→A+C‾=A‾+C‾
3 2 oveq1d ⊢A∈ℂ∧C∈ℂ→A+C‾⁢B=A‾+C‾⁢B
4 3 3adant2 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A+C‾⁢B=A‾+C‾⁢B
5 simp1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A∈ℂ
6 5 cjcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A‾∈ℂ
7 simp3 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→C∈ℂ
8 7 cjcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→C‾∈ℂ
9 simp2 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B∈ℂ
10 6 8 9 adddird ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A‾+C‾⁢B=A‾⁢B+C‾⁢B
11 4 10 eqtrd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A+C‾⁢B=A‾⁢B+C‾⁢B
12 11 fveq2d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→ℑ⁡A+C‾⁢B=ℑ⁡A‾⁢B+C‾⁢B
13 6 9 mulcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A‾⁢B∈ℂ
14 8 9 mulcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→C‾⁢B∈ℂ
15 13 14 imaddd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→ℑ⁡A‾⁢B+C‾⁢B=ℑ⁡A‾⁢B+ℑ⁡C‾⁢B
16 12 15 eqtrd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→ℑ⁡A+C‾⁢B=ℑ⁡A‾⁢B+ℑ⁡C‾⁢B
17 5 7 addcld ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A+C∈ℂ
18 1 sigarval ⊢A+C∈ℂ∧B∈ℂ→A+CGB=ℑ⁡A+C‾⁢B
19 17 9 18 syl2anc ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A+CGB=ℑ⁡A+C‾⁢B
20 1 sigarval ⊢A∈ℂ∧B∈ℂ→AGB=ℑ⁡A‾⁢B
21 20 3adant3 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→AGB=ℑ⁡A‾⁢B
22 3simpc ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B∈ℂ∧C∈ℂ
23 22 ancomd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→C∈ℂ∧B∈ℂ
24 1 sigarval ⊢C∈ℂ∧B∈ℂ→CGB=ℑ⁡C‾⁢B
25 23 24 syl ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→CGB=ℑ⁡C‾⁢B
26 21 25 oveq12d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→AGB+CGB=ℑ⁡A‾⁢B+ℑ⁡C‾⁢B
27 16 19 26 3eqtr4d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A+CGB=AGB+CGB